{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T22:36:32Z","timestamp":1763764592206,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642342806"},{"type":"electronic","value":"9783642342813"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34281-3_12","type":"book-chapter","created":{"date-parts":[[2012,10,29]],"date-time":"2012-10-29T18:38:09Z","timestamp":1351535889000},"page":"135-150","source":"Crossref","is-referenced-by-count":11,"title":["Modeling and Verification of Probabilistic Actor Systems Using pRebeca"],"prefix":"10.1007","author":[{"given":"Mahsa","family":"Varshosaz","sequence":"first","affiliation":[]},{"given":"Ramtin","family":"Khosravi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"12_CR1","first-page":"385","volume":"63","author":"M. Sirjani","year":"2004","unstructured":"Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundam. Inf.\u00a063(4), 385\u2013410 (2004)","journal-title":"Fundam. Inf."},{"key":"12_CR2","unstructured":"Hewitt, C.: Description and theoretical analysis (using schemata) of PLANNER: A language for proving theorems and manipulating models in a robot. MIT Artificial Intelligence Technical Report 258, Department of Computer Science. MIT (April 1972)"},{"key":"12_CR3","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"Actors: a model of concurrent computation in distributed systems","author":"G. Agha","year":"1986","unstructured":"Agha, G.: Actors: a model of concurrent computation in distributed systems. MIT Press, Cambridge (1986)"},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S095679689700261X","volume":"7","author":"G. Agha","year":"1998","unstructured":"Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. Journal of Functional Programming\u00a07, 1\u201372 (1998)","journal-title":"Journal of Functional Programming"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1596655.1596658","volume-title":"Proceedings of the 7th International Conference on Principles and Practice of Programming in Java, PPPJ 2009","author":"R.K. Karmani","year":"2009","unstructured":"Karmani, R.K., Shali, A., Agha, G.: Actor frameworks for the JVM platform: a comparative analysis. In: Proceedings of the 7th International Conference on Principles and Practice of Programming in Java, PPPJ 2009, pp. 11\u201320. ACM, New York (2009)"},{"issue":"5","key":"12_CR6","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1109\/MIC.2008.107","volume":"12","author":"C. Hewitt","year":"2008","unstructured":"Hewitt, C.: Orgs for scalable, robust, privacy-friendly client cloud computing. IEEE Internet Computing\u00a012(5), 96\u201399 (2008)","journal-title":"IEEE Internet Computing"},{"key":"12_CR7","unstructured":"Hewitt, C.: Actorscript(tm): Industrial strength integration of local and nonlocal concurrency for client-cloud computing. CoRR abs\/0907.3330 (2009)"},{"issue":"2","key":"12_CR8","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","volume":"153","author":"G. Agha","year":"2006","unstructured":"Agha, G., Meseguer, J., Sen, K.: Pmaude: Rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci.\u00a0153(2), 213\u2013239 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"issue":"2","key":"12_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1880050.1880055","volume":"10","author":"N. Razavi","year":"2011","unstructured":"Razavi, N., Behjati, R., Sabouri, H., Khamespanah, E., Shali, A., Sirjani, M.: Sysfier: Actor-based formal verification of systemc. ACM Trans. Embed. Comput. Syst.\u00a010(2), 19:1\u201319:35 (2011)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1016\/S1571-0661(05)80465-7","volume":"7","author":"C. Baier","year":"1997","unstructured":"Baier, C., Kwiatkowska, M.Z.: Domain equations for probabilistic processes. Electr. Notes Theor. Comput. Sci.\u00a07, 34\u201354 (1997)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1016\/S1571-0661(05)82521-6","volume":"22","author":"J. Hartog den","year":"1999","unstructured":"den Hartog, J., de Vink, E.P.: Mixing up nondeterminism and probability: a preliminary report. Electr. Notes Theor. Comput. Sci.\u00a022, 88\u2013110 (1999)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"12_CR13","volume-title":"Time and Probability in Formal Design of Distributed Systems","author":"H.A. Hansson","year":"1994","unstructured":"Hansson, H.A.: Time and Probability in Formal Design of Distributed Systems. Elsevier Science Inc., New York (1994)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/BFb0084809","volume-title":"CONCUR \u201992","author":"K.G. Larsen","year":"1992","unstructured":"Larsen, K.G., Skou, A.: Compositional Verification of Probabilistic Processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 456\u2013471. Springer, Heidelberg (1992)"},{"issue":"2","key":"12_CR15","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/0304-3975(94)00171-E","volume":"138","author":"G. Lowe","year":"1995","unstructured":"Lowe, G.: Probabilistic and prioritized models of timed csp. Theor. Comput. Sci.\u00a0138(2), 315\u2013352 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Mathematical Foundations of Computer Science 1996","year":"1996","unstructured":"Penczek, W., Sza\u0142as, A. (eds.): MFCS 1996. LNCS, vol.\u00a01113. Springer, Heidelberg (1996)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1007\/BFb0039078","volume-title":"CONCUR \u201990","author":"C. Tofts","year":"1990","unstructured":"Tofts, C.: A Synchronous Calculus of Relative Frequency. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol.\u00a0458, pp. 467\u2013480. Springer, Heidelberg (1990)"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST 2006), pp. 131\u2013132. IEEE CS Press (2006)","DOI":"10.1109\/QEST.2006.25"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The Ins and Outs of The Probabilistic Model Checker MRMC. In: Quantitative Evaluation of Systems (QEST), pp. 167\u2013176. IEEE Computer Society (2009), www.mrmc-tool.org","DOI":"10.1109\/QEST.2009.11"},{"issue":"10","key":"12_CR20","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"H.C. Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: Modest: A compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng.\u00a032(10), 812\u2013830 (2006)","journal-title":"IEEE Trans. Software Eng."},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","year":"1999","unstructured":"Katoen, J.-P. (ed.): ARTS 1999. LNCS, vol.\u00a01601. Springer, Heidelberg (1999)"},{"key":"12_CR22","unstructured":"Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), San Diego, California, USA, June 23-25. IEEE (2004)"},{"key":"12_CR23","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. Representation and Mind Series. The MIT Press (2008)"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Information and Computation 88(1) (1990)","DOI":"10.1016\/0890-5401(90)90004-2"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34281-3_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,19]],"date-time":"2025-04-19T21:24:41Z","timestamp":1745097881000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34281-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642342806","9783642342813"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34281-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}