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
3 - Algebraic properties of bisimilarity
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
In this chapter we introduce some common process operators, which impose a structure on processes and bring in concepts from algebra. The operators we consider are inspired by those of the Calculus of Communicating Systems (CCS) [Mil89, AILS07], one of the most studied process calculi. Given a process calculus (or a language), one obtains an LTS by providing, for each operator, a set of inference rules that determine the possible transitions of the processes in the syntax-driven fashion of Plotkin's Structured Operational Semantics (SOS) [Plo04a, Plo04b]. We restrain from going into a thorough discussion on process calculi. We do present, however, nearly all the operators of CCS. What here, and in the following chapters, is called CCS is in fact very close to the standard presentation as in, e.g., [Mil89, AILS07]. The only technical differences are that we do not introduce the relabelling operator, and, for writing processes with an infinite behaviour, we use constant symbols instead of recursive process equations; each constant comes with its own transitions. These differences are discussed in Remark 3.5.8 and following exercises, and Remark 3.2.3.
The chapter offers a number of examples of the bisimulation proof method. The method is used to prove that bisimilarity is preserved by the operators considered (and that therefore it is a congruence in CCS), to prove some basic algebraic laws, and in various examples.
- Type
- Chapter
- Information
- Introduction to Bisimulation and Coinduction , pp. 89 - 107Publisher: Cambridge University PressPrint publication year: 2011