2007.04.10 | Lars Michael Kristensen

Model Checking Techniques for Colored Petri Nets

Model checking, or state space analysis, is a formalmethod to prove that finite state system match their specification. Given a formal model of the system and a property, usually expressed in a temporal logic such as the linear time temporal logic, a model checker explores all the possible behaviors of the system, (its state space) to trackthe erroneous ones. Despite its simplicity, its practical application is limited due to the well-known state explosion problem: the state space can be far too large to be explored in a reasonable time.

This talk presents differentstrategies used to cope with this problem. The first one is used prior to state space search in order to simplify the model. The second one does not in a strict sense limit the state explosion but offers a way to efficiently represent the state space in memory making it possible to analyze more complex models. The third method, known as partial order reduction, is used during state space exploration to avoid the execution of some unnecessary transitions. These techniques are implemented in a model checker called Helena
that can verify safety properties of colored Petri nets, a mathematical and graphical language well suited to the analysis of communication protocols. We will briefly introduce this tool and show by multiple experimentations the reductions that can be achieved by these techniques.

Host: Lars M. Kristensen