Abstract interpretation based verification of linear transition systems

OData support
Vörös András
Department of Measurement and Information Systems

Linear transition systems, such as Petri nets are a common graphical and mathematical modelling tool for asynchronous, distributed, concurrent, parallel and non-deterministic systems. Their behaviour is determined by the statespace, that is, the set of reachable states and state transitions. When analysing linear transition systems, reachability - i.e. whether or not the state space includes a given target state - becomes an important question. The problem is EXPSPACE-hard for simple Petri nets, and undecidable for linear transition systems.

Several methods based on mathematical abstraction provide a solution for the analysis of models with infinite state space. The advantage of these methods is that they examine reachability and/or invariant properties by building and exploring a finite representation of the state space. The abstract interpretation algorithm produces the finite representation using convex polyhedra, thus overapproximating the set of reachable states. However, known methods for Petri net based models are often not able to give a sufficiently precise approximation. In my work I dealt with further development of these methods and their extension for linear transition systems.

In the report I present methods based on refining abstract interpretation which allow the examination of systems that previous algorithms weren't able to handle. I developed a new algorithm that refines the explored state space by taking the reachability condition into account. I also present a method that combines abstract interpretation based solutions with algorithms that explicitly explore the state space to increase efficiency. I demonstrate the advantages of the new algorithms by examples and I prove their effectivity by measurements.


Please sign in to download the files of this thesis.