[{"article_processing_charge":"No","day":"01","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"OA_type":"closed access","oa_version":"None","publication_status":"published","status":"public","doi":"10.1109/ICSE55347.2025.00092","date_updated":"2025-09-30T14:01:55Z","ec_funded":1,"month":"05","publication":"47th International Conference on Software Engineering","citation":{"chicago":"Richter, Cedric, Marek Chalupa, Marie-Christine Jakobs, and Heike Wehrheim. “Cooperative Software Verification via Dynamic Program Splitting.” In <i>47th International Conference on Software Engineering</i>, 2087–99. IEEE, 2025. <a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">https://doi.org/10.1109/ICSE55347.2025.00092</a>.","ista":"Richter C, Chalupa M, Jakobs M-C, Wehrheim H. 2025. Cooperative software verification via dynamic program splitting. 47th International Conference on Software Engineering. ICSE: International Conference on Software Engineering, 2087–2099.","mla":"Richter, Cedric, et al. “Cooperative Software Verification via Dynamic Program Splitting.” <i>47th International Conference on Software Engineering</i>, IEEE, 2025, pp. 2087–99, doi:<a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">10.1109/ICSE55347.2025.00092</a>.","short":"C. Richter, M. Chalupa, M.-C. Jakobs, H. Wehrheim, in:, 47th International Conference on Software Engineering, IEEE, 2025, pp. 2087–2099.","ama":"Richter C, Chalupa M, Jakobs M-C, Wehrheim H. Cooperative software verification via dynamic program splitting. In: <i>47th International Conference on Software Engineering</i>. IEEE; 2025:2087-2099. doi:<a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">10.1109/ICSE55347.2025.00092</a>","apa":"Richter, C., Chalupa, M., Jakobs, M.-C., &#38; Wehrheim, H. (2025). Cooperative software verification via dynamic program splitting. In <i>47th International Conference on Software Engineering</i> (pp. 2087–2099). Ottawa, ON, Canada: IEEE. <a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">https://doi.org/10.1109/ICSE55347.2025.00092</a>","ieee":"C. Richter, M. Chalupa, M.-C. Jakobs, and H. Wehrheim, “Cooperative software verification via dynamic program splitting,” in <i>47th International Conference on Software Engineering</i>, Ottawa, ON, Canada, 2025, pp. 2087–2099."},"year":"2025","external_id":{"isi":["001538318100163"]},"abstract":[{"text":"Cooperative software verification divides the task of software verification among several verification tools in order to increase efficiency and effectiveness. The basic approach is to let verifiers work on different parts of a program and at the end join verification results. While this idea is intuitively appealing, cooperative verification is usually hindered by the fact that program decomposition (1) is often static, disregarding strengths and weaknesses of employed verifiers, and (2) often represents the decomposed program parts in a specific proprietary format, thereby making the use of off-the-shelf verifiers in cooperative verification difficult. In this paper, we propose a novel cooperative verification scheme that we call dynamic program splitting (DPS). Splitting decomposes programs into (smaller) programs, and thus directly enables the use of off-the-shelf tools. In DPS, splitting is dynamically applied on demand: Verification starts by giving a verification task (a program plus a correctness specification) to a verifier V1. Whenever V1 finds the current task to be hard to verify, it splits the task (i.e., the program) and restarts verification on subtasks. DPS continues until (1) a violation is found, (2) all subtasks are completed or (3) some user-defined stopping criterion is met. In the latter case, the remaining uncompleted subtasks are merged into a single one and are given to a next verifier V2, repeating the same procedure on the still unverified program parts. This way, the decomposition is steered by what is hard to verify for particular verifiers, leveraging their complementary strengths. We have implemented dynamic program splitting and evaluated it on benchmarks of the annual software verification competition SV-COMP. The evaluation shows that cooperative verification with DPS is able to solve verification tasks that none of the constituent verifiers can solve, without any significant overhead.","lang":"eng"}],"quality_controlled":"1","department":[{"_id":"ToHe"}],"author":[{"first_name":"Cedric","last_name":"Richter","full_name":"Richter, Cedric"},{"full_name":"Chalupa, Marek","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa"},{"last_name":"Jakobs","first_name":"Marie-Christine","full_name":"Jakobs, Marie-Christine"},{"full_name":"Wehrheim, Heike","first_name":"Heike","last_name":"Wehrheim"}],"title":"Cooperative software verification via dynamic program splitting","type":"conference","corr_author":"1","publication_identifier":{"isbn":["9798331505691"],"eissn":["1558-1225"]},"date_published":"2025-05-01T00:00:00Z","_id":"20024","page":"2087-2099","date_created":"2025-07-16T11:32:29Z","scopus_import":"1","language":[{"iso":"eng"}],"acknowledgement":"This work is partially supported by the German Research Foundation (DFG) – WE2290/13-2 (Coop2), and in part by the ERC-2020-AdG 101020093.","conference":{"end_date":"2025-05-06","start_date":"2025-04-26","name":"ICSE: International Conference on Software Engineering","location":"Ottawa, ON, Canada"},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","isi":1,"publisher":"IEEE"},{"ddc":["000"],"doi":"10.15479/AT-ISTA-20147","status":"public","publication_status":"published","date_updated":"2026-04-07T12:02:57Z","article_processing_charge":"No","day":"07","file":[{"content_type":"application/x-zip-compressed","date_updated":"2025-09-10T08:19:51Z","file_size":8884801,"creator":"esarac","relation":"source_file","checksum":"0f3015f1db36576a23d8d669afb60b41","access_level":"closed","file_name":"2025_Sarac_NaciEge_Thesis.zip","file_id":"20200","date_created":"2025-08-21T09:40:28Z"},{"content_type":"application/pdf","creator":"esarac","date_updated":"2025-08-21T09:40:34Z","file_size":2955584,"checksum":"332ed2fe61f580641664ec3f05d30f14","access_level":"open_access","relation":"main_file","date_created":"2025-08-21T09:40:34Z","success":1,"file_id":"20201","file_name":"2025_Sarac_NaciEge_Thesis.pdf"}],"project":[{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"file_date_updated":"2025-09-10T08:19:51Z","oa":1,"oa_version":"Published Version","has_accepted_license":"1","supervisor":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"citation":{"chicago":"Sarac, Naci E. “A Monitoring-Oriented Theory and Classification of Quantitative Specifications.” Institute of Science and Technology Austria, 2025. <a href=\"https://doi.org/10.15479/AT-ISTA-20147\">https://doi.org/10.15479/AT-ISTA-20147</a>.","short":"N.E. Sarac, A Monitoring-Oriented Theory and Classification of Quantitative Specifications, Institute of Science and Technology Austria, 2025.","mla":"Sarac, Naci E. <i>A Monitoring-Oriented Theory and Classification of Quantitative Specifications</i>. Institute of Science and Technology Austria, 2025, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-20147\">10.15479/AT-ISTA-20147</a>.","ista":"Sarac NE. 2025. A monitoring-oriented theory and classification of quantitative specifications. Institute of Science and Technology Austria.","apa":"Sarac, N. E. (2025). <i>A monitoring-oriented theory and classification of quantitative specifications</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-20147\">https://doi.org/10.15479/AT-ISTA-20147</a>","ama":"Sarac NE. A monitoring-oriented theory and classification of quantitative specifications. 2025. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-20147\">10.15479/AT-ISTA-20147</a>","ieee":"N. E. Sarac, “A monitoring-oriented theory and classification of quantitative specifications,” Institute of Science and Technology Austria, 2025."},"year":"2025","ec_funded":1,"degree_awarded":"PhD","month":"08","related_material":{"record":[{"id":"11775","status":"public","relation":"part_of_dissertation"},{"id":"13140","relation":"part_of_dissertation","status":"deleted"},{"relation":"part_of_dissertation","status":"public","id":"19741"},{"status":"public","relation":"part_of_dissertation","id":"9356"},{"relation":"part_of_dissertation","status":"deleted","id":"19643"},{"id":"17634","relation":"part_of_dissertation","status":"public"},{"id":"20342","relation":"part_of_dissertation","status":"public"},{"id":"13221","status":"public","relation":"part_of_dissertation"}]},"title":"A monitoring-oriented theory and classification of quantitative specifications","publication_identifier":{"issn":["2663-337X"]},"type":"dissertation","license":"https://creativecommons.org/licenses/by/4.0/","corr_author":"1","abstract":[{"text":"Quantitative properties offer a framework for specifying and verifying system behaviors beyond the traditional boolean perspective. For example, while a boolean property may specify whether a server eventually grants every request it receives, a quantitative one may map each server execution to its average response time. This quantitative view is relatively well-studied in the context of static verification. However, although such properties often appear in practice as performance or robustness measures in a dynamic verification context, a general theoretical framework for their analysis and classification from a monitoring perspective is still missing.\r\n\r\nIn this thesis, we aim to develop such a framework that takes resource-precision tradeoffs of monitors as a central consideration. We present the first theory of monitorability for quantitative properties where monitors can be naturally approximate and compared regarding their precision and resource use. In particular, we show that additional monitor resources such as registers or states lead to strictly better approximations for some properties. To enable such analyses in a machine-model independent way, we describe an abstract notion of monitors that can be instantiated with concrete models of monitors. Within this framework, we study how abstract monitors behave and identify classes of properties amenable to approximate monitoring with resource-precision considerations. We then extend the boolean safety-liveness dichotomy and safety-progress hierarchy to the quantitative setting with a monitoring perspective. In particular, we prove that every property is the pointwise minimum of a safety property and a liveness property, and properties that are both safe and co-safe can be approximately monitored arbitrarily precisely using only finitely many states. We also study the classes of quantitative properties definable by finite-state quantitative automata and provide algorithms for deciding their safety or liveness as well as their safety-liveness decompositions. Finally, we present the first general-purpose tool for automating the analysis, verification, and monitoring of quantitative automata.\r\n\r\n-------------------------------------------------------------------------------------------------------------------------------------------------------------- In reference to IEEE copyrighted material which is used with permission in this thesis, the IEEE does not\r\nendorse any of ISTA's products or services. Internal or personal use of this\r\nmaterial is permitted. If interested in reprinting/republishing IEEE copyrighted material for advertising or promotional\r\npurposes or for creating new collective works for resale or redistribution, please go to\r\nhttp://www.ieee.org/publications_standards/publications/rights/rights_link.html to learn how to obtain a License from\r\nRightsLink.\r\n","lang":"eng"}],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"author":[{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E"}],"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","publisher":"Institute of Science and Technology Austria","date_published":"2025-08-07T00:00:00Z","page":"149","alternative_title":["ISTA Thesis"],"_id":"20147","OA_place":"publisher","date_created":"2025-08-07T15:57:57Z","acknowledgement":"This work was supported in part by the Austrian Science Fund (FWF)\r\nunder grant Z211-N23 (Wittgenstein Award) and the ERC-2020-AdG 101020093.\r\n","language":[{"iso":"eng"}]},{"publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"type":"journal_article","corr_author":"1","title":"Gray-box runtime enforcement of hyperproperties","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"ToHe"}],"author":[{"full_name":"Hsu, Tzu Han","last_name":"Hsu","first_name":"Tzu Han"},{"full_name":"Oliveira Da Costa, Ana A","first_name":"Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","last_name":"Oliveira Da Costa"},{"full_name":"Wintenberg, Andrew","last_name":"Wintenberg","first_name":"Andrew"},{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"full_name":"Bonakdarpour, Borzoo","last_name":"Bonakdarpour","first_name":"Borzoo"}],"quality_controlled":"1","abstract":[{"text":"Enforcement of information-flow policies has been extensively studied by language-based approaches over the past few decades. In this paper, we propose an alternative, novel, general, and effective approach using enforcement of hyperproperties– a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We study black- vs. gray- vs. white-box enforcement of hyperproperties expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer has null, some, or complete information about the implementation of the system under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce the problem to controller synthesis for hyperproperties and subsequently to the satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers are transferable with low-overhead. We conduct a rich set of case studies, including information-flow control for JavaScript code, as well as synthesizing obfuscators for control plants.","lang":"eng"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_type":"original","publisher":"Springer Nature","isi":1,"scopus_import":"1","date_created":"2025-08-17T22:01:36Z","issue":"3","OA_place":"publisher","acknowledgement":"This project was funded in part by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502, Vienna Science and Technology Fund (WWTF) [10.47379/ICT19018] (ProbInG) and WWTF project ICT22-023 (TAIGER), National Science Foundation (NSF) CPS Award 1837680, NSF award ECCS-2144416 and NSF SaTC Award 2245114. Open access funding provided by Institute of Science and Technology (IST Austria).","language":[{"iso":"eng"}],"date_published":"2025-09-01T00:00:00Z","article_number":"30","intvolume":"        62","_id":"20186","date_updated":"2025-09-30T14:20:11Z","ddc":["000"],"doi":"10.1007/s00236-025-00502-1","status":"public","PlanS_conform":"1","publication_status":"published","oa":1,"oa_version":"Published Version","OA_type":"hybrid","article_processing_charge":"Yes (via OA deal)","day":"01","volume":62,"file_date_updated":"2025-09-02T05:53:47Z","project":[{"grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy"}],"file":[{"success":1,"file_name":"2025_ActaInformatica_Hsu.pdf","file_id":"20267","date_created":"2025-09-02T05:53:47Z","relation":"main_file","checksum":"90a43350fd4a8c5cb5b1b0e1aea7970d","access_level":"open_access","date_updated":"2025-09-02T05:53:47Z","file_size":6505049,"creator":"dernst","content_type":"application/pdf"}],"external_id":{"isi":["001546115300001"]},"citation":{"chicago":"Hsu, Tzu Han, Ana A Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci, and Borzoo Bonakdarpour. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>.","ista":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. 2025. Gray-box runtime enforcement of hyperproperties. Acta Informatica. 62(3), 30.","mla":"Hsu, Tzu Han, et al. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>, vol. 62, no. 3, 30, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>.","short":"T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour, Acta Informatica 62 (2025).","apa":"Hsu, T. H., Oliveira da Costa, A. A., Wintenberg, A., Bartocci, E., &#38; Bonakdarpour, B. (2025). Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>","ama":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. 2025;62(3). doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>","ieee":"T. H. Hsu, A. A. Oliveira da Costa, A. Wintenberg, E. Bartocci, and B. Bonakdarpour, “Gray-box runtime enforcement of hyperproperties,” <i>Acta Informatica</i>, vol. 62, no. 3. Springer Nature, 2025."},"year":"2025","has_accepted_license":"1","publication":"Acta Informatica","month":"09"},{"type":"conference","publication_identifier":{"isbn":["9783031986673"],"issn":["0302-9743"],"eissn":["1611-3349"]},"title":"Introducing certificates to the hardware model checking competition","department":[{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"author":[{"first_name":"Nils","last_name":"Froleyks","full_name":"Froleyks, Nils"},{"full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","first_name":"Zhengqi","orcid":"0000-0002-4993-773X","last_name":"Yu"},{"last_name":"Preiner","first_name":"Mathias","full_name":"Preiner, Mathias"},{"last_name":"Biere","first_name":"Armin","full_name":"Biere, Armin"},{"full_name":"Heljanko, Keijo","last_name":"Heljanko","first_name":"Keijo"}],"abstract":[{"text":"Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.","lang":"eng"}],"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","isi":1,"publisher":"Springer Nature","conference":{"end_date":"2025-07-25","start_date":"2025-07-23","location":"Zagreb, Croatia","name":"CAV: Computer Aided Verification"},"date_created":"2025-08-17T22:01:36Z","OA_place":"publisher","scopus_import":"1","language":[{"iso":"eng"}],"acknowledgement":"This work is supported in part by the ERC-2020-AdG 101020093, the LIT AI Lab funded by the State of Upper Austria, the Research Council of Finland under the project 336092, and a gift from Intel Corporation.\r\nFurthermore we of course also owe a big thank-you to the submitters of model checkers and benchmarks to the competition over all these years. Without their enthusiasm and support neither the competition nor this study would exist.","date_published":"2025-01-01T00:00:00Z","_id":"20189","alternative_title":["LNCS"],"intvolume":"     15931","page":"281-295","date_updated":"2025-12-01T12:34:05Z","ddc":["000"],"status":"public","publication_status":"published","doi":"10.1007/978-3-031-98668-0_14","oa":1,"OA_type":"hybrid","oa_version":"Published Version","volume":15931,"day":"01","article_processing_charge":"Yes (in subscription journal)","file":[{"file_id":"20266","file_name":"2025_CAV_Froleyks.pdf","success":1,"date_created":"2025-09-02T05:46:10Z","relation":"main_file","access_level":"open_access","checksum":"15ec1bc9b9409d3b2736f4c9d5f42fd1","file_size":1078274,"date_updated":"2025-09-02T05:46:10Z","creator":"dernst","content_type":"application/pdf"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"}],"file_date_updated":"2025-09-02T05:46:10Z","year":"2025","citation":{"ieee":"N. Froleyks, E. Yu, M. Preiner, A. Biere, and K. Heljanko, “Introducing certificates to the hardware model checking competition,” in <i>37th International Conference on Computer Aided Verification</i>, Zagreb, Croatia, 2025, vol. 15931, pp. 281–295.","chicago":"Froleyks, Nils, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko. “Introducing Certificates to the Hardware Model Checking Competition.” In <i>37th International Conference on Computer Aided Verification</i>, 15931:281–95. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">https://doi.org/10.1007/978-3-031-98668-0_14</a>.","ista":"Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates to the hardware model checking competition. 37th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.","mla":"Froleyks, Nils, et al. “Introducing Certificates to the Hardware Model Checking Competition.” <i>37th International Conference on Computer Aided Verification</i>, vol. 15931, Springer Nature, 2025, pp. 281–95, doi:<a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">10.1007/978-3-031-98668-0_14</a>.","short":"N. Froleyks, E. Yu, M. Preiner, A. Biere, K. Heljanko, in:, 37th International Conference on Computer Aided Verification, Springer Nature, 2025, pp. 281–295.","ama":"Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing certificates to the hardware model checking competition. In: <i>37th International Conference on Computer Aided Verification</i>. Vol 15931. Springer Nature; 2025:281-295. doi:<a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">10.1007/978-3-031-98668-0_14</a>","apa":"Froleyks, N., Yu, E., Preiner, M., Biere, A., &#38; Heljanko, K. (2025). Introducing certificates to the hardware model checking competition. In <i>37th International Conference on Computer Aided Verification</i> (Vol. 15931, pp. 281–295). Zagreb, Croatia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">https://doi.org/10.1007/978-3-031-98668-0_14</a>"},"external_id":{"isi":["001562507100014"]},"has_accepted_license":"1","month":"01","publication":"37th International Conference on Computer Aided Verification","ec_funded":1},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","isi":1,"conference":{"name":"CAV: Computer Aided Verification","location":"Zagreb, Croatia","start_date":"2025-07-23","end_date":"2025-07-25"},"scopus_import":"1","date_created":"2025-08-24T22:01:31Z","OA_place":"publisher","acknowledgement":"This work was supported in part by the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SIS-SMU-100) and the ERC project ERC-2020-AdG 101020093.","language":[{"iso":"eng"}],"date_published":"2025-07-22T00:00:00Z","page":"29-55","intvolume":"     15932","_id":"20225","alternative_title":["LNCS"],"publication_identifier":{"isbn":["9783031986789"],"eissn":["1611-3349"],"issn":["0302-9743"]},"arxiv":1,"type":"conference","title":"Supermartingale certificates for quantitative omega-regular verification and control","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"ToHe"}],"author":[{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","last_name":"Mallik"},{"full_name":"Sadeghi, Pouya","first_name":"Pouya","last_name":"Sadeghi"},{"first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","last_name":"Zikelic","full_name":"Zikelic, Dorde"}],"abstract":[{"lang":"eng","text":"We present the first supermartingale certificate for quantitative \r\n-regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic Büchi automaton that specifies the property of interest; hence we call it a limit-deterministic Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied only to quantitative reachability, safety, or reach-avoid properties, and to qualitative (i.e., probability 1) \r\n-regular properties.We also present fully automated algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic system dynamics and the controller can be represented in terms of polynomial inequalities. Our experiments demonstrate the ability of our method to solve verification and control tasks for stochastic systems that were beyond the reach of previous supermartingale-based approaches."}],"quality_controlled":"1","external_id":{"arxiv":["2505.18833"],"isi":["001562506600002"]},"year":"2025","citation":{"ama":"Henzinger TA, Mallik K, Sadeghi P, Zikelic D. Supermartingale certificates for quantitative omega-regular verification and control. In: <i>37th International Conference on Computer Aided Verification</i>. Vol 15932. Springer Nature; 2025:29-55. doi:<a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">10.1007/978-3-031-98679-6_2</a>","apa":"Henzinger, T. A., Mallik, K., Sadeghi, P., &#38; Zikelic, D. (2025). Supermartingale certificates for quantitative omega-regular verification and control. In <i>37th International Conference on Computer Aided Verification</i> (Vol. 15932, pp. 29–55). Zagreb, Croatia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">https://doi.org/10.1007/978-3-031-98679-6_2</a>","chicago":"Henzinger, Thomas A, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic. “Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.” In <i>37th International Conference on Computer Aided Verification</i>, 15932:29–55. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">https://doi.org/10.1007/978-3-031-98679-6_2</a>.","short":"T.A. Henzinger, K. Mallik, P. Sadeghi, D. Zikelic, in:, 37th International Conference on Computer Aided Verification, Springer Nature, 2025, pp. 29–55.","mla":"Henzinger, Thomas A., et al. “Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.” <i>37th International Conference on Computer Aided Verification</i>, vol. 15932, Springer Nature, 2025, pp. 29–55, doi:<a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">10.1007/978-3-031-98679-6_2</a>.","ista":"Henzinger TA, Mallik K, Sadeghi P, Zikelic D. 2025. Supermartingale certificates for quantitative omega-regular verification and control. 37th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15932, 29–55.","ieee":"T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic, “Supermartingale certificates for quantitative omega-regular verification and control,” in <i>37th International Conference on Computer Aided Verification</i>, Zagreb, Croatia, 2025, vol. 15932, pp. 29–55."},"has_accepted_license":"1","month":"07","publication":"37th International Conference on Computer Aided Verification","ec_funded":1,"date_updated":"2025-12-01T12:34:41Z","ddc":["000"],"doi":"10.1007/978-3-031-98679-6_2","status":"public","publication_status":"published","oa":1,"oa_version":"Published Version","OA_type":"hybrid","day":"22","article_processing_charge":"Yes (in subscription journal)","volume":15932,"file":[{"success":1,"file_id":"20272","file_name":"2025_CAV_HenzingerT.pdf","date_created":"2025-09-02T07:34:33Z","relation":"main_file","access_level":"open_access","checksum":"beb1e2637de5b2268cc2262119439113","date_updated":"2025-09-02T07:34:33Z","file_size":884831,"creator":"dernst","content_type":"application/pdf"}],"project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"file_date_updated":"2025-09-02T07:34:33Z"},{"ec_funded":1,"publication":"36th International Conference on Concurrency Theory","month":"08","has_accepted_license":"1","citation":{"ama":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Quantitative language automata. In: <i>36th International Conference on Concurrency Theory</i>. Vol 348. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">10.4230/LIPIcs.CONCUR.2025.21</a>","apa":"Henzinger, T. A., Kebis, P., Mazzocchi, N. A., &#38; Sarac, N. E. (2025). Quantitative language automata. In <i>36th International Conference on Concurrency Theory</i> (Vol. 348). Aarhus, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2025.21</a>","short":"T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 36th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025.","mla":"Henzinger, Thomas A., et al. “Quantitative Language Automata.” <i>36th International Conference on Concurrency Theory</i>, vol. 348, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">10.4230/LIPIcs.CONCUR.2025.21</a>.","ista":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2025. Quantitative language automata. 36th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 348, 21.","chicago":"Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Language Automata.” In <i>36th International Conference on Concurrency Theory</i>, Vol. 348. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2025.21</a>.","ieee":"T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Quantitative language automata,” in <i>36th International Conference on Concurrency Theory</i>, Aarhus, Denmark, 2025, vol. 348."},"year":"2025","external_id":{"arxiv":["2506.0515"],"isi":["001570540800021"]},"project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"file_date_updated":"2025-09-03T10:01:53Z","file":[{"date_created":"2025-09-03T10:01:53Z","success":1,"file_id":"20282","file_name":"2025_CONCUR_HenzingerT.pdf","access_level":"open_access","checksum":"9d4054058757a73477e6015b10ed6996","relation":"main_file","creator":"dernst","date_updated":"2025-09-03T10:01:53Z","file_size":1257397,"content_type":"application/pdf"}],"volume":348,"day":"18","article_processing_charge":"No","OA_type":"gold","oa_version":"Published Version","oa":1,"status":"public","publication_status":"published","doi":"10.4230/LIPIcs.CONCUR.2025.21","ddc":["000"],"date_updated":"2025-12-01T12:36:52Z","alternative_title":["LIPIcs"],"_id":"20253","intvolume":"       348","article_number":"21","date_published":"2025-08-18T00:00:00Z","language":[{"iso":"eng"}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.","OA_place":"publisher","date_created":"2025-08-31T22:01:32Z","scopus_import":"1","conference":{"name":"CONCUR: Conference on Concurrency Theory","location":"Aarhus, Denmark","start_date":"2025-08-26","end_date":"2025-08-29"},"isi":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","abstract":[{"lang":"eng","text":"A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA 𝒜 obtains a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained by nondeterministic runs of 𝒜 over w. We introduce quantitative language automata (QLAs) that define functions from language generators (i.e., implementations) to values, where a language generator can be nonprobabilistic, defining a set of infinite words, or probabilistic, defining a probability measure over infinite words. A QLA consists of a QWA and an aggregator function. For example, given a QWA 𝒜, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest lower bound assigned by 𝒜 to any word in L. For boolean value sets, QWAs define boolean properties of traces, and QLAs define boolean properties of sets of traces, i.e., hyperproperties. For more general value sets, QLAs serve as a specification language for a generalization of hyperproperties, called quantitative hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty assigns a value to each set (resp. distribution) G of traces, e.g., the minimal (resp. expected) average response time exhibited by the traces in G. We give several examples of quantitative hyperproperties and investigate three paradigmatic problems for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem, given a QLA 𝔸 and an implementation G, we ask for the value that 𝔸 assigns to G. In the nonemptiness (resp. universality) problem, given a QLA 𝔸 and a value k, we ask whether 𝔸 assigns at least k to some (resp. every) language. We provide a comprehensive picture of decidability for these problems for QLAs with common aggregators as well as their restrictions to ω-regular languages and trace distributions generated by finite-state Markov chains."}],"author":[{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Kebis, Pavol","last_name":"Kebis","first_name":"Pavol","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a"},{"full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi","first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"full_name":"Sarac, Naci E","last_name":"Sarac","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"department":[{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"title":"Quantitative language automata","type":"conference","corr_author":"1","arxiv":1,"publication_identifier":{"isbn":["9783959773898"],"issn":["1868-8969"]}},{"ec_funded":1,"publication":"7th Annual Learning for Dynamics & Control Conference","month":"06","has_accepted_license":"1","year":"2025","citation":{"ama":"Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. Predictive monitoring of black-box dynamical systems. In: <i>7th Annual Learning for Dynamics &#38; Control Conference</i>. Vol 283. ML Research Press; 2025:804-816.","apa":"Henzinger, T. A., Kresse, F., Mallik, K., Yu, E., &#38; Zikelic, D. (2025). Predictive monitoring of black-box dynamical systems. In <i>7th Annual Learning for Dynamics &#38; Control Conference</i> (Vol. 283, pp. 804–816). Ann Arbor, MI, United States: ML Research Press.","ista":"Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. 2025. Predictive monitoring of black-box dynamical systems. 7th Annual Learning for Dynamics &#38; Control Conference. L4DC: Learning for Dynamics &#38; Control, PMLR, vol. 283, 804–816.","mla":"Henzinger, Thomas A., et al. “Predictive Monitoring of Black-Box Dynamical Systems.” <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, vol. 283, ML Research Press, 2025, pp. 804–16.","short":"T.A. Henzinger, F. Kresse, K. Mallik, E. Yu, D. Zikelic, in:, 7th Annual Learning for Dynamics &#38; Control Conference, ML Research Press, 2025, pp. 804–816.","chicago":"Henzinger, Thomas A, Fabian Kresse, Kaushik Mallik, Emily Yu, and Dorde Zikelic. “Predictive Monitoring of Black-Box Dynamical Systems.” In <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, 283:804–16. ML Research Press, 2025.","ieee":"T. A. Henzinger, F. Kresse, K. Mallik, E. Yu, and D. Zikelic, “Predictive monitoring of black-box dynamical systems,” in <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, Ann Arbor, MI, United States, 2025, vol. 283, pp. 804–816."},"external_id":{"arxiv":["2412.16564"]},"volume":283,"day":"01","article_processing_charge":"No","file":[{"checksum":"d5236e561560635f5ae1d17de4903033","access_level":"open_access","relation":"main_file","date_created":"2025-09-03T10:32:12Z","success":1,"file_name":"2025_L4DC_HenzingerT.pdf","file_id":"20283","content_type":"application/pdf","creator":"dernst","date_updated":"2025-09-03T10:32:12Z","file_size":489639}],"file_date_updated":"2025-09-03T10:32:12Z","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"oa":1,"OA_type":"gold","oa_version":"Published Version","ddc":["000"],"status":"public","publication_status":"published","date_updated":"2025-09-03T10:37:59Z","date_published":"2025-06-01T00:00:00Z","alternative_title":["PMLR"],"_id":"20256","intvolume":"       283","page":"804-816","date_created":"2025-08-31T22:01:32Z","OA_place":"publisher","scopus_import":"1","language":[{"iso":"eng"}],"acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093.\r\n","conference":{"end_date":"2025-06-06","location":"Ann Arbor, MI, United States","name":"L4DC: Learning for Dynamics & Control","start_date":"2025-06-04"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"ML Research Press","abstract":[{"lang":"eng","text":"We study the problem of predictive runtime monitoring of black-box dynamical systems with quantitative safety properties. The black-box setting stipulates that the exact semantics of the dynamical system and the controller are unknown, and that we are only able to observe the state of the controlled (aka, closed-loop) system at finitely many time points. We present a novel framework for predicting future states of the system based on the states observed in the past. The numbers of past states and of predicted future states are parameters provided by the user. Our method is based on a combination of Taylor’s expansion and the backward difference operator for numerical differentiation. We also derive an upper bound on the prediction error under the assumption that the system dynamics and the controller are smooth. The predicted states are then used to predict safety violations ahead in time. Our experiments demonstrate practical applicability of our method for complex black-box systems, showing that it is computationally lightweight and yet significantly more accurate than the state-of-the-art predictive safety monitoring techniques."}],"quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"ChLa"}],"author":[{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Kresse, Fabian","first_name":"Fabian","id":"faff3c84-23f6-11ef-9085-e5187b51c604","last_name":"Kresse"},{"orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","last_name":"Mallik","full_name":"Mallik, Kaushik"},{"id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","first_name":"Zhengqi","last_name":"Yu","full_name":"Yu, Zhengqi"},{"orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","full_name":"Zikelic, Dorde"}],"title":"Predictive monitoring of black-box dynamical systems","corr_author":"1","type":"conference","publication_identifier":{"eissn":["2640-3498"]},"arxiv":1},{"file":[{"file_id":"20306","file_name":"2025_MFCS_Brice.pdf","success":1,"date_created":"2025-09-08T07:11:12Z","relation":"main_file","checksum":"9bc6b8e537662d371d2a27444cbc0b75","access_level":"open_access","file_size":1149694,"date_updated":"2025-09-08T07:11:12Z","creator":"dernst","content_type":"application/pdf"}],"project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"file_date_updated":"2025-09-08T07:11:12Z","article_processing_charge":"Yes","day":"20","volume":345,"oa_version":"Published Version","OA_type":"gold","oa":1,"doi":"10.4230/LIPIcs.MFCS.2025.30","publication_status":"published","status":"public","ddc":["000"],"date_updated":"2025-09-08T07:15:40Z","ec_funded":1,"month":"08","publication":"50th International Symposium on Mathematical Foundations of Computer Science","has_accepted_license":"1","external_id":{"arxiv":["2502.0531"]},"year":"2025","citation":{"ieee":"L. Brice, T. A. Henzinger, and K. S. Thejaswini, “Finding equilibria: Simpler for pessimists, simplest for optimists,” in <i>50th International Symposium on Mathematical Foundations of Computer Science</i>, Warsaw, Poland, 2025, vol. 345.","chicago":"Brice, Léonard, Thomas A Henzinger, and K. S. Thejaswini. “Finding Equilibria: Simpler for Pessimists, Simplest for Optimists.” In <i>50th International Symposium on Mathematical Foundations of Computer Science</i>, Vol. 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.30\">https://doi.org/10.4230/LIPIcs.MFCS.2025.30</a>.","short":"L. Brice, T.A. Henzinger, K.S. Thejaswini, in:, 50th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025.","mla":"Brice, Léonard, et al. “Finding Equilibria: Simpler for Pessimists, Simplest for Optimists.” <i>50th International Symposium on Mathematical Foundations of Computer Science</i>, vol. 345, 30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.30\">10.4230/LIPIcs.MFCS.2025.30</a>.","ista":"Brice L, Henzinger TA, Thejaswini KS. 2025. Finding equilibria: Simpler for pessimists, simplest for optimists. 50th International Symposium on Mathematical Foundations of Computer Science. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 345, 30.","apa":"Brice, L., Henzinger, T. A., &#38; Thejaswini, K. S. (2025). Finding equilibria: Simpler for pessimists, simplest for optimists. In <i>50th International Symposium on Mathematical Foundations of Computer Science</i> (Vol. 345). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.30\">https://doi.org/10.4230/LIPIcs.MFCS.2025.30</a>","ama":"Brice L, Henzinger TA, Thejaswini KS. Finding equilibria: Simpler for pessimists, simplest for optimists. In: <i>50th International Symposium on Mathematical Foundations of Computer Science</i>. Vol 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.30\">10.4230/LIPIcs.MFCS.2025.30</a>"},"quality_controlled":"1","abstract":[{"text":"We consider equilibria in multiplayer stochastic graph games with terminal-node rewards. In such games, Nash equilibria are defined assuming that each player seeks to maximise their expected payoff, ignoring their aversion or tolerance to risk. We therefore study risk-sensitive equilibria (RSEs), where the expected payoff is replaced by a risk measure. A classical risk measure in the literature is the entropic risk measure, where each player has a real valued parameter capturing their risk-averseness. We introduce the extreme risk measure, which corresponds to extreme cases of entropic risk measure, where players are either extreme optimists or extreme pessimists. Under extreme risk measure, every player is an extremist: an extreme optimist perceives their reward as the maximum payoff that can be achieved with positive probability, while an extreme pessimist expects the minimum payoff achievable with positive probability. We argue that the extreme risk measure, especially in multi-player graph based settings, is particularly relevant as they can model several real life instances such as interactions between secure systems and potential security threats, or distributed controls for safety critical systems. We prove that RSEs defined with the extreme risk measure are guaranteed to exist when all rewards are non-negative. Furthermore, we prove that the problem of deciding whether a given game contains an RSE that generates risk measures within specified intervals is decidable and NP-complete for our extreme risk measure, and even PTIME-complete when all players are extreme optimists, while that same problem is undecidable using the entropic risk measure or even the classical expected payoff. This establishes, to our knowledge, the first decidable fragment for equilibria in simple stochastic games without restrictions on strategy types or number of players.","lang":"eng"}],"author":[{"full_name":"Brice, Léonard","first_name":"Léonard","last_name":"Brice"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Thejaswini, K. S.","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","first_name":"K. S.","last_name":"Thejaswini"}],"department":[{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"title":"Finding equilibria: Simpler for pessimists, simplest for optimists","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773881"]},"arxiv":1,"corr_author":"1","type":"conference","article_number":"30","_id":"20290","intvolume":"       345","alternative_title":["LIPIcs"],"date_published":"2025-08-20T00:00:00Z","acknowledgement":"This work is a part of project VAMOS that has received funding from the European\r\nResearch Council (ERC), grant agreement No 101020093. We thank anonymous reviewers for pointing us to the Hurwicz criterion and to the work of Gallego-Hernández and Mansutti [13]. We thank Marie van den Bogaard for her valuable feedback on the first author’s PhD dissertation, which helped improve the quality of this work. ","language":[{"iso":"eng"}],"scopus_import":"1","OA_place":"publisher","date_created":"2025-09-07T22:01:32Z","conference":{"start_date":"2025-08-25","name":"MFCS: Mathematical Foundations of Computer Science","location":"Warsaw, Poland","end_date":"2025-08-29"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"date_published":"2025-08-20T00:00:00Z","intvolume":"       345","_id":"20291","alternative_title":["LIPIcs"],"article_number":"57","date_created":"2025-09-07T22:01:32Z","OA_place":"publisher","scopus_import":"1","language":[{"iso":"eng"}],"acknowledgement":"This work is a part of project VAMOS that has received funding from the European Research Council (ERC), grant agreement No 101020093.","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","location":"Warsaw, Poland","start_date":"2025-08-25","end_date":"2025-08-29"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","abstract":[{"lang":"eng","text":"We define and study classes of ω-regular automata for which the nondeterminism can be resolved by a policy that uses a combination of memory and randomness on any input word, based solely on the prefix read so far. We examine two settings for providing the input word to an automaton. In the first setting, called adversarial resolvability, the input word is constructed letter-by-letter by an adversary, dependent on the resolver’s previous decisions. In the second setting, called stochastic resolvability, the adversary pre-commits to an infinite word and reveals it letter-by-letter. In each setting, we require the existence of an almost-sure resolver, i.e., a policy that ensures that as long as the adversary provides a word in the language of the underlying nondeterministic automaton, the run constructed by the policy is accepting with probability 1.\r\nThe class of automata that are adversarially resolvable is the well-studied class of history-deterministic automata. The case of stochastically resolvable automata, on the other hand, defines a novel class. Restricting the class of resolvers in both settings to stochastic policies without memory introduces two additional new classes of automata. We show that the new automata classes offer interesting trade-offs between succinctness, expressivity, and computational complexity, providing a fine gradation between deterministic automata and nondeterministic automata."}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"ToHe"}],"author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"last_name":"Prakash","first_name":"Aditya","full_name":"Prakash, Aditya"},{"last_name":"Thejaswini","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","first_name":"K. S.","full_name":"Thejaswini, K. S."}],"title":"Resolving nondeterminism with randomness","type":"conference","corr_author":"1","publication_identifier":{"isbn":["9783959773881"],"issn":["1868-8969"]},"arxiv":1,"ec_funded":1,"publication":"50th International Symposium on Mathematical Foundations of Computer Science","month":"08","has_accepted_license":"1","year":"2025","citation":{"mla":"Henzinger, Thomas A., et al. “Resolving Nondeterminism with Randomness.” <i>50th International Symposium on Mathematical Foundations of Computer Science</i>, vol. 345, 57, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.57\">10.4230/LIPIcs.MFCS.2025.57</a>.","short":"T.A. Henzinger, A. Prakash, K.S. Thejaswini, in:, 50th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025.","ista":"Henzinger TA, Prakash A, Thejaswini KS. 2025. Resolving nondeterminism with randomness. 50th International Symposium on Mathematical Foundations of Computer Science. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 345, 57.","chicago":"Henzinger, Thomas A, Aditya Prakash, and K. S. Thejaswini. “Resolving Nondeterminism with Randomness.” In <i>50th International Symposium on Mathematical Foundations of Computer Science</i>, Vol. 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.57\">https://doi.org/10.4230/LIPIcs.MFCS.2025.57</a>.","ama":"Henzinger TA, Prakash A, Thejaswini KS. Resolving nondeterminism with randomness. In: <i>50th International Symposium on Mathematical Foundations of Computer Science</i>. Vol 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.57\">10.4230/LIPIcs.MFCS.2025.57</a>","apa":"Henzinger, T. A., Prakash, A., &#38; Thejaswini, K. S. (2025). Resolving nondeterminism with randomness. In <i>50th International Symposium on Mathematical Foundations of Computer Science</i> (Vol. 345). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.57\">https://doi.org/10.4230/LIPIcs.MFCS.2025.57</a>","ieee":"T. A. Henzinger, A. Prakash, and K. S. Thejaswini, “Resolving nondeterminism with randomness,” in <i>50th International Symposium on Mathematical Foundations of Computer Science</i>, Warsaw, Poland, 2025, vol. 345."},"external_id":{"arxiv":["2502.12872"]},"volume":345,"article_processing_charge":"No","day":"20","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"file":[{"relation":"main_file","access_level":"open_access","checksum":"6068b772aba6cb0d01f3e5a90abed973","success":1,"file_id":"20305","file_name":"2025_MFCS_HenzingerT.pdf","date_created":"2025-09-08T06:56:56Z","content_type":"application/pdf","date_updated":"2025-09-08T06:56:56Z","file_size":1009644,"creator":"dernst"}],"file_date_updated":"2025-09-08T06:56:56Z","oa":1,"OA_type":"gold","oa_version":"Published Version","ddc":["000"],"publication_status":"published","status":"public","doi":"10.4230/LIPIcs.MFCS.2025.57","date_updated":"2025-09-08T07:06:11Z"},{"external_id":{"arxiv":["2506.00496"]},"year":"2025","citation":{"ama":"Gupta A, Henzinger TA, Kueffner K, Mallik K, Pape D. Monitoring robustness and individual fairness. In: <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>. Vol 2. Association for Computing Machinery; 2025:790-801. doi:<a href=\"https://doi.org/10.1145/3711896.3737054\">10.1145/3711896.3737054</a>","apa":"Gupta, A., Henzinger, T. A., Kueffner, K., Mallik, K., &#38; Pape, D. (2025). Monitoring robustness and individual fairness. In <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i> (Vol. 2, pp. 790–801). Toronto, Canada: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3711896.3737054\">https://doi.org/10.1145/3711896.3737054</a>","chicago":"Gupta, Ashutosh, Thomas A Henzinger, Konstantin Kueffner, Kaushik Mallik, and David Pape. “Monitoring Robustness and Individual Fairness.” In <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>, 2:790–801. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3711896.3737054\">https://doi.org/10.1145/3711896.3737054</a>.","ista":"Gupta A, Henzinger TA, Kueffner K, Mallik K, Pape D. 2025. Monitoring robustness and individual fairness. Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining. KDD: Conference on Knowledge Discovery and Data Mining vol. 2, 790–801.","mla":"Gupta, Ashutosh, et al. “Monitoring Robustness and Individual Fairness.” <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>, vol. 2, Association for Computing Machinery, 2025, pp. 790–801, doi:<a href=\"https://doi.org/10.1145/3711896.3737054\">10.1145/3711896.3737054</a>.","short":"A. Gupta, T.A. Henzinger, K. Kueffner, K. Mallik, D. Pape, in:, Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining, Association for Computing Machinery, 2025, pp. 790–801.","ieee":"A. Gupta, T. A. Henzinger, K. Kueffner, K. Mallik, and D. Pape, “Monitoring robustness and individual fairness,” in <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>, Toronto, Canada, 2025, vol. 2, pp. 790–801."},"has_accepted_license":"1","month":"08","publication":"Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining","ec_funded":1,"date_updated":"2025-09-08T08:54:24Z","doi":"10.1145/3711896.3737054","status":"public","publication_status":"published","ddc":["000"],"oa_version":"Published Version","oa":1,"project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"file":[{"file_size":7745940,"date_updated":"2025-09-08T08:46:31Z","creator":"dernst","content_type":"application/pdf","file_name":"2025_KDD_Gupta.pdf","file_id":"20310","success":1,"date_created":"2025-09-08T08:46:31Z","relation":"main_file","access_level":"open_access","checksum":"81e18cdf9ca5f6dfa79425b326ea9725"}],"file_date_updated":"2025-09-08T08:46:31Z","article_processing_charge":"No","day":"03","volume":2,"publisher":"Association for Computing Machinery","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2025-08-07","start_date":"2025-08-03","name":"KDD: Conference on Knowledge Discovery and Data Mining","location":"Toronto, Canada"},"acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093 and the SBI Foundation Hub for Data Science &Analytics, IIT Bombay.","language":[{"iso":"eng"}],"scopus_import":"1","date_created":"2025-09-07T22:01:33Z","OA_place":"publisher","page":"790-801","_id":"20292","intvolume":"         2","date_published":"2025-08-03T00:00:00Z","publication_identifier":{"issn":["2154-817X"],"isbn":["9798400714542"]},"arxiv":1,"type":"conference","corr_author":"1","title":"Monitoring robustness and individual fairness","related_material":{"link":[{"relation":"software","url":"https://github.com/ariez-xyz/clemont"}]},"author":[{"full_name":"Gupta, Ashutosh","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Kueffner, Konstantin","last_name":"Kueffner","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","orcid":"0000-0001-8974-2542","first_name":"Konstantin"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","orcid":"0000-0001-9864-7475","last_name":"Mallik","full_name":"Mallik, Kaushik"},{"full_name":"Pape, David","last_name":"Pape","first_name":"David"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"ToHe"}],"abstract":[{"text":"In automated decision-making, it is desirable that outputs of decision-makers be robust to slight perturbations in their inputs, a property that may be called input-output robustness. Input-output robustness appears in various different forms in the literature, such as robustness of AI models to adversarial or semantic perturbations and individual fairness of AI models that make decisions about humans. We propose runtime monitoring of input-output robustness of deployed, black-box AI models, where the goal is to design monitors that would observe one long execution sequence of the model, and would raise an alarm whenever it is detected that two similar inputs from the past led to dissimilar outputs. This way, monitoring will complement existing offline ''robustification'' approaches to increase the trustworthiness of AI decision-makers. We show that the monitoring problem can be cast as the fixed-radius nearest neighbor (FRNN) search problem, which, despite being well-studied, lacks suitable online solutions. We present our tool Clemont, which offers a number of lightweight monitors, some of which use upgraded online variants of existing FRNN algorithms, and one uses a novel algorithm based on binary decision diagrams--a data-structure commonly used in software and hardware verification. We have also developed an efficient parallelization technique that can substantially cut down the computation time of monitors for which the distance between input-output pairs is measured using the L∞norm. Using standard benchmarks from the literature of adversarial and semantic robustness and individual fairness, we perform a comparative study of different monitors in Clemont, and demonstrate their effectiveness in correctly detecting robustness violations at runtime.","lang":"eng"}],"quality_controlled":"1"},{"ec_funded":1,"publication":"2nd International Conferenceon Neuro-Symbolic Systems","month":"06","acknowledged_ssus":[{"_id":"ScienComp"}],"has_accepted_license":"1","external_id":{"arxiv":["2505.19932"]},"year":"2025","citation":{"ieee":"F. Kresse, E. Yu, C. Lampert, and T. A. Henzinger, “Logic gate neural networks are good for verification,” in <i>2nd International Conferenceon Neuro-Symbolic Systems</i>, Philadephia, PA, United States, 2025, vol. 288.","ama":"Kresse F, Yu E, Lampert C, Henzinger TA. Logic gate neural networks are good for verification. In: <i>2nd International Conferenceon Neuro-Symbolic Systems</i>. Vol 288. ML Research Press; 2025.","apa":"Kresse, F., Yu, E., Lampert, C., &#38; Henzinger, T. A. (2025). Logic gate neural networks are good for verification. In <i>2nd International Conferenceon Neuro-Symbolic Systems</i> (Vol. 288). Philadephia, PA, United States: ML Research Press.","chicago":"Kresse, Fabian, Emily Yu, Christoph Lampert, and Thomas A Henzinger. “Logic Gate Neural Networks Are Good for Verification.” In <i>2nd International Conferenceon Neuro-Symbolic Systems</i>, Vol. 288. ML Research Press, 2025.","mla":"Kresse, Fabian, et al. “Logic Gate Neural Networks Are Good for Verification.” <i>2nd International Conferenceon Neuro-Symbolic Systems</i>, vol. 288, 26, ML Research Press, 2025.","short":"F. Kresse, E. Yu, C. Lampert, T.A. Henzinger, in:, 2nd International Conferenceon Neuro-Symbolic Systems, ML Research Press, 2025.","ista":"Kresse F, Yu E, Lampert C, Henzinger TA. 2025. Logic gate neural networks are good for verification. 2nd International Conferenceon Neuro-Symbolic Systems. NeuS: International Conferenceon Neuro-Symbolic Systems, PMLR, vol. 288, 26."},"file":[{"date_created":"2025-09-09T08:10:13Z","success":1,"file_id":"20314","file_name":"2025_NeuS_Kresse.pdf","access_level":"open_access","checksum":"90a32defed34787e771a5c1623b6b0d2","relation":"main_file","creator":"dernst","date_updated":"2025-09-09T08:10:13Z","file_size":295466,"content_type":"application/pdf"}],"file_date_updated":"2025-09-09T08:10:13Z","project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"day":"01","article_processing_charge":"No","volume":288,"oa_version":"Published Version","OA_type":"diamond","oa":1,"publication_status":"published","status":"public","ddc":["000"],"date_updated":"2025-09-09T08:12:44Z","article_number":"26","intvolume":"       288","_id":"20296","alternative_title":["PMLR"],"date_published":"2025-06-01T00:00:00Z","acknowledgement":"This work is supported in part by the ERC grant under Grant No. ERC-2020-AdG 101020093 and\r\nthe Austrian Science Fund (FWF) [10.55776/COE12]. This research was supported by the Scientific\r\nService Units (SSU) of ISTA through resources provided by Scientific Computing (SciComp).","language":[{"iso":"eng"}],"scopus_import":"1","OA_place":"publisher","date_created":"2025-09-07T22:01:34Z","conference":{"location":"Philadephia, PA, United States","name":"NeuS: International Conferenceon Neuro-Symbolic Systems","start_date":"2025-05-28","end_date":"2025-05-30"},"publisher":"ML Research Press","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"Learning-based systems are increasingly deployed across various domains, yet the complexity of traditional neural networks poses significant challenges for formal verification. Unlike conventional neural networks, learned Logic Gate Networks (LGNs) replace multiplications with Boolean logic gates, yielding a sparse, netlist-like architecture that is inherently more amenable to symbolic verification, while still delivering promising performance. In this paper, we introduce a SAT encoding for verifying global robustness and fairness in LGNs. We evaluate our method on five benchmark datasets, including a newly constructed 5-class variant, and find that LGNs are both verification-friendly and maintain strong predictive performance."}],"quality_controlled":"1","author":[{"id":"faff3c84-23f6-11ef-9085-e5187b51c604","first_name":"Fabian","last_name":"Kresse","full_name":"Kresse, Fabian"},{"full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","first_name":"Zhengqi","last_name":"Yu"},{"last_name":"Lampert","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8622-7887","first_name":"Christoph","full_name":"Lampert, Christoph"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"}],"department":[{"_id":"ChLa"},{"_id":"ToHe"}],"title":"Logic gate neural networks are good for verification","publication_identifier":{"eissn":["2640-3498"]},"arxiv":1,"corr_author":"1","type":"conference"},{"volume":21,"article_processing_charge":"Yes","day":"08","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"file":[{"creator":"esarac","file_size":709584,"date_updated":"2025-09-11T12:17:12Z","content_type":"application/pdf","date_created":"2025-09-11T12:17:12Z","file_name":"2307.06016.pdf","file_id":"20343","success":1,"checksum":"0b4d477bd981379724c35a4de2c176e5","access_level":"open_access","relation":"main_file"}],"file_date_updated":"2025-09-11T12:17:12Z","oa":1,"OA_type":"gold","oa_version":"Published Version","ddc":["000"],"publication_status":"published","status":"public","PlanS_conform":"1","doi":"10.46298/lmcs-21(2:2)2025","DOAJ_listed":"1","date_updated":"2026-04-07T12:02:57Z","ec_funded":1,"publication":"Logical Methods in Computer Science","month":"04","has_accepted_license":"1","year":"2025","citation":{"chicago":"Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “ Safety and Liveness of Quantitative Properties and Automata.” <i>Logical Methods in Computer Science</i>. EPI Sciences, 2025. <a href=\"https://doi.org/10.46298/lmcs-21(2:2)2025\">https://doi.org/10.46298/lmcs-21(2:2)2025</a>.","mla":"Boker, Udi, et al. “ Safety and Liveness of Quantitative Properties and Automata.” <i>Logical Methods in Computer Science</i>, vol. 21, no. 2, 13149, EPI Sciences, 2025, doi:<a href=\"https://doi.org/10.46298/lmcs-21(2:2)2025\">10.46298/lmcs-21(2:2)2025</a>.","short":"U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, Logical Methods in Computer Science 21 (2025).","ista":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2025.  Safety and liveness of quantitative properties and automata. Logical Methods in Computer Science. 21(2), 13149.","apa":"Boker, U., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2025).  Safety and liveness of quantitative properties and automata. <i>Logical Methods in Computer Science</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/lmcs-21(2:2)2025\">https://doi.org/10.46298/lmcs-21(2:2)2025</a>","ama":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE.  Safety and liveness of quantitative properties and automata. <i>Logical Methods in Computer Science</i>. 2025;21(2). doi:<a href=\"https://doi.org/10.46298/lmcs-21(2:2)2025\">10.46298/lmcs-21(2:2)2025</a>","ieee":"U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “ Safety and liveness of quantitative properties and automata,” <i>Logical Methods in Computer Science</i>, vol. 21, no. 2. EPI Sciences, 2025."},"external_id":{"arxiv":["2307.06016"],"isi":["001468887900001"]},"abstract":[{"text":"Safety and liveness stand as fundamental concepts in formal languages, playing a key role in verification. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In the quantitative setting, properties are arbitrary functions from infinite words to partially-ordered domains. Extending this paradigm to the quantitative domain, where properties are arbitrary functions mapping infinite words to partially-ordered domains, we introduce and study the notions of quantitative safety and liveness. First, we formally define quantitative safety and liveness, and prove that our definitions induce conservative quantitative generalizations of both the safety-progress hierarchy and the safety-liveness decomposition of boolean properties. Consequently, like their boolean counterparts, quantitative properties can be min-decomposed into safety and liveness parts, or alternatively, max-decomposed into co-safety and co-liveness parts. We further establish a connection between quantitative safety and topological continuity and provide alternative characterizations of quantitative safety and liveness in terms of their boolean analogs. Second, we instantiate our framework with the specific classes of quantitative properties expressed by automata. These quantitative 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 totally-ordered domain of real numbers. For all common value functions, we provide a procedure for deciding whether a given automaton is safe or live, we show how to construct its safety closure, and we present a min-decomposition into safe and live automata.","lang":"eng"}],"quality_controlled":"1","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","last_name":"Boker","full_name":"Boker, Udi"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi","first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","last_name":"Sarac","full_name":"Sarac, Naci E"}],"related_material":{"record":[{"id":"13221","relation":"earlier_version","status":"public"},{"id":"20147","status":"public","relation":"dissertation_contains"}]},"title":" Safety and liveness of quantitative properties and automata","type":"journal_article","corr_author":"1","arxiv":1,"publication_identifier":{"eissn":["1860-5974"]},"date_published":"2025-04-08T00:00:00Z","intvolume":"        21","_id":"20342","article_number":"13149","issue":"2","date_created":"2025-09-11T12:17:52Z","OA_place":"publisher","scopus_import":"1","language":[{"iso":"eng"}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 and the Israel Science Foundation grant 2410/22. N. Mazzocchi was affiliated with ISTA when this work was submitted for publication.","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","isi":1,"publisher":"EPI Sciences","article_type":"original"},{"abstract":[{"text":"Information-flow interfaces is a formalism recently proposed for specifying, composing, and refining system-wide security requirements. In this work, we show how the widely used concept of security lattices provides a natural semantic interpretation for information-flow interfaces.","lang":"eng"}],"quality_controlled":"1","department":[{"_id":"ToHe"}],"author":[{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Nickovic, Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan"},{"full_name":"Oliveira da Costa, Ana","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","first_name":"Ana","orcid":"0000-0002-8741-5799","last_name":"Oliveira da Costa"}],"title":"Information-Flow Interfaces and Security Lattices","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2406.14374"}],"arxiv":1,"publication_identifier":{"eisbn":["9783031975370"],"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031975363"]},"corr_author":"1","type":"book_chapter","date_published":"2025-10-02T00:00:00Z","page":"251-263","_id":"20723","intvolume":"     15471","alternative_title":["LNCS"],"scopus_import":"1","date_created":"2025-12-01T15:44:58Z","OA_place":"repository","acknowledgement":"This project was funded in part by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502 and by the ERC-2020-AdG 101020093.","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","place":"Cham","publisher":"Springer Nature","day":"02","article_processing_charge":"No","volume":15471,"project":[{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"oa":1,"oa_version":"Preprint","OA_type":"green","doi":"10.1007/978-3-031-97537-0_15","status":"public","publication_status":"published","date_updated":"2025-12-09T07:57:55Z","ec_funded":1,"month":"10","publication":"Engineering Safe and Trustworthy Cyber Physical Systems","external_id":{"arxiv":["2406.14374"]},"citation":{"mla":"Bartocci, Ezio, et al. “Information-Flow Interfaces and Security Lattices.” <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>, vol. 15471, Springer Nature, 2025, pp. 251–63, doi:<a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">10.1007/978-3-031-97537-0_15</a>.","short":"E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, Engineering Safe and Trustworthy Cyber Physical Systems, Springer Nature, Cham, 2025, pp. 251–263.","ista":"Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.Information-Flow Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber Physical Systems. LNCS, vol. 15471, 251–263.","chicago":"Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Information-Flow Interfaces and Security Lattices.” In <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>, 15471:251–63. Cham: Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">https://doi.org/10.1007/978-3-031-97537-0_15</a>.","ama":"Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-Flow Interfaces and Security Lattices. In: <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>. Vol 15471. Cham: Springer Nature; 2025:251-263. doi:<a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">10.1007/978-3-031-97537-0_15</a>","apa":"Bartocci, E., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2025). Information-Flow Interfaces and Security Lattices. In <i>Engineering Safe and Trustworthy Cyber Physical Systems</i> (Vol. 15471, pp. 251–263). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">https://doi.org/10.1007/978-3-031-97537-0_15</a>","ieee":"E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Information-Flow Interfaces and Security Lattices,” in <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>, vol. 15471, Cham: Springer Nature, 2025, pp. 251–263."},"year":"2025"},{"external_id":{"isi":["001327852600001"]},"citation":{"ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “VAMOS: Middleware for best-effort third-party monitoring,” <i>Science of Computer Programming</i>, vol. 240, no. 2. Elsevier, 2025.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2025). VAMOS: Middleware for best-effort third-party monitoring. <i>Science of Computer Programming</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.scico.2024.103212\">https://doi.org/10.1016/j.scico.2024.103212</a>","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. VAMOS: Middleware for best-effort third-party monitoring. <i>Science of Computer Programming</i>. 2025;240(2). doi:<a href=\"https://doi.org/10.1016/j.scico.2024.103212\">10.1016/j.scico.2024.103212</a>","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2025. VAMOS: Middleware for best-effort third-party monitoring. Science of Computer Programming. 240(2), 103212.","mla":"Chalupa, Marek, et al. “VAMOS: Middleware for Best-Effort Third-Party Monitoring.” <i>Science of Computer Programming</i>, vol. 240, no. 2, 103212, Elsevier, 2025, doi:<a href=\"https://doi.org/10.1016/j.scico.2024.103212\">10.1016/j.scico.2024.103212</a>.","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, Science of Computer Programming 240 (2025).","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “VAMOS: Middleware for Best-Effort Third-Party Monitoring.” <i>Science of Computer Programming</i>. Elsevier, 2025. <a href=\"https://doi.org/10.1016/j.scico.2024.103212\">https://doi.org/10.1016/j.scico.2024.103212</a>."},"year":"2025","has_accepted_license":"1","month":"02","publication":"Science of Computer Programming","ec_funded":1,"date_updated":"2025-09-09T12:25:29Z","ddc":["000"],"doi":"10.1016/j.scico.2024.103212","status":"public","publication_status":"published","oa":1,"oa_version":"Published Version","OA_type":"hybrid","article_processing_charge":"Yes (via OA deal)","day":"01","volume":240,"file_date_updated":"2025-01-13T09:02:47Z","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"file":[{"content_type":"application/pdf","file_size":1173677,"date_updated":"2025-01-13T09:02:47Z","creator":"dernst","relation":"main_file","access_level":"open_access","checksum":"cd93c0c356e479ffccfbe8499b6ba8e2","file_id":"18831","file_name":"2024_ScienceCompProg_Chalupa.pdf","success":1,"date_created":"2025-01-13T09:02:47Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_type":"original","publisher":"Elsevier","isi":1,"scopus_import":"1","issue":"2","date_created":"2024-10-06T22:01:10Z","OA_place":"publisher","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank the STTT reviewers for their valuable feedback and suggestions.","language":[{"iso":"eng"}],"date_published":"2025-02-01T00:00:00Z","article_number":"103212","intvolume":"       240","_id":"18169","publication_identifier":{"issn":["0167-6423"]},"corr_author":"1","type":"journal_article","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"12856"}]},"title":"VAMOS: Middleware for best-effort third-party monitoring","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"ToHe"}],"author":[{"last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","full_name":"Chalupa, Marek"},{"full_name":"Mühlböck, Fabian","first_name":"Fabian","orcid":"0000-0003-1548-0177","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","last_name":"Mühlböck"},{"full_name":"Muroya Lei, Stefanie","last_name":"Muroya Lei","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","first_name":"Stefanie"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"quality_controlled":"1","abstract":[{"lang":"eng","text":"As the complexity and criticality of software increase every year, so does the importance of runtime monitoring. Third-party and best-effort monitoring are especially valuable, yet under-explored areas of runtime monitoring. In this context, third-party monitoring means monitoring with a limited knowledge of the monitored software (as it has been developed by a third party). Best-effort monitoring keeps pace with the monitored software at the cost of possibly imprecise verdicts when keeping up with the monitored software would not be feasible. Most existing monitoring frameworks do not support the combination of third-party and best-effort monitoring because they either require the full access to the monitored code or the ability to process all observable events, or both.\r\nWe present a middleware framework, Vamos, for the runtime monitoring of software. Vamos is explicitly designed to support third-party and best-effort scenarios. The design goals of Vamos are (i) efficiency (tracing events with low overhead), (ii) flexibility (the ability to monitor a variety of different event channels, and to connect to a wide range of monitors), and (iii) ease-of-use. To achieve its goals, Vamos combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\nWe implemented a prototype toolchain for Vamos and conducted a set of experiments demonstrating the usability of the scheme. The results indicate that Vamos enables writing useful yet efficient monitors, and simplifies key aspects of setting up a monitoring system from scratch."}]},{"date_published":"2024-02-01T00:00:00Z","article_number":"101430","_id":"14400","intvolume":"        51","scopus_import":"1","issue":"2","date_created":"2023-10-08T22:01:15Z","acknowledgement":"We thank Daniel Hausmann and Nir Piterman for their valuable comments on an earlier version of the manuscript of our other paper [22] where we present, among other things, the parity fixpoint for 2 1/2-player games (for a slightly more general class of games) with a different and indirect proof of correctness. Based on their comments we observed that, unlike the other fixpoints that we present in [22], the parity fixpoint does not follow the exact same structure as its counterpart for 2-player games, which we also use int his paper.\r\nWe also thank Thejaswini Raghavan for observing that our symbolic parity fixpoint algorithm can be solved in quasi-polynomial time using recent improved algorithms for solving \r\n-calculus expressions. This significantly improved the complexity bounds of our algorithm in this paper.\r\nThe work of R. Majumdar and A.-K. Schmuck are partially supported by DFG, Germany project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded through DFG, Germany project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047.","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Elsevier","article_type":"original","isi":1,"quality_controlled":"1","abstract":[{"lang":"eng","text":"We consider the problem of computing the maximal probability of satisfying an \r\n-regular specification for stochastic, continuous-state, nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic constructions, to finding the maximal probability of satisfying a parity condition on a (possibly hybrid) state space. While characterizing the exact satisfaction probability is open, we show that a lower bound on this probability can be obtained by (I) computing an under-approximation of the qualitative winning region, i.e., states from which the parity condition can be enforced almost surely, and (II) computing the maximal probability of reaching this qualitative winning region.\r\nThe heart of our approach is a technique to symbolically compute the under-approximation of the qualitative winning region in step (I) via a finite-state abstraction of the original system as a \r\n-player parity game. Our abstraction procedure uses only the support of the probabilistic evolution; it does not use precise numerical transition probabilities. We prove that the winning set in the abstract -player game induces an under-approximation of the qualitative winning region in the original synthesis problem, along with a policy to solve it. By combining these contributions with (a) a symbolic fixpoint algorithm to solve \r\n-player games and (b) existing techniques for reachability policy synthesis in stochastic nonlinear systems, we get an abstraction-based algorithm for finding a lower bound on the maximal satisfaction probability.\r\nWe have implemented the abstraction-based algorithm in Mascot-SDS, where we combined the outlined abstraction step with our tool Genie (Majumdar et al., 2023) that solves \r\n-player parity games (through a reduction to Rabin games) more efficiently than existing algorithms. We evaluated our implementation on the nonlinear model of a perturbed bistable switch from the literature. We show empirically that the lower bound on the winning region computed by our approach is precise, by comparing against an over-approximation of the qualitative winning region. Moreover, our implementation outperforms a recently proposed tool for solving this problem by a large margin."}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"ToHe"}],"author":[{"full_name":"Majumdar, Rupak","last_name":"Majumdar","first_name":"Rupak"},{"orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","last_name":"Mallik","full_name":"Mallik, Kaushik"},{"first_name":"Anne Kathrin","last_name":"Schmuck","full_name":"Schmuck, Anne Kathrin"},{"last_name":"Soudjani","first_name":"Sadegh","full_name":"Soudjani, Sadegh"}],"title":"Symbolic control for stochastic systems via finite parity games","arxiv":1,"publication_identifier":{"issn":["1751-570X"]},"corr_author":"1","type":"journal_article","ec_funded":1,"publication":"Nonlinear Analysis: Hybrid Systems","month":"02","has_accepted_license":"1","external_id":{"isi":["001093188100001"],"arxiv":["2101.00834"]},"citation":{"mla":"Majumdar, Rupak, et al. “Symbolic Control for Stochastic Systems via Finite Parity Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 51, no. 2, 101430, Elsevier, 2024, doi:<a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">10.1016/j.nahs.2023.101430</a>.","short":"R. Majumdar, K. Mallik, A.K. Schmuck, S. Soudjani, Nonlinear Analysis: Hybrid Systems 51 (2024).","ista":"Majumdar R, Mallik K, Schmuck AK, Soudjani S. 2024. Symbolic control for stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems. 51(2), 101430.","chicago":"Majumdar, Rupak, Kaushik Mallik, Anne Kathrin Schmuck, and Sadegh Soudjani. “Symbolic Control for Stochastic Systems via Finite Parity Games.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2024. <a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">https://doi.org/10.1016/j.nahs.2023.101430</a>.","apa":"Majumdar, R., Mallik, K., Schmuck, A. K., &#38; Soudjani, S. (2024). Symbolic control for stochastic systems via finite parity games. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">https://doi.org/10.1016/j.nahs.2023.101430</a>","ama":"Majumdar R, Mallik K, Schmuck AK, Soudjani S. Symbolic control for stochastic systems via finite parity games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2024;51(2). doi:<a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">10.1016/j.nahs.2023.101430</a>","ieee":"R. Majumdar, K. Mallik, A. K. Schmuck, and S. Soudjani, “Symbolic control for stochastic systems via finite parity games,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 51, no. 2. Elsevier, 2024."},"year":"2024","day":"01","article_processing_charge":"Yes (in subscription journal)","volume":51,"file_date_updated":"2024-07-16T10:26:41Z","file":[{"file_name":"2024_NonlinearAnalysis_Majumdar.pdf","file_id":"17258","success":1,"date_created":"2024-07-16T10:26:41Z","relation":"main_file","checksum":"4eab70274d1004ea411f7f0e74c033ac","access_level":"open_access","file_size":1787569,"date_updated":"2024-07-16T10:26:41Z","creator":"dernst","content_type":"application/pdf"}],"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"oa":1,"oa_version":"Published Version","ddc":["000"],"doi":"10.1016/j.nahs.2023.101430","status":"public","publication_status":"published","date_updated":"2025-04-14T07:55:55Z"},{"citation":{"short":"G. Trinh, B. Benhamou, S. Pastva, S. Soliman, in:, Proceedings of the 38th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2024, pp. 10714–10722.","mla":"Trinh, Giang, et al. “Scalable Enumeration of Trap Spaces in Boolean Networks via Answer Set Programming.” <i>Proceedings of the 38th AAAI Conference on Artificial Intelligence</i>, vol. 38, no. 9, Association for the Advancement of Artificial Intelligence, 2024, pp. 10714–22, doi:<a href=\"https://doi.org/10.1609/aaai.v38i9.28943\">10.1609/aaai.v38i9.28943</a>.","ista":"Trinh G, Benhamou B, Pastva S, Soliman S. 2024. Scalable enumeration of trap spaces in boolean networks via answer set programming. Proceedings of the 38th AAAI Conference on Artificial Intelligence. vol. 38, 10714–10722.","chicago":"Trinh, Giang, Belaid Benhamou, Samuel Pastva, and Sylvain Soliman. “Scalable Enumeration of Trap Spaces in Boolean Networks via Answer Set Programming.” In <i>Proceedings of the 38th AAAI Conference on Artificial Intelligence</i>, 38:10714–22. Association for the Advancement of Artificial Intelligence, 2024. <a href=\"https://doi.org/10.1609/aaai.v38i9.28943\">https://doi.org/10.1609/aaai.v38i9.28943</a>.","apa":"Trinh, G., Benhamou, B., Pastva, S., &#38; Soliman, S. (2024). Scalable enumeration of trap spaces in boolean networks via answer set programming. In <i>Proceedings of the 38th AAAI Conference on Artificial Intelligence</i> (Vol. 38, pp. 10714–10722). Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v38i9.28943\">https://doi.org/10.1609/aaai.v38i9.28943</a>","ama":"Trinh G, Benhamou B, Pastva S, Soliman S. Scalable enumeration of trap spaces in boolean networks via answer set programming. In: <i>Proceedings of the 38th AAAI Conference on Artificial Intelligence</i>. Vol 38. Association for the Advancement of Artificial Intelligence; 2024:10714-10722. doi:<a href=\"https://doi.org/10.1609/aaai.v38i9.28943\">10.1609/aaai.v38i9.28943</a>","ieee":"G. Trinh, B. Benhamou, S. Pastva, and S. Soliman, “Scalable enumeration of trap spaces in boolean networks via answer set programming,” in <i>Proceedings of the 38th AAAI Conference on Artificial Intelligence</i>, 2024, vol. 38, no. 9, pp. 10714–10722."},"year":"2024","month":"03","publication":"Proceedings of the 38th AAAI Conference on Artificial Intelligence","ec_funded":1,"date_updated":"2026-06-18T17:48:08Z","ddc":["000"],"doi":"10.1609/aaai.v38i9.28943","publication_status":"published","status":"public","oa":1,"oa_version":"Published Version","day":"25","article_processing_charge":"No","volume":38,"project":[{"name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Association for the Advancement of Artificial Intelligence","scopus_import":"1","issue":"9","date_created":"2024-04-14T22:01:02Z","acknowledgement":"This work was supported by Institut Carnot STAR, Marseille, France and by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413.","language":[{"iso":"eng"}],"date_published":"2024-03-25T00:00:00Z","page":"10714-10722","_id":"15321","intvolume":"        38","main_file_link":[{"url":"https://amu.hal.science/hal-04523118/","open_access":"1"}],"publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"],"isbn":["1577358872"]},"type":"conference","title":"Scalable enumeration of trap spaces in boolean networks via answer set programming","department":[{"_id":"ToHe"}],"author":[{"first_name":"Giang","last_name":"Trinh","full_name":"Trinh, Giang"},{"full_name":"Benhamou, Belaid","first_name":"Belaid","last_name":"Benhamou"},{"full_name":"Pastva, Samuel","orcid":"0000-0003-1993-0331","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","first_name":"Samuel","last_name":"Pastva"},{"first_name":"Sylvain","last_name":"Soliman","full_name":"Soliman, Sylvain"}],"quality_controlled":"1","abstract":[{"lang":"eng","text":"Boolean Networks (BNs) are widely used as a modeling formalism in several domains, notably systems biology and computer science. A fundamental problem in BN analysis is the enumeration of trap spaces, which are hypercubes in the state space that cannot be escaped once entered. Several methods have been proposed for enumerating trap spaces, however they often suffer from scalability and efficiency issues, particularly for large and complex models. To our knowledge, the most efficient and recent methods for the trap space enumeration all rely on Answer Set Programming (ASP), which has been widely applied to the analysis of BNs. Motivated by these considerations, our work proposes a new method for enumerating trap spaces in BNs using ASP. We evaluate the method on a mix of 250+ real-world and 400+ randomly generated BNs, showing that it enables analysis of models beyond the capabilities of existing tools (namely pyboolnet, mpbn, trappist, and trapmvn)."}]},{"external_id":{"isi":["001284187100020"]},"year":"2024","citation":{"short":"M. Chalupa, C. Richter, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 353–358.","mla":"Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution).” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 353–358, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">10.1007/978-3-031-57256-2_20</a>.","ista":"Chalupa M, Richter C. 2024. Bubaak-SpLit: Split what you cannot verify (Competition contribution). 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 14572, 353–358.","chicago":"Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution).” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:353–358. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">https://doi.org/10.1007/978-3-031-57256-2_20</a>.","apa":"Chalupa, M., &#38; Richter, C. (2024). Bubaak-SpLit: Split what you cannot verify (Competition contribution). In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 353–358). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">https://doi.org/10.1007/978-3-031-57256-2_20</a>","ama":"Chalupa M, Richter C. Bubaak-SpLit: Split what you cannot verify (Competition contribution). In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:353–358. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">10.1007/978-3-031-57256-2_20</a>","ieee":"M. Chalupa and C. Richter, “Bubaak-SpLit: Split what you cannot verify (Competition contribution),” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 353–358."},"has_accepted_license":"1","month":"04","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","ec_funded":1,"date_updated":"2025-09-04T13:48:25Z","ddc":["000"],"doi":"10.1007/978-3-031-57256-2_20","status":"public","publication_status":"published","oa":1,"oa_version":"Published Version","day":"05","article_processing_charge":"Yes (in subscription journal)","volume":14572,"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"file_date_updated":"2024-04-26T11:27:26Z","file":[{"content_type":"application/pdf","date_updated":"2024-04-26T11:27:26Z","file_size":577128,"creator":"cchlebak","relation":"main_file","checksum":"208c855c60824bec936b8d01d0396474","access_level":"open_access","success":1,"file_name":"2024_LNCS_Chalupa.pdf","file_id":"15347","date_created":"2024-04-26T11:27:26Z"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publisher":"Springer Nature","isi":1,"conference":{"end_date":"2024-04-11","start_date":"2024-04-06","location":"Luxembourg City, Luxembourg","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"scopus_import":"1","date_created":"2024-04-20T18:14:06Z","acknowledgement":"This work was partially supported by the ERC-2020-AdG 10102009 grant.","language":[{"iso":"eng"}],"date_published":"2024-04-05T00:00:00Z","page":"353–358","_id":"15333","intvolume":"     14572","alternative_title":["LNCS"],"publication_identifier":{"eisbn":["9783031572562"],"isbn":["9783031572555"],"eissn":["1611-3349"],"issn":["0302-9743"]},"type":"conference","corr_author":"1","title":"Bubaak-SpLit: Split what you cannot verify (Competition contribution)","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"ToHe"}],"author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"full_name":"Richter, Cedric","first_name":"Cedric","last_name":"Richter"}],"quality_controlled":"1","abstract":[{"lang":"eng","text":"BUBAAK-SpLit is a tool for dynamically splitting verification tasks into parts that can then be analyzed in parallel. It is built on top of BUBAAK, a tool designed for running combinations of verifiers in parallel. In contrast to BUBAAK, that directly invokes verifiers on the inputs, BUBAAK-SpLit first starts by splitting the input program into multiple modified versions called program splits. During the splitting process, BUBAAK-SpLit utilizes a weak verifier (in our case symbolic execution with a short timelimit) to analyze each generated program split. If the weak verifier fails on a program split, we split this program split again and start the verification process again on the generated program splits. We run the splitting process until a predefined number of hard-to-verify program splits is generated or a splitting limit is reached. During the main verification phase, we run a combination of BUBAAK-LEE and SLOWBEAST in parallel on the remaining unsolved parts of the verification task."}]},{"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"file":[{"creator":"dernst","file_size":508191,"date_updated":"2024-05-22T07:09:24Z","content_type":"application/pdf","date_created":"2024-05-22T07:09:24Z","file_id":"15414","file_name":"2024_LNCS_Avni.pdf","success":1,"checksum":"dbeb123510997886d11925aedbf9c400","access_level":"open_access","relation":"main_file"}],"file_date_updated":"2024-05-22T07:09:24Z","volume":14572,"article_processing_charge":"Yes (in subscription journal)","day":"05","oa_version":"Published Version","oa":1,"publication_status":"published","status":"public","doi":"10.1007/978-3-031-57256-2_8","ddc":["000"],"date_updated":"2025-09-08T07:33:43Z","ec_funded":1,"month":"04","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","has_accepted_license":"1","year":"2024","citation":{"ama":"Avni G, Mallik K, Sadhukhan S. Auction-based scheduling. In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:153-172. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">10.1007/978-3-031-57256-2_8</a>","apa":"Avni, G., Mallik, K., &#38; Sadhukhan, S. (2024). Auction-based scheduling. In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 153–172). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">https://doi.org/10.1007/978-3-031-57256-2_8</a>","chicago":"Avni, Guy, Kaushik Mallik, and Suman Sadhukhan. “Auction-Based Scheduling.” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:153–72. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">https://doi.org/10.1007/978-3-031-57256-2_8</a>.","short":"G. Avni, K. Mallik, S. Sadhukhan, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 153–172.","ista":"Avni G, Mallik K, Sadhukhan S. 2024. Auction-based scheduling. 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 14572, 153–172.","mla":"Avni, Guy, et al. “Auction-Based Scheduling.” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 153–72, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">10.1007/978-3-031-57256-2_8</a>.","ieee":"G. Avni, K. Mallik, and S. Sadhukhan, “Auction-based scheduling,” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 153–172."},"external_id":{"arxiv":["2310.11798"],"isi":["001284187100008"]},"quality_controlled":"1","abstract":[{"lang":"eng","text":"Sequential decision-making tasks often require satisfaction of multiple, partially-contradictory objectives. Existing approaches are monolithic, where a single policy fulfills all objectives. We present auction-based scheduling, a decentralized framework for multi-objective sequential decision making. Each objective is fulfilled using a separate and independent policy. Composition of policies is performed at runtime, where at each step, the policies simultaneously bid from pre-allocated budgets for the privilege of choosing the next action. The framework allows policies to be independently created, modified, and replaced. We study path planning problems on finite graphs with two temporal objectives and present algorithms to synthesize policies together with bidding policies in a decentralized manner. We consider three categories of decentralized synthesis problems, parameterized by the assumptions that the policies make on each other. We identify a class of assumptions called assume-admissible for which synthesis is always possible for graphs whose every vertex has at most two outgoing edges."}],"author":[{"first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","full_name":"Avni, Guy"},{"last_name":"Mallik","orcid":"0000-0001-9864-7475","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik"},{"full_name":"Sadhukhan, Suman","last_name":"Sadhukhan","first_name":"Suman"}],"department":[{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"title":"Auction-based scheduling","type":"conference","corr_author":"1","arxiv":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031572555"]},"_id":"15376","alternative_title":["LNCS"],"intvolume":"     14572","page":"153-172","date_published":"2024-04-05T00:00:00Z","language":[{"iso":"eng"}],"acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093 and by ISF grant no. 1679/21.","date_created":"2024-05-12T22:01:02Z","scopus_import":"1","conference":{"start_date":"2024-04-06","location":"Luxembourg City, Luxembourg","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2024-04-11"},"isi":1,"publisher":"Springer Nature","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"scopus_import":"1","date_created":"2024-05-12T22:01:02Z","acknowledgement":"This work is a part of the project VAMOS that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme, grant agreements No 101020093. Rupak Majumdar was partially supported by the DFG project 389792660 TRR 248-CPEC.","language":[{"iso":"eng"}],"date_published":"2024-04-06T00:00:00Z","page":"213-231","intvolume":"     14572","_id":"15377","alternative_title":["LNCS"],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publisher":"Springer Nature","isi":1,"department":[{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"author":[{"full_name":"Majumdar, Rupak","last_name":"Majumdar","first_name":"Rupak"},{"full_name":"Sağlam, Irmak","last_name":"Sağlam","first_name":"Irmak"},{"last_name":"Thejaswini","first_name":"K. S.","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","full_name":"Thejaswini, K. S."}],"abstract":[{"lang":"eng","text":"We provide an algorithmto solve Rabin and Streett games over graphs\r\nwith n vertices,m edges, and k colours that runs in ˜O³mn(k!)1+o(1)´time and\r\nO(nk logk logn) space, where ˜O hides poly-logarithmic factors. Our algorithm\r\nis an improvement by a super quadratic dependence on k! from the currently\r\nbest known run time of O³mn2(k!)2+o(1)´, obtained by converting a Rabin\r\ngameinto a parity game,while simultaneously improving its exponential space\r\nrequirement.\r\nOur main technical ingredient is a characterisation of progress measures for\r\nRabin games using colourful trees and a combinatorial construction of succinctlyrepresented,\r\nuniversal colourful trees. Colourful universal trees are generalisations\r\nof universal trees used by Jurdzi´nski and Lazi´c (2017) to solve parity\r\ngames, as well as of Rabin progress measures of Klarlund and Kozen (1991).\r\nOur algorithm for Rabin games is a progress measure lifting algorithm where\r\nthe lifting is performed on succinct, colourful, universal trees."}],"quality_controlled":"1","arxiv":1,"publication_identifier":{"isbn":["9783031572555"],"issn":["0302-9743"],"eissn":["1611-3349"]},"type":"conference","corr_author":"1","title":"Rabin games and colourful universal trees","month":"04","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","ec_funded":1,"external_id":{"isi":["001284187100011"],"arxiv":["2401.07548"]},"year":"2024","citation":{"apa":"Majumdar, R., Sağlam, I., &#38; Thejaswini, K. S. (2024). Rabin games and colourful universal trees. In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 213–231). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">https://doi.org/10.1007/978-3-031-57256-2_11</a>","ama":"Majumdar R, Sağlam I, Thejaswini KS. Rabin games and colourful universal trees. In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:213-231. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">10.1007/978-3-031-57256-2_11</a>","chicago":"Majumdar, Rupak, Irmak Sağlam, and K. S. Thejaswini. “Rabin Games and Colourful Universal Trees.” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:213–31. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">https://doi.org/10.1007/978-3-031-57256-2_11</a>.","short":"R. Majumdar, I. Sağlam, K.S. Thejaswini, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 213–231.","ista":"Majumdar R, Sağlam I, Thejaswini KS. 2024. Rabin games and colourful universal trees. 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. , LNCS, vol. 14572, 213–231.","mla":"Majumdar, Rupak, et al. “Rabin Games and Colourful Universal Trees.” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 213–31, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">10.1007/978-3-031-57256-2_11</a>.","ieee":"R. Majumdar, I. Sağlam, and K. S. Thejaswini, “Rabin games and colourful universal trees,” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 2024, vol. 14572, pp. 213–231."},"has_accepted_license":"1","oa":1,"oa_version":"Published Version","article_processing_charge":"Yes (in subscription journal)","day":"06","volume":14572,"file":[{"relation":"main_file","checksum":"492be74f69cd6ea42d38681082d0b521","access_level":"open_access","success":1,"file_id":"15415","file_name":"2024_LNCS_Majumdar.pdf","date_created":"2024-05-22T07:24:45Z","content_type":"application/pdf","date_updated":"2024-05-22T07:24:45Z","file_size":462173,"creator":"dernst"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"}],"file_date_updated":"2024-05-22T07:24:45Z","date_updated":"2025-09-08T07:34:49Z","ddc":["000"],"doi":"10.1007/978-3-031-57256-2_11","status":"public","publication_status":"published"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems","location":"Kaiserslautern, Germany","start_date":"2024-02-14","end_date":"2024-02-15"},"scopus_import":"1","date_created":"2024-05-26T22:00:58Z","OA_place":"repository","acknowledgement":"This work is supported by the Austrian Science Fund (FWF) under the project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG 101020093 and by a gift from Intel Corporation.","language":[{"iso":"eng"}],"date_published":"2024-02-01T00:00:00Z","page":"148-151","_id":"17053","main_file_link":[{"url":"https://cca.informatik.uni-freiburg.de/papers/FroleyksYuBiere-MBMV24.pdf","open_access":"1"}],"publication_identifier":{"isbn":["9783800762682"]},"type":"conference","title":"Ternary simulation as abstract interpretation (Work in Progress)","department":[{"_id":"ToHe"}],"author":[{"last_name":"Froleyks","first_name":"Nils","full_name":"Froleyks, Nils"},{"full_name":"Yu, Zhengqi","last_name":"Yu","orcid":"0000-0002-4993-773X","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","first_name":"Zhengqi"},{"full_name":"Biere, Armin","last_name":"Biere","first_name":"Armin"}],"abstract":[{"lang":"eng","text":"We introduce a formalization of ternary simulation as abstract interpretation along with a widening operator to speed up convergence. With the same goal, we present a subsumption algorithm that can determine termination earlier than the usual approach using hash sets. Additionally, we introduce a narrowing operator that utilizes recent advances in backbone extraction, allowing to increase the overapproximation precision in simulation at any time. The experiments evaluate the presented techniques in the context of hardware model checking."}],"quality_controlled":"1","year":"2024","citation":{"ieee":"N. Froleyks, E. Yu, and A. Biere, “Ternary simulation as abstract interpretation (Work in Progress),” in <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, Kaiserslautern, Germany, 2024, pp. 148–151.","apa":"Froleyks, N., Yu, E., &#38; Biere, A. (2024). Ternary simulation as abstract interpretation (Work in Progress). In <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i> (pp. 148–151). Kaiserslautern, Germany.","ama":"Froleyks N, Yu E, Biere A. Ternary simulation as abstract interpretation (Work in Progress). In: <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>. ; 2024:148-151.","ista":"Froleyks N, Yu E, Biere A. 2024. Ternary simulation as abstract interpretation (Work in Progress). 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems. MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems, 148–151.","mla":"Froleyks, Nils, et al. “Ternary Simulation as Abstract Interpretation (Work in Progress).” <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, 2024, pp. 148–51.","short":"N. Froleyks, E. Yu, A. Biere, in:, 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems, 2024, pp. 148–151.","chicago":"Froleyks, Nils, Emily Yu, and Armin Biere. “Ternary Simulation as Abstract Interpretation (Work in Progress).” In <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, 148–51, 2024."},"publication":"27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems","month":"02","ec_funded":1,"date_updated":"2026-01-05T14:05:35Z","status":"public","publication_status":"published","oa":1,"oa_version":"Submitted Version","OA_type":"green","day":"01","article_processing_charge":"No","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}]}]