For the most recent entries see the Petri Nets Newsletter.

Verification of Coloured Petri Nets Using State Spaces with Equivalence Classes.

Jørgensen, Jens Bæk; Kristensen, Lars Michael

In: 97: Proceedings of the Workshop on Petri Nets in System Engineering (PNSE'97), Hamburg, September 25-26, 1997 / Farwer, B.; Moldt, D.; Stehr, M.-O.: Report FBI-HH-B-205, pages 20-31. Universität Hamburg, September 1997.

Abstract: This paper demonstrates the potential of verification based on state spaces reduced by equivalence relations. The basic observation is that quite often, some states of a system are similar, i.e., they induce similar behaviours. Similarity can be formally expressed by defining equivalence relations on the set of states and the set of actions of a system under consideration. A state space can be constructed, in which the nodes correspond to equivalence classes of states and the arcs correspond to equivalence classes of actions. Such a state space is often much smaller than the ordinary full state space, but it does allow derivation of many verification results. Other researchers have taken advantage of the symmetries in systems, which induce a certain kind of equivalence. The contribution of this paper is to show that a more general notion of equivalence is useful. As a representative example a communication protocol is verified. Aided by a developed computer tool significant reductions of state spaces are exhibited, representing some first results on the practical use of state spaces with equivalence classes for Coloured Petri Nets.

Keywords: State space based approaches; efficient model checking; tools; Coloured Petri Nets; communication protocols; reduction by equivalence and symmetry.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography