Book contents
- Frontmatter
- Contents
- List of illustrations
- Preface
- General introduction
- 1 Towards bisimulation
- 2 Coinduction and the duality with induction
- 3 Algebraic properties of bisimilarity
- 4 Processes with internal activities
- 5 Other approaches to behavioural equivalences
- 6 Refinements of simulation
- 7 Basic observables
- Appendix A Solutions to selected exercises
- List of notation
- References
- Index
2 - Coinduction and the duality with induction
Published online by Cambridge University Press: 05 August 2012
- Frontmatter
- Contents
- List of illustrations
- Preface
- General introduction
- 1 Towards bisimulation
- 2 Coinduction and the duality with induction
- 3 Algebraic properties of bisimilarity
- 4 Processes with internal activities
- 5 Other approaches to behavioural equivalences
- 6 Refinements of simulation
- 7 Basic observables
- Appendix A Solutions to selected exercises
- List of notation
- References
- Index
Summary
After introducing bisimulation on processes in the previous chapter, we see here other examples of predicates and relations that are defined in a similar style, and proof techniques for them. This style is quite different with respect to that of ordinary inductive definitions and proofs. It is in fact the style of coinduction. Through the examples we will begin to build up some intuition about the difference between coinduction and induction. Then we will make these intuitions formal, using fixed-point theory.
Intuitively, a set A is defined coinductively if it is the greatest solution of an inequation of a certain form; then the coinduction proof principle just says that any set that is solution of the same inequation is contained in A. Dually, a set A is defined inductively if it is the least solution of an inequation of a certain form, and the induction proof principle then says that any other set that is solution to the same inequation contains A. As we will see, familiar inductive definitions and proofs can be formalised in this way.
An abstract formalisation of the meaning of coinduction is not necessary for applications. In the previous chapter, for instance, we have seen that bisimulation can be defined on processes without talking about fixed points. But the theory of fixed points allows us to understand what we are doing, and to understand the analogies among different worlds.
- Type
- Chapter
- Information
- Introduction to Bisimulation and Coinduction , pp. 28 - 88Publisher: Cambridge University PressPrint publication year: 2011