English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Among the approximation methods for the verification of counter systems, oneof them consists in model-checking their flat unfoldings. Unfortunately, thecomplexity characterization of model-checking problems for such operationalmodels is not always well studied except for reachability queries or for PastLTL. In this paper, we characterize the complexity of model-checking problemson flat counter systems for the specification languages including first-orderlogic, linear mu-calculus, infinite automata, and related formalisms. Ourresults span different complexity classes (mainly from PTime to PSpace) andthey apply to languages in which arithmetical constraints on counter values aresystematically allowed. As far as the proof techniques are concerned, weprovide a uniform approach that focuses on the main issues.

On the Complexity of Verifying Regular Properties on Flat Counter Systems