Ranking Functions for Vector Addition Systems

TL;DR

This paper presents a comprehensive method for constructing ranking functions for vector addition systems with states, aiding in termination analysis, explanation, certification, and complexity assessment of such systems.

Contribution

It introduces a complete approach for generating ranking functions, enhancing understanding and verification of termination and complexity in vector addition systems.

Findings

Provides a method for constructing ranking functions

Enables certification of termination

Facilitates complexity analysis

Abstract

Vector addition systems are an important model in theoretical computer science and have been used for the analysis of systems in a variety of areas. Termination is a crucial property of vector addition systems and has received considerable interest in the literature. In this paper we give a complete method for the construction of ranking functions for vector addition systems with states. The interest in ranking functions is motivated by the fact that ranking functions provide valuable additional information in case of termination: They provide an explanation for the progress of the vector addition system, which can be reported to the user of a verification tool, and can be used as certificates for termination. Moreover, we show how ranking functions can be used for the computational complexity analysis of vector addition systems (here complexity refers to the number of steps the vector addition system under analysis can take in terms of the given initial vector).