LTL over integer periodicity constraints

DOI10.1016/j.tcs.2006.02.019zbMath1097.68073OpenAlexW2152132130MaRDI QIDQ2503321

Stéphane P. Demri

Publication date: 14 September 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.02.019

zbMATH Keywords

computational complexityQBFBüchi automatonperiodicity constraintsPresburger LTL

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items

Model-checking CTL* over flat Presburger counter systems, A brief account of runtime verification, An automata-theoretic approach to constraint LTL, Temporal stream logic modulo theories, Impartial Anticipation in Runtime-Verification, ``Most of leads to undecidability: failure of adding frequencies to LTL, Verification of qualitative \(\mathbb Z\) constraints, A theory of ultimately periodic languages and automata with an application to time granularity, Linear-time temporal logics with Presburger constraints: an overview ★, CTL* model checking for data-aware dynamic systems with arithmetic

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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Real-time logics: Complexity and expressiveness
• On the interpretability of arithmetic in temporal logic
• The power of temporal proofs
• A theory of timed automata
• Reasoning about infinite computations
• Many-dimensional modal logics: theory and applications
• Presburger liveness verification of discrete timed automata.
• Hierarchies of modal and temporal logics with reference pointers
• Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
• Semigroups, Presburger formulas, and languages
• Temporal logic can be more expressive
• Precise interprocedural analysis through linear algebra
• The complexity of propositional linear temporal logics
• A Decision Procedure for the First Order Theory of Real Addition with Order
• Datalog with integer periodicity constraints
• Calendar Logic
• A really temporal logic
• Representing and Reasoning about Temporal Granularities
• Representation, reasoning, and relational structures: a hybrid logic manifesto
• Deciding properties of integral relational automata
• The Expressive Power of Temporal Logic of Actions
• Modal Logics Between Propositional and First-order
• NEXP TIME-complete description logics with concrete domains
• A classification of symbolic transition systems
• Foundations of Software Science and Computation Structures
• Logics in Artificial Intelligence
• Automated Reasoning with Analytic Tableaux and Related Methods
• Efficient Symbolic Representations for Arithmetic Constraints in Verification
• Impossibility of an algorithm for the decision problem in finite classes
• Theoretical Computer Science
• CONCUR 2005 – Concurrency Theory
• CONCUR 2003 - Concurrency Theory
• Introduction to constraint databases