How hard is it to verify flat affine counter systems with the finite monoid property ?
Computational Complexity
2016-05-20 v1 Logic in Computer Science
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 , while model checking for First Order Logic is PSPACE-complete.
Keywords
Cite
@article{arxiv.1605.05836,
title = {How hard is it to verify flat affine counter systems with the finite monoid property ?},
author = {Radu Iosif and Arnaud Sangnier},
journal= {arXiv preprint arXiv:1605.05836},
year = {2016}
}