×

Probabilistic divide & congruence: branching bisimilarity. (English) Zbl 1436.68209

Summary: Since the seminal paper by B. Bloom et al. [ACM Trans. Comput. Log. 5, No. 1, 26–78 (2004; Zbl 1367.68209)], the Divide and Congruence technique allows for the derivation of compositional properties of nondeterministic processes from the SOS-based decomposition of their modal properties. In an earlier paper, we extended their technique to deal also with quantitative aspects of process behavior: we proved the (pre)congruence property for strong (bi)simulations on processes with nondeterminism and probability. In this paper we further extend our decomposition method to favor compositional reasoning with respect to probabilistic weak semantics. In detail, we consider probabilistic branching and rooted probabilistic branching bisimilarity, and we propose logical characterizations for them. These are strongly based on the modal operator \(\langle \varepsilon \rangle\) which combines quantitative information and weak semantics by introducing a sort of probabilistic lookahead on process behavior. Our enhanced method will exploit distribution specifications, an SOS-like framework defining the probabilistic behavior of processes, to decompose this particular form of lookahead. We will show how we can apply the proposed decomposition method to derive congruence formats for the considered equivalences from their logical characterizations.

MSC:

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

Citations:

Zbl 1367.68209
Full Text: DOI

References:

[1] Aceto, Luca; Fokkink, Wan J.; Verhoef, Chris, Structural operational semantics, (Handbook of Process Algebra (2001), Elsevier), 197-292 · Zbl 1062.68074
[2] Aldini, Alessandro; Di Pierro, Alessandra, A quantitative approach to noninterference for probabilistic systems, Electron. Notes Theor. Comput. Sci., 99, 155-182 (2004)
[3] Andova, Suzana, Process algebra with probabilistic choice, (Proceedings of ARTS’99. Proceedings of ARTS’99, LNCS, vol. 1601 (1999)), 111-129
[4] Andova, Suzana, Probabilistic Process Algebra (2002), Eindhoven University of Technology, Ph.D. thesis · Zbl 0983.68133
[5] Andova, Suzana; Georgievska, Sonja; Trcka, Nikola, Branching bisimulation congruence for probabilistic systems, Theor. Comput. Sci., 413, 1, 58-72 (2012) · Zbl 1234.68282
[6] Baeten, Jos C. M.; Weijland, Willem P., Process Algebra (1990), Cambridge University Press · Zbl 0716.68002
[7] Bartels, Falk, On Generalised Coinduction and Probabilistic Specification Formats: Distributive Laws in Coalgebraic Modelling (2004), VU University Amsterdam, Ph.D. thesis
[8] Basten, Twan, Branching bisimilarity is an equivalence indeed!, Inf. Process. Lett., 58, 3, 141-147 (1996) · Zbl 0875.68624
[9] Bloom, Bard, Structural operational semantics for weak bisimulations, Theor. Comput. Sci., 146, 1&2, 25-68 (1995) · Zbl 0873.68130
[10] Bloom, Bard; Fokkink, Wan J.; van Glabbeek, Rob J., Precongruence formats for decorated trace semantics, ACM Trans. Comput. Log., 5, 1, 26-78 (2004) · Zbl 1367.68209
[11] Bloom, Bard; Istrail, Sorin; Meyer, Albert R., Bisimulation can’t be traced, J. ACM, 42, 1, 232-268 (1995) · Zbl 0886.68027
[12] Castiglioni, Valentina; Gebler, Daniel; Tini, Simone, Logical characterization of bisimulation metrics, (Proceedings of QAPL 2016. Proceedings of QAPL 2016, EPTCS, vol. 227 (2016)), 44-62
[13] Castiglioni, Valentina; Gebler, Daniel; Tini, Simone, Modal decomposition on nondeterministic probabilistic processes, (Proceedings of CONCUR 2016. Proceedings of CONCUR 2016, LIPIcs 59 (2016)), 36:1-36:15 · Zbl 1392.68288
[14] Castiglioni, Valentina; Gebler, Daniel; Tini, Simone, SOS-based modal decomposition on nondeterministic probabilistic processes, Log. Methods Comput. Sci., 14, 2 (2018) · Zbl 1448.68333
[15] Castiglioni, Valentina; Tini, Simone, Logical characterization of branching metrics for nondeterministic probabilistic transition systems, Inf. Comput. (2019) · Zbl 1430.68161
[16] Clark, Keith L., Negation as failure, (Logic and Data Bases (1977)), 293-322
[17] D’Argenio, Pedro R.; Gebler, Daniel; Lee, Matias D., Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules, (Proceedings of FoSSaCS 2014. Proceedings of FoSSaCS 2014, LNCS, vol. 8412 (2014)), 289-303 · Zbl 1405.68182
[18] D’Argenio, Pedro R.; Gebler, Daniel; Lee, Matias D., A general SOS theory for the specification of probabilistic transition systems, Inf. Comput., 249 (2016) · Zbl 1344.68163
[19] D’Argenio, Pedro R.; Lee, Matias D., Probabilistic transition system specification: congruence and full abstraction of bisimulation, (Proceedings of FoSSaCS 2012. Proceedings of FoSSaCS 2012, LNCS, vol. 7213 (2012)), 452-466 · Zbl 1352.68180
[20] De Nicola, Rocco; Vaandrager, Frits W., Three logics for branching bisimulation, J. ACM, 42, 2, 458-487 (1995) · Zbl 0886.68064
[21] Deng, Yuxin, Semantics of Probabilistic Processes: an Operational Approach (2015), Springer · Zbl 1315.68002
[22] Deng, Yuxin; Chothia, Tom; Palamidessi, Catuscia; Pang, Jun, Metrics for action-labeled quantitative transition systems, Electron. Notes Theor. Comput. Sci., 153, 2, 79-96 (2006)
[23] Deng, Yuxin; Du, Wenjie, Probabilistic barbed congruence, Electron. Notes Theor. Comput. Sci., 190, 3, 185-203 (2007) · Zbl 1279.68255
[24] Deng, Yuxin; Du, Wenjie, Logical, metric, and algorithmic characterisations of probabilistic bisimulation (2011), CoRR
[25] Deng, Yuxin; van Glabbeek, Rob J., Characterising probabilistic processes logically - (extended abstract), (Proceedings of LPAR-17. Proceedings of LPAR-17, LNCS, vol. 6397 (2010)), 278-293 · Zbl 1306.68122
[26] Deng, Yuxin; van Glabbeek, Rob J.; Hennessy, Matthew; Morgan, Carrol, Characterising testing preorders for finite probabilistic processes, Log. Methods Comput. Sci., 4, 4 (2008) · Zbl 1161.68035
[27] Deng, Yuxin; van Glabbeek, Rob J.; Hennessy, Matthew; Morgan, Carroll; Zhang, Chenyi, Remarks on testing probabilistic processes, Electron. Notes Theor. Comput. Sci., 172, 359-397 (2007) · Zbl 1277.68121
[28] Desharnais, Josée; Gupta, Vineet; Jagadeesan, Radha; Panangaden, Prakash, Metrics for labeled Markov processes, Theor. Comput. Sci., 318, 3, 323-354 (2004) · Zbl 1068.68093
[29] Desharnais, Josée; Jagadeesan, Radha; Gupta, Vineet; Panangaden, Prakash, The metric analogue of weak bisimulation for probabilistic processes, (Proceedings of LICS 2002 (2002)), 413-422 · Zbl 1012.68139
[30] Florescu, Oana; de Hoon, Menno; Voeten, Jeroen; Corporaal, Henk, Probabilistic modelling and evaluation of soft real-time embedded systems, (Proceedings of SAMOS 2006. Proceedings of SAMOS 2006, LNCS, vol. 4017 (2006)), 206-215
[31] Fokkink, Wan J., Rooted branching bisimulation as a congruence, J. Comput. Syst. Sci., 60, 1, 13-37 (2000) · Zbl 0955.68074
[32] Fokkink, Wan J.; van Glabbeek, Rob J., Divide and congruence II: delay and weak bisimilarity, (Proceedings of LICS 2016 (2016)), 778-787 · Zbl 1392.68299
[33] Fokkink, Wan J.; van Glabbeek, Rob J., Divide and congruence II: from decomposition of modal formulas to preservation of delay and weak bisimilarity, Inf. Comput., 257, 79-113 (2017) · Zbl 1380.68295
[34] Fokkink, Wan J.; van Glabbeek, Rob J., Precongruence formats with lookahead through modal decomposition, (Proceedings of CSL 2017. Proceedings of CSL 2017, LIPIcs 82 (2017)), 25:1-25:20 · Zbl 1440.68168
[35] Fokkink, Wan J.; van Glabbeek, Rob J.; Luttik, Bas, Divide and congruence III: stability & divergence, (Proceedings of CONCUR 2017. Proceedings of CONCUR 2017, LIPIcs 85 (2017)), 15:1-15:16 · Zbl 1442.68139
[36] Fokkink, Wan J.; van Glabbeek, Rob J.; de Wind, Paulien, Compositionality of Hennessy-Milner logic by structural operational semantics, Theor. Comput. Sci., 354, 3, 421-440 (2006) · Zbl 1088.68094
[37] Fokkink, Wan J.; van Glabbeek, Rob J.; de Wind, Paulien, Divide and congruence: from decomposition of modal formulas to preservation of branching and η-bisimilarity, Inf. Comput., 214, 59-85 (2012) · Zbl 1277.68182
[38] Foster, Nate; Kozen, Dexter; Mamouras, Konstantinos; Reitblatt, Mark; Silva, Alexandra, Probabilistic NetKAT, (Proceedings of ESOP 2016. Proceedings of ESOP 2016, LNCS, vol. 9632 (2016)), 282-309 · Zbl 1335.68027
[39] Gebler, Daniel; Fokkink, Wan J., Compositionality of probabilistic Hennessy-Milner logic through structural operational semantics, (Proceedings of CONCUR 2012. Proceedings of CONCUR 2012, LNCS, vol. 7454 (2012)), 395-409 · Zbl 1364.68285
[40] Gebler, Daniel; Larsen, Kim G.; Tini, Simone, Compositional metric reasoning with probabilistic process calculi, Log. Methods Comput. Sci., 12, 4 (2016) · Zbl 1398.68365
[41] Gebler, Daniel; Tini, Simone, Compositionality of approximate bisimulation for probabilistic systems, (Proceedings of EXPRESS/SOS 2013. Proceedings of EXPRESS/SOS 2013, EPTCS, vol. 120 (2013)), 32-46 · Zbl 1464.68245
[42] Gebler, Daniel; Tini, Simone, Fixed-point characterization of compositionality properties of probabilistic processes combinators, (Proceedings of EXPRESS/SOS 2014 (2014)), 63-78 · Zbl 1464.68246
[43] Gebler, Daniel; Tini, Simone, SOS specifications of probabilistic systems by uniformly continuous operators, (Proceedings of CONCUR 2015. Proceedings of CONCUR 2015, LIPIcs, vol. 42 (2015)), 155-168 · Zbl 1374.68328
[44] Gebler, Daniel; Tini, Simone, SOS specifications for uniformly continuous operators, J. Comput. Syst. Sci., 92, 113-151 (2018) · Zbl 1380.68296
[45] van Glabbeek, Rob J., The linear time – branching time spectrum II, (Proceedings of CONCUR ’93 (1993)), 66-81
[46] van Glabbeek, Rob J., The meaning of negative premises in transition system specifications II, (Proceedings of ICALP’96 (1996)), 502-513 · Zbl 1046.68629
[47] van Glabbeek, Rob J., On cool congruence formats for weak bisimulations, Theor. Comput. Sci., 412, 28, 3283-3302 (2011) · Zbl 1216.68199
[48] van Glabbeek, Rob J.; Smolka, Scott A.; Steffen, Bernhard, Reactive, generative and stratified models of probabilistic processes, Inf. Comput., 121, 1, 59-80 (1995) · Zbl 0832.68042
[49] Groote, Jan Friso, Transition system specifications with negative premises, Theor. Comput. Sci., 118, 2, 263-299 (1993) · Zbl 0778.68057
[50] Gutiérrez-Reina, Daniel; Marín, Sergio L. Toral; Johnson, Princy; Barrero, Federico, A survey on probabilistic broadcast schemes for wireless ad hoc networks, Ad Hoc Netw., 25, 263-292 (2015)
[51] Hamadou, Sardaouna; Palamidessi, Catuscia; Sassone, Vladimiro, Quantifying leakage in the presence of unreliable sources of information, J. Comput. Syst. Sci., 88, 27-52 (2017) · Zbl 1371.68073
[52] Hansson, Hans; Jonsson, Bengt, A logic for reasoning about time and reliability, Form. Asp. Comput., 6, 5, 512-535 (1994) · Zbl 0820.68113
[53] Hennessy, Matthew; Milner, Robin, Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 137-161 (1985) · Zbl 0629.68021
[54] Jonsson, Bengt; Yi, Wang; Larsen, Kim G., Probabilistic extensions of process algebras, (Handbook of Process Algebra (2001), North-Holland/Elsevier), 685-710 · Zbl 1062.68081
[55] Keller, Robert M., Formal verification of parallel programs, Commun. ACM, 19, 7, 371-384 (1976) · Zbl 0329.68016
[56] Lanotte, Ruggero; Merro, Massimo; Tini, Simone, Compositional weak metrics for group key update, (Proceedings of MFCS 2017. Proceedings of MFCS 2017, LIPIcs, vol. 83 (2017)), 72:1-72:16 · Zbl 1441.68146
[57] Lanotte, Ruggero; Tini, Simone, Probabilistic bisimulation as a congruence, ACM Trans. Comput. Log., 10, 1-48 (2009) · Zbl 1351.68183
[58] Larsen, Kim G., Context-Dependent Bisimulation Between Processes (1986), University of Edinburgh, Ph.D. thesis
[59] Larsen, Kim G.; Skou, Arne, Bisimulation through probabilistic testing, Inf. Comput., 94, 1, 1-28 (1991) · Zbl 0756.68035
[60] Larsen, Kim G.; Xinxin, Liu, Compositionality through an operational semantics of contexts, J. Log. Comput., 1, 6, 761-795 (1991) · Zbl 0738.68056
[61] Lee, Matias D.; de Vink, Erik P., Rooted branching bisimulation as a congruence for probabilistic transition systems, (Proceedings of QAPL 2015. Proceedings of QAPL 2015, EPTCS, vol. 194 (2015)), 79-94
[62] Lee, Matias D.; de Vink, Erik P., Logical characterization of bisimulation for transition relations over probability distributions with internal actions, (Proceedings of MFCS 2016. Proceedings of MFCS 2016, LIPIcs, vol. 58 (2016)), 29:1-29:14 · Zbl 1398.68368
[63] Lynch, Nancy A.; Segala, Roberto; Vaandrager, Frits W., Observing branching structure through probabilistic contexts, SIAM J. Comput., 37, 4, 977-1013 (2007) · Zbl 1156.68020
[64] Mio, Matteo; Simpson, Alex, A proof system for compositional verification of probabilistic concurrent processes, (Proceedings of FoSSsCS 2013. Proceedings of FoSSsCS 2013, LNCS, vol. 7794 (2013)), 161-176 · Zbl 1260.68273
[65] Mousavi, Mohammad Reza; Reniers, Michel A.; Groote, Jan Friso, SOS formats and meta-theory: 20 years after, Theor. Comput. Sci., 373, 3, 238-272 (2007) · Zbl 1111.68069
[66] Parma, Augusto; Segala, Roberto, Logical characterizations of bisimulations for discrete probabilistic systems, (Proceedings of FoSSaCS 2007. Proceedings of FoSSaCS 2007, LNCS, vol. 4423 (2007)), 287-301 · Zbl 1195.68072
[67] Philippou, Anna; Lee, Insup; Sokolsky, Oleg, Weak bisimulation for probabilistic systems, (Proceedings of CONCUR 2000. Proceedings of CONCUR 2000, LNCS, vol. 1877 (2000)), 334-349 · Zbl 0999.68146
[68] Plotkin, Gordon D., An operational semantics for CSO, (Proceedings of Logics of Programs and Their Applications (1980)), 250-252 · Zbl 0506.68025
[69] Segala, Roberto, Modeling and Verification of Randomized Distributed Real-Time Systems (1995), MIT, Ph.D. thesis · Zbl 1374.68296
[70] de Simone, Robert, Higher-level synchronising devices in MEIJE-SCCS, Theor. Comput. Sci., 37, 245-267 (1985) · Zbl 0598.68027
[71] van Breugel, Frank; Worrell, James, An algorithm for quantitative verification of probabilistic transition systems, (Proceedings of CONCUR 2001. Proceedings of CONCUR 2001, LNCS, vol. 2154 (2001)), 336-350 · Zbl 1006.68079
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.