# A note on Coinduction and Weak Bisimilarity for While Programs

RAIRO - Theoretical Informatics and Applications (2010)

- Volume: 33, Issue: 4-5, page 393-400
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topRutten, J. J.M.M.. "A note on Coinduction and Weak Bisimilarity for While Programs." RAIRO - Theoretical Informatics and Applications 33.4-5 (2010): 393-400. <http://eudml.org/doc/222056>.

@article{Rutten2010,

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.
},

author = {Rutten, J. J.M.M.},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = { Coalgebra; automaton; weak bisimulation; coinduction;
while program.; weak bisimilarity},

language = {eng},

month = {3},

number = {4-5},

pages = {393-400},

publisher = {EDP Sciences},

title = {A note on Coinduction and Weak Bisimilarity for While Programs},

url = {http://eudml.org/doc/222056},

volume = {33},

year = {2010},

}

TY - JOUR

AU - Rutten, J. J.M.M.

TI - A note on Coinduction and Weak Bisimilarity for While Programs

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

PB - EDP Sciences

VL - 33

IS - 4-5

SP - 393

EP - 400

AB -
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.

LA - eng

KW - Coalgebra; automaton; weak bisimulation; coinduction;
while program.; weak bisimilarity

UR - http://eudml.org/doc/222056

ER -

## References

top- S.L. Bloom and Z. Ésik, The equational logic of fixed points. Theoret. Comput. Sci.179 (1997) 1-60.
- 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.
- 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.

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.