A Complete Axiomatisation for Observational Congruence of Finite-State Behaviors

Robin Milner

Research output: Contribution to journalArticlepeer-review

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 notion of weak bisimulation or observational equivalence due to Park and Milner. In this paper a complete axiomatisation for this congruence is presented. It extends the previously known complete axiomatisation by Hennessy and Milner for the case when all computations are finite; the extension consists of five simple rules for recursion.
Original languageEnglish
Pages (from-to)227-247
Number of pages21
JournalInformation and Computation
Volume81
Issue number2
DOIs
Publication statusPublished - May 1989

Fingerprint

Dive into the research topics of 'A Complete Axiomatisation for Observational Congruence of Finite-State Behaviors'. Together they form a unique fingerprint.

Cite this