



Solving Reachability Problem for Monotonic Counter Systems by Supercompilation Andrei V. Klimov,
We attempt to put supercompilation in the context of works on counter systems, wellstructured transition systems, Petri nets, etc. Two classic versions of the supercompilation algorithm are formulated for counter systems, using notions and notation close to the works of that community. Based on this we explain why a certain iterative procedure of application of a supercompiler to a program that encodes a monotonic counter system terminates having verified or refuted its safety property (provided the set of unsafe states is upperclosed). This fact was discovered in practice by A. Nemytykh and A. Lisitsa when they performed experiments on verification of cachecoherence protocols and other models by means of the Refal supercompiler SCP4, and since then its theoretical explanation was an open problem. The idea is that this iterative procedure fits the algorithmic schema called `Expand, Enlarge and Check' (ECC) developed by G. Geeraerts et al. They proved that ECC algorithms terminate and solve the reachability and coverability problems of wellstructured transition systems. 