The complexity of reversal-bounded model-checking

DOI10.1007/978-3-642-24364-6_6MaRDI QIDQ3172883zbMATH OpenOpenAlexFDO

Authors Marcello M. Bersani, Stéphane Demri

Publication date 7 October 2011

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24364-6_6

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Reversal-Bounded Counter Machines Revisited
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• Towards a Model-Checker for Counter Systems
• scientific article; zbMATH DE number 2081100
• Equivalence between model-checking flat counter systems and Presburger arithmetic

Cites work

• scientific article; zbMATH DE number 1302047 (Why is no real title available?)
• scientific article; zbMATH DE number 2081100 (Why is no real title available?)
• scientific article; zbMATH DE number 1759611 (Why is no real title available?)
• A really temporal logic
• Algorithmic metatheorems for decidable LTL model checking over infinite systems
• An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines
• Automated Technology for Verification and Analysis
• Bounds on Positive Integral Solutions of Linear Diophantine Equations
• Counter machines and verification problems.
• NExpTime-complete description logics with concrete domains
• On the complexity of integer programming
• Reasoning about infinite computations
• Reversal-Bounded Counter Machines Revisited
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• TaPAS: The Talence Presburger Arithmetic Suite
• The complexity of decision problems for finite-turn multicounter machines
• The complexity of reversal-bounded model-checking
• The covering and boundedness problems for vector addition systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification Decidability of Presburger Array Programs

Cited in

(8)

• Lower bounds on the complexity of \(\mathsf{MSO}_1\) model-checking
• Counter machines with infrequent reversals
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• The complexity of reversal-bounded model-checking
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Reasoning about reversal-bounded counter machines
• scientific article; zbMATH DE number 2081100 (Why is no real title available?)
• Complexity of model checking for cardinality-based belief revision operators

Describes a project that uses

Uses Software

• LIRA
• TaPAS
• z3
• cvc3

This page was built for publication: The complexity of reversal-bounded model-checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172883)