{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,26]],"date-time":"2025-07-26T08:44:44Z","timestamp":1753519484094},"reference-count":45,"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>We conservatively extend an ACP-style discrete-time process theory with discrete stochastic delays. The semantics of the timed delays relies on time additivity and time determinism, which are properties that enable us to merge subsequent timed delays and to impose their synchronous expiration. Stochastic delays, however, interact with respect to a so-called race condition that determines the set of delays that expire first, which is guided by an (implicit) probabilistic choice. The race condition precludes the property of time additivity as the merger of stochastic delays alters this probabilistic behavior. To this end, we resolve the race condition using conditionally-distributed unit delays. We give a sound and ground-complete axiomatization of the process theory comprising the standard set of ACP-style operators. In this generalized setting, the alternative composition is no longer associative, so we have to resort to special normal forms that explicitly resolve the underlying race condition. Our treatment succeeds in the initial challenge to conservatively extend standard time with stochastic time. However, the \u2018dissection\u2019 of the stochastic delays to conditionally-distributed unit delays comes at a price, as we can no longer relate the resolved race condition to the original stochastic delays. We seek a solution in the field of probabilistic refinements that enable the interchange of probabilistic and nondeterministic choices.<\/jats:p>","DOI":"10.1007\/s00165-012-0230-y","type":"journal-article","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T08:35:50Z","timestamp":1340872550000},"page":"497-518","source":"Crossref","is-referenced-by-count":6,"title":["Reconciling real and stochastic time: the need for probabilistic refinement"],"prefix":"10.1145","volume":"24","author":[{"given":"J.","family":"Markovski","sequence":"first","affiliation":[{"name":"Eindhoven University of Technology, Eindhoven, The Netherlands"}]},{"given":"P. R.","family":"D\u2019Argenio","sequence":"additional","affiliation":[{"name":"FaMAF, Universidad Nacional de C\u00f3rdoba, C\u00f3rdoba, Argentina"}]},{"given":"J. C. M.","family":"Baeten","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology, Eindhoven, The Netherlands"},{"name":"Centrum Wiskunde &amp; Informatica, Amsterdam, The Netherlands"}]},{"given":"E. P.","family":"de Vink","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology, Eindhoven, The Netherlands"},{"name":"Centrum Wiskunde &amp; Informatica, Amsterdam, The Netherlands"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1109\/90.298433"},{"key":"e_1_2_1_2_2_2","volume-title":"Modelling with generalized stochastic Petri nets","author":"Ajmone Marsan M","year":"1995"},{"key":"e_1_2_1_2_3_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 FMOODS 2011. Lecture Notes in Computer Science vol 6722. Springer Berlin pp 29\u201343","DOI":"10.1007\/978-3-642-21461-5_2"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.036"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/937555.937558"},{"key":"e_1_2_1_2_6_2","unstructured":"Bravetti M Bernardo M Gorrieri R (1997) From EMPA to GSMPA: allowing for general distributions. In: Proceedings of PAPM\u201997 Enschede pp 17\u201333"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90052-1"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Baeten JCM Basten T Reniers MA (2010) Process algebra: equational theories of communicating processes. In: Cambridge tracts in theoretical computer science vol 50. Cambridge University Press Cambridge","DOI":"10.1017\/CBO9781139195003"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bravetti M D\u2019Argenio PR (2004) Tutte le algebre insieme: concepts discussions and relations of stochastic process algebras with general distributions. In: Validation of stochastic systems\u2014a guide to current research. Lecture Notes in Computer Science vol 2925. Springer Berlin pp 44\u201388","DOI":"10.1007\/978-3-540-24611-4_2"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.104"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00127-8"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/38.7.552"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04995-2","volume-title":"Process algebra with timing. In: Monographs in theoretical computer science","author":"Baeten JCM","year":"2002"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Baeten JCM Reniers MA (2004) Timed process algebra (with a focus on explicit termination and relative timing). In: Proceedings of SFM 2004. Lecture Notes of Computer Science vol 3185. Springer Berlin pp 59\u201397","DOI":"10.1007\/978-3-540-30080-9_3"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Bravetti M (2002) Specification and analysis of stochastic real-time systems. PhD thesis Universit\u00e0\n\u00e0 di Bologna","DOI":"10.1007\/3-540-45605-8_14"},{"key":"e_1_2_1_2_16_2","volume-title":"Process algebra. Cambridge tracts in theoretical computer science, vol 18","author":"Baeten JCM","year":"1990"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Cattani S Segala R Kwiatkowska M Norman G (2005) Stochastic transition systems for continuous state spaces and non-determinism. In: Proceedings of FoSSaCS\u201905. Lecture Notes of Computer Science vol 3441. Springer Berlin pp 125\u2013139","DOI":"10.1007\/978-3-540-31982-5_8"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Cheung L Stoelinga M Vaandrager F (2007) A testing scenario for probabilistic processes. J ACM 54","DOI":"10.1145\/1314690.1314693"},{"key":"e_1_2_1_2_19_2","unstructured":"D\u2019Argenio PR (2003) From stochastic automata to timed automata: abstracting probability in a compositional manner. In: Proceedings of WAIT 2003 Buenos Aires"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"de Alfaro L Henzinger T Jhala R (2001) Compositional methods for probabilistic systems. In: Proceedings of CONCUR 2001. Lecture Notes in Computer Science vol 2154. Springer Berlin pp 351\u2013365","DOI":"10.1007\/3-540-44685-0_24"},{"issue":"1","key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ic.2005.07.001","article-title":"A theory of stochastic systems, part I: stochastic automata","volume":"203","author":"D\u2019Argenio PR","year":"2005","journal-title":"Inform Comput"},{"issue":"1","key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.ic.2005.07.002","article-title":"A theory of stochastic systems, part II: process algebra","volume":"203","author":"D\u2019Argenio PR","year":"2005","journal-title":"Inform Comput"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Georgievska S Andova S (2010) Retaining the probabilities in probabilistic testing theory. In: Proceedings of FOSSACS 2010. Lecture Notes in Computer Science vol 6014. Springer Berlin pp 79\u201393","DOI":"10.1007\/978-3-642-12032-9_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. In: Proceedings of MMB 2012. VDE Verlag (to appear). Available from: http:\/\/www.win.tue.nl\/sgeorgie\/.","DOI":"10.1007\/978-3-642-28540-0_10"},{"key":"e_1_2_1_2_25_2","first-page":"45","article-title":"On the expressive power of schedulers in distributed probabilistic systems","volume":"253","author":"Giro S","year":"2009","journal-title":"EPTCS"},{"key":"e_1_2_1_2_26_2","unstructured":"Georgievska S (2011) Probability and hiding in concurrent processes. PhD thesis Eindhoven University of Technology"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.21067"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Hermanns H (2002) Interactive Markov chains: the quest for quantified quality. Lecture Notes in Computer Science vol 2428. Springer Berlin","DOI":"10.1007\/3-540-45804-2"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/236373"},{"key":"e_1_2_1_2_30_2","unstructured":"Hermanns H Mertsiotakis V Rettelbach M (1994) Performance analysis of distributed systems using TIPP. In: Proceedings of UKPEW\u201994. University of Edinburgh pp 131\u2013144"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_32_2","volume-title":"Dynamic probabilistic systems","author":"Howard RA","year":"1971"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Katoen JP D\u2019Argenio PR (2001) General distributions in process algebra. In: Lectures on formal methods and performance analysis. Lecture Notes in Computer Science vol 2090. Springer Berlin pp 375\u2013429","DOI":"10.1007\/3-540-44667-2_11"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2002) PRISM: probabilistic symbolic model checker. In: Proceedings of TOOLS 2002. Lecture Notes in Computer Science vol 2324. Springer Berlin pp 200\u2013204","DOI":"10.1007\/3-540-46029-2_13"},{"key":"e_1_2_1_2_35_2","unstructured":"L\u00f3pez N N\u00fa\u00f1ez M (2000) NMSPA: a non-Markovian model for stochastic processes. In: Proceedings of ICDS 2000. IEEE pp 33\u201340"},{"key":"e_1_2_1_2_36_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_37_2","unstructured":"Markovski J (2008) Real and stochastic time in processs algebras for performance evaluation. PhD thesis Eindhoven University of Technology"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01213492"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Markovski J de Vink EP (2006) Embedding real-time in stochastic process algebras. In: Proceedings of EPEW 2006. Lecture Notes of Computer Science vol 4054. Springer Berlin pp 47\u201362","DOI":"10.1007\/11777830_4"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Markovski J de Vink EP (2007) Real-time process algebra with stochastic delays. In: Proceedings of ACSD 2007. IEEE pp 177\u2013186","DOI":"10.1109\/ACSD.2007.23"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Markovski J de Vink EP (2008) Extending timed process algebra with discrete stochastic time. In: Proceedings of AMAST 2008. Lecture Notes of Computer Science vol 5140. Springer Berlin pp 268\u2013283","DOI":"10.1007\/978-3-540-79980-1_21"},{"issue":"1","key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","first-page":"157","DOI":"10.3233\/FI-2009-146","article-title":"Performance evaluation of distributed systems based on a discrete real- and stochastic-time process algebra","volume":"95","author":"Markovski J","year":"2009","journal-title":"Fundam Inform"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Nicollin X Sifakis J (1992) An overview and synthesis of timed process algebras. In: Real-time: theory in practice. Lecture Notes of Computer Science vol 600. Springer Berlin pp 526\u2013548","DOI":"10.1007\/BFb0032006"},{"key":"e_1_2_1_2_44_2","unstructured":"Segala R (1995) Modeling and Verification of randomized distributed real-time systems. Phd thesis MIT"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Yi W (1991) CCS + time z \u00a0= an interleaving model for real-time systems. In: Proceedings of ICALP\u201991. Lecture Notes of Computer Science vol 510. Springer Berlin pp 217\u2013228","DOI":"10.1007\/3-540-54233-7_136"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0230-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:58:37Z","timestamp":1641484717000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0230-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":45,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["10.1007\/s00165-012-0230-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0230-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7]]}}}