Abstract
We present and compare several algorithms for computing the maximal strong bisimulation, the maximal divergence-respecting delay bisimulation, and the maximal divergence-respecting weak bisimulation of a generalised labelled transition system. These bisimulation relations preserve CSP semantics, as well as the operational semantics of programs in other languages with operational semantics described by such GLTSs and relying only on observational equivalence. They can therefore be used to combat the space explosion problem faced in explicit model checking for such languages
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Park, D.: Concurrency and automata on infinite sequences. Springer, Heidelberg (1981)
Milner, R.: A modal characterisation of observable machine-behaviour. In: Astesiano, E., Böhm, C. (eds.) CAAP 1981. LNCS, vol. 112, pp. 25–34. Springer, Heidelberg (1981)
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43, 555–600 (1996)
Phillips, I., Ulidowski, I.: Ordered SOS rules and weak bisimulation. In: Theory and Formal Methods (1996)
Sangiorgi, D.: A theory of bisimulation for the π-calculus. Acta informatica 33(1), 69–97 (1996)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Inc., Upper Saddle River (1985)
Roscoe, A.W.: The Theory and Practice of Concurrency (1998)
Roscoe, A.W.: Understanding Concurrent Systems. Springer, Heidelberg (2010)
Roscoe, A.W.: Model-Checking CSP. In: A Classical Mind: Essays in Honour of CAR Hoare (1994)
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: FDR3—A Modern Refinement Checker for CSP (2014)
Roscoe, A.W., Gardiner, P., Goldsmith, M., Hulance, J., Jackson, D.M., Scattergood, J.: Hierarchical compression for model-checking CSP, or How to check 1020 dining philosophers for deadlock. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133–152. Springer, Heidelberg (1995)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on Computing 16(6), 973–989 (1987)
Fernandez, J.-C.: An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming 13(2), 219–236 (1990)
Van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics: extended abstract. Rep./Centrum voor wiskunde en informatica. Computer science; CS-R8911 (1989)
Groote, J., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990)
Armstrong, P., Goldsmith, M., Lowe, G., Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: Recent developments in FDR. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 699–704. Springer, Heidelberg (2012)
Floyd, R.W.: Algorithm 97: Shortest path. Commun. ACM 5, 345 (1962)
Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM Journal on Computing 1(2), 146–160 (1972)
Tarjan, R.E.: Edge-disjoint spanning trees and depth-first search. Acta Informatica 6(2), 171–185 (1976)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W. (2014). Computing Maximal Bisimulations. In: Merz, S., Pang, J. (eds) Formal Methods and Software Engineering. ICFEM 2014. Lecture Notes in Computer Science, vol 8829. Springer, Cham. https://doi.org/10.1007/978-3-319-11737-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-11737-9_2
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11736-2
Online ISBN: 978-3-319-11737-9
eBook Packages: Computer ScienceComputer Science (R0)