Relating strong behavioral equivalences for processes with nondeterminism and probabilities. (English) Zbl 1360.68626
Summary: We present a comparison of behavioral equivalences for nondeterministic and probabilistic processes whose activities are all observable. In particular, we consider trace-based, testing, and bisimulation-based equivalences. For each of them, we examine the discriminating power of three variants stemming from three approaches that differ for the way probabilities of events are compared when nondeterministic choices are resolved via schedulers. The first approach compares two resolutions with respect to the probability distributions of all considered events. The second approach requires that the probabilities of the set of events of a resolution be individually matched by the probabilities of the same events in possibly different resolutions. The third approach only compares the extremal probabilities of each event stemming from the different resolutions. The three approaches have very reasonable motivations and, when applied to fully nondeterministic processes or fully probabilistic processes, give rise to the classical well studied relations. We shall see that, for processes with nondeterminism and probability, they instead give rise to a much wider variety of behavioral relations, whose discriminating power is thoroughly investigated here in the case of deterministic schedulers.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Keywords:
bisimulation equivalence; testing equivalence; failure equivalence; trace equivalence; nondeterminism; probabilityReferences:
| [1] | Abramsky, S., Observational equivalence as a testing equivalence, Theoret. Comput. Sci., 53, 225-241 (1987) · Zbl 0626.68016 |
| [2] | Baier, C.; Katoen, J.-P.; Hermanns, H.; Wolf, V., Comparative branching-time semantics for Markov chains, Inform. and Comput., 200, 149-214 (2005) · Zbl 1101.68053 |
| [3] | (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier) · Zbl 0971.00006 |
| [4] | Bernardo, M.; De Nicola, R.; Loreti, M., Revisiting trace and testing equivalences for nondeterministic and probabilistic processes, (Proc. of the 15th Int. Conf. on Foundations of Software Science and Computation Structures. Proc. of the 15th Int. Conf. on Foundations of Software Science and Computation Structures, FOSSACS 2012. Proc. of the 15th Int. Conf. on Foundations of Software Science and Computation Structures. Proc. of the 15th Int. Conf. on Foundations of Software Science and Computation Structures, FOSSACS 2012, Lecture Notes in Comput. Sci., vol. 7213 (2012), Springer), 195-209, Full version: Technical report 04/2013, IMT Institute for Advanced Studies Lucca, available on-line at · Zbl 1326.68197 |
| [5] | Bernardo, M.; De Nicola, R.; Loreti, M., A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences, Inform. and Comput., 225, 29-82 (2013) · Zbl 1358.68210 |
| [6] | Bernardo, M.; De Nicola, R.; Loreti, M., The spectrum of strong behavioral equivalences for nondeterministic and probabilistic processes, (Proc. of the 11th Int. Workshop on Quantitative Aspects of Programming Languages and Systems. Proc. of the 11th Int. Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013. Proc. of the 11th Int. Workshop on Quantitative Aspects of Programming Languages and Systems. Proc. of the 11th Int. Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013, Electr. Proc. Theoret. Comput. Sci., vol. 117 (2013)), 81-96 · Zbl 1464.68231 |
| [7] | Bernardo, M.; De Nicola, R.; Loreti, M., A companion of “Relating strong behavioral equivalences for processes with nondeterminism and probabilities”, CoRR, abs/1305.0538 (2013), available on-line at |
| [8] | Bernardo, M.; De Nicola, R.; Loreti, M., Group-by-group probabilistic bisimilarities and their logical characterizations, (Proc. of the 8th Int. Symp. on Trustworthy Global Computing. Proc. of the 8th Int. Symp. on Trustworthy Global Computing, TGC 2013. Proc. of the 8th Int. Symp. on Trustworthy Global Computing. Proc. of the 8th Int. Symp. on Trustworthy Global Computing, TGC 2013, Lecture Notes in Comput. Sci., vol. 8358 (2013), Springer), Full version: Technical Report 06/2013, IMT Institute for Advanced Studies Lucca, available on-line at · Zbl 1348.68156 |
| [9] | Brookes, S. D.; Hoare, C. A.R.; Roscoe, A. W., A theory of communicating sequential processes, J. ACM, 31, 560-599 (1984) · Zbl 0628.68025 |
| [10] | Cleaveland, R.; Dayar, Z.; Smolka, S. A.; Yuen, S., Testing preorders for probabilistic processes, Inform. and Comput., 154, 93-148 (1999) · Zbl 1045.68564 |
| [11] | Crafa, S.; Ranzato, F., A spectrum of behavioral relations over LTSs on probability distributions, (Proc. of the 22nd Int. Conf. on Concurrency Theory. Proc. of the 22nd Int. Conf. on Concurrency Theory, CONCUR 2011. Proc. of the 22nd Int. Conf. on Concurrency Theory. Proc. of the 22nd Int. Conf. on Concurrency Theory, CONCUR 2011, Lecture Notes in Comput. Sci., vol. 6901 (2011), Springer), 124-139 · Zbl 1344.68162 |
| [12] | de Alfaro, L.; Majumdar, R.; Raman, V.; Stoelinga, M., Game refinement relations and metrics, Log. Methods Comput. Sci., 3, 7 (2008) · Zbl 1147.68056 |
| [13] | De Nicola, R., Extensional equivalences for transition systems, Acta Inform., 24, 211-237 (1987) · Zbl 0636.68069 |
| [14] | De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theoret. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518 |
| [15] | Deng, Y.; van Glabbeek, R. J.; Hennessy, M.; Morgan, C., Characterising testing preorders for finite probabilistic processes, Log. Methods Comput. Sci., 4, 4, 1-33 (2008) · Zbl 1161.68035 |
| [16] | Derman, C., Finite State Markovian Decision Processes (1970), Academic Press · Zbl 0262.90001 |
| [17] | Desharnais, J.; Gupta, V.; Jagadeesan, R.; Panangaden, P., Approximating labelled Markov processes, Inform. and Comput., 184, 160-200 (2003) · Zbl 1028.68091 |
| [18] | Georgievska, S.; Andova, S., Retaining the probabilities in probabilistic testing theory, (Proc. of the 13th Int. Conf. on Foundations of Software Science and Computation Structures. Proc. of the 13th Int. Conf. on Foundations of Software Science and Computation Structures, FOSSACS 2010. Proc. of the 13th Int. Conf. on Foundations of Software Science and Computation Structures. Proc. of the 13th Int. Conf. on Foundations of Software Science and Computation Structures, FOSSACS 2010, Lecture Notes in Comput. Sci., vol. 6014 (2010), Springer), 79-93 · Zbl 1284.68397 |
| [19] | Giacalone, A.; Jou, C.-C.; Smolka, S. A., Algebraic reasoning for probabilistic concurrent systems, (Proc. of the 1st IFIP Working Conf. on Programming Concepts and Methods. Proc. of the 1st IFIP Working Conf. on Programming Concepts and Methods, PROCOMET 1990 (1990), North-Holland), 443-458 |
| [20] | Hansson, H.; Jonsson, B., A calculus for communicating systems with time and probabilities, (Proc. of the 11th IEEE Real-Time Systems Symp.. Proc. of the 11th IEEE Real-Time Systems Symp., RTSS 1990 (1990), IEEE-CS Press), 278-287 |
| [21] | Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 137-162 (1985) · Zbl 0629.68021 |
| [22] | Huynh, D. T.; Tian, L., On some equivalence relations for probabilistic processes, Fund. Inform., 17, 211-234 (1992) · Zbl 0766.68099 |
| [23] | Jifeng, H.; Seidel, K.; McIver, A., Probabilistic models for the guarded command language, Sci. Comput. Programming, 28, 171-192 (1997) · Zbl 0877.68014 |
| [24] | Jonsson, B.; Larsen, K. G., Specification and refinement of probabilistic processes, (Proc. of the 6th IEEE Symp. on Logic in Computer Science. Proc. of the 6th IEEE Symp. on Logic in Computer Science, LICS 1991 (1991), IEEE-CS Press), 266-277 |
| [25] | Jonsson, B.; Yi, W., Compositional testing preorders for probabilistic processes, (Proc. of the 10th IEEE Symp. on Logic in Computer Science. Proc. of the 10th IEEE Symp. on Logic in Computer Science, LICS 1995 (1995), IEEE-CS Press), 431-441 |
| [26] | Jou, C.-C.; Smolka, S. A., Equivalences, congruences, and complete axiomatizations for probabilistic processes, (Proc. of the 1st Int. Conf. on Concurrency Theory. Proc. of the 1st Int. Conf. on Concurrency Theory, CONCUR 1990. Proc. of the 1st Int. Conf. on Concurrency Theory. Proc. of the 1st Int. Conf. on Concurrency Theory, CONCUR 1990, Lecture Notes in Comput. Sci., vol. 458 (1990), Springer), 367-383 |
| [27] | Keller, R. M., Formal verification of parallel programs, Commun. ACM, 19, 371-384 (1976) · Zbl 0329.68016 |
| [28] | Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Inform. and Comput., 94, 1-28 (1991) · Zbl 0756.68035 |
| [29] | Lopez, N.; Nuñez, M., An overview of probabilistic process algebras and their equivalences, (Validation of Stochastic Systems. Validation of Stochastic Systems, Lecture Notes in Comput. Sci., vol. 2925 (2004), Springer), 89-123 · Zbl 1203.68115 |
| [30] | Philippou, A.; Lee, I.; Sokolsky, O., Weak bisimulation for probabilistic systems, (Proc. of the 11th Int. Conf. on Concurrency Theory. Proc. of the 11th Int. Conf. on Concurrency Theory, CONCUR 2000. Proc. of the 11th Int. Conf. on Concurrency Theory. Proc. of the 11th Int. Conf. on Concurrency Theory, CONCUR 2000, Lecture Notes in Comput. Sci., vol. 1877 (2000), Springer), 334-349 · Zbl 0999.68146 |
| [31] | Segala, R., Modeling and verification of randomized distributed real-time systems (1995), Ph.D. thesis |
| [32] | Segala, R., A compositional trace-based semantics for probabilistic automata, (Proc. of the 6th Int. Conf. on Concurrency Theory. Proc. of the 6th Int. Conf. on Concurrency Theory, CONCUR 1995. Proc. of the 6th Int. Conf. on Concurrency Theory. Proc. of the 6th Int. Conf. on Concurrency Theory, CONCUR 1995, Lecture Notes in Comput. Sci., vol. 962 (1995), Springer), 234-248 |
| [33] | Segala, R., Testing probabilistic automata, (Proc. of the 7th Int. Conf. on Concurrency Theory. Proc. of the 7th Int. Conf. on Concurrency Theory, CONCUR 1996. Proc. of the 7th Int. Conf. on Concurrency Theory. Proc. of the 7th Int. Conf. on Concurrency Theory, CONCUR 1996, Lecture Notes in Comput. Sci., vol. 1119 (1996), Springer), 299-314 · Zbl 1514.68112 |
| [34] | Segala, R.; Lynch, N. A., Probabilistic simulations for probabilistic processes, (Proc. of the 5th Int. Conf. on Concurrency Theory. Proc. of the 5th Int. Conf. on Concurrency Theory, CONCUR 1994. Proc. of the 5th Int. Conf. on Concurrency Theory. Proc. of the 5th Int. Conf. on Concurrency Theory, CONCUR 1994, Lecture Notes in Comput. Sci., vol. 836 (1994), Springer), 481-496 |
| [35] | Segala, R.; Turrini, A., Comparative analysis of bisimulation relations on alternating and non-alternating probabilistic models, (Proc. of the 2nd Int. Conf. on the Quantitative Evaluation of Systems. Proc. of the 2nd Int. Conf. on the Quantitative Evaluation of Systems, QEST 2005 (2005), IEEE-CS Press), 44-53 |
| [36] | Sokolova, A.; de Vink, E. P., Probabilistic automata: System types, parallel composition and comparison, (Validation of Stochastic Systems. Validation of Stochastic Systems, Lecture Notes in Comput. Sci., vol. 2925 (2004), Springer), 1-43 · Zbl 1203.68089 |
| [37] | Song, L.; Zhang, L.; Godskesen, J. C., Bisimulations meet PCTL equivalences for probabilistic automata, (Proc. of the 22nd Int. Conf. on Concurrency Theory. Proc. of the 22nd Int. Conf. on Concurrency Theory, CONCUR 2011. Proc. of the 22nd Int. Conf. on Concurrency Theory. Proc. of the 22nd Int. Conf. on Concurrency Theory, CONCUR 2011, Lecture Notes in Comput. Sci., vol. 6901 (2011), Springer), 108-123 · Zbl 1344.68170 |
| [38] | Tracol, M.; Desharnais, J.; Zhioua, A., Computing distances between probabilistic automata, (Proc. of the 9th Int. Workshop on Quantitative Aspects of Programming Languages. Proc. of the 9th Int. Workshop on Quantitative Aspects of Programming Languages, QAPL 2011. Proc. of the 9th Int. Workshop on Quantitative Aspects of Programming Languages. Proc. of the 9th Int. Workshop on Quantitative Aspects of Programming Languages, QAPL 2011, Electr. Proc. Theoret. Comput. Sci., vol. 57 (2011)), 148-162 · Zbl 1457.68151 |
| [39] | van Glabbeek, R. J., The linear time - branching time spectrum I, (Handbook of Process Algebra (2001), Elsevier), 3-99 · Zbl 1035.68073 |
| [40] | Varacca, D., Probability, nondeterminism and concurrency. Two denotational models for probabilistic computation (2003), Ph.D. thesis |
| [41] | Varacca, D.; Winskel, G., Distributing probability over non-determinism, Math. Structures Comput. Sci., 16, 87-113 (2006) · Zbl 1093.18002 |
| [42] | Vardi, M. Y., Automatic verification of probabilistic concurrent finite-state programs, (Proc. of the 26th IEEE Symp. on Foundations of Computer Science. Proc. of the 26th IEEE Symp. on Foundations of Computer Science, FOCS 1985 (1985), IEEE-CS Press), 327-338 |
| [43] | Wolf, V., Testing theory for probabilistic systems, (Model-Based Testing of Reactive Systems. Model-Based Testing of Reactive Systems, Lecture Notes in Comput. Sci., vol. 3472 (2005), Springer), 233-275 |
| [44] | Yi, W.; Larsen, K. G., Testing probabilistic and nondeterministic processes, (Proc. of the 12th Int. Symp. on Protocol Specification, Testing and Verification. Proc. of the 12th Int. Symp. on Protocol Specification, Testing and Verification, PSTV 1992 (1992), North-Holland), 47-61 |
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.
