Skip to Main content Skip to Navigation
Conference papers

Counting CTL

Abstract : This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct logics generalizing CTL. We provide a thorough analysis of their expressiveness and of the complexity of their model-checking problem (ranging from P-complete to undecidable).
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-00681263
Contributor : Antoine Meyer <>
Submitted on : Wednesday, March 21, 2012 - 9:43:56 AM
Last modification on : Wednesday, February 3, 2021 - 7:54:26 AM
Long-term archiving on: : Friday, June 22, 2012 - 2:21:13 AM

File

paper_41.pdf
Files produced by the author(s)

Identifiers

Citation

François Laroussinie, Antoine Meyer, Eudes Pétonnet. Counting CTL. FoSSaCS 2010, Mar 2010, Paphos, Cyprus. pp.206-220, ⟨10.1007/978-3-642-12032-9_15⟩. ⟨hal-00681263⟩

Share

Metrics

Record views

470

Files downloads

546