A simple algorithm for solving the coverability problem for monotonic counter systems

A. V. Klimov

M. V. Keldysh Institute for Applied Mathematics, Russian Academy of Sciences, Moscow

Abstract: An algorithm for solving the coverability problem for monotonic counter systems is presented. The solvability of this problem is well-known, but the algorithm is interesting due to its simplicity. The algorithm has emerged as a simplification of a certain procedure of a supercompiler application (a program specializer based on V.F. Turchin's supercompilation) to a program encoding a monotonic counter system along with initial and target sets of states and from the proof that under some conditions the procedure terminates and solves the coverability problem.

Keywords: well-structured transition systems, counter systems, reachability, coverability, supercompilation.

UDC: 519.681.3

Received: 17.10.2011