Automatic Verification of Counter Systems With Ranking Function

The verification of final termination for counter systems is undecidable. For non flattable counter systems, the verification of this type of property is generally based on the exhibition of a ranking function. Proving the existence of a ranking function for general counter systems is also undecidable. We provide a framework in which the verification whether a given function is a ranking function is decidable. This framework is applicable to convex counter systems which admit a Presburger or a LPDS ranking function. This extends the results of [A. Bradley, Z. Manna, and B. Sipma. Termination analysis of integer linear loops. In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, volume 3653 of Lecture Notes in Computer Science, pages 488–502. Springer, 2005]. From this framework, we derive a model-checking algorithm to verify whether a final termination property is satisfied or not. This approach has been successfully applied to the verification of a parametric version of the ZCSP protocol.