Equivalence between model-checking flat counter systems and Presburger arithmetic
From MaRDI portal
Publication:2636509
DOI10.1016/j.tcs.2017.07.007zbMath1393.68100OpenAlexW2737769985MaRDI QIDQ2636509
Arnaud Sangnier, Amit Kumar Dhar, Stéphane P. Demri
Publication date: 5 June 2018
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2017.07.007
Specification and verification (program logics, model checking, etc.) (68Q60) First-order arithmetic and fragments (03F30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The strong exponential hierarchy collapses
- Persistence of vector replacement systems is decidable
- The complexity of logical theories
- Modalities for model checking: Branching time logic strikes back
- Branching-Time Model Checking of One-Counter Processes and Timed Automata
- Branching-Time Model Checking of Parametric One-Counter Automata
- Model-checking CTL* over flat Presburger counter systems
- Taming Past LTL and Flat Counter Systems
- Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops
- The Complexity of Reversal-Bounded Model-Checking
- Reachability in Succinct and Parametric One-Counter Automata
- Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic
- TaPAS: The Talence Presburger Arithmetic Suite
- “Sometimes” and “not never” revisited
- Verification Decidability of Presburger Array Programs
- Reversal-Bounded Multicounter Machines and Their Decision Problems
- Subclasses of presburger arithmetic and the weak EXP hierarchy
- CONCUR 2004 - Concurrency Theory
- On the Complexity of Verifying Regular Properties on Flat Counter Systems,
- Automated Technology for Verification and Analysis
- Proving safety properties of infinite state systems by compilation into Presburger arithmetic
