{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:02:02Z","timestamp":1750309322324,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,8]],"date-time":"2024-04-08T00:00:00Z","timestamp":1712534400000},"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":["MTR\/2023\/000675"],"award-info":[{"award-number":["MTR\/2023\/000675"]}]},{"name":"Science and Education Research Board (SERB)","award":["CRG\/2023\/001847"],"award-info":[{"award-number":["CRG\/2023\/001847"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,8]]},"DOI":"10.1145\/3605098.3636032","type":"proceedings-article","created":{"date-parts":[[2024,5,21]],"date-time":"2024-05-21T17:59:16Z","timestamp":1716314356000},"page":"1712-1721","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Framework of Model and Logical Embeddings for Verification of Stochastic Systems"],"prefix":"10.1145","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, Madhya Pradesh, India"}]},{"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, Madhya Pradesh, India"}]}],"member":"320","published-online":{"date-parts":[[2024,5,21]]},"reference":[{"volume-title":"8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings. 269--276","author":"Aziz Adnan","key":"e_1_3_2_1_1_1","unstructured":"Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert K. Brayton. 1996. Verifying Continuous Time Markov Chains. In Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings. 269--276."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.36"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.078"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.03.001"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.02.002"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Marco Bernardo. 2012. Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Concurrent Processes. In QAPL (EPTCS 85). 122--136.","DOI":"10.4204\/EPTCS.85.9"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_23"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Peter Buchholz. 1994. Exact and Ordinary Lumpability in Finite Markov Chains. J. of Appl. Prob. (1994) 59--75.","DOI":"10.1017\/S0021900200107338"},{"key":"e_1_3_2_1_11_1","volume-title":"Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse.","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. In Tools and Algorithms for the Construction and Analysis of Systems. Springer International Publishing, Cham, 21--39."},{"volume-title":"Stochastic Process Algebras","author":"Clark Allan","key":"e_1_3_2_1_12_1","unstructured":"Allan Clark, Stephen Gilmore, Jane Hillston, and Mirco Tribastone. 2007. Stochastic Process Algebras. Springer Berlin Heidelberg, Berlin, Heidelberg, 132--179."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/648202.749254"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3412841.3442048"},{"key":"e_1_3_2_1_15_1","volume-title":"EPEW 2021, and 26th International Conference, ASMTA 2021, Virtual Event, December 9--10 and December 13--14, 2021, Proceedings. 44--61","author":"Das Susmoy","year":"2021","unstructured":"Susmoy Das and Arpit Sharma. 2021. State Space Minimization Preserving Embeddings for Continuous-Time Markov Chains. In Performance Engineering and Stochastic Modeling - 17th European Workshop, EPEW 2021, and 26th International Conference, ASMTA 2021, Virtual Event, December 9--10 and December 13--14, 2021, Proceedings. 44--61."},{"key":"e_1_3_2_1_16_1","volume-title":"FACS 2022, Virtual Event, November 10--11, 2022, Proceedings. 121--140","author":"Das Susmoy","year":"2022","unstructured":"Susmoy Das and Arpit Sharma. 2022. Embeddings Between State and Action Based Probabilistic Logics. In Formal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, November 10--11, 2022, Proceedings. 121--140."},{"volume-title":"FORTE (LNCS 13910)","author":"Das Susmoy","key":"e_1_3_2_1_17_1","unstructured":"Susmoy Das and Arpit Sharma. 2023. On the Use of Model and Logical Embeddings for Model Checking of Probabilistic Systems. In FORTE (LNCS 13910). Springer, 115--131."},{"volume-title":"CAV (LNCS 10427)","author":"Dehnert Christian","key":"e_1_3_2_1_18_1","unstructured":"Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. 2017. A STORM is Coming: A Modern Probabilistic Model Checker. In CAV (LNCS 10427). Springer, 592--600."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00068-1"},{"key":"e_1_3_2_1_20_1","unstructured":"James Edwards. 2001. Process Algebras for Protocol Validation and Analysis. In PREP."},{"key":"e_1_3_2_1_21_1","volume-title":"CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In TACAS","volume":"6605","author":"Garavel Hubert","year":"2011","unstructured":"Hubert Garavel, Fr\u00e9d\u00e9ric Lang, Radu Mateescu, and Wendelin Serwe. 2011. CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In TACAS, Vol. 6605. Springer, 372--387."},{"key":"e_1_3_2_1_22_1","volume-title":"7th International Conference","author":"Gilmore Stephen","year":"1994","unstructured":"Stephen Gilmore and Jane Hillston. 1994. The PEPA Workbench: A Tool to Support a Process Algebra-based Approach to Performance Modelling. In Computer Performance Evaluation, Modeling Techniques and Tools, 7th International Conference, Vienna, Austria, May 3--6, 1994, Proceedings (LNCS 794). Springer, 353--368."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.922715"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00305-4"},{"key":"e_1_3_2_1_25_1","volume-title":"Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 1--3, 2000, Proceedings. 420--439","author":"Hermanns Holger","year":"2000","unstructured":"Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, and Markus Siegle. 2000. Towards Model Checking Stochastic Process Algebra. In Integrated Formal Methods, Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 1--3, 2000, Proceedings. 420--439."},{"volume-title":"A Compositional Approach to Performance Modelling","author":"Hillston Jane","key":"e_1_3_2_1_26_1","unstructured":"Jane Hillston. 1996. A Compositional Approach to Performance Modelling. Cambridge University Press, USA."},{"key":"e_1_3_2_1_27_1","volume-title":"Zapreev","author":"Katoen Joost-Pieter","year":"2005","unstructured":"Joost-Pieter Katoen, Maneesh Khattri, and Ivan S. Zapreev. 2005. A Markov Reward Model Checker. In QEST. IEEE Computer Society, 243--244."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska G. Norman and D. Parker. 2007. Stochastic Model Checking. In Formal Methods for the Design of Computer Communication and Software Systems: Performance Evaluation (SFM'07) (LNCS (Tutorial Volume) 4486). Springer 220--270.","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"e_1_3_2_1_29_1","volume-title":"Proc. 23rd International Conference on Computer Aided Verification (CAV'11)","volume":"591","author":"Kwiatkowska M.","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV'11) (LNCS, Vol. 6806). Springer, 585--591."},{"key":"e_1_3_2_1_30_1","unstructured":"Marco Ajmone Marsan G. Balbo Gianni Conte S. Donatelli and G. Franceschinis. 1994. Modelling with Generalized Stochastic Petri Nets (1st ed.). John Wiley & Sons Inc. USA."},{"key":"e_1_3_2_1_31_1","volume-title":"International Workshop on Timed Petri Nets","author":"Meyer John F.","year":"1985","unstructured":"John F. Meyer, Ali Movaghar, and William H. Sanders. 1985. Stochastic Activity Networks: Structure, Behavior, and Application. In International Workshop on Timed Petri Nets, Torino, Italy, July 1--3, 1985. IEEE Computer Society, 106--115."},{"key":"e_1_3_2_1_32_1","volume-title":"Vaandrager","author":"Nicola Rocco De","year":"1990","unstructured":"Rocco De Nicola and Frits W. Vaandrager. 1990. Action versus State based Logics for Transition Systems. In Semantics of Systems of Concurrent Processes, LITP Spring School on Theoretical Computer Science, La Roche Posay, France, April 23--27, 1990, Proceedings (LNCS 469). Springer, 407--419."},{"key":"e_1_3_2_1_33_1","volume-title":"Vaandrager","author":"Nicola Rocco De","year":"1990","unstructured":"Rocco De Nicola and Frits W. Vaandrager. 1990. Action versus State based Logics for Transition Systems. In Semantics of Systems of Concurrent Processes, LITP Spring School on Theoretical Computer Science, La Roche Posay, France, April 23--27, 1990, Proceedings. 407--419."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/201019.201032"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.99196"},{"volume-title":"Reduction Techniques for Nondeterministic and Probabilistic Systems. Ph. D. Dissertation","author":"Sharma Arpit","key":"e_1_3_2_1_36_1","unstructured":"Arpit Sharma. 2015. Reduction Techniques for Nondeterministic and Probabilistic Systems. Ph. D. Dissertation. RWTH Aachen University, Germany."},{"key":"e_1_3_2_1_37_1","volume-title":"PSI 2011","author":"Sharma Arpit","year":"2011","unstructured":"Arpit Sharma and Joost-Pieter Katoen. 2011. Weighted Lumpability on Markov Chains. In Perspectives of Systems Informatics - 8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27-July 1, 2011, Revised Selected Papers (LNCS 7162). Springer, 322--339."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.74"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.042"}],"event":{"name":"SAC '24: 39th ACM\/SIGAPP Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Avila Spain","acronym":"SAC '24"},"container-title":["Proceedings of the 39th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3605098.3636032","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3605098.3636032","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:03:59Z","timestamp":1750291439000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3605098.3636032"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,8]]},"references-count":39,"alternative-id":["10.1145\/3605098.3636032","10.1145\/3605098"],"URL":"https:\/\/doi.org\/10.1145\/3605098.3636032","relation":{},"subject":[],"published":{"date-parts":[[2024,4,8]]},"assertion":[{"value":"2024-05-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}