×

zbMATH — the first resource for mathematics

Computing maximal weak and other bisimulations. (English) Zbl 1355.68190
Summary: 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. We concentrate on algorithms which work efficiently when implemented rather than on ones which have low asymptotic growth.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Armstrong P, Goldsmith M, Lowe G, Ouaknine J, Palikareva H, Roscoe AW, Worrell J (2012) Recent developments in FDR. In: Computer aided verification. Springer, pp 699-704 · Zbl 0251.05107
[2] Boulgakov A, Gibson-Robinson T, Roscoe AW (2014) Computing maximal bisimulations. In: Formal methods and software engineering. Springer, pp 11-26 · Zbl 0882.68085
[3] Blom, S; Orzan, S, A distributed algorithm for strong bisimulation reduction of state spaces, Electron Notes Theor Comput Sci, 68, 523-538, (2002) · Zbl 1270.68380
[4] Blom, S; Orzan, S, Distributed state space minimization, Int J Softw Tools Technol Transf, 7, 280-291, (2005)
[5] Blom S, van de Pol J (2009) Distributed branching bisimulation minimization by inductive signatures. arXiv preprint arXiv:0912.2550 · Zbl 0711.68058
[6] Dovier, A; Piazza, C; Policriti, A, An efficient algorithm for computing bisimulation equivalence, Theor Comput Sci, 311, 221-256, (2004) · Zbl 1070.68101
[7] Fernandez, J-C, An implementation of an efficient algorithm for bisimulation equivalence, Sci Comput Program, 13, 219-236, (1990) · Zbl 0711.68058
[8] Floyd, RW, Algorithm 97: shortest path, Commun ACM, 5, 345, (1962)
[9] Garavel, H; Lang, F; Mateescu, R; Serwe, W, CADP 2011: a toolbox for the construction and analysis of distributed processes, Int J Softw Tools Technol Transf, 15, 89-107, (2013) · Zbl 1316.68074
[10] Gibson-Robinson T, Armstrong P, Boulgakov A, Roscoe AW (2015) FDR3: a parallel refinement checker for CSP. Int J Softw Tools Technol Transf 1-19 · Zbl 1392.68300
[11] Groote, JF; Vaandrager, F; Paterson, MS (ed.), An efficient algorithm for branching bisimulation and stuttering equivalence, 626-638, (1990), Berlin · Zbl 0765.68125
[12] Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Inc., Upper Saddle River · Zbl 0637.68007
[13] Kanellakis PC, Smolka SA (1983) CCS expressions, finite state processes, and three problems of equivalence. In: Proceedings of the 2nd annual ACM symposium on principles of distributed computing, PODC ’83, pp 228-240, New York, NY, USA, ACM · Zbl 0882.68085
[14] Mateescu R (2005) On-the-fly state space reductions for weak equivalences. In: Proceedings of the 10th international workshop on formal methods for industrial critical systems, pp 80-89 ACM
[15] Milner R (1981) A modal characterisation of observable machine-behaviour. In: CAAP’81. Springer, pp 25-34
[16] Park D (1981) Concurrency and automata on infinite sequences. Springer, Berlin · Zbl 0457.68049
[17] Paige, R; Tarjan, RE, Three partition refinement algorithms, SIAM J Comput, 16, 973-989, (1987) · Zbl 0654.68072
[18] Phillips ICC, Ulidowski I (1996) Ordered SOS rules and weak bisimulation. Theory Formal Methods
[19] Roscoe AW, Gardiner PHB, Goldsmith MH, Hulance JR, Jackson DM, Scattergood JB (1995) Hierarchical compression for model-checking CSP, or how to check 10\^{20} dining philosophers for deadlock. In: Proceedings of TACAS 1995. BRICS
[20] Roscoe AW (1994) Model-checking CSP. A classical mind: essays in honour of CAR Hoare
[21] Roscoe AW (1998) The theory and practice of concurrency · Zbl 0654.68072
[22] Roscoe AW (2010) Understanding concurrent systems. Springer, Berlin · Zbl 1211.68205
[23] Sangiorgi, D, A theory of bisimulation for the \(π\)-calculus, Acta Informatica, 33, 69-97, (1996) · Zbl 0835.68072
[24] Tarjan, RE, Depth-first search and linear graph algorithms, SIAM J Comput, 1, 146-160, (1972) · Zbl 0251.05107
[25] Tarjan, RE, Edge-disjoint spanning trees and depth-first search, Acta Informatica, 6, 171-185, (1976) · Zbl 0307.05104
[26] Glabbeek, RJ; Weijland, WP, Branching time and abstraction in bisimulation semantics, J ACM, 43, 555-600, (1996) · Zbl 0882.68085
[27] Wimmer R, Herbstritt M, Hermanns H, Strampp K, Becker B (2006) Sigref—a symbolic bisimulation tool box. In: Automated technology for verification and analysis. Springer, pp 477-492 · Zbl 1161.68631
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.