Bisimulations and abstraction homomorphisms

Abstract

In this paper we show that the notion of bisimulation 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. The reduction relation is proven to enjoy some desirable properties, notably a 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.