The Complexity of Reversal-Bounded Model-Checking

DOI10.1007/978-3-642-24364-6_6zbMath1348.68121MaRDI QIDQ3172883

Marcello M. Bersani, Stéphane P. 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

68Q25: Analysis of algorithms and problem complexity

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

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

Uses Software

• cvc3
• z3
• TaPAS
• LIRA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines
• The complexity of decision problems for finite-turn multicounter machines
• The covering and boundedness problems for vector addition systems
• Reasoning about infinite computations
• Counter machines and verification problems.
• The Complexity of Reversal-Bounded Model-Checking
• Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems
• Reversal-Bounded Counter Machines Revisited
• TaPAS: The Talence Presburger Arithmetic Suite
• Verification Decidability of Presburger Array Programs
• On the complexity of integer programming
• Bounds on Positive Integral Solutions of Linear Diophantine Equations
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• A really temporal logic
• NEXP TIME-complete description logics with concrete domains
• Automated Technology for Verification and Analysis
• Tools and Algorithms for the Construction and Analysis of Systems