Paper Info
Title
On the complexity of verifying regular properties on flat counter systems,
Abstract
Among the approximation methods for the verification of counter systems, one of them consists in model-checking their flat unfoldings. Unfortunately, the complexity characterization of model-checking problems for such operational models is not always well studied except for reachability queries or for Past LTL. In this paper, we characterize the complexity of model-checking problems on flat counter systems for the specification languages including first-order logic, linear mu-calculus, infinite automata, and related formalisms. Our results span different complexity classes (mainly from PTime to PSpace) and they apply to languages in which arithmetical constraints on counter values are systematically allowed. As far as the proof techniques are concerned, we provide a uniform approach that focuses on the main issues.
Year
DOI
Venue
2013
10.1007/978-3-642-39212-2_17
ICALP'11 Proceedings of the 38th international conference on Automata, languages and programming - Volume Part II
Keywords
DocType
Volume
regular property,flat unfoldings,flat counter system,counter system,different complexity class,counter value,arithmetical constraint,model-checking problem,approximation method,complexity characterization,Past LTL
Conference
abs/1304.6301
ISSN
Citations 
PageRank 
0302-9743
1
0.35
References 
Authors
14
3
Name
Order
Citations
PageRank
Stéphane Demri183260.65
Amit Kumar Dhar2172.71
Arnaud Sangnier323617.99