Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic
From MaRDI portal
Publication:3447697
DOI10.1007/978-3-319-11439-2_7zbMath1393.68101OpenAlexW148785827MaRDI QIDQ3447697
Stéphane P. Demri, Arnaud Sangnier, Amit Kumar Dhar
Publication date: 28 October 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-11439-2_7
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 (4)
Equivalence between model-checking flat counter systems and Presburger arithmetic ⋮ Verification of Flat FIFO Systems ⋮ Model-Checking Counting Temporal Logics on Flat Structures ⋮ Taming past LTL and flat counter systems
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
- TaPAS: The Talence Presburger Arithmetic Suite
- “Sometimes” and “not never” revisited
- CONCUR 2004 - Concurrency Theory
- On the Complexity of Verifying Regular Properties on Flat Counter Systems,
- Automated Technology for Verification and Analysis
This page was built for publication: Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic