Selected publications at LSV: 2006

Abstract:
This paper deals with model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. We have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing translation of the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We have provided evidence that our results are close to optimal with respect to the class of counter systems described above. Finally, we design a complete semi-algorithm to verify first-order LTL properties over trace-flattable counter systems, extending the previous underlying FAST semi-algorithm to verify reachability questions over flattable counter systems.

@inproceedings{DDFG-atva06,
   address = {Beijing, China},
   author = {Demri, St{\'e}phane and Finkel, Alain and Goranko, Valentin and van Drimmelen, Govert},
   booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'06)},
   DOI = {10.1007/11901914_36},
   editor = {Graf, Susanne and Zhang, Wenhui},
   month = oct,
   pages = {493-507},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Towards a model-checker for counter systems},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf},
   volume = {4218},
   year = {2006},
}

About LSV