Counting LTL

François Laroussinie (1) , Antoine Meyer (2) , Eudes Petonnet (1)

1 LIAFA - Laboratoire d'informatique Algorithmique : Fondements et Applications
2 LIGM - Laboratoire d'Informatique Gaspard-Monge

This paper presents a quantitative extension for the linear-time temporal logic LTL allowing to specify the number of states satisfying certain sub-formulas along paths. We give decision procedures for the satisfiability and model checking of this new temporal logic and study the complexity of the corresponding problems. Furthermore we show that the problems become undecidable when more expressive constraints are considered.

Mots clés: temporal logic; ltl; expressiveness; model-checking; satisfiability

Domaines: Logique en informatique [cs.LO]

François Laroussinie, Antoine Meyer, Eudes Petonnet. Counting LTL. TIME 2010, Sep 2010, Paris, France. p. 51-58, ⟨10.1109/TIME.2010.20⟩. ⟨hal-00681267⟩