[{"OA_place":"publisher","file_date_updated":"2026-06-22T08:18:41Z","oa_version":"Published Version","alternative_title":["LNCS"],"das_tickbox":"0","date_updated":"2026-06-22T08:21:09Z","publication":"27th International Symposium on Formal Methods","volume":16557,"ddc":["000"],"article_processing_charge":"No","conference":{"name":"FM: Formal Methods","start_date":"2026-05-18","end_date":"2026-05-22","location":"Tokyo, Japan"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","author":[{"full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","first_name":"Marek"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Sarac","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E"},{"full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","first_name":"Zhengqi","last_name":"Yu","orcid":"0000-0002-4993-773X"}],"title":"Quantitative monitoring of Signal First-Order logic","citation":{"ista":"Chalupa M, Henzinger TA, Sarac NE, Yu E. 2026. Quantitative monitoring of Signal First-Order logic. 27th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 16557, 214–233.","ama":"Chalupa M, Henzinger TA, Sarac NE, Yu E. Quantitative monitoring of Signal First-Order logic. In: 27th International Symposium on Formal Methods. Vol 16557. Springer Nature; 2026:214-233. doi:10.1007/978-3-032-26220-2_11","apa":"Chalupa, M., Henzinger, T. A., Sarac, N. E., & Yu, E. (2026). Quantitative monitoring of Signal First-Order logic. In 27th International Symposium on Formal Methods (Vol. 16557, pp. 214–233). Tokyo, Japan: Springer Nature. https://doi.org/10.1007/978-3-032-26220-2_11","ieee":"M. Chalupa, T. A. Henzinger, N. E. Sarac, and E. Yu, “Quantitative monitoring of Signal First-Order logic,” in 27th International Symposium on Formal Methods, Tokyo, Japan, 2026, vol. 16557, pp. 214–233.","mla":"Chalupa, Marek, et al. “Quantitative Monitoring of Signal First-Order Logic.” 27th International Symposium on Formal Methods, vol. 16557, Springer Nature, 2026, pp. 214–33, doi:10.1007/978-3-032-26220-2_11.","chicago":"Chalupa, Marek, Thomas A Henzinger, Naci E Sarac, and Emily Yu. “Quantitative Monitoring of Signal First-Order Logic.” In 27th International Symposium on Formal Methods, 16557:214–33. Springer Nature, 2026. https://doi.org/10.1007/978-3-032-26220-2_11.","short":"M. Chalupa, T.A. Henzinger, N.E. Sarac, E. Yu, in:, 27th International Symposium on Formal Methods, Springer Nature, 2026, pp. 214–233."},"day":"18","page":"214-233","oa":1,"intvolume":" 16557","quality_controlled":"1","doi":"10.1007/978-3-032-26220-2_11","keyword":["Signal first-order logic","Robustness-based quantitative semantics","Online runtime monitoring"],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"_id":"22006","month":"05","has_accepted_license":"1","publication_status":"published","external_id":{"arxiv":["2603.00728"]},"publisher":"Springer Nature","file":[{"content_type":"application/pdf","date_updated":"2026-06-22T08:18:41Z","relation":"main_file","checksum":"7055199ecb985e9e2e272f4988827067","file_size":849237,"access_level":"open_access","file_id":"22113","file_name":"2026_LNCS_Chalupa.pdf","date_created":"2026-06-22T08:18:41Z","success":1,"creator":"dernst"}],"OA_type":"hybrid","date_created":"2026-06-14T22:01:44Z","abstract":[{"text":"Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.","lang":"eng"}],"year":"2026","publication_identifier":{"isbn":["9783032262196"],"eissn":["1611-3349"],"issn":["0302-9743"]},"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported by the European Research Council (ERC) Grants VAMOS (No. 101020093) and HYPER (No. 101055412), and by the Advanced Research and Invention Agency under the Safeguarded AI programme (MSAI-PR01-P047).","date_published":"2026-05-18T00:00:00Z","scopus_import":"1","department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"status":"public","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"fulldoi":"https://doi.org/10.1007/978-3-032-26220-2_11","arxiv":1},{"language":[{"iso":"eng"}],"status":"public","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.","date_published":"2026-01-01T00:00:00Z","scopus_import":"1","department":[{"_id":"ToHe"}],"corr_author":"1","ec_funded":1,"issue":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"PlanS_conform":"1","fulldoi":"https://doi.org/10.1145/3737447","has_accepted_license":"1","publication_status":"published","publisher":"Association for Computing Machinery","file":[{"file_name":"2026_CommACM_Barrett.pdf","access_level":"open_access","file_id":"21028","creator":"dernst","success":1,"date_created":"2026-01-21T08:52:07Z","date_updated":"2026-01-21T08:52:07Z","content_type":"application/pdf","file_size":2623108,"checksum":"d909a9091c254b2d18ba014124663f69","relation":"main_file"}],"month":"01","_id":"21012","publication_identifier":{"eissn":["1557-7317"],"issn":["0001-0782"]},"date_created":"2026-01-20T10:08:21Z","OA_type":"hybrid","abstract":[{"text":"In certifiable machine learning, AI systems produce not only results but also verifiable certificates that the results can be trusted.","lang":"eng"}],"year":"2026","day":"01","page":"66-75","article_type":"original","citation":{"mla":"Barrett, Clark, et al. “Certificates in AI: Learn but Verify.” Communications of the ACM, vol. 69, no. 1, Association for Computing Machinery, 2026, pp. 66–75, doi:10.1145/3737447.","short":"C. Barrett, T.A. Henzinger, S.A. Seshia, Communications of the ACM 69 (2026) 66–75.","chicago":"Barrett, Clark, Thomas A Henzinger, and Sanjit A. Seshia. “Certificates in AI: Learn but Verify.” Communications of the ACM. Association for Computing Machinery, 2026. https://doi.org/10.1145/3737447.","ieee":"C. Barrett, T. A. Henzinger, and S. A. Seshia, “Certificates in AI: Learn but verify,” Communications of the ACM, vol. 69, no. 1. Association for Computing Machinery, pp. 66–75, 2026.","ama":"Barrett C, Henzinger TA, Seshia SA. Certificates in AI: Learn but verify. Communications of the ACM. 2026;69(1):66-75. doi:10.1145/3737447","apa":"Barrett, C., Henzinger, T. A., & Seshia, S. A. (2026). Certificates in AI: Learn but verify. Communications of the ACM. Association for Computing Machinery. https://doi.org/10.1145/3737447","ista":"Barrett C, Henzinger TA, Seshia SA. 2026. Certificates in AI: Learn but verify. Communications of the ACM. 69(1), 66–75."},"doi":"10.1145/3737447","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"oa":1,"intvolume":" 69","quality_controlled":"1","oa_version":"Published Version","date_updated":"2026-01-21T08:55:24Z","OA_place":"publisher","file_date_updated":"2026-01-21T08:52:07Z","article_processing_charge":"Yes (via OA deal)","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","title":"Certificates in AI: Learn but verify","author":[{"full_name":"Barrett, Clark","first_name":"Clark","last_name":"Barrett"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"last_name":"Seshia","first_name":"Sanjit A.","full_name":"Seshia, Sanjit A."}],"publication":"Communications of the ACM","volume":69,"ddc":["000"]},{"fulldoi":"https://doi.org/10.15479/AT-ISTA-21401","ec_funded":1,"status":"public","language":[{"iso":"eng"}],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"corr_author":"1","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","date_published":"2026-03-05T00:00:00Z","publication_identifier":{"issn":["2791-4585"]},"year":"2026","date_created":"2026-03-05T15:20:47Z","abstract":[{"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","lang":"eng"}],"publisher":"Institute of Science and Technology Austria","file":[{"content_type":"application/pdf","date_updated":"2026-03-10T15:20:09Z","relation":"main_file","checksum":"3f49f05c9d123e14d7adb73d3bc50fe2","file_size":766048,"access_level":"open_access","file_id":"21404","file_name":"2026_Karimi_Mahyar_Thesis.pdf","date_created":"2026-03-06T14:06:25Z","creator":"mkarimi"},{"date_created":"2026-03-06T14:06:25Z","creator":"mkarimi","access_level":"closed","file_id":"21405","file_name":"2026_Karimi_Mahyar_Thesis_src.zip","relation":"source_file","checksum":"8fb9db4b4187e26443369a993427a5ff","file_size":1243394,"content_type":"application/zip","date_updated":"2026-03-06T14:06:25Z"}],"has_accepted_license":"1","publication_status":"published","supervisor":[{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"}],"_id":"21401","month":"03","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"_id":"34a4ce89-11ca-11ed-8bc3-8cc37fb6e11f","name":"Security and Privacy by Design for Complex Systems","grant_number":"F8512"}],"doi":"10.15479/AT-ISTA-21401","keyword":["Privacy-preserving verification","Runtime verification","Monitoring","Reactive functionalities","Cryptographic protocols"],"oa":1,"page":"60","day":"05","citation":{"ieee":"M. Karimi, “Privacy-preserving runtime verification,” Institute of Science and Technology Austria, 2026.","short":"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. https://doi.org/10.15479/AT-ISTA-21401.","mla":"Karimi, Mahyar. Privacy-Preserving Runtime Verification. Institute of Science and Technology Austria, 2026, doi:10.15479/AT-ISTA-21401.","ista":"Karimi M. 2026. Privacy-preserving runtime verification. Institute of Science and Technology Austria.","apa":"Karimi, M. (2026). Privacy-preserving runtime verification. Institute of Science and Technology Austria. https://doi.org/10.15479/AT-ISTA-21401","ama":"Karimi M. Privacy-preserving runtime verification. 2026. doi:10.15479/AT-ISTA-21401"},"type":"dissertation","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","author":[{"first_name":"Mahyar","last_name":"Karimi","full_name":"Karimi, Mahyar","id":"6e5417ba-5355-11ee-ae5a-94c2e510b26b","orcid":"0009-0005-0820-1696"}],"title":"Privacy-preserving runtime verification","article_processing_charge":"No","ddc":["000"],"degree_awarded":"MS","date_updated":"2026-03-13T13:37:20Z","oa_version":"Published Version","alternative_title":["ISTA Master’s Thesis"],"OA_place":"repository","file_date_updated":"2026-03-10T15:20:09Z","related_material":{"record":[{"status":"public","id":"21020","relation":"part_of_dissertation"}]}},{"supplementarymaterial":"no","fulldoi":"https://doi.org/10.5220/0014483200004052","ec_funded":1,"status":"public","language":[{"iso":"eng"}],"scopus_import":"1","department":[{"_id":"ToHe"}],"corr_author":"1","date_published":"2026-04-01T00:00:00Z","acknowledgement":"This work has been supported by the European Research Council under Grant No.: ERC-2020-AdG\r\n101020093. LLM–based tools have been used as\r\nwriting assistance to help improve presentation.\r\n","publication_identifier":{"issn":["2184-3589"],"isbn":["9789897587962"],"eissn":["2184-433X"]},"year":"2026","abstract":[{"text":"Modern AI systems increasingly rely on opaque, highly complex models whose inner workings remain inaccessible even to experts. This opacity creates challenges for trust, accountability, and compliance with\r\nemerging regulatory expectations such as the “right to an explanation”. While traditional explainability methods—feature attributions, counterfactuals, surrogate models—and interpretable model classes provide valuable insights for engineers, they often fall short of delivering the contextual, conversational explanations that\r\nreal users expect. Large Language Models (LLMs) offer a promising new avenue for explanation due to their\r\nability to engage interactively, adapt to user needs, and translate technical outputs into more accessible reasoning. However, their tendencies toward hallucination, conflict avoidance, and oversimplification introduce\r\nserious risks when used as explanatory agents. This paper analyzes these opportunities and limitations, examines verification strategies for ensuring explanation fidelity, and situates LLM-generated explanations within\r\nbroader concerns about public trust. The paper concludes by outlining best practices and future research directions for building robust, verifiable, and human-aligned explanation systems.","lang":"eng"}],"date_created":"2026-06-21T22:03:00Z","OA_type":"green","publisher":"Science and Technology Publications","publication_status":"published","_id":"22103","month":"04","main_file_link":[{"open_access":"1","url":"https://filipcano.org/files/icaart26llm.pdf"}],"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"keyword":["Explainable AI","Large Language Models","Trust in AI"],"doi":"10.5220/0014483200004052","quality_controlled":"1","intvolume":" 5","oa":1,"page":"4689-4696","day":"01","citation":{"ieee":"F. Cano Cordoba, “Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants,” in Proceedings of the 18th International Conference on Agents and Artificial Intelligence, Marbella, Spain, 2026, vol. 5, pp. 4689–4696.","mla":"Cano Cordoba, Filip. “Explaining Decisions One Conversation at a Time: Opportunities and Risks of LLMs as Explainability Assistants.” Proceedings of the 18th International Conference on Agents and Artificial Intelligence, vol. 5, Science and Technology Publications, 2026, pp. 4689–96, doi:10.5220/0014483200004052.","chicago":"Cano Cordoba, Filip. “Explaining Decisions One Conversation at a Time: Opportunities and Risks of LLMs as Explainability Assistants.” In Proceedings of the 18th International Conference on Agents and Artificial Intelligence, 5:4689–96. Science and Technology Publications, 2026. https://doi.org/10.5220/0014483200004052.","short":"F. Cano Cordoba, in:, Proceedings of the 18th International Conference on Agents and Artificial Intelligence, Science and Technology Publications, 2026, pp. 4689–4696.","ista":"Cano Cordoba F. 2026. Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants. Proceedings of the 18th International Conference on Agents and Artificial Intelligence. ICAART: International Conference on Agents and Artificial Intelligence vol. 5, 4689–4696.","ama":"Cano Cordoba F. Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants. In: Proceedings of the 18th International Conference on Agents and Artificial Intelligence. Vol 5. Science and Technology Publications; 2026:4689-4696. doi:10.5220/0014483200004052","apa":"Cano Cordoba, F. (2026). Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants. In Proceedings of the 18th International Conference on Agents and Artificial Intelligence (Vol. 5, pp. 4689–4696). Marbella, Spain: Science and Technology Publications. https://doi.org/10.5220/0014483200004052"},"title":"Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants","author":[{"orcid":"0000-0002-0783-904X","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","full_name":"Cano Cordoba, Filip","first_name":"Filip","last_name":"Cano Cordoba"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","conference":{"location":"Marbella, Spain","end_date":"2026-03-08","start_date":"2026-03-05","name":"ICAART: International Conference on Agents and Artificial Intelligence"},"article_processing_charge":"No","volume":5,"publication":"Proceedings of the 18th International Conference on Agents and Artificial Intelligence","date_updated":"2026-06-24T08:37:00Z","oa_version":"Accepted Version","das_tickbox":"0","OA_place":"repository","researchdata_availability":"no"},{"author":[{"orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"title":"Bidding Games","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"book_chapter","article_processing_charge":"No","editor":[{"last_name":"Fijalkow","first_name":" Nathanaël","full_name":"Fijalkow, Nathanaël"}],"publication":"Games on Graphs. From Logic and Automata to Algorithms","oa_version":"None","das_tickbox":"1","date_updated":"2026-07-13T13:32:47Z","doi":"10.1017/9781009500678.022","quality_controlled":"1","page":"529-569","day":"26","citation":{"ieee":"G. Avni and T. A. Henzinger, “Bidding Games,” in Games on Graphs. From Logic and Automata to Algorithms, Nathanaël Fijalkow, Ed. Cambridge University Press, 2026, pp. 529–569.","mla":"Avni, Guy, and Thomas A. Henzinger. “Bidding Games.” Games on Graphs. From Logic and Automata to Algorithms, edited by Nathanaël Fijalkow, Cambridge University Press, 2026, pp. 529–69, doi:10.1017/9781009500678.022.","short":"G. Avni, T.A. Henzinger, in:, Nathanaël Fijalkow (Ed.), Games on Graphs. From Logic and Automata to Algorithms, Cambridge University Press, 2026, pp. 529–569.","chicago":"Avni, Guy, and Thomas A Henzinger. “Bidding Games.” In Games on Graphs. From Logic and Automata to Algorithms, edited by Nathanaël Fijalkow, 529–69. Cambridge University Press, 2026. https://doi.org/10.1017/9781009500678.022.","ista":"Avni G, Henzinger TA. 2026.Bidding Games. In: Games on Graphs. From Logic and Automata to Algorithms. , 529–569.","ama":"Avni G, Henzinger TA. Bidding Games. In: Fijalkow Nathanaël, ed. Games on Graphs. From Logic and Automata to Algorithms. Cambridge University Press; 2026:529-569. doi:10.1017/9781009500678.022","apa":"Avni, G., & Henzinger, T. A. (2026). Bidding Games. In Nathanaël Fijalkow (Ed.), Games on Graphs. From Logic and Automata to Algorithms (pp. 529–569). Cambridge University Press. https://doi.org/10.1017/9781009500678.022"},"publication_identifier":{"isbn":["9781009500685"],"eisbn":["9781009500678"]},"year":"2026","abstract":[{"text":"As seen in previous chapters, a graph game proceeds by placing a token on one of the vertices and allowing the players to move it throughout the graph to produce an infinite trace, which determines the winner or payoff of the game.","lang":"eng"}],"OA_type":"closed access","date_created":"2026-07-13T10:44:22Z","publisher":"Cambridge University Press","publication_status":"published","_id":"22300","month":"04","fulldoi":"https://doi.org/10.1017/9781009500678.022","status":"public","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"scopus_import":"1","corr_author":"1","date_published":"2026-04-26T00:00:00Z"},{"conference":{"name":"ICAART: International Conference on Agents and Artificial Intelligence","start_date":"2026-03-05","end_date":"2026-03-08","location":"Marbella, Spain"},"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Machine unlearning using forgetting neural networks","author":[{"full_name":"Hatua, Amartya","last_name":"Hatua","first_name":"Amartya"},{"last_name":"Nguyen","first_name":"Trung","full_name":"Nguyen, Trung"},{"full_name":"Cano Cordoba, Filip","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","last_name":"Cano Cordoba","first_name":"Filip","orcid":"0000-0002-0783-904X"},{"full_name":"Sung, Andrew","first_name":"Andrew","last_name":"Sung"}],"article_processing_charge":"No","publication":"Proceedings of the 18th International Conference on Agents and Artificial Intelligence","volume":2,"oa_version":"Preprint","date_updated":"2026-07-16T09:02:53Z","das_tickbox":"1","OA_place":"repository","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2410.22374"}],"doi":"10.5220/0014326500004052","keyword":["Machine Unlearning","Neuroscience-Inspired Machine Learning","Membership Inference Attacks"],"quality_controlled":"1","oa":1,"intvolume":" 2","page":"1536-1546","day":"30","citation":{"ama":"Hatua A, Nguyen T, Cano Cordoba F, Sung A. Machine unlearning using forgetting neural networks. In: Proceedings of the 18th International Conference on Agents and Artificial Intelligence. Vol 2. SciTePress; 2026:1536-1546. doi:10.5220/0014326500004052","apa":"Hatua, A., Nguyen, T., Cano Cordoba, F., & Sung, A. (2026). Machine unlearning using forgetting neural networks. In Proceedings of the 18th International Conference on Agents and Artificial Intelligence (Vol. 2, pp. 1536–1546). Marbella, Spain: SciTePress. https://doi.org/10.5220/0014326500004052","ista":"Hatua A, Nguyen T, Cano Cordoba F, Sung A. 2026. Machine unlearning using forgetting neural networks. Proceedings of the 18th International Conference on Agents and Artificial Intelligence. ICAART: International Conference on Agents and Artificial Intelligence vol. 2, 1536–1546.","mla":"Hatua, Amartya, et al. “Machine Unlearning Using Forgetting Neural Networks.” Proceedings of the 18th International Conference on Agents and Artificial Intelligence, vol. 2, SciTePress, 2026, pp. 1536–46, doi:10.5220/0014326500004052.","chicago":"Hatua, Amartya, Trung Nguyen, Filip Cano Cordoba, and Andrew Sung. “Machine Unlearning Using Forgetting Neural Networks.” In Proceedings of the 18th International Conference on Agents and Artificial Intelligence, 2:1536–46. SciTePress, 2026. https://doi.org/10.5220/0014326500004052.","short":"A. Hatua, T. Nguyen, F. Cano Cordoba, A. Sung, in:, Proceedings of the 18th International Conference on Agents and Artificial Intelligence, SciTePress, 2026, pp. 1536–1546.","ieee":"A. Hatua, T. Nguyen, F. Cano Cordoba, and A. Sung, “Machine unlearning using forgetting neural networks,” in Proceedings of the 18th International Conference on Agents and Artificial Intelligence, Marbella, Spain, 2026, vol. 2, pp. 1536–1546."},"publication_identifier":{"eissn":["2184-433X"],"isbn":["9789897587962"]},"year":"2026","date_created":"2026-07-13T09:46:46Z","OA_type":"green","abstract":[{"text":"Modern computer systems store vast amounts of personal data, enabling advances in AI and ML but risking user privacy and trust. For privacy reasons, it is sometimes desired for an ML model to forget part of the data it was trained on. In this paper, we introduce a novel unlearning approach based on Forgetting Neural Networks (FNNs), a neuroscience-inspired architecture that explicitly encodes forgetting through multiplicative decay factors. While FNNs had previously been studied as a theoretical construct, we provide the first concrete implementation and demonstrate their effectiveness for targeted unlearning. We propose several variants with per-neuron forgetting factors, including rank-based assignments guided by activation levels, and evaluate them on MNIST and Fashion-MNIST benchmarks. Our method systematically removes information associated with forget sets while preserving performance on retained data. Membership inference attacks confirm the effectiveness of FNN-based unlearning in erasing information about the training data from the neural network. These results establish FNNs as a promising foundation for efficient and interpretable unlearning. ","lang":"eng"}],"external_id":{"arxiv":["2410.22374"]},"publisher":"SciTePress","publication_status":"published","_id":"22294","month":"06","arxiv":1,"fulldoi":"https://doi.org/10.5220/0014326500004052","status":"public","language":[{"iso":"eng"}],"scopus_import":"1","department":[{"_id":"ToHe"}],"date_published":"2026-06-30T00:00:00Z"},{"citation":{"mla":"Cano Cordoba, Filip, et al. “Energy Shields for Fairness.” Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency, Association for Computing Machinery, 2026, pp. 4243–75, doi:10.1145/3805689.3806807.","chicago":"Cano Cordoba, Filip, Thomas A Henzinger, and Konstantin Kueffner. “Energy Shields for Fairness.” In Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency, 4243–75. Association for Computing Machinery, 2026. https://doi.org/10.1145/3805689.3806807.","short":"F. Cano Cordoba, T.A. Henzinger, K. Kueffner, in:, Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency, Association for Computing Machinery, 2026, pp. 4243–4275.","ieee":"F. Cano Cordoba, T. A. Henzinger, and K. Kueffner, “Energy shields for fairness,” in Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency, Montreal, Canada, 2026, pp. 4243–4275.","ama":"Cano Cordoba F, Henzinger TA, Kueffner K. Energy shields for fairness. In: Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency. Association for Computing Machinery; 2026:4243-4275. doi:10.1145/3805689.3806807","apa":"Cano Cordoba, F., Henzinger, T. A., & Kueffner, K. (2026). Energy shields for fairness. In Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency (pp. 4243–4275). Montreal, Canada: Association for Computing Machinery. https://doi.org/10.1145/3805689.3806807","ista":"Cano Cordoba F, Henzinger TA, Kueffner K. 2026. Energy shields for fairness. Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency. FAccT: Conference on Fairness, Accountability and Transparency, 4243–4275."},"day":"01","page":"4243 - 4275","oa":1,"quality_controlled":"1","doi":"10.1145/3805689.3806807","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"researchdata_availability":"no","file_date_updated":"2026-07-16T09:23:15Z","OA_place":"publisher","oa_version":"Published Version","date_updated":"2026-07-22T06:15:56Z","das_tickbox":"0","publication":"Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency","ddc":["000"],"article_processing_charge":"Yes","title":"Energy shields for fairness","author":[{"last_name":"Cano Cordoba","first_name":"Filip","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","full_name":"Cano Cordoba, Filip","orcid":"0000-0002-0783-904X"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","full_name":"Kueffner, Konstantin","last_name":"Kueffner","first_name":"Konstantin","orcid":"0000-0001-8974-2542"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2026-06-28","location":"Montreal, Canada","name":"FAccT: Conference on Fairness, Accountability and Transparency","start_date":"2026-06-25"},"type":"conference","date_published":"2026-07-01T00:00:00Z","acknowledgement":"This work has been supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","corr_author":"1","scopus_import":"1","department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"status":"public","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"fulldoi":"https://doi.org/10.1145/3805689.3806807","arxiv":1,"supplementarymaterial":"yes","month":"07","_id":"22321","publication_status":"published","has_accepted_license":"1","file":[{"relation":"main_file","checksum":"21e648ea3b529f0df7545ad4b31b0ef4","file_size":3129128,"content_type":"application/pdf","date_updated":"2026-07-16T09:23:15Z","date_created":"2026-07-16T09:23:15Z","success":1,"creator":"dernst","file_id":"22348","access_level":"open_access","file_name":"2026_ACMFACCT_Cano.pdf"}],"publisher":"Association for Computing Machinery","external_id":{"arxiv":["2605.24926"]},"abstract":[{"lang":"eng","text":"Runtime fairness is not a one-time constraint but a dynamic property evaluated over a sequence of decisions. To ensure fairness at runtime, it is necessary to account for past decisions, information neglected by conventional, static classifiers. Traditional fairness shields enforce runtime fairness abruptly, by intervening deterministically whenever a sequence of decisions violates the target for a running fairness measure. This motivates our main conceptual contribution: energy shields. An energy shield is a novel, lightweight, adaptive controller that monitors a sequence of decisions and intervenes probabilistically to ensure runtime fairness smoothly, by utilizing physics-inspired energy functions to nudge the sequence toward fairness: the more unfair the decisions, the stronger the nudging force becomes. This makes energy shields the first fairness shields to provide both short-term safety and long-term liveness guarantees. Safety ensures that the running fairness measure stays within a running target interval with high probability, and liveness ensures that the limit of the fairness measure lies within the limit target interval. Intuitively, the short-term specifies the tolerated fairness values and the long-term specifies the desired fairness values. We also provide a synthesis procedure for constructing the least intrusive energy shield for a given target specification, and demonstrate its efficiency experimentally. We evaluate our energy shields against existing fairness shields through the lens of short- and long-term fairness."}],"date_created":"2026-07-14T05:32:45Z","OA_type":"gold","year":"2026"},{"intvolume":" 380","oa":1,"quality_controlled":"1","keyword":["Concurrent games","Shared randomness","Topology","Algebraic Geometry"],"doi":"10.4230/LIPIcs.LICS.2026.23","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"citation":{"mla":"Brice, Leonard J., et al. “Dicey Games: Shared Sources of Randomness in Distributed Systems.” 41st Annual Symposium on Logic in Computer Science, vol. 380, 23:1-23:26, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:10.4230/LIPIcs.LICS.2026.23.","chicago":"Brice, Leonard J, Thomas A Henzinger, and K. S. Thejaswini. “Dicey Games: Shared Sources of Randomness in Distributed Systems.” In 41st Annual Symposium on Logic in Computer Science, Vol. 380. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.LICS.2026.23.","short":"L.J. Brice, T.A. Henzinger, K.S. Thejaswini, in:, 41st Annual Symposium on Logic in Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","ieee":"L. J. Brice, T. A. Henzinger, and K. S. Thejaswini, “Dicey games: Shared sources of randomness in distributed systems,” in 41st Annual Symposium on Logic in Computer Science, Lisbon, Portugal, 2026, vol. 380.","ama":"Brice LJ, Henzinger TA, Thejaswini KS. Dicey games: Shared sources of randomness in distributed systems. In: 41st Annual Symposium on Logic in Computer Science. Vol 380. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:10.4230/LIPIcs.LICS.2026.23","apa":"Brice, L. J., Henzinger, T. A., & Thejaswini, K. S. (2026). Dicey games: Shared sources of randomness in distributed systems. In 41st Annual Symposium on Logic in Computer Science (Vol. 380). Lisbon, Portugal: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.LICS.2026.23","ista":"Brice LJ, Henzinger TA, Thejaswini KS. 2026. Dicey games: Shared sources of randomness in distributed systems. 41st Annual Symposium on Logic in Computer Science. LICS: Logic in Computer Science, LIPIcs, vol. 380, 23:1-23:26."},"day":"09","volume":380,"publication":"41st Annual Symposium on Logic in Computer Science","ddc":["000"],"article_processing_charge":"No","title":"Dicey games: Shared sources of randomness in distributed systems","author":[{"full_name":"Brice, Leonard J","id":"ce3b3409-db6c-11f0-aa64-ad678f7fd937","first_name":"Leonard J","last_name":"Brice"},{"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":"Thejaswini, K. S.","last_name":"Thejaswini","first_name":"K. S."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","conference":{"end_date":"2026-07-23","location":"Lisbon, Portugal","name":"LICS: Logic in Computer Science","start_date":"2026-07-20"},"researchdata_availability":"no","file_date_updated":"2026-08-03T07:02:30Z","OA_place":"publisher","alternative_title":["LIPIcs"],"date_updated":"2026-08-03T07:03:28Z","oa_version":"Published Version","das_tickbox":"0","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"fulldoi":"https://doi.org/10.4230/LIPIcs.LICS.2026.23","arxiv":1,"supplementarymaterial":"no","date_published":"2026-07-09T00:00:00Z","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS).\r\nLéonard Brice: Part of this work was realised when this author was an FNRS aspirant at Université libre de Bruxelles.\r\nK. S. Thejaswini: Part of this work was realised when this author was a post-doctoral researcher at IST Austria.\r\nAcknowledgements We thank all our colleagues who took the time to hear our puzzle and wasted several hours of their research time in pursuit of the optimal bounds for the 3-player matching.\r\npennies problem.\r\n","article_number":"23:1-23:26","scopus_import":"1","department":[{"_id":"ToHe"}],"corr_author":"1","language":[{"iso":"eng"}],"status":"public","abstract":[{"text":"Consider a 4-player version of Matching Pennies where a team of three players competes against the Devil. Each player simultaneously says \"Heads\" or \"Tails\". The team wins if all four choices match; otherwise the Devil wins. If all team players randomise independently, they win with probability 1/8; if all players share a common source of randomness, they win with probability 1/2. What happens when each pair of team players shares a source of randomness? Can the team do better than win with probability 1/4? The surprising (and nontrivial) answer is yes!\r\nWe introduce Dicey Games, a formal framework motivated by the study of distributed systems with shared sources of randomness (of which the above example is a specific instance). We characterise the existence, representation and computational complexity of optimal strategies in Dicey Games, and we study the problem of allocating limited sources of randomness optimally within a team.","lang":"eng"}],"OA_type":"gold","date_created":"2026-08-02T22:01:52Z","year":"2026","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959774345"]},"month":"07","_id":"22617","publication_status":"published","has_accepted_license":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"access_level":"open_access","file_id":"22625","file_name":"2026_LIPICSLICS_Brice.pdf","success":1,"date_created":"2026-08-03T07:02:30Z","creator":"dernst","content_type":"application/pdf","date_updated":"2026-08-03T07:02:30Z","relation":"main_file","file_size":919708,"checksum":"5d0ff4d267565188a8b4c7502e1bd243"}],"external_id":{"arxiv":["2601.18303"]}},{"year":"2026","abstract":[{"text":"It is known that for a uniform morphic sequence 𝒖 =⟨𝑢𝑛⟩∞\r\n𝑛=0 and an algebraic number 𝛽 such that |𝛽| >1, the number [[𝒖]]𝛽 :=∑∞\r\n𝑛=0(𝑢𝑛/𝛽𝑛) either lies in ℚ(𝛽) or is transcendental. In this paper, we show a similar rational–transcendental dichotomy for sequences defined by irreducible Pisot morphisms on binary alphabets. Subject to the Pisot conjecture (an irreducible Pisot morphism has pure discrete spectrum), we generalise the latter result to arbitrary finite alphabets. In certain cases, we are able to show transcendence of [[𝒖]]𝛽 outright. In particular, for 𝑘 ≥2, if 𝒖 is the k-Bonacci word, then [[𝒖]]𝛽 is transcendental.","lang":"eng"}],"OA_type":"hybrid","date_created":"2026-07-27T05:53:25Z","publication_identifier":{"eissn":["1469-4417"],"issn":["0143-3857"]},"month":"07","_id":"22406","publisher":"Cambridge University Press","external_id":{"arxiv":["2405.05279"]},"publication_status":"epub_ahead","has_accepted_license":"1","fulldoi":"https://doi.org/10.1017/etds.2026.10324","PlanS_conform":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"arxiv":1,"supplementarymaterial":"no","scopus_import":"1","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"date_published":"2026-07-10T00:00:00Z","acknowledgement":"We thank the anonymous referee for identifying an error in an earlier\r\nversion of the paper. We gratefully acknowledge support from UKRI Frontier Research\r\nGrant EP/X033813/1, ERC grant DynAMiCS (101167561) and DFG grant 389792660 as\r\npart of TRR 248. J.O. is also affiliated with Keble College, Oxford as an Emmy Network\r\nfellow.","status":"public","language":[{"iso":"eng"}],"ddc":["000"],"publication":"Ergodic Theory and Dynamical Systems","title":"Transcendence for Pisot morphic words over an algebraic base","author":[{"id":"2e0132b3-4e98-11ef-b275-cf7281c2802a","full_name":"Kebis, Pavol","first_name":"Pavol","last_name":"Kebis"},{"last_name":"LUCA","first_name":"FLORIAN","full_name":"LUCA, FLORIAN"},{"last_name":"OUAKNINE","first_name":"JOEL","full_name":"OUAKNINE, JOEL"},{"first_name":"ANDREW","last_name":"SCOONES","full_name":"SCOONES, ANDREW"},{"full_name":"WORRELL, JAMES","last_name":"WORRELL","first_name":"JAMES"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","article_processing_charge":"Yes (in subscription journal)","OA_place":"publisher","researchdata_availability":"no","mathsc":["11J81","37B10","11J87"],"das_tickbox":"0","date_updated":"2026-08-03T06:17:50Z","oa_version":"Published Version","quality_controlled":"1","oa":1,"main_file_link":[{"url":"https://doi.org/10.1017/etds.2026.10324","open_access":"1"}],"keyword":["balanced-pair algorithm","Cobham’s conjecture","k-Bonacci words","Pisot conjecture","subspace theorem"],"doi":"10.1017/etds.2026.10324","citation":{"ama":"Kebis P, LUCA F, OUAKNINE J, SCOONES A, WORRELL J. Transcendence for Pisot morphic words over an algebraic base. Ergodic Theory and Dynamical Systems. 2026:1-22. doi:10.1017/etds.2026.10324","apa":"Kebis, P., LUCA, F., OUAKNINE, J., SCOONES, A., & WORRELL, J. (2026). Transcendence for Pisot morphic words over an algebraic base. Ergodic Theory and Dynamical Systems. Cambridge University Press. https://doi.org/10.1017/etds.2026.10324","ista":"Kebis P, LUCA F, OUAKNINE J, SCOONES A, WORRELL J. 2026. Transcendence for Pisot morphic words over an algebraic base. Ergodic Theory and Dynamical Systems., 1–22.","mla":"Kebis, Pavol, et al. “Transcendence for Pisot Morphic Words over an Algebraic Base.” Ergodic Theory and Dynamical Systems, Cambridge University Press, 2026, pp. 1–22, doi:10.1017/etds.2026.10324.","short":"P. Kebis, F. LUCA, J. OUAKNINE, A. SCOONES, J. WORRELL, Ergodic Theory and Dynamical Systems (2026) 1–22.","chicago":"Kebis, Pavol, FLORIAN LUCA, JOEL OUAKNINE, ANDREW SCOONES, and JAMES WORRELL. “Transcendence for Pisot Morphic Words over an Algebraic Base.” Ergodic Theory and Dynamical Systems. Cambridge University Press, 2026. https://doi.org/10.1017/etds.2026.10324.","ieee":"P. Kebis, F. LUCA, J. OUAKNINE, A. SCOONES, and J. WORRELL, “Transcendence for Pisot morphic words over an algebraic base,” Ergodic Theory and Dynamical Systems. Cambridge University Press, pp. 1–22, 2026."},"article_type":"original","page":"1-22","day":"10"},{"month":"07","_id":"22717","publication_status":"published","has_accepted_license":"1","publisher":"Springer Nature","file":[{"file_id":"22724","access_level":"open_access","file_name":"2026_LNCS_Brice.pdf","success":1,"date_created":"2026-08-18T06:53:22Z","creator":"dernst","content_type":"application/pdf","date_updated":"2026-08-18T06:53:22Z","relation":"main_file","file_size":1902192,"checksum":"10ded8a3ab9ed34c9e4794c0b277622c"}],"external_id":{"arxiv":["2603.07094"]},"abstract":[{"lang":"eng","text":"We study concurrent graph games where n players cooperate against an opponent to reach a set of target states. Unlike traditional settings, we study distributed randomisation: team players do not share a source of randomness, and their private random sources are hidden from the opponent and from each other.\r\n\r\nWe show that memoryless strategies are sufficient for the threshold problem (deciding whether there is a strategy for the team that ensures winning with probability that exceeds a threshold), a result that not only places the problem in the Existential Theory of the Reals (ER) but also enables the construction of value iteration algorithms. We additionally show that the threshold problem is NP-hard. For the almost-sure reachability problem, we prove NP-completeness.\r\n\r\nWe introduce Individually Randomised Alternating-time Temporal Logic (IRATL). This logic extends the standard ATL framework to reason about probability thresholds, with semantics explicitly designed for coalitions that lack a shared source of randomness. On the practical side, we implement and evaluate a solver for the threshold and almost-sure problem based on the algorithms that we develop."}],"OA_type":"hybrid","date_created":"2026-08-16T22:01:44Z","year":"2026","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783032325181"]},"date_published":"2026-07-24T00:00:00Z","acknowledgement":"This work is a part of project VAMOS that has received funding from the European Research Council (ERC), grant agreement No 101020093. Part of this work was realised when the first author was an FNRS aspirant at Université libre de Bruxelles.","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"scopus_import":"1","language":[{"iso":"eng"}],"status":"public","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"fulldoi":"https://doi.org/10.1007/978-3-032-32519-8_12","arxiv":1,"supplementarymaterial":"no","researchdata_availability":"yes","file_date_updated":"2026-08-18T06:53:22Z","OA_place":"publisher","oa_version":"Published Version","das_tickbox":"1","date_updated":"2026-08-18T06:55:38Z","volume":16682,"publication":"38th International Conference on Computer Aided Verification","ddc":["000"],"article_processing_charge":"Yes (in subscription journal)","title":"Randomise alone, reach as a team","author":[{"last_name":"Brice","first_name":"Leonard J","full_name":"Brice, Leonard J","id":"ce3b3409-db6c-11f0-aa64-ad678f7fd937"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Montaseri, Alipasha","id":"709a7f96-8896-11f0-9809-d75612fc0f2e","last_name":"Montaseri","first_name":"Alipasha"},{"id":"2783031a-7378-11f0-b2d0-f17f1db2ebad","full_name":"Shafiee, Ali","first_name":"Ali","last_name":"Shafiee"},{"full_name":"Thejaswini, K. S.","first_name":"K. S.","last_name":"Thejaswini"}],"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2026-07-29","location":"Lisbon, Portugal","name":"CAV: Computer Aided Verification","start_date":"2026-07-26"},"citation":{"apa":"Brice, L. J., Henzinger, T. A., Montaseri, A., Shafiee, A., & Thejaswini, K. S. (2026). Randomise alone, reach as a team. In 38th International Conference on Computer Aided Verification (Vol. 16682, pp. 215–236). Lisbon, Portugal: Springer Nature. https://doi.org/10.1007/978-3-032-32519-8_12","ama":"Brice LJ, Henzinger TA, Montaseri A, Shafiee A, Thejaswini KS. Randomise alone, reach as a team. In: 38th International Conference on Computer Aided Verification. Vol 16682. Springer Nature; 2026:215-236. doi:10.1007/978-3-032-32519-8_12","ista":"Brice LJ, Henzinger TA, Montaseri A, Shafiee A, Thejaswini KS. 2026. Randomise alone, reach as a team. 38th International Conference on Computer Aided Verification. CAV: Computer Aided Verification vol. 16682, 215–236.","short":"L.J. Brice, T.A. Henzinger, A. Montaseri, A. Shafiee, K.S. Thejaswini, in:, 38th International Conference on Computer Aided Verification, Springer Nature, 2026, pp. 215–236.","chicago":"Brice, Leonard J, Thomas A Henzinger, Alipasha Montaseri, Ali Shafiee, and K. S. Thejaswini. “Randomise Alone, Reach as a Team.” In 38th International Conference on Computer Aided Verification, 16682:215–36. Springer Nature, 2026. https://doi.org/10.1007/978-3-032-32519-8_12.","mla":"Brice, Leonard J., et al. “Randomise Alone, Reach as a Team.” 38th International Conference on Computer Aided Verification, vol. 16682, Springer Nature, 2026, pp. 215–36, doi:10.1007/978-3-032-32519-8_12.","ieee":"L. J. Brice, T. A. Henzinger, A. Montaseri, A. Shafiee, and K. S. Thejaswini, “Randomise alone, reach as a team,” in 38th International Conference on Computer Aided Verification, Lisbon, Portugal, 2026, vol. 16682, pp. 215–236."},"day":"24","page":"215-236","intvolume":" 16682","oa":1,"dataavailabilitystatement":"The artifact can be accessed at the link: https://doi. org/10.5281/zenodo.19680359.\r\nThe source code is available at:https://github.com/alipashamontaseri/Team-Concurrent-Game.","quality_controlled":"1","doi":"10.1007/978-3-032-32519-8_12","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}]},{"acknowledgement":"This work is funded by the following grants: European Research Council under Grant No.: ERC-2020-AdG 101020093, ISF grant no. 1679/21, grant RYC2024-049116, MICIU/AEI/10.13039/501100011033, the ESF+, and Volkswagen Foundation within its Momentum framework under project no. 9C283.","date_published":"2026-07-24T00:00:00Z","scopus_import":"1","department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"status":"public","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"fulldoi":"https://doi.org/10.1007/978-3-032-32519-8_13","supplementarymaterial":"no","arxiv":1,"_id":"22719","month":"07","has_accepted_license":"1","publication_status":"published","external_id":{"arxiv":["2605.13185"]},"file":[{"relation":"main_file","checksum":"f17ba3f82854fdb4eb69fd922965661a","file_size":531980,"content_type":"application/pdf","date_updated":"2026-08-18T08:40:07Z","date_created":"2026-08-18T08:40:07Z","success":1,"creator":"dernst","access_level":"open_access","file_id":"22730","file_name":"2026_LNCS_Avni.pdf"}],"publisher":"Springer Nature","date_created":"2026-08-16T22:01:44Z","OA_type":"hybrid","abstract":[{"text":"We study the problem of generating paths on a graph that satisfy a collection of w-regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler—oblivious to the graph and objective—dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions—simple, a priori restrictions agreed upon before the graph or objectives are revealed—that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of w-regular objectives. In particular, Büchi objectives admit universal composition of finite-memory policies without scheduler communication; co-Büchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.","lang":"eng"}],"year":"2026","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783032325181"]},"citation":{"ista":"Avni G, Henzinger TA, Mallik K, Sadhukhan S, Thejaswini KS. 2026. Decoupled planning for multiple omega-regular objectives. 38th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 16682, 237–257.","apa":"Avni, G., Henzinger, T. A., Mallik, K., Sadhukhan, S., & Thejaswini, K. S. (2026). Decoupled planning for multiple omega-regular objectives. In 38th International Conference on Computer Aided Verification (Vol. 16682, pp. 237–257). Lisbon, Portugal: Springer Nature. https://doi.org/10.1007/978-3-032-32519-8_13","ama":"Avni G, Henzinger TA, Mallik K, Sadhukhan S, Thejaswini KS. Decoupled planning for multiple omega-regular objectives. In: 38th International Conference on Computer Aided Verification. Vol 16682. Springer Nature; 2026:237-257. doi:10.1007/978-3-032-32519-8_13","ieee":"G. Avni, T. A. Henzinger, K. Mallik, S. Sadhukhan, and K. S. Thejaswini, “Decoupled planning for multiple omega-regular objectives,” in 38th International Conference on Computer Aided Verification, Lisbon, Portugal, 2026, vol. 16682, pp. 237–257.","short":"G. Avni, T.A. Henzinger, K. Mallik, S. Sadhukhan, K.S. Thejaswini, in:, 38th International Conference on Computer Aided Verification, Springer Nature, 2026, pp. 237–257.","chicago":"Avni, Guy, Thomas A Henzinger, Kaushik Mallik, Suman Sadhukhan, and K. S. Thejaswini. “Decoupled Planning for Multiple Omega-Regular Objectives.” In 38th International Conference on Computer Aided Verification, 16682:237–57. Springer Nature, 2026. https://doi.org/10.1007/978-3-032-32519-8_13.","mla":"Avni, Guy, et al. “Decoupled Planning for Multiple Omega-Regular Objectives.” 38th International Conference on Computer Aided Verification, vol. 16682, Springer Nature, 2026, pp. 237–57, doi:10.1007/978-3-032-32519-8_13."},"day":"24","page":"237-257","oa":1,"intvolume":" 16682","quality_controlled":"1","doi":"10.1007/978-3-032-32519-8_13","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"researchdata_availability":"no","OA_place":"publisher","file_date_updated":"2026-08-18T08:40:07Z","das_tickbox":"0","oa_version":"Published Version","date_updated":"2026-08-18T08:41:44Z","alternative_title":["LNCS"],"publication":"38th International Conference on Computer Aided Verification","volume":16682,"ddc":["000"],"article_processing_charge":"Yes (in subscription journal)","conference":{"location":"Lisbon, Portugal","end_date":"2026-07-29","start_date":"2026-07-26","name":"CAV: Computer Aided Verification"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","title":"Decoupled planning for multiple omega-regular objectives","author":[{"first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"orcid":"0000-0001-9864-7475","last_name":"Mallik","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik"},{"full_name":"Sadhukhan, Suman","last_name":"Sadhukhan","first_name":"Suman"},{"last_name":"Thejaswini","first_name":"K. S.","full_name":"Thejaswini, K. S."}]},{"fulldoi":"https://doi.org/10.1007/978-3-032-32526-6_20","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"supplementarymaterial":"no","arxiv":1,"scopus_import":"1","department":[{"_id":"ToHe"}],"acknowledgement":"This work was supported by the European Research Council (ERC) Grants VAMOS (No. 101020093) and HYPER (No. 101055412).","date_published":"2026-01-01T00:00:00Z","status":"public","language":[{"iso":"eng"}],"year":"2026","OA_type":"hybrid","date_created":"2026-08-23T22:01:47Z","abstract":[{"text":"Quantitative automata (QAs) extend finite-state automata on infinite words with weighted transitions to specify quantitative system properties. However, their finite weight sets rule out properties like average response time, where response times can be arbitrarily large. Nested quantitative automata (NQAs) overcome this limitation: a parent automaton spawns child automata to compute unbounded values over finite infixes and aggregates them into a final result. Despite this expressiveness, NQAs have lacked practical tool support to date.\r\n\r\nWe close this gap by extending the Quantitative Automata Kit (QuAK), a software tool for QA analysis, to support NQAs. Our core contribution is implementing a suite of flattening procedures that reduce NQAs to QAs, leveraging QuAK’s existing decision procedures. These reductions preserve the answers to threshold decision problems, while allowing users to specify properties in the more expressive NQA formalism. The tool handles all combinations of parent aggregators (including limits and averages) and child functions (extrema and monotonic or bounded summations) for which emptiness and universality are known to be decidable. Experiments on response-time and resource-consumption benchmarks demonstrate QuAK’s effectiveness.","lang":"eng"}],"publication_identifier":{"isbn":["9783032325259"],"eissn":["1611-3349"],"issn":["0302-9743"]},"month":"01","_id":"22754","external_id":{"arxiv":["2605.12418"]},"publisher":"Springer Nature","file":[{"date_updated":"2026-09-09T06:33:55Z","content_type":"application/pdf","file_size":425988,"checksum":"043ba7b83f28d036d5a0e6e70a52cc9a","relation":"main_file","file_name":"2026_LNCS_HenzingerT.pdf","access_level":"open_access","file_id":"22861","creator":"dernst","success":1,"date_created":"2026-09-09T06:33:55Z"}],"has_accepted_license":"1","publication_status":"published","dataavailabilitystatement":"The artifact supporting the experimental results in this paper is available in the QuAK repository at https://github.com/ista-vamos/nested-quak. It contains the extended QuAK implementation, benchmark generators, example inputs, and scripts/logs for reproducing the reported tables. The artifact is intended to reproduce the experiments under the setup described in Sect. 4; runtimes may vary across machines, and the reported timeout and memory-exhaustion results depend on the stated hardware limits. No sensitive or restricted data are used. An archived version is available on Zenodo at DOI: http://doi.org/10.5281/zenodo.19844606.","quality_controlled":"1","oa":1,"intvolume":" 16683","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"doi":"10.1007/978-3-032-32526-6_20","citation":{"apa":"Henzinger, T. A., Mazzocchi, N. A., Sarac, N. E., & Yılmaz, H. (2026). Extending QuAK with nested quantitative automata. In 38th International Conference on Computer Aided Verification (Vol. 16683, pp. 418–432). Lisbon, Portugal: Springer Nature. https://doi.org/10.1007/978-3-032-32526-6_20","ama":"Henzinger TA, Mazzocchi NA, Sarac NE, Yılmaz H. Extending QuAK with nested quantitative automata. In: 38th International Conference on Computer Aided Verification. Vol 16683. Springer Nature; 2026:418-432. doi:10.1007/978-3-032-32526-6_20","ista":"Henzinger TA, Mazzocchi NA, Sarac NE, Yılmaz H. 2026. Extending QuAK with nested quantitative automata. 38th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 16683, 418–432.","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, Naci E Sarac, and Harun Yılmaz. “Extending QuAK with Nested Quantitative Automata.” In 38th International Conference on Computer Aided Verification, 16683:418–32. Springer Nature, 2026. https://doi.org/10.1007/978-3-032-32526-6_20.","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, H. Yılmaz, in:, 38th International Conference on Computer Aided Verification, Springer Nature, 2026, pp. 418–432.","mla":"Henzinger, Thomas A., et al. “Extending QuAK with Nested Quantitative Automata.” 38th International Conference on Computer Aided Verification, vol. 16683, Springer Nature, 2026, pp. 418–32, doi:10.1007/978-3-032-32526-6_20.","ieee":"T. A. Henzinger, N. A. Mazzocchi, N. E. Sarac, and H. Yılmaz, “Extending QuAK with nested quantitative automata,” in 38th International Conference on Computer Aided Verification, Lisbon, Portugal, 2026, vol. 16683, pp. 418–432."},"page":"418-432","day":"01","ddc":["000"],"publication":"38th International Conference on Computer Aided Verification","volume":16683,"conference":{"location":"Lisbon, Portugal","end_date":"2026-07-29","start_date":"2026-07-26","name":"CAV: Computer Aided Verification"},"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Extending QuAK with nested quantitative automata","author":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","last_name":"Mazzocchi"},{"first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"},{"first_name":"Harun","last_name":"Yılmaz","full_name":"Yılmaz, Harun"}],"article_processing_charge":"No","OA_place":"publisher","file_date_updated":"2026-09-09T06:33:55Z","researchdata_availability":"yes","date_updated":"2026-09-09T06:37:41Z","alternative_title":["LNCS"],"das_tickbox":"1","oa_version":"Published Version"},{"publication_identifier":{"isbn":["9783959774475"],"eissn":["1868-8969"]},"year":"2026","abstract":[{"text":"Two-player games on graphs are a classical framework for analyzing strategic decision making. In turn-based games, two players move a token along the edges of the graph, and the right to move the token is determined by the current vertex. In traditional bidding games - referred to as pure bidding games - the right to move the token is determined at each step through bidding; here we consider Richman bidding, where the winning player of a bid pays the losing player. The winner is decided based on a temporal or quantitative specification evaluated over the resulting infinite play.\r\nIn this work, we combine turn-based games and pure bidding games into generalized bidding games, with player-1 vertices, player-2 vertices, and bidding vertices. This natural and simple generalization of bidding games has far-reaching consequences. First, we show that, as a model, generalized bidding games are more expressive than pure bidding games, and we provide several applications. Second, and most importantly, we show that generalized Richman bidding games are structurally equivalent to simple stochastic games, a well-studied model: they are linearly interreducible to each other. As was previously known, the special case of pure Richman bidding games corresponds to random-turn games. In other words, generalized bidding games extend pure bidding games in the same way that simple stochastic games extend random-turn games. We use this connection to solve generalized Richman bidding games for temporal (parity) and quantitative (mean-payoff and discounted-sum) specifications. From a computational perspective, we establish that generalized bidding games with parity and mean-payoff specifications retain the best known upper bounds for turn-based games and pure bidding games, namely NP∩coNP.\r\nFinally, we study a repair problem that asks whether bidding vertices can be assigned \"owners\" so as to bring the threshold budget required to win the game below a given target. This problem has direct applications in compositional policy synthesis for multi-objective settings, and we show it to be NP-complete.","lang":"eng"}],"date_created":"2026-09-13T22:01:53Z","OA_type":"gold","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"success":1,"date_created":"2026-09-17T09:43:28Z","creator":"dernst","access_level":"open_access","file_id":"22946","file_name":"2026_LIPIcsCONCUR_Asadi.pdf","relation":"main_file","file_size":1175682,"checksum":"de9af748d78fa42c173f68a71cbbd8d9","content_type":"application/pdf","date_updated":"2026-09-17T09:43:28Z"}],"external_id":{"arxiv":["2606.29420"]},"publication_status":"published","has_accepted_license":"1","month":"08","_id":"22920","arxiv":1,"supplementarymaterial":"yes","fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"status":"public","language":[{"iso":"eng"}],"corr_author":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":"1","date_published":"2026-08-24T00:00:00Z","acknowledgement":"The research was partially supported by Austrian Science Fund (FWF) 10.55776/COE12,\r\nERC CoG 863818 (ForM-SMArt), FWF-2022-SFB F8502 (SPyCoDe), ERC-2020-AdG 101020093\r\n(VAMOS), and the RYC2024-049116-I grant funded by MICIU/AEI/10.13039/501100011033 and\r\nESF+.\r\n","article_number":"13:1-13:20","author":[{"full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","first_name":"Ali","last_name":"Asadi"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshadi","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587"},{"full_name":"Kebis, Pavol","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a","first_name":"Pavol","last_name":"Kebis"},{"orcid":"0000-0001-9864-7475","last_name":"Mallik","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik"}],"title":"Generalized bidding games: Where bidding and stochastic games meet","conference":{"name":"CONCUR: Conference on Concurrency Theory","start_date":"2026-09-01","end_date":"2026-09-04","location":"Liverpool, United Kingdom"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","article_processing_charge":"Yes","ddc":["000"],"volume":391,"publication":"37th International Conference on Concurrency Theory","das_tickbox":"0","alternative_title":["LIPIcs"],"date_updated":"2026-09-17T09:44:41Z","oa_version":"Published Version","file_date_updated":"2026-09-17T09:43:28Z","OA_place":"publisher","researchdata_availability":"no","project":[{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"},{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"doi":"10.4230/LIPIcs.CONCUR.2026.13","keyword":["Bidding Games","Stochastic Games"],"quality_controlled":"1","intvolume":" 391","oa":1,"day":"24","citation":{"ieee":"A. Asadi, T. A. Henzinger, E. Goharshady, P. Kebis, and K. Mallik, “Generalized bidding games: Where bidding and stochastic games meet,” in 37th International Conference on Concurrency Theory, Liverpool, United Kingdom, 2026, vol. 391.","mla":"Asadi, Ali, et al. “Generalized Bidding Games: Where Bidding and Stochastic Games Meet.” 37th International Conference on Concurrency Theory, vol. 391, 13:1-13:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:10.4230/LIPIcs.CONCUR.2026.13.","chicago":"Asadi, Ali, Thomas A Henzinger, Ehsan Goharshady, Pavol Kebis, and Kaushik Mallik. “Generalized Bidding Games: Where Bidding and Stochastic Games Meet.” In 37th International Conference on Concurrency Theory, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.CONCUR.2026.13.","short":"A. Asadi, T.A. Henzinger, E. Goharshady, P. Kebis, K. Mallik, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","ista":"Asadi A, Henzinger TA, Goharshady E, Kebis P, Mallik K. 2026. Generalized bidding games: Where bidding and stochastic games meet. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 13:1-13:20.","ama":"Asadi A, Henzinger TA, Goharshady E, Kebis P, Mallik K. Generalized bidding games: Where bidding and stochastic games meet. In: 37th International Conference on Concurrency Theory. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:10.4230/LIPIcs.CONCUR.2026.13","apa":"Asadi, A., Henzinger, T. A., Goharshady, E., Kebis, P., & Mallik, K. (2026). Generalized bidding games: Where bidding and stochastic games meet. In 37th International Conference on Concurrency Theory (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2026.13"}},{"abstract":[{"lang":"eng","text":"Reachability is the most fundamental logical objective, yet it is notoriously difficult to learn in reinforcement learning settings: even for Markov decision processes, PAC learning of reachability is impossible without additional assumptions. This difficulty also holds in turn-based stochastic games (TBSGs), where two adversarial players interact on a finite state space. In this work, we consider turn-based stochastic games with reachability objectives. For such settings, adversarial learning, in which players are adversarial even in the learning phase, is impossible. Therefore, the goal is to consider learning, in which both players learn the unknown model together. In this spirit, previous literature on PAC learning in TBSGs considers (a) public information shared by both players; and (b) centralized learning, which means that players share the same learning algorithm. In this work, our contribution is two-fold. First, we relax these strong assumptions and ensure learning: (i) with private information not shared with the other player; and (ii) decentralized learning where the players do not share the same learning algorithm. To the best of our knowledge, this work is the first positive result for decentralized and private information learning of TBSGs with reachability objectives. Second, we introduce a game-theoretic generalization of the Expected Conditional Distance (ECD) parameter, which measures the expected length of reaching the target set. We establish a polynomial-sample complexity bound with respect to the number of states, actions, ECD parameter, and inverses of error tolerance and failure probability."}],"OA_type":"gold","date_created":"2026-09-13T22:01:53Z","year":"2026","publication_identifier":{"isbn":["9783959774475"],"eissn":["1868-8969"]},"month":"08","_id":"22919","publication_status":"published","has_accepted_license":"1","file":[{"content_type":"application/pdf","date_updated":"2026-09-17T09:50:00Z","relation":"main_file","file_size":959234,"checksum":"2e6c55b65d9d7ce436a6f59e81d7ba17","access_level":"open_access","file_id":"22947","file_name":"2026_LIPIcsCONCUR_Asadi2.pdf","success":1,"date_created":"2026-09-17T09:50:00Z","creator":"dernst"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","external_id":{"arxiv":["2607.14877"]},"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12","arxiv":1,"supplementarymaterial":"yes","date_published":"2026-08-24T00:00:00Z","acknowledgement":"The research was partially supported by Austrian Science Fund (FWF) 10.55776/COE12,\r\nERC CoG 863818 (ForM-SMArt), FWF-2022-SFB F8502 (SPyCoDe), and ERC-2020-AdG 101020093\r\n(VAMOS) grants.","article_number":"12:1-12:23","corr_author":"1","scopus_import":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"},{"_id":"ToHe"}],"language":[{"iso":"eng"}],"status":"public","volume":391,"publication":"37th International Conference on Concurrency Theory","ddc":["000"],"article_processing_charge":"Yes","title":"PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance","author":[{"first_name":"Ali","last_name":"Asadi","full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Pavol","last_name":"Kebis","full_name":"Kebis, Pavol","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a"}],"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2026-09-04","location":"Liverpool, United Kingdom","name":"CONCUR: Conference on Concurrency Theory","start_date":"2026-09-01"},"researchdata_availability":"no","file_date_updated":"2026-09-17T09:50:00Z","OA_place":"publisher","alternative_title":["LIPIcs"],"date_updated":"2026-09-17T09:51:25Z","das_tickbox":"0","oa_version":"Published Version","intvolume":" 391","oa":1,"quality_controlled":"1","doi":"10.4230/LIPIcs.CONCUR.2026.12","keyword":["formal methods","games and logic","logical aspects of AI","model checking"],"project":[{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"},{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"citation":{"ama":"Asadi A, Chatterjee K, Kebis P. PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance. In: 37th International Conference on Concurrency Theory. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:10.4230/LIPIcs.CONCUR.2026.12","apa":"Asadi, A., Chatterjee, K., & Kebis, P. (2026). PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance. In 37th International Conference on Concurrency Theory (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2026.12","ista":"Asadi A, Chatterjee K, Kebis P. 2026. PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 12:1-12:23.","mla":"Asadi, Ali, et al. “PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance.” 37th International Conference on Concurrency Theory, vol. 391, 12:1-12:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:10.4230/LIPIcs.CONCUR.2026.12.","chicago":"Asadi, Ali, Krishnendu Chatterjee, and Pavol Kebis. “PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance.” In 37th International Conference on Concurrency Theory, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.CONCUR.2026.12.","short":"A. Asadi, K. Chatterjee, P. Kebis, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","ieee":"A. Asadi, K. Chatterjee, and P. Kebis, “PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance,” in 37th International Conference on Concurrency Theory, Liverpool, United Kingdom, 2026, vol. 391."},"day":"24"},{"publication_identifier":{"issn":["2663-337X"],"isbn":["978-3-99078-089-3"]},"year":"2026","date_created":"2026-09-05T15:59:19Z","abstract":[{"lang":"eng","text":"As automated decision-makers have become ubiquitous in many domains of life,\r\ntheir decisions have become increasingly consequential. Recent years have shown\r\nthat such systems can exhibit discriminatory behaviour against individuals and\r\nsocial groups alike, thereby amplifying existing biases and entrenching\r\nsocio-economic disparities over time. Algorithmic fairness addresses this\r\nproblem by developing methods to quantify and mitigate unfair behaviour.\r\nHowever, much of the existing literature studies fairness in a static\r\npre-deployment setting and, therefore, neglects that automated decision-makers are\r\noften deployed in dynamic environments, where their behaviour and the\r\npopulations they affect may change over time.\r\n\r\nThis thesis addresses this gap through the lens of runtime verification.\r\nInstead of treating fairness as a property of a classifier together with a fixed\r\ninput distribution, it reframes fairness as a property of the interaction trace\r\nbetween the decision-maker and its deployment environment. To evaluate such\r\nsequential fairness properties, the thesis develops runtime monitors that\r\nobserve the evolving interaction between the system and the environment and\r\nissue verdicts after each new observation. Because, these monitors are designed to detect\r\nunfair behaviour during deployment, they complement fair training,\r\nauditing, verification, and enforcement by providing an additional layer of mathematically rigorous fairness assurance.\r\n\r\nIn summary, the thesis develops quantitative, trace-based analogues of\r\nclassical group and individual fairness measures and constructs monitors for\r\nthem. This includes monitors for long-run group fairness over Markovian traces,\r\nfor the time-varying welfare of a changing population in a dynamical system, and\r\nfor the individual fairness of an arbitrary system generating a trace of inputs\r\nand outputs. To achieve this, the monitors combine ideas from runtime\r\nverification, sequential statistics, and nearest-neighbour search. In the\r\ngroup-fairness settings, monitoring is primarily a sequential statistical\r\nestimation problem: the monitor must construct statistically sound interval\r\nestimates of fairness values from dependent and partially observed interactions.\r\nIn the individual-fairness setting, the main challenge is computational\r\nefficiency: the monitor must detect individual fairness violations by efficiently comparing the\r\ncurrent decision with all previously observed decisions.\r\n"}],"file":[{"file_name":"Thesis_Konstantin_Kueffner-3.zip","file_id":"22903","access_level":"closed","creator":"kkueffne","date_created":"2026-09-11T07:32:13Z","date_updated":"2026-09-11T07:32:13Z","content_type":"application/zip","checksum":"716ce44a6ed9a727f231bdebdeecc741","file_size":26356903,"relation":"source_file"},{"date_created":"2026-09-11T07:32:17Z","creator":"kkueffne","access_level":"open_access","file_id":"22904","file_name":"Thesis_Konstantin_Kueffner-2.pdf","relation":"main_file","checksum":"77082e90b8330fb46f585843840c5d5c","file_size":10051715,"content_type":"application/pdf","date_updated":"2026-09-11T07:32:17Z"}],"publisher":"Institute of Science and Technology Austria","has_accepted_license":"1","publication_status":"published","supervisor":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"}],"_id":"22808","month":"09","fulldoi":"https://doi.org/10.15479/AT-ISTA-22808","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"status":"public","language":[{"iso":"eng"}],"corr_author":"1","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS).\r\n","doi_confirm":"1","date_published":"2026-09-07T00:00:00Z","type":"dissertation","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","author":[{"orcid":"0000-0001-8974-2542","first_name":"Konstantin","last_name":"Kueffner","full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515"}],"title":"Monitoring algorithmic fairness in sequential decision making","article_processing_charge":"No","ddc":["000"],"degree_awarded":"PhD","alternative_title":["ISTA Thesis"],"oa_version":"Published Version","date_updated":"2026-09-18T07:41:29Z","OA_place":"publisher","file_date_updated":"2026-09-11T07:32:17Z","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"13310"},{"status":"public","id":"14454","relation":"part_of_dissertation"},{"status":"public","id":"20292","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"21090","status":"public"},{"relation":"part_of_dissertation","id":"13228","status":"public"}]},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"doi":"10.15479/AT-ISTA-22808","oa":1,"page":"183","day":"07","citation":{"ama":"Kueffner K. Monitoring algorithmic fairness in sequential decision making. 2026. doi:10.15479/AT-ISTA-22808","apa":"Kueffner, K. (2026). Monitoring algorithmic fairness in sequential decision making. Institute of Science and Technology Austria. https://doi.org/10.15479/AT-ISTA-22808","ista":"Kueffner K. 2026. Monitoring algorithmic fairness in sequential decision making. Institute of Science and Technology Austria.","mla":"Kueffner, Konstantin. Monitoring Algorithmic Fairness in Sequential Decision Making. Institute of Science and Technology Austria, 2026, doi:10.15479/AT-ISTA-22808.","chicago":"Kueffner, Konstantin. “Monitoring Algorithmic Fairness in Sequential Decision Making.” Institute of Science and Technology Austria, 2026. https://doi.org/10.15479/AT-ISTA-22808.","short":"K. Kueffner, Monitoring Algorithmic Fairness in Sequential Decision Making, Institute of Science and Technology Austria, 2026.","ieee":"K. Kueffner, “Monitoring algorithmic fairness in sequential decision making,” Institute of Science and Technology Austria, 2026."}},{"quality_controlled":"1","dataavailabilitystatement":"Software (Source Code): https://github.com/filipcano/monitoringdiscounted-sum-properties [10]\r\narchived at swh:1:dir:cb99396415f279c985cd05206b44320227f64245\r\n","intvolume":" 391","oa":1,"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"keyword":["Runtime Verification","Probabilistic Systems","Quantitative Verification","Approximate Monitoring"],"doi":"10.4230/LIPIcs.CONCUR.2026.22","citation":{"mla":"Cano Cordoba, Filip, et al. “Monitoring Discounted Sum Properties.” 37th International Conference on Concurrency Theory, vol. 391, 22:1-22:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:10.4230/LIPIcs.CONCUR.2026.22.","short":"F. Cano Cordoba, T.A. Henzinger, K. Kueffner, N.E. Sarac, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","chicago":"Cano Cordoba, Filip, Thomas A Henzinger, Konstantin Kueffner, and Naci E Sarac. “Monitoring Discounted Sum Properties.” In 37th International Conference on Concurrency Theory, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.CONCUR.2026.22.","ieee":"F. Cano Cordoba, T. A. Henzinger, K. Kueffner, and N. E. Sarac, “Monitoring discounted sum properties,” in 37th International Conference on Concurrency Theory, Liverpool, United Kingdom, 2026, vol. 391.","ama":"Cano Cordoba F, Henzinger TA, Kueffner K, Sarac NE. Monitoring discounted sum properties. In: 37th International Conference on Concurrency Theory. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:10.4230/LIPIcs.CONCUR.2026.22","apa":"Cano Cordoba, F., Henzinger, T. A., Kueffner, K., & Sarac, N. E. (2026). Monitoring discounted sum properties. In 37th International Conference on Concurrency Theory (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2026.22","ista":"Cano Cordoba F, Henzinger TA, Kueffner K, Sarac NE. 2026. Monitoring discounted sum properties. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 22:1-22:19."},"day":"24","ddc":["000"],"volume":391,"publication":"37th International Conference on Concurrency Theory","author":[{"orcid":"0000-0002-0783-904X","full_name":"Cano Cordoba, Filip","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","first_name":"Filip","last_name":"Cano Cordoba"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner","first_name":"Konstantin","orcid":"0000-0001-8974-2542"},{"first_name":"Naci E","last_name":"Sarac","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E"}],"title":"Monitoring discounted sum properties","conference":{"start_date":"2026-09-01","name":"CONCUR: Conference on Concurrency Theory","location":"Liverpool, United Kingdom","end_date":"2026-09-04"},"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"Yes","file_date_updated":"2026-09-22T05:59:03Z","OA_place":"publisher","researchdata_availability":"no","oa_version":"Published Version","alternative_title":["LIPIcs"],"date_updated":"2026-09-22T06:02:06Z","das_tickbox":"1","fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.22","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"arxiv":1,"supplementarymaterial":"no","scopus_import":"1","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"corr_author":"1","date_published":"2026-08-24T00:00:00Z","article_number":"22:1-22:19","acknowledgement":"This work has been supported by the European Research Council under Grant No.: ERC2020-AdG 101020093 and ERC-2021-AdG 101055412.\r\nFilip Cano: ERC-2020-AdG 101020093\r\nThomas A. Henzinger: ERC-2020-AdG 101020093\r\nKonstantin Kueffner: ERC-2020-AdG 101020093\r\nN. Ege Saraç: ERC-2021-AdG 101055412","status":"public","language":[{"iso":"eng"}],"year":"2026","abstract":[{"lang":"eng","text":"Runtime monitoring of quantitative signals faces a fundamental trade-off between volatility and over-aggregation: instantaneous observations are noisy, while long-run averages obscure local structure. Localisation measures such as discounted averages offer a principled middle ground, yet remain poorly understood in runtime verification. This paper studies discounted sums from a monitoring perspective, in both deterministic and stochastic settings. We formalize the discounted monitoring problem and show that exact, sound monitoring of discounted sums cannot be achieved with finite memory. To overcome this impossibility, we introduce ε-approximately sound monitoring, deriving explicit bounds on memory and observation requirements. We then extend the framework to stochastic processes via expected discounted sums, defining pointwise and uniform (ε,δ)-soundness notions, establishing statistical optimality, and proving impossibility beyond a precision threshold. We also formalize the resource complexity of deterministic discounted monitoring via affine register machines and prove a tight worst-case lower bound. Finally, we present a specification language for arithmetic expressions over multiple discounted sums with synchronous and asynchronous semantics, and evaluate our approach on practical scenarios including algorithmic fairness."}],"date_created":"2026-09-13T22:01:54Z","OA_type":"gold","publication_identifier":{"isbn":["9783959774475"],"issn":["1868-8969"]},"month":"08","_id":"22921","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"file_id":"22978","access_level":"open_access","file_name":"2026_LIPIcsCONCUR_Cano.pdf","date_created":"2026-09-22T05:59:03Z","success":1,"creator":"dernst","content_type":"application/pdf","date_updated":"2026-09-22T05:59:03Z","relation":"main_file","checksum":"f7b2e22428344fd7972c54f099df6aba","file_size":997156}],"external_id":{"arxiv":["2606.25979"]},"publication_status":"published","has_accepted_license":"1"},{"ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6","supplementarymaterial":"no","article_number":"6:1-6:7","acknowledgement":" Krishnendu Chatterjee: Supported in part by the Austrian Science Fund (FWF) COE\r\ngrant 10.55776/COE12 and the ERC CoG 863818 (ForM-SMArt).\r\nThomas A. Henzinger: Supported in part by the ERC AdG 101020093 (VAMOS) and the FWF\r\nSFB grant F8502 (SPyCoDe).\r\nNir Piterman: Supported in part by the Swedish research council (VR) project no. 2025-05419 and\r\nthe Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and\r\nAlice Wallenberg Foundation.\r\nAcknowledgements We thank the jury that our paper introducing Strategy Logic at the Conference\r\non Concurrency Theory (CONCUR) 2007 [10] was chosen for a CONCUR Test-of-Time Award at\r\nCONCUR 2026.","date_published":"2026-08-24T00:00:00Z","corr_author":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":"1","language":[{"iso":"eng"}],"status":"public","OA_type":"gold","date_created":"2026-09-13T22:01:54Z","abstract":[{"text":"In this note, we recall the history and our motivation behind the development of Strategy Logic and we discuss some of the work that ensued from its introduction.","lang":"eng"}],"year":"2026","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959774475"]},"month":"08","_id":"22922","has_accepted_license":"1","publication_status":"published","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"creator":"dernst","success":1,"date_created":"2026-09-22T05:53:16Z","file_name":"2026_LIPIcsCONCUR_Chatterjee.pdf","access_level":"open_access","file_id":"22977","file_size":517651,"checksum":"f3995df175701f56a702bdb012e4f710","relation":"main_file","date_updated":"2026-09-22T05:53:16Z","content_type":"application/pdf"}],"oa":1,"intvolume":" 391","quality_controlled":"1","keyword":["Strategy Logic","Games","Automata"],"doi":"10.4230/LIPIcs.CONCUR.2026.6","project":[{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"}],"citation":{"mla":"Chatterjee, Krishnendu, et al. “A Look Back at Strategy Logic.” 37th International Conference on Concurrency Theory, vol. 391, 6:1-6:7, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:10.4230/LIPIcs.CONCUR.2026.6.","short":"K. Chatterjee, T.A. Henzinger, N. Piterman, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Nir Piterman. “A Look Back at Strategy Logic.” In 37th International Conference on Concurrency Theory, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.CONCUR.2026.6.","ieee":"K. Chatterjee, T. A. Henzinger, and N. Piterman, “A look back at strategy logic,” in 37th International Conference on Concurrency Theory, Liverpool, United Kingdom, 2026, vol. 391.","ama":"Chatterjee K, Henzinger TA, Piterman N. A look back at strategy logic. In: 37th International Conference on Concurrency Theory. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:10.4230/LIPIcs.CONCUR.2026.6","apa":"Chatterjee, K., Henzinger, T. A., & Piterman, N. (2026). A look back at strategy logic. In 37th International Conference on Concurrency Theory (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2026.6","ista":"Chatterjee K, Henzinger TA, Piterman N. 2026. A look back at strategy logic. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 6:1-6:7."},"day":"24","publication":"37th International Conference on Concurrency Theory","volume":391,"ddc":["000"],"article_processing_charge":"Yes","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Liverpool, United Kingdom","end_date":"2026-09-04","start_date":"2026-09-01","name":"CONCUR: Conference on Concurrency Theory"},"type":"conference","title":"A look back at strategy logic","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Piterman","first_name":"Nir","full_name":"Piterman, Nir"}],"researchdata_availability":"no","OA_place":"publisher","file_date_updated":"2026-09-22T05:53:16Z","das_tickbox":"0","alternative_title":["LIPIcs"],"date_updated":"2026-09-22T05:54:30Z","oa_version":"Published Version"},{"month":"09","_id":"22999","publisher":"Elsevier","has_accepted_license":"1","publication_status":"epub_ahead","year":"2026","date_created":"2026-09-27T22:01:51Z","OA_type":"gold","abstract":[{"text":"The safety of Reinforcement Learning (RL)-based controllers has become a prominent research area in recent years, with various approaches being proposed to address this critical issue. Runtime Safety Assurance (RSA) methods for RL, such as Shielded RL, provide formal safety guarantees by preventing agents from taking unsafe actions and suggesting safe alternatives when necessary. However, previous surveys and reviews on RSA for RL have not thoroughly analysed the challenges and applications within the industrial sector. This study builds on existing state-of-the-art research on Shielded RL methods, emphasising its contributions to industrial applications and offering a domain-specific categorisation. This categorisation highlights the primary industrial domains utilising Shielded RL, detailing the optimised functions achieved by RL and the safety functions ensured by the shield. Additionally, the study presents a categorisation based on environmental features, enabling readers to assess the complexity of the problems addressed by the techniques studied. The shield’s attributes are analysed for each work, identifying key trends in their application, including their adaptability to new scenarios. Finally, a basic categorisation model for Shielded RL approaches, grounded in industrial safety standards, is introduced. This model serves as a baseline for future studies aiming to evaluate the maturity level of the works reviewed.","lang":"eng"}],"publication_identifier":{"issn":["2667-3053"]},"corr_author":"1","department":[{"_id":"ToHe"}],"scopus_import":"1","acknowledgement":"This work was supported in part by the SAFEXPLAIN project under Grant 101069595.\r\nThis work was supported in part by the ROBOCONS project under Grant 101235566, from the European Union‘s HORIZON-CL5-2024-D4-02 research and innovation programme.\r\nThis work was supported in part by the Austrian Science Fund (FWF) - Reference 10.55776/COE12.\r\nThis work was supported in part by the Intelligent Systems for Industrial Systems research group of Mondragon Unibertsitatea - Reference IT1870-26. Department of Science, Universities and Innovation of the Basque Government.\r\nThis work was supported in part by the European Research Council under Grant No.: ERC-2020-AdG 101020093. This work was also supported by the ISTA Responsible AI Program, made possible through the support of Garrett Camp and the Camp Foundation .","article_number":"200729","date_published":"2026-09-18T00:00:00Z","status":"public","DOAJ_listed":"1","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1016/j.iswa.2026.200729","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"PlanS_conform":"1","supplementarymaterial":"no","OA_place":"publisher","researchdata_availability":"no","das_tickbox":"1","oa_version":"Published Version","date_updated":"2026-10-07T06:25:37Z","ddc":["000"],"publication":"Intelligent Systems with Applications","volume":32,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","title":"Shielded reinforcement learning for industrial applications: A systematic literature survey","author":[{"first_name":"Haritz","last_name":"Odriozola-Olalde","full_name":"Odriozola-Olalde, Haritz"},{"orcid":"0000-0002-0783-904X","last_name":"Cano Cordoba","first_name":"Filip","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","full_name":"Cano Cordoba, Filip"},{"full_name":"Könighofer, Bettina","last_name":"Könighofer","first_name":"Bettina"},{"full_name":"Arana-Arexolaleiba, Nestor","first_name":"Nestor","last_name":"Arana-Arexolaleiba"},{"first_name":"Maider","last_name":"Zamalloa","full_name":"Zamalloa, Maider"},{"last_name":"Perez-Cerrolaza","first_name":"Jon","full_name":"Perez-Cerrolaza, Jon"}],"article_processing_charge":"Yes","citation":{"ieee":"H. Odriozola-Olalde, F. Cano Cordoba, B. Könighofer, N. Arana-Arexolaleiba, M. Zamalloa, and J. Perez-Cerrolaza, “Shielded reinforcement learning for industrial applications: A systematic literature survey,” Intelligent Systems with Applications, vol. 32. Elsevier, 2026.","mla":"Odriozola-Olalde, Haritz, et al. “Shielded Reinforcement Learning for Industrial Applications: A Systematic Literature Survey.” Intelligent Systems with Applications, vol. 32, 200729, Elsevier, 2026, doi:10.1016/j.iswa.2026.200729.","short":"H. Odriozola-Olalde, F. Cano Cordoba, B. Könighofer, N. Arana-Arexolaleiba, M. Zamalloa, J. Perez-Cerrolaza, Intelligent Systems with Applications 32 (2026).","chicago":"Odriozola-Olalde, Haritz, Filip Cano Cordoba, Bettina Könighofer, Nestor Arana-Arexolaleiba, Maider Zamalloa, and Jon Perez-Cerrolaza. “Shielded Reinforcement Learning for Industrial Applications: A Systematic Literature Survey.” Intelligent Systems with Applications. Elsevier, 2026. https://doi.org/10.1016/j.iswa.2026.200729.","ista":"Odriozola-Olalde H, Cano Cordoba F, Könighofer B, Arana-Arexolaleiba N, Zamalloa M, Perez-Cerrolaza J. 2026. Shielded reinforcement learning for industrial applications: A systematic literature survey. Intelligent Systems with Applications. 32, 200729.","ama":"Odriozola-Olalde H, Cano Cordoba F, Könighofer B, Arana-Arexolaleiba N, Zamalloa M, Perez-Cerrolaza J. Shielded reinforcement learning for industrial applications: A systematic literature survey. Intelligent Systems with Applications. 2026;32. doi:10.1016/j.iswa.2026.200729","apa":"Odriozola-Olalde, H., Cano Cordoba, F., Könighofer, B., Arana-Arexolaleiba, N., Zamalloa, M., & Perez-Cerrolaza, J. (2026). Shielded reinforcement learning for industrial applications: A systematic literature survey. Intelligent Systems with Applications. Elsevier. https://doi.org/10.1016/j.iswa.2026.200729"},"article_type":"review","day":"18","quality_controlled":"1","dataavailabilitystatement":"No data was used for the research described in the article.","oa":1,"intvolume":" 32","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1016/j.iswa.2026.200729"}],"project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"doi":"10.1016/j.iswa.2026.200729","keyword":["Reinforcement learning","Runtime safety assurance","Shield","Safety","Industrial application"]},{"publisher":"Gesellschaft für Informatik","file":[{"date_updated":"2026-10-19T08:39:37Z","content_type":"application/pdf","file_size":147208,"checksum":"3371c63711ed26efa41744834d337d28","relation":"main_file","file_name":"2026_LNI_Richter.pdf","file_id":"23170","access_level":"open_access","creator":"dernst","success":1,"date_created":"2026-10-19T08:39:37Z"}],"publication_status":"published","has_accepted_license":"1","_id":"22622","month":"03","publication_identifier":{"eissn":["1617-5468"]},"year":"2026","abstract":[{"lang":"eng","text":"Cooperative software verification aims at improving the effectiveness and efficiency of software verification by enabling multiple verification tools to work together. Existing cooperative verification schemes, however, typically require specialized interfaces or tight integration, limiting their practical applicability. In our International Conference on Software Engineering (ICSE) 2025 publication, we introduce dynamic program splitting – a novel approach that enables cooperation between off-the-shelf verification tools without requiring any modifications. The key idea is to probe verification tools on a given verification task under a time limit and split tasks dynamically that cannot be verified under the given time constraints. The process continues recursively, incrementally identifying program parts that are particularly hard for the given verifier. The remaining unverified parts are provided to a second verifier, allowing to leverage the complementary strengths of different tools. Our evaluation on SV-COMP benchmarks demonstrates that cooperation through dynamic program splitting enables the verification of tasks that none of the individual verifiers can solve on their own."}],"date_created":"2026-08-02T22:01:54Z","OA_type":"hybrid","status":"public","language":[{"iso":"eng"}],"scopus_import":"1","department":[{"_id":"ToHe"}],"date_published":"2026-03-01T00:00:00Z","supplementarymaterial":"no","fulldoi":"https://doi.org/10.18420/se2026_45","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-sa/4.0/legalcode","image":"/images/cc_by_sa.png","name":"Creative Commons Attribution-ShareAlike 4.0 International Public License (CC BY-SA 4.0)","short":"CC BY-SA (4.0)"},"das_tickbox":"1","alternative_title":["Lecture Notes in Informatics"],"date_updated":"2026-10-19T08:49:32Z","oa_version":"Published Version","file_date_updated":"2026-10-19T08:39:37Z","OA_place":"publisher","researchdata_availability":"yes","author":[{"first_name":"Cedric","last_name":"Richter","full_name":"Richter, Cedric"},{"last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek"},{"first_name":"Marie Christine","last_name":"Jakobs","full_name":"Jakobs, Marie Christine"},{"full_name":"Wehrheim, Heike","first_name":"Heike","last_name":"Wehrheim"}],"title":"Off-the-Shelf cooperative software verification by splitting programs dynamically","conference":{"end_date":"2026-02-27","location":"Bonn, Switzerland","name":"SE: Software Engineering","start_date":"2026-02-23"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","article_processing_charge":"No","ddc":["000"],"volume":"P-377","publication":"Software Engineering 2026","page":"41-42","day":"01","citation":{"ama":"Richter C, Chalupa M, Jakobs MC, Wehrheim H. Off-the-Shelf cooperative software verification by splitting programs dynamically. In: Software Engineering 2026. Vol P-377. Gesellschaft für Informatik; 2026:41-42. doi:10.18420/se2026_45","apa":"Richter, C., Chalupa, M., Jakobs, M. C., & Wehrheim, H. (2026). Off-the-Shelf cooperative software verification by splitting programs dynamically. In Software Engineering 2026 (Vol. P-377, pp. 41–42). Bonn, Switzerland: Gesellschaft für Informatik. https://doi.org/10.18420/se2026_45","ista":"Richter C, Chalupa M, Jakobs MC, Wehrheim H. 2026. Off-the-Shelf cooperative software verification by splitting programs dynamically. Software Engineering 2026. SE: Software Engineering, Lecture Notes in Informatics, vol. P-377, 41–42.","mla":"Richter, Cedric, et al. “Off-the-Shelf Cooperative Software Verification by Splitting Programs Dynamically.” Software Engineering 2026, vol. P-377, Gesellschaft für Informatik, 2026, pp. 41–42, doi:10.18420/se2026_45.","chicago":"Richter, Cedric, Marek Chalupa, Marie Christine Jakobs, and Heike Wehrheim. “Off-the-Shelf Cooperative Software Verification by Splitting Programs Dynamically.” In Software Engineering 2026, P-377:41–42. Gesellschaft für Informatik, 2026. https://doi.org/10.18420/se2026_45.","short":"C. Richter, M. Chalupa, M.C. Jakobs, H. Wehrheim, in:, Software Engineering 2026, Gesellschaft für Informatik, 2026, pp. 41–42.","ieee":"C. Richter, M. Chalupa, M. C. Jakobs, and H. Wehrheim, “Off-the-Shelf cooperative software verification by splitting programs dynamically,” in Software Engineering 2026, Bonn, Switzerland, 2026, vol. P-377, pp. 41–42."},"doi":"10.18420/se2026_45","license":"https://creativecommons.org/licenses/by-sa/4.0/","keyword":["Software Verification","Cooperation","Program Decomposition"],"quality_controlled":"1","dataavailabilitystatement":"All our implementations and data are archived and available at Zenodo5\r\nand are evaluated as an artifact in the ICSE 2025 artifact evaluation. Furthermore, our\r\napproach is integrated into the software verifier Bubaak [CR25] which we submitted as\r\npart of our contribution to SV-COMP 2025.","oa":1},{"_id":"20866","month":"12","external_id":{"arxiv":["2305.02836"]},"file":[{"relation":"main_file","checksum":"06ed45a1218ad8464818803ae2968aaf","file_size":7117003,"content_type":"application/pdf","date_updated":"2026-01-05T12:26:43Z","date_created":"2026-01-05T12:26:43Z","success":1,"creator":"dernst","file_id":"20944","access_level":"open_access","file_name":"2025_ActaInformatica_Bartocci.pdf"}],"publisher":"Springer Nature","has_accepted_license":"1","publication_status":"published","year":"2025","date_created":"2025-12-29T12:07:12Z","OA_type":"hybrid","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."}],"publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"corr_author":"1","department":[{"_id":"ToHe"}],"scopus_import":"1","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).","article_number":"43","date_published":"2025-12-09T00:00:00Z","status":"public","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1007/s00236-025-00509-8","issue":"4","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"arxiv":1,"OA_place":"publisher","file_date_updated":"2026-01-05T12:26:43Z","related_material":{"record":[{"id":"14405","relation":"earlier_version","status":"public"}]},"date_updated":"2026-01-05T12:27:41Z","oa_version":"Published Version","ddc":["000"],"publication":"Acta Informatica","volume":62,"type":"journal_article","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Bartocci, Ezio","last_name":"Bartocci","first_name":"Ezio"},{"full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","first_name":"Marek"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Nickovic","first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan"},{"orcid":"0000-0002-8741-5799","full_name":"Oliveira da Costa, Ana","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","last_name":"Oliveira da Costa","first_name":"Ana"}],"title":"Hypernode automata","article_processing_charge":"Yes (via OA deal)","citation":{"ieee":"E. Bartocci, M. Chalupa, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode automata,” Acta Informatica, vol. 62, no. 4. Springer Nature, 2025.","short":"E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, Acta Informatica 62 (2025).","chicago":"Bartocci, Ezio, Marek Chalupa, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Hypernode Automata.” Acta Informatica. Springer Nature, 2025. https://doi.org/10.1007/s00236-025-00509-8.","mla":"Bartocci, Ezio, et al. “Hypernode Automata.” Acta Informatica, vol. 62, no. 4, 43, Springer Nature, 2025, doi:10.1007/s00236-025-00509-8.","ista":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025. Hypernode automata. Acta Informatica. 62(4), 43.","apa":"Bartocci, E., Chalupa, M., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A. (2025). Hypernode automata. Acta Informatica. Springer Nature. https://doi.org/10.1007/s00236-025-00509-8","ama":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata. Acta Informatica. 2025;62(4). doi:10.1007/s00236-025-00509-8"},"article_type":"original","day":"09","quality_controlled":"1","oa":1,"intvolume":" 62","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"},{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"doi":"10.1007/s00236-025-00509-8"}]