[{"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"article_type":"original","publication_status":"published","quality_controlled":"1","corr_author":"1","citation":{"mla":"Barrett, Clark, et al. “Certificates in AI: Learn but Verify.” <i>Communications of the ACM</i>, vol. 69, no. 1, Association for Computing Machinery, 2026, pp. 66–75, doi:<a href=\"https://doi.org/10.1145/3737447\">10.1145/3737447</a>.","ama":"Barrett C, Henzinger TA, Seshia SA. Certificates in AI: Learn but verify. <i>Communications of the ACM</i>. 2026;69(1):66-75. doi:<a href=\"https://doi.org/10.1145/3737447\">10.1145/3737447</a>","apa":"Barrett, C., Henzinger, T. A., &#38; Seshia, S. A. (2026). Certificates in AI: Learn but verify. <i>Communications of the ACM</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3737447\">https://doi.org/10.1145/3737447</a>","short":"C. Barrett, T.A. Henzinger, S.A. Seshia, Communications of the ACM 69 (2026) 66–75.","ista":"Barrett C, Henzinger TA, Seshia SA. 2026. Certificates in AI: Learn but verify. Communications of the ACM. 69(1), 66–75.","ieee":"C. Barrett, T. A. Henzinger, and S. A. Seshia, “Certificates in AI: Learn but verify,” <i>Communications of the ACM</i>, vol. 69, no. 1. Association for Computing Machinery, pp. 66–75, 2026.","chicago":"Barrett, Clark, Thomas A Henzinger, and Sanjit A. Seshia. “Certificates in AI: Learn but Verify.” <i>Communications of the ACM</i>. Association for Computing Machinery, 2026. <a href=\"https://doi.org/10.1145/3737447\">https://doi.org/10.1145/3737447</a>."},"publication":"Communications of the ACM","issue":"1","date_created":"2026-01-20T10:08:21Z","scopus_import":"1","ddc":["000"],"file":[{"content_type":"application/pdf","file_size":2623108,"file_id":"21028","success":1,"creator":"dernst","checksum":"d909a9091c254b2d18ba014124663f69","access_level":"open_access","date_created":"2026-01-21T08:52:07Z","file_name":"2026_CommACM_Barrett.pdf","relation":"main_file","date_updated":"2026-01-21T08:52:07Z"}],"ec_funded":1,"publication_identifier":{"eissn":["1557-7317"],"issn":["0001-0782"]},"OA_place":"publisher","oa_version":"Published Version","department":[{"_id":"ToHe"}],"oa":1,"article_processing_charge":"Yes (via OA deal)","year":"2026","page":"66-75","doi":"10.1145/3737447","month":"01","PlanS_conform":"1","publisher":"Association for Computing Machinery","_id":"21012","title":"Certificates in AI: Learn but verify","date_published":"2026-01-01T00:00:00Z","volume":69,"intvolume":"        69","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"acknowledgement":"T.A.H. thanks Đorde Žikelic for many stimulating discussions about CML. This work was supported in part by NSFCPS Frontier Grant 1545126, by a BAIR Commons project, by the Berkeley iCy-Phy Center, by the Stanford Center for Automated Reasoning, and by the ERC Advanced Grant 101020093.","abstract":[{"lang":"eng","text":"In certifiable machine learning, AI systems produce not only results but also verifiable certificates that the results can be trusted."}],"file_date_updated":"2026-01-21T08:52:07Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","date_updated":"2026-01-21T08:55:24Z","status":"public","license":"https://creativecommons.org/licenses/by/4.0/","type":"journal_article","author":[{"first_name":"Clark","full_name":"Barrett, Clark","last_name":"Barrett"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger"},{"full_name":"Seshia, Sanjit A.","first_name":"Sanjit A.","last_name":"Seshia"}],"language":[{"iso":"eng"}],"OA_type":"hybrid","has_accepted_license":"1"},{"degree_awarded":"MS","page":"60","year":"2026","article_processing_charge":"No","doi":"10.15479/AT-ISTA-21401","ec_funded":1,"file":[{"creator":"mkarimi","file_id":"21404","file_size":766048,"content_type":"application/pdf","checksum":"3f49f05c9d123e14d7adb73d3bc50fe2","file_name":"2026_Karimi_Mahyar_Thesis.pdf","date_created":"2026-03-06T14:06:25Z","access_level":"open_access","date_updated":"2026-03-10T15:20:09Z","relation":"main_file"},{"content_type":"application/zip","file_size":1243394,"file_id":"21405","creator":"mkarimi","checksum":"8fb9db4b4187e26443369a993427a5ff","access_level":"closed","date_created":"2026-03-06T14:06:25Z","file_name":"2026_Karimi_Mahyar_Thesis_src.zip","relation":"source_file","date_updated":"2026-03-06T14:06:25Z"}],"ddc":["000"],"oa_version":"Published Version","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"oa":1,"publication_identifier":{"issn":["2791-4585"]},"OA_place":"repository","related_material":{"record":[{"id":"21020","status":"public","relation":"part_of_dissertation"}]},"date_created":"2026-03-05T15:20:47Z","supervisor":[{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"publication_status":"published","citation":{"ista":"Karimi M. 2026. Privacy-preserving runtime verification. Institute of Science and Technology Austria.","ieee":"M. Karimi, “Privacy-preserving runtime verification,” Institute of Science and Technology Austria, 2026.","chicago":"Karimi, Mahyar. “Privacy-Preserving Runtime Verification.” Institute of Science and Technology Austria, 2026. <a href=\"https://doi.org/10.15479/AT-ISTA-21401\">https://doi.org/10.15479/AT-ISTA-21401</a>.","ama":"Karimi M. Privacy-preserving runtime verification. 2026. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-21401\">10.15479/AT-ISTA-21401</a>","short":"M. Karimi, Privacy-Preserving Runtime Verification, Institute of Science and Technology Austria, 2026.","apa":"Karimi, M. (2026). <i>Privacy-preserving runtime verification</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-21401\">https://doi.org/10.15479/AT-ISTA-21401</a>","mla":"Karimi, Mahyar. <i>Privacy-Preserving Runtime Verification</i>. Institute of Science and Technology Austria, 2026, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-21401\">10.15479/AT-ISTA-21401</a>."},"corr_author":"1","date_updated":"2026-03-13T13:37:20Z","language":[{"iso":"eng"}],"has_accepted_license":"1","type":"dissertation","status":"public","author":[{"id":"6e5417ba-5355-11ee-ae5a-94c2e510b26b","full_name":"Karimi, Mahyar","first_name":"Mahyar","last_name":"Karimi","orcid":"0009-0005-0820-1696"}],"abstract":[{"lang":"eng","text":"Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification.\r\n\r\nIn this thesis, we propose a protocol for privacy-preserving runtime verification of systems against formal sequential specifications. We develop the protocol in two steps. In the first step, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. In the second step, we extend the protocol to ensure that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocol adapts and improves existing techniques used in cryptography, and more specifically, multi-party computation.\r\n\r\nThe sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocol exchanges a single message per observation step, after an initialization phase. This design minimizes communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.\r\n"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"},{"name":"Security and Privacy by Design for Complex Systems","grant_number":"F8512","_id":"34a4ce89-11ca-11ed-8bc3-8cc37fb6e11f"}],"acknowledgement":"This work is part of the project VAMOS, which has received funding from the European\r\nResearch Council (ERC) under grant agreement No. 101020093, and the Austrian Science\r\nFund (FWF) SFB project SpyCoDe F8502.\r\n","day":"05","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","file_date_updated":"2026-03-10T15:20:09Z","_id":"21401","alternative_title":["ISTA Master’s Thesis"],"keyword":["Privacy-preserving verification","Runtime verification","Monitoring","Reactive functionalities","Cryptographic protocols"],"title":"Privacy-preserving runtime verification","date_published":"2026-03-05T00:00:00Z","publisher":"Institute of Science and Technology Austria","month":"03"},{"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.","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"intvolume":"       240","abstract":[{"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.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2025-01-13T09:02:47Z","day":"01","date_updated":"2025-09-09T12:25:29Z","author":[{"last_name":"Chalupa","first_name":"Marek","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"orcid":"0000-0003-1548-0177","last_name":"Mühlböck","first_name":"Fabian","full_name":"Mühlböck, Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425"},{"last_name":"Muroya Lei","full_name":"Muroya Lei, Stefanie","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","first_name":"Stefanie"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger"}],"external_id":{"isi":["001327852600001"]},"status":"public","type":"journal_article","OA_type":"hybrid","has_accepted_license":"1","language":[{"iso":"eng"}],"month":"02","publisher":"Elsevier","title":"VAMOS: Middleware for best-effort third-party monitoring","_id":"18169","volume":240,"date_published":"2025-02-01T00:00:00Z","scopus_import":"1","ddc":["000"],"file":[{"creator":"dernst","success":1,"file_id":"18831","file_size":1173677,"content_type":"application/pdf","checksum":"cd93c0c356e479ffccfbe8499b6ba8e2","file_name":"2024_ScienceCompProg_Chalupa.pdf","date_created":"2025-01-13T09:02:47Z","access_level":"open_access","date_updated":"2025-01-13T09:02:47Z","relation":"main_file"}],"ec_funded":1,"publication_identifier":{"issn":["0167-6423"]},"OA_place":"publisher","oa":1,"department":[{"_id":"ToHe"}],"oa_version":"Published Version","article_processing_charge":"Yes (via OA deal)","year":"2025","doi":"10.1016/j.scico.2024.103212","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"article_number":"103212","publication_status":"published","article_type":"original","isi":1,"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.","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.","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>.","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>","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, Science of Computer Programming 240 (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>","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>."},"corr_author":"1","quality_controlled":"1","publication":"Science of Computer Programming","issue":"2","related_material":{"record":[{"status":"public","id":"12856","relation":"earlier_version"}]},"date_created":"2024-10-06T22:01:10Z"},{"date_created":"2025-06-08T22:01:22Z","issue":"5","related_material":{"record":[{"status":"public","id":"19800","relation":"research_data"}],"link":[{"relation":"software","url":"https://github.com/jcrozum/biobalm"}]},"quality_controlled":"1","corr_author":"1","citation":{"mla":"Trinh, Van Giang, et al. “Mapping the Attractor Landscape of Boolean Networks with Biobalm.” <i>Bioinformatics</i>, vol. 41, no. 5, btaf280, Oxford University Press, 2025, doi:<a href=\"https://doi.org/10.1093/bioinformatics/btaf280\">10.1093/bioinformatics/btaf280</a>.","apa":"Trinh, V. G., Park, K. H., Pastva, S., &#38; Rozum, J. C. (2025). Mapping the attractor landscape of Boolean networks with biobalm. <i>Bioinformatics</i>. Oxford University Press. <a href=\"https://doi.org/10.1093/bioinformatics/btaf280\">https://doi.org/10.1093/bioinformatics/btaf280</a>","short":"V.G. Trinh, K.H. Park, S. Pastva, J.C. Rozum, Bioinformatics 41 (2025).","ama":"Trinh VG, Park KH, Pastva S, Rozum JC. Mapping the attractor landscape of Boolean networks with biobalm. <i>Bioinformatics</i>. 2025;41(5). doi:<a href=\"https://doi.org/10.1093/bioinformatics/btaf280\">10.1093/bioinformatics/btaf280</a>","chicago":"Trinh, Van Giang, Kyu Hyong Park, Samuel Pastva, and Jordan C. Rozum. “Mapping the Attractor Landscape of Boolean Networks with Biobalm.” <i>Bioinformatics</i>. Oxford University Press, 2025. <a href=\"https://doi.org/10.1093/bioinformatics/btaf280\">https://doi.org/10.1093/bioinformatics/btaf280</a>.","ieee":"V. G. Trinh, K. H. Park, S. Pastva, and J. C. Rozum, “Mapping the attractor landscape of Boolean networks with biobalm,” <i>Bioinformatics</i>, vol. 41, no. 5. Oxford University Press, 2025.","ista":"Trinh VG, Park KH, Pastva S, Rozum JC. 2025. Mapping the attractor landscape of Boolean networks with biobalm. Bioinformatics. 41(5), btaf280."},"publication":"Bioinformatics","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"article_number":"btaf280","article_type":"original","publication_status":"published","isi":1,"doi":"10.1093/bioinformatics/btaf280","article_processing_charge":"Yes","year":"2025","publication_identifier":{"eissn":["1367-4811"]},"OA_place":"publisher","oa_version":"Published Version","department":[{"_id":"ToHe"}],"oa":1,"scopus_import":"1","ec_funded":1,"ddc":["000"],"file":[{"success":1,"creator":"dernst","content_type":"application/pdf","file_size":2695801,"file_id":"19801","checksum":"fa9d68aa0f5ce37598a623c9be936f09","date_created":"2025-06-10T07:07:45Z","file_name":"2025_Bioinformatics_Trinh.pdf","access_level":"open_access","relation":"main_file","date_updated":"2025-06-10T07:07:45Z"}],"date_published":"2025-05-01T00:00:00Z","volume":41,"title":"Mapping the attractor landscape of Boolean networks with biobalm","_id":"19796","month":"05","DOAJ_listed":"1","publisher":"Oxford University Press","type":"journal_article","status":"public","external_id":{"isi":["001493400600001"],"pmid":["40327535"]},"author":[{"last_name":"Trinh","first_name":"Van Giang","full_name":"Trinh, Van Giang"},{"first_name":"Kyu Hyong","full_name":"Park, Kyu Hyong","last_name":"Park"},{"full_name":"Pastva, Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","first_name":"Samuel","orcid":"0000-0003-1993-0331","last_name":"Pastva"},{"full_name":"Rozum, Jordan C.","first_name":"Jordan C.","last_name":"Rozum"}],"language":[{"iso":"eng"}],"has_accepted_license":"1","OA_type":"gold","date_updated":"2025-09-30T12:46:33Z","pmid":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file_date_updated":"2025-06-10T07:07:45Z","day":"01","project":[{"grant_number":"101034413","call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"intvolume":"        41","acknowledgement":"V.-G.T. was supported by Institut Carnot STAR, Marseille, France. K.H.P. was supported by NSF grant MCB1715826 to Réka Albert. S.P. has received funding from the European Union’s Horizon 2020 Research and Innovation Programme under the Marie Sklodowska-Curie Grant Agreement No. 101034413. J.C.R. was supported by internal departmental funds provided by Luis M. Rocha. No funding bodies had any role in study design, analysis, decision to publish, or preparation of the article.","abstract":[{"lang":"eng","text":"Motivation: Boolean networks are popular dynamical models of cellular processes in systems biology. Their attractors model phenotypes that arise from the interplay of key regulatory subcircuits. A succession diagram (SD) describes this interplay in a discrete analog of Waddington’s epigenetic attractor landscape that allows for fast identification of attractors and attractor control strategies. Efficient computational tools for studying SDs are essential for the understanding of Boolean attractor landscapes and connecting them to their biological functions.\r\nResults: We present a new approach to SD construction for asynchronously updated Boolean networks, implemented in the biologist’s Boolean attractor landscape mapper, biobalm. We compare biobalm to similar tools and find a substantial performance increase in SD construction, attractor identification, and attractor control. We perform the most comprehensive comparative analysis to date of the SD structure in experimentally-validated Boolean models of cell processes and random ensembles. We find that random models (including critical Kauffman networks) have relatively small SDs, indicating simple decision structures. In contrast, nonrandom models from the literature are enriched in extremely large SDs, indicating an abundance of decision points and suggesting the presence of complex Waddington landscapes in nature.\r\nAvailability and implementation: The tool biobalm is available online at https://github.com/jcrozum/biobalm. Further data, scripts for testing, analysis, and figure generation are available online at https://github.com/jcrozum/biobalm-analysis and in the reproducibility artefact at https://doi.org/10.5281/zenodo.13854760."}]},{"file_date_updated":"2025-06-23T11:10:01Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","day":"12","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020"}],"intvolume":"        91","acknowledgement":"Ondřej Huvar has been supported by the Czech Science Foundation grant No. GA22-10845S. Samuel Pastva received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie Grant Agreement No. 101034413. Kyu Hyong Park and Réka Albert have been supported by NSF grant MCB 1715826 and ARO grant 79961-SM-MUR. No funding bodies had any role in study design, analysis, decision to publish, or preparation of the manuscript.","abstract":[{"lang":"eng","text":"Asynchronous Boolean networks are a type of discrete dynamical system in which each variable can take one of two states, and a single variable state is updated in each time step according to pre-selected rules. Boolean networks are popular in systems biology due to their ability to model long-term biological phenotypes within a qualitative, predictive framework. Boolean networks model phenotypes as attractors, which are closely linked to minimal trap spaces (inescapable hypercubes in the system’s state space). In biological applications, attractors and minimal trap spaces are typically in one-to-one correspondence. However, this correspondence is not guaranteed: motif-avoidant attractors (MAAs) that lie outside minimal trap spaces are possible. MAAs are rare and poorly understood, despite recent efforts. In this contribution to the BMB & JMB Special Collection “Problems, Progress and Perspectives in Mathematical and Computational Biology”, we summarize the current state of knowledge regarding MAAs and present several novel observations regarding their response to node deletion reductions and linear extensions of edges. We conduct large-scale computational studies on an ensemble of 14 000 models derived from published Boolean models of biological systems, and more than 100 million Random Boolean Networks. Our findings quantify the rarity of MAAs; in particular, we only observed MAAs in biological models after applying standard simplification methods, highlighting the role of network reduction in introducing MAAs into the dynamics. We also show that MAAs are fragile to linear extensions: in sparse networks, even a single linear node can disrupt virtually all MAAs. Motivated by this observation, we improve the upper bound on the number of delays needed to disrupt a motif-avoidant attractor."}],"status":"public","type":"journal_article","external_id":{"arxiv":["2410.03976"],"isi":["001507009300001"]},"author":[{"first_name":"Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","full_name":"Pastva, Samuel","last_name":"Pastva","orcid":"0000-0003-1993-0331"},{"last_name":"Park","first_name":"Kyu Hyong","full_name":"Park, Kyu Hyong"},{"first_name":"Ondřej","full_name":"Huvar, Ondřej","last_name":"Huvar"},{"first_name":"Jordan C.","full_name":"Rozum, Jordan C.","last_name":"Rozum"},{"last_name":"Albert","first_name":"Réka","full_name":"Albert, Réka"}],"language":[{"iso":"eng"}],"has_accepted_license":"1","OA_type":"hybrid","date_updated":"2025-09-30T13:36:46Z","month":"06","publisher":"Springer Nature","volume":91,"date_published":"2025-06-12T00:00:00Z","title":"An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks?","_id":"19854","publication_identifier":{"eissn":["1432-1416"],"issn":["0303-6812"]},"OA_place":"publisher","oa_version":"Published Version","oa":1,"department":[{"_id":"ToHe"}],"scopus_import":"1","file":[{"relation":"main_file","date_updated":"2025-06-23T11:10:01Z","date_created":"2025-06-23T11:10:01Z","file_name":"2025_JourMathBiology_Pastva.pdf","access_level":"open_access","checksum":"a385ef2662f1d0c3497ed3f2721fe594","success":1,"creator":"dernst","content_type":"application/pdf","file_size":1243163,"file_id":"19871"}],"ddc":["000"],"ec_funded":1,"doi":"10.1007/s00285-025-02235-8","article_processing_charge":"Yes (in subscription journal)","year":"2025","quality_controlled":"1","citation":{"chicago":"Pastva, Samuel, Kyu Hyong Park, Ondřej Huvar, Jordan C. Rozum, and Réka Albert. “An Open Problem: Why Are Motif-Avoidant Attractors so Rare in Asynchronous Boolean Networks?” <i>Journal of Mathematical Biology</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00285-025-02235-8\">https://doi.org/10.1007/s00285-025-02235-8</a>.","ista":"Pastva S, Park KH, Huvar O, Rozum JC, Albert R. 2025. An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks? Journal of Mathematical Biology. 91, 11.","ieee":"S. Pastva, K. H. Park, O. Huvar, J. C. Rozum, and R. Albert, “An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks?,” <i>Journal of Mathematical Biology</i>, vol. 91. Springer Nature, 2025.","mla":"Pastva, Samuel, et al. “An Open Problem: Why Are Motif-Avoidant Attractors so Rare in Asynchronous Boolean Networks?” <i>Journal of Mathematical Biology</i>, vol. 91, 11, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00285-025-02235-8\">10.1007/s00285-025-02235-8</a>.","apa":"Pastva, S., Park, K. H., Huvar, O., Rozum, J. C., &#38; Albert, R. (2025). An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks? <i>Journal of Mathematical Biology</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00285-025-02235-8\">https://doi.org/10.1007/s00285-025-02235-8</a>","short":"S. Pastva, K.H. Park, O. Huvar, J.C. Rozum, R. Albert, Journal of Mathematical Biology 91 (2025).","ama":"Pastva S, Park KH, Huvar O, Rozum JC, Albert R. An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks? <i>Journal of Mathematical Biology</i>. 2025;91. doi:<a href=\"https://doi.org/10.1007/s00285-025-02235-8\">10.1007/s00285-025-02235-8</a>"},"corr_author":"1","publication":"Journal of Mathematical Biology","article_type":"original","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"article_number":"11","arxiv":1,"publication_status":"published","isi":1,"date_created":"2025-06-22T22:02:05Z"},{"article_processing_charge":"No","year":"2025","page":"2087-2099","conference":{"end_date":"2025-05-06","name":"ICSE: International Conference on Software Engineering","location":"Ottawa, ON, Canada","start_date":"2025-04-26"},"doi":"10.1109/ICSE55347.2025.00092","scopus_import":"1","ec_funded":1,"publication_identifier":{"isbn":["9798331505691"],"eissn":["1558-1225"]},"oa_version":"None","department":[{"_id":"ToHe"}],"date_created":"2025-07-16T11:32:29Z","publication_status":"published","isi":1,"quality_controlled":"1","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.","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.","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>.","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>","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>"},"corr_author":"1","publication":"47th International Conference on Software Engineering","date_updated":"2025-09-30T14:01:55Z","type":"conference","status":"public","external_id":{"isi":["001538318100163"]},"author":[{"last_name":"Richter","full_name":"Richter, Cedric","first_name":"Cedric"},{"full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","last_name":"Chalupa"},{"last_name":"Jakobs","full_name":"Jakobs, Marie-Christine","first_name":"Marie-Christine"},{"last_name":"Wehrheim","first_name":"Heike","full_name":"Wehrheim, Heike"}],"language":[{"iso":"eng"}],"OA_type":"closed access","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"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.","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"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","day":"01","title":"Cooperative software verification via dynamic program splitting","_id":"20024","date_published":"2025-05-01T00:00:00Z","month":"05","publisher":"IEEE"},{"file_date_updated":"2025-09-02T05:53:47Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","day":"01","project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502","name":"Interface Theory for Security and Privacy"}],"intvolume":"        62","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).","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"}],"external_id":{"isi":["001546115300001"]},"type":"journal_article","status":"public","author":[{"last_name":"Hsu","first_name":"Tzu Han","full_name":"Hsu, Tzu Han"},{"first_name":"Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","full_name":"Oliveira Da Costa, Ana A","last_name":"Oliveira Da Costa"},{"first_name":"Andrew","full_name":"Wintenberg, Andrew","last_name":"Wintenberg"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"first_name":"Borzoo","full_name":"Bonakdarpour, Borzoo","last_name":"Bonakdarpour"}],"language":[{"iso":"eng"}],"has_accepted_license":"1","OA_type":"hybrid","date_updated":"2025-09-30T14:20:11Z","month":"09","PlanS_conform":"1","publisher":"Springer Nature","volume":62,"date_published":"2025-09-01T00:00:00Z","_id":"20186","title":"Gray-box runtime enforcement of hyperproperties","publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"OA_place":"publisher","oa_version":"Published Version","oa":1,"department":[{"_id":"ToHe"}],"scopus_import":"1","ddc":["000"],"file":[{"creator":"dernst","success":1,"file_size":6505049,"file_id":"20267","content_type":"application/pdf","checksum":"90a43350fd4a8c5cb5b1b0e1aea7970d","file_name":"2025_ActaInformatica_Hsu.pdf","date_created":"2025-09-02T05:53:47Z","access_level":"open_access","date_updated":"2025-09-02T05:53:47Z","relation":"main_file"}],"doi":"10.1007/s00236-025-00502-1","article_processing_charge":"Yes (via OA deal)","year":"2025","quality_controlled":"1","citation":{"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>.","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>","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>","short":"T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour, Acta Informatica 62 (2025).","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.","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.","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>."},"corr_author":"1","publication":"Acta Informatica","article_type":"original","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"article_number":"30","publication_status":"published","isi":1,"date_created":"2025-08-17T22:01:36Z","issue":"3"},{"date_created":"2025-08-17T22:01:36Z","publication":"37th International Conference on Computer Aided Verification","citation":{"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>.","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>","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>","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.","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."},"quality_controlled":"1","isi":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"publication_status":"published","doi":"10.1007/978-3-031-98668-0_14","conference":{"location":"Zagreb, Croatia","start_date":"2025-07-23","end_date":"2025-07-25","name":"CAV: Computer Aided Verification"},"page":"281-295","year":"2025","article_processing_charge":"Yes (in subscription journal)","oa":1,"department":[{"_id":"ToHe"}],"oa_version":"Published Version","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031986673"],"eissn":["1611-3349"]},"OA_place":"publisher","file":[{"creator":"dernst","success":1,"file_id":"20266","file_size":1078274,"content_type":"application/pdf","checksum":"15ec1bc9b9409d3b2736f4c9d5f42fd1","file_name":"2025_CAV_Froleyks.pdf","date_created":"2025-09-02T05:46:10Z","access_level":"open_access","date_updated":"2025-09-02T05:46:10Z","relation":"main_file"}],"ec_funded":1,"ddc":["000"],"scopus_import":"1","date_published":"2025-01-01T00:00:00Z","volume":15931,"alternative_title":["LNCS"],"_id":"20189","title":"Introducing certificates to the hardware model checking competition","publisher":"Springer Nature","month":"01","OA_type":"hybrid","has_accepted_license":"1","language":[{"iso":"eng"}],"author":[{"last_name":"Froleyks","first_name":"Nils","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"},{"full_name":"Preiner, Mathias","first_name":"Mathias","last_name":"Preiner"},{"full_name":"Biere, Armin","first_name":"Armin","last_name":"Biere"},{"full_name":"Heljanko, Keijo","first_name":"Keijo","last_name":"Heljanko"}],"type":"conference","external_id":{"isi":["001562507100014"]},"status":"public","date_updated":"2025-12-01T12:34:05Z","day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2025-09-02T05:46:10Z","abstract":[{"lang":"eng","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."}],"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.","intvolume":"     15931","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}]},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2025-09-02T07:34:33Z","day":"22","intvolume":"     15932","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"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.","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."}],"external_id":{"arxiv":["2505.18833"],"isi":["001562506600002"]},"type":"conference","status":"public","author":[{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"orcid":"0000-0001-9864-7475","last_name":"Mallik","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik"},{"last_name":"Sadeghi","full_name":"Sadeghi, Pouya","first_name":"Pouya"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic"}],"language":[{"iso":"eng"}],"has_accepted_license":"1","OA_type":"hybrid","date_updated":"2025-12-01T12:34:41Z","month":"07","publisher":"Springer Nature","volume":15932,"date_published":"2025-07-22T00:00:00Z","_id":"20225","title":"Supermartingale certificates for quantitative omega-regular verification and control","alternative_title":["LNCS"],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031986789"]},"OA_place":"publisher","oa_version":"Published Version","department":[{"_id":"ToHe"}],"oa":1,"scopus_import":"1","ddc":["000"],"ec_funded":1,"file":[{"checksum":"beb1e2637de5b2268cc2262119439113","content_type":"application/pdf","file_id":"20272","file_size":884831,"success":1,"creator":"dernst","relation":"main_file","date_updated":"2025-09-02T07:34:33Z","access_level":"open_access","date_created":"2025-09-02T07:34:33Z","file_name":"2025_CAV_HenzingerT.pdf"}],"conference":{"location":"Zagreb, Croatia","start_date":"2025-07-23","name":"CAV: Computer Aided Verification","end_date":"2025-07-25"},"doi":"10.1007/978-3-031-98679-6_2","article_processing_charge":"Yes (in subscription journal)","page":"29-55","year":"2025","quality_controlled":"1","citation":{"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.","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.","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>.","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>","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>."},"publication":"37th International Conference on Computer Aided Verification","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"arxiv":1,"publication_status":"published","isi":1,"date_created":"2025-08-24T22:01:31Z"},{"year":"2025","article_processing_charge":"No","doi":"10.4230/LIPIcs.CONCUR.2025.21","conference":{"end_date":"2025-08-29","name":"CONCUR: Conference on Concurrency Theory","start_date":"2025-08-26","location":"Aarhus, Denmark"},"ddc":["000"],"file":[{"success":1,"creator":"dernst","content_type":"application/pdf","file_size":1257397,"file_id":"20282","checksum":"9d4054058757a73477e6015b10ed6996","date_created":"2025-09-03T10:01:53Z","file_name":"2025_CONCUR_HenzingerT.pdf","access_level":"open_access","relation":"main_file","date_updated":"2025-09-03T10:01:53Z"}],"ec_funded":1,"scopus_import":"1","oa":1,"department":[{"_id":"ToHe"}],"oa_version":"Published Version","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773898"]},"OA_place":"publisher","date_created":"2025-08-31T22:01:32Z","isi":1,"publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"article_number":"21","arxiv":1,"publication":"36th International Conference on Concurrency Theory","citation":{"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.","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.","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>.","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>.","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>","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.","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>"},"corr_author":"1","quality_controlled":"1","date_updated":"2025-12-01T12:36:52Z","OA_type":"gold","has_accepted_license":"1","language":[{"iso":"eng"}],"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"first_name":"Pavol","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a","full_name":"Kebis, Pavol","last_name":"Kebis"},{"last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien"},{"last_name":"Sarac","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E"}],"status":"public","type":"conference","external_id":{"arxiv":["2506.0515"],"isi":["001570540800021"]},"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."}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"intvolume":"       348","day":"18","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2025-09-03T10:01:53Z","title":"Quantitative language automata","_id":"20253","alternative_title":["LIPIcs"],"volume":348,"date_published":"2025-08-18T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","month":"08"},{"quality_controlled":"1","citation":{"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.","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.","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.","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.","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.","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.","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."},"corr_author":"1","publication":"7th Annual Learning for Dynamics & Control Conference","arxiv":1,"publication_status":"published","date_created":"2025-08-31T22:01:32Z","OA_place":"publisher","publication_identifier":{"eissn":["2640-3498"]},"oa_version":"Published Version","oa":1,"department":[{"_id":"ToHe"},{"_id":"ChLa"}],"scopus_import":"1","ddc":["000"],"file":[{"checksum":"d5236e561560635f5ae1d17de4903033","creator":"dernst","success":1,"file_size":489639,"file_id":"20283","content_type":"application/pdf","date_updated":"2025-09-03T10:32:12Z","relation":"main_file","file_name":"2025_L4DC_HenzingerT.pdf","date_created":"2025-09-03T10:32:12Z","access_level":"open_access"}],"ec_funded":1,"conference":{"location":"Ann Arbor, MI, United States","start_date":"2025-06-04","end_date":"2025-06-06","name":"L4DC: Learning for Dynamics & Control"},"article_processing_charge":"No","year":"2025","page":"804-816","month":"06","publisher":"ML Research Press","volume":283,"date_published":"2025-06-01T00:00:00Z","_id":"20256","alternative_title":["PMLR"],"title":"Predictive monitoring of black-box dynamical systems","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2025-09-03T10:32:12Z","day":"01","intvolume":"       283","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093.\r\n","abstract":[{"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.","lang":"eng"}],"type":"conference","status":"public","external_id":{"arxiv":["2412.16564"]},"author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"last_name":"Kresse","first_name":"Fabian","full_name":"Kresse, Fabian","id":"faff3c84-23f6-11ef-9085-e5187b51c604"},{"orcid":"0000-0001-9864-7475","last_name":"Mallik","first_name":"Kaushik","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"last_name":"Yu","first_name":"Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi"},{"first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699"}],"language":[{"iso":"eng"}],"has_accepted_license":"1","OA_type":"gold","date_updated":"2025-09-03T10:37:59Z"},{"date_created":"2025-09-07T22:01:32Z","arxiv":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"article_number":"30","publication_status":"published","publication":"50th International Symposium on Mathematical Foundations of Computer Science","quality_controlled":"1","corr_author":"1","citation":{"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>","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.","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>","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>.","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>.","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.","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."},"year":"2025","article_processing_charge":"Yes","doi":"10.4230/LIPIcs.MFCS.2025.30","conference":{"end_date":"2025-08-29","name":"MFCS: Mathematical Foundations of Computer Science","location":"Warsaw, Poland","start_date":"2025-08-25"},"ddc":["000"],"ec_funded":1,"file":[{"access_level":"open_access","file_name":"2025_MFCS_Brice.pdf","date_created":"2025-09-08T07:11:12Z","date_updated":"2025-09-08T07:11:12Z","relation":"main_file","file_id":"20306","file_size":1149694,"content_type":"application/pdf","creator":"dernst","success":1,"checksum":"9bc6b8e537662d371d2a27444cbc0b75"}],"scopus_import":"1","oa_version":"Published Version","department":[{"_id":"ToHe"}],"oa":1,"publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773881"]},"OA_place":"publisher","_id":"20290","alternative_title":["LIPIcs"],"title":"Finding equilibria: Simpler for pessimists, simplest for optimists","volume":345,"date_published":"2025-08-20T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","month":"08","date_updated":"2025-09-08T07:15:40Z","language":[{"iso":"eng"}],"OA_type":"gold","has_accepted_license":"1","external_id":{"arxiv":["2502.0531"]},"type":"conference","status":"public","author":[{"last_name":"Brice","full_name":"Brice, Léonard","first_name":"Léonard"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Thejaswini","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","full_name":"Thejaswini, K. S.","first_name":"K. S."}],"abstract":[{"lang":"eng","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."}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093"}],"intvolume":"       345","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. ","day":"20","file_date_updated":"2025-09-08T07:11:12Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"file_date_updated":"2025-09-08T06:56:56Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"20","acknowledgement":"This work is a part of project VAMOS that has received funding from the European Research Council (ERC), grant agreement No 101020093.","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"intvolume":"       345","abstract":[{"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.","lang":"eng"}],"author":[{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Prakash, Aditya","first_name":"Aditya","last_name":"Prakash"},{"last_name":"Thejaswini","full_name":"Thejaswini, K. S.","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","first_name":"K. S."}],"status":"public","type":"conference","external_id":{"arxiv":["2502.12872"]},"OA_type":"gold","has_accepted_license":"1","language":[{"iso":"eng"}],"date_updated":"2025-09-08T07:06:11Z","month":"08","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":345,"date_published":"2025-08-20T00:00:00Z","_id":"20291","alternative_title":["LIPIcs"],"title":"Resolving nondeterminism with randomness","publication_identifier":{"isbn":["9783959773881"],"issn":["1868-8969"]},"OA_place":"publisher","oa":1,"department":[{"_id":"ToHe"}],"oa_version":"Published Version","scopus_import":"1","file":[{"checksum":"6068b772aba6cb0d01f3e5a90abed973","file_id":"20305","file_size":1009644,"content_type":"application/pdf","creator":"dernst","success":1,"date_updated":"2025-09-08T06:56:56Z","relation":"main_file","access_level":"open_access","file_name":"2025_MFCS_HenzingerT.pdf","date_created":"2025-09-08T06:56:56Z"}],"ddc":["000"],"ec_funded":1,"conference":{"location":"Warsaw, Poland","start_date":"2025-08-25","name":"MFCS: Mathematical Foundations of Computer Science","end_date":"2025-08-29"},"doi":"10.4230/LIPIcs.MFCS.2025.57","article_processing_charge":"No","year":"2025","citation":{"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.","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>","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>","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>.","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>.","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.","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."},"corr_author":"1","quality_controlled":"1","publication":"50th International Symposium on Mathematical Foundations of Computer Science","arxiv":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"article_number":"57","publication_status":"published","date_created":"2025-09-07T22:01:32Z"},{"intvolume":"         2","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"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.","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"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2025-09-08T08:46:31Z","day":"03","date_updated":"2025-09-08T08:54:24Z","status":"public","type":"conference","external_id":{"arxiv":["2506.00496"]},"author":[{"last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger"},{"full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","first_name":"Konstantin","orcid":"0000-0001-8974-2542","last_name":"Kueffner"},{"first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475"},{"first_name":"David","full_name":"Pape, David","last_name":"Pape"}],"language":[{"iso":"eng"}],"has_accepted_license":"1","month":"08","publisher":"Association for Computing Machinery","title":"Monitoring robustness and individual fairness","_id":"20292","date_published":"2025-08-03T00:00:00Z","volume":2,"scopus_import":"1","ddc":["000"],"ec_funded":1,"file":[{"date_updated":"2025-09-08T08:46:31Z","relation":"main_file","file_name":"2025_KDD_Gupta.pdf","date_created":"2025-09-08T08:46:31Z","access_level":"open_access","checksum":"81e18cdf9ca5f6dfa79425b326ea9725","creator":"dernst","success":1,"file_id":"20310","file_size":7745940,"content_type":"application/pdf"}],"OA_place":"publisher","publication_identifier":{"issn":["2154-817X"],"isbn":["9798400714542"]},"oa_version":"Published Version","department":[{"_id":"ToHe"}],"oa":1,"article_processing_charge":"No","page":"790-801","year":"2025","conference":{"name":"KDD: Conference on Knowledge Discovery and Data Mining","end_date":"2025-08-07","location":"Toronto, Canada","start_date":"2025-08-03"},"doi":"10.1145/3711896.3737054","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"arxiv":1,"publication_status":"published","quality_controlled":"1","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>","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.","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>","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>.","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.","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.","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>."},"corr_author":"1","publication":"Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining","related_material":{"link":[{"url":"https://github.com/ariez-xyz/clemont","relation":"software"}]},"date_created":"2025-09-07T22:01:33Z"},{"acknowledged_ssus":[{"_id":"ScienComp"}],"volume":288,"date_published":"2025-06-01T00:00:00Z","_id":"20296","alternative_title":["PMLR"],"title":"Logic gate neural networks are good for verification","month":"06","publisher":"ML Research Press","external_id":{"arxiv":["2505.19932"]},"status":"public","type":"conference","author":[{"first_name":"Fabian","full_name":"Kresse, Fabian","id":"faff3c84-23f6-11ef-9085-e5187b51c604","last_name":"Kresse"},{"last_name":"Yu","full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","first_name":"Zhengqi"},{"full_name":"Lampert, Christoph","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","first_name":"Christoph","orcid":"0000-0001-8622-7887","last_name":"Lampert"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"language":[{"iso":"eng"}],"OA_type":"diamond","has_accepted_license":"1","date_updated":"2025-09-09T08:12:44Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2025-09-09T08:10:13Z","day":"01","intvolume":"       288","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"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).","abstract":[{"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.","lang":"eng"}],"date_created":"2025-09-07T22:01:34Z","quality_controlled":"1","corr_author":"1","citation":{"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.","short":"F. Kresse, E. Yu, C. Lampert, T.A. Henzinger, in:, 2nd International Conferenceon Neuro-Symbolic Systems, 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.","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.","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.","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."},"publication":"2nd International Conferenceon Neuro-Symbolic Systems","arxiv":1,"publication_status":"published","article_number":"26","conference":{"name":"NeuS: International Conferenceon Neuro-Symbolic Systems","end_date":"2025-05-30","start_date":"2025-05-28","location":"Philadephia, PA, United States"},"article_processing_charge":"No","year":"2025","OA_place":"publisher","publication_identifier":{"eissn":["2640-3498"]},"oa_version":"Published Version","department":[{"_id":"ChLa"},{"_id":"ToHe"}],"oa":1,"scopus_import":"1","ec_funded":1,"ddc":["000"],"file":[{"date_created":"2025-09-09T08:10:13Z","file_name":"2025_NeuS_Kresse.pdf","access_level":"open_access","relation":"main_file","date_updated":"2025-09-09T08:10:13Z","success":1,"creator":"dernst","content_type":"application/pdf","file_size":295466,"file_id":"20314","checksum":"90a32defed34787e771a5c1623b6b0d2"}]},{"title":"Information-Flow Interfaces and Security Lattices","_id":"20723","alternative_title":["LNCS"],"date_published":"2025-10-02T00:00:00Z","volume":15471,"month":"10","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2406.14374"}],"publisher":"Springer Nature","date_updated":"2025-12-09T07:57:55Z","place":"Cham","external_id":{"arxiv":["2406.14374"]},"status":"public","type":"book_chapter","author":[{"last_name":"Bartocci","full_name":"Bartocci, Ezio","first_name":"Ezio"},{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic"},{"first_name":"Ana","full_name":"Oliveira da Costa, Ana","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","orcid":"0000-0002-8741-5799","last_name":"Oliveira da Costa"}],"language":[{"iso":"eng"}],"OA_type":"green","project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"intvolume":"     15471","acknowledgement":"This project was funded in part by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502 and by the ERC-2020-AdG 101020093.","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"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"02","date_created":"2025-12-01T15:44:58Z","arxiv":1,"publication_status":"published","quality_controlled":"1","citation":{"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>.","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.","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.","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>.","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>","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.","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>"},"corr_author":"1","publication":"Engineering Safe and Trustworthy Cyber Physical Systems","article_processing_charge":"No","page":"251-263","year":"2025","doi":"10.1007/978-3-031-97537-0_15","scopus_import":"1","ec_funded":1,"OA_place":"repository","publication_identifier":{"isbn":["9783031975363"],"eissn":["1611-3349"],"eisbn":["9783031975370"],"issn":["0302-9743"]},"oa_version":"Preprint","oa":1,"department":[{"_id":"ToHe"}]},{"day":"11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"As AI-based decision-makers increasingly influence human lives, it is a growing concern that their decisions may be unfair or biased with respect to people's protected attributes, such as gender and race. Most existing bias prevention measures provide probabilistic fairness guarantees in the long run, and it is possible that the decisions are biased on any decision sequence of fixed length. We introduce *fairness shielding*, where a symbolic decision-maker---the fairness shield---continuously monitors the sequence of decisions of another deployed black-box decision-maker, and makes interventions so that a given fairness criterion is met while the total intervention costs are minimized. We present four different algorithms for computing fairness shields, among which one guarantees fairness over fixed horizons, and three guarantee fairness periodically after fixed intervals. Given a distribution over future decisions and their intervention costs, our algorithms solve different instances of bounded-horizon optimal control problems with different levels of computational costs and optimality guarantees. Our empirical evaluation demonstrates the effectiveness of these shields in ensuring fairness while maintaining cost efficiency across various scenarios.","lang":"eng"}],"acknowledgement":"This work is partly supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093. It is also partially supported by the State Government of Styria, Austria – Department Zukunftsfonds Steiermark.","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"intvolume":"        39","OA_type":"green","language":[{"iso":"eng"}],"author":[{"orcid":"0000-0002-0783-904X","last_name":"Cano Cordoba","first_name":"Filip","full_name":"Cano Cordoba, Filip","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1"},{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Bettina","full_name":"Könighofer, Bettina","last_name":"Könighofer"},{"full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","first_name":"Konstantin","orcid":"0000-0001-8974-2542","last_name":"Kueffner"},{"first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475"}],"status":"public","type":"conference","external_id":{"arxiv":["2412.11994"]},"date_updated":"2026-02-16T12:24:30Z","publisher":"Association for the Advancement of Artificial Intelligence","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.11994"}],"month":"04","date_published":"2025-04-11T00:00:00Z","volume":39,"title":"Fairness shields: Safeguarding against biased decision makers","_id":"19665","department":[{"_id":"ToHe"}],"oa":1,"oa_version":"Preprint","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"OA_place":"repository","ec_funded":1,"scopus_import":"1","doi":"10.1609/aaai.v39i15.33719","conference":{"end_date":"2025-03-04","name":"AAAI: Conference on Artificial Intelligence","location":"Philadelphia, PA, United States","start_date":"2025-02-25"},"year":"2025","page":"15659-15668","article_processing_charge":"No","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","corr_author":"1","citation":{"ista":"Cano Cordoba F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. 2025. Fairness shields: Safeguarding against biased decision makers. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 15659–15668.","ieee":"F. Cano Cordoba, T. A. Henzinger, B. Könighofer, K. Kueffner, and K. Mallik, “Fairness shields: Safeguarding against biased decision makers,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 15, pp. 15659–15668.","chicago":"Cano Cordoba, Filip, Thomas A Henzinger, Bettina Könighofer, Konstantin Kueffner, and Kaushik Mallik. “Fairness Shields: Safeguarding against Biased Decision Makers.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:15659–68. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">https://doi.org/10.1609/aaai.v39i15.33719</a>.","mla":"Cano Cordoba, Filip, et al. “Fairness Shields: Safeguarding against Biased Decision Makers.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 15, Association for the Advancement of Artificial Intelligence, 2025, pp. 15659–68, doi:<a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">10.1609/aaai.v39i15.33719</a>.","ama":"Cano Cordoba F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. Fairness shields: Safeguarding against biased decision makers. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:15659-15668. doi:<a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">10.1609/aaai.v39i15.33719</a>","apa":"Cano Cordoba, F., Henzinger, T. A., Könighofer, B., Kueffner, K., &#38; Mallik, K. (2025). Fairness shields: Safeguarding against biased decision makers. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 15659–15668). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">https://doi.org/10.1609/aaai.v39i15.33719</a>","short":"F. Cano Cordoba, T.A. Henzinger, B. Könighofer, K. Kueffner, K. Mallik, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 15659–15668."},"quality_controlled":"1","publication_status":"published","arxiv":1,"date_created":"2025-05-11T22:02:39Z","issue":"15"},{"ec_funded":1,"scopus_import":"1","oa":1,"department":[{"_id":"ToHe"}],"oa_version":"Preprint","OA_place":"repository","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"year":"2025","page":"26409-26417","article_processing_charge":"No","conference":{"end_date":"2025-03-04","name":"AAAI: Conference on Artificial Intelligence","location":"Philadelphia, PA, United States","start_date":"2025-02-25"},"doi":"10.1609/aaai.v39i25.34840","arxiv":1,"publication_status":"published","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","corr_author":"1","citation":{"chicago":"Yu, Emily, Dorde Zikelic, and Thomas A Henzinger. “Neural Control and Certificate Repair via Runtime Monitoring.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:26409–17. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">https://doi.org/10.1609/aaai.v39i25.34840</a>.","ieee":"E. Yu, D. Zikelic, and T. A. Henzinger, “Neural control and certificate repair via runtime monitoring,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 25, pp. 26409–26417.","ista":"Yu E, Zikelic D, Henzinger TA. 2025. Neural control and certificate repair via runtime monitoring. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 26409–26417.","mla":"Yu, Emily, et al. “Neural Control and Certificate Repair via Runtime Monitoring.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 25, Association for the Advancement of Artificial Intelligence, 2025, pp. 26409–17, doi:<a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">10.1609/aaai.v39i25.34840</a>.","apa":"Yu, E., Zikelic, D., &#38; Henzinger, T. A. (2025). Neural control and certificate repair via runtime monitoring. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 26409–26417). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">https://doi.org/10.1609/aaai.v39i25.34840</a>","short":"E. Yu, D. Zikelic, T.A. Henzinger, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 26409–26417.","ama":"Yu E, Zikelic D, Henzinger TA. Neural control and certificate repair via runtime monitoring. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:26409-26417. doi:<a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">10.1609/aaai.v39i25.34840</a>"},"quality_controlled":"1","issue":"25","date_created":"2025-05-11T22:02:40Z","abstract":[{"text":"Learning-based methods provide a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. To ensure the satisfaction of a safety property, learning-based methods jointly learn a control policy together with a certificate function for the property. Popular examples include barrier functions for safety and Lyapunov functions for asymptotic stability. While there has been significant progress on learning-based control with certificate functions in the white-box setting, where the correctness of the certificate function can be formally verified, there has been little work on ensuring their reliability in the black-box setting where the system dynamics are unknown. In this work, we consider the problems of certifying and repairing neural network control policies and certificate functions in the black-box setting. We propose a novel framework that utilizes runtime monitoring to detect system behaviors that violate the property of interest under some initially trained neural network policy and certificate. These violating behaviors are used to extract new training data, that is used to re-train the neural network policy and the certificate function and to ultimately repair them. We demonstrate the effectiveness of our approach empirically by using it to repair and to boost the safety rate of neural network policies learned by a state-of-the-art method for learning-based control on two autonomous system control tasks.","lang":"eng"}],"acknowledgement":"This work was supported in part by the ERC project ERC2020-AdG 101020093","intvolume":"        39","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"day":"11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-05-12T09:49:25Z","OA_type":"green","language":[{"iso":"eng"}],"author":[{"last_name":"Yu","first_name":"Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi"},{"orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"status":"public","external_id":{"arxiv":["2412.12996"]},"type":"conference","publisher":"Association for the Advancement of Artificial Intelligence","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.12996"}],"month":"04","title":"Neural control and certificate repair via runtime monitoring","_id":"19668","date_published":"2025-04-11T00:00:00Z","volume":39},{"day":"01","file_date_updated":"2025-06-02T07:10:35Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"Cooperative verification is gaining momentum in recent years. The usual setup in cooperative verification is that a verifier A is run with some pre-defined resources, and if it is not able to verify the program, the verification task is passed to a verifier B together with information learned about the program by verifier A, then the chain can continue to a verifier C, and so on. This scheme is static: tools run one after another in a fixed pre-defined order and fixed parameters and resource limits (the scheme may differ for properties to be analyzed, though).\r\n\r\nBubaak is a program analysis tool that allows to run multiple program verifiers in a dynamically changing combination of parallel and sequential portfolios. Bubaak starts the verification process by invoking an initial set of tasks; every task, when it is done (e.g., because of hitting a time limit or finishing its job), rewrites itself into one or more successor tasks. New tasks can be also spawned upon events generated by other tasks. This all happens dynamically based on the information gathered by finished and running tasks. During their execution, tasks that run in parallel can exchange (partial) verification artifacts, either directly or with Bubaak as an intermediary."}],"acknowledgement":"This work was in part supported by the ERC-2020-AdG 10102009 grant, and in part by the German Research Foundation (DFG) - WE2290/13-2 (Coop2).","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"intvolume":"     15698","has_accepted_license":"1","OA_type":"hybrid","language":[{"iso":"eng"}],"author":[{"last_name":"Chalupa","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"last_name":"Richter","first_name":"Cedric","full_name":"Richter, Cedric"}],"status":"public","type":"conference","date_updated":"2025-06-02T07:21:41Z","publisher":"Springer Nature","month":"05","date_published":"2025-05-01T00:00:00Z","volume":15698,"_id":"19739","title":"BUBAAK: Dynamic cooperative verification","alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"oa":1,"oa_version":"Published Version","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031906596"],"issn":["0302-9743"]},"OA_place":"publisher","ddc":["000"],"ec_funded":1,"file":[{"access_level":"open_access","date_created":"2025-06-02T07:10:35Z","file_name":"2025_TACAS_Chalupa.pdf","relation":"main_file","date_updated":"2025-06-02T07:10:35Z","content_type":"application/pdf","file_id":"19766","file_size":259050,"success":1,"creator":"dernst","checksum":"3f604f25dbe37383acb7f8308aad3ca6"}],"scopus_import":"1","doi":"10.1007/978-3-031-90660-2_14","conference":{"end_date":"2025-05-08","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Hamilton, ON, Canada","start_date":"2025-05-03"},"year":"2025","page":"212-216","article_processing_charge":"No","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","corr_author":"1","citation":{"chicago":"Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15698:212–16. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">https://doi.org/10.1007/978-3-031-90660-2_14</a>.","ieee":"M. Chalupa and C. Richter, “BUBAAK: Dynamic cooperative verification,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15698, pp. 212–216.","ista":"Chalupa M, Richter C. 2025. BUBAAK: Dynamic cooperative verification. 31st 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. 15698, 212–216.","mla":"Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15698, Springer Nature, 2025, pp. 212–16, doi:<a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">10.1007/978-3-031-90660-2_14</a>.","apa":"Chalupa, M., &#38; Richter, C. (2025). BUBAAK: Dynamic cooperative verification. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15698, pp. 212–216). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">https://doi.org/10.1007/978-3-031-90660-2_14</a>","short":"M. Chalupa, C. Richter, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 212–216.","ama":"Chalupa M, Richter C. BUBAAK: Dynamic cooperative verification. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15698. Springer Nature; 2025:212-216. doi:<a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">10.1007/978-3-031-90660-2_14</a>"},"quality_controlled":"1","publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"date_created":"2025-05-25T22:17:04Z"},{"month":"12","publisher":"Springer Nature","date_published":"2025-12-09T00:00:00Z","volume":62,"title":"Hypernode automata","_id":"20866","file_date_updated":"2026-01-05T12:26:43Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"09","acknowledgement":"This work was supported in part by the Austrian Science Fund (FWF) SFB project SpyCoDe 10.55776/F85, by the FWF projects ZK-35 and W1255-N23, and by the ERC Advanced Grant VAMOS 101020093. Open access funding provided by Institute of Science and Technology (IST Austria).","intvolume":"        62","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"abstract":[{"lang":"eng","text":"In this work, we present hypernode automata as a specification formalism for hyperproperties of systems whose executions may be misaligned among themselves, such as concurrent systems. These automata consist of nodes labeled with hypernode logic formulas and transitions marked with synchronizing actions. Hypernode logic formulas establish relations between sequences of variable values among different system executions. This logic enables both synchronous and asynchronous analysis of traces. In its asynchronous view on execution traces, hypernode formulas establish relations on the order of value changes for each variable without correlating their timing. In both views, the analysis of different execution traces is synchronized through the transitions of hypernode automata. By combining logic’s declarative nature with automata’s procedural power, hypernode automata seamlessly integrate asynchronicity requirements at the node level with synchronicity between node transitions. We show that the model-checking problem for hypernode automata is decidable for specifications where each node specifies either a synchronous or an asynchronous requirement for the system’s executions, but not both."}],"author":[{"last_name":"Bartocci","full_name":"Bartocci, Ezio","first_name":"Ezio"},{"last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic"},{"last_name":"Oliveira da Costa","orcid":"0000-0002-8741-5799","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","full_name":"Oliveira da Costa, Ana","first_name":"Ana"}],"status":"public","external_id":{"arxiv":["2305.02836"]},"type":"journal_article","has_accepted_license":"1","OA_type":"hybrid","language":[{"iso":"eng"}],"date_updated":"2026-01-05T12:27:41Z","corr_author":"1","citation":{"apa":"Bartocci, E., Chalupa, M., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2025). Hypernode automata. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-025-00509-8\">https://doi.org/10.1007/s00236-025-00509-8</a>","short":"E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, Acta Informatica 62 (2025).","ama":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata. <i>Acta Informatica</i>. 2025;62(4). doi:<a href=\"https://doi.org/10.1007/s00236-025-00509-8\">10.1007/s00236-025-00509-8</a>","mla":"Bartocci, Ezio, et al. “Hypernode Automata.” <i>Acta Informatica</i>, vol. 62, no. 4, 43, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00236-025-00509-8\">10.1007/s00236-025-00509-8</a>.","chicago":"Bartocci, Ezio, Marek Chalupa, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Hypernode Automata.” <i>Acta Informatica</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00236-025-00509-8\">https://doi.org/10.1007/s00236-025-00509-8</a>.","ieee":"E. Bartocci, M. Chalupa, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode automata,” <i>Acta Informatica</i>, vol. 62, no. 4. Springer Nature, 2025.","ista":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025. Hypernode automata. Acta Informatica. 62(4), 43."},"quality_controlled":"1","publication":"Acta Informatica","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"publication_status":"published","article_type":"original","article_number":"43","arxiv":1,"date_created":"2025-12-29T12:07:12Z","issue":"4","related_material":{"record":[{"status":"public","id":"14405","relation":"earlier_version"}]},"publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"OA_place":"publisher","oa":1,"department":[{"_id":"ToHe"}],"oa_version":"Published Version","scopus_import":"1","ec_funded":1,"file":[{"checksum":"06ed45a1218ad8464818803ae2968aaf","file_id":"20944","file_size":7117003,"content_type":"application/pdf","creator":"dernst","success":1,"date_updated":"2026-01-05T12:26:43Z","relation":"main_file","access_level":"open_access","file_name":"2025_ActaInformatica_Bartocci.pdf","date_created":"2026-01-05T12:26:43Z"}],"ddc":["000"],"doi":"10.1007/s00236-025-00509-8","article_processing_charge":"Yes (via OA deal)","year":"2025"}]