On the evaluation of Petri-net reachability algorithms

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

Nowadays many systems require a high degree of assurance of correctness. In many cases, these systems are so complex that engineers are not able to see through the whole operation. So the verification of the system is only possible by automated techniques, which can prove the correctness of the system. One of these techniques are the formal methods. Model checking is a popular way of verification. Given a suitable model of the system, it provides mathematically based, exhaustive analysis of the examined properties.

One of these properties is the reachability problem, which checks if the model can reach a given state. The number of possible states of a model can be infinite, which makes the decision of the reachability problem very hard.

In this paper I investigated algorithms, that try to decide the reachability problem of models described by the Petri Nets modeling language.

In the course of our previous work, we investigated one of these methods, the usage of CEGAR on Petri Nets.

In this paper I introduce the CEGAR algorithm and some deficiencies of it, and I develop a new algorithm being able to solve the decision problem for a different class of problems. I implemented the new solution and compared its efficiency with CEGER on different types of models by measurements.


Please sign in to download the files of this thesis.