On the Computation of McMillan's Prefix for Contextual Nets and Graph Grammars
P. Baldan(1),
A. Corradini (2),
B. König(3)
S. Schwoon(4),
(1)
Dipartimento di Matematica, Università di Padova, Italy
(2)
Dipartimento di Informatica, Università di Pisa, Italia.
(3)
Institut für Informatik und interaktive Systeme,
Universität Duisburg-Essen, Germany.
(4)
LSV, ENS Cachan & CNRS, INRIA Saclay, France
Abstract:
In recent years, a research thread focused on the use of the
unfolding semantics for verification purposes. This started with a
paper by McMillan, which devises an algorithm for constructing a
finite complete prefix of the unfolding of a safe Petri net, providing a
compact representation of the reachability graph.
The extension to contextual nets and graph transformation systems is
far from being trivial because events can have multiple causal
histories. Recently, we proposed an abstract algorithm that
generalizes McMillan's construction to bounded contextual nets
without resorting to an encoding into plain P/T nets. Here, we
provide a more explicit construction that renders the algorithm
effective. To allow for an inductive definition of concurrency,
missing in the original proposal and essential for an efficient
unfolding procedure, the key intuition is to associate histories not only
with events, but also with places. Additionally, we outline how the
proposed algorithm can be extended to graph transformation systems,
for which previous algorithms based on the encoding of read arcs
would not be applicable.