{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T00:43:14Z","timestamp":1777596194235,"version":"3.51.4"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,7,11]],"date-time":"2013-07-11T00:00:00Z","timestamp":1373500800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2013,10]]},"abstract":"<jats:p>\n            We introduce a unifying framework to provide the semantics of process algebras, including their quantitative variants useful for modeling quantitative aspects of behaviors. The unifying framework is then used to describe some of the most representative stochastic process algebras. This provides a general and clear support for an understanding of their similarities and differences. The framework is based on\n            <jats:italic>State to Function Labeled Transition Systems<\/jats:italic>\n            , F\n            <jats:sc>u<\/jats:sc>\n            TS\n            <jats:sc>s<\/jats:sc>\n            for short, that are state transition structures where each transition is a triple of the form (\n            <jats:italic>s<\/jats:italic>\n            ,\u03b1,\ud835\udcab). The first and the second components are the source state,\n            <jats:italic>s<\/jats:italic>\n            , and the label, \u03b1, of the transition, while the third component is the\n            <jats:italic>continuation function<\/jats:italic>\n            , \ud835\udcab, associating a value of a suitable type to each state\n            <jats:italic>s<\/jats:italic>\n            '. For example, in the case of stochastic process algebras the value of the\n            <jats:italic>continuation function<\/jats:italic>\n            on\n            <jats:italic>s<\/jats:italic>\n            ' represents the rate of the negative exponential distribution characterizing the duration\/delay of the action performed to reach state\n            <jats:italic>s<\/jats:italic>\n            ' from\n            <jats:italic>s<\/jats:italic>\n            . We first provide the semantics of a simple formalism used to describe continuous-time Markov chains, then we model a number of process algebras that permit parallel composition of models according to the two main interaction paradigms (multiparty and one-to-one synchronization). Finally, we deal with formalisms where actions and rates are kept separate and address the issues related to the coexistence of stochastic, probabilistic, and nondeterministic behaviors. For each formalism, we establish the formal correspondence between the F\n            <jats:sc>u<\/jats:sc>\n            TS\n            <jats:sc>s<\/jats:sc>\n            semantics and its original semantics.\n          <\/jats:p>","DOI":"10.1145\/2522968.2522973","type":"journal-article","created":{"date-parts":[[2013,11,6]],"date-time":"2013-11-06T14:09:19Z","timestamp":1383746959000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":37,"title":["A uniform definition of stochastic process calculi"],"prefix":"10.1145","volume":"46","author":[{"given":"Rocco de","family":"Nicola","sequence":"first","affiliation":[{"name":"IMT -- Institute for Advanced Studies Lucca, Lucca, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Diego","family":"Latella","sequence":"additional","affiliation":[{"name":"CNR -- Istituto di Scienza e Tecnologie dell'Informazione \u201cA. Faedo\u201d, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michele","family":"Loreti","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Firenze, Firenze, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mieke","family":"Massink","sequence":"additional","affiliation":[{"name":"CNR -- Istituto di Scienza e Tecnologie dell'Informazione \u201cA. Faedo\u201d, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,7,11]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Aceto L. Fokking W. and Verhoef C. 2001. Structural operational semantics. In Handbook of Process Algebra. Elsevier 197--292.  Aceto L. Fokking W. and Verhoef C. 2001. Structural operational semantics. In Handbook of Process Algebra. Elsevier 197--292.","DOI":"10.1016\/B978-044482830-9\/50021-7"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"Aldini A. Bernardo M. and Corradini F. 2010. A Process Algebraic Approach to Software Architecture Design. Springer.   Aldini A. Bernardo M. and Corradini F. 2010. A Process Algebraic Approach to Software Architecture Design. Springer.","DOI":"10.1007\/978-1-84800-223-4"},{"key":"e_1_2_2_3_1","first-page":"1","article-title":"GSOS for probabilistic transition systems","volume":"65","author":"Bartels F.","year":"2002","unstructured":"Bartels , F. 2002 . GSOS for probabilistic transition systems . Electron. Notes Theor. Comput. Syst. 65 , 1, 1 -- 25 . Bartels, F. 2002. GSOS for probabilistic transition systems. Electron. Notes Theor. Comput. Syst. 65, 1, 1--25.","journal-title":"Electron. Notes Theor. Comput. Syst."},{"key":"e_1_2_2_4_1","first-page":"1","article-title":"A hierarchy of probabilistic system types","volume":"82","author":"Bartels F.","year":"2003","unstructured":"Bartels , F. , Sokolova , A. , and de Vink , E. P. 2003 . A hierarchy of probabilistic system types . Electron. Notes Theor. Comput. Syst. 82 , 1, 1 -- 19 . Bartels, F., Sokolova, A., and de Vink, E. P. 2003. A hierarchy of probabilistic system types. Electron. Notes Theor. Comput. Syst. 82, 1, 1--19.","journal-title":"Electron. Notes Theor. Comput. Syst."},{"key":"e_1_2_2_5_1","volume-title":"eds","author":"Bergstra J.","year":"2001","unstructured":"Bergstra , J. , Ponse , A. , and Smolka , S. , eds . 2001 . Handbook of Process Algebra. Elsevier . Bergstra, J., Ponse, A., and Smolka, S., eds. 2001. Handbook of Process Algebra. Elsevier."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.25.19"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1893701.1893705"},{"key":"e_1_2_2_8_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01)","author":"Blom S.","unstructured":"Blom , S. , Fokkink , W. , Groote , J. F. , van Langevelde , I. , Lisser , B. , and van de Pol , J. 2001. &mu;crl : A toolset for analysing algebraic specifications . In Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01) . Lecture Notes in Computer Science , vol. 2102 , Springer , 250--254. Blom, S., Fokkink, W., Groote, J. F., van Langevelde, I., Lisser, B., and van de Pol, J. 2001. &mu;crl: A toolset for analysing algebraic specifications. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01). Lecture Notes in Computer Science, vol. 2102, Springer, 250--254."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.104"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Brinksma E.\n     and \n      Hermanns H\n  . \n  2001\n  . Process algebra and markov chains. In Lectures on Formal Methods and Performance Analysis Lecture Notes in Computer Science vol. \n  2090 Springer 181--231.   Brinksma E. and Hermanns H. 2001. Process algebra and markov chains. In Lectures on Formal Methods and Performance Analysis Lecture Notes in Computer Science vol. 2090 Springer 181--231.","DOI":"10.1007\/3-540-44667-2_5"},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the 2nd International Workshop on Process Algebras and Probabilistic Modeling (PAPM'94)","author":"Buchholz P.","year":"1994","unstructured":"Buchholz , P. 1994 . Markovian process algebra: Composition and equivalence . In Proceedings of the 2nd International Workshop on Process Algebras and Probabilistic Modeling (PAPM'94) . 11--30. Buchholz, P. 1994. Markovian process algebra: Composition and equivalence. In Proceedings of the 2nd International Workshop on Process Algebras and Probabilistic Modeling (PAPM'94). 11--30."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.30"},{"key":"e_1_2_2_13_1","unstructured":"De Nicola R. Katoen J.-P. Latella D. Loreti M. and Massink M. 2006. Klaim and its stochastic semantics. Tech. rep. 6 Dipartimento di Sistemi e Informatica Universit\u00e0 di Firenze. http:\/\/rap.dsi.unifi.it\/&sim;loreti\/papers\/TR062006.pdf.  De Nicola R. Katoen J.-P. Latella D. Loreti M. and Massink M. 2006. Klaim and its stochastic semantics. Tech. rep. 6 Dipartimento di Sistemi e Informatica Universit\u00e0 di Firenze. http:\/\/rap.dsi.unifi.it\/&sim;loreti\/papers\/TR062006.pdf."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.07.071"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04570-7_2"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02930-1_36"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066677.1066777"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.15"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.41"},{"key":"e_1_2_2_20_1","volume-title":"Proceedings of the 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11)","author":"Fahrenberg U.","unstructured":"Fahrenberg , U. , Thrane , C. , and Larsen , K . 2011. Distances for weighted transition systems: Games and properties . In Proceedings of the 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11) . 134--147. Fahrenberg, U., Thrane, C., and Larsen, K. 2011. Distances for weighted transition systems: Games and properties. In Proceedings of the 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11). 134--147."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647339.721059"},{"key":"e_1_2_2_22_1","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Markov Chains","author":"Hermanns H.","unstructured":"Hermanns , H. 2002. Interactive Markov Chains . Lecture Notes in Computer Science , vol. 2428 , Springer . Hermanns, H. 2002. Interactive Markov Chains. Lecture Notes in Computer Science, vol. 2428, Springer."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00305-4"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0169-7552(97)00133-5"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2007.96"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939101.1939127"},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods (PAPM'94)","author":"Hillston J.","year":"1994","unstructured":"Hillston , J. 1994 . The nature of synchronisation . In Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods (PAPM'94) . 51--70. Hillston, J. 1994. The nature of synchronisation. In Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods (PAPM'94). 51--70."},{"key":"e_1_2_2_28_1","volume-title":"A Compositional Approach to Performance Modelling. Distinguished Dissertation in Computer Science","author":"Hillston J.","unstructured":"Hillston , J. 1996. A Compositional Approach to Performance Modelling. Distinguished Dissertation in Computer Science , Cambridge University Press . Hillston, J. 1996. A Compositional Approach to Performance Modelling. Distinguished Dissertation in Computer Science, Cambridge University Press."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1363686.1363775"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050034"},{"key":"e_1_2_2_31_1","series-title":"Lecture Notes in Computer Science","volume-title":"Semantics and Algebraic Specification","author":"Klin B.","unstructured":"Klin , B. 2009. Structural operational semantics for weighted transition systems . In Semantics and Algebraic Specification . Lecture Notes in Computer Science , vol. 5700 , Springer , 121--139. Klin, B. 2009. Structural operational semantics for weighted transition systems. In Semantics and Algebraic Specification. Lecture Notes in Computer Science, vol. 5700, Springer, 121--139."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792833"},{"key":"e_1_2_2_33_1","volume-title":"Continuous-time probabilistic automata. InInformation and Control 15","author":"Knast R.","unstructured":"Knast , R. 1969. Continuous-time probabilistic automata. InInformation and Control 15 . Elsevier , 335--352. Knast, R. 1969. Continuous-time probabilistic automata. InInformation and Control 15. Elsevier, 335--352."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.93.2"},{"key":"e_1_2_2_35_1","series-title":"Series in Computer Science","volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"Milner , R. 1989. Communication and Concurrency . Series in Computer Science . Prentice Hall . Milner, R. 1989. Communication and Concurrency. Series in Computer Science. Prentice Hall."},{"key":"e_1_2_2_36_1","volume-title":"Matrix-Geometric Solutions in Stochastic Models\u2014An Algorithmic Approach","author":"Neuts M.","unstructured":"Neuts , M. 1981. Matrix-Geometric Solutions in Stochastic Models\u2014An Algorithmic Approach . The Johns Hopkins University Press , Baltimore, MD . Neuts, M. 1981. Matrix-Geometric Solutions in Stochastic Models\u2014An Algorithmic Approach. The Johns Hopkins University Press, Baltimore, MD."},{"key":"e_1_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Plotkin G. D. 2004. A structural approach to operational semantics. J. Logic Algebraic Program. 60--61 17--139.  Plotkin G. D. 2004. A structural approach to operational semantics. J. Logic Algebraic Program. 60--61 17--139.","DOI":"10.1016\/j.jlap.2004.05.001"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/38.7.578"},{"key":"e_1_2_2_40_1","series-title":"Lecture Notes in Computer Science","volume-title":"Validation of Stochastic Systems. A Guide to Current Research","author":"Sokolova A.","unstructured":"Sokolova , A. and de Vink , E. P. 2004. Probabilistic automata: System types, parallel composition and comparison . In Validation of Stochastic Systems. A Guide to Current Research . Lecture Notes in Computer Science , vol. 2925 , Springer , 1--43. Sokolova, A. and de Vink, E. P. 2004. Probabilistic automata: System types, parallel composition and comparison. In Validation of Stochastic Systems. A Guide to Current Research. Lecture Notes in Computer Science, vol. 2925, Springer, 1--43."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_26"},{"key":"e_1_2_2_42_1","volume-title":"Handbook of Process Algebra","author":"Van Glabbeek R.","unstructured":"Van Glabbeek , R. 2001. The linear time -- Branching time spectrum i . In Handbook of Process Algebra , Elsevier , 3--99. Van Glabbeek, R. 2001. The linear time -- Branching time spectrum i. In Handbook of Process Algebra, Elsevier, 3--99."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:6)2008"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2522968.2522973","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2522968.2522973","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:53Z","timestamp":1750232093000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2522968.2522973"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7,11]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["10.1145\/2522968.2522973"],"URL":"https:\/\/doi.org\/10.1145\/2522968.2522973","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7,11]]},"assertion":[{"value":"2011-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-07-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}