A Complete Axiomatisation for Observational Congruence of Finite-state Behaviours

R. Milner

Abstract: Finite state automata, with non-determinism and silent transitions, can be interpreted not as subsets of the free monoid as in classical automata theory, but as congruence classes under a congruence relation based upon the idea of bisimulation due to Park. In this paper a complete axiomatisation for this congruence is presented. It extends the previously known complete axiomatisation by Hennessy and Milner for finite automata (no cycles); the extension consists of file recursion rules.

LFCS report ECS-LFCS-86-8

Previous | Index | Next