How hard is it to verify flat affine counter systems with the finite monoid property?

DOI10.1007/978-3-319-46520-3_6zbMATH Open1398.68311arXiv1605.05836OpenAlexW2400739323MaRDI QIDQ1990502FDOQ1990502

Authors: Radu Iosif, Arnaud Sangnier 

Publication date: 25 October 2018

Abstract: We study several decision problems for counter systems with guards defined by convex polyhedra and updates defined by affine transformations. In general, the reachability problem is undecidable for such systems. Decidability can be achieved by imposing two restrictions: (i) the control structure of the counter system is flat, meaning that nested loops are forbidden, and (ii) the set of matrix powers is finite, for any affine update matrix in the system. We provide tight complexity bounds for several decision problems of such systems, by proving that reachability and model checking for Past Linear Temporal Logic are complete for the second level of the polynomial hierarchy $Sigm{a}_2^P$, while model checking for First Order Logic is PSPACE-complete.

Full work available at URL: https://arxiv.org/abs/1605.05836

Recommendations

• On the Complexity of Verifying Regular Properties on Flat Counter Systems,
• Taming past LTL and flat counter systems
• Taming past LTL and flat counter systems
• Automated Technology for Verification and Analysis
• Equivalence between model-checking flat counter systems and Presburger arithmetic

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (10)

• On simulating Turing machines with matrix semigroups with integrality tests
• Verification of Flat FIFO Systems
• Taming past LTL and flat counter systems
• Safety problems are NP-complete for flat integer programs with octagonal loops
• Verification of flat FIFO systems
• Affine extensions of integer vector addition systems with states
• Title not available (Why is that?)
• Title not available (Why is that?)
• Taming past LTL and flat counter systems
• Automated Technology for Verification and Analysis

This page was built for publication: How hard is it to verify flat affine counter systems with the finite monoid property?

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