Counter Systems and Temporal Logics





Course information

The course has two parts. The first part is going to be held in Buenos Aires, at the Computer Science Department. The second part of the course is going to be in Córdoba, at the FaMAF. Each part is a three-day course.
  • Part I (in Buenos Aires): October 26, 28 and 29, 15-17hs.
  • Part II (in Córdoba): November 1, 2 and 3.

Professor

Stèphane Demri - Senior Researcher, CNRS, Cachan, France [Home page]

Plan of lectures about counter systems and temporal logics

[Ln] means "this part is strongly related to the material of lecture n of the ESSLI'10 course described here". Observe that each series of slides can cover a two-hour lecture (I did not present everything at ESSLLI'10) and therefore I will make a selection of topics covered here.

Part I: Counter systems

Lecture 1: Introduction to counter systems [L1]
  • 1.1 Example
  • 1.2 Presburger arithmetic
  • 1.3 Counter systems
  • 1.4 A selection of subclasses
Lecture 2: Classes with semilinear reachability sets
  • 2.1 Relational counter systems [L1]
  • 2.2 Reversal-bounded counter automata [L4]
  • 2.3 Flat relational counter automata [L5]
Lecture 3: Vector addition systems with states [L3]
  • 3.1 Relationships with Petri nets
  • 3.2 Coverability graphs
  • 3.3 Complexity issues

Part II: Logics for counter systems

Lecture 4: Linear-time temporal logics [L2]
  • 4.1 Basics on LTL
  • 4.2 LTL for counter systems
  • 4.3 Fragments
Lecture 5: Model-checking counter systems [L5]
  • 5.1 Control state repeated reachability problem
  • 5.2 Decidable fragments thanks to semilinearity
Lecture 6: Data logics and counters
  • 6.1 Introduction to data logics
  • 6.2 Reduction between data logics and verification problems for counter systems

Bibliography

Here is a possible list of articles to read before the lectures. Of course, I will treat only part of the material there with other topics.

Related to 2.2:
@Article{Ibarra78,
author={O. Ibarra},
title={Reversal-bounded multicounter machines and their decision problems},
journal={JACM},
year={1978},
volume={25},
number={1},
pages={116-133},
}

Related to 2.2:
@inproceedings{Finkel&Sangnier08,
author={A. Finkel and A. Sangnier},
booktitle={MFCS'08},
publisher={Springer},
series={LNCS},
title={Reversal-Bounded Counter Machines Revisited},
volume={5162},
pages={323-334},
year={2008},
}

Related to 2.3:
@InProceedings{Leroux&Sutre05,
author={J. Leroux and G. Sutre},
title={Flat counter systems are everywhere!},
booktitle={ATVA'05},
pages={489-503},
year={2005},
OPTeditor={D. Peled and Y.K. Tsay},
volume={3707},
series={LNCS},
publisher={Springer},
}

Related to 3.1 (Survey paper on Petri nets):
@inproceedings{Esparza98,
author={J. Esparza},
title={Decidability and Complexity of Petri Net Problems - An Introduction},
booktitle={Advances in Petri Nets 1998},
pages={374-428},
year={1998},
volume={1491},
series={LNCS},
publisher={Springer, Berlin},
}

Related to 3.3:
@article{Rackoff78,
author={C. Rackoff},
title={The covering and boundedness problems for vector addition systems},
journal={TCS},
pages={223-231},
year={1978},
volume={6},
number={2},
}

Related to 3.3:
@InProceedings{Faouzi&Habermehl09,
author={M. Faouzi Atig and P. Habermehl},
title={On Yen's Path Logic for Petri Nets},
booktitle={RP'09},
pages={51-63},
year={2009},
volume={5797},
series={LNCS},
publisher={Springer},
}

Related to 4.2:
@InProceedings{Comon&Cortier00,
author={H. Comon and V. Cortier},
title={Flatness is not a weakness},
booktitle={CSL'00},
pages={262-276},
year={2000},
volume={1862},
series={LNCS},
publisher={Springer},
}

Related to 4.3 (about Freeze LTL):
@Article{Demri&Lazic&Nowak06,
author={S. Demri and R. Lazic and D. Nowak},
title={On the freeze quantifier in constraint LTL: decidability and complexity},
journal={IC},
year={2007},
volume={205},
number={1},
pages={2-24},
}

Related to 5.1 (translation from LTL formulae to Buchi automata):
@InProceedings{Wolper00,
author={P. Wolper},
title={Constructing Automata from Temporal Logic Formulas: A Tutorial},
booktitle={European Educational Forum: School on Formal Methods and Performance Analysis},
year={2000},
volume={2090},
pages={261-277},
OPTeditor={E. Brinksma and H. Hermanns and J.-P. Katoen},
series={LNCS},
publisher={Springer},
}

Related to 6.1: Survey paper on formalisms for structures with data:
@InProceedings{Segoufin06,
author={L. Segoufin},
title={Automata and Logics for Words and Trees over an Infinite Alphabet},
booktitle={CSL'06},
year={2006},
volume={4207},
pages={41-57},
series={LNCS},
publisher={Springer},
}