[{"title":"Quantitative monitoring of Signal First-Order logic","publication_identifier":{"issn":["0302-9743"],"isbn":["9783032262196"],"eissn":["1611-3349"]},"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported by the European Research Council (ERC) Grants VAMOS (No. 101020093) and HYPER (No. 101055412), and by the Advanced Research and Invention Agency under the Safeguarded AI programme (MSAI-PR01-P047).","date_updated":"2026-06-22T08:21:09Z","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"conference":{"name":"FM: Formal Methods","end_date":"2026-05-22","location":"Tokyo, Japan","start_date":"2026-05-18"},"quality_controlled":"1","OA_type":"hybrid","das_tickbox":"0","keyword":["Signal first-order logic","Robustness-based quantitative semantics","Online runtime monitoring"],"status":"public","publication":"27th International Symposium on Formal Methods","page":"214-233","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"citation":{"ieee":"M. Chalupa, T. A. Henzinger, N. E. Sarac, and E. Yu, “Quantitative monitoring of Signal First-Order logic,” in <i>27th International Symposium on Formal Methods</i>, Tokyo, Japan, 2026, vol. 16557, pp. 214–233.","ama":"Chalupa M, Henzinger TA, Sarac NE, Yu E. Quantitative monitoring of Signal First-Order logic. In: <i>27th International Symposium on Formal Methods</i>. Vol 16557. Springer Nature; 2026:214-233. doi:<a href=\"https://doi.org/10.1007/978-3-032-26220-2_11\">10.1007/978-3-032-26220-2_11</a>","apa":"Chalupa, M., Henzinger, T. A., Sarac, N. E., &#38; Yu, E. (2026). Quantitative monitoring of Signal First-Order logic. In <i>27th International Symposium on Formal Methods</i> (Vol. 16557, pp. 214–233). Tokyo, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-26220-2_11\">https://doi.org/10.1007/978-3-032-26220-2_11</a>","short":"M. Chalupa, T.A. Henzinger, N.E. Sarac, E. Yu, in:, 27th International Symposium on Formal Methods, Springer Nature, 2026, pp. 214–233.","mla":"Chalupa, Marek, et al. “Quantitative Monitoring of Signal First-Order Logic.” <i>27th International Symposium on Formal Methods</i>, vol. 16557, Springer Nature, 2026, pp. 214–33, doi:<a href=\"https://doi.org/10.1007/978-3-032-26220-2_11\">10.1007/978-3-032-26220-2_11</a>.","ista":"Chalupa M, Henzinger TA, Sarac NE, Yu E. 2026. Quantitative monitoring of Signal First-Order logic. 27th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 16557, 214–233.","chicago":"Chalupa, Marek, Thomas A Henzinger, Naci E Sarac, and Emily Yu. “Quantitative Monitoring of Signal First-Order Logic.” In <i>27th International Symposium on Formal Methods</i>, 16557:214–33. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-26220-2_11\">https://doi.org/10.1007/978-3-032-26220-2_11</a>."},"scopus_import":"1","ddc":["000"],"department":[{"_id":"ToHe"}],"date_created":"2026-06-14T22:01:44Z","author":[{"first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Sarac","first_name":"Naci E","full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"},{"first_name":"Zhengqi","last_name":"Yu","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi","orcid":"0000-0002-4993-773X"}],"doi":"10.1007/978-3-032-26220-2_11","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"intvolume":"     16557","type":"conference","file":[{"creator":"dernst","date_created":"2026-06-22T08:18:41Z","file_name":"2026_LNCS_Chalupa.pdf","date_updated":"2026-06-22T08:18:41Z","file_id":"22113","checksum":"7055199ecb985e9e2e272f4988827067","relation":"main_file","success":1,"access_level":"open_access","file_size":849237,"content_type":"application/pdf"}],"_id":"22006","publisher":"Springer Nature","arxiv":1,"alternative_title":["LNCS"],"year":"2026","oa":1,"volume":16557,"date_published":"2026-05-18T00:00:00Z","file_date_updated":"2026-06-22T08:18:41Z","publication_status":"published","abstract":[{"text":"Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.","lang":"eng"}],"ec_funded":1,"external_id":{"arxiv":["2603.00728"]},"oa_version":"Published Version","OA_place":"publisher","day":"18","month":"05","has_accepted_license":"1"},{"corr_author":"1","department":[{"_id":"ToHe"}],"status":"public","citation":{"short":"T.A. Henzinger, K. Kueffner, E. Yu, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 54–72.","ista":"Henzinger TA, Kueffner K, Yu E. 2025. Formal verification of neural certificates done dynamically. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 54–72.","mla":"Henzinger, Thomas A., et al. “Formal Verification of Neural Certificates Done Dynamically.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 54–72, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">10.1007/978-3-032-05435-7_4</a>.","chicago":"Henzinger, Thomas A, Konstantin Kueffner, and Emily Yu. “Formal Verification of Neural Certificates Done Dynamically.” In <i>25th International Conference on Runtime Verification</i>, 16087:54–72. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">https://doi.org/10.1007/978-3-032-05435-7_4</a>.","ieee":"T. A. Henzinger, K. Kueffner, and E. Yu, “Formal verification of neural certificates done dynamically,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 54–72.","ama":"Henzinger TA, Kueffner K, Yu E. Formal verification of neural certificates done dynamically. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:54-72. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">10.1007/978-3-032-05435-7_4</a>","apa":"Henzinger, T. A., Kueffner, K., &#38; Yu, E. (2025). Formal verification of neural certificates done dynamically. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 54–72). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">https://doi.org/10.1007/978-3-032-05435-7_4</a>"},"page":"54-72","publication":"25th International Conference on Runtime Verification","conference":{"name":"RV: Runtime Verification","end_date":"2025-09-19","location":"Graz, Austria","start_date":"2025-09-15"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"quality_controlled":"1","OA_type":"green","title":"Formal verification of neural certificates done dynamically","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","date_updated":"2026-02-16T11:53:25Z","publication_identifier":{"eisbn":["9783032054357"],"issn":["0302-9743"],"eissn":["1611-3349"]},"article_processing_charge":"No","oa_version":"Preprint","ec_funded":1,"external_id":{"arxiv":["2507.11987"]},"day":"13","OA_place":"repository","month":"09","alternative_title":["LNCS"],"arxiv":1,"date_published":"2025-09-13T00:00:00Z","volume":16087,"year":"2025","oa":1,"abstract":[{"lang":"eng","text":"Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates."}],"publication_status":"published","_id":"21091","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2507.11987","open_access":"1"}],"publisher":"Springer Nature","author":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"first_name":"Konstantin","last_name":"Kueffner","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","full_name":"Kueffner, Konstantin","orcid":"0000-0001-8974-2542"},{"last_name":"Yu","first_name":"Zhengqi","orcid":"0000-0002-4993-773X","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi"}],"date_created":"2026-01-29T16:03:01Z","doi":"10.1007/978-3-032-05435-7_4","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"type":"conference","intvolume":"     16087"},{"corr_author":"1","issue":"25","department":[{"_id":"ToHe"}],"status":"public","citation":{"short":"E. Yu, D. Zikelic, T.A. Henzinger, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 26409–26417.","chicago":"Yu, Emily, Dorde Zikelic, and Thomas A Henzinger. “Neural Control and Certificate Repair via Runtime Monitoring.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:26409–17. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">https://doi.org/10.1609/aaai.v39i25.34840</a>.","ista":"Yu E, Zikelic D, Henzinger TA. 2025. Neural control and certificate repair via runtime monitoring. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 26409–26417.","mla":"Yu, Emily, et al. “Neural Control and Certificate Repair via Runtime Monitoring.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 25, Association for the Advancement of Artificial Intelligence, 2025, pp. 26409–17, doi:<a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">10.1609/aaai.v39i25.34840</a>.","ama":"Yu E, Zikelic D, Henzinger TA. Neural control and certificate repair via runtime monitoring. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:26409-26417. doi:<a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">10.1609/aaai.v39i25.34840</a>","apa":"Yu, E., Zikelic, D., &#38; Henzinger, T. A. (2025). Neural control and certificate repair via runtime monitoring. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 26409–26417). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">https://doi.org/10.1609/aaai.v39i25.34840</a>","ieee":"E. Yu, D. Zikelic, and T. A. Henzinger, “Neural control and certificate repair via runtime monitoring,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 25, pp. 26409–26417."},"page":"26409-26417","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2025-02-25","name":"AAAI: Conference on Artificial Intelligence","end_date":"2025-03-04","location":"Philadelphia, PA, United States"},"language":[{"iso":"eng"}],"quality_controlled":"1","OA_type":"green","title":"Neural control and certificate repair via runtime monitoring","date_updated":"2025-05-12T09:49:25Z","acknowledgement":"This work was supported in part by the ERC project ERC2020-AdG 101020093","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"article_processing_charge":"No","oa_version":"Preprint","external_id":{"arxiv":["2412.12996"]},"ec_funded":1,"day":"11","OA_place":"repository","month":"04","arxiv":1,"volume":39,"date_published":"2025-04-11T00:00:00Z","oa":1,"year":"2025","abstract":[{"lang":"eng","text":"Learning-based methods provide a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. To ensure the satisfaction of a safety property, learning-based methods jointly learn a control policy together with a certificate function for the property. Popular examples include barrier functions for safety and Lyapunov functions for asymptotic stability. While there has been significant progress on learning-based control with certificate functions in the white-box setting, where the correctness of the certificate function can be formally verified, there has been little work on ensuring their reliability in the black-box setting where the system dynamics are unknown. In this work, we consider the problems of certifying and repairing neural network control policies and certificate functions in the black-box setting. We propose a novel framework that utilizes runtime monitoring to detect system behaviors that violate the property of interest under some initially trained neural network policy and certificate. These violating behaviors are used to extract new training data, that is used to re-train the neural network policy and the certificate function and to ultimately repair them. We demonstrate the effectiveness of our approach empirically by using it to repair and to boost the safety rate of neural network policies learned by a state-of-the-art method for learning-based control on two autonomous system control tasks."}],"publication_status":"published","_id":"19668","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2412.12996","open_access":"1"}],"publisher":"Association for the Advancement of Artificial Intelligence","author":[{"id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi","last_name":"Yu","first_name":"Zhengqi"},{"last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"date_created":"2025-05-11T22:02:40Z","doi":"10.1609/aaai.v39i25.34840","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"intvolume":"        39","type":"conference"},{"status":"public","isi":1,"scopus_import":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"page":"281-295","citation":{"short":"N. Froleyks, E. Yu, M. Preiner, A. Biere, K. Heljanko, in:, 37th International Conference on Computer Aided Verification, Springer Nature, 2025, pp. 281–295.","ista":"Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates to the hardware model checking competition. 37th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.","mla":"Froleyks, Nils, et al. “Introducing Certificates to the Hardware Model Checking Competition.” <i>37th International Conference on Computer Aided Verification</i>, vol. 15931, Springer Nature, 2025, pp. 281–95, doi:<a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">10.1007/978-3-031-98668-0_14</a>.","chicago":"Froleyks, Nils, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko. “Introducing Certificates to the Hardware Model Checking Competition.” In <i>37th International Conference on Computer Aided Verification</i>, 15931:281–95. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">https://doi.org/10.1007/978-3-031-98668-0_14</a>.","ieee":"N. Froleyks, E. Yu, M. Preiner, A. Biere, and K. Heljanko, “Introducing certificates to the hardware model checking competition,” in <i>37th International Conference on Computer Aided Verification</i>, Zagreb, Croatia, 2025, vol. 15931, pp. 281–295.","apa":"Froleyks, N., Yu, E., Preiner, M., Biere, A., &#38; Heljanko, K. (2025). Introducing certificates to the hardware model checking competition. In <i>37th International Conference on Computer Aided Verification</i> (Vol. 15931, pp. 281–295). Zagreb, Croatia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">https://doi.org/10.1007/978-3-031-98668-0_14</a>","ama":"Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing certificates to the hardware model checking competition. In: <i>37th International Conference on Computer Aided Verification</i>. Vol 15931. Springer Nature; 2025:281-295. doi:<a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">10.1007/978-3-031-98668-0_14</a>"},"publication":"37th International Conference on Computer Aided Verification","ddc":["000"],"department":[{"_id":"ToHe"}],"acknowledgement":"This work is supported in part by the ERC-2020-AdG 101020093, the LIT AI Lab funded by the State of Upper Austria, the Research Council of Finland under the project 336092, and a gift from Intel Corporation.\r\nFurthermore we of course also owe a big thank-you to the submitters of model checkers and benchmarks to the competition over all these years. Without their enthusiasm and support neither the competition nor this study would exist.","date_updated":"2025-12-01T12:34:05Z","publication_identifier":{"isbn":["9783031986673"],"eissn":["1611-3349"],"issn":["0302-9743"]},"title":"Introducing certificates to the hardware model checking competition","article_processing_charge":"Yes (in subscription journal)","quality_controlled":"1","conference":{"end_date":"2025-07-25","location":"Zagreb, Croatia","name":"CAV: Computer Aided Verification","start_date":"2025-07-23"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"OA_type":"hybrid","date_published":"2025-01-01T00:00:00Z","volume":15931,"oa":1,"year":"2025","alternative_title":["LNCS"],"abstract":[{"text":"Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.","lang":"eng"}],"publication_status":"published","file_date_updated":"2025-09-02T05:46:10Z","day":"01","OA_place":"publisher","oa_version":"Published Version","ec_funded":1,"external_id":{"isi":["001562507100014"]},"has_accepted_license":"1","month":"01","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"doi":"10.1007/978-3-031-98668-0_14","author":[{"full_name":"Froleyks, Nils","last_name":"Froleyks","first_name":"Nils"},{"last_name":"Yu","first_name":"Zhengqi","orcid":"0000-0002-4993-773X","full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342"},{"last_name":"Preiner","first_name":"Mathias","full_name":"Preiner, Mathias"},{"full_name":"Biere, Armin","first_name":"Armin","last_name":"Biere"},{"first_name":"Keijo","last_name":"Heljanko","full_name":"Heljanko, Keijo"}],"date_created":"2025-08-17T22:01:36Z","type":"conference","intvolume":"     15931","file":[{"date_updated":"2025-09-02T05:46:10Z","date_created":"2025-09-02T05:46:10Z","file_name":"2025_CAV_Froleyks.pdf","creator":"dernst","success":1,"relation":"main_file","checksum":"15ec1bc9b9409d3b2736f4c9d5f42fd1","file_id":"20266","content_type":"application/pdf","access_level":"open_access","file_size":1078274}],"publisher":"Springer Nature","_id":"20189"},{"page":"804-816","citation":{"short":"T.A. Henzinger, F. Kresse, K. Mallik, E. Yu, D. Zikelic, in:, 7th Annual Learning for Dynamics &#38; Control Conference, ML Research Press, 2025, pp. 804–816.","chicago":"Henzinger, Thomas A, Fabian Kresse, Kaushik Mallik, Emily Yu, and Dorde Zikelic. “Predictive Monitoring of Black-Box Dynamical Systems.” In <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, 283:804–16. ML Research Press, 2025.","ista":"Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. 2025. Predictive monitoring of black-box dynamical systems. 7th Annual Learning for Dynamics &#38; Control Conference. L4DC: Learning for Dynamics &#38; Control, PMLR, vol. 283, 804–816.","mla":"Henzinger, Thomas A., et al. “Predictive Monitoring of Black-Box Dynamical Systems.” <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, vol. 283, ML Research Press, 2025, pp. 804–16.","ama":"Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. Predictive monitoring of black-box dynamical systems. In: <i>7th Annual Learning for Dynamics &#38; Control Conference</i>. Vol 283. ML Research Press; 2025:804-816.","apa":"Henzinger, T. A., Kresse, F., Mallik, K., Yu, E., &#38; Zikelic, D. (2025). Predictive monitoring of black-box dynamical systems. In <i>7th Annual Learning for Dynamics &#38; Control Conference</i> (Vol. 283, pp. 804–816). Ann Arbor, MI, United States: ML Research Press.","ieee":"T. A. Henzinger, F. Kresse, K. Mallik, E. Yu, and D. Zikelic, “Predictive monitoring of black-box dynamical systems,” in <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, Ann Arbor, MI, United States, 2025, vol. 283, pp. 804–816."},"publication":"7th Annual Learning for Dynamics & Control Conference","scopus_import":"1","status":"public","department":[{"_id":"ToHe"},{"_id":"ChLa"}],"ddc":["000"],"corr_author":"1","article_processing_charge":"No","title":"Predictive monitoring of black-box dynamical systems","acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093.\r\n","date_updated":"2025-09-03T10:37:59Z","publication_identifier":{"eissn":["2640-3498"]},"OA_type":"gold","conference":{"start_date":"2025-06-04","location":"Ann Arbor, MI, United States","end_date":"2025-06-06","name":"L4DC: Learning for Dynamics & Control"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"quality_controlled":"1","file_date_updated":"2025-09-03T10:32:12Z","abstract":[{"lang":"eng","text":"We study the problem of predictive runtime monitoring of black-box dynamical systems with quantitative safety properties. The black-box setting stipulates that the exact semantics of the dynamical system and the controller are unknown, and that we are only able to observe the state of the controlled (aka, closed-loop) system at finitely many time points. We present a novel framework for predicting future states of the system based on the states observed in the past. The numbers of past states and of predicted future states are parameters provided by the user. Our method is based on a combination of Taylor’s expansion and the backward difference operator for numerical differentiation. We also derive an upper bound on the prediction error under the assumption that the system dynamics and the controller are smooth. The predicted states are then used to predict safety violations ahead in time. Our experiments demonstrate practical applicability of our method for complex black-box systems, showing that it is computationally lightweight and yet significantly more accurate than the state-of-the-art predictive safety monitoring techniques."}],"publication_status":"published","alternative_title":["PMLR"],"arxiv":1,"volume":283,"date_published":"2025-06-01T00:00:00Z","oa":1,"year":"2025","has_accepted_license":"1","month":"06","oa_version":"Published Version","external_id":{"arxiv":["2412.16564"]},"ec_funded":1,"day":"01","OA_place":"publisher","type":"conference","intvolume":"       283","date_created":"2025-08-31T22:01:32Z","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Kresse","first_name":"Fabian","full_name":"Kresse, Fabian","id":"faff3c84-23f6-11ef-9085-e5187b51c604"},{"first_name":"Kaushik","last_name":"Mallik","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475"},{"last_name":"Yu","first_name":"Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi"},{"first_name":"Dorde","last_name":"Zikelic","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"_id":"20256","publisher":"ML Research Press","file":[{"creator":"dernst","date_created":"2025-09-03T10:32:12Z","file_name":"2025_L4DC_HenzingerT.pdf","date_updated":"2025-09-03T10:32:12Z","file_size":489639,"access_level":"open_access","content_type":"application/pdf","file_id":"20283","checksum":"d5236e561560635f5ae1d17de4903033","relation":"main_file","success":1}]},{"quality_controlled":"1","language":[{"iso":"eng"}],"conference":{"start_date":"2025-05-28","location":"Philadephia, PA, United States","end_date":"2025-05-30","name":"NeuS: International Conferenceon Neuro-Symbolic Systems"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_type":"diamond","publication_identifier":{"eissn":["2640-3498"]},"acknowledgement":"This work is supported in part by the ERC grant under Grant No. ERC-2020-AdG 101020093 and\r\nthe Austrian Science Fund (FWF) [10.55776/COE12]. This research was supported by the Scientific\r\nService Units (SSU) of ISTA through resources provided by Scientific Computing (SciComp).","date_updated":"2025-09-09T08:12:44Z","title":"Logic gate neural networks are good for verification","article_number":"26","article_processing_charge":"No","ddc":["000"],"corr_author":"1","department":[{"_id":"ChLa"},{"_id":"ToHe"}],"status":"public","scopus_import":"1","publication":"2nd International Conferenceon Neuro-Symbolic Systems","citation":{"ieee":"F. Kresse, E. Yu, C. Lampert, and T. A. Henzinger, “Logic gate neural networks are good for verification,” in <i>2nd International Conferenceon Neuro-Symbolic Systems</i>, Philadephia, PA, United States, 2025, vol. 288.","apa":"Kresse, F., Yu, E., Lampert, C., &#38; Henzinger, T. A. (2025). Logic gate neural networks are good for verification. In <i>2nd International Conferenceon Neuro-Symbolic Systems</i> (Vol. 288). Philadephia, PA, United States: ML Research Press.","ama":"Kresse F, Yu E, Lampert C, Henzinger TA. Logic gate neural networks are good for verification. In: <i>2nd International Conferenceon Neuro-Symbolic Systems</i>. Vol 288. ML Research Press; 2025.","short":"F. Kresse, E. Yu, C. Lampert, T.A. Henzinger, in:, 2nd International Conferenceon Neuro-Symbolic Systems, ML Research Press, 2025.","mla":"Kresse, Fabian, et al. “Logic Gate Neural Networks Are Good for Verification.” <i>2nd International Conferenceon Neuro-Symbolic Systems</i>, vol. 288, 26, ML Research Press, 2025.","ista":"Kresse F, Yu E, Lampert C, Henzinger TA. 2025. Logic gate neural networks are good for verification. 2nd International Conferenceon Neuro-Symbolic Systems. NeuS: International Conferenceon Neuro-Symbolic Systems, PMLR, vol. 288, 26.","chicago":"Kresse, Fabian, Emily Yu, Christoph Lampert, and Thomas A Henzinger. “Logic Gate Neural Networks Are Good for Verification.” In <i>2nd International Conferenceon Neuro-Symbolic Systems</i>, Vol. 288. ML Research Press, 2025."},"file":[{"access_level":"open_access","file_size":295466,"content_type":"application/pdf","file_id":"20314","relation":"main_file","checksum":"90a32defed34787e771a5c1623b6b0d2","success":1,"date_created":"2025-09-09T08:10:13Z","file_name":"2025_NeuS_Kresse.pdf","creator":"dernst","date_updated":"2025-09-09T08:10:13Z"}],"publisher":"ML Research Press","_id":"20296","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"author":[{"first_name":"Fabian","last_name":"Kresse","full_name":"Kresse, Fabian","id":"faff3c84-23f6-11ef-9085-e5187b51c604"},{"first_name":"Zhengqi","last_name":"Yu","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi"},{"first_name":"Christoph","last_name":"Lampert","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","full_name":"Lampert, Christoph","orcid":"0000-0001-8622-7887"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger"}],"date_created":"2025-09-07T22:01:34Z","intvolume":"       288","type":"conference","OA_place":"publisher","day":"01","ec_funded":1,"external_id":{"arxiv":["2505.19932"]},"oa_version":"Published Version","month":"06","has_accepted_license":"1","year":"2025","oa":1,"date_published":"2025-06-01T00:00:00Z","volume":288,"arxiv":1,"alternative_title":["PMLR"],"acknowledged_ssus":[{"_id":"ScienComp"}],"publication_status":"published","abstract":[{"lang":"eng","text":"Learning-based systems are increasingly deployed across various domains, yet the complexity of traditional neural networks poses significant challenges for formal verification. Unlike conventional neural networks, learned Logic Gate Networks (LGNs) replace multiplications with Boolean logic gates, yielding a sparse, netlist-like architecture that is inherently more amenable to symbolic verification, while still delivering promising performance. In this paper, we introduce a SAT encoding for verifying global robustness and fairness in LGNs. We evaluate our method on five benchmark datasets, including a newly constructed 5-class variant, and find that LGNs are both verification-friendly and maintain strong predictive performance."}],"file_date_updated":"2025-09-09T08:10:13Z"},{"day":"01","ec_funded":1,"external_id":{"arxiv":["2405.04297"],"isi":["001273489700017"]},"oa_version":"Published Version","month":"07","has_accepted_license":"1","oa":1,"year":"2024","volume":14739,"date_published":"2024-07-01T00:00:00Z","arxiv":1,"alternative_title":["LNCS"],"publication_status":"published","abstract":[{"text":"Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.","lang":"eng"}],"file_date_updated":"2024-08-12T06:53:39Z","file":[{"checksum":"7d7839fc8c5c680ea3ac09f40a66e55d","relation":"main_file","success":1,"file_id":"17414","content_type":"application/pdf","file_size":556902,"access_level":"open_access","date_updated":"2024-08-12T06:53:39Z","file_name":"2024_LNCS_Froleyks.pdf","date_created":"2024-08-12T06:53:39Z","creator":"dernst"}],"publisher":"Springer Nature","_id":"17413","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"doi":"10.1007/978-3-031-63498-7_17","date_created":"2024-08-11T22:01:13Z","author":[{"last_name":"Froleyks","first_name":"Nils","full_name":"Froleyks, Nils"},{"first_name":"Zhengqi","last_name":"Yu","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi"},{"last_name":"Biere","first_name":"Armin","full_name":"Biere, Armin"},{"last_name":"Heljanko","first_name":"Keijo","full_name":"Heljanko, Keijo"}],"intvolume":"     14739","type":"conference","ddc":["000"],"department":[{"_id":"ToHe"}],"status":"public","scopus_import":"1","isi":1,"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"citation":{"short":"N. Froleyks, E. Yu, A. Biere, K. Heljanko, in:, Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2024, pp. 284–303.","chicago":"Froleyks, Nils, Emily Yu, Armin Biere, and Keijo Heljanko. “Certifying Phase Abstraction.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, 14739:284–303. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">https://doi.org/10.1007/978-3-031-63498-7_17</a>.","mla":"Froleyks, Nils, et al. “Certifying Phase Abstraction.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, vol. 14739, Springer Nature, 2024, pp. 284–303, doi:<a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">10.1007/978-3-031-63498-7_17</a>.","ista":"Froleyks N, Yu E, Biere A, Heljanko K. 2024. Certifying phase abstraction. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). IJCAR: International Joint Conference on Automated Reasoning, LNCS, vol. 14739, 284–303.","apa":"Froleyks, N., Yu, E., Biere, A., &#38; Heljanko, K. (2024). Certifying phase abstraction. In <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 14739, pp. 284–303). Nancy, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">https://doi.org/10.1007/978-3-031-63498-7_17</a>","ama":"Froleyks N, Yu E, Biere A, Heljanko K. Certifying phase abstraction. In: <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 14739. Springer Nature; 2024:284-303. doi:<a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">10.1007/978-3-031-63498-7_17</a>","ieee":"N. Froleyks, E. Yu, A. Biere, and K. Heljanko, “Certifying phase abstraction,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Nancy, France, 2024, vol. 14739, pp. 284–303."},"page":"284-303","quality_controlled":"1","conference":{"start_date":"2024-07-03","name":"IJCAR: International Joint Conference on Automated Reasoning","end_date":"2024-07-06","location":"Nancy, France"},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031634970"]},"date_updated":"2025-09-08T08:49:53Z","acknowledgement":"This work is supported by the Austrian Science Fund (FWF) under the project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG 101020093, the Academy of Finland under the project 336092 and by a gift from Intel Corporation.","title":"Certifying phase abstraction","article_processing_charge":"Yes (in subscription journal)"},{"department":[{"_id":"ToHe"}],"citation":{"mla":"Froleyks, Nils, et al. “Ternary Simulation as Abstract Interpretation (Work in Progress).” <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, VDE Verlag, 2024, pp. 148–51.","ista":"Froleyks N, Yu E, Biere A. 2024. Ternary simulation as abstract interpretation (Work in Progress). 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems. MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems, 148–151.","chicago":"Froleyks, Nils, Emily Yu, and Armin Biere. “Ternary Simulation as Abstract Interpretation (Work in Progress).” In <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, 148–51. VDE Verlag, 2024.","short":"N. Froleyks, E. Yu, A. Biere, in:, 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems, VDE Verlag, 2024, pp. 148–151.","ieee":"N. Froleyks, E. Yu, and A. Biere, “Ternary simulation as abstract interpretation (Work in Progress),” in <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, Kaiserslautern, Germany, 2024, pp. 148–151.","ama":"Froleyks N, Yu E, Biere A. Ternary simulation as abstract interpretation (Work in Progress). In: <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>. VDE Verlag; 2024:148-151.","apa":"Froleyks, N., Yu, E., &#38; Biere, A. (2024). Ternary simulation as abstract interpretation (Work in Progress). In <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i> (pp. 148–151). Kaiserslautern, Germany: VDE Verlag."},"page":"148-151","publication":"27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems","scopus_import":"1","das_tickbox":"1","status":"public","OA_type":"green","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"conference":{"name":"MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems","end_date":"2024-02-15","location":"Kaiserslautern, Germany","start_date":"2024-02-14"},"quality_controlled":"1","article_processing_charge":"No","title":"Ternary simulation as abstract interpretation (Work in Progress)","date_updated":"2026-07-07T07:03:23Z","acknowledgement":"This work is supported by the Austrian Science Fund (FWF) under the project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG 101020093 and by a gift from Intel Corporation.","publication_identifier":{"isbn":["9783800762682"]},"month":"02","oa_version":"Submitted Version","ec_funded":1,"day":"01","OA_place":"repository","abstract":[{"text":"We introduce a formalization of ternary simulation as abstract interpretation along with a widening operator to speed up convergence. With the same goal, we present a subsumption algorithm that can determine termination earlier than the usual approach using hash sets. Additionally, we introduce a narrowing operator that utilizes recent advances in backbone extraction, allowing to increase the overapproximation precision in simulation at any time. The experiments evaluate the presented techniques in the context of hardware model checking.","lang":"eng"}],"publication_status":"published","date_published":"2024-02-01T00:00:00Z","oa":1,"year":"2024","_id":"17053","main_file_link":[{"url":"https://cca.informatik.uni-freiburg.de/papers/FroleyksYuBiere-MBMV24.pdf","open_access":"1"}],"publisher":"VDE Verlag","type":"conference","author":[{"first_name":"Nils","last_name":"Froleyks","full_name":"Froleyks, Nils"},{"last_name":"Yu","first_name":"Zhengqi","orcid":"0000-0002-4993-773X","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi"},{"full_name":"Biere, Armin","first_name":"Armin","last_name":"Biere"}],"date_created":"2024-05-26T22:00:58Z","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}]}]