On the freeze quantifier in Constraint LTL: Decidability and complexity

DOI10.1016/j.ic.2006.08.003zbMath1116.03014OpenAlexW4256476220MaRDI QIDQ868025

Ranko Lazić, David E. Nowak, Stéphane P. Demri

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

zbMATH Keywords

computational complexitydecidabilityconstraintslinear-time temporal logicfreeze quantifier

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items (16)

Reactive synthesis from visibly register pushdown automata ⋮ Future-Looking Logics on Data Words and Trees ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Complexity results on register context-free grammars and related formalisms ⋮ Taming strategy logic: non-recurrent fragments ⋮ Temporal stream logic modulo theories ⋮ Some Recent Results in Metric Temporal Logic ⋮ Model checking memoryful linear-time logics over one-counter automata ⋮ Beyond Shapes: Lists with Ordered Data ⋮ Optimal run problem for weighted register automata ⋮ Expressiveness of Hybrid Temporal Logic on Data Words ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The Complexity of Flat Freeze LTL ⋮ Unnamed Item

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
• A theory of timed automata
• An algebraic approach to data languages and timed languages
• Many-dimensional modal logics: theory and applications
• Decidable fragments of first-order temporal logics
• Axiomatizing the monodic fragment of first-order temporal logic
• A logical characterization of data languages.
• A semantics of sequence diagrams.
• Equality and monodic first-order temporal logic
• Hierarchies of modal and temporal logics with reference pointers
• Temporal logic can be more expressive
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• Flat fragments of CTL and CTL: separating the expressive and distinguishing powers
• A really temporal logic
• The benefits of relaxing punctuality
• Modal Logics Between Propositional and First-order
• Finite state machines for strings over infinite alphabets
• NEXP TIME-complete description logics with concrete domains
• Computer Science Logic
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Automated Technology for Verification and Analysis
• CONCUR 2005 – Concurrency Theory
• Introduction to constraint databases
• Constrained properties, semilinear systems, and Petri nets

This page was built for publication: On the freeze quantifier in Constraint LTL: Decidability and complexity