[{"ec_funded":1,"date_updated":"2026-03-09T11:43:38Z","file_date_updated":"2026-03-09T11:39:59Z","citation":{"chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, and Mateusz Ujma. “Learning Algorithms for Verification of Markov Decision Processes.” <i>TheoretiCS</i>. TheoretiCS Foundation, 2025. <a href=\"https://doi.org/10.46298/theoretics.25.10\">https://doi.org/10.46298/theoretics.25.10</a>.","mla":"Brázdil, Tomáš, et al. “Learning Algorithms for Verification of Markov Decision Processes.” <i>TheoretiCS</i>, vol. 4, 10, TheoretiCS Foundation, 2025, doi:<a href=\"https://doi.org/10.46298/theoretics.25.10\">10.46298/theoretics.25.10</a>.","ama":"Brázdil T, Chatterjee K, Chmelik M, et al. Learning algorithms for verification of Markov decision processes. <i>TheoretiCS</i>. 2025;4. doi:<a href=\"https://doi.org/10.46298/theoretics.25.10\">10.46298/theoretics.25.10</a>","ieee":"T. Brázdil <i>et al.</i>, “Learning algorithms for verification of Markov decision processes,” <i>TheoretiCS</i>, vol. 4. TheoretiCS Foundation, 2025.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2025). Learning algorithms for verification of Markov decision processes. <i>TheoretiCS</i>. TheoretiCS Foundation. <a href=\"https://doi.org/10.46298/theoretics.25.10\">https://doi.org/10.46298/theoretics.25.10</a>","ista":"Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Meggendorfer T, Parker D, Ujma M. 2025. Learning algorithms for verification of Markov decision processes. TheoretiCS. 4, 10.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, T. Meggendorfer, D. Parker, M. Ujma, TheoretiCS 4 (2025)."},"article_type":"original","quality_controlled":"1","department":[{"_id":"KrCh"}],"_id":"21413","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"title":"Learning algorithms for verification of Markov decision processes","status":"public","type":"journal_article","month":"04","publisher":"TheoretiCS Foundation","scopus_import":"1","external_id":{"arxiv":["2403.09184"]},"author":[{"last_name":"Brázdil","full_name":"Brázdil, Tomáš","first_name":"Tomáš"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Vojtěch","full_name":"Forejt, Vojtěch","last_name":"Forejt"},{"first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kwiatkowska","first_name":"Marta","full_name":"Kwiatkowska, Marta"},{"last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165"},{"first_name":"David","full_name":"Parker, David","last_name":"Parker"},{"last_name":"Ujma","full_name":"Ujma, Mateusz","first_name":"Mateusz"}],"has_accepted_license":"1","OA_type":"gold","publication_status":"published","publication_identifier":{"eissn":["2751-4838"]},"oa":1,"OA_place":"publisher","language":[{"iso":"eng"}],"day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"checksum":"2ccf563ae577ee08d82baf752292ca7b","creator":"dernst","access_level":"open_access","content_type":"application/pdf","file_name":"2026_TheoretiCS_Brazdil.pdf","date_updated":"2026-03-09T11:39:59Z","file_id":"21417","success":1,"relation":"main_file","file_size":861607,"date_created":"2026-03-09T11:39:59Z"}],"abstract":[{"text":"We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs).\r\nThe primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}zdil et al., significantly extending it as well as refining several details and fixing errors.\r\nThe presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios.\r\nThe first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.","lang":"eng"}],"date_published":"2025-04-01T00:00:00Z","publication":"TheoretiCS","article_processing_charge":"Yes","doi":"10.46298/theoretics.25.10","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement AdG-267989 (QUAREM)*, AdG-246967 (VERIWARE)*, StG-279307 (Graph Games)*\r\n, CoG-863818 (ForM-SMArt), and AdG-834115 (FUN2MODEL), by the EU FP7 project HIERATIC*, by the German Research Foundation (DFG) project 427755713 (GOPro), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE)* , S11407-N23 (RiSE)*\r\n, and P23499-N23* , by the Czech Science Foundation grant No P202/12/P612* and GA23-06963S, by the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant\r\nAgency of Masaryk University, by EPSRC project EP/K038575/1*, and by the Microsoft faculty fellows award*. A preliminary version of this article appeared at ATVA 2014 [33]. The * indicates funding that supported that version.","year":"2025","arxiv":1,"intvolume":"         4","project":[{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"},{"call_identifier":"FWF","grant_number":"S11402-N23","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"}],"DOAJ_listed":"1","ddc":["000"],"volume":4,"oa_version":"Published Version","article_number":"10","PlanS_conform":"1","date_created":"2026-03-08T23:01:46Z"},{"date_created":"2025-03-09T23:01:29Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2410.18293"}],"project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413","call_identifier":"H2020"}],"volume":15530,"oa_version":"Preprint","acknowledgement":"This research was funded in part by the DFG project 427755713 GOPro, the DFG GRK 2428 (ConVeY), the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant Agency of Masaryk University, and the EU under MSCA grant agreement 101034413 (IST-BRIDGE).","year":"2025","arxiv":1,"intvolume":"     15530","abstract":[{"text":"Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs.\r\n\r\nThe idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.","lang":"eng"}],"publication":"26th International Conference on Verification, Model Checking, and Abstract Interpretation","article_processing_charge":"No","date_published":"2025-01-23T00:00:00Z","doi":"10.1007/978-3-031-82703-7_5","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa":1,"OA_place":"repository","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031827020"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"day":"23","external_id":{"isi":["001446577100005"],"arxiv":["2410.18293"]},"scopus_import":"1","author":[{"last_name":"Azeem","first_name":"Muqsit","full_name":"Azeem, Muqsit"},{"first_name":"Debraj","full_name":"Chakraborty, Debraj","last_name":"Chakraborty"},{"last_name":"Kanav","first_name":"Sudeep","full_name":"Kanav, Sudeep"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan"},{"full_name":"Mohagheghi, Mohammadsadegh","first_name":"Mohammadsadegh","last_name":"Mohagheghi"},{"full_name":"Mohr, Stefanie","first_name":"Stefanie","last_name":"Mohr"},{"first_name":"Maximilian","full_name":"Weininger, Maximilian","last_name":"Weininger","id":"02ab0197-cc70-11ed-ab61-918e71f56881"}],"OA_type":"green","publication_status":"published","status":"public","title":"1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization","type":"conference","alternative_title":["LNCS"],"month":"01","publisher":"Springer Nature","isi":1,"_id":"19375","quality_controlled":"1","department":[{"_id":"KrCh"}],"date_updated":"2025-09-30T10:46:54Z","citation":{"short":"M. Azeem, D. Chakraborty, S. Kanav, J. Kretinsky, M. Mohagheghi, S. Mohr, M. Weininger, in:, 26th International Conference on Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2025, pp. 97–120.","ista":"Azeem M, Chakraborty D, Kanav S, Kretinsky J, Mohagheghi M, Mohr S, Weininger M. 2025. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. 26th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 15530, 97–120.","apa":"Azeem, M., Chakraborty, D., Kanav, S., Kretinsky, J., Mohagheghi, M., Mohr, S., &#38; Weininger, M. (2025). 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i> (Vol. 15530, pp. 97–120). Denver, CO, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">https://doi.org/10.1007/978-3-031-82703-7_5</a>","ieee":"M. Azeem <i>et al.</i>, “1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization,” in <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, Denver, CO, United States, 2025, vol. 15530, pp. 97–120.","mla":"Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, vol. 15530, Springer Nature, 2025, pp. 97–120, doi:<a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">10.1007/978-3-031-82703-7_5</a>.","ama":"Azeem M, Chakraborty D, Kanav S, et al. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In: <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>. Vol 15530. Springer Nature; 2025:97-120. doi:<a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">10.1007/978-3-031-82703-7_5</a>","chicago":"Azeem, Muqsit, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh Mohagheghi, Stefanie Mohr, and Maximilian Weininger. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” In <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, 15530:97–120. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">https://doi.org/10.1007/978-3-031-82703-7_5</a>."},"ec_funded":1,"page":"97-120","conference":{"end_date":"2025-01-21","location":"Denver, CO, United States","name":"VMCAI: Verification, Model Checking, and Abstract Interpretation","start_date":"2025-01-20"}},{"_id":"20688","title":"Stopping criteria for value iteration on concurrent stochastic reachability and safety games","status":"public","month":"10","type":"conference","publisher":"IEEE","quality_controlled":"1","department":[{"_id":"KrCh"}],"ec_funded":1,"page":"568-580","conference":{"name":"LICS: Logic in Computer Science","start_date":"2025-06-23","location":"Singapore, Singapore","end_date":"2025-06-26"},"date_updated":"2025-11-26T07:34:19Z","citation":{"ama":"Grobelna M, Kretinsky J, Weininger M. Stopping criteria for value iteration on concurrent stochastic reachability and safety games. In: <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2025:568-580. doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00049\">10.1109/lics65433.2025.00049</a>","mla":"Grobelna, Marta, et al. “Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games.” <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2025, pp. 568–80, doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00049\">10.1109/lics65433.2025.00049</a>.","chicago":"Grobelna, Marta, Jan Kretinsky, and Maximilian Weininger. “Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games.” In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 568–80. IEEE, 2025. <a href=\"https://doi.org/10.1109/lics65433.2025.00049\">https://doi.org/10.1109/lics65433.2025.00049</a>.","short":"M. Grobelna, J. Kretinsky, M. Weininger, in:, 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2025, pp. 568–580.","ista":"Grobelna M, Kretinsky J, Weininger M. 2025. Stopping criteria for value iteration on concurrent stochastic reachability and safety games. 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 568–580.","apa":"Grobelna, M., Kretinsky, J., &#38; Weininger, M. (2025). Stopping criteria for value iteration on concurrent stochastic reachability and safety games. In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 568–580). Singapore, Singapore: IEEE. <a href=\"https://doi.org/10.1109/lics65433.2025.00049\">https://doi.org/10.1109/lics65433.2025.00049</a>","ieee":"M. Grobelna, J. Kretinsky, and M. Weininger, “Stopping criteria for value iteration on concurrent stochastic reachability and safety games,” in <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Singapore, Singapore, 2025, pp. 568–580."},"project":[{"call_identifier":"H2020","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"oa_version":"Preprint","date_created":"2025-11-24T14:23:49Z","corr_author":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2505.21087"}],"abstract":[{"lang":"eng","text":"We consider two-player zero-sum concurrent stochastic games (CSGs) played on graphs with reachability and safety objectives. These include degenerate classes such as Markov decision processes or turn-based stochastic games, which can be solved by linear or quadratic programming; however, in practice, value iteration (VI) outperforms the other approaches and is the most implemented method. Similarly, for CSGs, this practical performance makes VI an attractive alternative to the standard theoretical solution via the existential theory of reals.VI starts with an under-approximation of the sought values for each state and iteratively updates them, traditionally terminating once two consecutive approximations are ϵ-close. However, this stopping criterion lacks guarantees on the precision of the approximation, which is the goal of this work. We provide bounded (a.k.a. interval) VI for CSGs: it complements standard VI with a converging sequence of over-approximations and terminates once the over- and under-approximations are ϵ-close."}],"date_published":"2025-10-09T00:00:00Z","article_processing_charge":"No","publication":"2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science","doi":"10.1109/lics65433.2025.00049","acknowledgement":"This research was funded in part by the German Research Foundation (DFG) project 427755713 GOPro, the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant Agency of Masaryk University, the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 101034413, and the ERC Starting Grant DEUCE (101077178).","year":"2025","arxiv":1,"publication_identifier":{"eisbn":["9798331579005"]},"oa":1,"OA_place":"repository","day":"09","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"arxiv":["2505.21087"]},"scopus_import":"1","author":[{"last_name":"Grobelna","first_name":"Marta","full_name":"Grobelna, Marta"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger","orcid":"0000-0002-0163-2152","id":"02ab0197-cc70-11ed-ab61-918e71f56881"}],"OA_type":"green","publication_status":"published"},{"page":"90-146","citation":{"mla":"Andriushchenko, Roman, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” <i>TOOLympics Challenge 2023</i>, vol. 14550, Springer Nature, 2024, pp. 90–146, doi:<a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">10.1007/978-3-031-67695-6_4</a>.","ama":"Andriushchenko R, Bork A, Budde CE, et al. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In: <i>TOOLympics Challenge 2023</i>. Vol 14550. Springer Nature; 2024:90-146. doi:<a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">10.1007/978-3-031-67695-6_4</a>","chicago":"Andriushchenko, Roman, Alexander Bork, Carlos E. Budde, Milan Češka, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” In <i>TOOLympics Challenge 2023</i>, 14550:90–146. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">https://doi.org/10.1007/978-3-031-67695-6_4</a>.","short":"R. Andriushchenko, A. Bork, C.E. Budde, M. Češka, K. Grover, E.M. Hahn, A. Hartmanns, B. Israelsen, N. Jansen, J. Jeppson, S. Junges, M.A. Köhl, B. Könighofer, J. Kretinsky, T. Meggendorfer, D. Parker, S. Pranger, T. Quatmann, E. Ruijters, L. Taylor, M. Volk, M. Weininger, Z. Zhang, in:, TOOLympics Challenge 2023, Springer Nature, 2024, pp. 90–146.","ista":"Andriushchenko R, Bork A, Budde CE, Češka M, Grover K, Hahn EM, Hartmanns A, Israelsen B, Jansen N, Jeppson J, Junges S, Köhl MA, Könighofer B, Kretinsky J, Meggendorfer T, Parker D, Pranger S, Quatmann T, Ruijters E, Taylor L, Volk M, Weininger M, Zhang Z. 2024. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. TOOLympics Challenge 2023. , LNCS, vol. 14550, 90–146.","apa":"Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E. M., … Zhang, Z. (2024). Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In <i>TOOLympics Challenge 2023</i> (Vol. 14550, pp. 90–146). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">https://doi.org/10.1007/978-3-031-67695-6_4</a>","ieee":"R. Andriushchenko <i>et al.</i>, “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report,” in <i>TOOLympics Challenge 2023</i>, 2024, vol. 14550, pp. 90–146."},"date_updated":"2025-09-08T14:45:11Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","_id":"18600","isi":1,"publisher":"Springer Nature","alternative_title":["LNCS"],"type":"conference","month":"11","title":"Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report","status":"public","OA_type":"green","publication_status":"published","author":[{"full_name":"Andriushchenko, Roman","first_name":"Roman","last_name":"Andriushchenko"},{"full_name":"Bork, Alexander","first_name":"Alexander","last_name":"Bork"},{"last_name":"Budde","first_name":"Carlos E.","full_name":"Budde, Carlos E."},{"last_name":"Češka","full_name":"Češka, Milan","first_name":"Milan"},{"last_name":"Grover","full_name":"Grover, Kush","first_name":"Kush"},{"first_name":"Ernst Moritz","full_name":"Hahn, Ernst Moritz","last_name":"Hahn"},{"full_name":"Hartmanns, Arnd","first_name":"Arnd","last_name":"Hartmanns"},{"last_name":"Israelsen","first_name":"Bryant","full_name":"Israelsen, Bryant"},{"last_name":"Jansen","full_name":"Jansen, Nils","first_name":"Nils"},{"full_name":"Jeppson, Joshua","first_name":"Joshua","last_name":"Jeppson"},{"last_name":"Junges","first_name":"Sebastian","full_name":"Junges, Sebastian"},{"first_name":"Maximilian A.","full_name":"Köhl, Maximilian A.","last_name":"Köhl"},{"last_name":"Könighofer","first_name":"Bettina","full_name":"Könighofer, Bettina"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky"},{"last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165"},{"last_name":"Parker","full_name":"Parker, David","first_name":"David"},{"full_name":"Pranger, Stefan","first_name":"Stefan","last_name":"Pranger"},{"last_name":"Quatmann","first_name":"Tim","full_name":"Quatmann, Tim"},{"full_name":"Ruijters, Enno","first_name":"Enno","last_name":"Ruijters"},{"last_name":"Taylor","full_name":"Taylor, Landon","first_name":"Landon"},{"first_name":"Matthias","full_name":"Volk, Matthias","last_name":"Volk"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","last_name":"Weininger","full_name":"Weininger, Maximilian","first_name":"Maximilian"},{"full_name":"Zhang, Zhen","first_name":"Zhen","last_name":"Zhang"}],"external_id":{"arxiv":["2405.13583"],"isi":["001434957500004"]},"scopus_import":"1","day":"01","language":[{"iso":"eng"}],"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031676949"],"issn":["0302-9743"]},"OA_place":"repository","oa":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","doi":"10.1007/978-3-031-67695-6_4","article_processing_charge":"No","publication":"TOOLympics Challenge 2023","date_published":"2024-11-01T00:00:00Z","abstract":[{"lang":"eng","text":"The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today’s active areas and tomorrow’s challenges in tool-focused research for quantitative verification."}],"arxiv":1,"intvolume":"     14550","year":"2024","acknowledgement":"The authors are ordered alphabetically. This work was supported by DFG RTG 2236/2 (UnRAVeL) and DFG project TRR 248 (CPEC, ID 389792660), by the EU under MSCA grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED), by ERC Starting Grant 101077178 (DEUCE), ERC Consolidator Grant 864075 (CAESAR), and ERC Advanced Grant 834115 (FUN2MODEL), by GAČR grant GA23-06963S (VESCAA), by National Science Foundation grant 1856733, by NextGenerationEU project D53D23008400006 (SMARTITUDE), and by NWO VENI grant 639.021.754.","oa_version":"Preprint","volume":14550,"main_file_link":[{"url":" https://doi.org/10.48550/arXiv.2405.13583","open_access":"1"}],"date_created":"2024-12-01T23:01:53Z"},{"_id":"13967","isi":1,"type":"conference","month":"07","status":"public","title":"Stopping criteria for value iteration on stochastic games with quantitative objectives","publisher":"Institute of Electrical and Electronics Engineers","department":[{"_id":"KrCh"}],"quality_controlled":"1","conference":{"end_date":"2023-06-29","location":"Boston, MA, United States","start_date":"2023-06-26","name":"LICS: Logic in Computer Science"},"date_updated":"2025-07-10T11:50:43Z","citation":{"apa":"Kretinsky, J., Meggendorfer, T., &#38; Weininger, M. (2023). Stopping criteria for value iteration on stochastic games with quantitative objectives. In <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (Vol. 2023). Boston, MA, United States: Institute of Electrical and Electronics Engineers. <a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">https://doi.org/10.1109/LICS56636.2023.10175771</a>","ieee":"J. Kretinsky, T. Meggendorfer, and M. Weininger, “Stopping criteria for value iteration on stochastic games with quantitative objectives,” in <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Boston, MA, United States, 2023, vol. 2023.","short":"J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2023.","ista":"Kretinsky J, Meggendorfer T, Weininger M. 2023. Stopping criteria for value iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2023.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, and Maximilian Weininger. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” In <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Vol. 2023. Institute of Electrical and Electronics Engineers, 2023. <a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">https://doi.org/10.1109/LICS56636.2023.10175771</a>.","ama":"Kretinsky J, Meggendorfer T, Weininger M. Stopping criteria for value iteration on stochastic games with quantitative objectives. In: <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Vol 2023. Institute of Electrical and Electronics Engineers; 2023. doi:<a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">10.1109/LICS56636.2023.10175771</a>","mla":"Kretinsky, Jan, et al. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, vol. 2023, Institute of Electrical and Electronics Engineers, 2023, doi:<a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">10.1109/LICS56636.2023.10175771</a>."},"volume":2023,"oa_version":"Preprint","date_created":"2023-08-06T22:01:10Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2304.09930"}],"corr_author":"1","abstract":[{"text":"A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently. As a consequence, even the most used model checkers could return arbitrarily wrong results. Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, in particular MDP with reachability, total reward, and mean payoff, and SG with reachability.In this paper, we provide the first stopping criteria for VI on SG with total reward and mean payoff, yielding the first anytime algorithms in these settings. To this end, we provide the solution in two flavours: First through a reduction to the MDP case and second directly on SG. The former is simpler and automatically utilizes any advances on MDP. The latter allows for more local computations, heading towards better practical efficiency.Our solution unifies the previously mentioned approaches for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution.","lang":"eng"}],"doi":"10.1109/LICS56636.2023.10175771","article_processing_charge":"No","publication":"38th Annual ACM/IEEE Symposium on Logic in Computer Science","date_published":"2023-07-01T00:00:00Z","acknowledgement":"This research was funded in part by DFG projects 383882557 “SUV” and 427755713 “GOPro”.","intvolume":"      2023","arxiv":1,"year":"2023","language":[{"iso":"eng"}],"day":"01","oa":1,"publication_identifier":{"issn":["1043-6871"],"isbn":["9798350335873"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","last_name":"Weininger","first_name":"Maximilian","full_name":"Weininger, Maximilian"}],"scopus_import":"1","external_id":{"arxiv":["2304.09930"],"isi":["001036707700042"]},"publication_status":"published"},{"department":[{"_id":"KrCh"}],"quality_controlled":"1","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"_id":"14259","isi":1,"publisher":"Springer Nature","alternative_title":["LNCS"],"type":"conference","month":"07","status":"public","title":"Guessing winning policies in LTL synthesis by semantic learning","conference":{"start_date":"2023-07-17","name":"CAV: Computer Aided Verification","location":"Paris, France","end_date":"2023-07-22"},"page":"390-414","citation":{"ieee":"J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning policies in LTL synthesis by semantic learning,” in <i>35th International Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13964, pp. 390–414.","apa":"Kretinsky, J., Meggendorfer, T., Prokop, M., &#38; Rieder, S. (2023). Guessing winning policies in LTL synthesis by semantic learning. In <i>35th International Conference on Computer Aided Verification</i> (Vol. 13964, pp. 390–414). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">https://doi.org/10.1007/978-3-031-37706-8_20</a>","ista":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies in LTL synthesis by semantic learning. 35th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414.","short":"J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 390–414.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In <i>35th International Conference on Computer Aided Verification</i>, 13964:390–414. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">https://doi.org/10.1007/978-3-031-37706-8_20</a>.","ama":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies in LTL synthesis by semantic learning. In: <i>35th International Conference on Computer Aided Verification</i>. Vol 13964. Springer Nature; 2023:390-414. doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">10.1007/978-3-031-37706-8_20</a>","mla":"Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” <i>35th International Conference on Computer Aided Verification</i>, vol. 13964, Springer Nature, 2023, pp. 390–414, doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">10.1007/978-3-031-37706-8_20</a>."},"file_date_updated":"2023-09-06T08:25:50Z","date_updated":"2026-07-07T13:39:23Z","doi":"10.1007/978-3-031-37706-8_20","publication":"35th International Conference on Computer Aided Verification","date_published":"2023-07-17T00:00:00Z","article_processing_charge":"Yes (in subscription journal)","abstract":[{"lang":"eng","text":"We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed strategy be applied as best-effort in cases where the game’s huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn contrast to previous works, we (i) reflect the highly structured logical information in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii) learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning."}],"year":"2023","intvolume":"     13964","acknowledgement":"This research was funded in part by the German Research Foundation (DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).","volume":13964,"oa_version":"Published Version","ddc":["000"],"date_created":"2023-09-03T22:01:16Z","publication_status":"published","has_accepted_license":"1","das_tickbox":"1","author":[{"first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer"},{"last_name":"Prokop","first_name":"Maximilian","full_name":"Prokop, Maximilian"},{"last_name":"Rieder","first_name":"Sabine","full_name":"Rieder, Sabine"}],"external_id":{"isi":["001310786500020"]},"scopus_import":"1","language":[{"iso":"eng"}],"day":"17","oa":1,"publication_identifier":{"isbn":["9783031377051"],"issn":["0302-9743"],"eissn":["1611-3349"]},"file":[{"file_id":"14276","success":1,"relation":"main_file","file_size":428354,"date_created":"2023-09-06T08:25:50Z","checksum":"ed66278b61bb869e1baba3d9b9081271","creator":"dernst","content_type":"application/pdf","access_level":"open_access","file_name":"2023_LNCS_CAV_Kretinsky.pdf","date_updated":"2023-09-06T08:25:50Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"department":[{"_id":"KrCh"}],"quality_controlled":"1","publisher":"Springer Nature","keyword":["computer networks and communications","information systems","software"],"type":"journal_article","month":"10","status":"public","title":"Index appearance record with preorders","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"_id":"10602","isi":1,"citation":{"mla":"Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>, vol. 59, Springer Nature, 2022, pp. 585–618, doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record with preorders. <i>Acta Informatica</i>. 2022;59:585-618. doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>.","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance record with preorders. Acta Informatica. 59, 585–618.","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618.","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record with preorders,” <i>Acta Informatica</i>, vol. 59. Springer Nature, pp. 585–618, 2022.","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2022). Index appearance record with preorders. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>"},"file_date_updated":"2022-01-07T07:50:31Z","date_updated":"2025-04-15T06:53:08Z","page":"585-618","article_type":"original","intvolume":"        59","year":"2022","acknowledgement":"This work is partially funded by the German Research Foundation (DFG) projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification (No. 383882557), and the Alexander von Humboldt Foundation with funds from the German Federal Ministry of Education and Research. It is an extended version of [21], including all proofs together with further explanations and examples. Moreover, we provide a new, more efficient construction based on (total) preorders, unifying previous optimizations. Experiments are performed with a new, performant implementation, comparing our approach to the current state of the art.","doi":"10.1007/s00236-021-00412-y","article_processing_charge":"Yes (via OA deal)","date_published":"2022-10-01T00:00:00Z","publication":"Acta Informatica","abstract":[{"lang":"eng","text":"Transforming ω-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches."}],"corr_author":"1","date_created":"2022-01-06T12:37:27Z","oa_version":"Published Version","volume":59,"ddc":["000"],"project":[{"name":"IST Austria Open Access Fund","_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854"}],"publication_status":"published","has_accepted_license":"1","author":[{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky"},{"orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer"},{"last_name":"Waldmann","first_name":"Clara","full_name":"Waldmann, Clara"},{"last_name":"Weininger","full_name":"Weininger, Maximilian","first_name":"Maximilian"}],"external_id":{"isi":["000735765500001"]},"scopus_import":"1","file":[{"file_name":"2021_ActaInfor_Křetínský.pdf","content_type":"application/pdf","access_level":"open_access","date_updated":"2022-01-07T07:50:31Z","creator":"cchlebak","checksum":"bf1c195b6aaf59e8530cf9e3a9d731f7","date_created":"2022-01-07T07:50:31Z","relation":"main_file","file_size":1066082,"file_id":"10603","success":1}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","language":[{"iso":"eng"}],"day":"01","publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"oa":1},{"year":"2022","arxiv":1,"intvolume":"       243","acknowledgement":"Kush Grover: The author has been supported by the DFG research training group GRK\r\n2428 ConVeY.\r\nMaximilian Weininger: The author has been partially supported by DFG projects 383882557\r\nStatistical Unbounded Verification (SUV) and 427755713 Group-By Objectives in Probabilistic\r\nVerification (GOPro)","doi":"10.4230/LIPIcs.CONCUR.2022.11","article_processing_charge":"No","date_published":"2022-09-15T00:00:00Z","publication":"33rd International Conference on Concurrency Theory","abstract":[{"lang":"eng","text":"We consider the problem of approximating the reachability probabilities in Markov decision processes (MDP) with uncountable (continuous) state and action spaces. While there are algorithms that, for special classes of such MDP, provide a sequence of approximations converging to the true value in the limit, our aim is to obtain an algorithm with guarantees on the precision of the approximation.\r\nAs this problem is undecidable in general, assumptions on the MDP are necessary. Our main contribution is to identify sufficient assumptions that are as weak as possible, thus approaching the \"boundary\" of which systems can be correctly and reliably analyzed. To this end, we also argue why each of our assumptions is necessary for algorithms based on processing finitely many observations.\r\nWe present two solution variants. The first one provides converging lower bounds under weaker assumptions than typical ones from previous works concerned with guarantees. The second one then utilizes stronger assumptions to additionally provide converging upper bounds. Altogether, we obtain an anytime algorithm, i.e. yielding a sequence of approximants with known and iteratively improving precision, converging to the true value in the limit. Besides, due to the generality of our assumptions, our algorithms are very general templates, readily allowing for various heuristics from literature in contrast to, e.g., a specific discretization algorithm. Our theoretical contribution thus paves the way for future practical improvements without sacrificing correctness guarantees."}],"corr_author":"1","date_created":"2023-03-28T08:09:32Z","article_number":"11","volume":243,"oa_version":"Published Version","ddc":["000"],"publication_status":"published","has_accepted_license":"1","das_tickbox":"1","author":[{"full_name":"Grover, Kush","first_name":"Kush","last_name":"Grover"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"full_name":"Weininger, Maimilian","first_name":"Maimilian","last_name":"Weininger"}],"external_id":{"arxiv":["2008.04824"]},"scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"checksum":"e282e43d3ae0ba6e067b72f4583e13c0","access_level":"open_access","content_type":"application/pdf","file_name":"2022_LIPIcS_Grover.pdf","date_updated":"2023-09-26T10:43:15Z","creator":"dernst","file_id":"14372","success":1,"date_created":"2023-09-26T10:43:15Z","relation":"main_file","file_size":960036}],"day":"15","language":[{"iso":"eng"}],"oa":1,"publication_identifier":{"issn":["1868-8969"]},"department":[{"_id":"KrCh"}],"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","alternative_title":["LIPIcs"],"type":"conference","month":"09","status":"public","title":"Anytime guarantees for reachability in uncountable Markov decision processes","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"_id":"12775","citation":{"mla":"Grover, Kush, et al. “Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.” <i>33rd International Conference on Concurrency Theory</i>, vol. 243, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2022.11\">10.4230/LIPIcs.CONCUR.2022.11</a>.","ama":"Grover K, Kretinsky J, Meggendorfer T, Weininger M. Anytime guarantees for reachability in uncountable Markov decision processes. In: <i>33rd International Conference on Concurrency Theory</i>. Vol 243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2022.11\">10.4230/LIPIcs.CONCUR.2022.11</a>","chicago":"Grover, Kush, Jan Kretinsky, Tobias Meggendorfer, and Maimilian Weininger. “Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.” In <i>33rd International Conference on Concurrency Theory</i>, Vol. 243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2022.11\">https://doi.org/10.4230/LIPIcs.CONCUR.2022.11</a>.","short":"K. Grover, J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 33rd International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.","ista":"Grover K, Kretinsky J, Meggendorfer T, Weininger M. 2022. Anytime guarantees for reachability in uncountable Markov decision processes. 33rd International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 243, 11.","apa":"Grover, K., Kretinsky, J., Meggendorfer, T., &#38; Weininger, M. (2022). Anytime guarantees for reachability in uncountable Markov decision processes. In <i>33rd International Conference on Concurrency Theory</i> (Vol. 243). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2022.11\">https://doi.org/10.4230/LIPIcs.CONCUR.2022.11</a>","ieee":"K. Grover, J. Kretinsky, T. Meggendorfer, and M. Weininger, “Anytime guarantees for reachability in uncountable Markov decision processes,” in <i>33rd International Conference on Concurrency Theory</i>, Warsaw, Poland, 2022, vol. 243."},"file_date_updated":"2023-09-26T10:43:15Z","date_updated":"2026-07-07T13:37:58Z","conference":{"name":"CONCUR: Conference on Concurrency Theory","start_date":"2022-09-13","end_date":"2022-09-16","location":"Warsaw, Poland"}},{"alternative_title":["LNCS"],"month":"04","type":"conference","status":"public","title":"Strategy representation by decision trees in reactive synthesis","publisher":"Springer","_id":"297","isi":1,"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","date_updated":"2025-03-31T16:01:11Z","citation":{"ieee":"T. Brázdil, K. Chatterjee, J. Kretinsky, and V. Toman, “Strategy representation by decision trees in reactive synthesis,” presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece, 2018, vol. 10805, pp. 385–407.","apa":"Brázdil, T., Chatterjee, K., Kretinsky, J., &#38; Toman, V. (2018). Strategy representation by decision trees in reactive synthesis (Vol. 10805, pp. 385–407). Presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece: Springer. <a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">https://doi.org/10.1007/978-3-319-89960-2_21</a>","ista":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. 2018. Strategy representation by decision trees in reactive synthesis. TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10805, 385–407.","short":"T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp. 385–407.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Jan Kretinsky, and Viktor Toman. “Strategy Representation by Decision Trees in Reactive Synthesis,” 10805:385–407. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">https://doi.org/10.1007/978-3-319-89960-2_21</a>.","mla":"Brázdil, Tomáš, et al. <i>Strategy Representation by Decision Trees in Reactive Synthesis</i>. Vol. 10805, Springer, 2018, pp. 385–407, doi:<a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">10.1007/978-3-319-89960-2_21</a>.","ama":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. Strategy representation by decision trees in reactive synthesis. In: Vol 10805. Springer; 2018:385-407. doi:<a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">10.1007/978-3-319-89960-2_21</a>"},"file_date_updated":"2020-07-14T12:45:57Z","page":"385 - 407","ec_funded":1,"conference":{"start_date":"2018-04-14","name":"TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems","location":"Thessaloniki, Greece","end_date":"2018-04-20"},"date_created":"2018-12-11T11:45:41Z","ddc":["000"],"project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","call_identifier":"H2020"}],"volume":10805,"oa_version":"Published Version","intvolume":"     10805","year":"2018","abstract":[{"lang":"eng","text":"Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with ω -regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs."}],"doi":"10.1007/978-3-319-89960-2_21","date_published":"2018-04-12T00:00:00Z","article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"file_id":"5723","date_created":"2018-12-17T16:29:08Z","file_size":1829940,"relation":"main_file","checksum":"b13874ffb114932ad9cc2586b7469db4","date_updated":"2020-07-14T12:45:57Z","access_level":"open_access","content_type":"application/pdf","file_name":"2018_LNCS_Brazdil.pdf","creator":"dernst"}],"language":[{"iso":"eng"}],"day":"12","oa":1,"author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan"},{"orcid":"0000-0001-9036-063X","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor","full_name":"Toman, Viktor","last_name":"Toman"}],"scopus_import":"1","external_id":{"isi":["000546326300021"]},"publication_status":"published","has_accepted_license":"1","publist_id":"7584"},{"date_updated":"2025-09-18T10:42:48Z","citation":{"chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 10205:443–60. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">https://doi.org/10.1007/978-3-662-54577-5_26</a>.","mla":"Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 10205, Springer, 2017, pp. 443–60, doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">10.1007/978-3-662-54577-5_26</a>.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record for transforming Rabin automata into parity automata. In: <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 10205. Springer; 2017:443-460. doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">10.1007/978-3-662-54577-5_26</a>","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record for transforming Rabin automata into parity automata,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Uppsala, Sweden, 2017, vol. 10205, pp. 443–460.","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2017). Index appearance record for transforming Rabin automata into parity automata. In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 10205, pp. 443–460). Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">https://doi.org/10.1007/978-3-662-54577-5_26</a>","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance record for transforming Rabin automata into parity automata. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460."},"page":"443-460","conference":{"start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Uppsala, Sweden","end_date":"2017-04-29"},"department":[{"_id":"KrCh"}],"quality_controlled":"1","alternative_title":["LNCS"],"month":"03","type":"conference","status":"public","title":"Index appearance record for transforming Rabin automata into parity automata","publisher":"Springer","_id":"13160","isi":1,"author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan"},{"last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165"},{"last_name":"Waldmann","full_name":"Waldmann, Clara","first_name":"Clara"},{"last_name":"Weininger","first_name":"Maximilian","full_name":"Weininger, Maximilian"}],"external_id":{"arxiv":["1701.05738"],"isi":["000440734900026"]},"publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"day":"31","oa":1,"publication_identifier":{"isbn":["9783662545768"],"issn":["0302-9743"],"eisbn":["9783662545775"],"eissn":["1611-3349"]},"acknowledgement":"This work is partially funded by the DFG project “Verified Model Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.","arxiv":1,"intvolume":"     10205","year":"2017","abstract":[{"lang":"eng","text":"Transforming deterministic ω\r\n-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae."}],"doi":"10.1007/978-3-662-54577-5_26","publication":"Tools and Algorithms for the Construction and Analysis of Systems","article_processing_charge":"No","date_published":"2017-03-31T00:00:00Z","date_created":"2023-06-21T13:21:14Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.1701.05738","open_access":"1"}],"corr_author":"1","volume":10205,"oa_version":"Preprint"},{"publist_id":"5800","external_id":{"arxiv":["1410.5387"],"isi":["000390637000014"]},"scopus_import":"1","author":[{"last_name":"Svoreňová","full_name":"Svoreňová, Mária","first_name":"Mária"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Cěrná, Ivana","first_name":"Ivana","last_name":"Cěrná"},{"full_name":"Belta, Cǎlin","first_name":"Cǎlin","last_name":"Belta"}],"publication_status":"published","oa":1,"language":[{"iso":"eng"}],"day":"01","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","abstract":[{"lang":"eng","text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study."}],"article_processing_charge":"No","publication":"Nonlinear Analysis: Hybrid Systems","date_published":"2017-02-01T00:00:00Z","doi":"10.1016/j.nahs.2016.04.006","year":"2017","intvolume":"        23","arxiv":1,"project":[{"name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"oa_version":"Preprint","volume":23,"date_created":"2018-12-11T11:51:50Z","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"ec_funded":1,"page":"230 - 253","date_updated":"2025-06-11T06:33:00Z","citation":{"chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>.","ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23(2):230-253. doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>.","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2. Elsevier, pp. 230–253, 2017.","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253."},"issue":"2","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"related_material":{"record":[{"id":"1689","relation":"earlier_version","status":"public"}]},"isi":1,"_id":"1407","status":"public","title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","type":"journal_article","month":"02","publisher":"Elsevier"},{"publist_id":"7349","external_id":{"arxiv":["1504.05739"],"isi":["000405208400005"]},"scopus_import":"1","author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan"},{"orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","first_name":"Tatjana","full_name":"Petrov, Tatjana","last_name":"Petrov"}],"publication_status":"published","publication_identifier":{"issn":["1529-3785"]},"oa":1,"language":[{"iso":"eng"}],"day":"01","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","abstract":[{"lang":"eng","text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds. "}],"publication":"ACM Transactions on Computational Logic","article_processing_charge":"No","date_published":"2017-05-01T00:00:00Z","doi":"10.1145/3060139","intvolume":"        18","arxiv":1,"year":"2017","project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF"},{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems"},{"name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734"}],"oa_version":"Submitted Version","volume":18,"article_number":"12","date_created":"2018-12-11T11:46:39Z","main_file_link":[{"url":"https://arxiv.org/abs/1504.05739","open_access":"1"}],"corr_author":"1","ec_funded":1,"date_updated":"2025-09-22T09:21:16Z","citation":{"apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2017). Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic</i>. ACM. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” <i>ACM Transactions on Computational Logic</i>, vol. 18, no. 2. ACM, 2017.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic 18 (2017).","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic. 18(2), 12.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic</i>. 2017;18(2). doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>","mla":"Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic</i>, vol. 18, no. 2, 12, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>."},"issue":"2","quality_controlled":"1","department":[{"_id":"ToHe"}],"related_material":{"record":[{"relation":"earlier_version","id":"1234","status":"public"}]},"isi":1,"_id":"471","title":"Faster statistical model checking for unbounded temporal properties","status":"public","type":"journal_article","month":"05","publisher":"ACM"},{"main_file_link":[{"url":"https://arxiv.org/abs/1705.02326","open_access":"1"}],"date_created":"2018-12-11T11:47:41Z","volume":10426,"oa_version":"Submitted Version","project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"}],"intvolume":"     10426","arxiv":1,"year":"2017","date_published":"2017-07-13T00:00:00Z","article_processing_charge":"No","doi":"10.1007/978-3-319-63387-9_10","abstract":[{"text":"Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalism for expressing long term performance. Value iteration (VI) is one of the simplest and most efficient algorithmic approaches to MDPs with other properties, such as reachability objectives. Unfortunately, a naive extension of VI does not work for MDPs with long-run average rewards, as there is no known stopping criterion. In this work our contributions are threefold. (1) We refute a conjecture related to stopping criteria for MDPs with long-run average rewards. (2) We present two practical algorithms for MDPs with long-run average rewards based on VI. First, we show that a combination of applying VI locally for each maximal end-component (MEC) and VI for reachability objectives can provide approximation guarantees. Second, extending the above approach with a simulation-guided on-demand variant of VI, we present an anytime algorithm that is able to deal with very large models. (3) Finally, we present experimental results showing that our methods significantly outperform the standard approaches on several benchmarks.","lang":"eng"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_identifier":{"isbn":["978-331963386-2"]},"oa":1,"language":[{"iso":"eng"}],"day":"13","publication_status":"published","scopus_import":"1","external_id":{"isi":["000432196400010"],"arxiv":["1705.02326"]},"author":[{"first_name":"Pranav","full_name":"Ashok, Pranav","last_name":"Ashok"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Tobias","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer"}],"publist_id":"7135","publisher":"Springer","status":"public","title":"Value iteration for long run average reward in markov decision processes","type":"conference","month":"07","alternative_title":["LNCS"],"isi":1,"_id":"645","quality_controlled":"1","department":[{"_id":"KrCh"}],"editor":[{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"},{"full_name":"Kunčak, Viktor","first_name":"Viktor","last_name":"Kunčak"}],"citation":{"ista":"Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. 2017. Value iteration for long run average reward in markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 10426, 201–221.","short":"P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.","ieee":"P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, and T. Meggendorfer, “Value iteration for long run average reward in markov decision processes,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426, pp. 201–221.","apa":"Ashok, P., Chatterjee, K., Daca, P., Kretinsky, J., &#38; Meggendorfer, T. (2017). Value iteration for long run average reward in markov decision processes. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10426, pp. 201–221). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63387-9_10\">https://doi.org/10.1007/978-3-319-63387-9_10</a>","mla":"Ashok, Pranav, et al. <i>Value Iteration for Long Run Average Reward in Markov Decision Processes</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 201–21, doi:<a href=\"https://doi.org/10.1007/978-3-319-63387-9_10\">10.1007/978-3-319-63387-9_10</a>.","ama":"Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. Value iteration for long run average reward in markov decision processes. In: Majumdar R, Kunčak V, eds. Vol 10426. Springer; 2017:201-221. doi:<a href=\"https://doi.org/10.1007/978-3-319-63387-9_10\">10.1007/978-3-319-63387-9_10</a>","chicago":"Ashok, Pranav, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretinsky, and Tobias Meggendorfer. “Value Iteration for Long Run Average Reward in Markov Decision Processes.” edited by Rupak Majumdar and Viktor Kunčak, 10426:201–21. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63387-9_10\">https://doi.org/10.1007/978-3-319-63387-9_10</a>."},"date_updated":"2025-09-11T07:18:04Z","conference":{"location":"Heidelberg, Germany","end_date":"2017-07-28","name":"CAV: Computer Aided Verification","start_date":"2017-07-24"},"ec_funded":1,"page":"201 - 221"},{"license":"https://creativecommons.org/licenses/by-nd/4.0/","ec_funded":1,"file_date_updated":"2020-07-14T12:46:33Z","citation":{"chicago":"Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">https://doi.org/10.23638/LMCS-13(2:15)2017</a>.","mla":"Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 2, 15, International Federation for Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">10.23638/LMCS-13(2:15)2017</a>.","ama":"Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. <i>Logical Methods in Computer Science</i>. 2017;13(2). doi:<a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">10.23638/LMCS-13(2:15)2017</a>","apa":"Chatterjee, K., Křetínská, Z., &#38; Kretinsky, J. (2017). Unifying two views on multiple mean-payoff objectives in Markov decision processes. <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">https://doi.org/10.23638/LMCS-13(2:15)2017</a>","ieee":"K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 2. International Federation for Computational Logic, 2017.","short":"K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science 13 (2017).","ista":"Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 13(2), 15."},"date_updated":"2026-07-06T13:26:27Z","issue":"2","quality_controlled":"1","related_material":{"record":[{"status":"public","id":"5429","relation":"earlier_version"},{"relation":"earlier_version","id":"5435","status":"public"},{"status":"public","id":"1657","relation":"earlier_version"}]},"department":[{"_id":"KrCh"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","short":"CC BY-ND (4.0)","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png"},"isi":1,"_id":"466","publisher":"International Federation for Computational Logic","status":"public","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","type":"journal_article","month":"07","publist_id":"7355","das_tickbox":"1","has_accepted_license":"1","publication_status":"published","external_id":{"isi":["000419160800002"]},"scopus_import":"1","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Křetínská, Zuzana","first_name":"Zuzana","last_name":"Křetínská"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"}],"oa":1,"publication_identifier":{"issn":["1860-5974"]},"language":[{"iso":"eng"}],"day":"03","pubrep_id":"957","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"system","content_type":"application/pdf","access_level":"open_access","file_name":"IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf","date_updated":"2020-07-14T12:46:33Z","checksum":"bfa405385ec6229ad5ead89ab5751639","relation":"main_file","file_size":511832,"date_created":"2018-12-12T10:18:32Z","file_id":"5354"}],"article_processing_charge":"No","publication":"Logical Methods in Computer Science","date_published":"2017-07-03T00:00:00Z","doi":"10.23638/LMCS-13(2:15)2017","abstract":[{"text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. ","lang":"eng"}],"intvolume":"        13","year":"2017","volume":13,"oa_version":"Published Version","article_number":"15","project":[{"call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"_id":"2590DB08-B435-11E9-9278-68D0E5697425","name":"Atomic Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes","grant_number":"701309","call_identifier":"H2020"}],"ddc":["004"],"corr_author":"1","date_created":"2018-12-11T11:46:38Z"},{"related_material":{"record":[{"relation":"dissertation_contains","id":"1155","status":"public"}]},"department":[{"_id":"ToHe"},{"_id":"KrCh"},{"_id":"CaGu"}],"quality_controlled":"1","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"_id":"1093","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","type":"conference","month":"08","alternative_title":["LIPIcs"],"status":"public","title":"Linear distances between Markov chains","conference":{"location":"Quebec City; Canada","end_date":"2016-08-26","name":"CONCUR: Concurrency Theory","start_date":"2016-08-23"},"ec_funded":1,"citation":{"chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>","mla":"Daca, Przemyslaw, et al. <i>Linear Distances between Markov Chains</i>. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City; Canada, 2016, vol. 59.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Linear distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016."},"file_date_updated":"2018-12-12T10:11:39Z","date_updated":"2026-04-15T10:02:12Z","doi":"10.4230/LIPIcs.CONCUR.2016.20","date_published":"2016-08-01T00:00:00Z","abstract":[{"lang":"eng","text":"We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. "}],"intvolume":"        59","year":"2016","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF) under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award), by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced Postdoc. Mobility Fellowship – grant number P300P2_161067.","article_number":"20","oa_version":"Published Version","volume":59,"ddc":["004"],"project":[{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","grant_number":"Z211"}],"date_created":"2018-12-11T11:50:06Z","publist_id":"6283","publication_status":"published","has_accepted_license":"1","author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"last_name":"Petrov","full_name":"Petrov, Tatjana","first_name":"Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905"}],"scopus_import":1,"language":[{"iso":"eng"}],"day":"01","oa":1,"pubrep_id":"794","file":[{"file_id":"4895","file_size":501827,"relation":"main_file","date_created":"2018-12-12T10:11:39Z","creator":"system","date_updated":"2018-12-12T10:11:39Z","access_level":"open_access","file_name":"IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf","content_type":"application/pdf"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"publist_id":"6099","publication_status":"published","external_id":{"arxiv":["1504.05739"],"isi":["000406428000007"]},"scopus_import":"1","author":[{"full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905","last_name":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana"}],"oa":1,"language":[{"iso":"eng"}],"day":"01","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2016-01-01T00:00:00Z","article_processing_charge":"No","doi":"10.1007/978-3-662-49674-9_7","abstract":[{"text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.","lang":"eng"}],"intvolume":"      9636","arxiv":1,"year":"2016","acknowledgement":"This research was funded in part by the European Research Council (ERC) under\r\ngrant  agreement  267989  (QUAREM),  the  Austrian  Science  Fund  (FWF)  under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation under grant agreement P202/12/G061.","volume":9636,"oa_version":"Preprint","project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"grant_number":"Z211","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.05739"}],"date_created":"2018-12-11T11:50:51Z","conference":{"end_date":"2016-04-08","location":"Eindhoven, The Netherlands","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2016-04-02"},"ec_funded":1,"page":"112 - 129","citation":{"ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model checking for unbounded temporal properties. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp. 112–129.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands, 2016, vol. 9636, pp. 112–129.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Faster statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">https://doi.org/10.1007/978-3-662-49674-9_7</a>","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:<a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">10.1007/978-3-662-49674-9_7</a>","mla":"Daca, Przemyslaw, et al. <i>Faster Statistical Model Checking for Unbounded Temporal Properties</i>. Vol. 9636, Springer, 2016, pp. 112–29, doi:<a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">10.1007/978-3-662-49674-9_7</a>.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">https://doi.org/10.1007/978-3-662-49674-9_7</a>."},"date_updated":"2026-04-15T10:02:12Z","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"related_material":{"record":[{"status":"public","id":"471","relation":"later_version"},{"status":"public","id":"1155","relation":"dissertation_contains"}]},"isi":1,"_id":"1234","publisher":"Springer","status":"public","title":"Faster statistical model checking for unbounded temporal properties","type":"conference","month":"01","alternative_title":["LNCS"]},{"publist_id":"5680","publication_status":"published","has_accepted_license":"1","author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan"},{"full_name":"Larsen, Kim","first_name":"Kim","last_name":"Larsen"},{"last_name":"Laursen","first_name":"Simon","full_name":"Laursen, Simon"},{"first_name":"Jiří","full_name":"Srba, Jiří","last_name":"Srba"}],"scopus_import":1,"day":"01","language":[{"iso":"eng"}],"oa":1,"pubrep_id":"498","file":[{"file_id":"4672","date_created":"2018-12-12T10:08:12Z","relation":"main_file","file_size":623563,"checksum":"49eb5021caafaabe5356c65b9c5f8c9c","content_type":"application/pdf","access_level":"open_access","file_name":"IST-2016-498-v1+1_32.pdf","date_updated":"2020-07-14T12:44:58Z","creator":"system"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.4230/LIPIcs.CONCUR.2015.142","date_published":"2015-01-01T00:00:00Z","abstract":[{"text":"We consider weighted automata with both positive and negative integer weights on edges and\r\nstudy the problem of synchronization using adaptive strategies that may only observe whether\r\nthe current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata.","lang":"eng"}],"year":"2015","intvolume":"        42","acknowledgement":"The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement 601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM), the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Czech Science Foundation under grant agreement P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734.","oa_version":"Published Version","volume":42,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989"},{"call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7"}],"ddc":["000","003"],"date_created":"2018-12-11T11:52:22Z","conference":{"end_date":"2015-09-04","location":"Madrid, Spain","name":"CONCUR: Concurrency Theory","start_date":"2015-09-01"},"page":"142 - 154","ec_funded":1,"citation":{"ieee":"J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability of weighted synchronization under partial observability,” presented at the CONCUR: Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.","apa":"Kretinsky, J., Larsen, K., Laursen, S., &#38; Srba, J. (2015). Polynomial time decidability of weighted synchronization under partial observability (Vol. 42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>","ista":"Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability of weighted synchronization under partial observability. CONCUR: Concurrency Theory, LIPIcs, vol. 42, 142–154.","short":"J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–154.","chicago":"Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time Decidability of Weighted Synchronization under Partial Observability,” 42:142–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>.","mla":"Kretinsky, Jan, et al. <i>Polynomial Time Decidability of Weighted Synchronization under Partial Observability</i>. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>.","ama":"Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2015:142-154. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>"},"file_date_updated":"2020-07-14T12:44:58Z","date_updated":"2025-04-15T06:26:02Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"quality_controlled":"1","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"_id":"1499","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","month":"01","type":"conference","alternative_title":["LIPIcs"],"title":"Polynomial time decidability of weighted synchronization under partial observability","status":"public"},{"conference":{"end_date":"2015-05-08","location":"Montreal, QC, Canada","start_date":"2015-05-04","name":"CBSE: Component-Based Software Engineering "},"page":"101 - 110","ec_funded":1,"citation":{"apa":"Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Nickovic, D. (2015). Complete composition operators for IOCO-testing theory (pp. 101–110). Presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>","ieee":"N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.","short":"N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 101–110.","ista":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition operators for IOCO-testing theory. CBSE: Component-Based Software Engineering , Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering , , 101–110.","chicago":"Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10. ACM, 2015. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>.","mla":"Beneš, Nikola, et al. <i>Complete Composition Operators for IOCO-Testing Theory</i>. ACM, 2015, pp. 101–10, doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>.","ama":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>"},"file_date_updated":"2020-07-14T12:44:59Z","date_updated":"2026-04-15T10:02:12Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"related_material":{"record":[{"status":"public","id":"1155","relation":"dissertation_contains"}]},"quality_controlled":"1","_id":"1502","isi":1,"publisher":"ACM","type":"conference","alternative_title":["Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering "],"month":"05","status":"public","title":"Complete composition operators for IOCO-testing theory","publist_id":"5676","publication_status":"published","has_accepted_license":"1","author":[{"last_name":"Beneš","first_name":"Nikola","full_name":"Beneš, Nikola"},{"full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","last_name":"Nickovic"}],"external_id":{"isi":["000380554800013"]},"scopus_import":"1","day":"01","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-1-4503-3471-6"]},"oa":1,"file":[{"checksum":"c6ce681035c163a158751f240cb7d389","date_updated":"2020-07-14T12:44:59Z","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf","creator":"system","file_id":"5303","date_created":"2018-12-12T10:17:46Z","file_size":467561,"relation":"main_file"}],"pubrep_id":"625","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","doi":"10.1145/2737166.2737175","article_processing_charge":"No","date_published":"2015-05-01T00:00:00Z","abstract":[{"lang":"eng","text":"We extend the theory of input-output conformance with operators for merge and quotient. The former is useful when testing against multiple requirements or views. The latter can be used to generate tests for patches of an already tested system. Both operators can combine systems with different action alphabets, which is usually the case when constructing complex systems and specifications from parts, for instance different views as well as newly defined functionality of a~previous version of the system."}],"year":"2015","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23(RiSE) and Z211-N23 (Wittgestein Award), by People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373 (nSafeCer).  Jan Křetínský has been partially supported by the Czech Science Foundation, grant No.  P202/12/G061.  Nikola Beneš has been supported by the\r\nMEYS project No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for Scientific Excellence.","oa_version":"Submitted Version","ddc":["000"],"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF"},{"call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"date_created":"2018-12-11T11:52:24Z"},{"language":[{"iso":"eng"}],"day":"22","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publist_id":"5577","publication_status":"published","scopus_import":"1","external_id":{"isi":["000375574900012"]},"author":[{"last_name":"Forejt","first_name":"Vojtěch","full_name":"Forejt, Vojtěch"},{"first_name":"Jan","full_name":"Krčál, Jan","last_name":"Krčál"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan"}],"oa_version":"None","volume":9450,"project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"date_created":"2018-12-11T11:52:55Z","date_published":"2015-11-22T00:00:00Z","article_processing_charge":"No","doi":"10.1007/978-3-662-48899-7_12","abstract":[{"lang":"eng","text":"Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata."}],"year":"2015","intvolume":"      9450","acknowledgement":"This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE), and by the ERC Start Grant (279307: Graph Games).\r\n","conference":{"end_date":"2015-11-28","location":"Suva, Fiji","name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","start_date":"2015-11-24"},"ec_funded":1,"page":"162 - 177","citation":{"apa":"Forejt, V., Krčál, J., &#38; Kretinsky, J. (2015). Controller synthesis for MDPs and frequency LTL\\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>","ieee":"V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and frequency LTL\\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.","short":"V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.","ista":"Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency LTL\\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 9450, 162–177.","chicago":"Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for MDPs and Frequency LTL\\GU,” 9450:162–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>.","ama":"Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\\GU. In: Vol 9450. Springer; 2015:162-177. doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>","mla":"Forejt, Vojtěch, et al. <i>Controller Synthesis for MDPs and Frequency LTL\\GU</i>. Vol. 9450, Springer, 2015, pp. 162–77, doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>."},"date_updated":"2025-09-23T08:21:59Z","isi":1,"_id":"1594","publisher":"Springer","status":"public","title":"Controller synthesis for MDPs and frequency LTL\\GU","type":"conference","alternative_title":["LNCS"],"month":"11","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}]},{"oa":1,"day":"16","language":[{"iso":"eng"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file":[{"checksum":"5885236fa88a439baba9ac6f3e801e93","creator":"dernst","access_level":"open_access","file_name":"2015_CAV_Babiak.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:45:04Z","file_id":"7850","relation":"main_file","file_size":1651779,"date_created":"2020-05-15T08:38:12Z"}],"publist_id":"5566","scopus_import":"1","external_id":{"isi":["000364182900031"]},"author":[{"last_name":"Babiak","first_name":"Tomáš","full_name":"Babiak, Tomáš"},{"last_name":"Blahoudek","full_name":"Blahoudek, František","first_name":"František"},{"full_name":"Duret Lutz, Alexandre","first_name":"Alexandre","last_name":"Duret Lutz"},{"last_name":"Klein","first_name":"Joachim","full_name":"Klein, Joachim"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"full_name":"Mueller, Daniel","first_name":"Daniel","last_name":"Mueller"},{"first_name":"David","full_name":"Parker, David","last_name":"Parker"},{"full_name":"Strejček, Jan","first_name":"Jan","last_name":"Strejček"}],"has_accepted_license":"1","publication_status":"published","project":[{"grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"}],"ddc":["000"],"oa_version":"Submitted Version","volume":9206,"date_created":"2018-12-11T11:52:57Z","abstract":[{"lang":"eng","text":"We propose a flexible exchange format for ω-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata."}],"article_processing_charge":"No","date_published":"2015-07-16T00:00:00Z","doi":"10.1007/978-3-319-21690-4_31","intvolume":"      9206","year":"2015","ec_funded":1,"page":"479 - 486","conference":{"start_date":"2015-07-18","name":"CAV: Computer Aided Verification","location":"San Francisco, CA, United States","end_date":"2015-07-24"},"date_updated":"2025-09-23T13:50:55Z","file_date_updated":"2020-07-14T12:45:04Z","citation":{"short":"T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller, D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486.","ista":"Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification, LNCS, vol. 9206, 479–486.","apa":"Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller, D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>","ieee":"T. Babiak <i>et al.</i>, “The Hanoi omega-automata format,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 479–486.","mla":"Babiak, Tomáš, et al. <i>The Hanoi Omega-Automata Format</i>. Vol. 9206, Springer, 2015, pp. 479–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>.","ama":"Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format. In: Vol 9206. Springer; 2015:479-486. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>","chicago":"Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein, Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata Format,” 9206:479–86. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>."},"isi":1,"_id":"1601","status":"public","title":"The Hanoi omega-automata format","type":"conference","alternative_title":["LNCS"],"month":"07","publisher":"Springer","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}]}]