Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic

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

Mathematics Subject Classification ID

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