Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints

DOI10.1016/j.jcss.2016.02.002zbMath1358.03032OpenAlexW1644422701MaRDI QIDQ269503

Alexander Kartzow, Markus Lohrey, Claudia Carapelle

Publication date: 18 April 2016

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2016.02.002

zbMATH Keywords

decidabilitytemporal logicsatisfiabilitybounding quantifierscomputation tree logicextended computation tree logicinteger constraints

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Related Items (2)

Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints ⋮ CTL* model checking for data-aware dynamic systems with arithmetic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combining interval-based temporal reasoning with general TBoxes
• An automata-theoretic approach to constraint LTL
• A tableau algorithm for description logics with concrete domains and general TBoxes
• Verification of qualitative \(\mathbb Z\) constraints
• A finite model theorem for the propositional \(\mu\)-calculus
• Monadic second-order definable graph transductions: a survey
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• Monadic second-order logic on tree-like structures
• Temporal logics on strings with prefix relation
• Satisfiability of CTL* with Constraints
• LTL with the freeze quantifier and register automata
• Satisfiability of ECTL* with Tree Constraints
• Temporal logic can be more expressive
• The Complexity of Tree Automata and Logics of Programs
• Deciding properties of integral relational automata
• An Automata-based Approach for CTL⋆ With Constraints
• NEXP TIME-complete description logics with concrete domains
• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Foundations of Software Science and Computation Structures
• On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic

This page was built for publication: Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints