Cited By
View all- Cranen SKeiren JWillemse T(2018)Parity game reductionsActa Informatica10.1007/s00236-017-0301-x55:5(401-444)Online publication date: 1-Aug-2018
Branching Bisimulation Games
Pages 142 - 157
Abstract
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 $$\textsc {Spoiler}$$SPOILER and $$\textsc {Duplicator}$$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.
References
[1]
Basten, T.: Branching bisimilarity is an equivalence indeed!. Inform. Process. Lett. 583, 141---147 1996
[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
[3]
Bulychev, P.E., Konnov, I.V., Zakharov, V.A.: Computing bisimulation 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
[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. 152, 89---107 2013
[6]
Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. Inform. Comput. 1502, 132---152 1999
[7]
Grädel, E., Thomas, W., Wilke, T. eds.: Automata Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg 2002
[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
[9]
Groote, J.F., Wijs, A.: An Om 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.
[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
[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
[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
[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
[14]
Reniers, M.A., Schoren, R., Willemse, T.A.C.: Results on embeddings between state-based and event-based systems. Comput. J. 571, 73---92 2014
[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
[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
[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
[18]
van Glabbeek, R.J., Luttik, S.P., Trçka, N.: Branching bisimilarity with explicit divergence. Fundam. Inform. 934, 371---392 2009
[19]
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 433, 555---600 1996
[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
Index Terms
- Branching Bisimulation Games
Recommendations
Branching bisimulation for probabilistic systems: characteristics and decidability
Expressiveness in concurrencyWe address the concept of abstraction in the setting of probabilistic reactive systems, and study its formal underpinnings for the strictly alternating model of Hansson. In particular, we define the notion of branching bisimilarity and study its ...
Branching time and abstraction in bisimulation semantics
In comparative concurrency semantics, one usually distinguishes between linear time and branching time semantic equivalences. Milner's notion of observatin equivalence is often mentioned as the standard example of a branching time equivalence. In this ...
Branching bisimulation semantics for quantum processes
AbstractThe qCCS model proposed by Feng et al. provides a powerful framework to describe and reason about quantum communication systems that could be entangled with the environment. However, they only studied weak bisimulation semantics. In this paper we ...
Highlights- A new branching bisimilarity for quantum CCS has been proposed based on the notion of ϵ-tree.
- This bisimilarity has been shown to be a congruence relation.
- An efficient verification algorithm for the ground version of our branching ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 06 June 2016
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 27 Nov 2024
Other Metrics
Citations
Cited By
View all- Cranen SKeiren JWillemse T(2018)Parity game reductionsActa Informatica10.1007/s00236-017-0301-x55:5(401-444)Online publication date: 1-Aug-2018
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in