A note on coinduction and weak bisimiliarity for while programs. (English) Zbl 0945.68073

Summary: An illustration of coinduction in terms of a notion of weak bisimilarity is presented. First, an operational semantics \({\mathcal O}\) for while programs is defined in terms of a final automaton. It identifies any two programs that are weakly bisimilar, and induces in a canonical manner a compositional model \({\mathcal D}\). Next, \({\mathcal O}= {\mathcal D}\) is proved by coinduction.


68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
Full Text: DOI EuDML


[1] S.L. Bloom and Z. Ésik, The equational logic of fixed points. Theoret. Comput. Sci.179 (1997) 1-60. · Zbl 0920.03067
[2] J.W. de Bakker, Mathematical theory of program correctness. Prentice-Hall International (1980). · Zbl 0452.68011
[3] C.C. Elgot, Monadic computation and iterative algebraic theories, H.E. Rose and J.C. Shepherdson, Eds., Logic Colloquium ’73. North-Holland, Stud. Log. Found. Math. 80 (1975) 175-230. Zbl0327.02040 · Zbl 0327.02040
[4] R. Milner, Communication and Concurrency. Prentice Hall International, New York, Prentice Hall Internat. Ser. Comput. Sci. (1989). · Zbl 0683.68008
[5] J.J.M.M. Rutten, Universal coalgebra: A theory of systems. Report CS-R9652, CWI, 1996. FTP-available at ftp.cwi.nl as pub/CWIreports/AP/CS-R9652.ps.Z. Theoret. Comput. Sci., to appear.
[6] J.J.M.M. Rutten, Automata and coinduction (an exercise in coalgebra). Report SEN-R9803, CWI, 1998. FTP-available at ftp.cwi.nl as pub/CWIreports/SEN/SEN-R9803.ps.Z. Also in the proceedings of CONCUR ’98, Lecture Notes in Comput. Sci.1466 (1998) 194-218. · Zbl 0940.68085
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.