A note on Coinduction and Weak Bisimilarity for While Programs
- 1 July 1999
- journal article
- Published by EDP Sciences in RAIRO - Theoretical Informatics and Applications
- Vol. 33 (4-5) , 393-400
- https://doi.org/10.1051/ita:1999125
Abstract
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.Keywords
This publication has 2 references indexed in Scilit:
- Automata and coinduction (an exercise in coalgebra)Published by Springer Nature ,1998
- The equational logic of fixed pointsTheoretical Computer Science, 1997