A simple algorithm for solving the coverability problem for monotonic counter systems
Andrei Valentinovich Klimov · Automatic Control and Computer Sciences · 2012
An algorithm to solve 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 application of a supercompiler (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.