Satisfiability of ECTL^ with constraints

DOI10.1016/J.JCSS.2016.02.002MaRDI QIDQ269503zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

decidabilitysatisfiabilitybounding quantifierscomputation tree logicextended computation tree logicinteger constraintstemporal logic

Mathematics Subject Classification ID

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)

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

Cites work

• 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?)
• 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
• CTL^* and ECTL^* as fragments of the modal -calculus
• Combining interval-based temporal reasoning with general TBoxes
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Deciding properties of integral relational automata
• Foundations of Software Science and Computation Structures
• 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

Cited in

(8)

• Temporal logics with local constraints (invited talk)
• CTL* model checking for data-aware dynamic systems with arithmetic
• scientific article; zbMATH DE number 4119650 (Why is no real title available?)
• 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

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)