François Taïani, Mario Paludetto, and Thierry Cros

Avoiding State Explosion: A Brief Introduction To Binary Branching Diagrams And Petri Net Unfoldings

Toulouse (F), September, Rapport LAAS number No00377 Contrat de Recherche LAAS-Twam Informatique N 413/99, 2000 (14p.)

The use of formal verification methods has been studied for several decades now as a promising mean to improve software quality, particularly in the context of concurrent systems. Among them, approaches based on finite state-machine representations certainly belong to the most popular. Unfortunately, the state machine representation of a concurrent system grows exponentially in size with the number of its concurrent components. In this technical report we give an overview of two of the most important techniques proposed to fight against this combinatorial state proliferation, commonly known as the state space explosion.
The first one, based on Binary Decision Diagrams [BCM90], is a representative of symbolic approaches. These techniques use compact representations of state regions and transition relationships to reduce the memory requirement of verification algorithms. We first introduce general BDDs in an informal way using a small example. Then we show how those BDDs can be used to code a small state transition system.
The second state reduction technique we present is based on partial unfolding of Petri Nets [McMill95]. It belongs to the partial order reduction methods. Such approaches are based on the idea that in most cases the total interleaving of concurrent actions is not needed to check a given property on a system. In such cases, a total interleaving distinguishes between action sequences and their intermediary state counterparts that are equivalent from the point of view of the checked property. In this report we use a small concurrent system expressed with two state machines to show how the partial unfolding technique can be applied to it. We also introduce the informal concept of 'unambiguous past / divergent future' to sum up the 'self conflict freedom' and 'forward conflict freedom' rules introduced in [McMill95].

complete document


[Maison.png]Back to Home

Last generated on 8 Dec 2019     Valid HTML 4.0!