On the freeze quantifier in Constraint LTL: Decidability and complexity
DOI10.1016/J.IC.2006.08.003zbMATH Open1116.03014OpenAlexW4256476220MaRDI QIDQ868025FDOQ868025
Authors: Ranko Lazić, Stéphane Demri, David Nowak
Publication date: 19 February 2007
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2006.08.003
Recommendations
Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)
Cites Work
- A theory of timed automata
- Many-dimensional modal logics: theory and applications
- The complexity of propositional linear temporal logics
- Reversal-Bounded Multicounter Machines and Their Decision Problems
- A really temporal logic
- The benefits of relaxing punctuality
- Title not available (Why is that?)
- Temporal logic can be more expressive
- Title not available (Why is that?)
- NEXP TIME-complete description logics with concrete domains
- “Sometimes” and “not never” revisited
- Title not available (Why is that?)
- Computer Science Logic
- Title not available (Why is that?)
- Automated Technology for Verification and Analysis
- Hierarchies of modal and temporal logics with reference pointers
- Decidable fragments of first-order temporal logics
- An algebraic approach to data languages and timed languages
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Title not available (Why is that?)
- Finite state machines for strings over infinite alphabets
- CONCUR 2005 – Concurrency Theory
- A logical characterization of data languages.
- Title not available (Why is that?)
- Axiomatizing the monodic fragment of first-order temporal logic
- Title not available (Why is that?)
- Introduction to constraint databases
- Modal Logics Between Propositional and First-order
- Title not available (Why is that?)
- Constrained properties, semilinear systems, and Petri nets
- Title not available (Why is that?)
- Title not available (Why is that?)
- Equality and monodic first-order temporal logic
- A semantics of sequence diagrams.
- Flat fragments of CTL and CTL: separating the expressive and distinguishing powers
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (17)
- Temporal stream logic modulo theories
- Reactive synthesis from visibly register pushdown automata
- Title not available (Why is that?)
- Model checking memoryful linear-time logics over one-counter automata
- The Complexity of Flat Freeze LTL
- Title not available (Why is that?)
- Title not available (Why is that?)
- Future-Looking Logics on Data Words and Trees
- Title not available (Why is that?)
- Taming strategy logic: non-recurrent fragments
- Optimal run problem for weighted register automata
- Expressiveness of hybrid temporal logic on data words
- Complexity results on register context-free grammars and related formalisms
- Some Recent Results in Metric Temporal Logic
- Automata and grammars for data words
- Beyond Shapes: Lists with Ordered Data
- Title not available (Why is that?)
This page was built for publication: On the freeze quantifier in Constraint LTL: Decidability and complexity
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q868025)