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
topHow 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 ?
topYou must be logged in to post comments.
To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.