Verification of qualitative \(\mathbb Z\) constraints

DOI10.1016/j.tcs.2008.07.023zbMath1157.68048MaRDI QIDQ959820

Stéphane P. Demri, Régis Gascon

Publication date: 12 December 2008

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

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

zbMATH Keywords

complexity; temporal logic; Büchi automaton; symbolic model; arithmetical constraint

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

68Q60: Specification and verification (program logics, model checking, etc.)

03B44: Temporal logic

Related Items

Verification of gap-order constraint abstractions of counter systems, Verification of Gap-Order Constraint Abstractions of Counter Systems

Uses Software

• FAST

Cites Work

• Untiming timed languages
• Automata for branching and layered temporal structures. An investigation into regularities of infinite transition systems
• An automata-theoretic approach to constraint LTL
• The theory of ends, pushdown automata, and second-order logic
• A theory of timed automata
• Reasoning about infinite computations
• On infinite transition graphs having a decidable monadic theory
• Presburger liveness verification of discrete timed automata.
• DP lower bounds for equivalence-checking and model-checking of one-counter automata
• LTL over integer periodicity constraints
• THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS
• Temporal logic can be more expressive
• Towards a Model-Checker for Counter Systems
• The complexity of propositional linear temporal logics
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• A really temporal logic
• Deciding properties of integral relational automata
• NEXP TIME-complete description logics with concrete domains
• A classification of symbolic transition systems
• Programming Languages and Systems
• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
• Programs with Lists Are Counter Automata
• CONCUR 2005 – Concurrency Theory
• CONCUR 2003 - Concurrency Theory
• Flat Parametric Counter Automata
• Introduction to constraint databases
• Reachability analysis of pushdown automata: Application to model-checking
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item