[{"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"department":[{"_id":"ToHe"}],"ec_funded":1,"file":[{"date_updated":"2023-01-27T03:18:34Z","file_name":"main.pdf","access_level":"open_access","content_type":"application/pdf","checksum":"55426e463fdeafe9777fc3ff635154c7","success":1,"file_size":662409,"creator":"fmuehlbo","date_created":"2023-01-27T03:18:34Z","file_id":"12408","relation":"main_file"}],"author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"last_name":"Mühlböck","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","first_name":"Fabian"},{"id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","first_name":"Stefanie","last_name":"Muroya Lei","full_name":"Muroya Lei, Stefanie"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Published Version","oa":1,"publication_status":"published","month":"01","doi":"10.15479/AT:ISTA:12407","date_published":"2023-01-27T00:00:00Z","_id":"12407","type":"technical_report","keyword":["runtime monitoring","best effort","third party"],"file_date_updated":"2023-01-27T03:18:34Z","publication_identifier":{"eissn":["2664-1690"]},"language":[{"iso":"eng"}],"alternative_title":["IST Austria Technical Report"],"publisher":"Institute of Science and Technology Austria","date_updated":"2023-04-25T07:19:06Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["005"],"title":"VAMOS: Middleware for Best-Effort Third-Party Monitoring","article_processing_charge":"No","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"status":"public","page":"38","date_created":"2023-01-27T03:18:08Z","year":"2023","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. \r\nThe authors would like to thank the anonymous FASE reviewers for their valuable feedback and suggestions.","related_material":{"record":[{"relation":"later_version","id":"12856","status":"public"}]},"has_accepted_license":"1","abstract":[{"text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\n\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch.","lang":"eng"}],"license":"https://creativecommons.org/licenses/by/4.0/","citation":{"mla":"Chalupa, Marek, et al. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:12407\">10.15479/AT:ISTA:12407</a>.","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023.","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, VAMOS: Middleware for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria, 2023.","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria; 2023. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:12407\">10.15479/AT:ISTA:12407</a>","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023. <a href=\"https://doi.org/10.15479/AT:ISTA:12407\">https://doi.org/10.15479/AT:ISTA:12407</a>.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2023). <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:12407\">https://doi.org/10.15479/AT:ISTA:12407</a>","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. VAMOS: Middleware for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria, 38p."},"day":"27"},{"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"ec_funded":1,"file":[{"success":1,"access_level":"open_access","content_type":"application/pdf","checksum":"981025aed580b6b27c426cb8856cf63e","file_name":"qsl.pdf","date_updated":"2023-01-31T07:22:21Z","file_size":449027,"creator":"esarac","file_id":"12468","date_created":"2023-01-31T07:22:21Z","relation":"main_file"},{"content_type":"application/pdf","access_level":"open_access","checksum":"f16e2af1e0eb243158ab0f0fe74e7d5a","success":1,"file_name":"2023_LNCS_HenzingerT.pdf","date_updated":"2023-06-19T10:28:09Z","file_id":"13153","relation":"main_file","date_created":"2023-06-19T10:28:09Z","file_size":1048171,"creator":"dernst"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E"}],"oa_version":"Published Version","month":"04","conference":{"location":"Paris, France","end_date":"2023-04-27","name":"FOSSACS: Foundations of Software Science and Computation Structures","start_date":"2023-04-22"},"external_id":{"arxiv":["2301.11175"]},"arxiv":1,"doi":"10.1007/978-3-031-30829-1_17","date_published":"2023-04-21T00:00:00Z","_id":"12467","intvolume":"     13992","oa":1,"publication":"26th International Conference Foundations of Software Science and Computation Structures","quality_controlled":"1","publication_status":"published","alternative_title":["LNCS"],"type":"conference","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031308284"]},"file_date_updated":"2023-06-19T10:28:09Z","language":[{"iso":"eng"}],"title":"Quantitative safety and liveness","article_processing_charge":"No","date_updated":"2023-07-14T11:20:27Z","publisher":"Springer Nature","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","ddc":["000"],"date_created":"2023-01-31T07:23:56Z","year":"2023","volume":13992,"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","status":"public","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"page":"349-370","scopus_import":"1","has_accepted_license":"1","citation":{"short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference Foundations of Software Science and Computation Structures, Springer Nature, 2023, pp. 349–370.","ista":"Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness. 26th International Conference Foundations of Software Science and Computation Structures. FOSSACS: Foundations of Software Science and Computation Structures, LNCS, vol. 13992, 349–370.","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Safety and Liveness.” In <i>26th International Conference Foundations of Software Science and Computation Structures</i>, 13992:349–70. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">https://doi.org/10.1007/978-3-031-30829-1_17</a>.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In: <i>26th International Conference Foundations of Software Science and Computation Structures</i>. Vol 13992. Springer Nature; 2023:349-370. doi:<a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">10.1007/978-3-031-30829-1_17</a>","apa":"Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Quantitative safety and liveness. In <i>26th International Conference Foundations of Software Science and Computation Structures</i> (Vol. 13992, pp. 349–370). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">https://doi.org/10.1007/978-3-031-30829-1_17</a>","mla":"Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” <i>26th International Conference Foundations of Software Science and Computation Structures</i>, vol. 13992, Springer Nature, 2023, pp. 349–70, doi:<a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">10.1007/978-3-031-30829-1_17</a>.","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and liveness,” in <i>26th International Conference Foundations of Software Science and Computation Structures</i>, Paris, France, 2023, vol. 13992, pp. 349–370."},"day":"21","abstract":[{"lang":"eng","text":"Safety and liveness are elementary concepts of computation, and the foundation of many verification paradigms. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In quantitative specification and verification, properties assign not truth values, but quantitative values to infinite traces (e.g., a cost, or the distance to a boolean property). We introduce quantitative safety and liveness, and we prove that our definitions induce conservative quantitative generalizations of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness decomposition of boolean properties. In particular, we show that every quantitative property can be written as the pointwise minimum of a quantitative safety property and a quantitative liveness property. Consequently, like boolean properties, also quantitative properties can be min-decomposed into safety and liveness parts, or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover, quantitative properties can be approximated naturally. We prove that every quantitative property that has both safe and co-safe approximations can be monitored arbitrarily precisely by a monitor that uses only a finite number of states."}]},{"abstract":[{"lang":"eng","text":"Adversarial training (i.e., training on adversarially perturbed input data) is a well-studied method for making neural networks robust to potential adversarial attacks during inference. However, the improved robustness does not come for free but rather is accompanied by a decrease in overall model accuracy and performance. Recent work has shown that, in practical robot learning applications, the effects of adversarial training do not pose a fair trade-off but inflict a net loss when measured in holistic robot performance. This work revisits the robustness-accuracy trade-off in robot learning by systematically analyzing if recent advances in robust training methods and theory in conjunction with adversarial robot learning, are capable of making adversarial training suitable for real-world robot applications. We evaluate three different robot learning tasks ranging from autonomous driving in a high-fidelity environment amenable to sim-to-real deployment to mobile robot navigation and gesture recognition. Our results demonstrate that, while these techniques make incremental improvements on the trade-off on a relative scale, the negative impact on the nominal accuracy caused by adversarial training still outweighs the improved robustness by an order of magnitude. We conclude that although progress is happening, further advances in robust learning methods are necessary before they can benefit robot learning tasks in practice."}],"day":"01","isi":1,"citation":{"chicago":"Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” <i>IEEE Robotics and Automation Letters</i>. Institute of Electrical and Electronics Engineers, 2023. <a href=\"https://doi.org/10.1109/LRA.2023.3240930\">https://doi.org/10.1109/LRA.2023.3240930</a>.","ista":"Lechner M, Amini A, Rus D, Henzinger TA. 2023. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. IEEE Robotics and Automation Letters. 8(3), 1595–1602.","ama":"Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. <i>IEEE Robotics and Automation Letters</i>. 2023;8(3):1595-1602. doi:<a href=\"https://doi.org/10.1109/LRA.2023.3240930\">10.1109/LRA.2023.3240930</a>","apa":"Lechner, M., Amini, A., Rus, D., &#38; Henzinger, T. A. (2023). Revisiting the adversarial robustness-accuracy tradeoff in robot learning. <i>IEEE Robotics and Automation Letters</i>. Institute of Electrical and Electronics Engineers. <a href=\"https://doi.org/10.1109/LRA.2023.3240930\">https://doi.org/10.1109/LRA.2023.3240930</a>","short":"M. Lechner, A. Amini, D. Rus, T.A. Henzinger, IEEE Robotics and Automation Letters 8 (2023) 1595–1602.","ieee":"M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial robustness-accuracy tradeoff in robot learning,” <i>IEEE Robotics and Automation Letters</i>, vol. 8, no. 3. Institute of Electrical and Electronics Engineers, pp. 1595–1602, 2023.","mla":"Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” <i>IEEE Robotics and Automation Letters</i>, vol. 8, no. 3, Institute of Electrical and Electronics Engineers, 2023, pp. 1595–602, doi:<a href=\"https://doi.org/10.1109/LRA.2023.3240930\">10.1109/LRA.2023.3240930</a>."},"has_accepted_license":"1","related_material":{"record":[{"relation":"earlier_version","id":"11366","status":"public"}]},"scopus_import":"1","page":"1595-1602","status":"public","article_type":"original","acknowledgement":"We thank Christoph Lampert for inspiring this work. The\r\nviews and conclusions contained in this document are those of\r\nthe authors and should not be interpreted as representing the\r\nofficial policies, either expressed or implied, of the United States\r\nAir Force or the U.S. Government. The U.S. Government is\r\nauthorized to reproduce and distribute reprints for Government\r\npurposes notwithstanding any copyright notation herein.","volume":8,"year":"2023","date_created":"2023-03-05T23:01:04Z","ddc":["000"],"date_updated":"2023-08-01T13:36:50Z","publisher":"Institute of Electrical and Electronics Engineers","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","article_processing_charge":"No","title":"Revisiting the adversarial robustness-accuracy tradeoff in robot learning","language":[{"iso":"eng"}],"publication_identifier":{"eissn":["2377-3766"]},"file_date_updated":"2023-03-07T12:22:23Z","issue":"3","type":"journal_article","publication_status":"published","quality_controlled":"1","publication":"IEEE Robotics and Automation Letters","intvolume":"         8","oa":1,"_id":"12704","doi":"10.1109/LRA.2023.3240930","date_published":"2023-03-01T00:00:00Z","external_id":{"isi":["000936534100012"],"arxiv":["2204.07373"]},"arxiv":1,"month":"03","oa_version":"Published Version","author":[{"first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner"},{"first_name":"Alexander","full_name":"Amini, Alexander","last_name":"Amini"},{"first_name":"Daniela","full_name":"Rus, Daniela","last_name":"Rus"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"file":[{"creator":"cchlebak","file_size":944052,"file_id":"12714","date_created":"2023-03-07T12:22:23Z","relation":"main_file","success":1,"content_type":"application/pdf","access_level":"open_access","checksum":"5a75dcd326ea66685de2b1aaec259e85","file_name":"2023_IEEERobAutLetters_Lechner.pdf","date_updated":"2023-03-07T12:22:23Z"}],"department":[{"_id":"ToHe"}]},{"file_date_updated":"2023-04-25T06:58:36Z","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783031308192"],"eisbn":["9783031308208"],"eissn":["1611-3349"],"issn":["0302-9743"]},"type":"conference","alternative_title":["LNCS"],"quality_controlled":"1","publication_status":"published","publication":"Tools and Algorithms for the Construction and Analysis of Systems","intvolume":"     13994","oa":1,"date_published":"2023-04-20T00:00:00Z","doi":"10.1007/978-3-031-30820-8_32","_id":"12854","month":"04","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22","end_date":"2023-04-27","location":"Paris, France"},"author":[{"first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek","last_name":"Chalupa"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger"}],"oa_version":"Published Version","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"file":[{"file_size":16096413,"creator":"dernst","file_id":"12864","date_created":"2023-04-25T06:58:36Z","relation":"main_file","date_updated":"2023-04-25T06:58:36Z","file_name":"2023_LNCS_Chalupa.pdf","success":1,"checksum":"120d2c2a38384058ad0630fdf8288312","access_level":"open_access","content_type":"application/pdf"}],"department":[{"_id":"ToHe"}],"ec_funded":1,"abstract":[{"text":"The main idea behind BUBAAK is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis.\r\nAt SV-COMP  2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why BUBAAK only ran several analyses in parallel, without any coordination. Still, BUBAAK won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition.","lang":"eng"}],"day":"20","citation":{"ieee":"M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Paris, France, 2023, vol. 13994, pp. 535–540.","mla":"Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13994, Springer Nature, 2023, pp. 535–40, doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">10.1007/978-3-031-30820-8_32</a>.","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 13994:535–40. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">https://doi.org/10.1007/978-3-031-30820-8_32</a>.","apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Bubaak: Runtime monitoring of program verifiers. In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">https://doi.org/10.1007/978-3-031-30820-8_32</a>","ama":"Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers. In: <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13994. Springer Nature; 2023:535-540. doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">10.1007/978-3-031-30820-8_32</a>","ista":"Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 535–540.","short":"M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 535–540."},"has_accepted_license":"1","page":"535-540","status":"public","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"volume":13994,"acknowledgement":"This work was supported by the ERC-2020-AdG 10102009 grant.","date_created":"2023-04-20T08:22:53Z","year":"2023","ddc":["000"],"date_updated":"2023-04-25T07:02:43Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","title":"Bubaak: Runtime monitoring of program verifiers","article_processing_charge":"No"},{"title":"Vamos: Middleware for best-effort third-party monitoring","article_processing_charge":"No","ddc":["000"],"publisher":"Springer Nature","date_updated":"2023-04-25T07:19:07Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":13991,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank the anonymous FASE reviewers for their valuable feedback and suggestions.","date_created":"2023-04-20T08:29:42Z","year":"2023","page":"260-281","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"status":"public","related_material":{"record":[{"id":"12407","relation":"earlier_version","status":"public"}]},"has_accepted_license":"1","day":"20","citation":{"mla":"Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” <i>Fundamental Approaches to Software Engineering</i>, vol. 13991, Springer Nature, 2023, pp. 260–81, doi:<a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">10.1007/978-3-031-30826-0_15</a>.","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware for best-effort third-party monitoring,” in <i>Fundamental Approaches to Software Engineering</i>, Paris, France, 2023, vol. 13991, pp. 260–281.","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2023, pp. 260–281.","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. Vamos: Middleware for best-effort third-party monitoring. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13991, 260–281.","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort third-party monitoring. In: <i>Fundamental Approaches to Software Engineering</i>. Vol 13991. Springer Nature; 2023:260-281. doi:<a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">10.1007/978-3-031-30826-0_15</a>","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2023). Vamos: Middleware for best-effort third-party monitoring. In <i>Fundamental Approaches to Software Engineering</i> (Vol. 13991, pp. 260–281). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">https://doi.org/10.1007/978-3-031-30826-0_15</a>","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” In <i>Fundamental Approaches to Software Engineering</i>, 13991:260–81. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">https://doi.org/10.1007/978-3-031-30826-0_15</a>."},"abstract":[{"lang":"eng","text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch."}],"file":[{"success":1,"access_level":"open_access","content_type":"application/pdf","checksum":"17a7c8e08be609cf2408d37ea55e322c","date_updated":"2023-04-25T07:16:36Z","file_name":"2023_LNCS_ChalupaM.pdf","file_size":580828,"creator":"dernst","date_created":"2023-04-25T07:16:36Z","file_id":"12865","relation":"main_file"}],"department":[{"_id":"ToHe"}],"ec_funded":1,"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"author":[{"last_name":"Chalupa","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian","last_name":"Mühlböck"},{"first_name":"Stefanie","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","full_name":"Muroya Lei, Stefanie","last_name":"Muroya Lei"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"}],"oa_version":"Published Version","doi":"10.1007/978-3-031-30826-0_15","date_published":"2023-04-20T00:00:00Z","_id":"12856","month":"04","conference":{"start_date":"2023-04-22","name":"FASE: Fundamental Approaches to Software Engineering","end_date":"2023-04-27","location":"Paris, France"},"quality_controlled":"1","publication_status":"published","publication":"Fundamental Approaches to Software Engineering","intvolume":"     13991","oa":1,"alternative_title":["LNCS"],"file_date_updated":"2023-04-25T07:16:36Z","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783031308253"],"eisbn":["9783031308260"],"eissn":["1611-3349"],"issn":["0302-9743"]},"type":"conference"},{"article_type":"original","status":"public","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020"}],"date_created":"2023-04-30T22:01:05Z","year":"2023","volume":39,"acknowledgement":"This work was partially supported by GACR [grant No. GA22-10845S]; and Grant Agency of Masaryk University [grant No. MUNI/G/1771/2020]. This work was partially supported by European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie [Grant Agreement No. 101034413 to S.P.].","date_updated":"2023-08-01T14:27:28Z","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publisher":"Oxford Academic","ddc":["000"],"title":"Boolean network sketches: A unifying framework for logical model inference","pmid":1,"article_processing_charge":"No","article_number":"btad158","abstract":[{"lang":"eng","text":"Motivation: The problem of model inference is of fundamental importance to systems biology. Logical models (e.g. Boolean networks; BNs) represent a computationally attractive approach capable of handling large biological networks. The models are typically inferred from experimental data. However, even with a substantial amount of experimental data supported by some prior knowledge, existing inference methods often focus on a small sample of admissible candidate models only.\r\n\r\nResults: We propose Boolean network sketches as a new formal instrument for the inference of Boolean networks. A sketch integrates (typically partial) knowledge about the network’s topology and the update logic (obtained through, e.g. a biological knowledge base or a literature search), as well as further assumptions about the properties of the network’s transitions (e.g. the form of its attractor landscape), and additional restrictions on the model dynamics given by the measured experimental data. Our new BNs inference algorithm starts with an ‘initial’ sketch, which is extended by adding restrictions representing experimental data to a ‘data-informed’ sketch and subsequently computes all BNs consistent with the data-informed sketch. Our algorithm is based on a symbolic representation and coloured model-checking. Our approach is unique in its ability to cover a broad spectrum of knowledge and efficiently produce a compact representation of all inferred BNs. We evaluate the method on a non-trivial collection of real-world and simulated data."}],"citation":{"ieee":"N. Beneš, L. Brim, O. Huvar, S. Pastva, and D. Šafránek, “Boolean network sketches: A unifying framework for logical model inference,” <i>Bioinformatics</i>, vol. 39, no. 4. Oxford Academic, 2023.","mla":"Beneš, Nikola, et al. “Boolean Network Sketches: A Unifying Framework for Logical Model Inference.” <i>Bioinformatics</i>, vol. 39, no. 4, btad158, Oxford Academic, 2023, doi:<a href=\"https://doi.org/10.1093/bioinformatics/btad158\">10.1093/bioinformatics/btad158</a>.","ista":"Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. 2023. Boolean network sketches: A unifying framework for logical model inference. Bioinformatics. 39(4), btad158.","ama":"Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. Boolean network sketches: A unifying framework for logical model inference. <i>Bioinformatics</i>. 2023;39(4). doi:<a href=\"https://doi.org/10.1093/bioinformatics/btad158\">10.1093/bioinformatics/btad158</a>","apa":"Beneš, N., Brim, L., Huvar, O., Pastva, S., &#38; Šafránek, D. (2023). Boolean network sketches: A unifying framework for logical model inference. <i>Bioinformatics</i>. Oxford Academic. <a href=\"https://doi.org/10.1093/bioinformatics/btad158\">https://doi.org/10.1093/bioinformatics/btad158</a>","chicago":"Beneš, Nikola, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek. “Boolean Network Sketches: A Unifying Framework for Logical Model Inference.” <i>Bioinformatics</i>. Oxford Academic, 2023. <a href=\"https://doi.org/10.1093/bioinformatics/btad158\">https://doi.org/10.1093/bioinformatics/btad158</a>.","short":"N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, Bioinformatics 39 (2023)."},"isi":1,"day":"03","scopus_import":"1","related_material":{"link":[{"relation":"software","url":"https://doi.org/10.5281/zenodo.7688740"}]},"has_accepted_license":"1","oa_version":"Published Version","author":[{"full_name":"Beneš, Nikola","last_name":"Beneš","first_name":"Nikola"},{"full_name":"Brim, Luboš","last_name":"Brim","first_name":"Luboš"},{"last_name":"Huvar","full_name":"Huvar, Ondřej","first_name":"Ondřej"},{"full_name":"Pastva, Samuel","last_name":"Pastva","first_name":"Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b"},{"first_name":"David","last_name":"Šafránek","full_name":"Šafránek, David"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"department":[{"_id":"ToHe"}],"ec_funded":1,"file":[{"file_name":"2023_Bioinformatics_Benes.pdf","date_updated":"2023-05-02T07:39:04Z","success":1,"access_level":"open_access","content_type":"application/pdf","checksum":"2cb90ddf781baefddf47eac4b54e2a03","date_created":"2023-05-02T07:39:04Z","relation":"main_file","file_id":"12886","creator":"dernst","file_size":478740}],"type":"journal_article","issue":"4","publication_identifier":{"eissn":["1367-4811"]},"file_date_updated":"2023-05-02T07:39:04Z","language":[{"iso":"eng"}],"intvolume":"        39","publication":"Bioinformatics","oa":1,"quality_controlled":"1","publication_status":"published","month":"04","external_id":{"isi":["000976610800001"],"pmid":["37004199"]},"date_published":"2023-04-03T00:00:00Z","doi":"10.1093/bioinformatics/btad158","_id":"12876"},{"alternative_title":["LNCS"],"type":"conference","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308192"]},"language":[{"iso":"eng"}],"file_date_updated":"2023-06-19T08:43:21Z","conference":{"location":"Paris, France","end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22"},"month":"04","_id":"13141","doi":"10.1007/978-3-031-30820-8_15","date_published":"2023-04-20T00:00:00Z","publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","oa":1,"intvolume":"     13994","publication_status":"published","quality_controlled":"1","oa_version":"Published Version","author":[{"first_name":"Ashwani","last_name":"Anand","full_name":"Anand, Ashwani"},{"last_name":"Mallik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik"},{"first_name":"Satya Prakash","full_name":"Nayak, Satya Prakash","last_name":"Nayak"},{"first_name":"Anne Kathrin","full_name":"Schmuck, Anne Kathrin","last_name":"Schmuck"}],"department":[{"_id":"ToHe"}],"file":[{"date_updated":"2023-06-19T08:43:21Z","file_name":"2023_LNCS_Anand.pdf","success":1,"content_type":"application/pdf","checksum":"60dcafc1b4f6f070be43bad3fe877974","access_level":"open_access","creator":"dernst","file_size":521425,"date_created":"2023-06-19T08:43:21Z","file_id":"13151","relation":"main_file"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"citation":{"apa":"Anand, A., Mallik, K., Nayak, S. P., &#38; Schmuck, A. K. (2023). Computing adequately permissive assumptions for synthesis. In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13994, pp. 211–228). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">https://doi.org/10.1007/978-3-031-30820-8_15</a>","ama":"Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions for synthesis. In: <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13994. Springer Nature; 2023:211-228. doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">10.1007/978-3-031-30820-8_15</a>","chicago":"Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, 13994:211–28. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">https://doi.org/10.1007/978-3-031-30820-8_15</a>.","ista":"Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 211–228.","short":"A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 211–228.","ieee":"A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately permissive assumptions for synthesis,” in <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, Paris, France, 2023, vol. 13994, pp. 211–228.","mla":"Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.” <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13994, Springer Nature, 2023, pp. 211–28, doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">10.1007/978-3-031-30820-8_15</a>."},"day":"20","abstract":[{"lang":"eng","text":"We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an ω-regular winning condition Φ for the system player, we compute an ω-regular assumption Ψ for the environment player, such that (i) every environment strategy compliant with Ψ allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ψ does not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games, which are canonical representations of ω-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches—both theoretically and empirically. To the best of our knowledge, for ω\r\n-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive."}],"scopus_import":"1","has_accepted_license":"1","year":"2023","date_created":"2023-06-18T22:00:47Z","volume":13994,"status":"public","page":"211-228","article_processing_charge":"No","title":"Computing adequately permissive assumptions for synthesis","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-06-19T08:49:46Z","publisher":"Springer Nature","ddc":["000"]},{"abstract":[{"lang":"eng","text":"Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions."}],"day":"22","citation":{"apa":"Chatterjee, K., Henzinger, T. A., Lechner, M., &#38; Zikelic, D. (2023). A learner-verifier framework for neural network controllers and certificates of stochastic systems. In <i>Tools and Algorithms for the Construction and Analysis of Systems </i> (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">https://doi.org/10.1007/978-3-031-30823-9_1</a>","ama":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: <i>Tools and Algorithms for the Construction and Analysis of Systems </i>. Vol 13993. Springer Nature; 2023:3-25. doi:<a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">10.1007/978-3-031-30823-9_1</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Mathias Lechner, and Dorde Zikelic. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” In <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, 13993:3–25. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">https://doi.org/10.1007/978-3-031-30823-9_1</a>.","ista":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier framework for neural network controllers and certificates of stochastic systems. Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 3–25.","short":"K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2023, pp. 3–25.","ieee":"K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “A learner-verifier framework for neural network controllers and certificates of stochastic systems,” in <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, Paris, France, 2023, vol. 13993, pp. 3–25.","mla":"Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, vol. 13993, Springer Nature, 2023, pp. 3–25, doi:<a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">10.1007/978-3-031-30823-9_1</a>."},"has_accepted_license":"1","scopus_import":"1","page":"3-25","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"status":"public","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","volume":13993,"year":"2023","date_created":"2023-06-18T22:00:47Z","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-07-14T09:09:52Z","publisher":"Springer Nature","article_processing_charge":"No","title":"A learner-verifier framework for neural network controllers and certificates of stochastic systems","publication_identifier":{"isbn":["9783031308222"],"eissn":["1611-3349"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"file_date_updated":"2023-06-19T08:29:30Z","type":"conference","alternative_title":["LNCS"],"publication_status":"published","quality_controlled":"1","publication":"Tools and Algorithms for the Construction and Analysis of Systems ","oa":1,"intvolume":"     13993","_id":"13142","doi":"10.1007/978-3-031-30823-9_1","date_published":"2023-04-22T00:00:00Z","conference":{"start_date":"2023-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Paris, France","end_date":"2023-04-27"},"month":"04","oa_version":"Published Version","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"},{"full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"file":[{"file_name":"2023_LNCS_Chatterjee.pdf","date_updated":"2023-06-19T08:29:30Z","content_type":"application/pdf","access_level":"open_access","checksum":"3d8a8bb24d211bc83360dfc2fd744307","success":1,"file_size":528455,"creator":"dernst","relation":"main_file","date_created":"2023-06-19T08:29:30Z","file_id":"13150"}],"ec_funded":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}]},{"article_processing_charge":"No","title":"Safety and liveness of quantitative automata","article_number":"17","date_updated":"2023-10-09T07:14:03Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"year":"2023","date_created":"2023-07-14T10:00:15Z","acknowledgement":"We thank Christof Löding for pointing us to some results on PSpace-hardess of universality problems and the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093 and the Israel Science Foundation grant 2410/22.","volume":279,"project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"status":"public","has_accepted_license":"1","citation":{"mla":"Boker, Udi, et al. “Safety and Liveness of Quantitative Automata.” <i>34th International Conference on Concurrency Theory</i>, vol. 279, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">10.4230/LIPIcs.CONCUR.2023.17</a>.","ieee":"U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Safety and liveness of quantitative automata,” in <i>34th International Conference on Concurrency Theory</i>, Antwerp, Belgium, 2023, vol. 279.","short":"U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 34th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.","chicago":"Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Safety and Liveness of Quantitative Automata.” In <i>34th International Conference on Concurrency Theory</i>, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.17</a>.","ista":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Safety and liveness of quantitative automata. 34th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 279, 17.","apa":"Boker, U., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Safety and liveness of quantitative automata. In <i>34th International Conference on Concurrency Theory</i> (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.17</a>","ama":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative automata. In: <i>34th International Conference on Concurrency Theory</i>. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">10.4230/LIPIcs.CONCUR.2023.17</a>"},"day":"01","abstract":[{"lang":"eng","text":"The safety-liveness dichotomy is a fundamental concept in formal languages which plays a key role in verification. Recently, this dichotomy has been lifted to quantitative properties, which are arbitrary functions from infinite words to partially-ordered domains. We look into harnessing the dichotomy for the specific classes of quantitative properties expressed by quantitative automata. These automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totallyordered domain of real numbers. In this automata-theoretic setting, we establish a connection between quantitative safety and topological continuity and provide an alternative characterization of quantitative safety and liveness in terms of their boolean counterparts. For all common value functions, we show how the safety closure of a quantitative automaton can be constructed in PTime, and we provide PSpace-complete checks of whether a given quantitative automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata, for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf, and LimSup automata, we give PTime decompositions into safe and live automata. These decompositions enable the separation of techniques for safety and liveness verification for quantitative specifications."}],"ec_funded":1,"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file":[{"date_updated":"2023-07-14T12:03:48Z","file_name":"CONCUR23.pdf","success":1,"checksum":"d40e57a04448ea5c77d7e1cfb9590a81","access_level":"open_access","content_type":"application/pdf","file_size":755529,"creator":"esarac","relation":"main_file","file_id":"13224","date_created":"2023-07-14T12:03:48Z"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"author":[{"last_name":"Boker","full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien"},{"first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E","last_name":"Sarac"}],"oa_version":"Published Version","external_id":{"arxiv":["2307.06016"]},"conference":{"start_date":"2023-09-18","name":"CONCUR: Conference on Concurrency Theory","location":"Antwerp, Belgium","end_date":"2023-09-23"},"arxiv":1,"month":"09","_id":"13221","doi":"10.4230/LIPIcs.CONCUR.2023.17","date_published":"2023-09-01T00:00:00Z","oa":1,"publication":"34th International Conference on Concurrency Theory","intvolume":"       279","publication_status":"published","quality_controlled":"1","alternative_title":["LIPIcs"],"type":"conference","file_date_updated":"2023-07-14T12:03:48Z","publication_identifier":{"isbn":["9783959772990"],"eissn":["1868-8969"]},"language":[{"iso":"eng"}]},{"type":"conference","file_date_updated":"2023-07-18T07:43:10Z","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9781450372527"]},"publication":"FAccT '23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency","oa":1,"quality_controlled":"1","publication_status":"published","month":"06","arxiv":1,"conference":{"location":"Chicago, IL, United States","end_date":"2023-06-15","start_date":"2023-06-12","name":"FAccT: Conference on Fairness, Accountability and Transparency"},"external_id":{"isi":["001062819300057"],"arxiv":["2305.04699"]},"date_published":"2023-06-12T00:00:00Z","doi":"10.1145/3593013.3594028","_id":"13228","author":[{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Mahyar","last_name":"Karimi","full_name":"Karimi, Mahyar"},{"last_name":"Kueffner","orcid":"0000-0001-8974-2542","full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","first_name":"Konstantin"},{"first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","last_name":"Mallik"}],"oa_version":"Published Version","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"department":[{"_id":"ToHe"}],"ec_funded":1,"file":[{"relation":"main_file","date_created":"2023-07-18T07:43:10Z","file_id":"13245","file_size":4100596,"creator":"dernst","date_updated":"2023-07-18T07:43:10Z","file_name":"2023_ACM_HenzingerT.pdf","success":1,"checksum":"96c759db9cdf94b81e37871a66a6ff48","access_level":"open_access","content_type":"application/pdf"}],"abstract":[{"lang":"eng","text":"A machine-learned system that is fair in static decision-making tasks may have biased societal impacts in the long-run. This may happen when the system interacts with humans and feedback patterns emerge, reinforcing old biases in the system and creating new biases. While existing works try to identify and mitigate long-run biases through smart system design, we introduce techniques for monitoring fairness in real time. Our goal is to build and deploy a monitor that will continuously observe a long sequence of events generated by the system in the wild, and will output, with each event, a verdict on how fair the system is at the current point in time. The advantages of monitoring are two-fold. Firstly, fairness is evaluated at run-time, which is important because unfair behaviors may not be eliminated a priori, at design-time, due to partial knowledge about the system and the environment, as well as uncertainties and dynamic changes in the system and the environment, such as the unpredictability of human behavior. Secondly, monitors are by design oblivious to how the monitored system is constructed, which makes them suitable to be used as trusted third-party fairness watchdogs. They function as computationally lightweight statistical estimators, and their correctness proofs rely on the rigorous analysis of the stochastic process that models the assumptions about the underlying dynamics of the system. We show, both in theory and experiments, how monitors can warn us (1) if a bank’s credit policy over time has created an unfair distribution of credit scores among the population, and (2) if a resource allocator’s allocation policy over time has made unfair allocations. Our experiments demonstrate that the monitors introduce very low overhead. We believe that runtime monitoring is an important and mathematically rigorous new addition to the fairness toolbox."}],"citation":{"mla":"Henzinger, Thomas A., et al. “Runtime Monitoring of Dynamic Fairness Properties.” <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>, Association for Computing Machinery, 2023, pp. 604–14, doi:<a href=\"https://doi.org/10.1145/3593013.3594028\">10.1145/3593013.3594028</a>.","ieee":"T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Runtime monitoring of dynamic fairness properties,” in <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>, Chicago, IL, United States, 2023, pp. 604–614.","short":"T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency, Association for Computing Machinery, 2023, pp. 604–614.","ista":"Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Runtime monitoring of dynamic fairness properties. FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency. FAccT: Conference on Fairness, Accountability and Transparency, 604–614.","apa":"Henzinger, T. A., Karimi, M., Kueffner, K., &#38; Mallik, K. (2023). Runtime monitoring of dynamic fairness properties. In <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i> (pp. 604–614). Chicago, IL, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3593013.3594028\">https://doi.org/10.1145/3593013.3594028</a>","ama":"Henzinger TA, Karimi M, Kueffner K, Mallik K. Runtime monitoring of dynamic fairness properties. In: <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>. Association for Computing Machinery; 2023:604-614. doi:<a href=\"https://doi.org/10.1145/3593013.3594028\">10.1145/3593013.3594028</a>","chicago":"Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. “Runtime Monitoring of Dynamic Fairness Properties.” In <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>, 604–14. Association for Computing Machinery, 2023. <a href=\"https://doi.org/10.1145/3593013.3594028\">https://doi.org/10.1145/3593013.3594028</a>."},"day":"12","isi":1,"scopus_import":"1","has_accepted_license":"1","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"status":"public","page":"604-614","date_created":"2023-07-16T22:01:09Z","year":"2023","acknowledgement":"The authors would like to thank the anonymous reviewers for their valuable comments and helpful suggestions. This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","date_updated":"2023-12-13T11:30:31Z","publisher":"Association for Computing Machinery","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"title":"Runtime monitoring of dynamic fairness properties","article_processing_charge":"No"},{"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark, and by the Villum Investigator Grant S4OS.","volume":25,"year":"2023","date_created":"2023-07-16T22:01:11Z","page":"575-592","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"status":"public","article_type":"original","article_processing_charge":"Yes (in subscription journal)","title":"Into the unknown: Active monitoring of neural networks (extended version)","ddc":["000"],"date_updated":"2024-01-30T12:06:57Z","publisher":"Springer Nature","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","isi":1,"day":"01","citation":{"mla":"Kueffner, Konstantin, et al. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 25, Springer Nature, 2023, pp. 575–92, doi:<a href=\"https://doi.org/10.1007/s10009-023-00711-4\">10.1007/s10009-023-00711-4</a>.","ieee":"K. Kueffner, A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: Active monitoring of neural networks (extended version),” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 25. Springer Nature, pp. 575–592, 2023.","short":"K. Kueffner, A. Lukina, C. Schilling, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 25 (2023) 575–592.","ista":"Kueffner K, Lukina A, Schilling C, Henzinger TA. 2023. Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. 25, 575–592.","ama":"Kueffner K, Lukina A, Schilling C, Henzinger TA. Into the unknown: Active monitoring of neural networks (extended version). <i>International Journal on Software Tools for Technology Transfer</i>. 2023;25:575-592. doi:<a href=\"https://doi.org/10.1007/s10009-023-00711-4\">10.1007/s10009-023-00711-4</a>","apa":"Kueffner, K., Lukina, A., Schilling, C., &#38; Henzinger, T. A. (2023). Into the unknown: Active monitoring of neural networks (extended version). <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-023-00711-4\">https://doi.org/10.1007/s10009-023-00711-4</a>","chicago":"Kueffner, Konstantin, Anna Lukina, Christian Schilling, and Thomas A Henzinger. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/s10009-023-00711-4\">https://doi.org/10.1007/s10009-023-00711-4</a>."},"abstract":[{"lang":"eng","text":"Neural-network classifiers achieve high accuracy when predicting the class of an input that they were trained to identify. Maintaining this accuracy in dynamic environments, where inputs frequently fall outside the fixed set of initially known classes, remains a challenge. We consider the problem of monitoring the classification decisions of neural networks in the presence of novel classes. For this purpose, we generalize our recently proposed abstraction-based monitor from binary output to real-valued quantitative output. This quantitative output enables new applications, two of which we investigate in the paper. As our first application, we introduce an algorithmic framework for active monitoring of a neural network, which allows us to learn new classes dynamically and yet maintain high monitoring performance. As our second application, we present an offline procedure to retrain the neural network to improve the monitor’s detection performance without deteriorating the network’s classification accuracy. Our experimental evaluation demonstrates both the benefits of our active monitoring framework in dynamic scenarios and the effectiveness of the retraining procedure."}],"has_accepted_license":"1","related_material":{"record":[{"relation":"shorter_version","id":"10206","status":"public"}]},"scopus_import":"1","author":[{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","first_name":"Konstantin","last_name":"Kueffner","full_name":"Kueffner, Konstantin","orcid":"0000-0001-8974-2542"},{"id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425","first_name":"Anna","last_name":"Lukina","full_name":"Lukina, Anna"},{"full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Published Version","file":[{"success":1,"content_type":"application/pdf","checksum":"3c4b347f39412a76872f9a6f30101f94","access_level":"open_access","date_updated":"2024-01-30T12:06:07Z","file_name":"2023_JourSoftwareTools_Kueffner.pdf","file_id":"14903","relation":"main_file","date_created":"2024-01-30T12:06:07Z","creator":"dernst","file_size":13387667}],"ec_funded":1,"department":[{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"file_date_updated":"2024-01-30T12:06:07Z","language":[{"iso":"eng"}],"type":"journal_article","_id":"13234","doi":"10.1007/s10009-023-00711-4","date_published":"2023-08-01T00:00:00Z","external_id":{"arxiv":["2009.06429"],"isi":["001020160000001"]},"arxiv":1,"month":"08","publication_status":"published","quality_controlled":"1","intvolume":"        25","oa":1,"publication":"International Journal on Software Tools for Technology Transfer"},{"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"department":[{"_id":"ToHe"}],"ec_funded":1,"file":[{"file_name":"2023_Bioinformatics_Trinh.pdf","date_updated":"2023-07-31T11:09:05Z","content_type":"application/pdf","access_level":"open_access","checksum":"ba3abe1171df1958413b7c7f957f5486","success":1,"file_id":"13335","date_created":"2023-07-31T11:09:05Z","relation":"main_file","file_size":641736,"creator":"dernst"}],"author":[{"first_name":"Van Giang","full_name":"Trinh, Van Giang","last_name":"Trinh"},{"last_name":"Benhamou","full_name":"Benhamou, Belaid","first_name":"Belaid"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","first_name":"Samuel","last_name":"Pastva","orcid":"0000-0003-1993-0331","full_name":"Pastva, Samuel"}],"oa_version":"Published Version","oa":1,"intvolume":"        39","publication":"Bioinformatics","quality_controlled":"1","publication_status":"published","month":"06","external_id":{"isi":["001027457000060"],"pmid":["37387165"]},"date_published":"2023-06-30T00:00:00Z","doi":"10.1093/bioinformatics/btad262","_id":"13263","type":"journal_article","issue":"Supplement_1","language":[{"iso":"eng"}],"file_date_updated":"2023-07-31T11:09:05Z","publication_identifier":{"issn":["1367-4803"],"eissn":["1367-4811"]},"publisher":"Oxford Academic","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-12-13T11:41:52Z","ddc":["000"],"title":"Trap spaces of multi-valued networks: Definition, computation, and applications","pmid":1,"article_processing_charge":"Yes","article_type":"original","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020"}],"status":"public","page":"i513-i522","date_created":"2023-07-23T22:01:12Z","year":"2023","volume":39,"acknowledgement":"This work was supported by L’Institut Carnot STAR, Marseille, France, and by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. [101034413].","scopus_import":"1","related_material":{"link":[{"url":"https://github.com/giang-trinh/trap-mvn","relation":"software"}]},"has_accepted_license":"1","abstract":[{"text":"Motivation: Boolean networks are simple but efficient mathematical formalism for modelling complex biological systems. However, having only two levels of activation is sometimes not enough to fully capture the dynamics of real-world biological systems. Hence, the need for multi-valued networks (MVNs), a generalization of Boolean networks. Despite the importance of MVNs for modelling biological systems, only limited progress has been made on developing theories, analysis methods, and tools that can support them. In particular, the recent use of trap spaces in Boolean networks made a great impact on the field of systems biology, but there has been no similar concept defined and studied for MVNs to date.\r\n\r\nResults: In this work, we generalize the concept of trap spaces in Boolean networks to that in MVNs. We then develop the theory and the analysis methods for trap spaces in MVNs. In particular, we implement all proposed methods in a Python package called trapmvn. Not only showing the applicability of our approach via a realistic case study, we also evaluate the time efficiency of the method on a large collection of real-world models. The experimental results confirm the time efficiency, which we believe enables more accurate analysis on larger and more complex multi-valued models.","lang":"eng"}],"citation":{"ieee":"V. G. Trinh, B. Benhamou, T. A. Henzinger, and S. Pastva, “Trap spaces of multi-valued networks: Definition, computation, and applications,” <i>Bioinformatics</i>, vol. 39, no. Supplement_1. Oxford Academic, pp. i513–i522, 2023.","mla":"Trinh, Van Giang, et al. “Trap Spaces of Multi-Valued Networks: Definition, Computation, and Applications.” <i>Bioinformatics</i>, vol. 39, no. Supplement_1, Oxford Academic, 2023, pp. i513–22, doi:<a href=\"https://doi.org/10.1093/bioinformatics/btad262\">10.1093/bioinformatics/btad262</a>.","ista":"Trinh VG, Benhamou B, Henzinger TA, Pastva S. 2023. Trap spaces of multi-valued networks: Definition, computation, and applications. Bioinformatics. 39(Supplement_1), i513–i522.","ama":"Trinh VG, Benhamou B, Henzinger TA, Pastva S. Trap spaces of multi-valued networks: Definition, computation, and applications. <i>Bioinformatics</i>. 2023;39(Supplement_1):i513-i522. doi:<a href=\"https://doi.org/10.1093/bioinformatics/btad262\">10.1093/bioinformatics/btad262</a>","apa":"Trinh, V. G., Benhamou, B., Henzinger, T. A., &#38; Pastva, S. (2023). Trap spaces of multi-valued networks: Definition, computation, and applications. <i>Bioinformatics</i>. Oxford Academic. <a href=\"https://doi.org/10.1093/bioinformatics/btad262\">https://doi.org/10.1093/bioinformatics/btad262</a>","chicago":"Trinh, Van Giang, Belaid Benhamou, Thomas A Henzinger, and Samuel Pastva. “Trap Spaces of Multi-Valued Networks: Definition, Computation, and Applications.” <i>Bioinformatics</i>. Oxford Academic, 2023. <a href=\"https://doi.org/10.1093/bioinformatics/btad262\">https://doi.org/10.1093/bioinformatics/btad262</a>.","short":"V.G. Trinh, B. Benhamou, T.A. Henzinger, S. Pastva, Bioinformatics 39 (2023) i513–i522."},"isi":1,"day":"30"},{"citation":{"short":"T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 50th International Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20.","ista":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2023. Regular methods for operator precedence languages. 50th International Colloquium on Automata, Languages, and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LIPIcs, vol. 261, 129:1--129:20.","ama":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator precedence languages. In: <i>50th International Colloquium on Automata, Languages, and Programming</i>. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023:129:1--129:20. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">10.4230/LIPIcs.ICALP.2023.129</a>","apa":"Henzinger, T. A., Kebis, P., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Regular methods for operator precedence languages. In <i>50th International Colloquium on Automata, Languages, and Programming</i> (Vol. 261, p. 129:1--129:20). Paderborn, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">https://doi.org/10.4230/LIPIcs.ICALP.2023.129</a>","chicago":"Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Regular Methods for Operator Precedence Languages.” In <i>50th International Colloquium on Automata, Languages, and Programming</i>, 261:129:1--129:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">https://doi.org/10.4230/LIPIcs.ICALP.2023.129</a>.","mla":"Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.” <i>50th International Colloquium on Automata, Languages, and Programming</i>, vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">10.4230/LIPIcs.ICALP.2023.129</a>.","ieee":"T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods for operator precedence languages,” in <i>50th International Colloquium on Automata, Languages, and Programming</i>, Paderborn, Germany, 2023, vol. 261, p. 129:1--129:20."},"day":"05","abstract":[{"lang":"eng","text":"The operator precedence languages (OPLs) represent the largest known subclass of the context-free languages which enjoys all desirable closure and decidability properties. This includes the decidability of language inclusion, which is the ultimate verification problem. Operator precedence grammars, automata, and logics have been investigated and used, for example, to verify programs with arithmetic expressions and exceptions (both of which are deterministic pushdown but lie outside the scope of the visibly pushdown languages). In this paper, we complete the picture and give, for the first time, an algebraic characterization of the class of OPLs in the form of a syntactic congruence that has finitely many equivalence classes exactly for the operator precedence languages. This is a generalization of the celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of the consequences, we show that universality and language inclusion for nondeterministic operator precedence automata can be solved by an antichain algorithm. Antichain algorithms avoid determinization and complementation through an explicit subset construction, by leveraging a quasi-order on words, which allows the pruning of the search space for counterexample words without sacrificing completeness. Antichain algorithms can be implemented symbolically, and these implementations are today the best-performing algorithms in practice for the inclusion of finite automata. We give a generic construction of the quasi-order needed for antichain algorithms from a finite syntactic congruence. This yields the first antichain algorithm for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem for OPLs in exponential time."}],"has_accepted_license":"1","year":"2023","date_created":"2023-07-24T15:11:41Z","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe thank Pierre Ganty for early discussions and the anonymous reviewers for their helpful comments.\r\n","volume":261,"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"status":"public","page":"129:1--129:20","article_processing_charge":"Yes","title":"Regular methods for operator precedence languages","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2023-07-31T08:38:38Z","ddc":["000"],"alternative_title":["LIPIcs"],"type":"conference","language":[{"iso":"eng"}],"file_date_updated":"2023-07-24T15:11:05Z","publication_identifier":{"eissn":["1868-8969"],"isbn":["9783959772785"]},"external_id":{"arxiv":["2305.03447"]},"arxiv":1,"conference":{"start_date":"2023-07-10","name":"ICALP: International Colloquium on Automata, Languages, and Programming","end_date":"2023-07-14","location":"Paderborn, Germany"},"month":"07","_id":"13292","doi":"10.4230/LIPIcs.ICALP.2023.129","date_published":"2023-07-05T00:00:00Z","intvolume":"       261","publication":"50th International Colloquium on Automata, Languages, and Programming","oa":1,"publication_status":"published","quality_controlled":"1","oa_version":"Published Version","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"},{"first_name":"Pavol","full_name":"Kebis, Pavol","last_name":"Kebis"},{"first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E"}],"ec_funded":1,"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file":[{"file_id":"13293","date_created":"2023-07-24T15:11:05Z","relation":"main_file","creator":"esarac","file_size":859379,"success":1,"checksum":"5d4c8932ef3450615a53b9bb15d92eb2","access_level":"open_access","content_type":"application/pdf","date_updated":"2023-07-24T15:11:05Z","file_name":"icalp23.pdf"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"}},{"article_processing_charge":"Yes (in subscription journal)","title":"Monitoring algorithmic fairness","publisher":"Springer Nature","date_updated":"2023-09-05T15:14:00Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","ddc":["000"],"year":"2023","date_created":"2023-07-25T18:32:40Z","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG101020093.","volume":13965,"status":"public","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"page":"358–382","has_accepted_license":"1","citation":{"ieee":"T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness,” in <i>Computer Aided Verification</i>, Paris, France, 2023, vol. 13965, pp. 358–382.","mla":"Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness.” <i>Computer Aided Verification</i>, vol. 13965, Springer Nature, 2023, pp. 358–382, doi:<a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">10.1007/978-3-031-37703-7_17</a>.","ista":"Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness. Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13965, 358–382.","apa":"Henzinger, T. A., Karimi, M., Kueffner, K., &#38; Mallik, K. (2023). Monitoring algorithmic fairness. In <i>Computer Aided Verification</i> (Vol. 13965, pp. 358–382). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">https://doi.org/10.1007/978-3-031-37703-7_17</a>","chicago":"Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. “Monitoring Algorithmic Fairness.” In <i>Computer Aided Verification</i>, 13965:358–382. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">https://doi.org/10.1007/978-3-031-37703-7_17</a>.","ama":"Henzinger TA, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness. In: <i>Computer Aided Verification</i>. Vol 13965. Springer Nature; 2023:358–382. doi:<a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">10.1007/978-3-031-37703-7_17</a>","short":"T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification, Springer Nature, 2023, pp. 358–382."},"day":"18","abstract":[{"text":"Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. Our monitors are of two types, and use, respectively, frequentist and Bayesian statistical inference techniques. While the frequentist monitors compute estimates that are objectively correct with respect to the ground truth, the Bayesian monitors compute estimates that are correct subject to a given prior belief about the system’s model. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. Although they exhibit different theoretical complexities in certain cases, in our experiments, both frequentist and Bayesian monitors took less than a millisecond to update their verdicts after each observation.","lang":"eng"}],"ec_funded":1,"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file":[{"success":1,"access_level":"open_access","checksum":"ccaf94bf7d658ba012c016e11869b54c","content_type":"application/pdf","date_updated":"2023-07-31T08:11:20Z","file_name":"2023_LNCS_CAV_HenzingerT.pdf","creator":"dernst","file_size":647760,"date_created":"2023-07-31T08:11:20Z","file_id":"13327","relation":"main_file"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"oa_version":"Published Version","author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Karimi, Mahyar","orcid":"0009-0005-0820-1696","last_name":"Karimi","first_name":"Mahyar","id":"f1dedef5-2f78-11ee-989a-c4c97bccf506"},{"last_name":"Kueffner","orcid":"0000-0001-8974-2542","full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","first_name":"Konstantin"},{"full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","last_name":"Mallik","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"}],"conference":{"end_date":"2023-07-22","location":"Paris, France","start_date":"2023-07-17","name":"CAV: Computer Aided Verification"},"external_id":{"arxiv":["2305.15979"]},"arxiv":1,"month":"07","_id":"13310","doi":"10.1007/978-3-031-37703-7_17","date_published":"2023-07-18T00:00:00Z","publication":"Computer Aided Verification","intvolume":"     13965","oa":1,"publication_status":"published","quality_controlled":"1","alternative_title":["LNCS"],"type":"conference","file_date_updated":"2023-07-31T08:11:20Z","language":[{"iso":"eng"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031377037"],"isbn":["9783031377020"]}},{"month":"06","external_id":{"arxiv":["2210.05308"]},"conference":{"start_date":"2023-02-07","name":"AAAI: Conference on Artificial Intelligence","end_date":"2023-02-14","location":"Washington, DC, United States"},"arxiv":1,"date_published":"2023-06-26T00:00:00Z","doi":"10.1609/aaai.v37i10.26407","_id":"14830","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","intvolume":"        37","quality_controlled":"1","publication_status":"published","type":"conference","issue":"10","keyword":["General Medicine"],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"ec_funded":1,"author":[{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Preprint","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"14600"}]},"citation":{"ieee":"D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 10, pp. 11926–11935.","mla":"Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 10, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–35, doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>.","chicago":"Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:11926–35. Association for the Advancement of Artificial Intelligence, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>.","ista":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control policies for stochastic systems with reach-avoid guarantees. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 11926–11935.","ama":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:11926-11935. doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>","apa":"Zikelic, D., Lechner, M., Henzinger, T. A., &#38; Chatterjee, K. (2023). Learning control policies for stochastic systems with reach-avoid guarantees. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 11926–11935). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>","short":"D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–11935."},"day":"26","abstract":[{"text":"We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks.","lang":"eng"}],"title":"Learning control policies for stochastic systems with reach-avoid guarantees","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-07-14T09:10:02Z","publisher":"Association for the Advancement of Artificial Intelligence","date_created":"2024-01-18T07:44:31Z","year":"2023","volume":37,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"},{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"status":"public","page":"11926-11935"},{"ddc":["000"],"date_updated":"2024-02-05T10:21:51Z","publisher":"EPI Sciences","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_number":"4","article_processing_charge":"Yes","title":"Fast symbolic algorithms for mega-regular games under strong transition fairness","status":"public","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"article_type":"original","acknowledgement":"A previous version of this paper has appeared in TACAS 2022. Authors ordered alphabetically. T. Banerjee was interning with MPI-SWS when this research was conducted. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093.","volume":2,"year":"2023","date_created":"2024-01-31T13:40:49Z","has_accepted_license":"1","abstract":[{"lang":"eng","text":"We consider fixpoint algorithms for two-player games on graphs with $\\omega$-regular winning conditions, where the environment is constrained by a strong transition fairness assumption. Strong transition fairness is a widely occurring special case of strong fairness, which requires that any execution is strongly fair with respect to a specified set of live edges: whenever the\r\nsource vertex of a live edge is visited infinitely often along a play, the edge itself is traversed infinitely often along the play as well. We show that, surprisingly, strong transition fairness retains the algorithmic characteristics of the fixpoint algorithms for $\\omega$-regular games -- the new algorithms have the same alternation depth as the classical algorithms but invoke a new type of predecessor operator. For Rabin games with $k$ pairs, the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is independent of the number of live edges in the strong transition fairness assumption. Further, we show that GR(1) specifications with strong transition fairness assumptions can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm. In contrast, strong fairness necessarily requires increasing the alternation depth depending on the number of fairness assumptions. We get symbolic algorithms for (generalized) Rabin, parity and GR(1) objectives under strong transition fairness assumptions as well as a direct symbolic algorithm for qualitative winning in stochastic\r\n$\\omega$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps, improving the state of the art. Finally, we have implemented a BDD-based synthesis engine based on our algorithm. We show on a set of synthetic and real benchmarks that our algorithm is scalable, parallelizable, and outperforms previous algorithms by orders of magnitude."}],"day":"24","citation":{"mla":"Banerjee, Tamajit, et al. “Fast Symbolic Algorithms for Mega-Regular Games under Strong Transition Fairness.” <i>TheoretiCS</i>, vol. 2, 4, EPI Sciences, 2023, doi:<a href=\"https://doi.org/10.46298/theoretics.23.4\">10.46298/theoretics.23.4</a>.","ieee":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani, “Fast symbolic algorithms for mega-regular games under strong transition fairness,” <i>TheoretiCS</i>, vol. 2. EPI Sciences, 2023.","short":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, TheoretiCS 2 (2023).","ama":"Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. Fast symbolic algorithms for mega-regular games under strong transition fairness. <i>TheoretiCS</i>. 2023;2. doi:<a href=\"https://doi.org/10.46298/theoretics.23.4\">10.46298/theoretics.23.4</a>","chicago":"Banerjee, Tamajit, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, and Sadegh Soudjani. “Fast Symbolic Algorithms for Mega-Regular Games under Strong Transition Fairness.” <i>TheoretiCS</i>. EPI Sciences, 2023. <a href=\"https://doi.org/10.46298/theoretics.23.4\">https://doi.org/10.46298/theoretics.23.4</a>.","apa":"Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., &#38; Soudjani, S. (2023). Fast symbolic algorithms for mega-regular games under strong transition fairness. <i>TheoretiCS</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/theoretics.23.4\">https://doi.org/10.46298/theoretics.23.4</a>","ista":"Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. 2023. Fast symbolic algorithms for mega-regular games under strong transition fairness. TheoretiCS. 2, 4."},"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"file":[{"content_type":"application/pdf","access_level":"open_access","checksum":"2972d531122a6f15727b396110fb3f5c","success":1,"date_updated":"2024-02-05T10:19:35Z","file_name":"2023_TheoretiCS_Banerjee.pdf","relation":"main_file","file_id":"14940","date_created":"2024-02-05T10:19:35Z","file_size":917076,"creator":"dernst"}],"ec_funded":1,"department":[{"_id":"ToHe"}],"oa_version":"Published Version","author":[{"first_name":"Tamajit","last_name":"Banerjee","full_name":"Banerjee, Tamajit"},{"first_name":"Rupak","last_name":"Majumdar","full_name":"Majumdar, Rupak"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik"},{"last_name":"Schmuck","full_name":"Schmuck, Anne-Kathrin","first_name":"Anne-Kathrin"},{"last_name":"Soudjani","full_name":"Soudjani, Sadegh","first_name":"Sadegh"}],"publication_status":"published","quality_controlled":"1","intvolume":"         2","publication":"TheoretiCS","oa":1,"_id":"14920","doi":"10.46298/theoretics.23.4","date_published":"2023-02-24T00:00:00Z","external_id":{"arxiv":["2202.07480"]},"arxiv":1,"month":"02","file_date_updated":"2024-02-05T10:19:35Z","language":[{"iso":"eng"}],"publication_identifier":{"issn":["2751-4838"]},"type":"journal_article"},{"type":"research_data_reference","abstract":[{"text":"This resource contains the artifacts for reproducing the experimental results presented in the paper titled \"A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties\" that has been submitted in CAV 2023.","lang":"eng"}],"day":"28","citation":{"ama":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 2023. doi:<a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>","ista":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>.","apa":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., &#38; Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.7877790\">https://doi.org/10.5281/ZENODO.7877790</a>","chicago":"Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.7877790\">https://doi.org/10.5281/ZENODO.7877790</a>.","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, (2023).","ieee":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties.” Zenodo, 2023.","mla":"Majumdar, Rupak, et al. <i>A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties</i>. Zenodo, 2023, doi:<a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>."},"oa":1,"date_published":"2023-04-28T00:00:00Z","related_material":{"record":[{"relation":"used_in_publication","id":"14758","status":"public"}]},"doi":"10.5281/ZENODO.7877790","has_accepted_license":"1","_id":"14994","month":"04","main_file_link":[{"url":"https://doi.org/10.5281/zenodo.7877790","open_access":"1"}],"author":[{"last_name":"Majumdar","full_name":"Majumdar, Rupak","first_name":"Rupak"},{"last_name":"Mallik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik"},{"last_name":"Rychlicki","full_name":"Rychlicki, Mateusz","first_name":"Mateusz"},{"first_name":"Anne-Kathrin","full_name":"Schmuck, Anne-Kathrin","last_name":"Schmuck"},{"first_name":"Sadegh","last_name":"Soudjani","full_name":"Soudjani, Sadegh"}],"oa_version":"Published Version","status":"public","date_created":"2024-02-14T15:13:00Z","year":"2023","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Zenodo","date_updated":"2024-02-27T07:39:51Z","title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","department":[{"_id":"ToHe"}],"article_processing_charge":"No"},{"day":"15","citation":{"ieee":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger, “Compositional policy learning in stochastic control systems with formal guarantees,” in <i>37th Conference on Neural Information Processing Systems</i>, New Orleans, LO, United States, 2023.","mla":"Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” <i>37th Conference on Neural Information Processing Systems</i>, 2023.","ista":"Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional policy learning in stochastic control systems with formal guarantees. 37th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems.","ama":"Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. Compositional policy learning in stochastic control systems with formal guarantees. In: <i>37th Conference on Neural Information Processing Systems</i>. ; 2023.","chicago":"Zikelic, Dorde, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A Henzinger. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” In <i>37th Conference on Neural Information Processing Systems</i>, 2023.","apa":"Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., &#38; Henzinger, T. A. (2023). Compositional policy learning in stochastic control systems with formal guarantees. In <i>37th Conference on Neural Information Processing Systems</i>. New Orleans, LO, United States.","short":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th Conference on Neural Information Processing Systems, 2023."},"language":[{"iso":"eng"}],"type":"conference","abstract":[{"lang":"eng","text":"Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph’s sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment."}],"date_published":"2023-12-15T00:00:00Z","_id":"15023","month":"12","external_id":{"arxiv":["2312.01456"]},"arxiv":1,"conference":{"location":"New Orleans, LO, United States","end_date":"2023-12-16","start_date":"2023-12-10","name":"NeurIPS: Neural Information Processing Systems"},"quality_controlled":"1","publication_status":"epub_ahead","publication":"37th Conference on Neural Information Processing Systems","oa":1,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS) and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt).","date_created":"2024-02-25T09:23:24Z","year":"2023","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2312.01456"}],"oa_version":"Preprint","author":[{"first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic"},{"full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Abhinav","id":"a235593c-d7fa-11eb-a0c5-b22ca3c66ee6","full_name":"Verma, Abhinav","last_name":"Verma"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"status":"public","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Compositional policy learning in stochastic control systems with formal guarantees","ec_funded":1,"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-07-14T09:10:04Z"},{"date_created":"2024-02-28T07:34:34Z","year":"2023","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"oa_version":"Published Version","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5281/zenodo.8191722"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"status":"public","title":"Monitoring hyperproperties with prefix transducers","department":[{"_id":"ToHe"}],"ec_funded":1,"article_processing_charge":"No","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ddc":["000"],"date_updated":"2024-02-28T12:33:09Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Zenodo","day":"28","citation":{"apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.8191723\">https://doi.org/10.5281/ZENODO.8191723</a>","ama":"Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. 2023. doi:<a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.8191723\">https://doi.org/10.5281/ZENODO.8191723</a>.","ista":"Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>.","short":"M. Chalupa, T.A. Henzinger, (2023).","ieee":"M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers.” Zenodo, 2023.","mla":"Chalupa, Marek, and Thomas A. Henzinger. <i>Monitoring Hyperproperties with Prefix Transducers</i>. Zenodo, 2023, doi:<a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>."},"type":"research_data_reference","abstract":[{"lang":"eng","text":"This artifact aims to reproduce experiments from the paper Monitoring Hyperproperties With Prefix Transducers accepted at RV'23, and give further pointers to implementation of prefix transducers.\r\nIt has two parts: a pre-compiled docker image and sources that one can use to compile (locally or in docker) the software and run the experiments."}],"doi":"10.5281/ZENODO.8191723","related_material":{"record":[{"relation":"used_in_publication","id":"14076","status":"public"}]},"date_published":"2023-07-28T00:00:00Z","has_accepted_license":"1","_id":"15035","month":"07","oa":1},{"alternative_title":["LNCS"],"file_date_updated":"2023-10-16T07:15:11Z","language":[{"iso":"eng"}],"publication_identifier":{"eisbn":["978-3-031-44267-4"],"isbn":["978-3-031-44266-7"]},"type":"conference","doi":"10.1007/978-3-031-44267-4_9","date_published":"2023-10-01T00:00:00Z","_id":"14076","month":"10","conference":{"location":"Thessaloniki, Greek","end_date":"2023-10-07","name":"RV: Conference on Runtime Verification","start_date":"2023-10-04"},"quality_controlled":"1","publication_status":"published","oa":1,"publication":"23nd International Conference on Runtime Verification","intvolume":"     14245","oa_version":"Published Version","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"file":[{"creator":"dernst","file_size":867256,"relation":"main_file","file_id":"14430","date_created":"2023-10-16T07:15:11Z","success":1,"content_type":"application/pdf","access_level":"open_access","checksum":"ee33bd6f1a26f4dae7a8192584869fd8","file_name":"2023_LNCS_RV_Chalupa.pdf","date_updated":"2023-10-16T07:15:11Z"}],"department":[{"_id":"ToHe"}],"ec_funded":1,"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"day":"01","citation":{"mla":"Chalupa, Marek, and Thomas A. Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” <i>23nd International Conference on Runtime Verification</i>, vol. 14245, Springer Nature, 2023, pp. 168–90, doi:<a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">10.1007/978-3-031-44267-4_9</a>.","ieee":"M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers,” in <i>23nd International Conference on Runtime Verification</i>, Thessaloniki, Greek, 2023, vol. 14245, pp. 168–190.","short":"M. Chalupa, T.A. Henzinger, in:, 23nd International Conference on Runtime Verification, Springer Nature, 2023, pp. 168–190.","ama":"Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. In: <i>23nd International Conference on Runtime Verification</i>. Vol 14245. Springer Nature; 2023:168-190. doi:<a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">10.1007/978-3-031-44267-4_9</a>","apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. In <i>23nd International Conference on Runtime Verification</i> (Vol. 14245, pp. 168–190). Thessaloniki, Greek: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">https://doi.org/10.1007/978-3-031-44267-4_9</a>","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” In <i>23nd International Conference on Runtime Verification</i>, 14245:168–90. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">https://doi.org/10.1007/978-3-031-44267-4_9</a>.","ista":"Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers. 23nd International Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS, vol. 14245, 168–190."},"abstract":[{"text":"Hyperproperties are properties that relate multiple execution traces. Previous work on monitoring hyperproperties focused on synchronous hyperproperties, usually specified in HyperLTL. When monitoring synchronous hyperproperties, all traces are assumed to proceed at the same speed. We introduce (multi-trace) prefix transducers and show how to use them for monitoring synchronous as well as, for the first time, asynchronous hyperproperties. Prefix transducers map multiple input traces into one or more output traces by incrementally matching prefixes of the input traces against expressions similar to regular expressions. The prefixes of different traces which are consumed by a single matching step of the monitor may have different lengths. The deterministic and executable nature of prefix transducers makes them more suitable as an intermediate formalism for runtime verification than logical specifications, which tend to be highly non-deterministic, especially in the case of asynchronous hyperproperties. We report on a set of experiments about monitoring asynchronous version of observational determinism.","lang":"eng"}],"related_material":{"record":[{"relation":"research_data","id":"15035","status":"public"}]},"has_accepted_license":"1","volume":14245,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank Ana Oliveira da Costa for commenting on a draft of the paper.","date_created":"2023-08-16T20:46:08Z","year":"2023","page":"168-190","status":"public","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"title":"Monitoring hyperproperties with prefix transducers","article_processing_charge":"Yes (in subscription journal)","ddc":["000"],"date_updated":"2024-02-28T12:33:08Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature"}]