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). © 2010 Springer-Verlag.
CITATION STYLE
Laroussinie, F., Meyer, A., & Petonnet, E. (2010). Counting CTL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6014 LNCS, pp. 206–220). https://doi.org/10.1007/978-3-642-12032-9_15
Mendeley helps you to discover research relevant for your work.