The Complexity of Reversal-Bounded Model-Checking

DOI10.1007/978-3-642-24364-6_6zbMath1348.68121OpenAlexW80793323MaRDI 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

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

Related Items (3)

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

This page was built for publication: The Complexity of Reversal-Bounded Model-Checking