An automata-theoretic approach to constraint LTL
From MaRDI portal
Publication:870361
DOI10.1016/j.ic.2006.09.006zbMath1113.03015OpenAlexW2019145653MaRDI QIDQ870361
Deepak D'Souza, Stéphane P. Demri
Publication date: 12 March 2007
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2006.09.006
Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)
Related Items
Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints ⋮ Verification of Gap-Order Constraint Abstractions of Counter Systems ⋮ Generalized Qualitative Spatio-Temporal Reasoning: Complexity and Tableau Method ⋮ On clock-aware LTL parameter synthesis of timed automata ⋮ On temporal logics with data variable quantifications: decidability and complexity ⋮ Unnamed Item ⋮ Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints ⋮ Separation logics and modalities: a survey ⋮ An SMT-based approach to satisfiability checking of MITL ⋮ Temporal stream logic modulo theories ⋮ Church synthesis on register automata over linearly ordered data domains ⋮ Realizability problem for constraint LTL ⋮ Reasoning about sequences of memory states ⋮ Verification of gap-order constraint abstractions of counter systems ⋮ Constraint LTL satisfiability checking without automata ⋮ On the initialization of clocks in timed formalisms ⋮ Verification of qualitative \(\mathbb Z\) constraints ⋮ Model checking of linear-time properties in multi-valued systems ⋮ A logical characterization of timed regular languages ⋮ Using formal verification to evaluate the execution time of Spark applications ⋮ Using model theory to find decidable and tractable description logics with concrete domains ⋮ Description logics with concrete domains and general concept inclusions revisited ⋮ CTL* model checking for data-aware dynamic systems with arithmetic ⋮ A tool for deciding the satisfiability of continuous-time metric temporal logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Maintaining knowledge about temporal intervals
- Untiming timed languages
- Real-time logics: Complexity and expressiveness
- From local to global consistency
- A theory of timed automata
- Reasoning about infinite computations
- Many-dimensional modal logics: theory and applications
- Multi-dimensional modal logic as a framework for spatio-temporal reasoning
- Presburger liveness verification of discrete timed automata.
- LTL over integer periodicity constraints
- LTL with the freeze quantifier and register automata
- Temporal logic can be more expressive
- Linear-time temporal logics with Presburger constraints: an overview ★
- The Effects of Bounding Syntactic Resources on Presburger LTL
- The complexity of propositional linear temporal logics
- A really temporal logic
- Deciding properties of integral relational automata
- PSpace Reasoning with the Description Logic ALCF(D)
- NEXP TIME-complete description logics with concrete domains
- Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
- Automated Reasoning with Analytic Tableaux and Related Methods
- CONCUR 2005 – Concurrency Theory
- CONCUR 2003 - Concurrency Theory
- Introduction to constraint databases
