Partial-congruence factorization of bisimilarity induced by open maps

Abstract

We investigate some relationships between bisimilarity defined by open maps and behavioural equivalence factorized by indistin-guishability relations. This is done in the setting of a concrete category supporting algebraic constructions of subobject and quotient. Some sufficient condition is found for bisimilarity to be factorizable by the greatest open congruences. We also find a necessary and sufficient condition for a factorization of bisimilarity: quotients by all maximal open congruences are isomorphic. The general results are motivated and illustrated by important examples: transition systems, event structures and presheaves.