[{"has_accepted_license":"1","citation":{"ama":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In: <i>35th International Conference on Computer Aided Verification</i>. Vol 13966. Springer Nature; 2023:3-15. doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">10.1007/978-3-031-37709-9_1</a>","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, in:, 35th International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 3–15.","ieee":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties,” in <i>35th International Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13966, pp. 3–15.","ista":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 35th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 3–15.","apa":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., &#38; Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In <i>35th International Conference on Computer Aided Verification</i> (Vol. 13966, pp. 3–15). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">https://doi.org/10.1007/978-3-031-37709-9_1</a>","mla":"Majumdar, Rupak, et al. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” <i>35th International Conference on Computer Aided Verification</i>, vol. 13966, Springer Nature, 2023, pp. 3–15, doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">10.1007/978-3-031-37709-9_1</a>.","chicago":"Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” In <i>35th International Conference on Computer Aided Verification</i>, 13966:3–15. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">https://doi.org/10.1007/978-3-031-37709-9_1</a>."},"related_material":{"record":[{"id":"14994","status":"public","relation":"research_data"}]},"title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","isi":1,"acknowledgement":"Authors ordered alphabetically. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248-CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. M. Rychlicki is supported by the EPSRC project EP/V00252X/1. S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047.","scopus_import":"1","oa_version":"Published Version","_id":"14758","corr_author":"1","article_processing_charge":"Yes (in subscription journal)","author":[{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"},{"first_name":"Kaushik","last_name":"Mallik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"full_name":"Rychlicki, Mateusz","last_name":"Rychlicki","first_name":"Mateusz"},{"first_name":"Anne-Kathrin","full_name":"Schmuck, Anne-Kathrin","last_name":"Schmuck"},{"first_name":"Sadegh","full_name":"Soudjani, Sadegh","last_name":"Soudjani"}],"oa":1,"language":[{"iso":"eng"}],"page":"3-15","status":"public","day":"16","type":"conference","publisher":"Springer Nature","publication_identifier":{"eisbn":["9783031377099"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031377082"]},"quality_controlled":"1","month":"07","file_date_updated":"2024-01-09T10:01:07Z","publication":"35th International Conference on Computer Aided Verification","file":[{"access_level":"open_access","date_updated":"2024-01-09T10:01:07Z","file_size":405147,"file_name":"2023_LNCSCAV_Majumdar.pdf","creator":"dernst","date_created":"2024-01-09T10:01:07Z","content_type":"application/pdf","success":1,"checksum":"1a361d83db0244fd32c03b544c294b5a","file_id":"14765","relation":"main_file"}],"intvolume":"     13966","department":[{"_id":"ToHe"}],"external_id":{"isi":["001310805600001"]},"publication_status":"published","doi":"10.1007/978-3-031-37709-9_1","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"We present a flexible and efficient toolchain to symbolically solve (standard) Rabin games, fair-adversarial Rabin games, and 2 1/2 license type-player Rabin games. To our best knowledge, our tools are the first ones to be able to solve these problems. Furthermore, using these flexible game solvers as a back-end, we implemented a tool for computing correct-by-construction controllers for stochastic dynamical systems under LTL specifications. Our implementations use the recent theoretical result that all of these games can be solved using the same symbolic fixpoint algorithm but utilizing different, domain specific calculations of the involved predecessor operators. The main feature of our toolchain is the utilization of two programming abstractions: one to separate the symbolic fixpoint computations from the predecessor calculations, and another one to allow the integration of different BDD libraries as back-ends. In particular, we employ a multi-threaded execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan, which leads to enormous computational savings."}],"ec_funded":1,"date_published":"2023-07-16T00:00:00Z","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"ddc":["000"],"conference":{"name":"CAV: Computer Aided Verification","end_date":"2023-07-22","start_date":"2023-07-17","location":"Paris, France"},"date_updated":"2025-09-09T14:16:49Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"volume":13966,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2024-01-08T13:18:00Z","year":"2023"},{"status":"public","page":"11926-11935","OA_place":"repository","type":"conference","day":"26","publisher":"Association for the Advancement of Artificial Intelligence","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"month":"06","quality_controlled":"1","issue":"10","_id":"14830","keyword":["General Medicine"],"corr_author":"1","article_processing_charge":"No","author":[{"first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mathias","full_name":"Lechner, Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"}],"language":[{"iso":"eng"}],"oa":1,"related_material":{"record":[{"id":"14600","relation":"earlier_version","status":"public"}]},"title":"Learning control policies for stochastic systems with reach-avoid guarantees","OA_type":"green","scopus_import":"1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","oa_version":"Preprint","citation":{"mla":"Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 10, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–35, doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>.","chicago":"Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:11926–35. Association for the Advancement of Artificial Intelligence, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>.","ieee":"D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 10, pp. 11926–11935.","ama":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:11926-11935. doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>","short":"D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–11935.","apa":"Zikelic, D., Lechner, M., Henzinger, T. A., &#38; Chatterjee, K. (2023). Learning control policies for stochastic systems with reach-avoid guarantees. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 11926–11935). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>","ista":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control policies for stochastic systems with reach-avoid guarantees. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 11926–11935."},"arxiv":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2210.05308"}],"date_created":"2024-01-18T07:44:31Z","year":"2023","project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"date_published":"2023-06-26T00:00:00Z","conference":{"name":"AAAI: Conference on Artificial Intelligence","end_date":"2023-02-14","start_date":"2023-02-07","location":"Washington, DC, United States"},"volume":37,"date_updated":"2025-07-03T11:38:12Z","external_id":{"arxiv":["2210.05308"]},"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publication_status":"published","doi":"10.1609/aaai.v37i10.26407","abstract":[{"text":"We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks.","lang":"eng"}],"ec_funded":1,"intvolume":"        37","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence"},{"arxiv":1,"citation":{"ama":"Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. Fast symbolic algorithms for mega-regular games under strong transition fairness. <i>TheoretiCS</i>. 2023;2. doi:<a href=\"https://doi.org/10.46298/theoretics.23.4\">10.46298/theoretics.23.4</a>","short":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, TheoretiCS 2 (2023).","ieee":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani, “Fast symbolic algorithms for mega-regular games under strong transition fairness,” <i>TheoretiCS</i>, vol. 2. EPI Sciences, 2023.","ista":"Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. 2023. Fast symbolic algorithms for mega-regular games under strong transition fairness. TheoretiCS. 2, 4.","apa":"Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., &#38; Soudjani, S. (2023). Fast symbolic algorithms for mega-regular games under strong transition fairness. <i>TheoretiCS</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/theoretics.23.4\">https://doi.org/10.46298/theoretics.23.4</a>","mla":"Banerjee, Tamajit, et al. “Fast Symbolic Algorithms for Mega-Regular Games under Strong Transition Fairness.” <i>TheoretiCS</i>, vol. 2, 4, EPI Sciences, 2023, doi:<a href=\"https://doi.org/10.46298/theoretics.23.4\">10.46298/theoretics.23.4</a>.","chicago":"Banerjee, Tamajit, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, and Sadegh Soudjani. “Fast Symbolic Algorithms for Mega-Regular Games under Strong Transition Fairness.” <i>TheoretiCS</i>. EPI Sciences, 2023. <a href=\"https://doi.org/10.46298/theoretics.23.4\">https://doi.org/10.46298/theoretics.23.4</a>."},"has_accepted_license":"1","title":"Fast symbolic algorithms for mega-regular games under strong transition fairness","acknowledgement":"A previous version of this paper has appeared in TACAS 2022. Authors ordered alphabetically. T. Banerjee was interning with MPI-SWS when this research was conducted. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093.","oa_version":"Published Version","article_processing_charge":"Yes","article_type":"original","_id":"14920","corr_author":"1","language":[{"iso":"eng"}],"oa":1,"author":[{"full_name":"Banerjee, Tamajit","last_name":"Banerjee","first_name":"Tamajit"},{"last_name":"Majumdar","full_name":"Majumdar, Rupak","first_name":"Rupak"},{"first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","last_name":"Mallik"},{"last_name":"Schmuck","full_name":"Schmuck, Anne-Kathrin","first_name":"Anne-Kathrin"},{"full_name":"Soudjani, Sadegh","last_name":"Soudjani","first_name":"Sadegh"}],"day":"24","type":"journal_article","status":"public","month":"02","quality_controlled":"1","publication_identifier":{"issn":["2751-4838"]},"article_number":"4","publisher":"EPI Sciences","file_date_updated":"2024-02-05T10:19:35Z","file":[{"relation":"main_file","file_id":"14940","checksum":"2972d531122a6f15727b396110fb3f5c","content_type":"application/pdf","success":1,"date_created":"2024-02-05T10:19:35Z","creator":"dernst","date_updated":"2024-02-05T10:19:35Z","file_size":917076,"file_name":"2023_TheoretiCS_Banerjee.pdf","access_level":"open_access"}],"intvolume":"         2","publication":"TheoretiCS","publication_status":"published","department":[{"_id":"ToHe"}],"external_id":{"arxiv":["2202.07480"]},"ec_funded":1,"abstract":[{"text":"We consider fixpoint algorithms for two-player games on graphs with $\\omega$-regular winning conditions, where the environment is constrained by a strong transition fairness assumption. Strong transition fairness is a widely occurring special case of strong fairness, which requires that any execution is strongly fair with respect to a specified set of live edges: whenever the\r\nsource vertex of a live edge is visited infinitely often along a play, the edge itself is traversed infinitely often along the play as well. We show that, surprisingly, strong transition fairness retains the algorithmic characteristics of the fixpoint algorithms for $\\omega$-regular games -- the new algorithms have the same alternation depth as the classical algorithms but invoke a new type of predecessor operator. For Rabin games with $k$ pairs, the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is independent of the number of live edges in the strong transition fairness assumption. Further, we show that GR(1) specifications with strong transition fairness assumptions can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm. In contrast, strong fairness necessarily requires increasing the alternation depth depending on the number of fairness assumptions. We get symbolic algorithms for (generalized) Rabin, parity and GR(1) objectives under strong transition fairness assumptions as well as a direct symbolic algorithm for qualitative winning in stochastic\r\n$\\omega$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps, improving the state of the art. Finally, we have implemented a BDD-based synthesis engine based on our algorithm. We show on a set of synthetic and real benchmarks that our algorithm is scalable, parallelizable, and outperforms previous algorithms by orders of magnitude.","lang":"eng"}],"doi":"10.46298/theoretics.23.4","date_published":"2023-02-24T00:00:00Z","ddc":["000"],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"date_updated":"2025-04-14T07:55:57Z","volume":2,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2023","date_created":"2024-01-31T13:40:49Z"},{"date_updated":"2025-09-09T14:16:48Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"oa":1,"author":[{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"},{"orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","last_name":"Mallik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik"},{"last_name":"Rychlicki","full_name":"Rychlicki, Mateusz","first_name":"Mateusz"},{"full_name":"Schmuck, Anne-Kathrin","last_name":"Schmuck","first_name":"Anne-Kathrin"},{"first_name":"Sadegh","full_name":"Soudjani, Sadegh","last_name":"Soudjani"}],"date_published":"2023-04-28T00:00:00Z","ddc":["000"],"article_processing_charge":"No","_id":"14994","corr_author":"1","month":"04","year":"2023","date_created":"2024-02-14T15:13:00Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5281/zenodo.7877790"}],"publisher":"Zenodo","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"28","type":"research_data_reference","status":"public","citation":{"mla":"Majumdar, Rupak, et al. <i>A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties</i>. Zenodo, 2023, doi:<a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>.","chicago":"Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.7877790\">https://doi.org/10.5281/ZENODO.7877790</a>.","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, (2023).","ieee":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties.” Zenodo, 2023.","ama":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 2023. doi:<a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>","ista":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>.","apa":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., &#38; Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.7877790\">https://doi.org/10.5281/ZENODO.7877790</a>"},"has_accepted_license":"1","oa_version":"Published Version","abstract":[{"text":"This resource contains the artifacts for reproducing the experimental results presented in the paper titled \"A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties\" that has been submitted in CAV 2023.","lang":"eng"}],"doi":"10.5281/ZENODO.7877790","title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"14758"}]},"department":[{"_id":"ToHe"}]},{"type":"research_data_reference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"28","status":"public","year":"2023","month":"07","publisher":"Zenodo","main_file_link":[{"url":"https://doi.org/10.5281/zenodo.8191722","open_access":"1"}],"date_created":"2024-02-28T07:34:34Z","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"ddc":["000"],"article_processing_charge":"No","date_published":"2023-07-28T00:00:00Z","_id":"15035","corr_author":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"oa":1,"date_updated":"2025-04-14T09:42:55Z","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"}],"title":"Monitoring hyperproperties with prefix transducers","related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"14076"}]},"department":[{"_id":"ToHe"}],"ec_funded":1,"abstract":[{"lang":"eng","text":"This artifact aims to reproduce experiments from the paper Monitoring Hyperproperties With Prefix Transducers accepted at RV'23, and give further pointers to implementation of prefix transducers.\r\nIt has two parts: a pre-compiled docker image and sources that one can use to compile (locally or in docker) the software and run the experiments."}],"oa_version":"Published Version","doi":"10.5281/ZENODO.8191723","citation":{"ista":"Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>.","apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.8191723\">https://doi.org/10.5281/ZENODO.8191723</a>","short":"M. Chalupa, T.A. Henzinger, (2023).","ieee":"M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers.” Zenodo, 2023.","ama":"Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. 2023. doi:<a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.8191723\">https://doi.org/10.5281/ZENODO.8191723</a>.","mla":"Chalupa, Marek, and Thomas A. Henzinger. <i>Monitoring Hyperproperties with Prefix Transducers</i>. Zenodo, 2023, doi:<a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>."},"has_accepted_license":"1"},{"doi":"10.34727/2023/isbn.978-3-85448-060-0_20","das_tickbox":"1","ec_funded":1,"abstract":[{"lang":"eng","text":"Binary decision diagrams (BDDs) are one of the fundamental data structures in formal methods and computer science in general. However, the performance of BDD-based algorithms greatly depends on memory latency due to the reliance on large hash tables and thus, by extension, on the speed of random memory access. This hinders the full utilisation of resources available on modern CPUs, since the absolute memory latency has not improved significantly for at least a decade. In this paper, we explore several implementation techniques that improve the performance of BDD manipulation either through enhanced memory locality or by partially eliminating random memory access. On a benchmark suite of 600+ BDDs derived from real-world applications, we demonstrate runtime that is comparable or better than parallelising the same operations on eight CPU cores. "}],"department":[{"_id":"ToHe"}],"external_id":{"isi":["001504402400020"]},"publication_status":"published","file":[{"file_size":524321,"file_name":"2023_FMCAD_Pastva.pdf","date_updated":"2024-01-02T08:14:23Z","access_level":"open_access","creator":"dernst","content_type":"application/pdf","success":1,"date_created":"2024-01-02T08:14:23Z","relation":"main_file","file_id":"14721","checksum":"818d6e13dd508f3a04f0941081022e5d"}],"publication":"Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design","file_date_updated":"2024-01-02T08:14:23Z","date_created":"2023-12-31T23:01:03Z","year":"2023","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2023-10-25","location":"Ames, IA, United States","end_date":"2023-10-27","name":"FMCAD: Formal Methods in Computer-Aided Design"},"date_updated":"2026-07-07T05:58:51Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"date_published":"2023-10-01T00:00:00Z","ddc":["000"],"project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program"},{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"isi":1,"oa_version":"Published Version","acknowledgement":"This work was supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413 and the\r\n“VAMOS” grant ERC-2020-AdG 101020093.","scopus_import":"1","title":"Binary decision diagrams on modern hardware","has_accepted_license":"1","citation":{"apa":"Pastva, S., &#38; Henzinger, T. A. (2023). Binary decision diagrams on modern hardware. In <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i> (pp. 122–131). Ames, IA, United States: TU Wien Academic Press. <a href=\"https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20\">https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20</a>","ista":"Pastva S, Henzinger TA. 2023. Binary decision diagrams on modern hardware. Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 122–131.","short":"S. Pastva, T.A. Henzinger, in:, Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press, 2023, pp. 122–131.","ama":"Pastva S, Henzinger TA. Binary decision diagrams on modern hardware. In: <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i>. TU Wien Academic Press; 2023:122-131. doi:<a href=\"https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20\">10.34727/2023/isbn.978-3-85448-060-0_20</a>","ieee":"S. Pastva and T. A. Henzinger, “Binary decision diagrams on modern hardware,” in <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i>, Ames, IA, United States, 2023, pp. 122–131.","mla":"Pastva, Samuel, and Thomas A. Henzinger. “Binary Decision Diagrams on Modern Hardware.” <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i>, TU Wien Academic Press, 2023, pp. 122–31, doi:<a href=\"https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20\">10.34727/2023/isbn.978-3-85448-060-0_20</a>.","chicago":"Pastva, Samuel, and Thomas A Henzinger. “Binary Decision Diagrams on Modern Hardware.” In <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i>, 122–31. TU Wien Academic Press, 2023. <a href=\"https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20\">https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20</a>."},"publisher":"TU Wien Academic Press","publication_identifier":{"isbn":["9783854480600"]},"month":"10","quality_controlled":"1","page":"122-131","status":"public","day":"01","type":"conference","author":[{"last_name":"Pastva","orcid":"0000-0003-1993-0331","full_name":"Pastva, Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","first_name":"Samuel"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"language":[{"iso":"eng"}],"oa":1,"corr_author":"1","_id":"14718","article_processing_charge":"No"},{"year":"2023","main_file_link":[{"url":"https://doi.org/10.1609/aaai.v37i5.25679","open_access":"1"}],"date_created":"2023-08-27T22:01:18Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":37,"date_updated":"2026-07-07T06:24:15Z","conference":{"location":"Washington, DC, United States","start_date":"2023-02-07","end_date":"2023-02-14","name":"AAAI: Conference on Artificial Intelligence"},"ddc":["000"],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"International IST Doctoral Program","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"date_published":"2023-06-27T00:00:00Z","abstract":[{"text":"Two-player zero-sum \"graph games\" are central in logic, verification, and multi-agent systems. The game proceeds by placing a token on a vertex of a graph, and allowing the players to move it to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In \"bidding games\", however, the players have budgets and in each turn, an auction (bidding) determines which player moves the token. So far, bidding games have only been studied as full-information games. In this work we initiate the study of partial-information bidding games: we study bidding games in which a player's initial budget is drawn from a known probability distribution. We show that while for some bidding mechanisms and objectives, it is straightforward to adapt the results from the full-information setting to the partial-information setting, for others, the analysis is significantly more challenging, requires new techniques, and gives rise to interesting results. Specifically, we study games with \"mean-payoff\" objectives in combination with \"poorman\" bidding. We construct optimal strategies for a partially-informed player who plays against a fully-informed adversary. We show that, somewhat surprisingly, the \"value\" under pure strategies does not necessarily exist in such games.","lang":"eng"}],"ec_funded":1,"das_tickbox":"1","doi":"10.1609/aaai.v37i5.25679","publication_status":"published","external_id":{"arxiv":["2211.13626"]},"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","intvolume":"        37","quality_controlled":"1","month":"06","publication_identifier":{"isbn":["9781577358800"]},"publisher":"AAAI Press","type":"conference","day":"27","status":"public","page":"5464-5471","language":[{"iso":"eng"}],"oa":1,"author":[{"first_name":"Guy","last_name":"Avni","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","full_name":"Jecker, Ismael R","last_name":"Jecker","first_name":"Ismael R"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde"}],"article_processing_charge":"No","issue":"5","_id":"14243","acknowledgement":"This research was supported in part by ISF grant no.1679/21, by the ERC CoG 863818 (ForM-SMArt), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","oa_version":"Published Version","scopus_import":"1","title":"Bidding graph games with partially-observable budgets","citation":{"mla":"Avni, Guy, et al. “Bidding Graph Games with Partially-Observable Budgets.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 5, AAAI Press, 2023, pp. 5464–71, doi:<a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">10.1609/aaai.v37i5.25679</a>.","chicago":"Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Bidding Graph Games with Partially-Observable Budgets.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:5464–71. AAAI Press, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">https://doi.org/10.1609/aaai.v37i5.25679</a>.","ama":"Avni G, Jecker IR, Zikelic D. Bidding graph games with partially-observable budgets. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. AAAI Press; 2023:5464-5471. doi:<a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">10.1609/aaai.v37i5.25679</a>","ieee":"G. Avni, I. R. Jecker, and D. Zikelic, “Bidding graph games with partially-observable budgets,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 5, pp. 5464–5471.","short":"G. Avni, I.R. Jecker, D. Zikelic, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, AAAI Press, 2023, pp. 5464–5471.","apa":"Avni, G., Jecker, I. R., &#38; Zikelic, D. (2023). Bidding graph games with partially-observable budgets. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 5464–5471). Washington, DC, United States: AAAI Press. <a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">https://doi.org/10.1609/aaai.v37i5.25679</a>","ista":"Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 5464–5471."},"arxiv":1},{"arxiv":1,"citation":{"chicago":"Zikelic, Dorde, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A Henzinger. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” In <i>37th Conference on Neural Information Processing Systems</i>. Neural Information Processing Systems Foundation, 2023.","mla":"Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” <i>37th Conference on Neural Information Processing Systems</i>, Neural Information Processing Systems Foundation, 2023.","ieee":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger, “Compositional policy learning in stochastic control systems with formal guarantees,” in <i>37th Conference on Neural Information Processing Systems</i>, New Orleans, LO, United States, 2023.","short":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2023.","ama":"Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. Compositional policy learning in stochastic control systems with formal guarantees. In: <i>37th Conference on Neural Information Processing Systems</i>. Neural Information Processing Systems Foundation; 2023.","ista":"Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional policy learning in stochastic control systems with formal guarantees. 37th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems, Advances in Neural Information Processing Systems, .","apa":"Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., &#38; Henzinger, T. A. (2023). Compositional policy learning in stochastic control systems with formal guarantees. In <i>37th Conference on Neural Information Processing Systems</i>. New Orleans, LO, United States: Neural Information Processing Systems Foundation."},"has_accepted_license":"1","title":"Compositional policy learning in stochastic control systems with formal guarantees","oa_version":"Published Version","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS) and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt).","article_processing_charge":"No","_id":"15023","corr_author":"1","language":[{"iso":"eng"}],"oa":1,"author":[{"first_name":"Dorde","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner"},{"first_name":"Abhinav","last_name":"Verma","full_name":"Verma, Abhinav","id":"a235593c-d7fa-11eb-a0c5-b22ca3c66ee6"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"day":"15","type":"conference","status":"public","quality_controlled":"1","month":"12","publisher":"Neural Information Processing Systems Foundation","publication_identifier":{"eissn":["1049-5258"]},"file_date_updated":"2024-07-22T11:45:17Z","file":[{"relation":"main_file","file_id":"17309","checksum":"739c6d72506b778302d4e708723bf12c","content_type":"application/pdf","success":1,"date_created":"2024-07-22T11:45:17Z","creator":"dernst","file_size":562008,"file_name":"2023_NeurIPS_Zikelic.pdf","date_updated":"2024-07-22T11:45:17Z","access_level":"open_access"}],"publication":"37th Conference on Neural Information Processing Systems","publication_status":"published","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"external_id":{"arxiv":["2312.01456"]},"ec_funded":1,"abstract":[{"text":"Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph’s sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.","lang":"eng"}],"das_tickbox":"1","alternative_title":["Advances in Neural Information Processing Systems"],"date_published":"2023-12-15T00:00:00Z","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"ddc":["000"],"date_updated":"2026-07-07T06:36:54Z","conference":{"end_date":"2023-12-16","name":"NeurIPS: Neural Information Processing Systems","location":"New Orleans, LO, United States","start_date":"2023-12-10"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2023","date_created":"2024-02-25T09:23:24Z"},{"article_processing_charge":"No","_id":"13221","corr_author":"1","language":[{"iso":"eng"}],"oa":1,"author":[{"full_name":"Boker, Udi","last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi","first_name":"Nicolas Adrien"},{"first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E","last_name":"Sarac"}],"day":"01","type":"conference","status":"public","month":"09","quality_controlled":"1","publication_identifier":{"eissn":["1868-8969"],"isbn":["9783959772990"]},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","article_number":"17","arxiv":1,"citation":{"apa":"Boker, U., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Safety and liveness of quantitative automata. In <i>34th International Conference on Concurrency Theory</i> (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.17</a>","ista":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Safety and liveness of quantitative automata. 34th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 279, 17.","ieee":"U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Safety and liveness of quantitative automata,” in <i>34th International Conference on Concurrency Theory</i>, Antwerp, Belgium, 2023, vol. 279.","ama":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative automata. In: <i>34th International Conference on Concurrency Theory</i>. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">10.4230/LIPIcs.CONCUR.2023.17</a>","short":"U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 34th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.","mla":"Boker, Udi, et al. “Safety and Liveness of Quantitative Automata.” <i>34th International Conference on Concurrency Theory</i>, vol. 279, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">10.4230/LIPIcs.CONCUR.2023.17</a>.","chicago":"Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Safety and Liveness of Quantitative Automata.” In <i>34th International Conference on Concurrency Theory</i>, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.17</a>."},"has_accepted_license":"1","title":"Safety and liveness of quantitative automata","related_material":{"record":[{"id":"20342","relation":"later_version","status":"public"},{"id":"20147","relation":"dissertation_contains","status":"public"}]},"acknowledgement":"We thank Christof Löding for pointing us to some results on PSpace-hardess of universality problems and the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093 and the Israel Science Foundation grant 2410/22.","scopus_import":"1","oa_version":"Published Version","isi":1,"date_published":"2023-09-01T00:00:00Z","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"ddc":["000"],"date_updated":"2026-07-27T12:48:18Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"volume":279,"conference":{"end_date":"2023-09-23","name":"CONCUR: Conference on Concurrency Theory","location":"Antwerp, Belgium","start_date":"2023-09-18"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2023","date_created":"2023-07-14T10:00:15Z","file_date_updated":"2023-07-14T12:03:48Z","publication":"34th International Conference on Concurrency Theory","file":[{"creator":"esarac","access_level":"open_access","date_updated":"2023-07-14T12:03:48Z","file_name":"CONCUR23.pdf","file_size":755529,"file_id":"13224","checksum":"d40e57a04448ea5c77d7e1cfb9590a81","relation":"main_file","date_created":"2023-07-14T12:03:48Z","success":1,"content_type":"application/pdf"}],"intvolume":"       279","publication_status":"published","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"external_id":{"arxiv":["2307.06016"],"isi":["001570542500017"]},"abstract":[{"text":"The safety-liveness dichotomy is a fundamental concept in formal languages which plays a key role in verification. Recently, this dichotomy has been lifted to quantitative properties, which are arbitrary functions from infinite words to partially-ordered domains. We look into harnessing the dichotomy for the specific classes of quantitative properties expressed by quantitative automata. These automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totallyordered domain of real numbers. In this automata-theoretic setting, we establish a connection between quantitative safety and topological continuity and provide an alternative characterization of quantitative safety and liveness in terms of their boolean counterparts. For all common value functions, we show how the safety closure of a quantitative automaton can be constructed in PTime, and we provide PSpace-complete checks of whether a given quantitative automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata, for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf, and LimSup automata, we give PTime decompositions into safe and live automata. These decompositions enable the separation of techniques for safety and liveness verification for quantitative specifications.","lang":"eng"}],"ec_funded":1,"doi":"10.4230/LIPIcs.CONCUR.2023.17","alternative_title":["LIPIcs"]},{"citation":{"ama":"Henzinger TA. Quantitative monitoring of software. In: <i>Software Verification</i>. Vol 13124. LNCS. Springer Nature; 2022:3-6. doi:<a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">10.1007/978-3-030-95561-8_1</a>","ieee":"T. A. Henzinger, “Quantitative monitoring of software,” in <i>Software Verification</i>, New Haven, CT, United States, 2022, vol. 13124, pp. 3–6.","short":"T.A. Henzinger, in:, Software Verification, Springer Nature, 2022, pp. 3–6.","apa":"Henzinger, T. A. (2022). Quantitative monitoring of software. In <i>Software Verification</i> (Vol. 13124, pp. 3–6). New Haven, CT, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">https://doi.org/10.1007/978-3-030-95561-8_1</a>","ista":"Henzinger TA. 2022. Quantitative monitoring of software. Software Verification. NSV: Numerical Software VerificationLNCS vol. 13124, 3–6.","mla":"Henzinger, Thomas A. “Quantitative Monitoring of Software.” <i>Software Verification</i>, vol. 13124, Springer Nature, 2022, pp. 3–6, doi:<a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">10.1007/978-3-030-95561-8_1</a>.","chicago":"Henzinger, Thomas A. “Quantitative Monitoring of Software.” In <i>Software Verification</i>, 13124:3–6. LNCS. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">https://doi.org/10.1007/978-3-030-95561-8_1</a>."},"title":"Quantitative monitoring of software","isi":1,"scopus_import":"1","acknowledgement":"The formal framework for quantitative monitoring which is presented in this invited talk was defined jointly with N. Ege Saraç at LICS 2021. This work was supported in part by the Wittgenstein Award Z211-N23 of the Austrian Science Fund.","oa_version":"None","corr_author":"1","_id":"10891","article_processing_charge":"No","author":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"language":[{"iso":"eng"}],"status":"public","page":"3-6","day":"22","type":"conference","publication_identifier":{"isbn":["9783030955601"],"issn":["0302-9743"],"eissn":["1611-3349"]},"publisher":"Springer Nature","month":"02","quality_controlled":"1","publication":"Software Verification","intvolume":"     13124","department":[{"_id":"ToHe"}],"external_id":{"isi":["000771713200001"]},"publication_status":"published","doi":"10.1007/978-3-030-95561-8_1","abstract":[{"text":"We present a formal framework for the online black-box monitoring of software using monitors with quantitative verdict functions. Quantitative verdict functions have several advantages. First, quantitative monitors can be approximate, i.e., the value of the verdict function does not need to correspond exactly to the value of the property under observation. Second, quantitative monitors can be quantified universally, i.e., for every possible observed behavior, the monitor tries to make the best effort to estimate the value of the property under observation. Third, quantitative monitors can watch boolean as well as quantitative properties, such as average response time. Fourth, quantitative monitors can use non-finite-state resources, such as counters. As a consequence, quantitative monitors can be compared according to how many resources they use (e.g., the number of counters) and how precisely they approximate the property under observation. This allows for a rich spectrum of cost-precision trade-offs in monitoring software.","lang":"eng"}],"date_published":"2022-02-22T00:00:00Z","project":[{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"conference":{"name":"NSV: Numerical Software Verification","end_date":"2021-10-19","start_date":"2021-10-18","location":"New Haven, CT, United States"},"date_updated":"2025-04-15T06:25:58Z","series_title":"LNCS","volume":13124,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","date_created":"2022-03-20T23:01:40Z","year":"2022"},{"conference":{"start_date":"2022-04-02","location":"Munich, Germany","end_date":"2022-04-07","name":"FASE: Fundamental Approaches to Software Engineering"},"date_updated":"2025-12-30T06:50:51Z","volume":13241,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"date_published":"2022-03-29T00:00:00Z","ddc":["000"],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"date_created":"2022-05-08T22:01:44Z","year":"2022","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publication":"Fundamental Approaches to Software Engineering","file":[{"creator":"dernst","date_updated":"2022-05-09T06:52:44Z","file_size":479146,"file_name":"2022_LNCS_Bartocci.pdf","access_level":"open_access","relation":"main_file","checksum":"7f6f860b20b8de2a249e9c1b4eee15cf","file_id":"11357","content_type":"application/pdf","success":1,"date_created":"2022-05-09T06:52:44Z"}],"intvolume":"     13241","file_date_updated":"2022-05-09T06:52:44Z","doi":"10.1007/978-3-030-99429-7_1","alternative_title":["LNCS"],"ec_funded":1,"abstract":[{"lang":"eng","text":"Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees.\r\nAlthough there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory that is designed for ensuring system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. We illustrate the applicability of our framework with an example inspired from the automotive domain."}],"department":[{"_id":"ToHe"}],"external_id":{"isi":["000782393600001"]},"publication_status":"published","author":[{"first_name":"Ezio","full_name":"Bartocci, Ezio","last_name":"Bartocci"},{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","first_name":"Thomas"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Nickovic, Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan"},{"first_name":"Ana Oliveira","full_name":"Da Costa, Ana Oliveira","last_name":"Da Costa"}],"language":[{"iso":"eng"}],"oa":1,"_id":"11355","article_processing_charge":"No","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783030994280"]},"publisher":"Springer Nature","month":"03","quality_controlled":"1","status":"public","page":"3-22","day":"29","type":"conference","has_accepted_license":"1","citation":{"chicago":"Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Information-Flow Interfaces.” In <i>Fundamental Approaches to Software Engineering</i>, 13241:3–22. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">https://doi.org/10.1007/978-3-030-99429-7_1</a>.","mla":"Bartocci, Ezio, et al. “Information-Flow Interfaces.” <i>Fundamental Approaches to Software Engineering</i>, vol. 13241, Springer Nature, 2022, pp. 3–22, doi:<a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">10.1007/978-3-030-99429-7_1</a>.","short":"E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2022, pp. 3–22.","ama":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Information-flow interfaces. In: <i>Fundamental Approaches to Software Engineering</i>. Vol 13241. Springer Nature; 2022:3-22. doi:<a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">10.1007/978-3-030-99429-7_1</a>","ieee":"E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Information-flow interfaces,” in <i>Fundamental Approaches to Software Engineering</i>, Munich, Germany, 2022, vol. 13241, pp. 3–22.","ista":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Information-flow interfaces. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13241, 3–22.","apa":"Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Da Costa, A. O. (2022). Information-flow interfaces. In <i>Fundamental Approaches to Software Engineering</i> (Vol. 13241, pp. 3–22). Munich, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">https://doi.org/10.1007/978-3-030-99429-7_1</a>"},"isi":1,"scopus_import":"1","acknowledgement":"This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 956123 and was funded in part by the FWF project W1255-N23 and by the ERC-2020-AdG 101020093.","oa_version":"Published Version","related_material":{"record":[{"relation":"extended_version","status":"public","id":"17094"}]},"title":"Information-flow interfaces"},{"date_updated":"2026-04-07T14:21:58Z","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"date_published":"2022-04-15T00:00:00Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2204.07373","open_access":"1"}],"date_created":"2022-05-12T13:20:17Z","year":"2022","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"arXiv","doi":"10.48550/arXiv.2204.07373","abstract":[{"lang":"eng","text":"Adversarial training (i.e., training on adversarially perturbed input data) is a well-studied method for making neural networks robust to potential adversarial attacks during inference. However, the improved robustness does not\r\ncome for free but rather is accompanied by a decrease in overall model accuracy and performance. Recent work has shown that, in practical robot learning applications, the effects of adversarial training do not pose a fair trade-off\r\nbut inflict a net loss when measured in holistic robot performance. This work revisits the robustness-accuracy trade-off in robot learning by systematically analyzing if recent advances in robust training methods and theory in\r\nconjunction with adversarial robot learning can make adversarial training suitable for real-world robot applications. We evaluate a wide variety of robot learning tasks ranging from autonomous driving in a high-fidelity environment\r\namenable to sim-to-real deployment, to mobile robot gesture recognition. Our results demonstrate that, while these techniques make incremental improvements on the trade-off on a relative scale, the negative side-effects caused by\r\nadversarial training still outweigh the improvements by an order of magnitude. We conclude that more substantial advances in robust learning methods are necessary before they can benefit robot learning tasks in practice."}],"ec_funded":1,"external_id":{"arxiv":["2204.07373"]},"department":[{"_id":"ToHe"}],"publication_status":"draft","author":[{"first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","full_name":"Lechner, Mathias"},{"full_name":"Amini, Alexander","last_name":"Amini","first_name":"Alexander"},{"first_name":"Daniela","last_name":"Rus","full_name":"Rus, Daniela"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"}],"oa":1,"language":[{"iso":"eng"}],"corr_author":"1","_id":"11366","article_processing_charge":"No","article_number":"2204.07373","month":"04","status":"public","OA_place":"repository","type":"preprint","day":"15","citation":{"mla":"Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” <i>ArXiv</i>, 2204.07373, doi:<a href=\"https://doi.org/10.48550/arXiv.2204.07373\">10.48550/arXiv.2204.07373</a>.","chicago":"Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2204.07373\">https://doi.org/10.48550/arXiv.2204.07373</a>.","ama":"Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2204.07373\">10.48550/arXiv.2204.07373</a>","ieee":"M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial robustness-accuracy tradeoff in robot learning,” <i>arXiv</i>. .","short":"M. Lechner, A. Amini, D. Rus, T.A. Henzinger, ArXiv (n.d.).","apa":"Lechner, M., Amini, A., Rus, D., &#38; Henzinger, T. A. (n.d.). Revisiting the adversarial robustness-accuracy tradeoff in robot learning. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2204.07373\">https://doi.org/10.48550/arXiv.2204.07373</a>","ista":"Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. arXiv, 2204.07373."},"arxiv":1,"acknowledgement":"This work was supported in parts by the ERC-2020-AdG 101020093, National Science Foundation (NSF), and JP\r\nMorgan Graduate Fellowships. We thank Christoph Lampert for inspiring this work.\r\n","oa_version":"Preprint","title":"Revisiting the adversarial robustness-accuracy tradeoff in robot learning","related_material":{"record":[{"id":"12704","relation":"later_version","status":"public"},{"relation":"dissertation_contains","status":"public","id":"11362"}]}},{"department":[{"_id":"ToHe"}],"external_id":{"arxiv":["2103.04909"],"isi":["000941277600124"]},"publication_status":"published","doi":"10.1109/ICRA46639.2022.9811650","abstract":[{"lang":"eng","text":"World models learn behaviors in a latent imagination space to enhance the sample-efficiency of deep reinforcement learning (RL) algorithms. While learning world models for high-dimensional observations (e.g., pixel inputs) has become practicable on standard RL benchmarks and some games, their effectiveness in real-world robotics applications has not been explored. In this paper, we investigate how such agents generalize to real-world autonomous vehicle control tasks, where advanced model-free deep RL algorithms fail. In particular, we set up a series of time-lap tasks for an F1TENTH racing robot, equipped with a high-dimensional LiDAR sensor, on a set of test tracks with a gradual increase in their complexity. In this continuous-control setting, we show that model-based agents capable of learning in imagination substantially outperform model-free agents with respect to performance, sample efficiency, successful task completion, and generalization. Moreover, we show that the generalization ability of model-based agents strongly depends on the choice of their observation model. We provide extensive empirical evidence for the effectiveness of world models provided with long enough memory horizons in sim2real tasks."}],"ec_funded":1,"publication":"2022 International Conference on Robotics and Automation","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2022-09-04T22:02:02Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2103.04909"}],"year":"2022","date_published":"2022-07-12T00:00:00Z","project":[{"call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"},{"name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"conference":{"name":"ICRA: International Conference on Robotics and Automation","end_date":"2022-05-27","location":"Philadelphia, PA, United States","start_date":"2022-05-23"},"date_updated":"2025-09-10T09:39:53Z","title":"Latent imagination facilitates zero-shot transfer in autonomous racing","isi":1,"acknowledgement":"L.B. was supported by the Doctoral College Resilient Embedded Systems. M.L. was supported in part by the ERC2020-AdG 101020093 and the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). R.H. and D.R. were supported by The Boeing Company and the Office of Naval Research (ONR) Grant N00014-18-1-2830. R.G. was partially supported by the Horizon-2020 ECSEL Project grant No. 783163 (iDev40) and A.B. by FFG Project ADEX.","scopus_import":"1","oa_version":"Preprint","arxiv":1,"citation":{"ista":"Brunnbauer A, Berducci L, Brandstatter A, Lechner M, Hasani R, Rus D, Grosu R. 2022. Latent imagination facilitates zero-shot transfer in autonomous racing. 2022 International Conference on Robotics and Automation. ICRA: International Conference on Robotics and Automation, 7513–7520.","apa":"Brunnbauer, A., Berducci, L., Brandstatter, A., Lechner, M., Hasani, R., Rus, D., &#38; Grosu, R. (2022). Latent imagination facilitates zero-shot transfer in autonomous racing. In <i>2022 International Conference on Robotics and Automation</i> (pp. 7513–7520). Philadelphia, PA, United States: IEEE. <a href=\"https://doi.org/10.1109/ICRA46639.2022.9811650\">https://doi.org/10.1109/ICRA46639.2022.9811650</a>","short":"A. Brunnbauer, L. Berducci, A. Brandstatter, M. Lechner, R. Hasani, D. Rus, R. Grosu, in:, 2022 International Conference on Robotics and Automation, IEEE, 2022, pp. 7513–7520.","ama":"Brunnbauer A, Berducci L, Brandstatter A, et al. Latent imagination facilitates zero-shot transfer in autonomous racing. In: <i>2022 International Conference on Robotics and Automation</i>. IEEE; 2022:7513-7520. doi:<a href=\"https://doi.org/10.1109/ICRA46639.2022.9811650\">10.1109/ICRA46639.2022.9811650</a>","ieee":"A. Brunnbauer <i>et al.</i>, “Latent imagination facilitates zero-shot transfer in autonomous racing,” in <i>2022 International Conference on Robotics and Automation</i>, Philadelphia, PA, United States, 2022, pp. 7513–7520.","mla":"Brunnbauer, Axel, et al. “Latent Imagination Facilitates Zero-Shot Transfer in Autonomous Racing.” <i>2022 International Conference on Robotics and Automation</i>, IEEE, 2022, pp. 7513–20, doi:<a href=\"https://doi.org/10.1109/ICRA46639.2022.9811650\">10.1109/ICRA46639.2022.9811650</a>.","chicago":"Brunnbauer, Axel, Luigi Berducci, Andreas Brandstatter, Mathias Lechner, Ramin Hasani, Daniela Rus, and Radu Grosu. “Latent Imagination Facilitates Zero-Shot Transfer in Autonomous Racing.” In <i>2022 International Conference on Robotics and Automation</i>, 7513–20. IEEE, 2022. <a href=\"https://doi.org/10.1109/ICRA46639.2022.9811650\">https://doi.org/10.1109/ICRA46639.2022.9811650</a>."},"status":"public","page":"7513-7520","day":"12","type":"conference","publisher":"IEEE","publication_identifier":{"issn":["1050-4729"],"isbn":["9781728196817"]},"month":"07","quality_controlled":"1","_id":"12010","article_processing_charge":"No","author":[{"full_name":"Brunnbauer, Axel","last_name":"Brunnbauer","first_name":"Axel"},{"last_name":"Berducci","full_name":"Berducci, Luigi","first_name":"Luigi"},{"first_name":"Andreas","full_name":"Brandstatter, Andreas","last_name":"Brandstatter"},{"first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner"},{"first_name":"Ramin","last_name":"Hasani","full_name":"Hasani, Ramin"},{"first_name":"Daniela","last_name":"Rus","full_name":"Rus, Daniela"},{"last_name":"Grosu","full_name":"Grosu, Radu","first_name":"Radu"}],"language":[{"iso":"eng"}],"oa":1},{"isi":1,"scopus_import":"1","acknowledgement":"This research was supported in part by the AI2050 program at Schmidt Futures (grant G-22-63172), the Boeing Company, and the United States Air Force Research Laboratory and the United States Air Force Artificial Intelligence Accelerator and was accomplished under cooperative agreement number FA8750-19-2-1000. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the United States Air Force or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes, notwithstanding any copyright notation herein. This work was further supported by The Boeing Company and Office of Naval Research grant N00014-18-1-2830. M.T. is supported by the Poul Due Jensen Foundation, grant 883901. M.L. was supported in part by the Austrian Science Fund under grant Z211-N23 (Wittgenstein Award). A.A. was supported by the National Science Foundation Graduate Research Fellowship Program. We thank T.-H. Wang, P. Kao, M. Chahine, W. Xiao, X. Li, L. Yin and Y. Ben for useful suggestions and for testing of CfC models to confirm the results across other domains.","oa_version":"Published Version","title":"Closed-form continuous-time neural networks","related_material":{"link":[{"relation":"erratum","url":"https://doi.org/10.1038/s42256-022-00597-y"}]},"has_accepted_license":"1","arxiv":1,"citation":{"ista":"Hasani R, Lechner M, Amini A, Liebenwein L, Ray A, Tschaikowski M, Teschl G, Rus D. 2022. Closed-form continuous-time neural networks. Nature Machine Intelligence. 4(11), 992–1003.","apa":"Hasani, R., Lechner, M., Amini, A., Liebenwein, L., Ray, A., Tschaikowski, M., … Rus, D. (2022). Closed-form continuous-time neural networks. <i>Nature Machine Intelligence</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s42256-022-00556-7\">https://doi.org/10.1038/s42256-022-00556-7</a>","short":"R. Hasani, M. Lechner, A. Amini, L. Liebenwein, A. Ray, M. Tschaikowski, G. Teschl, D. Rus, Nature Machine Intelligence 4 (2022) 992–1003.","ieee":"R. Hasani <i>et al.</i>, “Closed-form continuous-time neural networks,” <i>Nature Machine Intelligence</i>, vol. 4, no. 11. Springer Nature, pp. 992–1003, 2022.","ama":"Hasani R, Lechner M, Amini A, et al. Closed-form continuous-time neural networks. <i>Nature Machine Intelligence</i>. 2022;4(11):992-1003. doi:<a href=\"https://doi.org/10.1038/s42256-022-00556-7\">10.1038/s42256-022-00556-7</a>","chicago":"Hasani, Ramin, Mathias Lechner, Alexander Amini, Lucas Liebenwein, Aaron Ray, Max Tschaikowski, Gerald Teschl, and Daniela Rus. “Closed-Form Continuous-Time Neural Networks.” <i>Nature Machine Intelligence</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1038/s42256-022-00556-7\">https://doi.org/10.1038/s42256-022-00556-7</a>.","mla":"Hasani, Ramin, et al. “Closed-Form Continuous-Time Neural Networks.” <i>Nature Machine Intelligence</i>, vol. 4, no. 11, Springer Nature, 2022, pp. 992–1003, doi:<a href=\"https://doi.org/10.1038/s42256-022-00556-7\">10.1038/s42256-022-00556-7</a>."},"publisher":"Springer Nature","publication_identifier":{"issn":["2522-5839"]},"month":"11","quality_controlled":"1","page":"992-1003","status":"public","day":"15","type":"journal_article","author":[{"first_name":"Ramin","full_name":"Hasani, Ramin","last_name":"Hasani"},{"last_name":"Lechner","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias"},{"last_name":"Amini","full_name":"Amini, Alexander","first_name":"Alexander"},{"first_name":"Lucas","last_name":"Liebenwein","full_name":"Liebenwein, Lucas"},{"first_name":"Aaron","full_name":"Ray, Aaron","last_name":"Ray"},{"first_name":"Max","last_name":"Tschaikowski","full_name":"Tschaikowski, Max"},{"full_name":"Teschl, Gerald","last_name":"Teschl","first_name":"Gerald"},{"last_name":"Rus","full_name":"Rus, Daniela","first_name":"Daniela"}],"oa":1,"language":[{"iso":"eng"}],"_id":"12147","keyword":["Artificial Intelligence","Computer Networks and Communications","Computer Vision and Pattern Recognition","Human-Computer Interaction","Software"],"issue":"11","article_processing_charge":"No","article_type":"original","doi":"10.1038/s42256-022-00556-7","abstract":[{"lang":"eng","text":"Continuous-time neural networks are a class of machine learning systems that can tackle representation learning on spatiotemporal decision-making tasks. These models are typically represented by continuous differential equations. However, their expressive power when they are deployed on computers is bottlenecked by numerical differential equation solvers. This limitation has notably slowed down the scaling and understanding of numerous natural physical phenomena such as the dynamics of nervous systems. Ideally, we would circumvent this bottleneck by solving the given dynamical system in closed form. This is known to be intractable in general. Here, we show that it is possible to closely approximate the interaction between neurons and synapses—the building blocks of natural and artificial neural networks—constructed by liquid time-constant networks efficiently in closed form. To this end, we compute a tightly bounded approximation of the solution of an integral appearing in liquid time-constant dynamics that has had no known closed-form solution so far. This closed-form solution impacts the design of continuous-time and continuous-depth neural models. For instance, since time appears explicitly in closed form, the formulation relaxes the need for complex numerical solvers. Consequently, we obtain models that are between one and five orders of magnitude faster in training and inference compared with differential equation-based counterparts. More importantly, in contrast to ordinary differential equation-based continuous networks, closed-form networks can scale remarkably well compared with other deep learning instances. Lastly, as these models are derived from liquid networks, they show good performance in time-series modelling compared with advanced recurrent neural network models."}],"department":[{"_id":"ToHe"}],"external_id":{"isi":["000884215600003"],"arxiv":["2106.13898"]},"publication_status":"published","publication":"Nature Machine Intelligence","intvolume":"         4","file":[{"date_created":"2023-01-24T09:49:44Z","content_type":"application/pdf","success":1,"file_id":"12355","checksum":"b4789122ce04bfb4ac042390f59aaa8b","relation":"main_file","access_level":"open_access","date_updated":"2023-01-24T09:49:44Z","file_name":"2022_NatureMachineIntelligence_Hasani.pdf","file_size":3259553,"creator":"dernst"}],"file_date_updated":"2023-01-24T09:49:44Z","date_created":"2023-01-12T12:07:21Z","year":"2022","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","date_updated":"2025-04-15T06:26:02Z","volume":4,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"date_published":"2022-11-15T00:00:00Z","ddc":["000"],"project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems"}]},{"status":"public","page":"337-353","type":"conference","day":"21","publication_identifier":{"eisbn":["9783031199929"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031199912"]},"publisher":"Springer Nature","month":"10","quality_controlled":"1","corr_author":"1","_id":"12171","article_processing_charge":"No","author":[{"first_name":"Miriam","last_name":"Garcia Soto","full_name":"Garcia Soto, Miriam","orcid":"0000-0003-2936-5719","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Schilling","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian"}],"oa":1,"language":[{"iso":"eng"}],"title":"Synthesis of parametric hybrid automata from time series","isi":1,"scopus_import":"1","acknowledgement":"This work was supported in part by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement no. 847635, by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark, and by the Villum Investigator Grant S4OS.","oa_version":"Preprint","citation":{"mla":"Garcia Soto, Miriam, et al. “Synthesis of Parametric Hybrid Automata from Time Series.” <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 13505, Springer Nature, 2022, pp. 337–53, doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">10.1007/978-3-031-19992-9_22</a>.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis of Parametric Hybrid Automata from Time Series.” In <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, 13505:337–53. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">https://doi.org/10.1007/978-3-031-19992-9_22</a>.","ista":"Garcia Soto M, Henzinger TA, Schilling C. 2022. Synthesis of parametric hybrid automata from time series. 20th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 13505, 337–353.","apa":"Garcia Soto, M., Henzinger, T. A., &#38; Schilling, C. (2022). Synthesis of parametric hybrid automata from time series. In <i>20th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 13505, pp. 337–353). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">https://doi.org/10.1007/978-3-031-19992-9_22</a>","ieee":"M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of parametric hybrid automata from time series,” in <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, Virtual, 2022, vol. 13505, pp. 337–353.","ama":"Garcia Soto M, Henzinger TA, Schilling C. Synthesis of parametric hybrid automata from time series. In: <i>20th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 13505. Springer Nature; 2022:337-353. doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">10.1007/978-3-031-19992-9_22</a>","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, 20th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2022, pp. 337–353."},"arxiv":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2208.06383"}],"date_created":"2023-01-12T12:11:16Z","year":"2022","project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020"}],"date_published":"2022-10-21T00:00:00Z","conference":{"location":"Virtual","start_date":"2022-10-25","end_date":"2022-10-28","name":"ATVA: Automated Technology for Verification and Analysis"},"volume":13505,"date_updated":"2025-09-10T09:50:08Z","external_id":{"arxiv":["2208.06383"],"isi":["001456146500022"]},"department":[{"_id":"ToHe"}],"publication_status":"published","alternative_title":["LNCS"],"doi":"10.1007/978-3-031-19992-9_22","ec_funded":1,"abstract":[{"lang":"eng","text":"We propose an algorithmic approach for synthesizing linear hybrid automata from time-series data. Unlike existing approaches, our approach provides a whole family of models with the same discrete structure but different dynamics. Each model in the family is guaranteed to capture the input data up to a precision error ε, in the following sense: For each time series, the model contains an execution that is ε-close to the data points. Our construction allows to effectively choose a model from this family with minimal precision error ε. We demonstrate the algorithm’s efficiency and its ability to find precise models in two case studies."}],"intvolume":"     13505","publication":"20th International Symposium on Automated Technology for Verification and Analysis"},{"citation":{"chicago":"Bose, Sougata, Thomas A Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke. “History-Deterministic Timed Automata Are Not Determinizable.” In <i>16th International Conference on Reachability Problems</i>, 13608:67–76. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-19135-0_5\">https://doi.org/10.1007/978-3-031-19135-0_5</a>.","mla":"Bose, Sougata, et al. “History-Deterministic Timed Automata Are Not Determinizable.” <i>16th International Conference on Reachability Problems</i>, vol. 13608, Springer Nature, 2022, pp. 67–76, doi:<a href=\"https://doi.org/10.1007/978-3-031-19135-0_5\">10.1007/978-3-031-19135-0_5</a>.","apa":"Bose, S., Henzinger, T. A., Lehtinen, K., Schewe, S., &#38; Totzke, P. (2022). History-deterministic timed automata are not determinizable. In <i>16th International Conference on Reachability Problems</i> (Vol. 13608, pp. 67–76). Kaiserslautern, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-19135-0_5\">https://doi.org/10.1007/978-3-031-19135-0_5</a>","ista":"Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. 2022. History-deterministic timed automata are not determinizable. 16th International Conference on Reachability Problems. RC: Reachability Problems, LNCS, vol. 13608, 67–76.","ama":"Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. History-deterministic timed automata are not determinizable. In: <i>16th International Conference on Reachability Problems</i>. Vol 13608. Springer Nature; 2022:67-76. doi:<a href=\"https://doi.org/10.1007/978-3-031-19135-0_5\">10.1007/978-3-031-19135-0_5</a>","short":"S. Bose, T.A. Henzinger, K. Lehtinen, S. Schewe, P. Totzke, in:, 16th International Conference on Reachability Problems, Springer Nature, 2022, pp. 67–76.","ieee":"S. Bose, T. A. Henzinger, K. Lehtinen, S. Schewe, and P. Totzke, “History-deterministic timed automata are not determinizable,” in <i>16th International Conference on Reachability Problems</i>, Kaiserslautern, Germany, 2022, vol. 13608, pp. 67–76."},"scopus_import":"1","oa_version":"Preprint","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, the EPSRC project EP/V025848/1, and the EPSRC project EP/X017796/1.","isi":1,"title":"History-deterministic timed automata are not determinizable","language":[{"iso":"eng"}],"oa":1,"author":[{"first_name":"Sougata","last_name":"Bose","full_name":"Bose, Sougata"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","first_name":"Thomas A"},{"last_name":"Lehtinen","full_name":"Lehtinen, Karoliina","first_name":"Karoliina"},{"full_name":"Schewe, Sven","last_name":"Schewe","first_name":"Sven"},{"full_name":"Totzke, Patrick","last_name":"Totzke","first_name":"Patrick"}],"article_processing_charge":"No","_id":"12175","quality_controlled":"1","month":"10","publisher":"Springer Nature","publication_identifier":{"isbn":["9783031191343"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031191350"]},"day":"12","type":"conference","status":"public","page":"67-76","publication":"16th International Conference on Reachability Problems","intvolume":"     13608","ec_funded":1,"abstract":[{"text":"An automaton is history-deterministic (HD) if one can safely resolve its non-deterministic choices on the fly. In a recent paper, Henzinger, Lehtinen and Totzke studied this in the context of Timed Automata [9], where it was conjectured that the class of timed ω-languages recognised by HD-timed automata strictly extends that of deterministic ones. We provide a proof for this fact.","lang":"eng"}],"doi":"10.1007/978-3-031-19135-0_5","alternative_title":["LNCS"],"publication_status":"published","department":[{"_id":"ToHe"}],"external_id":{"isi":["001333698300005"]},"date_updated":"2025-09-10T09:50:45Z","volume":13608,"conference":{"location":"Kaiserslautern, Germany","start_date":"2022-10-17","end_date":"2022-10-21","name":"RC: Reachability Problems"},"date_published":"2022-10-12T00:00:00Z","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"year":"2022","date_created":"2023-01-12T12:11:57Z","main_file_link":[{"open_access":"1","url":"https://hal.science/hal-03849398/"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"_id":"12302","article_processing_charge":"No","author":[{"last_name":"Doveri","full_name":"Doveri, Kyveli","first_name":"Kyveli"},{"full_name":"Ganty, Pierre","last_name":"Ganty","first_name":"Pierre"},{"first_name":"Nicolas Adrien","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"}],"oa":1,"language":[{"iso":"eng"}],"status":"public","page":"109-129","type":"conference","day":"06","publisher":"Springer Nature","publication_identifier":{"isbn":["9783031131875"],"eisbn":["9783031131882"],"issn":["0302-9743"],"eissn":["1611-3349"]},"quality_controlled":"1","month":"08","has_accepted_license":"1","citation":{"apa":"Doveri, K., Ganty, P., &#38; Mazzocchi, N. A. (2022). FORQ-based language inclusion formal testing. In <i>Computer Aided Verification</i> (Vol. 13372, pp. 109–129). Haifa, Israel: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-13188-2_6\">https://doi.org/10.1007/978-3-031-13188-2_6</a>","ista":"Doveri K, Ganty P, Mazzocchi NA. 2022. FORQ-based language inclusion formal testing. Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13372, 109–129.","ama":"Doveri K, Ganty P, Mazzocchi NA. FORQ-based language inclusion formal testing. In: <i>Computer Aided Verification</i>. Vol 13372. Springer Nature; 2022:109-129. doi:<a href=\"https://doi.org/10.1007/978-3-031-13188-2_6\">10.1007/978-3-031-13188-2_6</a>","short":"K. Doveri, P. Ganty, N.A. Mazzocchi, in:, Computer Aided Verification, Springer Nature, 2022, pp. 109–129.","ieee":"K. Doveri, P. Ganty, and N. A. Mazzocchi, “FORQ-based language inclusion formal testing,” in <i>Computer Aided Verification</i>, Haifa, Israel, 2022, vol. 13372, pp. 109–129.","mla":"Doveri, Kyveli, et al. “FORQ-Based Language Inclusion Formal Testing.” <i>Computer Aided Verification</i>, vol. 13372, Springer Nature, 2022, pp. 109–29, doi:<a href=\"https://doi.org/10.1007/978-3-031-13188-2_6\">10.1007/978-3-031-13188-2_6</a>.","chicago":"Doveri, Kyveli, Pierre Ganty, and Nicolas Adrien Mazzocchi. “FORQ-Based Language Inclusion Formal Testing.” In <i>Computer Aided Verification</i>, 13372:109–29. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-13188-2_6\">https://doi.org/10.1007/978-3-031-13188-2_6</a>."},"arxiv":1,"title":"FORQ-based language inclusion formal testing","isi":1,"acknowledgement":"This work was partially funded by the ESF Investing in your future, the Madrid regional project S2018/TCS-4339 BLOQUES, the Spanish project PGC2018-102210-B-I00 BOSCO, the Ramón y Cajal fellowship RYC-2016-20281, and the ERC grant PR1001ERC02.","oa_version":"Published Version","scopus_import":"1","project":[{"call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"ddc":["000"],"date_published":"2022-08-06T00:00:00Z","conference":{"name":"CAV: Computer Aided Verification","end_date":"2022-08-10","start_date":"2022-08-07","location":"Haifa, Israel"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"volume":13372,"date_updated":"2025-04-14T07:55:56Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_created":"2023-01-16T10:06:31Z","year":"2022","file_date_updated":"2023-01-30T12:51:02Z","file":[{"access_level":"open_access","file_name":"2022_LNCS_Doveri.pdf","file_size":497682,"date_updated":"2023-01-30T12:51:02Z","creator":"dernst","date_created":"2023-01-30T12:51:02Z","content_type":"application/pdf","success":1,"checksum":"edc363b1be5447a09063e115c247918a","file_id":"12465","relation":"main_file"}],"intvolume":"     13372","publication":"Computer Aided Verification","external_id":{"arxiv":["2207.13549"],"isi":["000870310500006"]},"department":[{"_id":"ToHe"}],"publication_status":"published","alternative_title":["LNCS"],"doi":"10.1007/978-3-031-13188-2_6","abstract":[{"lang":"eng","text":"We propose a novel algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ, called the structural FORQ, induced by the Büchi automaton to the right of the inclusion sign. The resulting implementation, called FORKLIFT, scales up better than the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics. Artifact: https://doi.org/10.5281/zenodo.6552870"}],"ec_funded":1},{"place":"Dagstuhl, Germany","article_processing_charge":"No","corr_author":"1","_id":"12509","language":[{"iso":"eng"}],"oa":1,"author":[{"last_name":"Avni","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"}],"day":"22","type":"conference","status":"public","page":"3:1-3:6","quality_controlled":"1","month":"08","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_identifier":{"isbn":["9783959772563"],"issn":["1868-8969"]},"citation":{"ieee":"G. Avni and T. A. Henzinger, “An updated survey of bidding games on graphs,” in <i>47th International Symposium on Mathematical Foundations of Computer Science</i>, Vienna, Austria, 2022, vol. 241, p. 3:1-3:6.","short":"G. Avni, T.A. Henzinger, in:, 47th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2022, p. 3:1-3:6.","ama":"Avni G, Henzinger TA. An updated survey of bidding games on graphs. In: <i>47th International Symposium on Mathematical Foundations of Computer Science</i>. Vol 241. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022:3:1-3:6. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2022.3\">10.4230/LIPIcs.MFCS.2022.3</a>","ista":"Avni G, Henzinger TA. 2022. An updated survey of bidding games on graphs. 47th International Symposium on Mathematical Foundations of Computer Science. MFCS: Mathematical Foundations of Computer ScienceLeibniz International Proceedings in Informatics (LIPIcs) vol. 241, 3:1-3:6.","apa":"Avni, G., &#38; Henzinger, T. A. (2022). An updated survey of bidding games on graphs. In <i>47th International Symposium on Mathematical Foundations of Computer Science</i> (Vol. 241, p. 3:1-3:6). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2022.3\">https://doi.org/10.4230/LIPIcs.MFCS.2022.3</a>","chicago":"Avni, Guy, and Thomas A Henzinger. “An Updated Survey of Bidding Games on Graphs.” In <i>47th International Symposium on Mathematical Foundations of Computer Science</i>, 241:3:1-3:6. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2022.3\">https://doi.org/10.4230/LIPIcs.MFCS.2022.3</a>.","mla":"Avni, Guy, and Thomas A. Henzinger. “An Updated Survey of Bidding Games on Graphs.” <i>47th International Symposium on Mathematical Foundations of Computer Science</i>, vol. 241, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, p. 3:1-3:6, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2022.3\">10.4230/LIPIcs.MFCS.2022.3</a>."},"has_accepted_license":"1","title":"An updated survey of bidding games on graphs","oa_version":"Published Version","scopus_import":"1","acknowledgement":"Guy Avni: Work partially supported by the Israel Science Foundation, ISF grant agreement\r\nno 1679/21.\r\nThomas A. Henzinger: This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe would like to thank all our collaborators Milad Aghajohari, Ventsislav Chonev, Rasmus Ibsen-Jensen, Ismäel Jecker, Petr Novotný, Josef Tkadlec, and Ðorđe Žikelić; we hope the collaboration was as fun and meaningful for you as it was for us.","date_published":"2022-08-22T00:00:00Z","ddc":["000"],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020"}],"series_title":"Leibniz International Proceedings in Informatics (LIPIcs)","date_updated":"2025-07-10T11:50:27Z","volume":241,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"conference":{"end_date":"2022-08-26","name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2022-08-22","location":"Vienna, Austria"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2022","date_created":"2023-02-05T17:26:01Z","file_date_updated":"2023-02-06T09:13:04Z","publication":"47th International Symposium on Mathematical Foundations of Computer Science","intvolume":"       241","file":[{"date_updated":"2023-02-06T09:13:04Z","file_name":"2022_LIPICs_Avni.pdf","file_size":624586,"access_level":"open_access","creator":"dernst","success":1,"content_type":"application/pdf","date_created":"2023-02-06T09:13:04Z","relation":"main_file","checksum":"1888ec9421622f9526fbec2de035f132","file_id":"12519"}],"publication_status":"published","department":[{"_id":"ToHe"}],"ec_funded":1,"abstract":[{"text":"A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an \"auction\" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We summarize how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.","lang":"eng"}],"doi":"10.4230/LIPIcs.MFCS.2022.3"},{"article_processing_charge":"No","article_type":"original","keyword":["General Medicine"],"_id":"12510","issue":"6","language":[{"iso":"eng"}],"oa":1,"author":[{"last_name":"Gruenbacher","full_name":"Gruenbacher, Sophie A.","first_name":"Sophie A."},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","full_name":"Lechner, Mathias","first_name":"Mathias"},{"last_name":"Hasani","full_name":"Hasani, Ramin","first_name":"Ramin"},{"full_name":"Rus, Daniela","last_name":"Rus","first_name":"Daniela"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Smolka","full_name":"Smolka, Scott A.","first_name":"Scott A."},{"last_name":"Grosu","full_name":"Grosu, Radu","first_name":"Radu"}],"type":"journal_article","day":"28","status":"public","page":"6755-6764","quality_controlled":"1","month":"06","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"],"isbn":["978577358350"]},"publisher":"Association for the Advancement of Artificial Intelligence","citation":{"short":"S.A. Gruenbacher, M. Lechner, R. Hasani, D. Rus, T.A. Henzinger, S.A. Smolka, R. Grosu, Proceedings of the AAAI Conference on Artificial Intelligence 36 (2022) 6755–6764.","ama":"Gruenbacher SA, Lechner M, Hasani R, et al. GoTube: Scalable statistical verification of continuous-depth models. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. 2022;36(6):6755-6764. doi:<a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">10.1609/aaai.v36i6.20631</a>","ieee":"S. A. Gruenbacher <i>et al.</i>, “GoTube: Scalable statistical verification of continuous-depth models,” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 6. Association for the Advancement of Artificial Intelligence, pp. 6755–6764, 2022.","ista":"Gruenbacher SA, Lechner M, Hasani R, Rus D, Henzinger TA, Smolka SA, Grosu R. 2022. GoTube: Scalable statistical verification of continuous-depth models. Proceedings of the AAAI Conference on Artificial Intelligence. 36(6), 6755–6764.","apa":"Gruenbacher, S. A., Lechner, M., Hasani, R., Rus, D., Henzinger, T. A., Smolka, S. A., &#38; Grosu, R. (2022). GoTube: Scalable statistical verification of continuous-depth models. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">https://doi.org/10.1609/aaai.v36i6.20631</a>","mla":"Gruenbacher, Sophie A., et al. “GoTube: Scalable Statistical Verification of Continuous-Depth Models.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 6, Association for the Advancement of Artificial Intelligence, 2022, pp. 6755–64, doi:<a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">10.1609/aaai.v36i6.20631</a>.","chicago":"Gruenbacher, Sophie A., Mathias Lechner, Ramin Hasani, Daniela Rus, Thomas A Henzinger, Scott A. Smolka, and Radu Grosu. “GoTube: Scalable Statistical Verification of Continuous-Depth Models.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2022. <a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">https://doi.org/10.1609/aaai.v36i6.20631</a>."},"arxiv":1,"title":"GoTube: Scalable statistical verification of continuous-depth models","oa_version":"Preprint","acknowledgement":"SG is funded by the Austrian Science Fund (FWF) project number W1255-N23. ML and TH are supported in part by FWF under grant Z211-N23 (Wittgenstein Award) and the ERC-2020-AdG 101020093. SS is supported by NSF awards DCL-2040599, CCF-1918225, and CPS-1446832. RH and DR are partially supported by Boeing. RG is partially supported by Horizon-2020 ECSEL Project grant No. 783163 (iDev40).","scopus_import":"1","project":[{"name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF"},{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"date_published":"2022-06-28T00:00:00Z","volume":36,"date_updated":"2025-04-15T06:26:14Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2022","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2107.08467"}],"date_created":"2023-02-05T17:27:42Z","intvolume":"        36","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","publication_status":"published","external_id":{"arxiv":["2107.08467"]},"department":[{"_id":"ToHe"}],"ec_funded":1,"abstract":[{"lang":"eng","text":"We introduce a new statistical verification algorithm that formally quantifies the behavioral robustness of any time-continuous process formulated as a continuous-depth model. Our algorithm solves a set of global optimization (Go) problems over a given time horizon to construct a tight enclosure (Tube) of the set of all process executions starting from a ball of initial states. We call our algorithm GoTube. Through its construction, GoTube ensures that the bounding tube is conservative up to a desired probability and up to a desired tightness.\r\n GoTube is implemented in JAX and optimized to scale to complex continuous-depth neural network models. Compared to advanced reachability analysis tools for time-continuous neural networks, GoTube does not accumulate overapproximation errors between time steps and avoids the infamous wrapping effect inherent in symbolic techniques. We show that GoTube substantially outperforms state-of-the-art verification tools in terms of the size of the initial ball, speed, time-horizon, task completion, and scalability on a large set of experiments.\r\n GoTube is stable and sets the state-of-the-art in terms of its ability to scale to time horizons well beyond what has been previously possible."}],"doi":"10.1609/aaai.v36i6.20631"},{"publication_identifier":{"isbn":["9781577358350"],"issn":["2159-5399"],"eissn":["2374-3468"]},"publisher":"Association for the Advancement of Artificial Intelligence","quality_controlled":"1","month":"06","status":"public","page":"7326-7336","day":"28","type":"journal_article","author":[{"first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"language":[{"iso":"eng"}],"oa":1,"issue":"7","_id":"12511","keyword":["General Medicine"],"corr_author":"1","article_processing_charge":"No","article_type":"original","oa_version":"Preprint","scopus_import":"1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme\r\nunder the Marie Skłodowska-Curie Grant Agreement No. 665385.","title":"Stability verification in stochastic control systems via neural network supermartingales","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"14539"}]},"arxiv":1,"citation":{"mla":"Lechner, Mathias, et al. “Stability Verification in Stochastic Control Systems via Neural Network Supermartingales.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 7, Association for the Advancement of Artificial Intelligence, 2022, pp. 7326–36, doi:<a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">10.1609/aaai.v36i7.20695</a>.","chicago":"Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, and Thomas A Henzinger. “Stability Verification in Stochastic Control Systems via Neural Network Supermartingales.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2022. <a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">https://doi.org/10.1609/aaai.v36i7.20695</a>.","short":"M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, Proceedings of the AAAI Conference on Artificial Intelligence 36 (2022) 7326–7336.","ieee":"M. Lechner, D. Zikelic, K. Chatterjee, and T. A. Henzinger, “Stability verification in stochastic control systems via neural network supermartingales,” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 7. Association for the Advancement of Artificial Intelligence, pp. 7326–7336, 2022.","ama":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA. Stability verification in stochastic control systems via neural network supermartingales. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. 2022;36(7):7326-7336. doi:<a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">10.1609/aaai.v36i7.20695</a>","apa":"Lechner, M., Zikelic, D., Chatterjee, K., &#38; Henzinger, T. A. (2022). Stability verification in stochastic control systems via neural network supermartingales. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">https://doi.org/10.1609/aaai.v36i7.20695</a>","ista":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA. 2022. Stability verification in stochastic control systems via neural network supermartingales. Proceedings of the AAAI Conference on Artificial Intelligence. 36(7), 7326–7336."},"date_created":"2023-02-05T17:29:50Z","main_file_link":[{"url":"https://arxiv.org/abs/2112.09495","open_access":"1"}],"year":"2022","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-04-07T13:27:55Z","volume":36,"date_published":"2022-06-28T00:00:00Z","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"doi":"10.1609/aaai.v36i7.20695","abstract":[{"text":"We consider the problem of formally verifying almost-sure (a.s.) asymptotic stability in discrete-time nonlinear stochastic control systems. While verifying stability in deterministic control systems is extensively studied in the literature, verifying stability in stochastic control systems is an open problem. The few existing works on this topic either consider only specialized forms of stochasticity or make restrictive assumptions on the system, rendering them inapplicable to learning algorithms with neural network policies. \r\n In this work, we present an approach for general nonlinear stochastic control problems with two novel aspects: (a) instead of classical stochastic extensions of Lyapunov functions, we use ranking supermartingales (RSMs) to certify a.s. asymptotic stability, and (b) we present a method for learning neural network RSMs. \r\n We prove that our approach guarantees a.s. asymptotic stability of the system and\r\n provides the first method to obtain bounds on the stabilization time, which stochastic Lyapunov functions do not.\r\n Finally, we validate our approach experimentally on a set of nonlinear stochastic reinforcement learning environments with neural network policies.","lang":"eng"}],"ec_funded":1,"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"external_id":{"arxiv":["2112.09495"]},"publication_status":"published","intvolume":"        36","publication":"Proceedings of the AAAI Conference on Artificial Intelligence"}]