Bisimulations and abstraction homomorphisms

摘要

We show that the notion of bisimulation equivalence for a class of labelled transition systems (the class of nondeterministic processes) may be restated as one of “reducibility to a same system” via a simple reduction relation. This relation is proved to enjoy some desirable properties, notably the Church-Rosser property. We also show that, when restricted to finite nondeterministic processes, the relation yields unique minimal forms for processes and can be characterised algebraically by a set of reduction rules.