Bisimulation versus trace equivalence
Richard Garner – 13 April 2022
A labelled transition system with label-set B comprises a set of states S together with an operation which to each state from S, non-deterministically assigns an output symbol in B and a new state in S. A probabilistic generative system is the same thing, except that the non-deterministic assignment above becomes a probabilistic one.For labelled transition systems and probabilistic generative systems, there are many different meaningful notions of equivalence between states; the extremal choices are bisimulation equivalence and trace equivalence. It is well known that two states of a system are bisimilar if they become the same under the unique map to the final such system. On the other hand, a line of research, started by Power--Turi, and developed further by Hasuo, Jacobs and Sokolova, characterises trace equivalence in terms of equality under the unique map to a terminal object in a suitable Kleisli category.We propose a refinement of the Power--Turi--Hasuo--Jacobs--Sokolova theory, which instead characterises trace equivalence in terms of a terminal object in a suitable category of Eilenberg--Moore algebras. For the examples listed above, this recovers the full infinitary trace given by closed sets of B^N (for labelled transition systems) and probability distributions on B^N (for probabilistic generative systems).
Back