{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T16:30:29Z","timestamp":1759336229697,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2023,10,26]],"date-time":"2023-10-26T00:00:00Z","timestamp":1698278400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"German research council","award":["471367371"],"award-info":[{"award-number":["471367371"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Comput. Simul."],"published-print":{"date-parts":[[2023,10,31]]},"abstract":"<jats:p>\n            Stochastic hybrid automata (SHA) are a powerful tool to evaluate the dependability and safety of critical infrastructures. However, the resolution of nondeterminism, which is present in many purely hybrid models, is often only implicitly considered in SHA. This article instead proposes algorithms for computing maximum and minimum reachability probabilities for singular automata with\n            <jats:italic>urgent<\/jats:italic>\n            transitions and random clocks that follow arbitrary continuous probability distributions. We borrow a well-known approach from hybrid systems reachability analysis, namely flowpipe construction, which is then extended to optimize nondeterminism in the presence of random variables. First, valuations of random clocks that ensure reachability of specific goal states are extracted from the computed flowpipes, and second, reachability probabilities are computed by integrating over these valuations. We compute maximum and minimum probabilities for history-dependent prophetic and non-prophetic schedulers using set-based methods. The implementation featuring the library\n            <jats:sc>HyPro<\/jats:sc>\n            and the complexity of the approach are discussed in detail. Two case studies featuring nondeterministic choices show the feasibility of the approach.\n          <\/jats:p>","DOI":"10.1145\/3607197","type":"journal-article","created":{"date-parts":[[2023,7,11]],"date-time":"2023-07-11T11:52:40Z","timestamp":1689076360000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Optimizing Reachability Probabilities for a Restricted Class of Stochastic Hybrid Automata via Flowpipe Construction"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5510-4814","authenticated-orcid":false,"given":"Carina","family":"Da Silva","sequence":"first","affiliation":[{"name":"University of M\u00fcnster, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2055-7581","authenticated-orcid":false,"given":"Stefan","family":"Schupp","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Wien, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5912-4767","authenticated-orcid":false,"given":"Anne","family":"Remke","sequence":"additional","affiliation":[{"name":"University of M\u00fcnster, Germany"}]}],"member":"320","published-online":{"date-parts":[[2023,10,26]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.16.624-641"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_3_3_4_2","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-642-40196-1_30","volume-title":"10th Int. Conf. on Quantitative Evaluation of Systems (QEST\u201913) (LNCS)","author":"Ballarini Paolo","year":"2013","unstructured":"Paolo Ballarini, Nathalie Bertrand, Andr\u00e1s Horv\u00e1th, Marco Paolieri, and Enrico Vicario. 2013. Transient analysis of networks of stochastic timed automata using stochastic state classes. In 10th Int. Conf. on Quantitative Evaluation of Systems (QEST\u201913) (LNCS), Vol. 8054. Springer, 355\u2013371."},{"issue":"4","key":"e_1_3_3_5_2","first-page":"1","article-title":"Stochastic timed automata","volume":"10","author":"Bertrand Nathalie","year":"2014","unstructured":"Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, Marcus Gr\u00f6\u00dfer, and Marcin Jurdzinski. 2014. Stochastic timed automata. Logical Methods in Computer Science 10, 4 (2014), 1\u201373.","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.104"},{"key":"e_1_3_3_7_2","first-page":"340","volume-title":"24th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201918) (LNCS\u201918)","author":"Budde Carlos E.","year":"2018","unstructured":"Carlos E. Budde, Pedro R. D\u2019Argenio, Arnd Hartmanns, and Sean Sedwards. 2018. A statistical model checker for nondeterminism and rare events. In 24th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201918) (LNCS\u201918), Vol. 10806. Springer, 340\u2013358."},{"key":"e_1_3_3_8_2","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1007\/978-3-319-89366-2_21","volume-title":"21st Int. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS\u201918) (LNCS\u201918)","author":"D\u2019Argenio Pedro R.","year":"2018","unstructured":"Pedro R. D\u2019Argenio, Marcus Gerhold, Arnd Hartmanns, and Sean Sedwards. 2018. A hierarchy of scheduler classes for stochastic automata. In 21st Int. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS\u201918) (LNCS\u201918), Vol. 10803. Springer, 384\u2013402."},{"issue":"1","key":"e_1_3_3_9_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ic.2005.07.001","article-title":"A theory of stochastic systems part I: Stochastic automata","volume":"203","author":"D\u2019Argenio Pedro R.","year":"2005","unstructured":"Pedro R. D\u2019Argenio and Joost-Pieter Katoen. 2005. A theory of stochastic systems part I: Stochastic automata. Information and Computation 203, 1 (2005), 1\u201338.","journal-title":"Information and Computation"},{"key":"e_1_3_3_10_2","first-page":"1","volume-title":"17th Int. Symp. on Theoretical Aspects of Software Engineering (LNCS)","author":"Delicaris Joanna","year":"2023","unstructured":"Joanna Delicaris, Stefan Schupp, Erika \u00c1brah\u00e1m, and Anne Remke. 2023. Maximizing reachability probabilities in rectangular automata with random clocks. In 17th Int. Symp. on Theoretical Aspects of Software Engineering (LNCS), Vol. 13931. Springer, 1\u201319."},{"key":"e_1_3_3_11_2","article-title":"Analyse des Travaux de l\u2019acad\u00e9mie Royale des Sciences Pendant l\u2019ann\u00e9e 1824","author":"Fourier Jean Babtiste Joseph","year":"1827","unstructured":"Jean Babtiste Joseph Fourier. 1827. Analyse des Travaux de l\u2019acad\u00e9mie Royale des Sciences Pendant l\u2019ann\u00e9e 1824. Partie Math\u00e9matique (1827).","journal-title":"Partie Math\u00e9matique"},{"key":"e_1_3_3_12_2","first-page":"43","volume-title":"14th ACM Int. Conf. on Hybrid Systems: Computation and Control (HSCC\u201911)","author":"Fr\u00e4nzle Martin","year":"2011","unstructured":"Martin Fr\u00e4nzle, E. Moritz Hahn, Holger Hermanns, Nicol\u00e1s Wolovick, and Lijun Zhang. 2011. Measurability and safety verification for stochastic hybrid systems. In 14th ACM Int. Conf. on Hybrid Systems: Computation and Control (HSCC\u201911). ACM, 43\u201352."},{"key":"e_1_3_3_13_2","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"8th Int. Workshop on Hybrid Systems: Computation and Control (HSCC\u201905) (LNCS\u201905)","author":"Frehse Goran","year":"2005","unstructured":"Goran Frehse. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. In 8th Int. Workshop on Hybrid Systems: Computation and Control (HSCC\u201905) (LNCS\u201905), Vol. 3414. Springer, 258\u2013273."},{"key":"e_1_3_3_14_2","first-page":"165","volume-title":"7th EAI Int. Conf. on Performance Evaluation Methodologies and Tools (VALUETOOLS\u201913)","author":"Ghasemieh Hamed","year":"2013","unstructured":"Hamed Ghasemieh, Anne Remke, and Boudewijn R. Haverkort. 2013. Analysis of a sewage treatment facility using hybrid petri nets. In 7th EAI Int. Conf. on Performance Evaluation Methodologies and Tools (VALUETOOLS\u201913). ICST, 165\u2013174."},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/1538674"},{"key":"e_1_3_3_16_2","article-title":"Reachability and reward checking for stochastic timed automata","volume":"70","author":"Hahn E. Moritz","year":"2014","unstructured":"E. Moritz Hahn, Arnd Hartmanns, and Holger Hermanns. 2014. Reachability and reward checking for stochastic timed automata. Electronic Communiations of the EASST 70 (2014).","journal-title":"Electronic Communiations of the EASST"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0167-z"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59615-5_13"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2005.843874"},{"key":"e_1_3_3_21_2","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/978-3-030-55754-6_22","volume-title":"12th Int. NASA Formal Methods Symp. (NFM\u201920) (LNCS\u201920)","author":"H\u00fcls Jannik","year":"2020","unstructured":"Jannik H\u00fcls, Henner Niehaus, and Anne Remke. 2020. Hpnmg: A C++ tool for model checking hybrid petri nets with general transitions. In 12th Int. NASA Formal Methods Symp. (NFM\u201920) (LNCS\u201920), Vol. 12229. Springer, 369\u2013378."},{"key":"e_1_3_3_22_2","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/978-3-030-30281-8_11","volume-title":"16th Int. Conf. on Quantitative Evaluation of Systems (QEST\u201919) (LNCS\u201919)","author":"H\u00fcls Jannik","year":"2019","unstructured":"Jannik H\u00fcls, Carina Pilch, Patricia Schinke, Joanna Delicaris, and Anne Remke. 2019. State-space construction of hybrid petri nets with multiple stochastic firings. In 16th Int. Conf. on Quantitative Evaluation of Systems (QEST\u201919) (LNCS\u201919), Vol. 11785. Springer, 182\u2013199."},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3449353"},{"key":"e_1_3_3_24_2","volume-title":"10th EAI Int. Conf. on Performance Evaluation Methodologies and Tools (VALUETOOLS\u201916)","author":"H\u00fcls Jannik","year":"2016","unstructured":"Jannik H\u00fcls and Anne Remke. 2016. Coordinated charging strategies for plug-in electric vehicles to ensure a robust charging process. In 10th EAI Int. Conf. on Performance Evaluation Methodologies and Tools (VALUETOOLS\u201916). ICST."},{"key":"e_1_3_3_25_2","first-page":"385","volume-title":"24th IEEE Int. Symp. on Modeling, Analysis and Simulation of Computer and Telecommunication Systems","author":"H\u00fcls Jannik","year":"2016","unstructured":"Jannik H\u00fcls and Anne Remke. 2016. Energy storage in smart homes: Grid-convenience versus self-use and survivability. In 24th IEEE Int. Symp. on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. IEEE, 385\u2013390."},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCA.2007.914777"},{"key":"e_1_3_3_27_2","first-page":"123","volume-title":"11th Int. Conf. on Concurrency Theory (CONCUR\u201900) (LNCS\u201900)","author":"Kwiatkowska Marta Z.","year":"2000","unstructured":"Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. 2000. Verifying quantitative properties of continuous probabilistic timed automata. In 11th Int. Conf. on Concurrency Theory (CONCUR\u201900) (LNCS\u201900), Vol. 1877. Springer, 123\u2013137."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcp.2021.110386"},{"key":"e_1_3_3_29_2","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1017\/CCOL0521340446.006","volume-title":"Advances in Economic Theory","author":"Megiddo Nimrod","year":"1987","unstructured":"Nimrod Megiddo. 1987. On the complexity of linear programming. In Advances in Economic Theory. Cambridge University Press, London, 225\u2013268."},{"key":"e_1_3_3_30_2","volume-title":"Beitrage Zur Theorie Der Linearen Ungleichungen","author":"Motzkin Theodore Samuel","year":"1936","unstructured":"Theodore Samuel Motzkin. 1936. Beitrage Zur Theorie Der Linearen Ungleichungen. Azriel."},{"key":"e_1_3_3_31_2","first-page":"44","volume-title":"19th ACM-IEEE Int. Conf. on Formal Methods and Models for System Design (MEMOCODE\u201921)","author":"Niehage Mathis","year":"2021","unstructured":"Mathis Niehage, Arnd Hartmanns, and Anne Remke. 2021. Learning optimal decisions for stochastic hybrid systems. In 19th ACM-IEEE Int. Conf. on Formal Methods and Models for System Design (MEMOCODE\u201921). ACM, 44\u201355."},{"key":"e_1_3_3_32_2","first-page":"1","volume-title":"23rd ACM Int. Conf. on Hybrid Systems: Computation and Control (HSCC\u201920)","author":"Pilch Carina","year":"2020","unstructured":"Carina Pilch, Arnd Hartmanns, and Anne Remke. 2020. Classic and non-prophetic model checking for hybrid petri nets with stochastic firings. In 23rd ACM Int. Conf. on Hybrid Systems: Computation and Control (HSCC\u201920). ACM, 1\u201311."},{"key":"e_1_3_3_33_2","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/978-3-030-55754-6_23","volume-title":"12th Int. NASA Formal Methods Symp. (NFM\u201920) (LNCS)","author":"Pilch Carina","year":"2020","unstructured":"Carina Pilch, Maurice Krause, Anne Remke, and Erika \u00c1brah\u00e1m. 2020. A transformation of hybrid petri nets with stochastic firings into a subclass of stochastic hybrid automata. In 12th Int. NASA Formal Methods Symp. (NFM\u201920) (LNCS), Vol. 12229. Springer, 381\u2013400."},{"key":"e_1_3_3_34_2","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/978-3-030-85172-9_23","volume-title":"18th Int. Conf. on Quantitative Evaluation of Systems (QEST\u201921) (LNCS)","author":"Pilch Carina","year":"2021","unstructured":"Carina Pilch, Stefan Schupp, and Anne Remke. 2021. Optimizing reachability probabilities for a restricted class of stochastic hybrid automata via flowpipe-construction. In 18th Int. Conf. on Quantitative Evaluation of Systems (QEST\u201921) (LNCS), Vol. 12846. Springer, Cham, 435\u2013456."},{"key":"e_1_3_3_35_2","series-title":"LNCIS","first-page":"107","volume-title":"Stochastic Hybrid Systems: Theory and Safety Critical Applications","author":"Prandini Maria","year":"2006","unstructured":"Maria Prandini and Jianghai Hu. 2006. A stochastic approximation method for reachability computations. In Stochastic Hybrid Systems: Theory and Safety Critical Applications. LNCIS, Vol. 337. Springer, 107\u2013139."},{"key":"e_1_3_3_36_2","volume-title":"State Set Representations and Their Usage in the Reachability Analysis of Hybrid Systems","author":"Schupp Stefan","year":"2019","unstructured":"Stefan Schupp. 2019. State Set Representations and Their Usage in the Reachability Analysis of Hybrid Systems. Dissertation. RWTH Aachen University. http:\/\/publications.rwth-aachen.de\/record\/767529"},{"key":"e_1_3_3_37_2","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/978-3-319-57288-8_20","volume-title":"9th Int. NASA Formal Methods Symp. (NFM\u201917) (LNCS)","author":"Schupp Stefan","year":"2017","unstructured":"Stefan Schupp, Erika \u00c1brah\u00e1m, Ibtissem Ben Makhlouf, and Stefan Kowalewski. 2017. HyPro: A C++ library of state set representations for hybrid systems reachability analysis. In 9th Int. NASA Formal Methods Symp. (NFM\u201917) (LNCS), Vol. 10227. Springer, Cham, 288\u2013294."},{"key":"e_1_3_3_38_2","first-page":"272","volume-title":"21st Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915) (LNCS)","author":"Soudjani Sadegh E. Z.","year":"2015","unstructured":"Sadegh E. Z. Soudjani, Caspar Gevaerts, and Alessandro Abate. 2015. FAUST2: Formal abstractions of uncountable-STate STochastic processes. In 21st Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915) (LNCS), Vol. 9035. Springer, 272\u2013286."},{"key":"e_1_3_3_39_2","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-45352-0_5","volume-title":"6th Int. Symp. on Formal Techniques in Real-time and Fault-tolerant Systems (FTRTFT\u201900) (LNCS)","author":"Sproston Jeremy","year":"2000","unstructured":"Jeremy Sproston. 2000. Decidable model checking of probabilistic hybrid automata. In 6th Int. Symp. on Formal Techniques in Real-time and Fault-tolerant Systems (FTRTFT\u201900) (LNCS), Vol. 1926. Springer, 31\u201345."},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.3166\/EJC.18.572-587"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8431-1"}],"container-title":["ACM Transactions on Modeling and Computer Simulation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607197","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607197","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:34Z","timestamp":1750178254000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607197"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,26]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,10,31]]}},"alternative-id":["10.1145\/3607197"],"URL":"https:\/\/doi.org\/10.1145\/3607197","relation":{},"ISSN":["1049-3301","1558-1195"],"issn-type":[{"type":"print","value":"1049-3301"},{"type":"electronic","value":"1558-1195"}],"subject":[],"published":{"date-parts":[[2023,10,26]]},"assertion":[{"value":"2022-01-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-06-02","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-10-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}