{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:04:14Z","timestamp":1750309454085,"version":"3.41.0"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,3,3]],"date-time":"2025-03-03T00:00:00Z","timestamp":1740960000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Science and Education Research Board (SERB), Department of Science and Technology (DST), India","award":["CRG\/2023\/001847"],"award-info":[{"award-number":["CRG\/2023\/001847"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,6,30]]},"abstract":"<jats:p>\n            This article defines embeddings between state-based and action-based probabilistic logics which can be used to support probabilistic model checking. First, we slightly modify the model embeddings proposed in the literature to allow invisible computation steps and the preservation of forward and backward bisimulation relations. Next, we propose the syntax and semantics of an action-based Probabilistic Computation Tree Logic (APCTL) and an action-based PCTL* (APCTL*) interpreted over action-labeled discrete-time Markov chains (ADTMCs). We show that both these logics are strictly more expressive than the probabilistic variant of Hennessy\u2013Milner logic (prHML). We define an embedding\n            <jats:italic>aldl<\/jats:italic>\n            which can be used to construct APCTL* formulae from PCTL* formulae and an embedding\n            <jats:italic>sldl<\/jats:italic>\n            from APCTL* formulae to PCTL* formulae. Similarly, we define the embeddings\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(aldl^{\\prime }\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            and\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(sldl^{\\prime }\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            from PCTL to APCTL and APCTL to PCTL, respectively. We also define the reward-based variant of APCTL (APRCTL) interpreted over action-based Markov Reward Models (AMRM), and accordingly modify the logical embeddings\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(aldl^{\\prime }\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            and\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(sldl^{\\prime }\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            which allows us to take into account the notion of rewards. Additionally, we also show that the idea of rewards can be used to reason about the bounded until operator in PCTL and APCTL. Finally, we prove that our logical embeddings combined with the model embeddings enable one to minimize, analyze, and verify probabilistic models in one domain using state-of-the-art tools and techniques developed for the other domain. In order to validate the efficacy of our theoretical framework, we apply it to two case studies using the probabilistic symbolic model checker (PRISM).\n          <\/jats:p>","DOI":"10.1145\/3696431","type":"journal-article","created":{"date-parts":[[2024,9,21]],"date-time":"2024-09-21T09:49:15Z","timestamp":1726912155000},"page":"1-58","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Embeddings Between State and Action Based Probabilistic Logics"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9118-7402","authenticated-orcid":false,"given":"Susmoy","family":"Das","sequence":"first","affiliation":[{"name":"Department of Electrical Engineering and Computer Science, Indian Institute of Science Education and Research Bhopal, Bhopal, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-3923-2492","authenticated-orcid":false,"given":"Arpit","family":"Sharma","sequence":"additional","affiliation":[{"name":"Department of Electrical Engineering and Computer Science, Indian Institute of Science Education and Research Bhopal, Bhopal, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,3,3]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"88","volume-title":"Proceedings of the FORMATS (LNCS 2791)","author":"Andova Suzana","year":"2003","unstructured":"Suzana Andova, Holger Hermanns, and Joost-Pieter Katoen. 2003. Discrete-time rewards model-checked. In Proceedings of the FORMATS (LNCS 2791). Springer, 88\u2013104."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_75"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60045-0_48"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1135"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.36"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_24"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_14"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Christel Baier Holger Hermanns Joost-Pieter Katoen and Verena Wolf. 2005. Bisimulation and simulation relations for markov chains. In Proceedings of the Workshop \u201cEssays on Algebraic Process Calculi\u201d APC 25 Bertinoro Italy August 1\u20135 2005 (Electronic Notes in Theoretical Computer Science). Elsevier 73\u201378. DOI:10.1016\/J.ENTCS.2005.12.078","DOI":"10.1016\/J.ENTCS.2005.12.078"},{"key":"e_1_3_2_10_2","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008","unstructured":"C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.03.001"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.2307\/3215235"},{"key":"e_1_3_2_13_2","first-page":"21","volume-title":"Proceedings of the TACAS (LNCS 11428)","author":"Bunte Olav","year":"2019","unstructured":"Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse. 2019. The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In Proceedings of the TACAS (LNCS 11428). Springer, 21\u201339."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24756-2_8"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0025774"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.03.048"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780195366587.001.0001"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3412841.3442048"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91825-5_3"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-20872-0_8"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-35355-0_8"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2003.07.009"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"e_1_3_2_25_2","volume-title":"Labelled Markov Processes","author":"Desharnais Josee","year":"1999","unstructured":"Josee Desharnais. 1999. Labelled Markov Processes. PhD thesis. McGill University."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802190"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567081"},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","unstructured":"E. Allen Emerson and Joseph Y. Halpern. 1986. \u201cSometimes\u201d and \u201cNot Never\u201d revisited: On Branching versus linear time temporal logic. J. ACM 33 1 (1986) 151\u2013178.","DOI":"10.1145\/4904.4999"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_33"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-012-0244-Z"},{"key":"e_1_3_2_31_2","unstructured":"Geoffrey R. Grimmett and David R. Stirzaker. 2019. The lost boarding pass and other practical problems. arXiv:1910.02515. Retrieved from https:\/\/arxiv.org\/abs\/1910.02515"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68270-9_3"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_19"},{"key":"e_1_3_2_34_2","first-page":"278","volume-title":"Proceedings of the RTSS","author":"Hansson Hans","year":"1990","unstructured":"Hans Hansson and Bengt Jonsson. 1990. A calculus for communicating systems with time and probabitilies. In Proceedings of the RTSS. IEEE Computer Society, 278\u2013287."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00633-z"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.11.024"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569951"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614940"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151651"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039071"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2005.2"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"e_1_3_2_45_2","volume-title":"Finite Markov Chains","author":"Kemeny John G.","year":"1960","unstructured":"John G. Kemeny and James Laurie Snell. 1960. Finite Markov Chains. Vol. 356. Van Nostrand Princeton, NJ."},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_3_2_48_2","first-page":"25:1\u201325:18","volume-title":"Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India (LIPIcs)","volume":"65","author":"Larsen Kim G.","year":"2016","unstructured":"Kim G. Larsen, Radu Mardare, and Bingtian Xue. 2016. Probabilistic mu-calculus: Decidability and complete axiomatization. In Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India (LIPIcs), Vol. 65. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 25:1\u201325:18."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_3_2_50_2","first-page":"882","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015","author":"Liu Wanwei","year":"2015","unstructured":"Wanwei Liu, Lei Song, Ji Wang, and Lijun Zhang. 2015. A simple probabilistic extension of modal mu-calculus. In Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015. 882\u2013888."},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00171-E"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/190.191"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.2307\/2586667"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0499-0"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"Annabelle McIver and Carroll Morgan. 2007. Results on the quantitative \\(\\mu\\) -calculus qM \\(\\mu\\) . ACM Trans. Comput. Logic 8 1 (January 2007) 3-es. DOI:10.1145\/1182613.1182616","DOI":"10.1145\/1182613.1182616"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211557"},{"issue":"4","key":"e_1_3_2_57_2","article-title":"Probabilistic modal mu-calculus with independent product","volume":"8","author":"Mio Matteo","year":"2012","unstructured":"Matteo Mio. 2012. Probabilistic modal mu-calculus with independent product. Log. Methods Comput. Sci. 8, 4 (2012).","journal-title":"Log. Methods Comput. Sci."},{"key":"e_1_3_2_58_2","article-title":"A probabilistic temporal calculus based on expectations","author":"Morgan Carroll","year":"1997","unstructured":"Carroll Morgan and Annabelle McIver. 1997. A probabilistic temporal calculus based on expectations. Proceddings of Formal Methods 97 (1997).","journal-title":"Proceddings of Formal Methods"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(93)90047-8"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-53479-2_17"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/201019.201032"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_21"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxs156"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18381-2_41"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.74"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_23"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1123"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696431","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3696431","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:10:13Z","timestamp":1750295413000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696431"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,3]]},"references-count":66,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6,30]]}},"alternative-id":["10.1145\/3696431"],"URL":"https:\/\/doi.org\/10.1145\/3696431","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2025,3,3]]},"assertion":[{"value":"2023-05-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-03","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}