[{"conference":{"end_date":"2023-07-22","location":"Paris, France","start_date":"2023-07-17","name":"CAV: Computer Aided Verification"},"language":[{"iso":"eng"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"oa_version":"Published Version","month":"07","has_accepted_license":"1","publication":"Computer Aided Verification","file":[{"creator":"dernst","file_id":"13327","access_level":"open_access","relation":"main_file","success":1,"content_type":"application/pdf","file_name":"2023_LNCS_CAV_HenzingerT.pdf","date_updated":"2023-07-31T08:11:20Z","checksum":"ccaf94bf7d658ba012c016e11869b54c","file_size":647760,"date_created":"2023-07-31T08:11:20Z"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031377037"],"isbn":["9783031377020"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2023-07-18T00:00:00Z","publisher":"Springer Nature","ec_funded":1,"quality_controlled":"1","page":"358–382","file_date_updated":"2023-07-31T08:11:20Z","article_processing_charge":"Yes (in subscription journal)","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"date_created":"2023-07-25T18:32:40Z","publication_status":"published","intvolume":"     13965","alternative_title":["LNCS"],"title":"Monitoring algorithmic fairness","_id":"13310","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"},{"id":"f1dedef5-2f78-11ee-989a-c4c97bccf506","last_name":"Karimi","first_name":"Mahyar","full_name":"Karimi, Mahyar","orcid":"0009-0005-0820-1696"},{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","full_name":"Kueffner, Konstantin","orcid":"0000-0001-8974-2542","last_name":"Kueffner","first_name":"Konstantin"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik"}],"acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG101020093.","volume":13965,"ddc":["000"],"day":"18","arxiv":1,"doi":"10.1007/978-3-031-37703-7_17","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."}],"citation":{"ieee":"T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness,” in <i>Computer Aided Verification</i>, Paris, France, 2023, vol. 13965, pp. 358–382.","chicago":"Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. “Monitoring Algorithmic Fairness.” In <i>Computer Aided Verification</i>, 13965:358–382. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">https://doi.org/10.1007/978-3-031-37703-7_17</a>.","ama":"Henzinger TA, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness. In: <i>Computer Aided Verification</i>. Vol 13965. Springer Nature; 2023:358–382. doi:<a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">10.1007/978-3-031-37703-7_17</a>","apa":"Henzinger, T. A., Karimi, M., Kueffner, K., &#38; Mallik, K. (2023). Monitoring algorithmic fairness. In <i>Computer Aided Verification</i> (Vol. 13965, pp. 358–382). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">https://doi.org/10.1007/978-3-031-37703-7_17</a>","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.","short":"T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification, Springer Nature, 2023, pp. 358–382.","mla":"Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness.” <i>Computer Aided Verification</i>, vol. 13965, Springer Nature, 2023, pp. 358–382, doi:<a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">10.1007/978-3-031-37703-7_17</a>."},"year":"2023","date_updated":"2023-09-05T15:14:00Z","external_id":{"arxiv":["2305.15979"]}},{"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."}],"day":"01","doi":"10.1007/978-3-031-44267-4_9","citation":{"apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. In <i>23nd International Conference on Runtime Verification</i> (Vol. 14245, pp. 168–190). Thessaloniki, Greek: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">https://doi.org/10.1007/978-3-031-44267-4_9</a>","ama":"Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. In: <i>23nd International Conference on Runtime Verification</i>. Vol 14245. Springer Nature; 2023:168-190. doi:<a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">10.1007/978-3-031-44267-4_9</a>","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” In <i>23nd International Conference on Runtime Verification</i>, 14245:168–90. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">https://doi.org/10.1007/978-3-031-44267-4_9</a>.","ieee":"M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers,” in <i>23nd International Conference on Runtime Verification</i>, Thessaloniki, Greek, 2023, vol. 14245, pp. 168–190.","short":"M. Chalupa, T.A. Henzinger, in:, 23nd International Conference on Runtime Verification, Springer Nature, 2023, pp. 168–190.","mla":"Chalupa, Marek, and Thomas A. Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” <i>23nd International Conference on Runtime Verification</i>, vol. 14245, Springer Nature, 2023, pp. 168–90, doi:<a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">10.1007/978-3-031-44267-4_9</a>.","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."},"year":"2023","date_updated":"2024-02-28T12:33:08Z","ddc":["000"],"volume":14245,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank Ana Oliveira da Costa for commenting on a draft of the paper.","intvolume":"     14245","alternative_title":["LNCS"],"title":"Monitoring hyperproperties with prefix transducers","date_created":"2023-08-16T20:46:08Z","article_processing_charge":"Yes (in subscription journal)","department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"last_name":"Chalupa","first_name":"Marek","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"14076","publisher":"Springer Nature","file_date_updated":"2023-10-16T07:15:11Z","ec_funded":1,"quality_controlled":"1","page":"168-190","oa":1,"publication_identifier":{"isbn":["978-3-031-44266-7"],"eisbn":["978-3-031-44267-4"]},"type":"conference","date_published":"2023-10-01T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"related_material":{"record":[{"status":"public","id":"15035","relation":"research_data"}]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2023-10-16T07:15:11Z","checksum":"ee33bd6f1a26f4dae7a8192584869fd8","file_size":867256,"date_updated":"2023-10-16T07:15:11Z","content_type":"application/pdf","file_name":"2023_LNCS_RV_Chalupa.pdf","success":1,"access_level":"open_access","relation":"main_file","file_id":"14430","creator":"dernst"}],"month":"10","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"oa_version":"Published Version","has_accepted_license":"1","publication":"23nd International Conference on Runtime Verification","conference":{"location":"Thessaloniki, Greek","end_date":"2023-10-07","start_date":"2023-10-04","name":"RV: Conference on Runtime Verification"},"language":[{"iso":"eng"}]},{"publisher":"Association for the Advancement of Artificial Intelligence","page":"14964-14973","ec_funded":1,"quality_controlled":"1","publication_status":"published","article_processing_charge":"No","date_created":"2023-08-27T22:01:17Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Quantization-aware interval bound propagation for training certifiably robust quantized neural networks","intvolume":"        37","_id":"14242","scopus_import":"1","author":[{"full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Rus","first_name":"Daniela","full_name":"Rus, Daniela"}],"issue":"12","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.","volume":37,"arxiv":1,"doi":"10.1609/aaai.v37i12.26747","day":"26","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."}],"date_updated":"2025-07-14T09:09:56Z","year":"2023","citation":{"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.","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.","mla":"Lechner, Mathias, et al. “Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 12, Association for the Advancement of Artificial Intelligence, 2023, pp. 14964–73, doi:<a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">10.1609/aaai.v37i12.26747</a>.","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 <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:14964–73. Association for the Advancement of Artificial Intelligence, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">https://doi.org/10.1609/aaai.v37i12.26747</a>.","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 <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 12, pp. 14964–14973.","apa":"Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T. A., &#38; Rus, D. (2023). Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 14964–14973). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">https://doi.org/10.1609/aaai.v37i12.26747</a>","ama":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:14964-14973. doi:<a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">10.1609/aaai.v37i12.26747</a>"},"external_id":{"arxiv":["2211.16187"]},"conference":{"name":"AAAI: Conference on Artificial Intelligence","start_date":"2023-02-07","end_date":"2023-02-14","location":"Washington, DC, United States"},"language":[{"iso":"eng"}],"oa_version":"Preprint","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"}],"month":"06","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2211.16187","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","publication_identifier":{"isbn":["9781577358800"]},"oa":1,"date_published":"2023-06-26T00:00:00Z","type":"conference"},{"conference":{"name":"AAAI: Conference on Artificial Intelligence","start_date":"2023-02-07","end_date":"2023-02-14","location":"Washington, DC, United States"},"language":[{"iso":"eng"}],"month":"06","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"}],"oa_version":"Published Version","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","main_file_link":[{"url":"https://doi.org/10.1609/aaai.v37i5.25679","open_access":"1"}],"oa":1,"publication_identifier":{"isbn":["9781577358800"]},"type":"conference","date_published":"2023-06-27T00:00:00Z","ec_funded":1,"quality_controlled":"1","page":"5464-5471","intvolume":"        37","title":"Bidding graph games with partially-observable budgets","date_created":"2023-08-27T22:01:18Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"article_processing_charge":"No","publication_status":"published","issue":"5","author":[{"last_name":"Avni","first_name":"Guy","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","full_name":"Jecker, Ismael R","last_name":"Jecker","first_name":"Ismael R"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","first_name":"Dorde","last_name":"Zikelic"}],"scopus_import":"1","_id":"14243","volume":37,"acknowledgement":"This research was supported in part by ISF grant no.1679/21, by the 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.","abstract":[{"lang":"eng","text":"Two-player zero-sum \"graph games\" are central in logic, verification, and multi-agent systems. The game proceeds by placing a token on a vertex of a graph, and allowing the players to move it to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In \"bidding games\", however, the players have budgets and in each turn, an auction (bidding) determines which player moves the token. So far, bidding games have only been studied as full-information games. In this work we initiate the study of partial-information bidding games: we study bidding games in which a player's initial budget is drawn from a known probability distribution. We show that while for some bidding mechanisms and objectives, it is straightforward to adapt the results from the full-information setting to the partial-information setting, for others, the analysis is significantly more challenging, requires new techniques, and gives rise to interesting results. Specifically, we study games with \"mean-payoff\" objectives in combination with \"poorman\" bidding. We construct optimal strategies for a partially-informed player who plays against a fully-informed adversary. We show that, somewhat surprisingly, the \"value\" under pure strategies does not necessarily exist in such games."}],"day":"27","arxiv":1,"doi":"10.1609/aaai.v37i5.25679","external_id":{"arxiv":["2211.13626"]},"year":"2023","citation":{"ista":"Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 5464–5471.","short":"G. Avni, I.R. Jecker, D. Zikelic, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, 2023, pp. 5464–5471.","mla":"Avni, Guy, et al. “Bidding Graph Games with Partially-Observable Budgets.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 5, 2023, pp. 5464–71, doi:<a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">10.1609/aaai.v37i5.25679</a>.","chicago":"Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Bidding Graph Games with Partially-Observable Budgets.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:5464–71, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">https://doi.org/10.1609/aaai.v37i5.25679</a>.","ieee":"G. Avni, I. R. Jecker, and D. Zikelic, “Bidding graph games with partially-observable budgets,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 5, pp. 5464–5471.","apa":"Avni, G., Jecker, I. R., &#38; Zikelic, D. (2023). Bidding graph games with partially-observable budgets. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 5464–5471). Washington, DC, United States. <a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">https://doi.org/10.1609/aaai.v37i5.25679</a>","ama":"Avni G, Jecker IR, Zikelic D. Bidding graph games with partially-observable budgets. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. ; 2023:5464-5471. doi:<a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">10.1609/aaai.v37i5.25679</a>"},"date_updated":"2025-07-14T09:09:56Z"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","relation":"later_version","id":"12856"}]},"status":"public","file":[{"file_size":662409,"checksum":"55426e463fdeafe9777fc3ff635154c7","date_created":"2023-01-27T03:18:34Z","file_name":"main.pdf","content_type":"application/pdf","date_updated":"2023-01-27T03:18:34Z","access_level":"open_access","relation":"main_file","success":1,"creator":"fmuehlbo","file_id":"12408"}],"oa":1,"publication_identifier":{"eissn":["2664-1690"]},"type":"technical_report","date_published":"2023-01-27T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"keyword":["runtime monitoring","best effort","third party"],"language":[{"iso":"eng"}],"month":"01","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"oa_version":"Published Version","has_accepted_license":"1","ddc":["005"],"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.","abstract":[{"text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\n\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch.","lang":"eng"}],"day":"27","doi":"10.15479/AT:ISTA:12407","citation":{"ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023.","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023. <a href=\"https://doi.org/10.15479/AT:ISTA:12407\">https://doi.org/10.15479/AT:ISTA:12407</a>.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2023). <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:12407\">https://doi.org/10.15479/AT:ISTA:12407</a>","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria; 2023. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:12407\">10.15479/AT:ISTA:12407</a>","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. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:12407\">10.15479/AT:ISTA:12407</a>.","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."},"year":"2023","date_updated":"2023-04-25T07:19:06Z","publisher":"Institute of Science and Technology Austria","file_date_updated":"2023-01-27T03:18:34Z","ec_funded":1,"page":"38","alternative_title":["IST Austria Technical Report"],"title":"VAMOS: Middleware for Best-Effort Third-Party Monitoring","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2023-01-27T03:18:08Z","publication_status":"published","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek","first_name":"Marek","last_name":"Chalupa"},{"full_name":"Mühlböck, Fabian","orcid":"0000-0003-1548-0177","last_name":"Mühlböck","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425"},{"id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","last_name":"Muroya Lei","first_name":"Stefanie","full_name":"Muroya Lei, Stefanie"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A"}],"_id":"12407"},{"conference":{"name":"FOSSACS: Foundations of Software Science and Computation Structures","start_date":"2023-04-22","end_date":"2023-04-27","location":"Paris, France"},"language":[{"iso":"eng"}],"month":"04","oa_version":"Published Version","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"publication":"26th International Conference Foundations of Software Science and Computation Structures","has_accepted_license":"1","status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","file":[{"relation":"main_file","success":1,"access_level":"open_access","creator":"esarac","file_id":"12468","checksum":"981025aed580b6b27c426cb8856cf63e","file_size":449027,"date_created":"2023-01-31T07:22:21Z","file_name":"qsl.pdf","content_type":"application/pdf","date_updated":"2023-01-31T07:22:21Z"},{"date_updated":"2023-06-19T10:28:09Z","content_type":"application/pdf","file_name":"2023_LNCS_HenzingerT.pdf","date_created":"2023-06-19T10:28:09Z","file_size":1048171,"checksum":"f16e2af1e0eb243158ab0f0fe74e7d5a","file_id":"13153","creator":"dernst","success":1,"access_level":"open_access","relation":"main_file"}],"oa":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308284"]},"date_published":"2023-04-21T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"publisher":"Springer Nature","file_date_updated":"2023-06-19T10:28:09Z","page":"349-370","quality_controlled":"1","ec_funded":1,"title":"Quantitative safety and liveness","alternative_title":["LNCS"],"intvolume":"     13992","publication_status":"published","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2023-01-31T07:23:56Z","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"},{"first_name":"Nicolas Adrien","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E"}],"_id":"12467","scopus_import":"1","ddc":["000"],"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","volume":13992,"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."}],"doi":"10.1007/978-3-031-30829-1_17","arxiv":1,"day":"21","external_id":{"arxiv":["2301.11175"]},"date_updated":"2023-07-14T11:20:27Z","citation":{"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.","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.","mla":"Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” <i>26th International Conference Foundations of Software Science and Computation Structures</i>, vol. 13992, Springer Nature, 2023, pp. 349–70, doi:<a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">10.1007/978-3-031-30829-1_17</a>.","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and liveness,” in <i>26th International Conference Foundations of Software Science and Computation Structures</i>, Paris, France, 2023, vol. 13992, pp. 349–370.","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Safety and Liveness.” In <i>26th International Conference Foundations of Software Science and Computation Structures</i>, 13992:349–70. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">https://doi.org/10.1007/978-3-031-30829-1_17</a>.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In: <i>26th International Conference Foundations of Software Science and Computation Structures</i>. Vol 13992. Springer Nature; 2023:349-370. doi:<a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">10.1007/978-3-031-30829-1_17</a>","apa":"Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Quantitative safety and liveness. In <i>26th International Conference Foundations of Software Science and Computation Structures</i> (Vol. 13992, pp. 349–370). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">https://doi.org/10.1007/978-3-031-30829-1_17</a>"},"year":"2023"},{"file":[{"success":1,"access_level":"open_access","relation":"main_file","file_id":"12714","creator":"cchlebak","date_created":"2023-03-07T12:22:23Z","file_size":944052,"checksum":"5a75dcd326ea66685de2b1aaec259e85","date_updated":"2023-03-07T12:22:23Z","content_type":"application/pdf","file_name":"2023_IEEERobAutLetters_Lechner.pdf"}],"status":"public","related_material":{"record":[{"status":"public","id":"11366","relation":"earlier_version"}]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publication_identifier":{"eissn":["2377-3766"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_published":"2023-03-01T00:00:00Z","type":"journal_article","language":[{"iso":"eng"}],"oa_version":"Published Version","month":"03","publication":"IEEE Robotics and Automation Letters","has_accepted_license":"1","acknowledgement":"We thank Christoph Lampert for inspiring this work. The\r\nviews and conclusions contained in this document are those of\r\nthe authors and should not be interpreted as representing the\r\nofficial policies, either expressed or implied, of the United States\r\nAir Force or the U.S. Government. The U.S. Government is\r\nauthorized to reproduce and distribute reprints for Government\r\npurposes notwithstanding any copyright notation herein.","volume":8,"ddc":["000"],"doi":"10.1109/LRA.2023.3240930","arxiv":1,"day":"01","abstract":[{"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.","lang":"eng"}],"date_updated":"2023-08-01T13:36:50Z","year":"2023","citation":{"mla":"Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” <i>IEEE Robotics and Automation Letters</i>, vol. 8, no. 3, Institute of Electrical and Electronics Engineers, 2023, pp. 1595–602, doi:<a href=\"https://doi.org/10.1109/LRA.2023.3240930\">10.1109/LRA.2023.3240930</a>.","short":"M. Lechner, A. Amini, D. Rus, T.A. Henzinger, IEEE Robotics and Automation Letters 8 (2023) 1595–1602.","ista":"Lechner M, Amini A, Rus D, Henzinger TA. 2023. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. IEEE Robotics and Automation Letters. 8(3), 1595–1602.","ama":"Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. <i>IEEE Robotics and Automation Letters</i>. 2023;8(3):1595-1602. doi:<a href=\"https://doi.org/10.1109/LRA.2023.3240930\">10.1109/LRA.2023.3240930</a>","apa":"Lechner, M., Amini, A., Rus, D., &#38; Henzinger, T. A. (2023). Revisiting the adversarial robustness-accuracy tradeoff in robot learning. <i>IEEE Robotics and Automation Letters</i>. Institute of Electrical and Electronics Engineers. <a href=\"https://doi.org/10.1109/LRA.2023.3240930\">https://doi.org/10.1109/LRA.2023.3240930</a>","chicago":"Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” <i>IEEE Robotics and Automation Letters</i>. Institute of Electrical and Electronics Engineers, 2023. <a href=\"https://doi.org/10.1109/LRA.2023.3240930\">https://doi.org/10.1109/LRA.2023.3240930</a>.","ieee":"M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial robustness-accuracy tradeoff in robot learning,” <i>IEEE Robotics and Automation Letters</i>, vol. 8, no. 3. Institute of Electrical and Electronics Engineers, pp. 1595–1602, 2023."},"isi":1,"external_id":{"arxiv":["2204.07373"],"isi":["000936534100012"]},"publisher":"Institute of Electrical and Electronics Engineers","article_type":"original","page":"1595-1602","quality_controlled":"1","file_date_updated":"2023-03-07T12:22:23Z","publication_status":"published","article_processing_charge":"No","date_created":"2023-03-05T23:01:04Z","department":[{"_id":"ToHe"}],"title":"Revisiting the adversarial robustness-accuracy tradeoff in robot learning","intvolume":"         8","_id":"12704","scopus_import":"1","author":[{"first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Amini, Alexander","last_name":"Amini","first_name":"Alexander"},{"full_name":"Rus, Daniela","last_name":"Rus","first_name":"Daniela"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"issue":"3"},{"conference":{"location":"Paris, France","end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22"},"language":[{"iso":"eng"}],"month":"04","oa_version":"Published Version","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"publication":"Tools and Algorithms for the Construction and Analysis of Systems","has_accepted_license":"1","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_name":"2023_LNCS_Chalupa.pdf","content_type":"application/pdf","date_updated":"2023-04-25T06:58:36Z","file_size":16096413,"checksum":"120d2c2a38384058ad0630fdf8288312","date_created":"2023-04-25T06:58:36Z","creator":"dernst","file_id":"12864","access_level":"open_access","success":1,"relation":"main_file"}],"oa":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031308208"],"isbn":["9783031308192"]},"date_published":"2023-04-20T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"publisher":"Springer Nature","file_date_updated":"2023-04-25T06:58:36Z","page":"535-540","quality_controlled":"1","ec_funded":1,"alternative_title":["LNCS"],"title":"Bubaak: Runtime monitoring of program verifiers","intvolume":"     13994","publication_status":"published","date_created":"2023-04-20T08:22:53Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"12854","ddc":["000"],"volume":13994,"acknowledgement":"This work was supported by the ERC-2020-AdG 10102009 grant.","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."}],"doi":"10.1007/978-3-031-30820-8_32","day":"20","date_updated":"2023-04-25T07:02:43Z","year":"2023","citation":{"ista":"Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 535–540.","short":"M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 535–540.","mla":"Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13994, Springer Nature, 2023, pp. 535–40, doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">10.1007/978-3-031-30820-8_32</a>.","ieee":"M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Paris, France, 2023, vol. 13994, pp. 535–540.","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 13994:535–40. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">https://doi.org/10.1007/978-3-031-30820-8_32</a>.","apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Bubaak: Runtime monitoring of program verifiers. In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">https://doi.org/10.1007/978-3-031-30820-8_32</a>","ama":"Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers. In: <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13994. Springer Nature; 2023:535-540. doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">10.1007/978-3-031-30820-8_32</a>"}},{"intvolume":"     13991","title":"Vamos: Middleware for best-effort third-party monitoring","alternative_title":["LNCS"],"article_processing_charge":"No","date_created":"2023-04-20T08:29:42Z","department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"full_name":"Mühlböck, Fabian","orcid":"0000-0003-1548-0177","last_name":"Mühlböck","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425"},{"full_name":"Muroya Lei, Stefanie","first_name":"Stefanie","last_name":"Muroya Lei","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"12856","publisher":"Springer Nature","file_date_updated":"2023-04-25T07:16:36Z","quality_controlled":"1","ec_funded":1,"page":"260-281","abstract":[{"text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch.","lang":"eng"}],"day":"20","doi":"10.1007/978-3-031-30826-0_15","citation":{"ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware for best-effort third-party monitoring,” in <i>Fundamental Approaches to Software Engineering</i>, Paris, France, 2023, vol. 13991, pp. 260–281.","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” In <i>Fundamental Approaches to Software Engineering</i>, 13991:260–81. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">https://doi.org/10.1007/978-3-031-30826-0_15</a>.","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort third-party monitoring. In: <i>Fundamental Approaches to Software Engineering</i>. Vol 13991. Springer Nature; 2023:260-281. doi:<a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">10.1007/978-3-031-30826-0_15</a>","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2023). Vamos: Middleware for best-effort third-party monitoring. In <i>Fundamental Approaches to Software Engineering</i> (Vol. 13991, pp. 260–281). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">https://doi.org/10.1007/978-3-031-30826-0_15</a>","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.” <i>Fundamental Approaches to Software Engineering</i>, vol. 13991, Springer Nature, 2023, pp. 260–81, doi:<a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">10.1007/978-3-031-30826-0_15</a>.","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."},"year":"2023","date_updated":"2023-04-25T07:19:07Z","ddc":["000"],"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.","volume":13991,"month":"04","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"oa_version":"Published Version","has_accepted_license":"1","publication":"Fundamental Approaches to Software Engineering","conference":{"end_date":"2023-04-27","location":"Paris, France","start_date":"2023-04-22","name":"FASE: Fundamental Approaches to Software Engineering"},"language":[{"iso":"eng"}],"oa":1,"publication_identifier":{"isbn":["9783031308253"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031308260"]},"type":"conference","date_published":"2023-04-20T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"relation":"earlier_version","id":"12407","status":"public"}]},"status":"public","file":[{"file_name":"2023_LNCS_ChalupaM.pdf","content_type":"application/pdf","date_updated":"2023-04-25T07:16:36Z","checksum":"17a7c8e08be609cf2408d37ea55e322c","file_size":580828,"date_created":"2023-04-25T07:16:36Z","creator":"dernst","file_id":"12865","success":1,"access_level":"open_access","relation":"main_file"}]},{"scopus_import":"1","_id":"12876","pmid":1,"issue":"4","author":[{"full_name":"Beneš, Nikola","first_name":"Nikola","last_name":"Beneš"},{"last_name":"Brim","first_name":"Luboš","full_name":"Brim, Luboš"},{"first_name":"Ondřej","last_name":"Huvar","full_name":"Huvar, Ondřej"},{"id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","full_name":"Pastva, Samuel","first_name":"Samuel","last_name":"Pastva"},{"full_name":"Šafránek, David","last_name":"Šafránek","first_name":"David"}],"date_created":"2023-04-30T22:01:05Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","intvolume":"        39","title":"Boolean network sketches: A unifying framework for logical model inference","quality_controlled":"1","ec_funded":1,"file_date_updated":"2023-05-02T07:39:04Z","publisher":"Oxford Academic","article_type":"original","year":"2023","citation":{"chicago":"Beneš, Nikola, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek. “Boolean Network Sketches: A Unifying Framework for Logical Model Inference.” <i>Bioinformatics</i>. Oxford Academic, 2023. <a href=\"https://doi.org/10.1093/bioinformatics/btad158\">https://doi.org/10.1093/bioinformatics/btad158</a>.","ieee":"N. Beneš, L. Brim, O. Huvar, S. Pastva, and D. Šafránek, “Boolean network sketches: A unifying framework for logical model inference,” <i>Bioinformatics</i>, vol. 39, no. 4. Oxford Academic, 2023.","ama":"Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. Boolean network sketches: A unifying framework for logical model inference. <i>Bioinformatics</i>. 2023;39(4). doi:<a href=\"https://doi.org/10.1093/bioinformatics/btad158\">10.1093/bioinformatics/btad158</a>","apa":"Beneš, N., Brim, L., Huvar, O., Pastva, S., &#38; Šafránek, D. (2023). Boolean network sketches: A unifying framework for logical model inference. <i>Bioinformatics</i>. Oxford Academic. <a href=\"https://doi.org/10.1093/bioinformatics/btad158\">https://doi.org/10.1093/bioinformatics/btad158</a>","ista":"Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. 2023. Boolean network sketches: A unifying framework for logical model inference. Bioinformatics. 39(4), btad158.","mla":"Beneš, Nikola, et al. “Boolean Network Sketches: A Unifying Framework for Logical Model Inference.” <i>Bioinformatics</i>, vol. 39, no. 4, btad158, Oxford Academic, 2023, doi:<a href=\"https://doi.org/10.1093/bioinformatics/btad158\">10.1093/bioinformatics/btad158</a>.","short":"N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, Bioinformatics 39 (2023)."},"date_updated":"2023-08-01T14:27:28Z","external_id":{"pmid":["37004199"],"isi":["000976610800001"]},"isi":1,"day":"03","doi":"10.1093/bioinformatics/btad158","abstract":[{"lang":"eng","text":"Motivation: The problem of model inference is of fundamental importance to systems biology. Logical models (e.g. Boolean networks; BNs) represent a computationally attractive approach capable of handling large biological networks. The models are typically inferred from experimental data. However, even with a substantial amount of experimental data supported by some prior knowledge, existing inference methods often focus on a small sample of admissible candidate models only.\r\n\r\nResults: We propose Boolean network sketches as a new formal instrument for the inference of Boolean networks. A sketch integrates (typically partial) knowledge about the network’s topology and the update logic (obtained through, e.g. a biological knowledge base or a literature search), as well as further assumptions about the properties of the network’s transitions (e.g. the form of its attractor landscape), and additional restrictions on the model dynamics given by the measured experimental data. Our new BNs inference algorithm starts with an ‘initial’ sketch, which is extended by adding restrictions representing experimental data to a ‘data-informed’ sketch and subsequently computes all BNs consistent with the data-informed sketch. Our algorithm is based on a symbolic representation and coloured model-checking. Our approach is unique in its ability to cover a broad spectrum of knowledge and efficiently produce a compact representation of all inferred BNs. We evaluate the method on a non-trivial collection of real-world and simulated data."}],"volume":39,"acknowledgement":"This work was partially supported by GACR [grant No. GA22-10845S]; and Grant Agency of Masaryk University [grant No. MUNI/G/1771/2020]. This work was partially supported by European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie [Grant Agreement No. 101034413 to S.P.].","ddc":["000"],"has_accepted_license":"1","publication":"Bioinformatics","project":[{"grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020"}],"oa_version":"Published Version","article_number":"btad158","month":"04","language":[{"iso":"eng"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"journal_article","date_published":"2023-04-03T00:00:00Z","publication_identifier":{"eissn":["1367-4811"]},"oa":1,"file":[{"date_created":"2023-05-02T07:39:04Z","file_size":478740,"checksum":"2cb90ddf781baefddf47eac4b54e2a03","date_updated":"2023-05-02T07:39:04Z","file_name":"2023_Bioinformatics_Benes.pdf","content_type":"application/pdf","success":1,"access_level":"open_access","relation":"main_file","file_id":"12886","creator":"dernst"}],"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","related_material":{"link":[{"relation":"software","url":"https://doi.org/10.5281/zenodo.7688740"}]}},{"oa_version":"Preprint","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"month":"01","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","conference":{"location":"Philadelphia, PA, United States","end_date":"2022-01-18","start_date":"2022-01-16","name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783030945824"],"eissn":["16113349"],"issn":["03029743"]},"oa":1,"date_published":"2022-01-14T00:00:00Z","type":"conference","main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.2105.02013"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","publication_status":"published","date_created":"2022-02-20T23:01:34Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","title":"Flavors of sequential information flow","alternative_title":["LNCS"],"intvolume":"     13182","_id":"10774","scopus_import":"1","author":[{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas","first_name":"Thomas","last_name":"Ferrere"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"},{"full_name":"Nickovic, Dejan","first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ana Oliveira","last_name":"Da Costa","full_name":"Da Costa, Ana Oliveira"}],"publisher":"Springer Nature","page":"1-19","quality_controlled":"1","arxiv":1,"doi":"10.1007/978-3-030-94583-1_1","day":"14","abstract":[{"lang":"eng","text":"We study the problem of specifying sequential information-flow properties of systems. Information-flow properties are hyperproperties, as they compare different traces of a system. Sequential information-flow properties can express changes, over time, in the information-flow constraints. For example, information-flow constraints during an initialization phase of a system may be different from information-flow constraints that are required during the operation phase. We formalize several variants of interpreting sequential information-flow constraints, which arise from different assumptions about what can be observed of the system. For this purpose, we introduce a first-order logic, called Hypertrace Logic, with both trace and time quantifiers for specifying linear-time hyperproperties. We prove that HyperLTL, which corresponds to a fragment of Hypertrace Logic with restricted quantifier prefixes, cannot specify the majority of the studied variants of sequential information flow, including all variants in which the transition between sequential phases (such as initialization and operation) happens asynchronously. Our results rely on new equivalences between sets of traces that cannot be distinguished by certain classes of formulas from Hypertrace Logic. This presents a new approach to proving inexpressiveness results for HyperLTL."}],"date_updated":"2022-08-05T09:02:56Z","citation":{"chicago":"Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, 13182:1–19. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">https://doi.org/10.1007/978-3-030-94583-1_1</a>.","ieee":"E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Flavors of sequential information flow,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Philadelphia, PA, United States, 2022, vol. 13182, pp. 1–19.","ama":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential information flow. In: <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 13182. Springer Nature; 2022:1-19. doi:<a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">10.1007/978-3-030-94583-1_1</a>","apa":"Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Da Costa, A. O. (2022). Flavors of sequential information flow. In <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 13182, pp. 1–19). Philadelphia, PA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">https://doi.org/10.1007/978-3-030-94583-1_1</a>","ista":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Flavors of sequential information flow. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 13182, 1–19.","short":"E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:, Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2022, pp. 1–19.","mla":"Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, vol. 13182, Springer Nature, 2022, pp. 1–19, doi:<a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">10.1007/978-3-030-94583-1_1</a>."},"year":"2022","external_id":{"arxiv":["2105.02013"]},"acknowledgement":"This work was funded in part by the Wittgenstein Award Z211-N23 of the Austrian Science Fund (FWF) and by the FWF project W1255-N23.","volume":13182},{"publication_identifier":{"isbn":["9783030955601"],"eissn":["1611-3349"],"issn":["0302-9743"]},"type":"conference","date_published":"2022-02-22T00:00:00Z","status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"oa_version":"None","month":"02","publication":"Software Verification","conference":{"location":"New Haven, CT, United States","end_date":"2021-10-19","name":"NSV: Numerical Software Verification","start_date":"2021-10-18"},"language":[{"iso":"eng"}],"day":"22","doi":"10.1007/978-3-030-95561-8_1","abstract":[{"text":"We present a formal framework for the online black-box monitoring of software using monitors with quantitative verdict functions. Quantitative verdict functions have several advantages. First, quantitative monitors can be approximate, i.e., the value of the verdict function does not need to correspond exactly to the value of the property under observation. Second, quantitative monitors can be quantified universally, i.e., for every possible observed behavior, the monitor tries to make the best effort to estimate the value of the property under observation. Third, quantitative monitors can watch boolean as well as quantitative properties, such as average response time. Fourth, quantitative monitors can use non-finite-state resources, such as counters. As a consequence, quantitative monitors can be compared according to how many resources they use (e.g., the number of counters) and how precisely they approximate the property under observation. This allows for a rich spectrum of cost-precision trade-offs in monitoring software.","lang":"eng"}],"citation":{"mla":"Henzinger, Thomas A. “Quantitative Monitoring of Software.” <i>Software Verification</i>, vol. 13124, Springer Nature, 2022, pp. 3–6, doi:<a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">10.1007/978-3-030-95561-8_1</a>.","short":"T.A. Henzinger, in:, Software Verification, Springer Nature, 2022, pp. 3–6.","ista":"Henzinger TA. 2022. Quantitative monitoring of software. Software Verification. NSV: Numerical Software VerificationLNCS vol. 13124, 3–6.","ama":"Henzinger TA. Quantitative monitoring of software. In: <i>Software Verification</i>. Vol 13124. LNCS. Springer Nature; 2022:3-6. doi:<a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">10.1007/978-3-030-95561-8_1</a>","apa":"Henzinger, T. A. (2022). Quantitative monitoring of software. In <i>Software Verification</i> (Vol. 13124, pp. 3–6). New Haven, CT, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">https://doi.org/10.1007/978-3-030-95561-8_1</a>","ieee":"T. A. Henzinger, “Quantitative monitoring of software,” in <i>Software Verification</i>, New Haven, CT, United States, 2022, vol. 13124, pp. 3–6.","chicago":"Henzinger, Thomas A. “Quantitative Monitoring of Software.” In <i>Software Verification</i>, 13124:3–6. LNCS. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">https://doi.org/10.1007/978-3-030-95561-8_1</a>."},"year":"2022","date_updated":"2023-08-03T06:11:55Z","external_id":{"isi":["000771713200001"]},"isi":1,"acknowledgement":"The formal framework for quantitative monitoring which is presented in this invited talk was defined jointly with N. Ege Saraç at LICS 2021. This work was supported in part by the Wittgenstein Award Z211-N23 of the Austrian Science Fund.","volume":13124,"article_processing_charge":"No","department":[{"_id":"ToHe"}],"date_created":"2022-03-20T23:01:40Z","publication_status":"published","intvolume":"     13124","title":"Quantitative monitoring of software","scopus_import":"1","_id":"10891","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"}],"publisher":"Springer Nature","quality_controlled":"1","series_title":"LNCS","page":"3-6"},{"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","file":[{"creator":"dernst","file_id":"11357","access_level":"open_access","success":1,"relation":"main_file","file_name":"2022_LNCS_Bartocci.pdf","content_type":"application/pdf","date_updated":"2022-05-09T06:52:44Z","file_size":479146,"checksum":"7f6f860b20b8de2a249e9c1b4eee15cf","date_created":"2022-05-09T06:52:44Z"}],"type":"conference","date_published":"2022-03-29T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"isbn":["9783030994280"],"issn":["0302-9743"],"eissn":["1611-3349"]},"language":[{"iso":"eng"}],"conference":{"location":"Munich, Germany","end_date":"2022-04-07","name":"FASE: Fundamental Approaches to Software Engineering","start_date":"2022-04-02"},"has_accepted_license":"1","publication":"Fundamental Approaches to Software Engineering","month":"03","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"oa_version":"Published Version","ddc":["000"],"acknowledgement":"This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 956123 and was funded in part by the FWF project W1255-N23 and by the ERC-2020-AdG 101020093.","volume":13241,"external_id":{"isi":["000782393600001"]},"isi":1,"citation":{"mla":"Bartocci, Ezio, et al. “Information-Flow Interfaces.” <i>Fundamental Approaches to Software Engineering</i>, vol. 13241, Springer Nature, 2022, pp. 3–22, doi:<a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">10.1007/978-3-030-99429-7_1</a>.","short":"E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2022, pp. 3–22.","ista":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Information-flow interfaces. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13241, 3–22.","ama":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Information-flow interfaces. In: <i>Fundamental Approaches to Software Engineering</i>. Vol 13241. Springer Nature; 2022:3-22. doi:<a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">10.1007/978-3-030-99429-7_1</a>","apa":"Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Da Costa, A. O. (2022). Information-flow interfaces. In <i>Fundamental Approaches to Software Engineering</i> (Vol. 13241, pp. 3–22). Munich, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">https://doi.org/10.1007/978-3-030-99429-7_1</a>","chicago":"Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Information-Flow Interfaces.” In <i>Fundamental Approaches to Software Engineering</i>, 13241:3–22. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">https://doi.org/10.1007/978-3-030-99429-7_1</a>.","ieee":"E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Information-flow interfaces,” in <i>Fundamental Approaches to Software Engineering</i>, Munich, Germany, 2022, vol. 13241, pp. 3–22."},"year":"2022","date_updated":"2023-08-03T07:03:40Z","abstract":[{"text":"Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees.\r\nAlthough there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory that is designed for ensuring system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. We illustrate the applicability of our framework with an example inspired from the automotive domain.","lang":"eng"}],"day":"29","doi":"10.1007/978-3-030-99429-7_1","file_date_updated":"2022-05-09T06:52:44Z","quality_controlled":"1","ec_funded":1,"page":"3-22","publisher":"Springer Nature","author":[{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas","first_name":"Thomas","last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","last_name":"Nickovic","first_name":"Dejan"},{"last_name":"Da Costa","first_name":"Ana Oliveira","full_name":"Da Costa, Ana Oliveira"}],"scopus_import":"1","_id":"11355","intvolume":"     13241","alternative_title":["LNCS"],"title":"Information-flow interfaces","department":[{"_id":"ToHe"}],"date_created":"2022-05-08T22:01:44Z","article_processing_charge":"No","publication_status":"published"},{"publisher":"Institute of Science and Technology Austria","page":"124","ec_funded":1,"file_date_updated":"2022-05-17T15:19:39Z","publication_status":"published","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2022-05-12T07:14:01Z","title":"Learning verifiable representations","alternative_title":["ISTA Thesis"],"_id":"11362","license":"https://creativecommons.org/licenses/by-nd/4.0/","author":[{"full_name":"Lechner, Mathias","first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"}],"ddc":["004"],"doi":"10.15479/at:ista:11362","degree_awarded":"PhD","day":"12","abstract":[{"lang":"eng","text":"Deep learning has enabled breakthroughs in challenging computing problems and has emerged as the standard problem-solving tool for computer vision and natural language processing tasks.\r\nOne exception to this trend is safety-critical tasks where robustness and resilience requirements contradict the black-box nature of neural networks. \r\nTo deploy deep learning methods for these tasks, it is vital to provide guarantees on neural network agents' safety and robustness criteria. \r\nThis can be achieved by developing formal verification methods to verify the safety and robustness properties of neural networks.\r\n\r\nOur goal is to design, develop and assess safety verification methods for neural networks to improve their reliability and trustworthiness in real-world applications.\r\nThis thesis establishes techniques for the verification of compressed and adversarially trained models as well as the design of novel neural networks for verifiably safe decision-making.\r\n\r\nFirst, we establish the problem of verifying quantized neural networks. Quantization is a technique that trades numerical precision for the computational efficiency of running a neural network and is widely adopted in industry.\r\nWe show that neglecting the reduced precision when verifying a neural network can lead to wrong conclusions about the robustness and safety of the network, highlighting that novel techniques for quantized network verification are necessary. We introduce several bit-exact verification methods explicitly designed for quantized neural networks and experimentally confirm on realistic networks that the network's robustness and other formal properties are affected by the quantization.\r\n\r\nFurthermore, we perform a case study providing evidence that adversarial training, a standard technique for making neural networks more robust, has detrimental effects on the network's performance. This robustness-accuracy tradeoff has been studied before regarding the accuracy obtained on classification datasets where each data point is independent of all other data points. On the other hand, we investigate the tradeoff empirically in robot learning settings where a both, a high accuracy and a high robustness, are desirable.\r\nOur results suggest that the negative side-effects of adversarial training outweigh its robustness benefits in practice.\r\n\r\nFinally, we consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with systems over the infinite time horizon. Bayesian neural networks are probabilistic models for learning uncertainties in the data and are therefore often used on robotic and healthcare applications where data is inherently stochastic.\r\nWe introduce a method for recalibrating Bayesian neural networks so that they yield probability distributions over safe decisions only.\r\nOur method learns a safety certificate that guarantees safety over the infinite time horizon to determine which decisions are safe in every possible state of the system.\r\nWe demonstrate the effectiveness of our approach on a series of reinforcement learning benchmarks."}],"date_updated":"2025-07-14T09:10:11Z","year":"2022","citation":{"ista":"Lechner M. 2022. Learning verifiable representations. Institute of Science and Technology Austria.","mla":"Lechner, Mathias. <i>Learning Verifiable Representations</i>. Institute of Science and Technology Austria, 2022, doi:<a href=\"https://doi.org/10.15479/at:ista:11362\">10.15479/at:ista:11362</a>.","short":"M. Lechner, Learning Verifiable Representations, Institute of Science and Technology Austria, 2022.","ieee":"M. Lechner, “Learning verifiable representations,” Institute of Science and Technology Austria, 2022.","chicago":"Lechner, Mathias. “Learning Verifiable Representations.” Institute of Science and Technology Austria, 2022. <a href=\"https://doi.org/10.15479/at:ista:11362\">https://doi.org/10.15479/at:ista:11362</a>.","ama":"Lechner M. Learning verifiable representations. 2022. doi:<a href=\"https://doi.org/10.15479/at:ista:11362\">10.15479/at:ista:11362</a>","apa":"Lechner, M. (2022). <i>Learning verifiable representations</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:11362\">https://doi.org/10.15479/at:ista:11362</a>"},"language":[{"iso":"eng"}],"keyword":["neural networks","verification","machine learning"],"oa_version":"Published Version","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"month":"05","has_accepted_license":"1","file":[{"content_type":"application/zip","file_name":"src.zip","date_updated":"2022-05-13T12:49:00Z","checksum":"8eefa9c7c10ca7e1a2ccdd731962a645","file_size":13210143,"date_created":"2022-05-13T12:33:26Z","creator":"mlechner","file_id":"11378","relation":"source_file","access_level":"closed"},{"access_level":"open_access","relation":"main_file","file_id":"11382","creator":"mlechner","date_created":"2022-05-16T08:02:28Z","checksum":"1b9e1e5a9a83ed9d89dad2f5133dc026","file_size":2732536,"date_updated":"2022-05-17T15:19:39Z","file_name":"thesis_main-a2.pdf","content_type":"application/pdf"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","related_material":{"record":[{"id":"11366","relation":"part_of_dissertation","status":"public"},{"id":"7808","relation":"part_of_dissertation","status":"public"},{"id":"10666","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"10665","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"10667"}]},"status":"public","publication_identifier":{"isbn":["978-3-99078-017-6"]},"supervisor":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"},"date_published":"2022-05-12T00:00:00Z","type":"dissertation"},{"date_published":"2022-04-15T00:00:00Z","external_id":{"arxiv":["2204.07373"]},"type":"preprint","date_updated":"2023-08-01T13:36:50Z","year":"2022","citation":{"ista":"Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. arXiv, 2204.07373.","mla":"Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” <i>ArXiv</i>, 2204.07373, doi:<a href=\"https://doi.org/10.48550/arXiv.2204.07373\">10.48550/arXiv.2204.07373</a>.","short":"M. Lechner, A. Amini, D. Rus, T.A. Henzinger, ArXiv (n.d.).","chicago":"Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2204.07373\">https://doi.org/10.48550/arXiv.2204.07373</a>.","ieee":"M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial robustness-accuracy tradeoff in robot learning,” <i>arXiv</i>. .","ama":"Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2204.07373\">10.48550/arXiv.2204.07373</a>","apa":"Lechner, M., Amini, A., Rus, D., &#38; Henzinger, T. A. (n.d.). Revisiting the adversarial robustness-accuracy tradeoff in robot learning. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2204.07373\">https://doi.org/10.48550/arXiv.2204.07373</a>"},"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\r\ncome 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\r\nbut 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\r\nconjunction with adversarial robot learning can make adversarial training suitable for real-world robot applications. We evaluate a wide variety of robot learning tasks ranging from autonomous driving in a high-fidelity environment\r\namenable to sim-to-real deployment, to mobile robot gesture recognition. Our results demonstrate that, while these techniques make incremental improvements on the trade-off on a relative scale, the negative side-effects caused by\r\nadversarial training still outweigh the improvements by an order of magnitude. We conclude that more substantial advances in robust learning methods are necessary before they can benefit robot learning tasks in practice."}],"oa":1,"arxiv":1,"doi":"10.48550/arXiv.2204.07373","day":"15","related_material":{"record":[{"relation":"dissertation_contains","id":"11362","status":"public"},{"id":"12704","relation":"later_version","status":"public"}]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","acknowledgement":"This work was supported in parts by the ERC-2020-AdG 101020093, National Science Foundation (NSF), and JP\r\nMorgan Graduate Fellowships. We thank Christoph Lampert for inspiring this work.\r\n","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2204.07373"}],"author":[{"last_name":"Lechner","first_name":"Mathias","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Amini, Alexander","last_name":"Amini","first_name":"Alexander"},{"last_name":"Rus","first_name":"Daniela","full_name":"Rus, Daniela"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publication":"arXiv","_id":"11366","title":"Revisiting the adversarial robustness-accuracy tradeoff in robot learning","month":"04","article_number":"2204.07373","oa_version":"Preprint","publication_status":"submitted","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"date_created":"2022-05-12T13:20:17Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"ec_funded":1},{"file":[{"success":1,"access_level":"open_access","relation":"main_file","creator":"dernst","file_id":"12317","file_size":477110,"checksum":"05c7dcfbb9053a98f46441fb2eccb213","date_created":"2023-01-20T07:34:50Z","file_name":"2022_LNCS_RV_Henzinger.pdf","content_type":"application/pdf","date_updated":"2023-01-20T07:34:50Z"}],"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publication_identifier":{"issn":["0302-9743"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2022-09-23T00:00:00Z","conference":{"start_date":"2022-09-28","name":"RV: Runtime Verification","end_date":"2022-09-30","location":"Tbilisi, Georgia"},"language":[{"iso":"eng"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"oa_version":"Published Version","month":"09","has_accepted_license":"1","publication":"22nd International Conference on Runtime Verification","acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","volume":13498,"ddc":["000"],"day":"23","doi":"10.1007/978-3-031-17196-3_11","abstract":[{"lang":"eng","text":"Quantitative monitoring can be universal and approximate: For every finite sequence of observations, the specification provides a value and the monitor outputs a best-effort approximation of it. The quality of the approximation may depend on the resources that are available to the monitor. By taking to the limit the sequences of specification values and monitor outputs, we obtain precision-resource trade-offs also for limit monitoring. This paper provides a formal framework for studying such trade-offs using an abstract interpretation for monitors: For each natural number n, the aggregate semantics of a monitor at time n is an equivalence relation over all sequences of at most n observations so that two equivalent sequences are indistinguishable to the monitor and thus mapped to the same output. This abstract interpretation of quantitative monitors allows us to measure the number of equivalence classes (or “resource use”) that is necessary for a certain precision up to a certain time, or at any time. Our framework offers several insights. For example, we identify a family of specifications for which any resource-optimal exact limit monitor is independent of any error permitted over finite traces. Moreover, we present a specification for which any resource-optimal approximate limit monitor does not minimize its resource use at any time. "}],"year":"2022","citation":{"ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Abstract monitors for quantitative specifications,” in <i>22nd International Conference on Runtime Verification</i>, Tbilisi, Georgia, 2022, vol. 13498, pp. 200–220.","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Abstract Monitors for Quantitative Specifications.” In <i>22nd International Conference on Runtime Verification</i>, 13498:200–220. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">https://doi.org/10.1007/978-3-031-17196-3_11</a>.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Abstract monitors for quantitative specifications. In: <i>22nd International Conference on Runtime Verification</i>. Vol 13498. Springer Nature; 2022:200-220. doi:<a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">10.1007/978-3-031-17196-3_11</a>","apa":"Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2022). Abstract monitors for quantitative specifications. In <i>22nd International Conference on Runtime Verification</i> (Vol. 13498, pp. 200–220). Tbilisi, Georgia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">https://doi.org/10.1007/978-3-031-17196-3_11</a>","ista":"Henzinger TA, Mazzocchi NA, Sarac NE. 2022. Abstract monitors for quantitative specifications. 22nd International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 13498, 200–220.","mla":"Henzinger, Thomas A., et al. “Abstract Monitors for Quantitative Specifications.” <i>22nd International Conference on Runtime Verification</i>, vol. 13498, Springer Nature, 2022, pp. 200–20, doi:<a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">10.1007/978-3-031-17196-3_11</a>.","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 22nd International Conference on Runtime Verification, Springer Nature, 2022, pp. 200–220."},"date_updated":"2023-08-03T13:38:46Z","external_id":{"isi":["000866539700011"]},"isi":1,"publisher":"Springer Nature","quality_controlled":"1","ec_funded":1,"page":"200-220","file_date_updated":"2023-01-20T07:34:50Z","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"article_processing_charge":"Yes","date_created":"2022-08-08T17:09:09Z","publication_status":"published","intvolume":"     13498","alternative_title":["LNCS"],"title":"Abstract monitors for quantitative specifications","scopus_import":"1","_id":"11775","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","full_name":"Mazzocchi, Nicolas Adrien","first_name":"Nicolas Adrien","last_name":"Mazzocchi"},{"full_name":"Sarac, Naci E","first_name":"Naci E","last_name":"Sarac","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}]},{"type":"preprint","external_id":{"arxiv":["2210.05308"]},"date_published":"2022-11-29T00:00:00Z","citation":{"short":"D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, ArXiv (n.d.).","mla":"Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>ArXiv</i>, doi:<a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">10.48550/ARXIV.2210.05308</a>.","ista":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. arXiv, <a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">10.48550/ARXIV.2210.05308</a>.","ama":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">10.48550/ARXIV.2210.05308</a>","apa":"Zikelic, D., Lechner, M., Henzinger, T. A., &#38; Chatterjee, K. (n.d.). Learning control policies for stochastic systems with reach-avoid guarantees. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">https://doi.org/10.48550/ARXIV.2210.05308</a>","chicago":"Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">https://doi.org/10.48550/ARXIV.2210.05308</a>.","ieee":"D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” <i>arXiv</i>. ."},"year":"2022","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-sa/4.0/legalcode","short":"CC BY-SA (4.0)","name":"Creative Commons Attribution-ShareAlike 4.0 International Public License (CC BY-SA 4.0)","image":"/images/cc_by_sa.png"},"date_updated":"2025-07-14T09:10:02Z","oa":1,"abstract":[{"text":"We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold $p\\in[0,1]$ over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on $3$ stochastic non-linear reinforcement learning tasks.","lang":"eng"}],"day":"29","doi":"10.48550/ARXIV.2210.05308","arxiv":1,"related_material":{"record":[{"id":"14539","relation":"dissertation_contains","status":"public"},{"relation":"later_version","id":"14830","status":"public"}]},"status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","main_file_link":[{"url":"https://arxiv.org/abs/2210.05308","open_access":"1"}],"author":[{"orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"license":"https://creativecommons.org/licenses/by-sa/4.0/","_id":"14600","publication":"arXiv","title":"Learning control policies for stochastic systems with reach-avoid guarantees","month":"11","article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"},{"grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"date_created":"2023-11-24T13:10:09Z","publication_status":"submitted","oa_version":"Preprint","language":[{"iso":"eng"}],"ec_funded":1},{"author":[{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"14601","publication":"arXiv","title":"Learning stabilizing policies in stochastic control systems","month":"05","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"}],"date_created":"2023-11-24T13:22:30Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"submitted","oa_version":"Preprint","language":[{"iso":"eng"}],"ec_funded":1,"external_id":{"arxiv":["2205.11991"]},"type":"preprint","date_published":"2022-05-24T00:00:00Z","citation":{"chicago":"Zikelic, Dorde, Mathias Lechner, Krishnendu Chatterjee, and Thomas A Henzinger. “Learning Stabilizing Policies in Stochastic Control Systems.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2205.11991\">https://doi.org/10.48550/arXiv.2205.11991</a>.","ieee":"D. Zikelic, M. Lechner, K. Chatterjee, and T. A. Henzinger, “Learning stabilizing policies in stochastic control systems,” <i>arXiv</i>. .","apa":"Zikelic, D., Lechner, M., Chatterjee, K., &#38; Henzinger, T. A. (n.d.). Learning stabilizing policies in stochastic control systems. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2205.11991\">https://doi.org/10.48550/arXiv.2205.11991</a>","ama":"Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies in stochastic control systems. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2205.11991\">10.48550/arXiv.2205.11991</a>","ista":"Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies in stochastic control systems. arXiv, <a href=\"https://doi.org/10.48550/arXiv.2205.11991\">10.48550/arXiv.2205.11991</a>.","short":"D. Zikelic, M. Lechner, K. Chatterjee, T.A. Henzinger, ArXiv (n.d.).","mla":"Zikelic, Dorde, et al. “Learning Stabilizing Policies in Stochastic Control Systems.” <i>ArXiv</i>, doi:<a href=\"https://doi.org/10.48550/arXiv.2205.11991\">10.48550/arXiv.2205.11991</a>."},"year":"2022","date_updated":"2025-07-14T09:10:00Z","oa":1,"abstract":[{"lang":"eng","text":"In this work, we address the problem of learning provably stable neural\r\nnetwork policies for stochastic control systems. While recent work has\r\ndemonstrated the feasibility of certifying given policies using martingale\r\ntheory, the problem of how to learn such policies is little explored. Here, we\r\nstudy the effectiveness of jointly learning a policy together with a martingale\r\ncertificate that proves its stability using a single learning algorithm. We\r\nobserve that the joint optimization problem becomes easily stuck in local\r\nminima when starting from a randomly initialized policy. Our results suggest\r\nthat some form of pre-training of the policy is required for the joint\r\noptimization to repair and verify the policy successfully."}],"day":"24","doi":"10.48550/arXiv.2205.11991","arxiv":1,"status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","related_material":{"record":[{"status":"public","id":"14539","relation":"dissertation_contains"}]},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2205.11991"}]},{"author":[{"full_name":"Brunnbauer, Axel","last_name":"Brunnbauer","first_name":"Axel"},{"last_name":"Berducci","first_name":"Luigi","full_name":"Berducci, Luigi"},{"last_name":"Brandstatter","first_name":"Andreas","full_name":"Brandstatter, Andreas"},{"full_name":"Lechner, Mathias","first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Hasani","first_name":"Ramin","full_name":"Hasani, Ramin"},{"full_name":"Rus, Daniela","first_name":"Daniela","last_name":"Rus"},{"first_name":"Radu","last_name":"Grosu","full_name":"Grosu, Radu"}],"_id":"12010","scopus_import":"1","title":"Latent imagination facilitates zero-shot transfer in autonomous racing","publication_status":"published","date_created":"2022-09-04T22:02:02Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","page":"7513-7520","quality_controlled":"1","ec_funded":1,"publisher":"IEEE","external_id":{"arxiv":["2103.04909"]},"date_updated":"2022-09-05T08:46:12Z","citation":{"short":"A. Brunnbauer, L. Berducci, A. Brandstatter, M. Lechner, R. Hasani, D. Rus, R. Grosu, in:, 2022 International Conference on Robotics and Automation, IEEE, 2022, pp. 7513–7520.","mla":"Brunnbauer, Axel, et al. “Latent Imagination Facilitates Zero-Shot Transfer in Autonomous Racing.” <i>2022 International Conference on Robotics and Automation</i>, IEEE, 2022, pp. 7513–20, doi:<a href=\"https://doi.org/10.1109/ICRA46639.2022.9811650\">10.1109/ICRA46639.2022.9811650</a>.","ista":"Brunnbauer A, Berducci L, Brandstatter A, Lechner M, Hasani R, Rus D, Grosu R. 2022. Latent imagination facilitates zero-shot transfer in autonomous racing. 2022 International Conference on Robotics and Automation. ICRA: International Conference on Robotics and Automation, 7513–7520.","apa":"Brunnbauer, A., Berducci, L., Brandstatter, A., Lechner, M., Hasani, R., Rus, D., &#38; Grosu, R. (2022). Latent imagination facilitates zero-shot transfer in autonomous racing. In <i>2022 International Conference on Robotics and Automation</i> (pp. 7513–7520). Philadelphia, PA, United States: IEEE. <a href=\"https://doi.org/10.1109/ICRA46639.2022.9811650\">https://doi.org/10.1109/ICRA46639.2022.9811650</a>","ama":"Brunnbauer A, Berducci L, Brandstatter A, et al. Latent imagination facilitates zero-shot transfer in autonomous racing. In: <i>2022 International Conference on Robotics and Automation</i>. IEEE; 2022:7513-7520. doi:<a href=\"https://doi.org/10.1109/ICRA46639.2022.9811650\">10.1109/ICRA46639.2022.9811650</a>","chicago":"Brunnbauer, Axel, Luigi Berducci, Andreas Brandstatter, Mathias Lechner, Ramin Hasani, Daniela Rus, and Radu Grosu. “Latent Imagination Facilitates Zero-Shot Transfer in Autonomous Racing.” In <i>2022 International Conference on Robotics and Automation</i>, 7513–20. IEEE, 2022. <a href=\"https://doi.org/10.1109/ICRA46639.2022.9811650\">https://doi.org/10.1109/ICRA46639.2022.9811650</a>.","ieee":"A. Brunnbauer <i>et al.</i>, “Latent imagination facilitates zero-shot transfer in autonomous racing,” in <i>2022 International Conference on Robotics and Automation</i>, Philadelphia, PA, United States, 2022, pp. 7513–7520."},"year":"2022","abstract":[{"lang":"eng","text":"World models learn behaviors in a latent imagination space to enhance the sample-efficiency of deep reinforcement learning (RL) algorithms. While learning world models for high-dimensional observations (e.g., pixel inputs) has become practicable on standard RL benchmarks and some games, their effectiveness in real-world robotics applications has not been explored. In this paper, we investigate how such agents generalize to real-world autonomous vehicle control tasks, where advanced model-free deep RL algorithms fail. In particular, we set up a series of time-lap tasks for an F1TENTH racing robot, equipped with a high-dimensional LiDAR sensor, on a set of test tracks with a gradual increase in their complexity. In this continuous-control setting, we show that model-based agents capable of learning in imagination substantially outperform model-free agents with respect to performance, sample efficiency, successful task completion, and generalization. Moreover, we show that the generalization ability of model-based agents strongly depends on the choice of their observation model. We provide extensive empirical evidence for the effectiveness of world models provided with long enough memory horizons in sim2real tasks."}],"doi":"10.1109/ICRA46639.2022.9811650","arxiv":1,"day":"12","acknowledgement":"L.B. was supported by the Doctoral College Resilient Embedded Systems. M.L. was supported in part by the ERC2020-AdG 101020093 and the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). R.H. and D.R. were supported by The Boeing Company and the Office of Naval Research (ONR) Grant N00014-18-1-2830. R.G. was partially supported by the Horizon-2020 ECSEL Project grant No. 783163 (iDev40) and A.B. by FFG Project ADEX.","publication":"2022 International Conference on Robotics and Automation","month":"07","oa_version":"Preprint","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"language":[{"iso":"eng"}],"conference":{"location":"Philadelphia, PA, United States","end_date":"2022-05-27","name":"ICRA: International Conference on Robotics and Automation","start_date":"2022-05-23"},"date_published":"2022-07-12T00:00:00Z","type":"conference","oa":1,"publication_identifier":{"issn":["1050-4729"],"isbn":["9781728196817"]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2103.04909"}]},{"abstract":[{"lang":"eng","text":"Continuous-time neural networks are a class of machine learning systems that can tackle representation learning on spatiotemporal decision-making tasks. These models are typically represented by continuous differential equations. However, their expressive power when they are deployed on computers is bottlenecked by numerical differential equation solvers. This limitation has notably slowed down the scaling and understanding of numerous natural physical phenomena such as the dynamics of nervous systems. Ideally, we would circumvent this bottleneck by solving the given dynamical system in closed form. This is known to be intractable in general. Here, we show that it is possible to closely approximate the interaction between neurons and synapses—the building blocks of natural and artificial neural networks—constructed by liquid time-constant networks efficiently in closed form. To this end, we compute a tightly bounded approximation of the solution of an integral appearing in liquid time-constant dynamics that has had no known closed-form solution so far. This closed-form solution impacts the design of continuous-time and continuous-depth neural models. For instance, since time appears explicitly in closed form, the formulation relaxes the need for complex numerical solvers. Consequently, we obtain models that are between one and five orders of magnitude faster in training and inference compared with differential equation-based counterparts. More importantly, in contrast to ordinary differential equation-based continuous networks, closed-form networks can scale remarkably well compared with other deep learning instances. Lastly, as these models are derived from liquid networks, they show good performance in time-series modelling compared with advanced recurrent neural network models."}],"day":"15","doi":"10.1038/s42256-022-00556-7","arxiv":1,"external_id":{"arxiv":["2106.13898"],"isi":["000884215600003"]},"isi":1,"citation":{"ista":"Hasani R, Lechner M, Amini A, Liebenwein L, Ray A, Tschaikowski M, Teschl G, Rus D. 2022. Closed-form continuous-time neural networks. Nature Machine Intelligence. 4(11), 992–1003.","mla":"Hasani, Ramin, et al. “Closed-Form Continuous-Time Neural Networks.” <i>Nature Machine Intelligence</i>, vol. 4, no. 11, Springer Nature, 2022, pp. 992–1003, doi:<a href=\"https://doi.org/10.1038/s42256-022-00556-7\">10.1038/s42256-022-00556-7</a>.","short":"R. Hasani, M. Lechner, A. Amini, L. Liebenwein, A. Ray, M. Tschaikowski, G. Teschl, D. Rus, Nature Machine Intelligence 4 (2022) 992–1003.","ieee":"R. Hasani <i>et al.</i>, “Closed-form continuous-time neural networks,” <i>Nature Machine Intelligence</i>, vol. 4, no. 11. Springer Nature, pp. 992–1003, 2022.","chicago":"Hasani, Ramin, Mathias Lechner, Alexander Amini, Lucas Liebenwein, Aaron Ray, Max Tschaikowski, Gerald Teschl, and Daniela Rus. “Closed-Form Continuous-Time Neural Networks.” <i>Nature Machine Intelligence</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1038/s42256-022-00556-7\">https://doi.org/10.1038/s42256-022-00556-7</a>.","apa":"Hasani, R., Lechner, M., Amini, A., Liebenwein, L., Ray, A., Tschaikowski, M., … Rus, D. (2022). Closed-form continuous-time neural networks. <i>Nature Machine Intelligence</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s42256-022-00556-7\">https://doi.org/10.1038/s42256-022-00556-7</a>","ama":"Hasani R, Lechner M, Amini A, et al. Closed-form continuous-time neural networks. <i>Nature Machine Intelligence</i>. 2022;4(11):992-1003. doi:<a href=\"https://doi.org/10.1038/s42256-022-00556-7\">10.1038/s42256-022-00556-7</a>"},"year":"2022","date_updated":"2023-08-04T09:00:10Z","ddc":["000"],"volume":4,"acknowledgement":"This research was supported in part by the AI2050 program at Schmidt Futures (grant G-22-63172), the Boeing Company, and the United States Air Force Research Laboratory and the United States Air Force Artificial Intelligence Accelerator and was accomplished under cooperative agreement number FA8750-19-2-1000. 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, of 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 notation herein. This work was further supported by The Boeing Company and Office of Naval Research grant N00014-18-1-2830. M.T. is supported by the Poul Due Jensen Foundation, grant 883901. M.L. was supported in part by the Austrian Science Fund under grant Z211-N23 (Wittgenstein Award). A.A. was supported by the National Science Foundation Graduate Research Fellowship Program. We thank T.-H. Wang, P. Kao, M. Chahine, W. Xiao, X. Li, L. Yin and Y. Ben for useful suggestions and for testing of CfC models to confirm the results across other domains.","intvolume":"         4","title":"Closed-form continuous-time neural networks","date_created":"2023-01-12T12:07:21Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","issue":"11","author":[{"full_name":"Hasani, Ramin","first_name":"Ramin","last_name":"Hasani"},{"full_name":"Lechner, Mathias","first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Amini, Alexander","first_name":"Alexander","last_name":"Amini"},{"first_name":"Lucas","last_name":"Liebenwein","full_name":"Liebenwein, Lucas"},{"last_name":"Ray","first_name":"Aaron","full_name":"Ray, Aaron"},{"full_name":"Tschaikowski, Max","first_name":"Max","last_name":"Tschaikowski"},{"last_name":"Teschl","first_name":"Gerald","full_name":"Teschl, Gerald"},{"first_name":"Daniela","last_name":"Rus","full_name":"Rus, Daniela"}],"scopus_import":"1","_id":"12147","article_type":"original","publisher":"Springer Nature","file_date_updated":"2023-01-24T09:49:44Z","quality_controlled":"1","page":"992-1003","oa":1,"publication_identifier":{"issn":["2522-5839"]},"type":"journal_article","date_published":"2022-11-15T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","related_material":{"link":[{"relation":"erratum","url":"https://doi.org/10.1038/s42256-022-00597-y"}]},"file":[{"relation":"main_file","success":1,"access_level":"open_access","creator":"dernst","file_id":"12355","checksum":"b4789122ce04bfb4ac042390f59aaa8b","file_size":3259553,"date_created":"2023-01-24T09:49:44Z","content_type":"application/pdf","file_name":"2022_NatureMachineIntelligence_Hasani.pdf","date_updated":"2023-01-24T09:49:44Z"}],"month":"11","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","has_accepted_license":"1","publication":"Nature Machine Intelligence","keyword":["Artificial Intelligence","Computer Networks and Communications","Computer Vision and Pattern Recognition","Human-Computer Interaction","Software"],"language":[{"iso":"eng"}]}]