{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:31:22Z","timestamp":1774837882960,"version":"3.50.1"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"4-6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2012,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper considers the probabilistic may\/must testing theory for processes having external, internal, and probabilistic choices. We observe that the underlying testing equivalence is too strong and distinguishes between processes that are observationally equivalent. The problem arises from the observation that the classical compose-and-schedule approach yields unrealistic overestimation of the probabilities, a phenomenon that has been recently well studied from the point of view of compositionality, in the context of randomized protocols and in probabilistic model checking. To that end, we propose a new testing theory, aiming at preserving the probability information in a parallel context. The resulting testing equivalence is insensitive to the exact moment the internal and the probabilistic choices occur. We also give an alternative characterization of the testing preorder as a probabilistic ready-trace preorder.<\/jats:p>","DOI":"10.1007\/s00165-012-0236-5","type":"journal-article","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T08:35:50Z","timestamp":1340872550000},"page":"727-748","source":"Crossref","is-referenced-by-count":12,"title":["Probabilistic may\/must testing: retaining probabilities by restricted schedulers"],"prefix":"10.1145","volume":"24","author":[{"given":"Sonja","family":"Georgievska","sequence":"first","affiliation":[{"name":"Department of Mathematics and Computer Science, Eindhoven University of Technology, PO Box 513, 5600\u00a0MB, Eindhoven, The Netherlands"}]},{"given":"Suzana","family":"Andova","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, Eindhoven University of Technology, PO Box 513, 5600\u00a0MB, Eindhoven, The Netherlands"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Acciai L Boreale M De Nicola R (2011) Linear and may-testing semantics in a probabilistic reactive setting. FMOODS-FORTE\u201911 LNCS 6722. Springer Berlin pp 29\u201343","DOI":"10.1007\/978-3-642-21461-5_2"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Alvim MS Andr\u00e9s ME Palamidessi C van Rossum P (2010) Safe equivalences for security properties. IFIP TCS\u201910 pp 55\u201370","DOI":"10.1007\/978-3-642-15240-5_5"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.02.045"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/30.6.498"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Baeten JCM Basten T Reniers MA (2010) Process algebra: equational theories of communicating processes. Cambridge University Press","DOI":"10.1017\/CBO9781139195003"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bianco A de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. FSTTCS \u201995 LNCS 1026. Springer Berlin pp 499\u2013513","DOI":"10.1007\/3-540-60692-0_70"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Calin G Crouzen P D\u2019Argenio PR Hahn EM Zhang L (2010) Time-bounded reachability in distributed input\/output interactive probabilistic chains. SPIN\u201910 LNCS 6349. Springer Berlin pp 193\u2013211","DOI":"10.1007\/978-3-642-16164-3_15"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Canetti R (2001) Universally composable security: a new paradigm for cryptographic protocols. FOCS\u201901. IEEE pp 136\u2013145","DOI":"10.1109\/SFCS.2001.959888"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00040-1"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Chatzikokolakis K Palamidessi C (2007) Making random choices invisible to the scheduler. CONCUR\u201907 LNCS 4703. Springer Berlin pp 42\u201358","DOI":"10.1007\/978-3-540-74407-8_4"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.033"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1314690.1314693"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"de Alfaro L Henzinger T Jhala R (2001) Compositional methods for probabilistic systems. In: CONCUR\u201901 LNCS 2154. Springer Berlin pp 351\u2013365","DOI":"10.1007\/3-540-44685-0_24"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Deng Y van Glabbeek R Hennessy M Morgan C (2009) Testing finitary probabilistic processes (extended abstract). In: CONCUR\u201909. LNCS 5710. Springer Berlin pp 274\u2013288","DOI":"10.1007\/978-3-642-04081-8_19"},{"issue":"4","key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","first-page":"4","DOI":"10.2168\/LMCS-4(4:4)2008","article-title":"Characterising testing preorders for finite probabilistic processes","volume":"4","author":"Deng Y","year":"2008","journal-title":"Logical Methods Comput Sci"},{"key":"e_1_2_1_2_18_2","volume-title":"Stochastic processes","author":"Doob JL","year":"1953"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054108005814"},{"key":"e_1_2_1_2_20_2","unstructured":"Georgievska S (2011) Probability and hiding in concurrent processes. PhD thesis Eindhoven University of Technology"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Georgievska S Andova S (2010) Composing systems while preserving probabilities. EPEW 2010 LNCS 6342. Springer Berlin pp 268\u2013283","DOI":"10.1007\/978-3-642-15784-4_18"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Georgievska S Andova S (2010) Retaining the probabilities in probabilistic testing theory. FOSSACS\u201910 LNCS 6014. Springer Berlin pp 79\u201393","DOI":"10.1007\/978-3-642-12032-9_7"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Georgievska S Andova S (2010) Testing reactive probabilistic processes. QAPL\u201910 EPTCS 28 pp 99\u2013113","DOI":"10.4204\/EPTCS.28.7"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Georgievska S Andova S (2012) Probabilistic CSP: preserving the laws via restricted schedulers. MMB & DFT 2012 LNCS 7201. Springer Berlin pp 136\u2013150","DOI":"10.1007\/978-3-642-28540-0_10"},{"key":"e_1_2_1_2_25_2","unstructured":"Giro S (2010) On the automatic verification of distributed probabilistic automata with partial information. PhD thesis Universidad Nacional de C\u00f3rdoba"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Giro S D\u2019Argenio P (2009) On the expressive power of schedulers in distributed probabilistic systems. QAPL\u201909 ENTCS 253(3). Elsevier Amsterdam pp pp 45\u201371","DOI":"10.1016\/j.entcs.2009.10.005"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"van Glabbeek RJ (1993) The linear time-branching time spectrum II. CONCUR\u201993 LNCS 715. Springer Berlin pp 66\u201381","DOI":"10.1007\/3-540-57208-2_6"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"van Glabbeek RJ (2001) The linear time-branching time spectrum I; the semantics of concrete sequential processes. Handbook of process algebra chap 1. Elsevier Amsterdam pp 3\u201399","DOI":"10.1016\/B978-044482830-9\/50019-9"},{"key":"e_1_2_1_2_29_2","first-page":"371","article-title":"Branching bisimilarity with explicit divergence","volume":"93","author":"van Glabbeek RJ","year":"2009","journal-title":"Fundam Inf"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Gomez FC De Frutos Escrig D. Ruiz VV (1997) A sound and complete proof system for probabilistic processes. ARTS\u201997 LNCS 1231. Springer Berlin pp 340\u2013352","DOI":"10.1007\/3-540-63010-4_23"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/561335"},{"key":"e_1_2_1_2_32_2","volume-title":"Algebraic theory of processes","author":"Hennessy M","year":"1988"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_34_2","volume-title":"Semi-Markov and decision processes","author":"Howard RA","year":"1971"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00044-5"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(98)00023-X"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Kumar KN Cleaveland R Smolka SA (1998) Infinite probabilistic and nonprobabilistic testing. FSTTCS\u201998 LNCS 1530. Springer Berlin pp 209\u2013220","DOI":"10.1007\/978-3-540-49382-2_19"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G (1998) A testing equivalence for reactive probabilistic processes. EXPRESS\u201998 ENTCS 16. Elsevier Amsterdam pp 1\u201319","DOI":"10.1016\/S1571-0661(04)00121-5"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska MZ Norman GJ (1998) A fully abstract metric-space denotational semantics for reactive probabilistic processes. COMPROX \u201998 ENTCS 13. Elsevier Amsterdam pp 1\u201333","DOI":"10.1016\/S1571-0661(05)80222-1"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_2_41_2","volume-title":"Introduction to probability and statistics from a Bayesian viewpoint","author":"Lindley DV","year":"1980"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.10.047"},{"key":"e_1_2_1_2_43_2","unstructured":"Lowe G (1993) Representing nondeterministic and probabilistic behaviour in reactive processes. Technical Report PRG-TR-11-93. Oxford University Computing Labs"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539704446487"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/1036296"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01213492"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264365"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Palmeri MC De Nicola R Massink M (2007) Basic observables for probabilistic may testing. QEST \u201907. IEEE Computer Society pp 189\u2013200","DOI":"10.1109\/QEST.2007.19"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1985) Linear and branching structures in the semantics and logics of reactive systems. ICALP\u201985 LNCS 194. Springer Berlin pp 15\u201332","DOI":"10.1007\/BFb0015727"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.5555\/528623"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.06.002"},{"key":"e_1_2_1_2_54_2","volume-title":"The theory and practice of concurrency","author":"Roscoe AW","year":"1998"},{"key":"e_1_2_1_2_55_2","unstructured":"Segala R (1995) Modeling and verification of randomized distributed real-time systems. PhD thesis MIT"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Segala R (1996) Testing probabilistic automata. CONCUR\u201996 LNCS 1119. Springer Berlin pp 299\u2013314","DOI":"10.1007\/3-540-61604-7_62"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00286-0"},{"key":"e_1_2_1_2_58_2","unstructured":"Seidel K Morgan C McIver A (1997) Probabilistic imperative programming: a rigorous approach. Proceedings of formal methods Pacific \u201997. Springer Series in Discrete Mathematics and Theoretical Computer Science Singapore Springer Berlin"},{"key":"e_1_2_1_2_59_2","unstructured":"Sondik EJ (1971) The optimal control of partially observable Markov processes. PhD thesis Stanford University"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Wang Y Larsen KG (1992) Testing probabilistic and nondeterministic processes. Proceedings of IFIP TC6\/WG6.1 twelth international symposium on protocol specification testing and verification XII pp 47\u201361","DOI":"10.1016\/B978-0-444-89874-6.50010-6"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00056-X"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0236-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:59:49Z","timestamp":1641484789000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0236-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":61,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["10.1007\/s00165-012-0236-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0236-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7]]}}}