Equivalence between model-checking flat counter systems and Presburger arithmetic

DOI10.1007/978-3-319-11439-2_7MaRDI QIDQ3447697zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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)

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

Cites work

• scientific article; zbMATH DE number 1705163 (Why is no real title available?)
• scientific article; zbMATH DE number 1954380 (Why is no real title available?)
• scientific article; zbMATH DE number 1962855 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• Automated Technology for Verification and Analysis
• Branching-time model checking of one-counter processes and timed automata
• Branching-time model checking of parametric one-counter automata
• CONCUR 2004 - Concurrency Theory
• Modalities for model checking: Branching time logic strikes back
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• On the Complexity of Verifying Regular Properties on Flat Counter Systems,
• On the complexity of the linear-time μ-calculus for Petri Nets
• Safety problems are NP-complete for flat integer programs with octagonal loops
• TaPAS: The Talence Presburger Arithmetic Suite
• Taming past LTL and flat counter systems
• The complexity of logical theories
• The complexity of reversal-bounded model-checking
• “Sometimes” and “not never” revisited

Cited in

(12)

• How hard is it to verify flat affine counter systems with the finite monoid property?
• Verification of Flat FIFO Systems
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Taming past LTL and flat counter systems
• scientific article; zbMATH DE number 1979550 (Why is no real title available?)
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• Flat model checking for counting LTL using quantifier-free Presburger arithmetic
• 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)