Verification by State Spaces with Equivalence Classes

Abstract

This paper demonstrates the pontential 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 does allow derivation of many verification results.

Other researches have taken advantage of the symmetries of systems, which induce a certain kind of equivalence. The contribution fo this paper is to show that a more general notion of equivalence is useful. As example, a communication protocol modelled in the formalism of Coloured Petri Nets is verified. Aided by a computer tool supporting state spaces with equivalence classes, significant reduction of state spaces are exhibited.

Topics. State space reduction methods, equivalence vs. symmetry, High-level Petri Nets, communication protocols.