Counting CTL
Fran\c{c}ois Laroussinie (Universit\'e Paris Diderot - Paris 7),, Antoine Meyer (Universit\'e Paris Est - Marne-la-Vall\'ee), Eudes Petonnet, (Universit\'e Paris Diderot - Paris 7)
TL;DR
This paper introduces quantitative extensions to CTL, enabling constraints on the number of states satisfying sub-formulas, and analyzes their expressiveness, complexity, and variants.
Contribution
It develops new logics extending CTL with counting constraints, analyzes their properties, and compares different variants.
Findings
Several logics generalizing CTL are proposed.
Complexity ranges from P-complete to undecidable.
Two alternative logics with similar features are analyzed.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.