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

TL;DR

This paper investigates the complexity of verifying flat affine counter systems with the finite monoid property, establishing tight bounds for reachability and model checking problems under these restrictions.

Contribution

It introduces the finite monoid property as a key restriction that makes the verification of flat affine counter systems decidable and characterizes the complexity of various decision problems.

Findings

Reachability and LTL model checking are $ ext{Σ}_2^P$-complete.

FO model checking is PSPACE-complete.

Decidability is achieved under flatness and finite monoid restrictions.

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 $\Sigma^P_2$, while model checking for First Order Logic is PSPACE-complete.