{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:31:40Z","timestamp":1682094700917},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4-6","license":[{"start":{"date-parts":[[2012,7,1]],"date-time":"2012-07-01T00:00:00Z","timestamp":1341100800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"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>\n            We consider two characterisations of the may and must testing preorders for a probabilistic extension of the finite\n            <jats:italic>\u03c0<\/jats:italic>\n            -calculus: one based on notions of probabilistic weak simulations, and the other on a probabilistic extension of a fragment of Milner\u2013Parrow\u2013Walker modal logic for the\n            <jats:italic>\u03c0<\/jats:italic>\n            -calculus. We base our notions of simulations on similar concepts used in previous work for probabilistic CSP. However, unlike the case with CSP (or other non-value-passing calculi), there are several possible definitions of simulation for the probabilistic\n            <jats:italic>\u03c0<\/jats:italic>\n            -calculus, which arise from different ways of scoping the name quantification. We show that in order to capture the testing preorders, one needs to use the \u201cearliest\u201d simulation relation (in analogy to the notion of early (bi)simulation in the non-probabilistic case). The key ideas in both characterisations are the notion of a \u201ccharacteristic formula\u201d of a probabilistic process, and the notion of a \u201ccharacteristic test\u201d for a formula. As in an earlier work on testing equivalence for the\n            <jats:italic>\u03c0<\/jats:italic>\n            -calculus by Boreale and De Nicola, we extend the language of the\n            <jats:italic>\u03c0<\/jats:italic>\n            -calculus with a mismatch operator, without which the formulation of a characteristic test will not be possible.\n          <\/jats:p>","DOI":"10.1007\/s00165-012-0238-3","type":"journal-article","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T08:35:50Z","timestamp":1340872550000},"page":"701-726","source":"Crossref","is-referenced-by-count":2,"title":["Characterisations of testing preorders for a finite probabilistic\n            <i>\u03c0<\/i>\n            -calculus"],"prefix":"10.1145","volume":"24","author":[{"given":"Yuxin","family":"Deng","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai, China"},{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[{"name":"Research School of Computer Science, The Australian National University, Canberra, Australia"}]}],"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-time and may-testing in a probabilistic reactive setting. In: Proceedings of the conference on FMOODS\/FORTE. LNCS vol 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":"publisher","DOI":"10.1006\/inco.1995.1114"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.006"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/1314690.1314693"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.013"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:4)2008"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Deng Y van Glabbeek RJ Hennessy M Morgan C (2009) Testing finitary probabilistic processes. In: Proceedings of the conference on CONCUR. LNCS vol 5710. Springer Berlin pp 274\u2013288","DOI":"10.1007\/978-3-642-04081-8_19"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Deng Y van Glabbeek RJ Morgan C Zhang C (2007) Scalar outcomes suffice for finitary probabilistic testing. In: Proceedings of the conference on ESOP. LNCS vol 4421. Springer Berlin pp 363\u2013378","DOI":"10.1007\/978-3-540-71316-6_25"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Ferrari GL Montanari U Quaglia P (1995) The weak late pi-calculus semantics as observation equivalence. In: Proceeding of the conference on CONCUR. LNCS vol 962. Springer Berlin pp 57\u201371","DOI":"10.1007\/3-540-60218-6_5"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Hennessy M (1982) Power domains and nondeterministic recursive definitions. In: Proceedings of the conference symposium on programming. LNCS vol 137. Springer Berlin pp 178\u2013193","DOI":"10.1007\/3-540-11494-7_13"},{"key":"e_1_2_1_2_12_2","volume-title":"Algebraic Theory of Processes","author":"Hennessy M","year":"1988"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Hansson H Jonsson B (1990) A calculus for communicating systems with time and probabilities. In: Proceedings of the conference on IEEE real time systems symposium pp 278\u2013287","DOI":"10.1109\/REAL.1990.128759"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Herescu OM Palamidessi C (2000) Probabilistic asynchronous pi-calculus. In: Proceedings of the conference on FoSSaCS. LNCS vol 1784 Springer Berlin pp 146\u2013160","DOI":"10.1007\/3-540-46432-8_10"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00304-2"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90009-5"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90156-N"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.77"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Parma A Segala R (2007) Logical characterizations of bisimulations for discrete probabilistic systems. In: Proceedings of the conference on FOSSACS. LNCS vol 4423. Springer Berlin pp 287\u2013301","DOI":"10.1007\/978-3-540-71389-0_21"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0096"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Segala R (1996) Testing probabilistic automata. In: Proceedings of the conference on CONCUR. LNCS vol 1119. Springer Berlin pp 299\u2013314","DOI":"10.1007\/3-540-61604-7_62"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Segala R Lynch NA (1994) Probabilistic simulations for probabilistic processes. In: Proceedings of the conference on CONCUR LNCS vol 836. Springer Berlin pp 481\u2013496","DOI":"10.1007\/978-3-540-48654-1_35"},{"key":"e_1_2_1_2_25_2","volume-title":"\u03c0-calculus: a theory of mobile processes","author":"Sangiorgi D","year":"2001"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1123"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/233551.233556"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Wang Y Larsen KG (1992) Testing probabilistic and nondeterministic processes. In: Proceedings of the conference on PSTV. IFIP transactions vol C-8. North-Holland Amsterdam pp 47\u201361","DOI":"10.1016\/B978-0-444-89874-6.50010-6"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0238-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0238-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0238-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:59:55Z","timestamp":1641484795000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0238-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":28,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["10.1007\/s00165-012-0238-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0238-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7]]}}}