Solving Reachability Problem for Monotonic Counter Systems by Supercompilation

Andrei V. Klimov,
Keldysh Institute of Applied Mathematics, Russian Academy of Sciences

 

Abstract

We attempt to put supercompilation in the context of works on counter systems, well-structured 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 upper-closed). This fact was discovered in practice by A. Nemytykh and A. Lisitsa when they performed experiments on verification of cache-coherence 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 well-structured transition systems.