Skip to Main content Skip to Navigation
Conference papers

Counting LTL

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-00681267
Contributor : Antoine Meyer <>
Submitted on : Wednesday, March 21, 2012 - 9:55:38 AM
Last modification on : Wednesday, February 3, 2021 - 7:54:26 AM
Long-term archiving on: : Wednesday, December 14, 2016 - 5:18:01 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

539

Files downloads

671