Hostname: page-component-cd9895bd7-8ctnn Total loading time: 0 Render date: 2024-12-24T17:15:24.452Z 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; [email protected]. URL: www.cwi.nl/~janr
Get access

Abstract

An illustration of coinduction in terms of a notion of weak bisimilarity is presented. First, an operational semantics $\mbox{${\cal 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 $\mbox{${\cal D}$}$. Next $\mbox{${\cal O}$}= \mbox{${\cal D}$}$ is proved by coinduction.

Keywords

Coalgebraautomatonweak bisimulationcoinductionwhile program.
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.)

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