Satisfiability of CTL* with constraints
Claudia Carapelle, Alexander Kartzow, Markus Lohrey
TL;DR
This paper proves that the satisfiability problem for CTL* logic with various constraints over integers is decidable, extending known results beyond specific fragments to the full logic.
Contribution
It establishes the decidability of CTL* satisfiability with equality, order, and modulo constraints over integers, a significant extension of prior fragment-based results.
Findings
Decidability of CTL* with constraints over Z
Extension beyond known fragments like EF
Broader applicability of satisfiability results
Abstract
We show that satisfiability for CTL* with equality-, order-, and modulo-constraints over Z is decidable. Previously, decidability was only known for certain fragments of CTL*, e.g., the existential and positive fragments and EF.
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.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Natural Language Processing Techniques