[{"publication_status":"published","citation":{"chicago":"Kueffner, Konstantin, Anna Lukina, Christian Schilling, and Thomas A Henzinger. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/s10009-023-00711-4\">https://doi.org/10.1007/s10009-023-00711-4</a>.","ieee":"K. Kueffner, A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: Active monitoring of neural networks (extended version),” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 25. Springer Nature, pp. 575–592, 2023.","apa":"Kueffner, K., Lukina, A., Schilling, C., &#38; Henzinger, T. A. (2023). Into the unknown: Active monitoring of neural networks (extended version). <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-023-00711-4\">https://doi.org/10.1007/s10009-023-00711-4</a>","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.","short":"K. Kueffner, A. Lukina, C. Schilling, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 25 (2023) 575–592.","ama":"Kueffner K, Lukina A, Schilling C, Henzinger TA. Into the unknown: Active monitoring of neural networks (extended version). <i>International Journal on Software Tools for Technology Transfer</i>. 2023;25:575-592. doi:<a href=\"https://doi.org/10.1007/s10009-023-00711-4\">10.1007/s10009-023-00711-4</a>","mla":"Kueffner, Konstantin, et al. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 25, Springer Nature, 2023, pp. 575–92, doi:<a href=\"https://doi.org/10.1007/s10009-023-00711-4\">10.1007/s10009-023-00711-4</a>."},"author":[{"first_name":"Konstantin","orcid":"0000-0001-8974-2542","last_name":"Kueffner","full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515"},{"first_name":"Anna","full_name":"Lukina, Anna","last_name":"Lukina","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425"},{"first_name":"Christian","last_name":"Schilling","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"abstract":[{"lang":"eng","text":"Neural-network classifiers achieve high accuracy when predicting the class of an input that they were trained to identify. Maintaining this accuracy in dynamic environments, where inputs frequently fall outside the fixed set of initially known classes, remains a challenge. We consider the problem of monitoring the classification decisions of neural networks in the presence of novel classes. For this purpose, we generalize our recently proposed abstraction-based monitor from binary output to real-valued quantitative output. This quantitative output enables new applications, two of which we investigate in the paper. As our first application, we introduce an algorithmic framework for active monitoring of a neural network, which allows us to learn new classes dynamically and yet maintain high monitoring performance. As our second application, we present an offline procedure to retrain the neural network to improve the monitor’s detection performance without deteriorating the network’s classification accuracy. Our experimental evaluation demonstrates both the benefits of our active monitoring framework in dynamic scenarios and the effectiveness of the retraining procedure."}],"oa":1,"volume":25,"date_updated":"2024-01-30T12:06:57Z","article_processing_charge":"Yes (in subscription journal)","arxiv":1,"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.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093"}],"quality_controlled":"1","oa_version":"Published Version","_id":"13234","publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"ec_funded":1,"doi":"10.1007/s10009-023-00711-4","year":"2023","title":"Into the unknown: Active monitoring of neural networks (extended version)","external_id":{"arxiv":["2009.06429"],"isi":["001020160000001"]},"isi":1,"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)"},"ddc":["000"],"related_material":{"record":[{"status":"public","id":"10206","relation":"shorter_version"}]},"type":"journal_article","day":"01","status":"public","intvolume":"        25","file_date_updated":"2024-01-30T12:06:07Z","page":"575-592","publication":"International Journal on Software Tools for Technology Transfer","article_type":"original","date_published":"2023-08-01T00:00:00Z","month":"08","language":[{"iso":"eng"}],"publisher":"Springer Nature","scopus_import":"1","department":[{"_id":"ToHe"}],"has_accepted_license":"1","file":[{"checksum":"3c4b347f39412a76872f9a6f30101f94","date_created":"2024-01-30T12:06:07Z","file_size":13387667,"file_name":"2023_JourSoftwareTools_Kueffner.pdf","access_level":"open_access","date_updated":"2024-01-30T12:06:07Z","success":1,"creator":"dernst","file_id":"14903","relation":"main_file","content_type":"application/pdf"}],"date_created":"2023-07-16T22:01:11Z"},{"publication_status":"published","citation":{"chicago":"Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>.","ieee":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic,” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6. Springer Nature, pp. 741–758, 2020.","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., &#38; Ulus, D. (2020). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>","ista":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2020. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer. 22(6), 741–758.","short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal on Software Tools for Technology Transfer 22 (2020) 741–758.","ama":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. 2020;22(6):741-758. doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>","mla":"Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58, doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>."},"abstract":[{"lang":"eng","text":"We introduce in this paper AMT2.0, a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended signal temporal logic, which integrates timed regular expressions within signal temporal logic. The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal. We demonstrate the tool functionality on several running examples and case studies, and evaluate its performance."}],"author":[{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Lebeltel","full_name":"Lebeltel, Olivier","first_name":"Olivier"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"},{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Ferrere","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143"},{"last_name":"Ulus","full_name":"Ulus, Dogan","first_name":"Dogan"}],"keyword":["Information Systems","Software"],"date_updated":"2023-09-08T11:52:02Z","volume":22,"article_processing_charge":"No","_id":"10861","publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","quality_controlled":"1","oa_version":"None","year":"2020","doi":"10.1007/s10009-020-00582-z","title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","external_id":{"isi":["000555398600001"]},"isi":1,"related_material":{"record":[{"relation":"earlier_version","id":"299","status":"public"}]},"day":"03","type":"journal_article","intvolume":"        22","status":"public","issue":"6","publication":"International Journal on Software Tools for Technology Transfer","page":"741-758","month":"08","article_type":"original","date_published":"2020-08-03T00:00:00Z","publisher":"Springer Nature","scopus_import":"1","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"date_created":"2022-03-18T10:10:53Z"},{"type":"journal_article","day":"01","status":"public","intvolume":"         1","page":"86 - 109","publication":"Software Tools For Technology Transfer","issue":"1-2","date_published":"1997-01-01T00:00:00Z","article_type":"original","month":"01","language":[{"iso":"eng"}],"scopus_import":"1","publisher":"Springer","date_created":"2018-12-11T12:09:36Z","citation":{"apa":"Alur, R., &#38; Henzinger, T. A. (1997). Real-time system = discrete system + clock variables. <i>Software Tools For Technology Transfer</i>. Springer. <a href=\"https://doi.org/10.1007/s100090050007\">https://doi.org/10.1007/s100090050007</a>","ieee":"R. Alur and T. A. Henzinger, “Real-time system = discrete system + clock variables,” <i>Software Tools For Technology Transfer</i>, vol. 1, no. 1–2. Springer, pp. 86–109, 1997.","chicago":"Alur, Rajeev, and Thomas A Henzinger. “Real-Time System = Discrete System + Clock Variables.” <i>Software Tools For Technology Transfer</i>. Springer, 1997. <a href=\"https://doi.org/10.1007/s100090050007\">https://doi.org/10.1007/s100090050007</a>.","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Real-Time System = Discrete System + Clock Variables.” <i>Software Tools For Technology Transfer</i>, vol. 1, no. 1–2, Springer, 1997, pp. 86–109, doi:<a href=\"https://doi.org/10.1007/s100090050007\">10.1007/s100090050007</a>.","ama":"Alur R, Henzinger TA. Real-time system = discrete system + clock variables. <i>Software Tools For Technology Transfer</i>. 1997;1(1-2):86-109. doi:<a href=\"https://doi.org/10.1007/s100090050007\">10.1007/s100090050007</a>","ista":"Alur R, Henzinger TA. 1997. Real-time system = discrete system + clock variables. Software Tools For Technology Transfer. 1(1–2), 86–109.","short":"R. Alur, T.A. Henzinger, Software Tools For Technology Transfer 1 (1997) 86–109."},"publication_status":"published","author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"text":"This paper introduces, gently but rigorously, the clock approach to real-time programming. We present with mathematical precision, assuming no prerequisites other than familiarity with logical and programming notations, the concepts that are necessary for understanding, writing, and executing clock programs. In keeping with an expository style, all references are clustered in bibliographic remarks at the end of each section. The first appendix presents proof rules for verifying temporal properties of clock programs. The second appendix points to selected literature on formal methods and tools for programming with clocks. In particular, the timed automaton, which is a finite-state machine equipped with clocks, has become a standard paradigm for real-time model checking; it underlies the tools HyTech, Kronos, and Uppaal, which are discussed elsewhere in this volume.","lang":"eng"}],"article_processing_charge":"No","date_updated":"2022-08-17T08:27:20Z","volume":1,"publist_id":"123","quality_controlled":"1","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"The authors thank Rance Cleaveland, Limor Fix, David Karr, Peter Kopke, Fred Schneider, and Bernhard Steffen for helpful comments.","extern":"1","publication_identifier":{"issn":["1433-2779"]},"_id":"4584","doi":"10.1007/s100090050007","year":"1997","title":"Real-time system = discrete system + clock variables"},{"extern":"1","publication_identifier":{"issn":["1433-2779"]},"_id":"4493","quality_controlled":"1","oa_version":"None","acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, the NSF CAREER award CCR-501708, NSF grant CCR-9504469, AFOSR contract F49620-93-1-0056, ARO MURI grant DAAH-04-96-1-0341, ARPA grant  AG2-892, and SRC contract 95-DC-324.036.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","date_updated":"2022-08-17T11:14:15Z","publist_id":"236","volume":1,"abstract":[{"text":"A hybrid system is a dynamical system whose behavior exhibits both discrete and continuous change. A hybrid automaton is a mathematical model for hybrid systems, which combines, in a single formalism, automaton transitions for capturing discrete change with differential equations for capturing continuous change. HyTech is a symbolic model checker for linear hybrid automata, a subclass of hybrid automata that can be analyzed automatically by computing with polyhedral state sets. A key feature of HyTech is its ability to perform parametric analysis, i.e., to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal-logic requirement.","lang":"eng"}],"author":[{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ho, Pei","last_name":"Ho","first_name":"Pei"},{"last_name":"Wong Toi","full_name":"Wong Toi, Howard","first_name":"Howard"}],"citation":{"chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: A Model Checker for Hybrid Systems.” <i>Software Tools For Technology Transfer</i>. Springer, 1997. <a href=\"https://doi.org/10.1007/s100090050008\">https://doi.org/10.1007/s100090050008</a>.","apa":"Henzinger, T. A., Ho, P., &#38; Wong Toi, H. (1997). HyTech: A model checker for hybrid systems. <i>Software Tools For Technology Transfer</i>. Springer. <a href=\"https://doi.org/10.1007/s100090050008\">https://doi.org/10.1007/s100090050008</a>","ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “HyTech: A model checker for hybrid systems,” <i>Software Tools For Technology Transfer</i>, vol. 1, no. 1–2. Springer, pp. 110–122, 1997.","ista":"Henzinger TA, Ho P, Wong Toi H. 1997. HyTech: A model checker for hybrid systems. Software Tools For Technology Transfer. 1(1–2), 110–122.","short":"T.A. Henzinger, P. Ho, H. Wong Toi, Software Tools For Technology Transfer 1 (1997) 110–122.","ama":"Henzinger TA, Ho P, Wong Toi H. HyTech: A model checker for hybrid systems. <i>Software Tools For Technology Transfer</i>. 1997;1(1-2):110-122. doi:<a href=\"https://doi.org/10.1007/s100090050008\">10.1007/s100090050008</a>","mla":"Henzinger, Thomas A., et al. “HyTech: A Model Checker for Hybrid Systems.” <i>Software Tools For Technology Transfer</i>, vol. 1, no. 1–2, Springer, 1997, pp. 110–22, doi:<a href=\"https://doi.org/10.1007/s100090050008\">10.1007/s100090050008</a>."},"publication_status":"published","title":"HyTech: A model checker for hybrid systems","year":"1997","doi":"10.1007/s100090050008","publication":"Software Tools For Technology Transfer","issue":"1-2","page":"110 - 122","intvolume":"         1","status":"public","day":"01","type":"journal_article","date_created":"2018-12-11T12:09:08Z","scopus_import":"1","publisher":"Springer","language":[{"iso":"eng"}],"month":"01","date_published":"1997-01-01T00:00:00Z","article_type":"original"}]