In: Recent Trends in Algebraic Development Techniques: 14th International Workshop, WADT 99, Chateau de Bonas, September 15-18, 1999, pages 291-310. Volume 1827 of Lecture Notes in Computer Science / Didier Bert, Christine Choppy and Peter D. Mosses (Eds.) --- Springer-Verlag, September 1999.
Abstract: We investigate the notion of history preserving bisimulation 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 Winskels prime event structures. A finer equivalence, called RHP-bisimulation (where R stands for read), relies on asymmetric event structures, a generalization of prime event structures which gives a more faithful account of the dependencies among transition occurrences arising in contextual net computations. Extending previous work, we show that HP-bisimulation is decidable for finite n-safe contextual nets. Moreover by resorting to causal automata, 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.