Counting CTL
Logic in Computer Science
2015-07-01 v4
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 succinctness, and of the complexity of their model-checking and satisfiability problems (ranging from P-complete to undecidable). Finally, we present two alternative logics with similar features and provide a comparative study of the properties of both variants.
Keywords
Cite
@article{arxiv.1211.4651,
title = {Counting CTL},
author = {François Laroussinie and Antoine Meyer and Eudes Petonnet},
journal= {arXiv preprint arXiv:1211.4651},
year = {2015}
}
Comments
34 pages