A note on Coinduction and Weak Bisimilarity for While Programs

Issue		RAIRO-Theor. Inf. Appl. Volume 33, Number 4/5, July-October 1999


Page(s)		393 - 400
DOI		10.1051/ita:1999125

DOI: 10.1051/ita:1999125
Theoret. Informatics Appl. 33 (1999) 393-400

A note on Coinduction and Weak Bisimilarity for While Programs

J.J.M.M. Rutten
CWI, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands; (janr@cwi.nl) URL: www.cwi.nl/ $\sim$ janr

Received October 20, 1998. Revised April 26, 1999.

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 and phrases: Coalgebra, automaton, weak bisimulation, coinduction, while program.

AMS Subject Classification: 68Q10, 68Q55

What is OpenURL?

The OpenURL standard is a protocol for transmission of metadata describing the resource that you wish to access. An OpenURL link contains article metadata and directs it to the OpenURL server of your choice. The OpenURL server can provide access to the resource and also offer complementary services (specific search engine, export of references...). The OpenURL link can be generated by different means.

If your librarian has set up your subscription with an OpenURL resolver, OpenURL links appear automatically on the abstract pages.
You can define your own OpenURL resolver with your EDPS Account. In this case your choice will be given priority over that of your library.
You can use an add-on for your browser (Firefox or I.E.) to display OpenURL links on a page (see http://www.openly.com/openurlref/). You should disable this module if you wish to use the OpenURL server that you or your library have defined.