Author :
Laroussinie, François ; Meyer, Antoine ; Petonnet, Eudes
Author_Institution :
LIAFA, Univ. Paris Diderot - Paris 7, Paris, France
Abstract :
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.
Keywords :
computational complexity; decision making; formal verification; temporal logic; linear time temporal logic; model checking; Automata; Complexity theory; Computational modeling; Encoding; Lead; Polynomials; Semantics; counting; model-checking; satisfiability; temporal logic;
Conference_Titel :
Temporal Representation and Reasoning (TIME), 2010 17th International Symposium on
Conference_Location :
Paris
Print_ISBN :
978-1-4244-8014-2
DOI :
10.1109/TIME.2010.20
