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

, ,
Software Engineering [SEN]
Computer Security

Rutten, J.J.M.M. (1998). A note on coinduction and weak bisimilarity for while programs. Software Engineering [SEN]. CWI.