Raiders of the lost equivalence: probabilistic branching bisimilarity. (English) Zbl 1441.68145
Summary: Probabilistic branching bisimilarity allows us to compare process behaviour with respect to their branching structure and probabilistic features, while abstracting away from those computation steps that can be marked as irrelevant to the analysis at hand. To the best of our knowledge, in the context of nondeterministic probabilistic processes, no proof of probabilistic branching bisimilarity being an equivalence has been provided so far. Since, as happened in the fully nondeterministic case, some researchers are using such a result by taking it for granted, we decided to dedicate this note to a formal proof of it. More precisely, we extend and adapt the proof strategy used by Basten in the fully nondeterministic case. Thus, we introduce the probabilistic analogue to the notion of semi-branching bisimilarity and to van Glabbeek and Weijland’s Stuttering Lemma to prove that probabilistic branching bisimilarity is indeed an equivalence relation.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
Keywords:
formal semantics; nondeterministic probabilistic processes; probabilistic branching bisimilarity; semi-branching bisimilarity; equivalence relationsReferences:
| [1] | Andova, S.; Georgievska, S.; Trcka, N., Branching bisimulation congruence for probabilistic systems, Theor. Comput. Sci., 413, 58-72 (2012) · Zbl 1234.68282 |
| [2] | Andova, S.; Willemse, T. A., Branching bisimulation for probabilistic systems: characteristics and decidability, Theor. Comput. Sci., 356, 325-355 (2006) · Zbl 1092.68062 |
| [3] | Baier, C., On Algorithmic Verification Methods for Probabilistic Systems (1998), Fakultät für Mathematik and Informatik Uviversität Mannheim, Ph.D. thesis |
| [4] | Baier, C.; Hermanns, H., Weak bisimulation for fully probabilistic processes, (Proceedings of CAV ’97. Proceedings of CAV ’97, Lecture Notes in Computer Science, vol. 1254 (1997)), 119-130 |
| [5] | Basten, T., Branching bisimilarity is an equivalence indeed!, Inf. Process. Lett., 58, 141-147 (1996) · Zbl 0875.68624 |
| [6] | Belder, T.; ter Beek, M. H.; de Vink, E. P., Coherent branching feature bisimulation, (Proc. FMSPLE@ETAPS 2015 (2015)), 14-30 |
| [7] | Bergstra, J. A.; Ponse, A.; van der Zwaag, M., Branching time and orthogonal bisimulation equivalence, Theor. Comput. Sci., 309, 313-355 (2003) · Zbl 1070.68100 |
| [8] | Castiglioni, V.; Lanotte, R.; Tini, S., A specification format for rooted branching bisimulation, Fundam. Inform., 135, 355-369 (2014) · Zbl 1315.68190 |
| [9] | Castiglioni, V.; Tini, S., Probabilistic divide & congruence: branching bisimilarity, Theor. Comput. Sci., 802, 147-196 (2020) · Zbl 1436.68209 |
| [10] | De Nicola, R.; Montanari, U.; Vaandrager, F. W., Back and forth bisimulations, (Proc. CONCUR ’90. Proc. CONCUR ’90, Lecture Notes in Computer Science, vol. 458 (1990)), 152-165 |
| [11] | De Nicola, R.; Vaandrager, F. W., Three logics for branching bisimulation, J. ACM, 42, 458-487 (1995) · Zbl 0886.68064 |
| [12] | Deng, Y.; Du, W., Logical, metric, and algorithmic characterisations of probabilistic bisimulation (2011), CoRR |
| [13] | Deng, Y.; van Glabbeek, R. J., Characterising probabilistic processes logically - (extended abstract), (Proc. LPAR-17. Proc. LPAR-17, LNCS, vol. 6397 (2010)), 278-293 · Zbl 1306.68122 |
| [14] | Deng, Y.; van Glabbeek, R. J.; Hennessy, M.; Morgan, C., Characterising testing preorders for finite probabilistic processes, Log. Methods Comput. Sci., 4 (2008) · Zbl 1161.68035 |
| [15] | Fokkink, W. J., Rooted branching bisimulation as a congruence, J. Comput. Syst. Sci., 60, 13-37 (2000) · Zbl 0955.68074 |
| [16] | Fokkink, W. J.; van Glabbeek, R. J.; de Wind, P., Divide and congruence: from decomposition of modal formulas to preservation of branching and η-bisimilarity, Inf. Comput., 214, 59-85 (2012) · Zbl 1277.68182 |
| [17] | van Glabbeek, R. J., The linear time - branching time spectrum II, (Proc. CONCUR ’93 (1993)), 66-81 |
| [18] | van Glabbeek, R. J.; Smolka, S. A.; Steffen, B., Reactive, generative and stratified models of probabilistic processes, Inf. Comput., 121, 59-80 (1995) · Zbl 0832.68042 |
| [19] | van Glabbeek, R. J.; Weijland, W. P., Branching time and abstraction in bisimulation semantics (extended abstract), (IFIP Congress (1989)), 613-618 |
| [20] | van Glabbeek, R. J.; Weijland, W. P., Branching time and abstraction in bisimulation semantics, J. ACM, 43, 555-600 (1996) · Zbl 0882.68085 |
| [21] | Groote, J. F.; Jansen, D. N.; Keiren, J. J.A.; Wijs, A., An \(O(m \log n)\) algorithm for computing stuttering equivalence and branching bisimulation, ACM Trans. Comput. Log., 18, 1-34 (2017) · Zbl 1367.68211 |
| [22] | Groote, J. F.; Vaandrager, F. W., An efficient algorithm for branching bisimulation and stuttering equivalence, (Proc. ICALP ’90. Proc. ICALP ’90, Lecture Notes in Computer Science, vol. 443 (1990)), 626-638 · Zbl 0765.68125 |
| [23] | Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Form. Asp. Comput., 6, 512-535 (1994) · Zbl 0820.68113 |
| [24] | Hansson, H. A., Time and probabilities in specification and verification of real-time systems, (Proc. RTS 1992 (1992)), 92-97 |
| [25] | Hennessy, M., Exploring probabilistic bisimulations, part I, Form. Asp. Comput., 24, 749-768 (2012) · Zbl 1259.68153 |
| [26] | Hennessy, M.; Regan, T., A process algebra for timed systems, Inf. Comput., 117, 221-239 (1995) · Zbl 0826.68068 |
| [27] | Jou, C.; Smolka, S. A., Equivalences, congruences, and complete axiomatizations for probabilistic processes, (Proceedings of CONCUR ’90. Proceedings of CONCUR ’90, Lecture Notes in Computer Science, vol. 458 (1990)), 367-383 |
| [28] | Keller, R. M., Formal verification of parallel programs, Commun. ACM, 19, 371-384 (1976) · Zbl 0329.68016 |
| [29] | Lee, M. D.; de Vink, E. P., Rooted branching bisimulation as a congruence for probabilistic transition systems, (Proc. QAPL 2015. Proc. QAPL 2015, EPTCS, vol. 194 (2015)), 79-94 |
| [30] | Lynch, N. A.; Segala, R.; Vaandrager, F. W., Observing branching structure through probabilistic contexts, SIAM J. Comput., 37, 977-1013 (2007) · Zbl 1156.68020 |
| [31] | Milner, R., A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol. 92 (1980) · Zbl 0452.68027 |
| [32] | Park, D. M., Concurrency and automata of infinite sequences, (5th GI Conference. 5th GI Conference, LNCS, vol. 104 (1981)), 167-183 · Zbl 0457.68049 |
| [33] | Philippou, A.; Lee, I.; Sokolsky, O., Weak bisimulation for probabilistic systems, (Proc. CONCUR 2000. Proc. CONCUR 2000, Lecture Notes in Computer Science, vol. 1877 (2000)), 334-349 · Zbl 0999.68146 |
| [34] | Segala, R., Modeling and Verification of Randomized Distributed Real-Time Systems (1995), MIT, Ph.D. thesis |
| [35] | Segala, R.; Lynch, N. A., Probabilistic simulations for probabilistic processes, (Proceedings of CONCUR ’94. Proceedings of CONCUR ’94, Lecture Notes in Computer Science, vol. 836 (1994)), 481-496 |
| [36] | Timmer, M.; Katoen, J.; van de Pol, J.; Stoelinga, M., Confluence reduction for Markov automata, Theor. Comput. Sci., 655, 193-219 (2016) · Zbl 1356.68136 |
| [37] | Trcka, N., Strong, weak and branching bisimulation for transition systems and Markov reward chains: a unifying matrix approach, (Proc. QFM 2009. Proc. QFM 2009, EPTCS, vol. 13 (2009)), 55-65 |
| [38] | Turrini, A.; Hermanns, H., Polynomial time decision algorithms for probabilistic automata, Inf. Comput., 244, 134-171 (2015) · Zbl 1329.68168 |
| [39] | Yang, X.; Katoen, J.; Lin, H.; Liu, G.; Wu, H., Branching bisimulation and concurrent object verification, (Proc. DSN 2018 (2018)), 267-278 |
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.
