{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:57Z","timestamp":1753889817925,"version":"3.41.2"},"reference-count":24,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,6,1]],"date-time":"2012-06-01T00:00:00Z","timestamp":1338508800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The probabilistic (or quantitative) modal mu-calculus is a fixed-point logic\nde- signed for expressing properties of probabilistic labeled transition\nsystems (PLTS). Two semantics have been studied for this logic, both assigning\nto every process state a value in the interval [0,1] representing the\nprobability that the property expressed by the formula holds at the state. One\nsemantics is denotational and the other is a game semantics, specified in terms\nof two-player stochastic games. The two semantics have been proved to coincide\non all finite PLTS's, but the equivalence of the two semantics on arbitrary\nmodels has been open in literature. In this paper we prove that the equivalence\nindeed holds for arbitrary infinite models, and thus our result strengthens the\nfruitful connection between denotational and game semantics. Our proof adapts\nthe unraveling or unfolding method, a general proof technique for proving\nresult of parity games by induction on their complexity.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:7)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":5,"title":["On the equivalence of game and denotational semantics for the probabilistic mu-calculus"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"given":"Matteo","family":"Mio","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,6,1]]},"reference":[{"issue":"1","key":"10.2168\/LMCS-8(2:7)2012_Bartels02","doi-asserted-by":"crossref","DOI":"10.1016\/S1571-0661(04)80358-X","volume":"65","author":"F. Bartels","year":"2002","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1","key":"10.2168\/LMCS-8(2:7)2012_Dam94","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","journal-title":"In Theoretical Computer Science"},{"issue":"2","key":"10.2168\/LMCS-8(2:7)2012_AM04","first-page":"374","volume":"68","author":"L. de Alfaro and R. Majumdar","year":"2004","journal-title":"Journal of Computer and System Sciences, Volume 68 , Issue 2 pages 374 - 397, 2004"},{"key":"10.2168\/LMCS-8(2:7)2012_EJ91","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185392"},{"issue":"3","key":"10.2168\/LMCS-8(2:7)2012_FGK2010","volume":"47","author":"D. Fischer, E. Gr\u00e4del, and L. Kaiser","year":"2010","journal-title":"Theory of Computing Systems"},{"key":"10.2168\/LMCS-8(2:7)2012_Gradel2007","unstructured":"E. Gr\u00e4del.Finite Model Theory and Its Application. Texts in Theoretical Computer Science. Springer, 2007."},{"key":"10.2168\/LMCS-8(2:7)2012_HP2000","doi-asserted-by":"crossref","unstructured":"O. M. Herescu and C. Palamiessi. Probabilistic asynchronouspi-calculus. InProceedings of FOSSACS 2000, pages 146-160, 2000.","DOI":"10.1007\/3-540-46432-8_10"},{"key":"10.2168\/LMCS-8(2:7)2012_HM96","doi-asserted-by":"crossref","unstructured":"M. Huth and M. Kwiatkowska. Quantitative analysis and model checking. InProceedings of the 12th Annual IEEE Symposium on Logic In Computer Science, page 111, Washington, DC, USA, 1997. IEEE Computer Society.","DOI":"10.1109\/LICS.1997.614940"},{"key":"10.2168\/LMCS-8(2:7)2012_JW96","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/3-540-61604-7_60","volume":"1119","author":"D. Janin and I. Walukiewicz","year":"1996","journal-title":"Lecture Notes in Computer Science"},{"key":"10.2168\/LMCS-8(2:7)2012_Kechris","doi-asserted-by":"crossref","unstructured":"A. S. Kechris.Classical Descriptive Set Theory. Graduate Texts in Mathematics. Springer Verlag, 1994.","DOI":"10.1007\/978-1-4612-4190-4"},{"key":"10.2168\/LMCS-8(2:7)2012_Kozen83","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the propositional mu-calculus. InTheoretical Computer Science, pages 333-354, 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"10.2168\/LMCS-8(2:7)2012_KNPV2009","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, D. Parker, and M. Vigotti. Probabilistic mobile ambients.Theoretical Computer Science, pages 12-13, 2009.","DOI":"10.1016\/j.tcs.2008.12.058"},{"issue":"2","key":"10.2168\/LMCS-8(2:7)2012_MS98","doi-asserted-by":"crossref","first-page":"861","DOI":"10.1214\/aop\/1176989271","volume":"21","author":"A. Maitra and W. Sudderth","year":"1993","journal-title":"Annals of Probability"},{"issue":"4","key":"10.2168\/LMCS-8(2:7)2012_Martin98","doi-asserted-by":"crossref","first-page":"1565","DOI":"10.2307\/2586667","volume":"63","author":"D. A. Martin","year":"1998","journal-title":"In Journal of Symbolic Logic"},{"issue":"1","key":"10.2168\/LMCS-8(2:7)2012_MM07","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/1182613.1182616","volume":"8","author":"A. McIver and C. Morgan","year":"2007","journal-title":"ACM Trans. Comput. Logic"},{"key":"10.2168\/LMCS-8(2:7)2012_MIO11","doi-asserted-by":"crossref","unstructured":"M. Mio. Probabilistic Modal\u00ce\u00bc-Calculus with Independent Product. InFoundations of Software Science and Computation Structures, volume 6604 ofLecture Notes in Computer Science, pages 290-304. Springer-Verlag Berlin, 2011.","DOI":"10.1007\/978-3-642-19805-2_20"},{"key":"10.2168\/LMCS-8(2:7)2012_MioThesis","unstructured":"M. Mio.Game Semantics for Probabilistic\u00ce\u00bc-Calculi. PhD thesis, School of Informatics, University of Edinburgh, 2012."},{"key":"10.2168\/LMCS-8(2:7)2012_MM97","unstructured":"C. Morgan and A. McIver. A probabilistic temporal calculus based on expectations. InIn Lindsay Groves and Steve Reeves, editors, Proc. Formal Methods. Springer Verlag, 1997."},{"key":"10.2168\/LMCS-8(2:7)2012_Santocanale2002","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1051\/ita:2002010","volume":"36","author":"L. Santocanale","year":"2002","journal-title":"Theoretical Informatics and Applications September 2002"},{"key":"10.2168\/LMCS-8(2:7)2012_S95","unstructured":"R. Segala.Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Laboratory for Computer Science, Massachusetts Institute of Technology, 1995."},{"key":"10.2168\/LMCS-8(2:7)2012_Stirling96","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3550-5"},{"key":"10.2168\/LMCS-8(2:7)2012_Tao_measuretheory","doi-asserted-by":"crossref","unstructured":"T. Tao.An introduction to measure theory. Graduate Studies in Mathematics. American Mathematical Society, 2011.","DOI":"10.1090\/gsm\/126"},{"issue":"2","key":"10.2168\/LMCS-8(2:7)2012_Tarski1955","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","journal-title":"Pacific Journal of Mathematics"},{"key":"10.2168\/LMCS-8(2:7)2012_zielonka04","doi-asserted-by":"crossref","unstructured":"W. Zielonka. Perfect-information stochastic parity games. InFoundations of Software Science and Computation Structures, volume 2987 ofLecture Notes in Computer Science, pages 499-513. Springer, 2004.","DOI":"10.1007\/978-3-540-24727-2_35"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/787\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/787\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:55:58Z","timestamp":1681242958000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/787"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,1]]},"references-count":24,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:7)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1205.0126","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1205.0126","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,6,1]]},"article-number":"787"}}