Satisfiability of ECTL^ with constraints
This paper presents a study of a certain extension of the full computation tree logic \textsf{CTL}* by eliminating the path formulas and replacing the temporal operators by a general framework of automata. The resulting extended computation tree logic \textsf{ECTL}* thus has no syntactic restrictions on the applications of temporal operators and path quantifiers, and can describe regular (i.e., \textsf{MSO}-definable) properties of paths. While the original formulation of \textsf{ECTL}* makes use of the Büchi automata, the paper under review replaces the classical \textsf{CTL}* path formulas by \textsf{MSO}-formulas. As the main result, the authors prove that satisfiability and finite satisfiability for \textsf{ECTL}* with certain constraints over \(\mathbb{Z}\) are decidable. It is also shown that the choice of the mentioned constraints in the form of certain path formulas is necessary for the result.
- Satisfiability of \(\mathsf {ECTL}^*\) with tree constraints
- Satisfiability of \(\mathrm{CTL}^{*}\) with constraints
- Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints
- Completeness of the bounded satisfiability problem for constraint LTL
- Constraint Satisfaction, Bounded Treewidth, and Finite-Variable Logics
- Satisfiability, branch-width and Tseitin tautologies
- Satisfiability of acyclic and almost acyclic CNF formulas
- Satisfiability of acyclic and almost acyclic CNF formulas
- Bounded satisfiability for PCTL
- Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction
- A finite model theorem for the propositional \(\mu\)-calculus
- A tableau algorithm for description logics with concrete domains and general TBoxes
- An automata-based approach for \(\text{CTL}^{*}\) with constraints
- An automata-theoretic approach to constraint LTL
- Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
- Combining interval-based temporal reasoning with general TBoxes
- CTL^* and ECTL^* as fragments of the modal -calculus
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Deciding properties of integral relational automata
- Foundations of Software Science and Computation Structures
- scientific article; zbMATH DE number 3876574 (Why is no real title available?)
- scientific article; zbMATH DE number 1122449 (Why is no real title available?)
- scientific article; zbMATH DE number 4119650 (Why is no real title available?)
- scientific article; zbMATH DE number 2196595 (Why is no real title available?)
- LTL with the freeze quantifier and register automata
- Monadic second-order definable graph transductions: a survey
- Monadic second-order logic on tree-like structures
- NExpTime-complete description logics with concrete domains
- On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
- Satisfiability of \(\mathrm{CTL}^{*}\) with constraints
- Satisfiability of \(\mathsf {ECTL}^*\) with tree constraints
- Temporal logic can be more expressive
- Temporal logics on strings with prefix relation
- The Complexity of Tree Automata and Logics of Programs
- Verification of qualitative \(\mathbb Z\) constraints
- Weak \(\text{MSO}+U\) over infinite trees
- CTL* model checking for data-aware dynamic systems with arithmetic
- Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints
- Satisfiability of \(\mathrm{CTL}^{*}\) with constraints
- Satisfiability of \(\mathsf {ECTL}^*\) with tree constraints
- scientific article; zbMATH DE number 4119650 (Why is no real title available?)
- An automata-based approach for \(\text{CTL}^{*}\) with constraints
- Temporal logics with local constraints (invited talk)
- First steps towards taming description logics with strings
- Constraint automata on infinite data trees: from \(\mathrm{CTL}(\mathbb{Z})/\mathrm{CTL}^*(\mathbb{Z})\) to decision procedures
- Constraint automata on infinite data trees: from CTL\((\mathbb{Z})\text{CTL}^*(\mathbb{Z})\) to decision procedures
- Reachability and bounded emptiness problems of constraint automata with prefix, suffix and infix
This page was built for publication: Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q269503)
