Satisfiability of ECTL^ with constraints
DOI10.1016/J.JCSS.2016.02.002zbMATH Open1358.03032OpenAlexW1644422701MaRDI QIDQ269503FDOQ269503
Authors: Claudia Carapelle, Alexander Kartzow, Markus Lohrey
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
Recommendations
- 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
decidabilitysatisfiabilitybounding quantifierscomputation tree logicextended computation tree logicinteger constraintstemporal logic
Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Logic in computer science (03B70)
Cites Work
- Decidability of Second-Order Theories and Automata on Infinite Trees
- An automata-theoretic approach to constraint LTL
- 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 \(\mathrm{CTL}^{*}\) with constraints
- Weak \(\text{MSO}+U\) over infinite trees
- LTL with the freeze quantifier and register automata
- Satisfiability of \(\mathsf {ECTL}^*\) with tree constraints
- Temporal logic can be more expressive
- Title not available (Why is that?)
- The Complexity of Tree Automata and Logics of Programs
- Title not available (Why is that?)
- Deciding properties of integral relational automata
- Title not available (Why is that?)
- An automata-based approach for \(\text{CTL}^{*}\) with constraints
- NExpTime-complete description logics with concrete domains
- Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
- Title not available (Why is that?)
- Foundations of Software Science and Computation Structures
- On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
- Combining interval-based temporal reasoning with general TBoxes
- A tableau algorithm for description logics with concrete domains and general TBoxes
- Verification of qualitative \(\mathbb Z\) constraints
Cited In (8)
- CTL* model checking for data-aware dynamic systems with arithmetic
- Title not available (Why is that?)
- Satisfiability of \(\mathrm{CTL}^{*}\) with constraints
- Satisfiability of \(\mathsf {ECTL}^*\) with tree constraints
- An automata-based approach for \(\text{CTL}^{*}\) with constraints
- Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints
- First steps towards taming description logics with strings
- Temporal logics with local constraints (invited talk)
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)