Hostname: page-component-74656f9884-npj9w Total loading time: 0 Render date: 2026-11-07T18:14:15.326Z Has data issue: false hasContentIssue false
  • English
  • Français

A note on Coinduction and Weak Bisimilarity for While Programs

Published online by Cambridge University Press:  15 August 2002

J. J.M.M. Rutten
J. J.M.M. Rutten*
Affiliation:
CWI, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands; janr@cwi.nl. URL: www.cwi.nl/~janr
Get access

Abstract

An illustration of coinduction in terms of a notionof weak bisimilarity is presented.First, an operational semantics $\mbox{${\cal O}$}$ for while programs is definedin terms of a final automaton. It identifies any twoprograms that are weakly bisimilar, and induces in acanonical manner a compositional model $\mbox{${\cal D}$}$ .Next $\mbox{${\cal O}$}= \mbox{${\cal D}$}$ is proved by coinduction.

Keywords

Coalgebraautomatonweak bisimulationcoinductionwhileprogram.

Information

Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 33 , Issue 4-5 , July 1999 , pp. 393 - 400
Copyright
© EDP Sciences, 1999

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable

References

Bloom, S.L. and Ésik, Z., The equational logic of fixed points. Theoret. Comput. Sci. 179 (1997) 1-60. CrossRef
J.W. de Bakker, Mathematical theory of program correctness. Prentice-Hall International (1980).
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.
R. Milner, Communication and Concurrency. Prentice Hall International, New York, Prentice Hall Internat. Ser. Comput. Sci. (1989).
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.
Rutten, J.J.M.M., 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. CrossRef