Madhavan Mukund

Hereditary history preserving bisimulation is decidable for trace-labelled systems

M Mukund

Proc. FSTTCS '02, Springer LNCS 2556 (2002) 289-300.

© Springer-Verlag Berlin Heidelberg


Hereditary history preserving bisimulation is a natural extension of bisimulation to the setting of so-called ``true'' concurrency. Somewhat surprisingly, this extension turns out to be undecidable, in general, for finite-state concurrent systems. In this paper, we show that for a substantial and useful class of finite-state concurrent systems - those whose semantics can be described in terms of Mazurkiewicz traces -hereditary history preserving is decidable.

  • Download PDF.