2013/04/23 by Stéphane Demri, Demri, Stéphane, Amit Kumar Dhar +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1304.6301
openalex publication_date 2013/04/23 · openalex created_date 2021/05/24 · openalex updated_date 2026/07/28
Among the approximation methods for the verification of counter systems, one\nof them consists in model-checking their flat unfoldings. Unfortunately, the\ncomplexity characterization of model-checking problems for such operational\nmodels is not always well studied except for reachability queries or for Past\nLTL. In this paper, we characterize the complexity of model-checking problems\non flat counter systems for the specification languages including first-order\nlogic, linear mu-calculus, infinite automata, and related formalisms. Our\nresults span different complexity classes (mainly from PTime to PSpace) and\nthey apply to languages in which arithmetical constraints on counter values are\nsystematically allowed. As far as the proof techniques are concerned, we\nprovide a uniform approach that focuses on the main issues.\n