Bisimulation was introduced by Park and
Milner [1]}, [2]} for characterizing the
equivalence of two processes specified by transition systems or process algebra
terms. Over the years the notion has had an enduring impact on the study of the
behaviour of systems, with ramifications in concurrency, automata theory, modal
logic, coalgebras, games and formal verification. The basic notion of
bisimulation for discrete systems has been extended to probabilistic,
quantitative and even continuous systems.
