History Preserving Bisimulation
for Contextual Nets

Paolo Baldan, Andrea Corradini, Ugo Montanari

Dipartimento di Informatica
Università di Pisa

Abstract:

We investigate the notion of history preserving bisimulation [5,6,2] for contextual P/T nets, a generalization of ordinary P/T Petri nets where a transition may check for the presence of tokens without consuming them (non-destructive read operations). A first equivalence, simply called HP-bisimulation, is based on Winskel's prime event structures. A finer equivalence, called RHP-bisimulation (where ``R'' stands for ``read''), relies on asymmetric event structures [1], a generalization of prime event structures which gives a more faithful account of the dependencies among transition occurrences arising in contextual net computations. Extending the work in [3,7], we show that HP-bisimulation is decidable for finite n-safe contextual nets. Moreover by resorting to causal automata [4] -- a variation of ordinary automata introduced to deal with history dependent formalisms -- we can obtain an algorithm for deciding HP-bisimulation and for getting a minimal realization. Decidability of RHP-bisimulation, instead, remains an open question.

Bibliography

[1]    P. Baldan, A. Corradini, and U. Montanari.  An event structure semantics for P/T contextual nets: Asymmetric event
        structures.
        In M. Nivat, editor, Proceedings of FoSSaCS '98, volume 1378 of LNCS, pages 63-80. Springer Verlag, 1998.

 
[2]    E. Best, R. Devillers, A. Kiehn, and L. Pomello.  Concurrent bisimulations in Petri nets.

        Acta Informatica, 28(3):231-264, 1991.
 
[3]    U. Montanari and M. Pistore.  Minimal transition systems for history-preserving bisimulation.

        In 14th Annual Symposium on Theoretical Aspects of Computer Science, volume 1200 of LNCS, pages 413-425.
        Springer Verlag, 1997.
 
[4]    U. Montanari and M.  Pistore.History-dependent automata.

        Technical Report TR-98-11, Dipartimento di Informatica, 1998.
        Available as ftp://ftp.di.unipi.it/pub/techreports/TR-98-11.ps.Z.
 
[5]    A. Rabinovich and B. A. Trakhtenbrot.  Behavior Structures and Nets.

        Fundamenta Informaticæ, 11(4):357-404, 1988.
 
[6]    R. van Glabbeek and U. Goltz.  Equivalence notions for concurrent systems and refinement of actions.

        In A. Kreczmar and G. Mirkowska, editors, Proceedings of MFCS'89, volume 39 of LNCS, pages 237-248.
        Springer Verlag, 1989.
 
[7]    W. Vogler.  Deciding history preserving bisimilarity.

        In J. Leach Albert, B. Monien, and M. Rodríguez-Artalejo, editors, Proceedings of ICALP'91, volume 510 of LNCS,
        pages 495-505. Springer-Verlag, 1991.