Equivalence between model-checking flat counter systems and Presburger arithmetic
DOI10.1007/978-3-319-11439-2_7zbMATH Open1393.68101OpenAlexW148785827MaRDI QIDQ3447697FDOQ3447697
Authors: Stéphane Demri, A. K. Dhar, Arnaud Sangnier 
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
Recommendations
- Equivalence between model-checking flat counter systems and Presburger arithmetic
- Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
- Towards a Model-Checker for Counter Systems
- Flat model checking for counting LTL using quantifier-free Presburger arithmetic
- Taming past LTL and flat counter systems
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) First-order arithmetic and fragments (03F30)
Cites Work
- TaPAS: The Talence Presburger Arithmetic Suite
- Title not available (Why is that?)
- “Sometimes” and “not never” revisited
- Title not available (Why is that?)
- Model-checking CTL* over flat Presburger counter systems
- CONCUR 2004 - Concurrency Theory
- Automated Technology for Verification and Analysis
- On the complexity of the linear-time μ-calculus for Petri Nets
- Modalities for model checking: Branching time logic strikes back
- Taming Past LTL and Flat Counter Systems
- Title not available (Why is that?)
- The complexity of logical theories
- The Complexity of Reversal-Bounded Model-Checking
- Branching-Time Model Checking of Parametric One-Counter Automata
- Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops
- Title not available (Why is that?)
- On the Complexity of Verifying Regular Properties on Flat Counter Systems,
- Branching-time model checking of one-counter processes and timed automata
Cited In (8)
- Verification of Flat FIFO Systems
- Equivalence between model-checking flat counter systems and Presburger arithmetic
- Title not available (Why is that?)
- Taming past LTL and flat counter systems
- On the Complexity of Verifying Regular Properties on Flat Counter Systems,
- Model-Checking Counting Temporal Logics on Flat Structures
- Flat Parametric Counter Automata
- Towards a Model-Checker for Counter Systems
This page was built for publication: Equivalence between model-checking flat counter systems and Presburger arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3447697)
