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: (1) the control structure of the counter system is flat, meaning that nested loops are forbidden, and (2) the multiplicative monoid generated by the affine update matrices present in the system is finite. We provide complexity bounds for several decision problems of such systems, by proving that reachability and model checking for Past Linear Temporal Logic stands in the second level of the polynomial hierarchy Σ2P, while model checking for First Order Logic is PSPACE-complete.
How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property ?
SANGNIER A
2016-01-01
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: (1) the control structure of the counter system is flat, meaning that nested loops are forbidden, and (2) the multiplicative monoid generated by the affine update matrices present in the system is finite. We provide complexity bounds for several decision problems of such systems, by proving that reachability and model checking for Past Linear Temporal Logic stands in the second level of the polynomial hierarchy Σ2P, while model checking for First Order Logic is PSPACE-complete.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
