Abstract
In this chapter, two-player games are used as a tool for distinguishing between processes: in a simple copy-cat game, the first player aims at showing that two processes are different while the second player tries to show that they are equivalent. Such games, in which the second player must replicate each move by the first player on one process by a move along the same label in the other process, prepare for a more formal definition of bisimulation equivalence. Games can either be limited to a finite number of moves or be infinite, and notions of game equivalences parametrised by the length of the game are defined in terms of the existence of a winning strategy for the second player. It is then shown that properties of finite bisimulation games can be established by induction whereas those of infinite games require a different, coinductive approach. Next, a bisimulation relation on processes or labelled transition systems is formally defined and a proof principle for infinite games based on bisimulation relations is provided. Finally, a partition-refinement algorithm for infinite game equivalence based on bisimulation colourings is introduced, and bisimulation games for arbitrary ordinals are investigated.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag London
About this chapter
Cite this chapter
Moller, F., Struth, G. (2013). Distinguishing Between Processes. In: Modelling Computing Systems. Undergraduate Topics in Computer Science. Springer, London. https://doi.org/10.1007/978-1-84800-322-4_13
Download citation
DOI: https://doi.org/10.1007/978-1-84800-322-4_13
Published:
Publisher Name: Springer, London
Print ISBN: 978-1-84800-321-7
Online ISBN: 978-1-84800-322-4
eBook Packages: Computer ScienceComputer Science (R0)