Efficient Contetxual Unfolding
C. Rodríguez,(1),
S. Schwoon(1),
P. Baldan(2),
(1)
LSV, ENS Cachan & CNRS, INRIA Saclay, France
(2)
Dipartimento di Matematica, Università di Padova, Italy
Abstract:
A contextual net is a Petri net extended with read arcs, which allow
transitions to check for tokens without consuming them. Contextual
nets allow for better modelling of concurrent read access than Petri
nets, and their unfoldings can be exponentially more compact than
those of a corresponding Petri net. A constructive but abstract
procedure for generating those unfoldings was proposed in earlier
work; however, no concrete implementation existed. Here, we
close this gap providing two concrete methods for computing contextual
unfoldings, with a view to efficiency. We report on experiments
carried out on a number of benchmarks. These show that not only are
contextual unfoldings more compact than Petri net unfoldings, but they can
be computed with the same or better efficiency, in particular with respect
to the place-replication encoding of contextual nets into Petri nets.