Sciweavers

Share
GG
2010
Springer

On the Computation of McMillan's Prefix for Contextual Nets and Graph Grammars

11 years 9 months ago
On the Computation of McMillan's Prefix for Contextual Nets and Graph Grammars
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 e...
Paolo Baldan, Alessandro Bruni, Andrea Corradini,
Added 09 Nov 2010
Updated 09 Nov 2010
Type Conference
Year 2010
Where GG
Authors Paolo Baldan, Alessandro Bruni, Andrea Corradini, Barbara König, Stefan Schwoon
Comments (0)
books