--- _id: '12854' abstract: - lang: eng 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." acknowledgement: This work was supported by the ERC-2020-AdG 10102009 grant. alternative_title: - LNCS article_processing_charge: No author: - first_name: Marek full_name: Chalupa, Marek id: 87e34708-d6c6-11ec-9f5b-9391e7be2463 last_name: Chalupa - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers. In: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13994. Springer Nature; 2023:535-540. doi:10.1007/978-3-031-30820-8_32' apa: 'Chalupa, M., & Henzinger, T. A. (2023). Bubaak: Runtime monitoring of program verifiers. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_32' chicago: 'Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” In Tools and Algorithms for the Construction and Analysis of Systems, 13994:535–40. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_32.' ieee: 'M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,” in Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994, pp. 535–540.' 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.' mla: 'Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” Tools and Algorithms for the Construction and Analysis of Systems, vol. 13994, Springer Nature, 2023, pp. 535–40, doi:10.1007/978-3-031-30820-8_32.' short: M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 535–540. conference: end_date: 2023-04-27 location: Paris, France name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2023-04-22 date_created: 2023-04-20T08:22:53Z date_published: 2023-04-20T00:00:00Z date_updated: 2023-04-25T07:02:43Z day: '20' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-031-30820-8_32 ec_funded: 1 file: - access_level: open_access checksum: 120d2c2a38384058ad0630fdf8288312 content_type: application/pdf creator: dernst date_created: 2023-04-25T06:58:36Z date_updated: 2023-04-25T06:58:36Z file_id: '12864' file_name: 2023_LNCS_Chalupa.pdf file_size: 16096413 relation: main_file success: 1 file_date_updated: 2023-04-25T06:58:36Z has_accepted_license: '1' intvolume: ' 13994' language: - iso: eng license: https://creativecommons.org/licenses/by/4.0/ month: '04' oa: 1 oa_version: Published Version page: 535-540 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: Tools and Algorithms for the Construction and Analysis of Systems publication_identifier: eisbn: - '9783031308208' eissn: - 1611-3349 isbn: - '9783031308192' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' status: public title: 'Bubaak: Runtime monitoring of program verifiers' tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13994 year: '2023' ... --- _id: '12856' 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." 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. alternative_title: - LNCS article_processing_charge: No author: - first_name: Marek full_name: Chalupa, Marek id: 87e34708-d6c6-11ec-9f5b-9391e7be2463 last_name: Chalupa - first_name: Fabian full_name: Mühlböck, Fabian id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425 last_name: Mühlböck orcid: 0000-0003-1548-0177 - first_name: Stefanie full_name: Muroya Lei, Stefanie id: a376de31-8972-11ed-ae7b-d0251c13c8ff last_name: Muroya Lei - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort third-party monitoring. In: Fundamental Approaches to Software Engineering. Vol 13991. Springer Nature; 2023:260-281. doi:10.1007/978-3-031-30826-0_15' apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023). Vamos: Middleware for best-effort third-party monitoring. In Fundamental Approaches to Software Engineering (Vol. 13991, pp. 260–281). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30826-0_15' chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” In Fundamental Approaches to Software Engineering, 13991:260–81. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30826-0_15.' ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware for best-effort third-party monitoring,” in Fundamental Approaches to Software Engineering, Paris, France, 2023, vol. 13991, 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.' mla: 'Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” Fundamental Approaches to Software Engineering, vol. 13991, Springer Nature, 2023, pp. 260–81, doi:10.1007/978-3-031-30826-0_15.' 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. conference: end_date: 2023-04-27 location: Paris, France name: 'FASE: Fundamental Approaches to Software Engineering' start_date: 2023-04-22 date_created: 2023-04-20T08:29:42Z date_published: 2023-04-20T00:00:00Z date_updated: 2023-04-25T07:19:07Z day: '20' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-031-30826-0_15 ec_funded: 1 file: - access_level: open_access checksum: 17a7c8e08be609cf2408d37ea55e322c content_type: application/pdf creator: dernst date_created: 2023-04-25T07:16:36Z date_updated: 2023-04-25T07:16:36Z file_id: '12865' file_name: 2023_LNCS_ChalupaM.pdf file_size: 580828 relation: main_file success: 1 file_date_updated: 2023-04-25T07:16:36Z has_accepted_license: '1' intvolume: ' 13991' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: 260-281 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: Fundamental Approaches to Software Engineering publication_identifier: eisbn: - '9783031308260' eissn: - 1611-3349 isbn: - '9783031308253' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '12407' relation: earlier_version status: public status: public title: 'Vamos: Middleware for best-effort third-party monitoring' tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13991 year: '2023' ... --- _id: '12407' 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\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." 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." alternative_title: - IST Austria Technical Report article_processing_charge: No author: - first_name: Marek full_name: Chalupa, Marek id: 87e34708-d6c6-11ec-9f5b-9391e7be2463 last_name: Chalupa - first_name: Fabian full_name: Mühlböck, Fabian id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425 last_name: Mühlböck orcid: 0000-0003-1548-0177 - first_name: Stefanie full_name: Muroya Lei, Stefanie id: a376de31-8972-11ed-ae7b-d0251c13c8ff last_name: Muroya Lei - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria; 2023. doi:10.15479/AT:ISTA:12407' apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023). VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:12407' chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria, 2023. https://doi.org/10.15479/AT:ISTA:12407.' ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria, 2023.' 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.' mla: 'Chalupa, Marek, et al. VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria, 2023, doi:10.15479/AT:ISTA:12407.' 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.' date_created: 2023-01-27T03:18:08Z date_published: 2023-01-27T00:00:00Z date_updated: 2023-04-25T07:19:06Z day: '27' ddc: - '005' department: - _id: ToHe doi: 10.15479/AT:ISTA:12407 ec_funded: 1 file: - access_level: open_access checksum: 55426e463fdeafe9777fc3ff635154c7 content_type: application/pdf creator: fmuehlbo date_created: 2023-01-27T03:18:34Z date_updated: 2023-01-27T03:18:34Z file_id: '12408' file_name: main.pdf file_size: 662409 relation: main_file success: 1 file_date_updated: 2023-01-27T03:18:34Z has_accepted_license: '1' keyword: - runtime monitoring - best effort - third party language: - iso: eng month: '01' oa: 1 oa_version: Published Version page: '38' project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication_identifier: eissn: - 2664-1690 publication_status: published publisher: Institute of Science and Technology Austria related_material: record: - id: '12856' relation: later_version status: public status: public title: 'VAMOS: Middleware for Best-Effort Third-Party Monitoring' tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '13142' 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. 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. alternative_title: - LNCS article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic citation: ama: 'Chatterjee K, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: Tools and Algorithms for the Construction and Analysis of Systems . Vol 13993. Springer Nature; 2023:3-25. doi:10.1007/978-3-031-30823-9_1' apa: 'Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic, D. (2023). A learner-verifier framework for neural network controllers and certificates of stochastic systems. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_1' 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 Tools and Algorithms for the Construction and Analysis of Systems , 13993:3–25. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_1. 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 Tools and Algorithms for the Construction and Analysis of Systems , Paris, France, 2023, vol. 13993, pp. 3–25. 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.' mla: Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” Tools and Algorithms for the Construction and Analysis of Systems , vol. 13993, Springer Nature, 2023, pp. 3–25, doi:10.1007/978-3-031-30823-9_1. 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. conference: end_date: 2023-04-27 location: Paris, France name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2023-04-22 date_created: 2023-06-18T22:00:47Z date_published: 2023-04-22T00:00:00Z date_updated: 2023-06-19T08:30:54Z day: '22' ddc: - '000' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-031-30823-9_1 ec_funded: 1 file: - access_level: open_access checksum: 3d8a8bb24d211bc83360dfc2fd744307 content_type: application/pdf creator: dernst date_created: 2023-06-19T08:29:30Z date_updated: 2023-06-19T08:29:30Z file_id: '13150' file_name: 2023_LNCS_Chatterjee.pdf file_size: 528455 relation: main_file success: 1 file_date_updated: 2023-06-19T08:29:30Z has_accepted_license: '1' intvolume: ' 13993' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: 3-25 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 2564DBCA-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '665385' name: International IST Doctoral Program publication: 'Tools and Algorithms for the Construction and Analysis of Systems ' publication_identifier: eissn: - 1611-3349 isbn: - '9783031308222' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: A learner-verifier framework for neural network controllers and certificates of stochastic systems tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13993 year: '2023' ... --- _id: '12467' 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. acknowledgement: We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093. alternative_title: - LNCS article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Nicolas Adrien full_name: Mazzocchi, Nicolas Adrien id: b26baa86-3308-11ec-87b0-8990f34baa85 last_name: Mazzocchi - first_name: Naci E full_name: Sarac, Naci E id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425 last_name: Sarac citation: ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In: 26th International Conference Foundations of Software Science and Computation Structures. Vol 13992. Springer Nature; 2023:349-370. doi:10.1007/978-3-031-30829-1_17' apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Quantitative safety and liveness. In 26th International Conference Foundations of Software Science and Computation Structures (Vol. 13992, pp. 349–370). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30829-1_17' chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Safety and Liveness.” In 26th International Conference Foundations of Software Science and Computation Structures, 13992:349–70. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30829-1_17. ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and liveness,” in 26th International Conference Foundations of Software Science and Computation Structures, Paris, France, 2023, vol. 13992, 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.' mla: Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” 26th International Conference Foundations of Software Science and Computation Structures, vol. 13992, Springer Nature, 2023, pp. 349–70, doi:10.1007/978-3-031-30829-1_17. 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. conference: end_date: 2023-04-27 location: Paris, France name: 'FOSSACS: Foundations of Software Science and Computation Structures' start_date: 2023-04-22 date_created: 2023-01-31T07:23:56Z date_published: 2023-04-21T00:00:00Z date_updated: 2023-07-14T11:20:27Z day: '21' ddc: - '000' department: - _id: GradSch - _id: ToHe doi: 10.1007/978-3-031-30829-1_17 ec_funded: 1 external_id: arxiv: - '2301.11175' file: - access_level: open_access checksum: 981025aed580b6b27c426cb8856cf63e content_type: application/pdf creator: esarac date_created: 2023-01-31T07:22:21Z date_updated: 2023-01-31T07:22:21Z file_id: '12468' file_name: qsl.pdf file_size: 449027 relation: main_file success: 1 - access_level: open_access checksum: f16e2af1e0eb243158ab0f0fe74e7d5a content_type: application/pdf creator: dernst date_created: 2023-06-19T10:28:09Z date_updated: 2023-06-19T10:28:09Z file_id: '13153' file_name: 2023_LNCS_HenzingerT.pdf file_size: 1048171 relation: main_file success: 1 file_date_updated: 2023-06-19T10:28:09Z has_accepted_license: '1' intvolume: ' 13992' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: 349-370 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 26th International Conference Foundations of Software Science and Computation Structures publication_identifier: eissn: - 1611-3349 isbn: - '9783031308284' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Quantitative safety and liveness tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9 volume: 13992 year: '2023' ... --- _id: '13292' 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. 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" alternative_title: - LIPIcs article_processing_charge: Yes author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Pavol full_name: Kebis, Pavol last_name: Kebis - first_name: Nicolas Adrien full_name: Mazzocchi, Nicolas Adrien id: b26baa86-3308-11ec-87b0-8990f34baa85 last_name: Mazzocchi - first_name: Naci E full_name: Sarac, Naci E id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425 last_name: Sarac citation: ama: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator precedence languages. In: 50th International Colloquium on Automata, Languages, and Programming. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023:129:1--129:20. doi:10.4230/LIPIcs.ICALP.2023.129' apa: 'Henzinger, T. A., Kebis, P., Mazzocchi, N. A., & Sarac, N. E. (2023). Regular methods for operator precedence languages. In 50th International Colloquium on Automata, Languages, and Programming (Vol. 261, p. 129:1--129:20). Paderborn, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2023.129' chicago: Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Regular Methods for Operator Precedence Languages.” In 50th International Colloquium on Automata, Languages, and Programming, 261:129:1--129:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.ICALP.2023.129. ieee: T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods for operator precedence languages,” in 50th International Colloquium on Automata, Languages, and Programming, Paderborn, Germany, 2023, vol. 261, 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.' mla: Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.” 50th International Colloquium on Automata, Languages, and Programming, vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20, doi:10.4230/LIPIcs.ICALP.2023.129. 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. conference: end_date: 2023-07-14 location: Paderborn, Germany name: 'ICALP: International Colloquium on Automata, Languages, and Programming' start_date: 2023-07-10 date_created: 2023-07-24T15:11:41Z date_published: 2023-07-05T00:00:00Z date_updated: 2023-07-31T08:38:38Z day: '05' ddc: - '000' department: - _id: GradSch - _id: ToHe doi: 10.4230/LIPIcs.ICALP.2023.129 ec_funded: 1 external_id: arxiv: - '2305.03447' file: - access_level: open_access checksum: 5d4c8932ef3450615a53b9bb15d92eb2 content_type: application/pdf creator: esarac date_created: 2023-07-24T15:11:05Z date_updated: 2023-07-24T15:11:05Z file_id: '13293' file_name: icalp23.pdf file_size: 859379 relation: main_file success: 1 file_date_updated: 2023-07-24T15:11:05Z has_accepted_license: '1' intvolume: ' 261' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: 129:1--129:20 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 50th International Colloquium on Automata, Languages, and Programming publication_identifier: eissn: - 1868-8969 isbn: - '9783959772785' publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' status: public title: Regular methods for operator precedence languages tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 261 year: '2023' ... --- _id: '12704' 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. 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." article_processing_charge: No article_type: original author: - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Alexander full_name: Amini, Alexander last_name: Amini - first_name: Daniela full_name: Rus, Daniela last_name: Rus - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. IEEE Robotics and Automation Letters. 2023;8(3):1595-1602. doi:10.1109/LRA.2023.3240930 apa: Lechner, M., Amini, A., Rus, D., & Henzinger, T. A. (2023). Revisiting the adversarial robustness-accuracy tradeoff in robot learning. IEEE Robotics and Automation Letters. Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/LRA.2023.3240930 chicago: Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” IEEE Robotics and Automation Letters. Institute of Electrical and Electronics Engineers, 2023. https://doi.org/10.1109/LRA.2023.3240930. ieee: M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial robustness-accuracy tradeoff in robot learning,” IEEE Robotics and Automation Letters, vol. 8, no. 3. Institute of Electrical and Electronics Engineers, pp. 1595–1602, 2023. 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. mla: Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” IEEE Robotics and Automation Letters, vol. 8, no. 3, Institute of Electrical and Electronics Engineers, 2023, pp. 1595–602, doi:10.1109/LRA.2023.3240930. short: M. Lechner, A. Amini, D. Rus, T.A. Henzinger, IEEE Robotics and Automation Letters 8 (2023) 1595–1602. date_created: 2023-03-05T23:01:04Z date_published: 2023-03-01T00:00:00Z date_updated: 2023-08-01T13:36:50Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.1109/LRA.2023.3240930 external_id: arxiv: - '2204.07373' isi: - '000936534100012' file: - access_level: open_access checksum: 5a75dcd326ea66685de2b1aaec259e85 content_type: application/pdf creator: cchlebak date_created: 2023-03-07T12:22:23Z date_updated: 2023-03-07T12:22:23Z file_id: '12714' file_name: 2023_IEEERobAutLetters_Lechner.pdf file_size: 944052 relation: main_file success: 1 file_date_updated: 2023-03-07T12:22:23Z has_accepted_license: '1' intvolume: ' 8' isi: 1 issue: '3' language: - iso: eng month: '03' oa: 1 oa_version: Published Version page: 1595-1602 publication: IEEE Robotics and Automation Letters publication_identifier: eissn: - 2377-3766 publication_status: published publisher: Institute of Electrical and Electronics Engineers quality_controlled: '1' related_material: record: - id: '11366' relation: earlier_version status: public scopus_import: '1' status: public title: Revisiting the adversarial robustness-accuracy tradeoff in robot learning tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 volume: 8 year: '2023' ... --- _id: '14242' abstract: - lang: eng text: We study the problem of training and certifying adversarially robust quantized neural networks (QNNs). Quantization is a technique for making neural networks more efficient by running them using low-bit integer arithmetic and is therefore commonly adopted in industry. Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization, and certification of the quantized representation is necessary to guarantee robustness. In this work, we present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs. Inspired by advances in robust learning of non-quantized networks, our training algorithm computes the gradient of an abstract representation of the actual network. Unlike existing approaches, our method can handle the discrete semantics of QNNs. Based on QA-IBP, we also develop a complete verification procedure for verifying the adversarial robustness of QNNs, which is guaranteed to terminate and produce a correct answer. Compared to existing approaches, the key advantage of our verification procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate experimentally that our approach significantly outperforms existing methods and establish the new state-of-the-art for training and certifying the robustness of QNNs. 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. Research was sponsored by the United\r\nStates Air Force Research Laboratory and the United States Air Force Artificial Intelligence Accelerator and was accomplished under Cooperative Agreement Number FA8750-19-2-\r\n1000. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied,\r\nof the United States Air Force or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright\r\nnotation herein. The research was also funded in part by the AI2050 program at Schmidt Futures (Grant G-22-63172) and Capgemini SE." article_processing_charge: No author: - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Daniela full_name: Rus, Daniela last_name: Rus citation: ama: 'Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:14964-14973. doi:10.1609/aaai.v37i12.26747' apa: 'Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T. A., & Rus, D. (2023). Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In Proceedings of the 37th AAAI Conference on Artificial Intelligence (Vol. 37, pp. 14964–14973). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v37i12.26747' chicago: Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, Thomas A Henzinger, and Daniela Rus. “Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks.” In Proceedings of the 37th AAAI Conference on Artificial Intelligence, 37:14964–73. Association for the Advancement of Artificial Intelligence, 2023. https://doi.org/10.1609/aaai.v37i12.26747. ieee: M. Lechner, D. Zikelic, K. Chatterjee, T. A. Henzinger, and D. Rus, “Quantization-aware interval bound propagation for training certifiably robust quantized neural networks,” in Proceedings of the 37th AAAI Conference on Artificial Intelligence, Washington, DC, United States, 2023, vol. 37, no. 12, pp. 14964–14973. ista: 'Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. 2023. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 14964–14973.' mla: Lechner, Mathias, et al. “Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks.” Proceedings of the 37th AAAI Conference on Artificial Intelligence, vol. 37, no. 12, Association for the Advancement of Artificial Intelligence, 2023, pp. 14964–73, doi:10.1609/aaai.v37i12.26747. short: M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, D. Rus, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 14964–14973. conference: end_date: 2023-02-14 location: Washington, DC, United States name: 'AAAI: Conference on Artificial Intelligence' start_date: 2023-02-07 date_created: 2023-08-27T22:01:17Z date_published: 2023-06-26T00:00:00Z date_updated: 2023-09-05T07:06:14Z day: '26' department: - _id: ToHe - _id: KrCh doi: 10.1609/aaai.v37i12.26747 ec_funded: 1 external_id: arxiv: - '2211.16187' intvolume: ' 37' issue: '12' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2211.16187 month: '06' oa: 1 oa_version: Preprint page: 14964-14973 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 2564DBCA-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '665385' name: International IST Doctoral Program publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence publication_identifier: isbn: - '9781577358800' publication_status: published publisher: Association for the Advancement of Artificial Intelligence quality_controlled: '1' scopus_import: '1' status: public title: Quantization-aware interval bound propagation for training certifiably robust quantized neural networks type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 37 year: '2023' ... --- _id: '13310' abstract: - lang: eng 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. acknowledgement: 'This work is supported by the European Research Council under Grant No.: ERC-2020-AdG101020093.' alternative_title: - LNCS article_processing_charge: Yes (in subscription journal) author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Mahyar full_name: Karimi, Mahyar id: f1dedef5-2f78-11ee-989a-c4c97bccf506 last_name: Karimi orcid: 0009-0005-0820-1696 - first_name: Konstantin full_name: Kueffner, Konstantin id: 8121a2d0-dc85-11ea-9058-af578f3b4515 last_name: Kueffner orcid: 0000-0001-8974-2542 - first_name: Kaushik full_name: Mallik, Kaushik id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598 last_name: Mallik orcid: 0000-0001-9864-7475 citation: ama: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness. In: Computer Aided Verification. Vol 13965. Springer Nature; 2023:358–382. doi:10.1007/978-3-031-37703-7_17' apa: 'Henzinger, T. A., Karimi, M., Kueffner, K., & Mallik, K. (2023). Monitoring algorithmic fairness. In Computer Aided Verification (Vol. 13965, pp. 358–382). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37703-7_17' chicago: Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. “Monitoring Algorithmic Fairness.” In Computer Aided Verification, 13965:358–382. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37703-7_17. ieee: T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness,” in Computer Aided Verification, Paris, France, 2023, vol. 13965, pp. 358–382. 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.' mla: Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness.” Computer Aided Verification, vol. 13965, Springer Nature, 2023, pp. 358–382, doi:10.1007/978-3-031-37703-7_17. short: T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification, Springer Nature, 2023, pp. 358–382. conference: end_date: 2023-07-22 location: Paris, France name: 'CAV: Computer Aided Verification' start_date: 2023-07-17 date_created: 2023-07-25T18:32:40Z date_published: 2023-07-18T00:00:00Z date_updated: 2023-09-05T15:14:00Z day: '18' ddc: - '000' department: - _id: GradSch - _id: ToHe doi: 10.1007/978-3-031-37703-7_17 ec_funded: 1 external_id: arxiv: - '2305.15979' file: - access_level: open_access checksum: ccaf94bf7d658ba012c016e11869b54c content_type: application/pdf creator: dernst date_created: 2023-07-31T08:11:20Z date_updated: 2023-07-31T08:11:20Z file_id: '13327' file_name: 2023_LNCS_CAV_HenzingerT.pdf file_size: 647760 relation: main_file success: 1 file_date_updated: 2023-07-31T08:11:20Z has_accepted_license: '1' intvolume: ' 13965' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: 358–382 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: Computer Aided Verification publication_identifier: eisbn: - '9783031377037' eissn: - 1611-3349 isbn: - '9783031377020' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' status: public title: Monitoring algorithmic fairness tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 13965 year: '2023' ... --- _id: '13221' 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. 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. alternative_title: - LIPIcs article_number: '17' article_processing_charge: No author: - first_name: Udi full_name: Boker, Udi id: 31E297B6-F248-11E8-B48F-1D18A9856A87 last_name: Boker - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Nicolas Adrien full_name: Mazzocchi, Nicolas Adrien id: b26baa86-3308-11ec-87b0-8990f34baa85 last_name: Mazzocchi - first_name: Naci E full_name: Sarac, Naci E id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425 last_name: Sarac citation: ama: 'Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative automata. In: 34th International Conference on Concurrency Theory. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.17' apa: 'Boker, U., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Safety and liveness of quantitative automata. In 34th International Conference on Concurrency Theory (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.17' chicago: Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Safety and Liveness of Quantitative Automata.” In 34th International Conference on Concurrency Theory, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.CONCUR.2023.17. ieee: U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Safety and liveness of quantitative automata,” in 34th International Conference on Concurrency Theory, Antwerp, Belgium, 2023, vol. 279. 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.' mla: Boker, Udi, et al. “Safety and Liveness of Quantitative Automata.” 34th International Conference on Concurrency Theory, vol. 279, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:10.4230/LIPIcs.CONCUR.2023.17. 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. conference: end_date: 2023-09-23 location: Antwerp, Belgium name: 'CONCUR: Conference on Concurrency Theory' start_date: 2023-09-18 date_created: 2023-07-14T10:00:15Z date_published: 2023-09-01T00:00:00Z date_updated: 2023-10-09T07:14:03Z day: '01' ddc: - '000' department: - _id: GradSch - _id: ToHe doi: 10.4230/LIPIcs.CONCUR.2023.17 ec_funded: 1 external_id: arxiv: - '2307.06016' file: - access_level: open_access checksum: d40e57a04448ea5c77d7e1cfb9590a81 content_type: application/pdf creator: esarac date_created: 2023-07-14T12:03:48Z date_updated: 2023-07-14T12:03:48Z file_id: '13224' file_name: CONCUR23.pdf file_size: 755529 relation: main_file success: 1 file_date_updated: 2023-07-14T12:03:48Z has_accepted_license: '1' intvolume: ' 279' language: - iso: eng month: '09' oa: 1 oa_version: Published Version project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 34th International Conference on Concurrency Theory publication_identifier: eissn: - 1868-8969 isbn: - '9783959772990' publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' status: public title: Safety and liveness of quantitative automata tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 279 year: '2023' ... --- _id: '14405' abstract: - lang: eng text: We introduce hypernode automata as a new specification formalism for hyperproperties of concurrent systems. They are finite automata with nodes labeled with hypernode logic formulas and transitions labeled with actions. A hypernode logic formula specifies relations between sequences of variable values in different system executions. Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces by constraining the values and the order of value changes of each variable without correlating the timing of the changes. Different execution traces are synchronized solely through the transitions of hypernode automata. Hypernode automata naturally combine asynchronicity at the node level with synchronicity at the transition level. We show that the model-checking problem for hypernode automata is decidable over action-labeled Kripke structures, whose actions induce transitions of the specification automata. For this reason, hypernode automaton is a suitable formalism for specifying and verifying asynchronous hyperproperties, such as declassifying observational determinism in multi-threaded programs. acknowledgement: "This work was supported in part by the Austrian Science Fund (FWF) SFB project\r\nSpyCoDe F8502, by the FWF projects ZK-35 and W1255-N23, and by the ERC Advanced Grant\r\nVAMOS 101020093." alternative_title: - LIPIcs article_number: '21' article_processing_charge: Yes author: - first_name: Ezio full_name: Bartocci, Ezio last_name: Bartocci - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Ana full_name: Oliveira da Costa, Ana id: f347ec37-6676-11ee-b395-a888cb7b4fb4 last_name: Oliveira da Costa orcid: 0000-0002-8741-5799 citation: ama: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata. In: 34th International Conference on Concurrency Theory. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.21' apa: 'Bartocci, E., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A. (2023). Hypernode automata. In 34th International Conference on Concurrency Theory (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.21' chicago: Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Hypernode Automata.” In 34th International Conference on Concurrency Theory, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.CONCUR.2023.21. ieee: E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode automata,” in 34th International Conference on Concurrency Theory, Antwerp, Belgium, 2023, vol. 279. ista: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2023. Hypernode automata. 34th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 279, 21.' mla: Bartocci, Ezio, et al. “Hypernode Automata.” 34th International Conference on Concurrency Theory, vol. 279, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:10.4230/LIPIcs.CONCUR.2023.21. short: E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, 34th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. conference: end_date: 2023-09-22 location: Antwerp, Belgium name: 'CONCUR: Conference on Concurrency Theory' start_date: 2023-09-19 date_created: 2023-10-08T22:01:16Z date_published: 2023-09-01T00:00:00Z date_updated: 2023-10-09T07:43:44Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.4230/LIPIcs.CONCUR.2023.21 ec_funded: 1 external_id: arxiv: - '2305.02836' file: - access_level: open_access checksum: 215765e40454d806174ac0a223e8d6fa content_type: application/pdf creator: dernst date_created: 2023-10-09T07:42:45Z date_updated: 2023-10-09T07:42:45Z file_id: '14413' file_name: 2023_LIPcs_Bartocci.pdf file_size: 795790 relation: main_file success: 1 file_date_updated: 2023-10-09T07:42:45Z has_accepted_license: '1' intvolume: ' 279' language: - iso: eng month: '09' oa: 1 oa_version: Published Version project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 34th International Conference on Concurrency Theory publication_identifier: isbn: - '9783959772990' issn: - '18688969' publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' scopus_import: '1' status: public title: Hypernode automata tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 279 year: '2023' ... --- _id: '14454' abstract: - lang: eng text: As AI and machine-learned software are used increasingly for making decisions that affect humans, it is imperative that they remain fair and unbiased in their decisions. To complement design-time bias mitigation measures, runtime verification techniques have been introduced recently to monitor the algorithmic fairness of deployed systems. Previous monitoring techniques assume full observability of the states of the (unknown) monitored system. Moreover, they can monitor only fairness properties that are specified as arithmetic expressions over the probabilities of different events. In this work, we extend fairness monitoring to systems modeled as partially observed Markov chains (POMC), and to specifications containing arithmetic expressions over the expected values of numerical functions on event sequences. The only assumptions we make are that the underlying POMC is aperiodic and starts in the stationary distribution, with a bound on its mixing time being known. These assumptions enable us to estimate a given property for the entire distribution of possible executions of the monitored POMC, by observing only a single execution. Our monitors observe a long run of the system and, after each new observation, output updated PAC-estimates of how fair or biased the system is. The monitors are computationally lightweight and, using a prototype implementation, we demonstrate their effectiveness on several real-world examples. acknowledgement: 'This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.' alternative_title: - LNCS article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Konstantin full_name: Kueffner, Konstantin id: 8121a2d0-dc85-11ea-9058-af578f3b4515 last_name: Kueffner orcid: 0000-0001-8974-2542 - first_name: Kaushik full_name: Mallik, Kaushik id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598 last_name: Mallik orcid: 0000-0001-9864-7475 citation: ama: 'Henzinger TA, Kueffner K, Mallik K. Monitoring algorithmic fairness under partial observations. In: 23rd International Conference on Runtime Verification. Vol 14245. Springer Nature; 2023:291-311. doi:10.1007/978-3-031-44267-4_15' apa: 'Henzinger, T. A., Kueffner, K., & Mallik, K. (2023). Monitoring algorithmic fairness under partial observations. In 23rd International Conference on Runtime Verification (Vol. 14245, pp. 291–311). Thessaloniki, Greece: Springer Nature. https://doi.org/10.1007/978-3-031-44267-4_15' chicago: Henzinger, Thomas A, Konstantin Kueffner, and Kaushik Mallik. “Monitoring Algorithmic Fairness under Partial Observations.” In 23rd International Conference on Runtime Verification, 14245:291–311. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_15. ieee: T. A. Henzinger, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness under partial observations,” in 23rd International Conference on Runtime Verification, Thessaloniki, Greece, 2023, vol. 14245, pp. 291–311. ista: 'Henzinger TA, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness under partial observations. 23rd International Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS, vol. 14245, 291–311.' mla: Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness under Partial Observations.” 23rd International Conference on Runtime Verification, vol. 14245, Springer Nature, 2023, pp. 291–311, doi:10.1007/978-3-031-44267-4_15. short: T.A. Henzinger, K. Kueffner, K. Mallik, in:, 23rd International Conference on Runtime Verification, Springer Nature, 2023, pp. 291–311. conference: end_date: 2023-10-06 location: Thessaloniki, Greece name: 'RV: Conference on Runtime Verification' start_date: 2023-10-03 date_created: 2023-10-29T23:01:15Z date_published: 2023-10-01T00:00:00Z date_updated: 2023-10-31T11:48:20Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-031-44267-4_15 ec_funded: 1 external_id: arxiv: - '2308.00341' intvolume: ' 14245' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2308.00341 month: '10' oa: 1 oa_version: Preprint page: 291-311 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 23rd International Conference on Runtime Verification publication_identifier: eissn: - 1611-3349 isbn: - '9783031442667' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Monitoring algorithmic fairness under partial observations type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 14245 year: '2023' ... --- _id: '14559' abstract: - lang: eng text: We consider the problem of learning control policies in discrete-time stochastic systems which guarantee that the system stabilizes within some specified stabilization region with probability 1. Our approach is based on the novel notion of stabilizing ranking supermartingales (sRSMs) that we introduce in this work. Our sRSMs overcome the limitation of methods proposed in previous works whose applicability is restricted to systems in which the stabilizing region cannot be left once entered under any control policy. We present a learning procedure that learns a control policy together with an sRSM that formally certifies probability 1 stability, both learned as neural networks. We show that this procedure can also be adapted to formally verifying that, under a given Lipschitz continuous control policy, the stochastic system stabilizes within some stabilizing region with probability 1. Our experimental evaluation shows that our learning procedure can successfully learn provably stabilizing policies in practice. 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. alternative_title: - LNCS article_processing_charge: No author: - first_name: Matin full_name: Ansaripour, Matin last_name: Ansaripour - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 citation: ama: 'Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. Learning provably stabilizing neural controllers for discrete-time stochastic systems. In: 21st International Symposium on Automated Technology for Verification and Analysis. Vol 14215. Springer Nature; 2023:357-379. doi:10.1007/978-3-031-45329-8_17' apa: 'Ansaripour, M., Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic, D. (2023). Learning provably stabilizing neural controllers for discrete-time stochastic systems. In 21st International Symposium on Automated Technology for Verification and Analysis (Vol. 14215, pp. 357–379). Singapore, Singapore: Springer Nature. https://doi.org/10.1007/978-3-031-45329-8_17' chicago: Ansaripour, Matin, Krishnendu Chatterjee, Thomas A Henzinger, Mathias Lechner, and Dorde Zikelic. “Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems.” In 21st International Symposium on Automated Technology for Verification and Analysis, 14215:357–79. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-45329-8_17. ieee: M. Ansaripour, K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “Learning provably stabilizing neural controllers for discrete-time stochastic systems,” in 21st International Symposium on Automated Technology for Verification and Analysis, Singapore, Singapore, 2023, vol. 14215, pp. 357–379. ista: 'Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. Learning provably stabilizing neural controllers for discrete-time stochastic systems. 21st International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 14215, 357–379.' mla: Ansaripour, Matin, et al. “Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems.” 21st International Symposium on Automated Technology for Verification and Analysis, vol. 14215, Springer Nature, 2023, pp. 357–79, doi:10.1007/978-3-031-45329-8_17. short: M. Ansaripour, K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, 21st International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2023, pp. 357–379. conference: end_date: 2023-10-27 location: Singapore, Singapore name: 'ATVA: Automated Technology for Verification and Analysis' start_date: 2023-10-24 date_created: 2023-11-19T23:00:56Z date_published: 2023-10-22T00:00:00Z date_updated: 2023-11-20T08:30:20Z day: '22' department: - _id: ToHe - _id: KrCh doi: 10.1007/978-3-031-45329-8_17 ec_funded: 1 intvolume: ' 14215' language: - iso: eng month: '10' oa_version: None page: 357-379 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 2564DBCA-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '665385' name: International IST Doctoral Program publication: 21st International Symposium on Automated Technology for Verification and Analysis publication_identifier: eissn: - 1611-3349 isbn: - '9783031453281' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Learning provably stabilizing neural controllers for discrete-time stochastic systems type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 14215 year: '2023' ... --- _id: '13228' 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. 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.' article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Mahyar full_name: Karimi, Mahyar last_name: Karimi - first_name: Konstantin full_name: Kueffner, Konstantin id: 8121a2d0-dc85-11ea-9058-af578f3b4515 last_name: Kueffner orcid: 0000-0001-8974-2542 - first_name: Kaushik full_name: Mallik, Kaushik id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598 last_name: Mallik orcid: 0000-0001-9864-7475 citation: ama: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. Runtime monitoring of dynamic fairness properties. In: FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency. Association for Computing Machinery; 2023:604-614. doi:10.1145/3593013.3594028' apa: 'Henzinger, T. A., Karimi, M., Kueffner, K., & Mallik, K. (2023). Runtime monitoring of dynamic fairness properties. In FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency (pp. 604–614). Chicago, IL, United States: Association for Computing Machinery. https://doi.org/10.1145/3593013.3594028' chicago: 'Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. “Runtime Monitoring of Dynamic Fairness Properties.” In FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency, 604–14. Association for Computing Machinery, 2023. https://doi.org/10.1145/3593013.3594028.' ieee: 'T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Runtime monitoring of dynamic fairness properties,” in FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency, Chicago, IL, United States, 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.' mla: 'Henzinger, Thomas A., et al. “Runtime Monitoring of Dynamic Fairness Properties.” FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency, Association for Computing Machinery, 2023, pp. 604–14, doi:10.1145/3593013.3594028.' 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.' conference: end_date: 2023-06-15 location: Chicago, IL, United States name: 'FAccT: Conference on Fairness, Accountability and Transparency' start_date: 2023-06-12 date_created: 2023-07-16T22:01:09Z date_published: 2023-06-12T00:00:00Z date_updated: 2023-12-13T11:30:31Z day: '12' ddc: - '000' department: - _id: ToHe doi: 10.1145/3593013.3594028 ec_funded: 1 external_id: arxiv: - '2305.04699' isi: - '001062819300057' file: - access_level: open_access checksum: 96c759db9cdf94b81e37871a66a6ff48 content_type: application/pdf creator: dernst date_created: 2023-07-18T07:43:10Z date_updated: 2023-07-18T07:43:10Z file_id: '13245' file_name: 2023_ACM_HenzingerT.pdf file_size: 4100596 relation: main_file success: 1 file_date_updated: 2023-07-18T07:43:10Z has_accepted_license: '1' isi: 1 language: - iso: eng month: '06' oa: 1 oa_version: Published Version page: 604-614 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 'FAccT ''23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency' publication_identifier: isbn: - '9781450372527' publication_status: published publisher: Association for Computing Machinery quality_controlled: '1' scopus_import: '1' status: public title: Runtime monitoring of dynamic fairness properties tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '13263' abstract: - lang: eng 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." 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]. article_processing_charge: Yes article_type: original author: - first_name: Van Giang full_name: Trinh, Van Giang last_name: Trinh - first_name: Belaid full_name: Benhamou, Belaid last_name: Benhamou - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Samuel full_name: Pastva, Samuel id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b last_name: Pastva orcid: 0000-0003-1993-0331 citation: ama: 'Trinh VG, Benhamou B, Henzinger TA, Pastva S. Trap spaces of multi-valued networks: Definition, computation, and applications. Bioinformatics. 2023;39(Supplement_1):i513-i522. doi:10.1093/bioinformatics/btad262' apa: 'Trinh, V. G., Benhamou, B., Henzinger, T. A., & Pastva, S. (2023). Trap spaces of multi-valued networks: Definition, computation, and applications. Bioinformatics. Oxford Academic. https://doi.org/10.1093/bioinformatics/btad262' chicago: 'Trinh, Van Giang, Belaid Benhamou, Thomas A Henzinger, and Samuel Pastva. “Trap Spaces of Multi-Valued Networks: Definition, Computation, and Applications.” Bioinformatics. Oxford Academic, 2023. https://doi.org/10.1093/bioinformatics/btad262.' ieee: 'V. G. Trinh, B. Benhamou, T. A. Henzinger, and S. Pastva, “Trap spaces of multi-valued networks: Definition, computation, and applications,” Bioinformatics, vol. 39, no. Supplement_1. Oxford Academic, pp. i513–i522, 2023.' 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.' mla: 'Trinh, Van Giang, et al. “Trap Spaces of Multi-Valued Networks: Definition, Computation, and Applications.” Bioinformatics, vol. 39, no. Supplement_1, Oxford Academic, 2023, pp. i513–22, doi:10.1093/bioinformatics/btad262.' short: V.G. Trinh, B. Benhamou, T.A. Henzinger, S. Pastva, Bioinformatics 39 (2023) i513–i522. date_created: 2023-07-23T22:01:12Z date_published: 2023-06-30T00:00:00Z date_updated: 2023-12-13T11:41:52Z day: '30' ddc: - '000' department: - _id: ToHe doi: 10.1093/bioinformatics/btad262 ec_funded: 1 external_id: isi: - '001027457000060' pmid: - '37387165' file: - access_level: open_access checksum: ba3abe1171df1958413b7c7f957f5486 content_type: application/pdf creator: dernst date_created: 2023-07-31T11:09:05Z date_updated: 2023-07-31T11:09:05Z file_id: '13335' file_name: 2023_Bioinformatics_Trinh.pdf file_size: 641736 relation: main_file success: 1 file_date_updated: 2023-07-31T11:09:05Z has_accepted_license: '1' intvolume: ' 39' isi: 1 issue: Supplement_1 language: - iso: eng month: '06' oa: 1 oa_version: Published Version page: i513-i522 pmid: 1 project: - _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c call_identifier: H2020 grant_number: '101034413' name: 'IST-BRIDGE: International postdoctoral program' publication: Bioinformatics publication_identifier: eissn: - 1367-4811 issn: - 1367-4803 publication_status: published publisher: Oxford Academic quality_controlled: '1' related_material: link: - relation: software url: https://github.com/giang-trinh/trap-mvn scopus_import: '1' status: public title: 'Trap spaces of multi-valued networks: Definition, computation, and applications' tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 39 year: '2023' ... --- _id: '14718' abstract: - lang: eng text: 'Binary decision diagrams (BDDs) are one of the fundamental data structures in formal methods and computer science in general. However, the performance of BDD-based algorithms greatly depends on memory latency due to the reliance on large hash tables and thus, by extension, on the speed of random memory access. This hinders the full utilisation of resources available on modern CPUs, since the absolute memory latency has not improved significantly for at least a decade. In this paper, we explore several implementation techniques that improve the performance of BDD manipulation either through enhanced memory locality or by partially eliminating random memory access. On a benchmark suite of 600+ BDDs derived from real-world applications, we demonstrate runtime that is comparable or better than parallelising the same operations on eight CPU cores. ' acknowledgement: "This work was supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413 and the\r\n“VAMOS” grant ERC-2020-AdG 101020093." article_processing_charge: No author: - first_name: Samuel full_name: Pastva, Samuel id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b last_name: Pastva orcid: 0000-0003-1993-0331 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Pastva S, Henzinger TA. Binary decision diagrams on modern hardware. In: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design. TU Vienna Academic Press; 2023:122-131. doi:10.34727/2023/isbn.978-3-85448-060-0_20' apa: 'Pastva, S., & Henzinger, T. A. (2023). Binary decision diagrams on modern hardware. In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (pp. 122–131). Ames, IA, United States: TU Vienna Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20' chicago: Pastva, Samuel, and Thomas A Henzinger. “Binary Decision Diagrams on Modern Hardware.” In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, 122–31. TU Vienna Academic Press, 2023. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20. ieee: S. Pastva and T. A. Henzinger, “Binary decision diagrams on modern hardware,” in Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, Ames, IA, United States, 2023, pp. 122–131. ista: 'Pastva S, Henzinger TA. 2023. Binary decision diagrams on modern hardware. Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design. FMCAD: Conference on Formal Methods in Computer-aided design, 122–131.' mla: Pastva, Samuel, and Thomas A. Henzinger. “Binary Decision Diagrams on Modern Hardware.” Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, TU Vienna Academic Press, 2023, pp. 122–31, doi:10.34727/2023/isbn.978-3-85448-060-0_20. short: S. Pastva, T.A. Henzinger, in:, Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, TU Vienna Academic Press, 2023, pp. 122–131. conference: end_date: 2023-10-27 location: Ames, IA, United States name: 'FMCAD: Conference on Formal Methods in Computer-aided design' start_date: 2023-10-25 date_created: 2023-12-31T23:01:03Z date_published: 2023-10-01T00:00:00Z date_updated: 2024-01-02T08:16:28Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.34727/2023/isbn.978-3-85448-060-0_20 ec_funded: 1 file: - access_level: open_access checksum: 818d6e13dd508f3a04f0941081022e5d content_type: application/pdf creator: dernst date_created: 2024-01-02T08:14:23Z date_updated: 2024-01-02T08:14:23Z file_id: '14721' file_name: 2023_FMCAD_Pastva.pdf file_size: 524321 relation: main_file success: 1 file_date_updated: 2024-01-02T08:14:23Z has_accepted_license: '1' language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: 122-131 project: - _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c call_identifier: H2020 grant_number: '101034413' name: 'IST-BRIDGE: International postdoctoral program' - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design publication_identifier: isbn: - '9783854480600' publication_status: published publisher: TU Vienna Academic Press quality_controlled: '1' scopus_import: '1' status: public title: Binary decision diagrams on modern hardware tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '14830' abstract: - lang: eng 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. 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. article_processing_charge: No author: - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: 'Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:11926-11935. doi:10.1609/aaai.v37i10.26407' apa: 'Zikelic, D., Lechner, M., Henzinger, T. A., & Chatterjee, K. (2023). Learning control policies for stochastic systems with reach-avoid guarantees. In Proceedings of the 37th AAAI Conference on Artificial Intelligence (Vol. 37, pp. 11926–11935). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v37i10.26407' chicago: Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” In Proceedings of the 37th AAAI Conference on Artificial Intelligence, 37:11926–35. Association for the Advancement of Artificial Intelligence, 2023. https://doi.org/10.1609/aaai.v37i10.26407. ieee: D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” in Proceedings of the 37th AAAI Conference on Artificial Intelligence, Washington, DC, United States, 2023, vol. 37, no. 10, pp. 11926–11935. 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.' mla: Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” Proceedings of the 37th AAAI Conference on Artificial Intelligence, vol. 37, no. 10, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–35, doi:10.1609/aaai.v37i10.26407. 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. conference: end_date: 2023-02-14 location: Washington, DC, United States name: 'AAAI: Conference on Artificial Intelligence' start_date: 2023-02-07 date_created: 2024-01-18T07:44:31Z date_published: 2023-06-26T00:00:00Z date_updated: 2024-01-22T14:08:29Z day: '26' department: - _id: ToHe - _id: KrCh doi: 10.1609/aaai.v37i10.26407 ec_funded: 1 external_id: arxiv: - '2210.05308' intvolume: ' 37' issue: '10' keyword: - General Medicine language: - iso: eng month: '06' oa_version: Preprint page: 11926-11935 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 2564DBCA-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '665385' name: International IST Doctoral Program publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence publication_identifier: eissn: - 2374-3468 issn: - 2159-5399 publication_status: published publisher: Association for the Advancement of Artificial Intelligence quality_controlled: '1' related_material: record: - id: '14600' relation: earlier_version status: public status: public title: Learning control policies for stochastic systems with reach-avoid guarantees type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 37 year: '2023' ... --- _id: '13234' 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. 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. article_processing_charge: Yes (in subscription journal) article_type: original author: - first_name: Konstantin full_name: Kueffner, Konstantin id: 8121a2d0-dc85-11ea-9058-af578f3b4515 last_name: Kueffner orcid: 0000-0001-8974-2542 - first_name: Anna full_name: Lukina, Anna id: CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425 last_name: Lukina - first_name: Christian full_name: Schilling, Christian id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87 last_name: Schilling orcid: 0000-0003-3658-1065 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Kueffner K, Lukina A, Schilling C, Henzinger TA. Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. 2023;25:575-592. doi:10.1007/s10009-023-00711-4' apa: 'Kueffner, K., Lukina, A., Schilling, C., & Henzinger, T. A. (2023). Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. Springer Nature. https://doi.org/10.1007/s10009-023-00711-4' chicago: 'Kueffner, Konstantin, Anna Lukina, Christian Schilling, and Thomas A Henzinger. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” International Journal on Software Tools for Technology Transfer. Springer Nature, 2023. https://doi.org/10.1007/s10009-023-00711-4.' ieee: 'K. Kueffner, A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: Active monitoring of neural networks (extended version),” International Journal on Software Tools for Technology Transfer, vol. 25. Springer Nature, pp. 575–592, 2023.' 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.' mla: 'Kueffner, Konstantin, et al. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” International Journal on Software Tools for Technology Transfer, vol. 25, Springer Nature, 2023, pp. 575–92, doi:10.1007/s10009-023-00711-4.' short: K. Kueffner, A. Lukina, C. Schilling, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 25 (2023) 575–592. date_created: 2023-07-16T22:01:11Z date_published: 2023-08-01T00:00:00Z date_updated: 2024-01-30T12:06:57Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.1007/s10009-023-00711-4 ec_funded: 1 external_id: arxiv: - '2009.06429' isi: - '001020160000001' file: - access_level: open_access checksum: 3c4b347f39412a76872f9a6f30101f94 content_type: application/pdf creator: dernst date_created: 2024-01-30T12:06:07Z date_updated: 2024-01-30T12:06:07Z file_id: '14903' file_name: 2023_JourSoftwareTools_Kueffner.pdf file_size: 13387667 relation: main_file success: 1 file_date_updated: 2024-01-30T12:06:07Z has_accepted_license: '1' intvolume: ' 25' isi: 1 language: - iso: eng month: '08' oa: 1 oa_version: Published Version page: 575-592 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: International Journal on Software Tools for Technology Transfer publication_identifier: eissn: - 1433-2787 issn: - 1433-2779 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '10206' relation: shorter_version status: public scopus_import: '1' status: public title: 'Into the unknown: Active monitoring of neural networks (extended version)' tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 25 year: '2023' ... --- _id: '15023' 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. acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS) and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt)." article_processing_charge: No author: - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Abhinav full_name: Verma, Abhinav id: a235593c-d7fa-11eb-a0c5-b22ca3c66ee6 last_name: Verma - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. Compositional policy learning in stochastic control systems with formal guarantees. In: 37th Conference on Neural Information Processing Systems. ; 2023.' apa: Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., & Henzinger, T. A. (2023). Compositional policy learning in stochastic control systems with formal guarantees. In 37th Conference on Neural Information Processing Systems. New Orleans, LO, United States. chicago: Zikelic, Dorde, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A Henzinger. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” In 37th Conference on Neural Information Processing Systems, 2023. ieee: D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger, “Compositional policy learning in stochastic control systems with formal guarantees,” in 37th Conference on Neural Information Processing Systems, New Orleans, LO, United States, 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.' mla: Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” 37th Conference on Neural Information Processing Systems, 2023. short: D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th Conference on Neural Information Processing Systems, 2023. conference: end_date: 2023-12-16 location: New Orleans, LO, United States name: 'NeurIPS: Neural Information Processing Systems' start_date: 2023-12-10 date_created: 2024-02-25T09:23:24Z date_published: 2023-12-15T00:00:00Z date_updated: 2024-02-28T12:20:11Z day: '15' department: - _id: ToHe - _id: KrCh ec_funded: 1 external_id: arxiv: - '2312.01456' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2312.01456 month: '12' oa: 1 oa_version: Preprint project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 37th Conference on Neural Information Processing Systems publication_status: epub_ahead quality_controlled: '1' status: public title: Compositional policy learning in stochastic control systems with formal guarantees type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '14076' abstract: - lang: eng 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. 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. alternative_title: - LNCS article_processing_charge: Yes (in subscription journal) author: - first_name: Marek full_name: Chalupa, Marek id: 87e34708-d6c6-11ec-9f5b-9391e7be2463 last_name: Chalupa - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. In: 23nd International Conference on Runtime Verification. Vol 14245. Springer Nature; 2023:168-190. doi:10.1007/978-3-031-44267-4_9' apa: 'Chalupa, M., & Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. In 23nd International Conference on Runtime Verification (Vol. 14245, pp. 168–190). Thessaloniki, Greek: Springer Nature. https://doi.org/10.1007/978-3-031-44267-4_9' chicago: Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” In 23nd International Conference on Runtime Verification, 14245:168–90. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_9. ieee: M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers,” in 23nd International Conference on Runtime Verification, Thessaloniki, Greek, 2023, vol. 14245, pp. 168–190. 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.' mla: Chalupa, Marek, and Thomas A. Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” 23nd International Conference on Runtime Verification, vol. 14245, Springer Nature, 2023, pp. 168–90, doi:10.1007/978-3-031-44267-4_9. short: M. Chalupa, T.A. Henzinger, in:, 23nd International Conference on Runtime Verification, Springer Nature, 2023, pp. 168–190. conference: end_date: 2023-10-07 location: Thessaloniki, Greek name: 'RV: Conference on Runtime Verification' start_date: 2023-10-04 date_created: 2023-08-16T20:46:08Z date_published: 2023-10-01T00:00:00Z date_updated: 2024-02-28T12:33:08Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-031-44267-4_9 ec_funded: 1 file: - access_level: open_access checksum: ee33bd6f1a26f4dae7a8192584869fd8 content_type: application/pdf creator: dernst date_created: 2023-10-16T07:15:11Z date_updated: 2023-10-16T07:15:11Z file_id: '14430' file_name: 2023_LNCS_RV_Chalupa.pdf file_size: 867256 relation: main_file success: 1 file_date_updated: 2023-10-16T07:15:11Z has_accepted_license: '1' intvolume: ' 14245' language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: 168-190 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 23nd International Conference on Runtime Verification publication_identifier: eisbn: - 978-3-031-44267-4 isbn: - 978-3-031-44266-7 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '15035' relation: research_data status: public status: public title: Monitoring hyperproperties with prefix transducers tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 14245 year: '2023' ...