A note on Coinduction and Weak Bisimilarity for While Programs

J. J.M.M. Rutten

RAIRO - Theoretical Informatics and Applications (2010)

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

Abstract

top
An illustration of coinduction in terms of a notion of weak bisimilarity is presented. First, an operational semantics 𝒪 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 𝒟 . Next 𝒪 = 𝒟 is proved by coinduction.

How to cite

top

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

NotesEmbed ?

top

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.