×

Branching bisimulation games. (English) Zbl 1347.68276

Albert, Elvira (ed.) et al., Formal techniques for distributed objects, components, and systems. 36th IFIP WG 6.1 international conference, FORTE 2016, held as part of the 11th international federated conference on distributed computing techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6–9, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-39569-2/pbk; 978-3-319-39570-8/ebook). Lecture Notes in Computer Science 9688, 142-157 (2016).
Summary: Branching bisimilarity and branching bisimilarity with explicit divergences are typically used in process algebras with silent steps when relating implementations to specifications. When an implementation fails to conform to its specification, i.e., when both are not related by branching bisimilarity [with explicit divergence], pinpointing the root causes can be challenging. In this paper, we provide characterisations of branching bisimilarity [with explicit divergence] as games between \(\mathsc {Spoiler}\) and \(\mathsc {Duplicator}\), offering an operational understanding of both relations. Moreover, we show how such games can be used to assist in diagnosing non-conformance between implementation and specification.
For the entire collection see [Zbl 1339.68004].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

mCRL; CADP; mCRL2
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Basten, T.: Branching bisimilarity is an equivalence indeed!. Inform. Process. Lett. 58(3), 141–147 (1996) · Zbl 0875.68624 · doi:10.1016/0020-0190(96)00034-8
[2] Blom, S., Fokkink, W.J., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.: mgrCRL: a toolset for analysing algebraic specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Heidelberg (2001) · Zbl 0991.68640 · doi:10.1007/3-540-44585-4_23
[3] Bulychev, P.E., Konnov, I.V., Zakharov, V.A.: Computing (bi)simulation relations preserving CTL*-X for ordinary and fair Kripke structures. Inst. Syst. Program. Russ. Acad. Sci. Math. Meth. Algorithm 12, 59–76 (2007)
[4] Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 199–213. Springer, Heidelberg (2013) · Zbl 1381.68198 · doi:10.1007/978-3-642-36742-7_15
[5] 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(2), 89–107 (2013) · Zbl 1316.68074 · doi:10.1007/s10009-012-0244-z
[6] Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. Inform. Comput. 150(2), 132–152 (1999) · Zbl 1045.68588 · doi:10.1006/inco.1998.2778
[7] Grädel, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002) · Zbl 1011.00037
[8] Groote, J.F., Vaandrager, F.W.: An efficient algorithm for branching and stuttering equivalence. In: Paterson, M.S. (ed.) Automata, Languages and Programming. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990) · Zbl 0765.68125 · doi:10.1007/BFb0032063
[9] Groote, J.F., Wijs, A.: An O(m log n) algorithm for stuttering equivalence and branching bisimulation. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 607–624. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49674-9_40 · doi:10.1007/978-3-662-49674-9_40
[10] Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol. 85, pp. 299–309. Springer, Heidelberg (1980) · Zbl 0441.68018 · doi:10.1007/3-540-10003-2_79
[11] Korver, H.: Computing distinguishing formulas for branching bisimulation. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 13–23. Springer, Heidelberg (1992) · doi:10.1007/3-540-55179-4_3
[12] Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol. 1346, pp. 284–296. Springer, Heidelberg (1997) · doi:10.1007/BFb0058037
[13] Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Theoretical Computer Science. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981) · doi:10.1007/BFb0017309
[14] Reniers, M.A., Schoren, R., Willemse, T.A.C.: Results on embeddings between state-based and event-based systems. Comput. J. 57(1), 73–92 (2014) · doi:10.1093/comjnl/bxs156
[15] Stevens, P., Stirling, C.: Practical model-checking using games. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 85–101. Springer, Heidelberg (1998) · doi:10.1007/BFb0054166
[16] Stirling, C.: Modal and temporal logics for processes. In: Moller, F., Birtwistle, G. (eds.) Structure versus Automata. LNCS, vol. 1043, pp. 149–237. Springer, Heidelberg (1996) · doi:10.1007/3-540-60915-6_5
[17] Thomas, W.: On the Ehrenfeucht-Fraïssé game in theoretical computer science. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) TAPSOFT’93: Theory and Practice of Software Development. LNCS, vol. 668, pp. 559–568. Springer, Heidelberg (1993) · doi:10.1007/3-540-56610-4_89
[18] van Glabbeek, R.J., Luttik, S.P., Trçka, N.: Branching bisimilarity with explicit divergence. Fundam. Inform. 93(4), 371–392 (2009) · Zbl 1183.68404
[19] van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996) · Zbl 0882.68085 · doi:10.1145/233551.233556
[20] Yin, Q., Fu, Y., He, C., Huang, M., Tao, X.: Branching bisimilarity checking for PRS. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573, pp. 363–374. Springer, Heidelberg (2014) · Zbl 1409.68190 · doi:10.1007/978-3-662-43951-7_31
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.