salle A. Turing CE4
1 March 2016 - 14h00
On the Complexity of Verifying Regular Properties on Flat Counter Systems
by Arnaud Sangnier from LIAFA PARIS 7
Abstract: Among the approximation methods for the verification of counter systems, one of them consists in model-checking their flat unfoldings. That is why, optimal algorithms for model-checking flat counter systems are being designed since this may represent the core of a verification process. Unfortunately, the complexity characterization of model-checking problems for such operational models is not always well studied except for reachability queries. In this work, we characterize the complexity of model-checking problems on flat counter systems for the specification languages including Past LTL, first-order logic, linear mu-calculus, infinite and related formalisms. Our results span different complexity classes (mainly from P 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.
This is a joint work with Stéphane Demri and Amit Kumar Dhar
