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

DOI10.1007/978-3-319-46520-3_6MaRDI QIDQ1990502zbMATH OpenOpenAlexFDO

Authors Radu Iosif, Arnaud Sangnier

Publication date 25 October 2018

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

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)

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.

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

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
• scientific article; zbMATH DE number 7407773 (Why is no real title available?)
• scientific article; zbMATH DE number 7407775 (Why is no real title available?)
• 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)