[{"publication":"Theoretical Computer Science","day":"04","year":"2021","isi":1,"has_accepted_license":"1","date_created":"2021-07-11T22:01:18Z","doi":"10.1016/j.tcs.2021.05.023","date_published":"2021-06-04T00:00:00Z","page":"1-16","acknowledgement":"Tatjana Petrov’s research was supported in part by SNSF Advanced Postdoctoral Mobility Fellowship grant number P300P2 161067, the Ministry of Science, Research and the Arts of the state of Baden-Wurttemberg, and the DFG Centre of Excellence 2117 ‘Centre for the Advanced Study of Collective Behaviour’ (ID: 422037984). Claudia Igler is the recipient of a DOC Fellowship of the Austrian Academy of Sciences. Thomas A. Henzinger’s research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","oa":1,"publisher":"Elsevier","quality_controlled":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"chicago":"Petrov, Tatjana, Claudia Igler, Ali Sezgin, Thomas A Henzinger, and Calin C Guet. “Long Lived Transients in Gene Regulation.” Theoretical Computer Science. Elsevier, 2021. https://doi.org/10.1016/j.tcs.2021.05.023.","ista":"Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. 2021. Long lived transients in gene regulation. Theoretical Computer Science. 893, 1–16.","mla":"Petrov, Tatjana, et al. “Long Lived Transients in Gene Regulation.” Theoretical Computer Science, vol. 893, Elsevier, 2021, pp. 1–16, doi:10.1016/j.tcs.2021.05.023.","ama":"Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. Long lived transients in gene regulation. Theoretical Computer Science. 2021;893:1-16. doi:10.1016/j.tcs.2021.05.023","apa":"Petrov, T., Igler, C., Sezgin, A., Henzinger, T. A., & Guet, C. C. (2021). Long lived transients in gene regulation. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2021.05.023","ieee":"T. Petrov, C. Igler, A. Sezgin, T. A. Henzinger, and C. C. Guet, “Long lived transients in gene regulation,” Theoretical Computer Science, vol. 893. Elsevier, pp. 1–16, 2021.","short":"T. Petrov, C. Igler, A. Sezgin, T.A. Henzinger, C.C. Guet, Theoretical Computer Science 893 (2021) 1–16."},"title":"Long lived transients in gene regulation","external_id":{"isi":["000710180500002"]},"article_processing_charge":"No","author":[{"full_name":"Petrov, Tatjana","last_name":"Petrov","first_name":"Tatjana"},{"id":"46613666-F248-11E8-B48F-1D18A9856A87","first_name":"Claudia","last_name":"Igler","full_name":"Igler, Claudia"},{"first_name":"Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","full_name":"Sezgin, Ali","last_name":"Sezgin"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"},{"first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","last_name":"Guet","full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052"}],"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"d3aef34cfb13e53bba4cf44d01680793","file_id":"11364","success":1,"date_updated":"2022-05-12T12:13:27Z","file_size":2566504,"creator":"dernst","date_created":"2022-05-12T12:13:27Z","file_name":"2021_TheoreticalComputerScience_Petrov.pdf"}],"publication_status":"published","publication_identifier":{"issn":["0304-3975"]},"volume":893,"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Gene expression is regulated by the set of transcription factors (TFs) that bind to the promoter. The ensuing regulating function is often represented as a combinational logic circuit, where output (gene expression) is determined by current input values (promoter bound TFs) only. However, the simultaneous arrival of TFs is a strong assumption, since transcription and translation of genes introduce intrinsic time delays and there is no global synchronisation among the arrival times of different molecular species at their targets. We present an experimentally implementable genetic circuit with two inputs and one output, which in the presence of small delays in input arrival, exhibits qualitatively distinct population-level phenotypes, over timescales that are longer than typical cell doubling times. From a dynamical systems point of view, these phenotypes represent long-lived transients: although they converge to the same value eventually, they do so after a very long time span. The key feature of this toy model genetic circuit is that, despite having only two inputs and one output, it is regulated by twenty-three distinct DNA-TF configurations, two of which are more stable than others (DNA looped states), one promoting and another blocking the expression of the output gene. Small delays in input arrival time result in a majority of cells in the population quickly reaching the stable state associated with the first input, while exiting of this stable state occurs at a slow timescale. In order to mechanistically model the behaviour of this genetic circuit, we used a rule-based modelling language, and implemented a grid-search to find parameter combinations giving rise to long-lived transients. Our analysis shows that in the absence of feedback, there exist path-dependent gene regulatory mechanisms based on the long timescale of transients. The behaviour of this toy model circuit suggests that gene regulatory networks can exploit event timing to create phenotypes, and it opens the possibility that they could use event timing to memorise events, without regulatory feedback. The model reveals the importance of (i) mechanistically modelling the transitions between the different DNA-TF states, and (ii) employing transient analysis thereof."}],"intvolume":" 893","month":"06","scopus_import":"1","ddc":["004"],"date_updated":"2023-08-10T14:11:19Z","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"file_date_updated":"2022-05-12T12:13:27Z","_id":"9647","status":"public","tmp":{"short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png"},"type":"journal_article","article_type":"original"},{"abstract":[{"text":"We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.","lang":"eng"}],"oa_version":"Preprint","scopus_import":"1","alternative_title":["LNCS"],"place":"Cham","month":"10","intvolume":" 12974","publication_identifier":{"eisbn":["978-3-030-88494-9"],"eissn":["1611-3349"],"isbn":["978-3-030-88493-2"],"issn":["0302-9743"]},"publication_status":"published","file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","success":1,"checksum":"554c7fdb259eda703a8b6328a6dad55a","file_id":"10109","creator":"fmuehlbo","file_size":350632,"date_updated":"2021-10-07T23:32:18Z","file_name":"differentialmonitoring-cameraready-openaccess.pdf","date_created":"2021-10-07T23:32:18Z"}],"language":[{"iso":"eng"}],"related_material":{"record":[{"id":"9946","status":"public","relation":"extended_version"}]},"volume":12974,"_id":"10108","type":"conference","conference":{"start_date":"2021-10-11","end_date":"2021-10-14","location":"Virtual","name":"RV: Runtime Verification"},"status":"public","keyword":["run-time verification","software engineering","implicit specification"],"date_updated":"2023-08-14T07:20:30Z","ddc":["005"],"department":[{"_id":"ToHe"}],"file_date_updated":"2021-10-07T23:32:18Z","acknowledgement":"The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer, Adrian Francalanza, Owolabi Legunsen, Mae Milano, Manuel Rigger, Cesar Sanchez, and the members of the IST Verification Seminar for their helpful comments and insights on various stages of this work, as well as the reviewers of RV’21 for their helpful suggestions on the actual paper.","quality_controlled":"1","publisher":"Springer Nature","oa":1,"isi":1,"has_accepted_license":"1","year":"2021","day":"06","publication":"International Conference on Runtime Verification","page":"231-243","doi":"10.1007/978-3-030-88494-9_12","date_published":"2021-10-06T00:00:00Z","date_created":"2021-10-07T23:30:10Z","project":[{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"citation":{"mla":"Mühlböck, Fabian, and Thomas A. Henzinger. “Differential Monitoring.” International Conference on Runtime Verification, vol. 12974, Springer Nature, 2021, pp. 231–43, doi:10.1007/978-3-030-88494-9_12.","short":"F. Mühlböck, T.A. Henzinger, in:, International Conference on Runtime Verification, Springer Nature, Cham, 2021, pp. 231–243.","ieee":"F. Mühlböck and T. A. Henzinger, “Differential monitoring,” in International Conference on Runtime Verification, Virtual, 2021, vol. 12974, pp. 231–243.","apa":"Mühlböck, F., & Henzinger, T. A. (2021). Differential monitoring. In International Conference on Runtime Verification (Vol. 12974, pp. 231–243). Cham: Springer Nature. https://doi.org/10.1007/978-3-030-88494-9_12","ama":"Mühlböck F, Henzinger TA. Differential monitoring. In: International Conference on Runtime Verification. Vol 12974. Cham: Springer Nature; 2021:231-243. doi:10.1007/978-3-030-88494-9_12","chicago":"Mühlböck, Fabian, and Thomas A Henzinger. “Differential Monitoring.” In International Conference on Runtime Verification, 12974:231–43. Cham: Springer Nature, 2021. https://doi.org/10.1007/978-3-030-88494-9_12.","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring. International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 231–243."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"last_name":"Mühlböck","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","first_name":"Fabian"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"}],"article_processing_charge":"No","external_id":{"isi":["000719383800012"]},"title":"Differential monitoring"},{"_id":"9946","type":"technical_report","status":"public","keyword":["run-time verification","software engineering","implicit specification"],"date_updated":"2023-08-14T07:20:29Z","ddc":["005"],"department":[{"_id":"ToHe"}],"file_date_updated":"2021-09-03T12:34:28Z","abstract":[{"text":"We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["IST Austria Technical Report"],"month":"09","publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","file":[{"date_updated":"2021-09-03T12:34:28Z","file_size":"320453","creator":"fmuehlbo","date_created":"2021-08-20T19:59:44Z","file_name":"differentialmonitoring-techreport.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"0f9aafd59444cb6bdca6925d163ab946","file_id":"9948"}],"language":[{"iso":"eng"}],"related_material":{"record":[{"id":"9281","status":"public","relation":"other"},{"relation":"shorter_version","status":"public","id":"10108"}]},"project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"citation":{"chicago":"Mühlböck, Fabian, and Thomas A Henzinger. Differential Monitoring. IST Austria, 2021. https://doi.org/10.15479/AT:ISTA:9946.","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring, IST Austria, 17p.","mla":"Mühlböck, Fabian, and Thomas A. Henzinger. Differential Monitoring. IST Austria, 2021, doi:10.15479/AT:ISTA:9946.","ama":"Mühlböck F, Henzinger TA. Differential Monitoring. IST Austria; 2021. doi:10.15479/AT:ISTA:9946","apa":"Mühlböck, F., & Henzinger, T. A. (2021). Differential monitoring. IST Austria. https://doi.org/10.15479/AT:ISTA:9946","ieee":"F. Mühlböck and T. A. Henzinger, Differential monitoring. IST Austria, 2021.","short":"F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","author":[{"last_name":"Mühlböck","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"article_processing_charge":"No","title":"Differential monitoring","acknowledgement":"The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer, Adrian Francalanza, Owolabi Legunsen, Matthew Milano, Manuel Rigger, Cesar Sanchez, and the members of the IST Verification Seminar for their helpful comments and insights on various stages of this work, as well as the reviewers of RV’21 for their helpful suggestions on the actual paper.","publisher":"IST Austria","oa":1,"has_accepted_license":"1","year":"2021","day":"01","page":"17","date_published":"2021-09-01T00:00:00Z","doi":"10.15479/AT:ISTA:9946","date_created":"2021-08-20T20:00:37Z"},{"issue":"7","volume":40,"language":[{"iso":"eng"}],"publication_identifier":{"eissn":["1467-8659"],"issn":["0167-7055"]},"publication_status":"published","month":"11","intvolume":" 40","scopus_import":"1","main_file_link":[{"url":"https://arxiv.org/abs/2110.07667","open_access":"1"}],"oa_version":"Preprint","abstract":[{"text":"While convolutional neural networks (CNNs) have found wide adoption as state-of-the-art models for image-related tasks, their predictions are often highly sensitive to small input perturbations, which the human vision is robust against. This paper presents Perturber, a web-based application that allows users to instantaneously explore how CNN activations and predictions evolve when a 3D input scene is interactively perturbed. Perturber offers a large variety of scene modifications, such as camera controls, lighting and shading effects, background modifications, object morphing, as well as adversarial attacks, to facilitate the discovery of potential vulnerabilities. Fine-tuned model versions can be directly compared for qualitative evaluation of their robustness. Case studies with machine learning experts have shown that Perturber helps users to quickly generate hypotheses about model vulnerabilities and to qualitatively compare model behavior. Using quantitative analyses, we could replicate users’ insights with other CNN architectures and input images, yielding new insights about the vulnerability of adversarially trained models.","lang":"eng"}],"department":[{"_id":"ToHe"}],"date_updated":"2023-08-14T13:11:42Z","status":"public","type":"journal_article","article_type":"original","_id":"10404","date_published":"2021-11-27T00:00:00Z","doi":"10.1111/cgf.14418","date_created":"2021-12-05T23:01:40Z","page":"253-264","day":"27","publication":"Computer Graphics Forum","isi":1,"year":"2021","quality_controlled":"1","publisher":"Wiley","oa":1,"acknowledgement":"We thank Robert Geirhos and Roland Zimmermann for their participation in the case study and valuable feedback, Chris Olah and Nick Cammarata for valuable discussions in the early phase of the project, as well as the Distill Slack workspace as a platform for discussions. M.L. is supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). J.B. is supported by the German Federal Ministry of Education and Research\r\n(BMBF) through the Competence Center for Machine Learning (TUE.AI, FKZ 01IS18039A) and the International Max Planck Research School for Intelligent Systems (IMPRS-IS). R.H. is partially supported by Boeing and Horizon-2020 ECSEL (grant 783163, iDev40).\r\n","title":"Interactive analysis of CNN robustness","author":[{"first_name":"Stefan","last_name":"Sietzen","full_name":"Sietzen, Stefan"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias"},{"last_name":"Borowski","full_name":"Borowski, Judy","first_name":"Judy"},{"full_name":"Hasani, Ramin","last_name":"Hasani","first_name":"Ramin"},{"full_name":"Waldner, Manuela","last_name":"Waldner","first_name":"Manuela"}],"article_processing_charge":"No","external_id":{"isi":["000722952000024"],"arxiv":["2110.07667"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"apa":"Sietzen, S., Lechner, M., Borowski, J., Hasani, R., & Waldner, M. (2021). Interactive analysis of CNN robustness. Computer Graphics Forum. Wiley. https://doi.org/10.1111/cgf.14418","ama":"Sietzen S, Lechner M, Borowski J, Hasani R, Waldner M. Interactive analysis of CNN robustness. Computer Graphics Forum. 2021;40(7):253-264. doi:10.1111/cgf.14418","ieee":"S. Sietzen, M. Lechner, J. Borowski, R. Hasani, and M. Waldner, “Interactive analysis of CNN robustness,” Computer Graphics Forum, vol. 40, no. 7. Wiley, pp. 253–264, 2021.","short":"S. Sietzen, M. Lechner, J. Borowski, R. Hasani, M. Waldner, Computer Graphics Forum 40 (2021) 253–264.","mla":"Sietzen, Stefan, et al. “Interactive Analysis of CNN Robustness.” Computer Graphics Forum, vol. 40, no. 7, Wiley, 2021, pp. 253–64, doi:10.1111/cgf.14418.","ista":"Sietzen S, Lechner M, Borowski J, Hasani R, Waldner M. 2021. Interactive analysis of CNN robustness. Computer Graphics Forum. 40(7), 253–264.","chicago":"Sietzen, Stefan, Mathias Lechner, Judy Borowski, Ramin Hasani, and Manuela Waldner. “Interactive Analysis of CNN Robustness.” Computer Graphics Forum. Wiley, 2021. https://doi.org/10.1111/cgf.14418."},"project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}]},{"abstract":[{"lang":"eng","text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent, for example, the monetary value expressed in cents. We study, for the first time, the combination of discrete-bidding and infinite-duration games. Our most important result proves that these games form a large determined subclass of concurrent games, where determinacy is the strong property that there always exists exactly one player who can guarantee winning the game. In particular, we show that, in contrast to non-discrete bidding games, the mechanism with which tied bids are resolved plays an important role in discrete-bidding games. We study several natural tie-breaking mechanisms and show that, while some do not admit determinacy, most natural mechanisms imply determinacy for every pair of initial budgets."}],"oa_version":"Published Version","scopus_import":"1","month":"02","intvolume":" 17","publication_identifier":{"eissn":["1860-5974"]},"publication_status":"published","file":[{"file_name":"2021_LMCS_AGHAJOHAR.pdf","date_created":"2022-01-26T08:04:50Z","file_size":819878,"date_updated":"2022-01-26T08:04:50Z","creator":"alisjak","success":1,"checksum":"b35586a50ed1ca8f44767de116d18d81","file_id":"10690","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"language":[{"iso":"eng"}],"issue":"1","volume":17,"_id":"10674","article_type":"original","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","keyword":["computer science","computer science and game theory","logic in computer science"],"date_updated":"2023-08-17T06:56:42Z","ddc":["510"],"department":[{"_id":"ToHe"}],"file_date_updated":"2022-01-26T08:04:50Z","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M 2369-N33 (Meitner fellowship).\r\n","quality_controlled":"1","publisher":"International Federation for Computational Logic","oa":1,"has_accepted_license":"1","isi":1,"year":"2021","day":"03","publication":"Logical Methods in Computer Science","page":"10:1-10:23","doi":"10.23638/LMCS-17(1:10)2021","date_published":"2021-02-03T00:00:00Z","date_created":"2022-01-25T16:32:13Z","project":[{"grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"citation":{"short":"M. Aghajohari, G. Avni, T.A. Henzinger, Logical Methods in Computer Science 17 (2021) 10:1-10:23.","ieee":"M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding infinite-duration games,” Logical Methods in Computer Science, vol. 17, no. 1. International Federation for Computational Logic, p. 10:1-10:23, 2021.","apa":"Aghajohari, M., Avni, G., & Henzinger, T. A. (2021). Determinacy in discrete-bidding infinite-duration games. Logical Methods in Computer Science. International Federation for Computational Logic. https://doi.org/10.23638/LMCS-17(1:10)2021","ama":"Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration games. Logical Methods in Computer Science. 2021;17(1):10:1-10:23. doi:10.23638/LMCS-17(1:10)2021","mla":"Aghajohari, Milad, et al. “Determinacy in Discrete-Bidding Infinite-Duration Games.” Logical Methods in Computer Science, vol. 17, no. 1, International Federation for Computational Logic, 2021, p. 10:1-10:23, doi:10.23638/LMCS-17(1:10)2021.","ista":"Aghajohari M, Avni G, Henzinger TA. 2021. Determinacy in discrete-bidding infinite-duration games. Logical Methods in Computer Science. 17(1), 10:1-10:23.","chicago":"Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding Infinite-Duration Games.” Logical Methods in Computer Science. International Federation for Computational Logic, 2021. https://doi.org/10.23638/LMCS-17(1:10)2021."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"full_name":"Aghajohari, Milad","last_name":"Aghajohari","first_name":"Milad"},{"last_name":"Avni","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"external_id":{"isi":["000658724600010"],"arxiv":["1905.03588"]},"article_processing_charge":"No","title":"Determinacy in discrete-bidding infinite-duration games"},{"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"citation":{"mla":"Lechner, Mathias, et al. “Adversarial Training Is Not Ready for Robot Learning.” 2021 IEEE International Conference on Robotics and Automation, 2021, pp. 4140–47, doi:10.1109/ICRA48506.2021.9561036.","apa":"Lechner, M., Hasani, R., Grosu, R., Rus, D., & Henzinger, T. A. (2021). Adversarial training is not ready for robot learning. In 2021 IEEE International Conference on Robotics and Automation (pp. 4140–4147). Xi’an, China. https://doi.org/10.1109/ICRA48506.2021.9561036","ama":"Lechner M, Hasani R, Grosu R, Rus D, Henzinger TA. Adversarial training is not ready for robot learning. In: 2021 IEEE International Conference on Robotics and Automation. ICRA. ; 2021:4140-4147. doi:10.1109/ICRA48506.2021.9561036","short":"M. Lechner, R. Hasani, R. Grosu, D. Rus, T.A. Henzinger, in:, 2021 IEEE International Conference on Robotics and Automation, 2021, pp. 4140–4147.","ieee":"M. Lechner, R. Hasani, R. Grosu, D. Rus, and T. A. Henzinger, “Adversarial training is not ready for robot learning,” in 2021 IEEE International Conference on Robotics and Automation, Xi’an, China, 2021, pp. 4140–4147.","chicago":"Lechner, Mathias, Ramin Hasani, Radu Grosu, Daniela Rus, and Thomas A Henzinger. “Adversarial Training Is Not Ready for Robot Learning.” In 2021 IEEE International Conference on Robotics and Automation, 4140–47. ICRA, 2021. https://doi.org/10.1109/ICRA48506.2021.9561036.","ista":"Lechner M, Hasani R, Grosu R, Rus D, Henzinger TA. 2021. Adversarial training is not ready for robot learning. 2021 IEEE International Conference on Robotics and Automation. ICRA: International Conference on Robotics and AutomationICRA, 4140–4147."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","full_name":"Lechner, Mathias","last_name":"Lechner"},{"first_name":"Ramin","full_name":"Hasani, Ramin","last_name":"Hasani"},{"last_name":"Grosu","full_name":"Grosu, Radu","first_name":"Radu"},{"full_name":"Rus, Daniela","last_name":"Rus","first_name":"Daniela"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"external_id":{"isi":["000765738803040"],"arxiv":["2103.08187"]},"article_processing_charge":"No","title":"Adversarial training is not ready for robot learning","acknowledgement":"M.L. and T.A.H. are supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). R.H. and D.R. are supported by Boeing and R.G. by Horizon-2020 ECSEL Project grant no. 783163 (iDev40).","quality_controlled":"1","oa":1,"isi":1,"has_accepted_license":"1","year":"2021","publication":"2021 IEEE International Conference on Robotics and Automation","page":"4140-4147","doi":"10.1109/ICRA48506.2021.9561036","date_published":"2021-01-01T00:00:00Z","date_created":"2022-01-25T15:44:54Z","_id":"10666","series_title":"ICRA","type":"conference","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode","short":"CC BY-NC-ND (3.0)"},"conference":{"name":"ICRA: International Conference on Robotics and Automation","end_date":"2021-06-05","location":"Xi'an, China","start_date":"2021-05-30"},"status":"public","date_updated":"2023-08-17T06:58:38Z","ddc":["000"],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"abstract":[{"lang":"eng","text":"Adversarial training is an effective method to train deep learning models that are resilient to norm-bounded perturbations, with the cost of nominal performance drop. While adversarial training appears to enhance the robustness and safety of a deep model deployed in open-world decision-critical applications, counterintuitively, it induces undesired behaviors in robot learning settings. In this paper, we show theoretically and experimentally that neural controllers obtained via adversarial training are subjected to three types of defects, namely transient, systematic, and conditional errors. We first generalize adversarial training to a safety-domain optimization scheme allowing for more generic specifications. We then prove that such a learning process tends to cause certain error profiles. We support our theoretical results by a thorough experimental safety analysis in a robot-learning task. Our results suggest that adversarial training is not yet ready for robot learning."}],"oa_version":"None","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2103.08187"}],"publication_identifier":{"issn":["1050-4729"],"eissn":["2577-087X"],"isbn":["978-1-7281-9078-5"],"eisbn":["978-1-7281-9077-8"]},"publication_status":"published","language":[{"iso":"eng"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"11362","status":"public"}]},"license":"https://creativecommons.org/licenses/by-nc-nd/3.0/"},{"main_file_link":[{"url":"https://arxiv.org/abs/2009.06429","open_access":"1"}],"alternative_title":["LNCS"],"scopus_import":"1","place":"Cham","month":"10","abstract":[{"lang":"eng","text":"Neural-network classifiers achieve high accuracy when predicting the class of an input that they were trained to identify. Maintaining this accuracy in dynamic environments, where inputs frequently fall outside the fixed set of initially known classes, remains a challenge. The typical approach is to detect inputs from novel classes and retrain the classifier on an augmented dataset. However, not only the classifier but also the detection mechanism needs to adapt in order to distinguish between newly learned and yet unknown input classes. To address this challenge, we introduce an algorithmic framework for active monitoring of a neural network. A monitor wrapped in our framework operates in parallel with the neural network and interacts with a human user via a series of interpretable labeling queries for incremental adaptation. In addition, we propose an adaptive quantitative monitor to improve precision. An experimental evaluation on a diverse set of benchmarks with varying numbers of classes confirms the benefits of our active monitoring framework in dynamic scenarios."}],"oa_version":"Preprint","ec_funded":1,"volume":"12974 ","related_material":{"record":[{"relation":"extended_version","status":"public","id":"13234"}]},"publication_status":"published","publication_identifier":{"eisbn":["978-3-030-88494-9"],"issn":["0302-9743"],"isbn":["9-783-0308-8493-2"],"eissn":["1611-3349"]},"language":[{"iso":"eng"}],"conference":{"location":"Virtual","end_date":"2021-10-14","start_date":"2021-10-11","name":"RV: Runtime Verification"},"type":"conference","keyword":["monitoring","neural networks","novelty detection"],"status":"public","_id":"10206","department":[{"_id":"ToHe"}],"date_updated":"2024-01-30T12:06:56Z","oa":1,"publisher":"Springer Nature","quality_controlled":"1","acknowledgement":"We thank Christoph Lampert and Alex Greengold for fruitful discussions. This research was supported in part by the Simons Institute for the Theory of Computing, the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 754411.","page":"42-61","date_created":"2021-10-31T23:01:31Z","doi":"10.1007/978-3-030-88494-9_3","date_published":"2021-10-06T00:00:00Z","year":"2021","isi":1,"publication":"21st International Conference on Runtime Verification","day":"06","project":[{"name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"external_id":{"isi":["000719383800003"],"arxiv":["2009.06429"]},"article_processing_charge":"No","author":[{"last_name":"Lukina","full_name":"Lukina, Anna","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425","first_name":"Anna"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","last_name":"Schilling"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"title":"Into the unknown: active monitoring of neural networks","citation":{"chicago":"Lukina, Anna, Christian Schilling, and Thomas A Henzinger. “Into the Unknown: Active Monitoring of Neural Networks.” In 21st International Conference on Runtime Verification, 12974:42–61. Cham: Springer Nature, 2021. https://doi.org/10.1007/978-3-030-88494-9_3.","ista":"Lukina A, Schilling C, Henzinger TA. 2021. Into the unknown: active monitoring of neural networks. 21st International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 42–61.","mla":"Lukina, Anna, et al. “Into the Unknown: Active Monitoring of Neural Networks.” 21st International Conference on Runtime Verification, vol. 12974, Springer Nature, 2021, pp. 42–61, doi:10.1007/978-3-030-88494-9_3.","ieee":"A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: active monitoring of neural networks,” in 21st International Conference on Runtime Verification, Virtual, 2021, vol. 12974, pp. 42–61.","short":"A. Lukina, C. Schilling, T.A. Henzinger, in:, 21st International Conference on Runtime Verification, Springer Nature, Cham, 2021, pp. 42–61.","apa":"Lukina, A., Schilling, C., & Henzinger, T. A. (2021). Into the unknown: active monitoring of neural networks. In 21st International Conference on Runtime Verification (Vol. 12974, pp. 42–61). Cham: Springer Nature. https://doi.org/10.1007/978-3-030-88494-9_3","ama":"Lukina A, Schilling C, Henzinger TA. Into the unknown: active monitoring of neural networks. In: 21st International Conference on Runtime Verification. Vol 12974. Cham: Springer Nature; 2021:42-61. doi:10.1007/978-3-030-88494-9_3"},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8"},{"publication_status":"published","publication_identifier":{"issn":["2640-3498"]},"language":[{"iso":"eng"}],"file":[{"date_updated":"2022-01-26T11:08:51Z","file_size":2329798,"creator":"cchlebak","date_created":"2022-01-26T11:08:51Z","file_name":"2020_PMLR_Hasani.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"c9a4a29161777fc1a89ef451c040e3b1","file_id":"10691","success":1}],"abstract":[{"lang":"eng","text":"We propose a neural information processing system obtained by re-purposing the function of a biological neural circuit model to govern simulated and real-world control tasks. Inspired by the structure of the nervous system of the soil-worm, C. elegans, we introduce ordinary neural circuits (ONCs), defined as the model of biological neural circuits reparameterized for the control of alternative tasks. We first demonstrate that ONCs realize networks with higher maximum flow compared to arbitrary wired networks. We then learn instances of ONCs to control a series of robotic tasks, including the autonomous parking of a real-world rover robot. For reconfiguration of the purpose of the neural circuit, we adopt a search-based optimization algorithm. Ordinary neural circuits perform on par and, in some cases, significantly surpass the performance of contemporary deep learning models. ONC networks are compact, 77% sparser than their counterpart neural controllers, and their neural dynamics are fully interpretable at the cell-level."}],"oa_version":"Published Version","main_file_link":[{"open_access":"1","url":"http://proceedings.mlr.press/v119/hasani20a.html"}],"alternative_title":["PMLR"],"scopus_import":"1","date_updated":"2022-01-26T11:14:27Z","ddc":["000"],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file_date_updated":"2022-01-26T11:08:51Z","_id":"10673","series_title":"PMLR","conference":{"location":"Virtual","end_date":"2020-07-18","start_date":"2020-07-12","name":"ML: Machine Learning"},"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode","short":"CC BY-NC-ND (3.0)"},"type":"conference","status":"public","year":"2020","has_accepted_license":"1","publication":"Proceedings of the 37th International Conference on Machine Learning","page":"4082-4093","date_created":"2022-01-25T15:50:34Z","date_published":"2020-01-01T00:00:00Z","acknowledgement":"RH and RG are partially supported by Horizon-2020 ECSEL Project grant No. 783163 (iDev40), Productive 4.0, and ATBMBFW CPS-IoT Ecosystem. ML was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23\r\n(Wittgenstein Award). AA is supported by the National Science Foundation (NSF) Graduate Research Fellowship\r\nProgram. RH and DR are partially supported by The Boeing Company and JP Morgan Chase. This research work is\r\npartially drawn from the PhD dissertation of RH.\r\n","oa":1,"quality_controlled":"1","citation":{"chicago":"Hasani, Ramin, Mathias Lechner, Alexander Amini, Daniela Rus, and Radu Grosu. “A Natural Lottery Ticket Winner: Reinforcement Learning with Ordinary Neural Circuits.” In Proceedings of the 37th International Conference on Machine Learning, 4082–93. PMLR, 2020.","ista":"Hasani R, Lechner M, Amini A, Rus D, Grosu R. 2020. A natural lottery ticket winner: Reinforcement learning with ordinary neural circuits. Proceedings of the 37th International Conference on Machine Learning. ML: Machine LearningPMLR, PMLR, , 4082–4093.","mla":"Hasani, Ramin, et al. “A Natural Lottery Ticket Winner: Reinforcement Learning with Ordinary Neural Circuits.” Proceedings of the 37th International Conference on Machine Learning, 2020, pp. 4082–93.","ama":"Hasani R, Lechner M, Amini A, Rus D, Grosu R. A natural lottery ticket winner: Reinforcement learning with ordinary neural circuits. In: Proceedings of the 37th International Conference on Machine Learning. PMLR. ; 2020:4082-4093.","apa":"Hasani, R., Lechner, M., Amini, A., Rus, D., & Grosu, R. (2020). A natural lottery ticket winner: Reinforcement learning with ordinary neural circuits. In Proceedings of the 37th International Conference on Machine Learning (pp. 4082–4093). Virtual.","ieee":"R. Hasani, M. Lechner, A. Amini, D. Rus, and R. Grosu, “A natural lottery ticket winner: Reinforcement learning with ordinary neural circuits,” in Proceedings of the 37th International Conference on Machine Learning, Virtual, 2020, pp. 4082–4093.","short":"R. Hasani, M. Lechner, A. Amini, D. Rus, R. Grosu, in:, Proceedings of the 37th International Conference on Machine Learning, 2020, pp. 4082–4093."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","article_processing_charge":"No","author":[{"full_name":"Hasani, Ramin","last_name":"Hasani","first_name":"Ramin"},{"full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Amini","full_name":"Amini, Alexander","first_name":"Alexander"},{"first_name":"Daniela","last_name":"Rus","full_name":"Rus, Daniela"},{"first_name":"Radu","full_name":"Grosu, Radu","last_name":"Grosu"}],"title":"A natural lottery ticket winner: Reinforcement learning with ordinary neural circuits","project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}]},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Ferrere, Thomas, Thomas A Henzinger, and Bernhard Kragl. “Monitoring Event Frequencies.” In 28th EACSL Annual Conference on Computer Science Logic, Vol. 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CSL.2020.20.","ista":"Ferrere T, Henzinger TA, Kragl B. 2020. Monitoring event frequencies. 28th EACSL Annual Conference on Computer Science Logic. CSL: Computer Science Logic, LIPIcs, vol. 152, 20.","mla":"Ferrere, Thomas, et al. “Monitoring Event Frequencies.” 28th EACSL Annual Conference on Computer Science Logic, vol. 152, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.CSL.2020.20.","apa":"Ferrere, T., Henzinger, T. A., & Kragl, B. (2020). Monitoring event frequencies. In 28th EACSL Annual Conference on Computer Science Logic (Vol. 152). Barcelona, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2020.20","ama":"Ferrere T, Henzinger TA, Kragl B. Monitoring event frequencies. In: 28th EACSL Annual Conference on Computer Science Logic. Vol 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.CSL.2020.20","ieee":"T. Ferrere, T. A. Henzinger, and B. Kragl, “Monitoring event frequencies,” in 28th EACSL Annual Conference on Computer Science Logic, Barcelona, Spain, 2020, vol. 152.","short":"T. Ferrere, T.A. Henzinger, B. Kragl, in:, 28th EACSL Annual Conference on Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020."},"title":"Monitoring event frequencies","external_id":{"arxiv":["1910.06097"]},"article_processing_charge":"No","author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Ferrere","orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Bernhard","id":"320FC952-F248-11E8-B48F-1D18A9856A87","last_name":"Kragl","full_name":"Kragl, Bernhard","orcid":"0000-0001-7745-9117"}],"article_number":"20","project":[{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"publication":"28th EACSL Annual Conference on Computer Science Logic","day":"15","year":"2020","has_accepted_license":"1","date_created":"2020-01-21T11:22:21Z","doi":"10.4230/LIPIcs.CSL.2020.20","date_published":"2020-01-15T00:00:00Z","oa":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","ddc":["000"],"date_updated":"2021-01-12T08:13:12Z","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:47:56Z","_id":"7348","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"location":"Barcelona, Spain","end_date":"2020-01-16","start_date":"2020-01-13","name":"CSL: Computer Science Logic"},"type":"conference","language":[{"iso":"eng"}],"file":[{"file_id":"7349","checksum":"b9a691d658d075c6369d3304d17fb818","content_type":"application/pdf","access_level":"open_access","relation":"main_file","date_created":"2020-01-21T11:21:04Z","file_name":"main.pdf","date_updated":"2020-07-14T12:47:56Z","file_size":617206,"creator":"bkragl"}],"publication_status":"published","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959771320"]},"volume":152,"oa_version":"Published Version","abstract":[{"text":"The monitoring of event frequencies can be used to recognize behavioral anomalies, to identify trends, and to deduce or discard hypotheses about the underlying system. For example, the performance of a web server may be monitored based on the ratio of the total count of requests from the least and most active clients. Exact frequency monitoring, however, can be prohibitively expensive; in the above example it would require as many counters as there are clients. In this paper, we propose the efficient probabilistic monitoring of common frequency properties, including the mode (i.e., the most common event) and the median of an event sequence. We define a logic to express composite frequency properties as a combination of atomic frequency properties. Our main contribution is an algorithm that, under suitable probabilistic assumptions, can be used to monitor these important frequency properties with four counters, independent of the number of different events. Our algorithm samples longer and longer subwords of an infinite event sequence. We prove the almost-sure convergence of our algorithm by generalizing ergodic theory from increasing-length prefixes to increasing-length subwords of an infinite sequence. A similar algorithm could be used to learn a connected Markov chain of a given structure from observing its outputs, to arbitrary precision, for a given confidence. ","lang":"eng"}],"intvolume":" 152","month":"01","alternative_title":["LIPIcs"],"scopus_import":1},{"date_updated":"2021-01-12T08:20:06Z","department":[{"_id":"ToHe"}],"_id":"8572","conference":{"name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems","start_date":"2020-07-12","end_date":"2020-07-12"},"type":"conference","status":"public","publication_status":"published","language":[{"iso":"eng"}],"ec_funded":1,"volume":74,"abstract":[{"text":"We present the results of the ARCH 2020 friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. In its fourth edition, eight tools have been applied to solve eight different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA, C2E2, HyDRA, Hylaa, Hylaa-Continuous, JuliaReach, SpaceEx, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results provide one of the most complete assessments of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.","lang":"eng"}],"oa_version":"Published Version","main_file_link":[{"open_access":"1","url":"https://easychair.org/publications/download/DRpS"}],"intvolume":" 74","month":"09","citation":{"ista":"Althoff M, Bak S, Bao Z, Forets M, Frehse G, Freire D, Kochdumper N, Li Y, Mitra S, Ray R, Schilling C, Schupp S, Wetzlinger M. 2020. ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics. EPiC Series in Computing. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems vol. 74, 16–48.","chicago":"Althoff, Matthias, Stanley Bak, Zongnan Bao, Marcelo Forets, Goran Frehse, Daniel Freire, Niklas Kochdumper, et al. “ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Linear Dynamics.” In EPiC Series in Computing, 74:16–48. EasyChair, 2020. https://doi.org/10.29007/7dt2.","ama":"Althoff M, Bak S, Bao Z, et al. ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics. In: EPiC Series in Computing. Vol 74. EasyChair; 2020:16-48. doi:10.29007/7dt2","apa":"Althoff, M., Bak, S., Bao, Z., Forets, M., Frehse, G., Freire, D., … Wetzlinger, M. (2020). ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics. In EPiC Series in Computing (Vol. 74, pp. 16–48). EasyChair. https://doi.org/10.29007/7dt2","short":"M. Althoff, S. Bak, Z. Bao, M. Forets, G. Frehse, D. Freire, N. Kochdumper, Y. Li, S. Mitra, R. Ray, C. Schilling, S. Schupp, M. Wetzlinger, in:, EPiC Series in Computing, EasyChair, 2020, pp. 16–48.","ieee":"M. Althoff et al., “ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics,” in EPiC Series in Computing, 2020, vol. 74, pp. 16–48.","mla":"Althoff, Matthias, et al. “ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Linear Dynamics.” EPiC Series in Computing, vol. 74, EasyChair, 2020, pp. 16–48, doi:10.29007/7dt2."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","author":[{"first_name":"Matthias","last_name":"Althoff","full_name":"Althoff, Matthias"},{"full_name":"Bak, Stanley","last_name":"Bak","first_name":"Stanley"},{"full_name":"Bao, Zongnan","last_name":"Bao","first_name":"Zongnan"},{"last_name":"Forets","full_name":"Forets, Marcelo","first_name":"Marcelo"},{"first_name":"Goran","full_name":"Frehse, Goran","last_name":"Frehse"},{"full_name":"Freire, Daniel","last_name":"Freire","first_name":"Daniel"},{"first_name":"Niklas","full_name":"Kochdumper, Niklas","last_name":"Kochdumper"},{"last_name":"Li","full_name":"Li, Yangge","first_name":"Yangge"},{"first_name":"Sayan","full_name":"Mitra, Sayan","last_name":"Mitra"},{"last_name":"Ray","full_name":"Ray, Rajarshi","first_name":"Rajarshi"},{"last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Stefan","last_name":"Schupp","full_name":"Schupp, Stefan"},{"full_name":"Wetzlinger, Mark","last_name":"Wetzlinger","first_name":"Mark"}],"title":"ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics","project":[{"_id":"25C5A090-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z00312"},{"_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"}],"year":"2020","publication":"EPiC Series in Computing","day":"25","page":"16-48","date_created":"2020-09-26T14:49:43Z","doi":"10.29007/7dt2","date_published":"2020-09-25T00:00:00Z","acknowledgement":"The authors gratefully acknowledge financial support by the European Commission project\r\njustITSELF under grant number 817629, by the Austrian Science Fund (FWF) under grant\r\nZ211-N23 (Wittgenstein Award), by the European Union’s Horizon 2020 research and innovation programme under the Marie Sk lodowska-Curie grant agreement No. 754411, and by the\r\nScience and Engineering Research Board (SERB) project with file number IMP/2018/000523.\r\nThis material is based upon work supported by the Air Force Office of Scientific Research under\r\naward number FA9550-19-1-0288. Any opinions, finding, and conclusions or recommendations\r\nexpressed in this material are those of the author(s) and do not necessarily reflect the views of\r\nthe United States Air Force.","oa":1,"quality_controlled":"1","publisher":"EasyChair"},{"ec_funded":1,"volume":74,"publication_status":"published","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://easychair.org/publications/download/nrdD"}],"intvolume":" 74","month":"09","abstract":[{"text":"We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. These tools are applied to solve reachability analysis problems on six benchmark problems, two of them featuring hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.","lang":"eng"}],"oa_version":"Published Version","department":[{"_id":"ToHe"}],"date_updated":"2021-01-12T08:20:06Z","conference":{"end_date":"2020-07-12","start_date":"2020-07-12","name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems"},"type":"conference","status":"public","_id":"8571","page":"49-75","date_created":"2020-09-26T14:41:29Z","date_published":"2020-09-25T00:00:00Z","doi":"10.29007/zkf6","year":"2020","publication":"EPiC Series in Computing","day":"25","oa":1,"publisher":"EasyChair","quality_controlled":"1","acknowledgement":"Christian Schilling acknowledges support in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award) and the European Union’s Horizon 2020 research and innovation programme under the Marie Sk lodowska-Curie grant agreement No. 754411.","article_processing_charge":"No","author":[{"last_name":"Geretti","full_name":"Geretti, Luca","first_name":"Luca"},{"first_name":"Julien","last_name":"Alexandre Dit Sandretto","full_name":"Alexandre Dit Sandretto, Julien"},{"last_name":"Althoff","full_name":"Althoff, Matthias","first_name":"Matthias"},{"full_name":"Benet, Luis","last_name":"Benet","first_name":"Luis"},{"first_name":"Alexandre","last_name":"Chapoutot","full_name":"Chapoutot, Alexandre"},{"last_name":"Chen","full_name":"Chen, Xin","first_name":"Xin"},{"first_name":"Pieter","last_name":"Collins","full_name":"Collins, Pieter"},{"full_name":"Forets, Marcelo","last_name":"Forets","first_name":"Marcelo"},{"first_name":"Daniel","full_name":"Freire, Daniel","last_name":"Freire"},{"first_name":"Fabian","full_name":"Immler, Fabian","last_name":"Immler"},{"last_name":"Kochdumper","full_name":"Kochdumper, Niklas","first_name":"Niklas"},{"first_name":"David","last_name":"Sanders","full_name":"Sanders, David"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"}],"title":"ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics","citation":{"ista":"Geretti L, Alexandre Dit Sandretto J, Althoff M, Benet L, Chapoutot A, Chen X, Collins P, Forets M, Freire D, Immler F, Kochdumper N, Sanders D, Schilling C. 2020. ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics. EPiC Series in Computing. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems vol. 74, 49–75.","chicago":"Geretti, Luca, Julien Alexandre Dit Sandretto, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin Chen, Pieter Collins, et al. “ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” In EPiC Series in Computing, 74:49–75. EasyChair, 2020. https://doi.org/10.29007/zkf6.","apa":"Geretti, L., Alexandre Dit Sandretto, J., Althoff, M., Benet, L., Chapoutot, A., Chen, X., … Schilling, C. (2020). ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics. In EPiC Series in Computing (Vol. 74, pp. 49–75). EasyChair. https://doi.org/10.29007/zkf6","ama":"Geretti L, Alexandre Dit Sandretto J, Althoff M, et al. ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics. In: EPiC Series in Computing. Vol 74. EasyChair; 2020:49-75. doi:10.29007/zkf6","ieee":"L. Geretti et al., “ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics,” in EPiC Series in Computing, 2020, vol. 74, pp. 49–75.","short":"L. Geretti, J. Alexandre Dit Sandretto, M. Althoff, L. Benet, A. Chapoutot, X. Chen, P. Collins, M. Forets, D. Freire, F. Immler, N. Kochdumper, D. Sanders, C. Schilling, in:, EPiC Series in Computing, EasyChair, 2020, pp. 49–75.","mla":"Geretti, Luca, et al. “ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” EPiC Series in Computing, vol. 74, EasyChair, 2020, pp. 49–75, doi:10.29007/zkf6."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}]},{"abstract":[{"text":"A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating.","lang":"eng"}],"oa_version":"Published Version","scopus_import":"1","alternative_title":["LIPIcs"],"intvolume":" 171","month":"08","publication_status":"published","publication_identifier":{"issn":["18688969"],"isbn":["9783959771603"]},"language":[{"iso":"eng"}],"file":[{"file_id":"8610","checksum":"5039752f644c4b72b9361d21a5e31baf","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2020-10-05T14:04:25Z","file_name":"2020_LIPIcsCONCUR_Chatterjee.pdf","creator":"dernst","date_updated":"2020-10-05T14:04:25Z","file_size":601231}],"license":"https://creativecommons.org/licenses/by/3.0/","volume":171,"_id":"8600","conference":{"end_date":"2020-09-04","location":"Virtual","start_date":"2020-09-01","name":"CONCUR: Conference on Concurrency Theory"},"tmp":{"short":"CC BY (3.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)"},"type":"conference","status":"public","date_updated":"2021-01-12T08:20:15Z","ddc":["000"],"file_date_updated":"2020-10-05T14:04:25Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"oa":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","year":"2020","has_accepted_license":"1","publication":"31st International Conference on Concurrency Theory","day":"06","date_created":"2020-10-04T22:01:36Z","doi":"10.4230/LIPIcs.CONCUR.2020.23","date_published":"2020-08-06T00:00:00Z","article_number":"23","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"citation":{"mla":"Chatterjee, Krishnendu, et al. “Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.” 31st International Conference on Concurrency Theory, vol. 171, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.CONCUR.2020.23.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Multi-dimensional long-run average problems for vector addition systems with states,” in 31st International Conference on Concurrency Theory, Virtual, 2020, vol. 171.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, 31st International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","ama":"Chatterjee K, Henzinger TA, Otop J. Multi-dimensional long-run average problems for vector addition systems with states. In: 31st International Conference on Concurrency Theory. Vol 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.CONCUR.2020.23","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2020). Multi-dimensional long-run average problems for vector addition systems with states. In 31st International Conference on Concurrency Theory (Vol. 171). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2020.23","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.” In 31st International Conference on Concurrency Theory, Vol. 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CONCUR.2020.23.","ista":"Chatterjee K, Henzinger TA, Otop J. 2020. Multi-dimensional long-run average problems for vector addition systems with states. 31st International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 171, 23."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"arxiv":["2007.08917"]},"article_processing_charge":"No","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"title":"Multi-dimensional long-run average problems for vector addition systems with states"},{"date_updated":"2021-01-12T08:20:13Z","ddc":["000"],"department":[{"_id":"ToHe"}],"file_date_updated":"2020-10-05T14:13:19Z","_id":"8599","type":"conference","conference":{"name":"CONCUR: Conference on Concurrency Theory","start_date":"2020-09-01","location":"Virtual","end_date":"2020-09-04"},"tmp":{"short":"CC BY (3.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)"},"status":"public","publication_identifier":{"isbn":["9783959771603"],"issn":["18688969"]},"publication_status":"published","file":[{"creator":"dernst","date_updated":"2020-10-05T14:13:19Z","file_size":868510,"date_created":"2020-10-05T14:13:19Z","file_name":"2020_LIPIcsCONCUR_Avni.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"8611","checksum":"8f33b098e73724e0ac817f764d8e1a2d","success":1}],"language":[{"iso":"eng"}],"volume":171,"abstract":[{"text":"A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an \"auction\" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and study their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We show how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.","lang":"eng"}],"oa_version":"Published Version","scopus_import":"1","alternative_title":["LIPIcs"],"month":"08","intvolume":" 171","citation":{"chicago":"Avni, Guy, and Thomas A Henzinger. “A Survey of Bidding Games on Graphs.” In 31st International Conference on Concurrency Theory, Vol. 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CONCUR.2020.2.","ista":"Avni G, Henzinger TA. 2020. A survey of bidding games on graphs. 31st International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 171, 2.","mla":"Avni, Guy, and Thomas A. Henzinger. “A Survey of Bidding Games on Graphs.” 31st International Conference on Concurrency Theory, vol. 171, 2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.CONCUR.2020.2.","short":"G. Avni, T.A. Henzinger, in:, 31st International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","ieee":"G. Avni and T. A. Henzinger, “A survey of bidding games on graphs,” in 31st International Conference on Concurrency Theory, Virtual, 2020, vol. 171.","apa":"Avni, G., & Henzinger, T. A. (2020). A survey of bidding games on graphs. In 31st International Conference on Concurrency Theory (Vol. 171). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2020.2","ama":"Avni G, Henzinger TA. A survey of bidding games on graphs. In: 31st International Conference on Concurrency Theory. Vol 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.CONCUR.2020.2"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Avni","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"article_processing_charge":"No","title":"A survey of bidding games on graphs","article_number":"2","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"has_accepted_license":"1","year":"2020","day":"06","publication":"31st International Conference on Concurrency Theory","doi":"10.4230/LIPIcs.CONCUR.2020.2","date_published":"2020-08-06T00:00:00Z","date_created":"2020-10-04T22:01:36Z","acknowledgement":"We would like to thank all our collaborators Milad Aghajohari, Ventsislav Chonev, Rasmus Ibsen-Jensen, Ismäel Jecker, Petr Novotný, Josef Tkadlec, and Ðorđe Žikelić; we hope the collaboration was as fun and meaningful for you as it was for us.","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","oa":1},{"file_date_updated":"2021-02-09T09:39:02Z","department":[{"_id":"ToHe"}],"date_updated":"2021-02-09T09:39:59Z","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"end_date":"2020-09-24","location":"Online Conference","start_date":"2020-09-21","name":" FMCAD: Formal Methods in Computer-Aided Design"},"type":"conference","status":"public","_id":"9040","publication_status":"published","publication_identifier":{"eissn":["2708-7824"],"isbn":["9783854480426"]},"language":[{"iso":"eng"}],"file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","success":1,"checksum":"d616d549a0ade78606b16f8a9540820f","file_id":"9109","creator":"dernst","file_size":990999,"date_updated":"2021-02-09T09:39:02Z","file_name":"2020_FMCAD_Alamdari.pdf","date_created":"2021-02-09T09:39:02Z"}],"scopus_import":"1","month":"09","abstract":[{"lang":"eng","text":"Machine learning and formal methods have complimentary benefits and drawbacks. In this work, we address the controller-design problem with a combination of techniques from both fields. The use of black-box neural networks in deep reinforcement learning (deep RL) poses a challenge for such a combination. Instead of reasoning formally about the output of deep RL, which we call the wizard, we extract from it a decision-tree based model, which we refer to as the magic book. Using the extracted model as an intermediary, we are able to handle problems that are infeasible for either deep RL or formal methods by themselves. First, we suggest, for the first time, a synthesis procedure that is based on a magic book. We synthesize a stand-alone correct-by-design controller that enjoys the favorable performance of RL. Second, we incorporate a magic book in a bounded model checking (BMC) procedure. BMC allows us to find numerous traces of the plant under the control of the wizard, which a user can use to increase the trustworthiness of the wizard and direct further training."}],"oa_version":"Published Version","article_processing_charge":"No","author":[{"full_name":"Alamdari, Par Alizadeh","last_name":"Alamdari","first_name":"Par Alizadeh"},{"last_name":"Avni","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Anna","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425","last_name":"Lukina","full_name":"Lukina, Anna"}],"title":"Formal methods with a touch of magic","citation":{"ista":"Alamdari PA, Avni G, Henzinger TA, Lukina A. 2020. Formal methods with a touch of magic. Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 138–147.","chicago":"Alamdari, Par Alizadeh, Guy Avni, Thomas A Henzinger, and Anna Lukina. “Formal Methods with a Touch of Magic.” In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, 138–47. TU Wien Academic Press, 2020. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21.","apa":"Alamdari, P. A., Avni, G., Henzinger, T. A., & Lukina, A. (2020). Formal methods with a touch of magic. In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design (pp. 138–147). Online Conference: TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21","ama":"Alamdari PA, Avni G, Henzinger TA, Lukina A. Formal methods with a touch of magic. In: Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design. TU Wien Academic Press; 2020:138-147. doi:10.34727/2020/isbn.978-3-85448-042-6_21","ieee":"P. A. Alamdari, G. Avni, T. A. Henzinger, and A. Lukina, “Formal methods with a touch of magic,” in Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, Online Conference, 2020, pp. 138–147.","short":"P.A. Alamdari, G. Avni, T.A. Henzinger, A. Lukina, in:, Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press, 2020, pp. 138–147.","mla":"Alamdari, Par Alizadeh, et al. “Formal Methods with a Touch of Magic.” Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press, 2020, pp. 138–47, doi:10.34727/2020/isbn.978-3-85448-042-6_21."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"page":"138-147","date_created":"2021-01-24T23:01:10Z","date_published":"2020-09-21T00:00:00Z","doi":"10.34727/2020/isbn.978-3-85448-042-6_21","year":"2020","has_accepted_license":"1","publication":"Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design","day":"21","oa":1,"publisher":"TU Wien Academic Press","quality_controlled":"1","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award)."},{"citation":{"mla":"Singh, Sidak Pal, and Dan-Adrian Alistarh. “WoodFisher: Efficient Second-Order Approximation for Neural Network Compression.” Advances in Neural Information Processing Systems, vol. 33, Curran Associates, 2020, pp. 18098–109.","short":"S.P. Singh, D.-A. Alistarh, in:, Advances in Neural Information Processing Systems, Curran Associates, 2020, pp. 18098–18109.","ieee":"S. P. Singh and D.-A. Alistarh, “WoodFisher: Efficient second-order approximation for neural network compression,” in Advances in Neural Information Processing Systems, Vancouver, Canada, 2020, vol. 33, pp. 18098–18109.","apa":"Singh, S. P., & Alistarh, D.-A. (2020). WoodFisher: Efficient second-order approximation for neural network compression. In Advances in Neural Information Processing Systems (Vol. 33, pp. 18098–18109). Vancouver, Canada: Curran Associates.","ama":"Singh SP, Alistarh D-A. WoodFisher: Efficient second-order approximation for neural network compression. In: Advances in Neural Information Processing Systems. Vol 33. Curran Associates; 2020:18098-18109.","chicago":"Singh, Sidak Pal, and Dan-Adrian Alistarh. “WoodFisher: Efficient Second-Order Approximation for Neural Network Compression.” In Advances in Neural Information Processing Systems, 33:18098–109. Curran Associates, 2020.","ista":"Singh SP, Alistarh D-A. 2020. WoodFisher: Efficient second-order approximation for neural network compression. Advances in Neural Information Processing Systems. NeurIPS: Conference on Neural Information Processing Systems vol. 33, 18098–18109."},"user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","article_processing_charge":"No","external_id":{"arxiv":["2004.14340"]},"author":[{"last_name":"Singh","full_name":"Singh, Sidak Pal","id":"DD138E24-D89D-11E9-9DC0-DEF6E5697425","first_name":"Sidak Pal"},{"first_name":"Dan-Adrian","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3650-940X","full_name":"Alistarh, Dan-Adrian","last_name":"Alistarh"}],"title":"WoodFisher: Efficient second-order approximation for neural network compression","project":[{"call_identifier":"H2020","_id":"268A44D6-B435-11E9-9278-68D0E5697425","grant_number":"805223","name":"Elastic Coordination for Scalable Machine Learning"}],"year":"2020","publication":"Advances in Neural Information Processing Systems","day":"06","page":"18098-18109","date_created":"2021-07-04T22:01:26Z","date_published":"2020-12-06T00:00:00Z","acknowledgement":"This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 805223 ScaleML). Also, we would like to thank Alexander Shevchenko, Alexandra Peste, and other members of the group for fruitful discussions.","oa":1,"quality_controlled":"1","publisher":"Curran Associates","date_updated":"2023-02-23T14:03:06Z","department":[{"_id":"DaAl"},{"_id":"ToHe"}],"_id":"9632","conference":{"end_date":"2020-12-12","location":"Vancouver, Canada","start_date":"2020-12-06","name":"NeurIPS: Conference on Neural Information Processing Systems"},"type":"conference","status":"public","publication_status":"published","publication_identifier":{"issn":["10495258"],"isbn":["9781713829546"]},"language":[{"iso":"eng"}],"ec_funded":1,"volume":33,"abstract":[{"text":"Second-order information, in the form of Hessian- or Inverse-Hessian-vector products, is a fundamental tool for solving optimization problems. Recently, there has been significant interest in utilizing this information in the context of deep\r\nneural networks; however, relatively little is known about the quality of existing approximations in this context. Our work examines this question, identifies issues with existing approaches, and proposes a method called WoodFisher to compute a faithful and efficient estimate of the inverse Hessian. Our main application is to neural network compression, where we build on the classic Optimal Brain Damage/Surgeon framework. We demonstrate that WoodFisher significantly outperforms popular state-of-the-art methods for oneshot pruning. Further, even when iterative, gradual pruning is allowed, our method results in a gain in test accuracy over the state-of-the-art approaches, for standard image classification datasets such as ImageNet ILSVRC. We examine how our method can be extended to take into account first-order information, as well as\r\nillustrate its ability to automatically set layer-wise pruning thresholds and perform compression in the limited-data regime. The code is available at the following link, https://github.com/IST-DASLab/WoodFisher.","lang":"eng"}],"oa_version":"Published Version","main_file_link":[{"url":"https://proceedings.neurips.cc/paper/2020/hash/d1ff1ec86b62cd5f3903ff19c3a326b2-Abstract.html","open_access":"1"}],"scopus_import":"1","intvolume":" 33","month":"12"},{"volume":2020,"publication_identifier":{"issn":["07431546"],"isbn":["9781728174471"]},"publication_status":"published","language":[{"iso":"eng"}],"scopus_import":"1","main_file_link":[{"url":"https://arxiv.org/abs/2012.07458","open_access":"1"}],"month":"12","intvolume":" 2020","abstract":[{"text":"We introduce LRT-NG, a set of techniques and an associated toolset that computes a reachtube (an over-approximation of the set of reachable states over a given time horizon) of a nonlinear dynamical system. LRT-NG significantly advances the state-of-the-art Langrangian Reachability and its associated tool LRT. From a theoretical perspective, LRT-NG is superior to LRT in three ways. First, it uses for the first time an analytically computed metric for the propagated ball which is proven to minimize the ball’s volume. We emphasize that the metric computation is the centerpiece of all bloating-based techniques. Secondly, it computes the next reachset as the intersection of two balls: one based on the Cartesian metric and the other on the new metric. While the two metrics were previously considered opposing approaches, their joint use considerably tightens the reachtubes. Thirdly, it avoids the \"wrapping effect\" associated with the validated integration of the center of the reachset, by optimally absorbing the interval approximation in the radius of the next ball. From a tool-development perspective, LRT-NG is superior to LRT in two ways. First, it is a standalone tool that no longer relies on CAPD. This required the implementation of the Lohner method and a Runge-Kutta time-propagation method. Secondly, it has an improved interface, allowing the input model and initial conditions to be provided as external input files. Our experiments on a comprehensive set of benchmarks, including two Neural ODEs, demonstrates LRT-NG’s superior performance compared to LRT, CAPD, and Flow*.","lang":"eng"}],"oa_version":"Preprint","department":[{"_id":"ToHe"}],"date_updated":"2021-02-09T09:20:58Z","type":"conference","conference":{"name":"CDC: Conference on Decision and Control","location":"Jeju Islang, Korea (South)","end_date":"2020-12-18","start_date":"2020-12-14"},"status":"public","_id":"9103","page":"1556-1563","date_published":"2020-12-14T00:00:00Z","doi":"10.1109/CDC42340.2020.9304042","date_created":"2021-02-07T23:01:14Z","year":"2020","day":"14","publication":"Proceedings of the 59th IEEE Conference on Decision and Control","publisher":"IEEE","quality_controlled":"1","oa":1,"acknowledgement":"The authors would like to thank Ramin Hasani and Guillaume Berger for intellectual discussions about the research which lead to the generation of new ideas. ML was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). Smolka’s research was supported by NSF grants CPS-1446832 and CCF-1918225. Gruenbacher is funded by FWF project W1255-N23. JC was partially supported by NAWA Polish Returns grant\r\nPPN/PPO/2018/1/00029.\r\n","author":[{"full_name":"Gruenbacher, Sophie","last_name":"Gruenbacher","first_name":"Sophie"},{"first_name":"Jacek","full_name":"Cyranka, Jacek","last_name":"Cyranka"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias"},{"first_name":"Md Ariful","full_name":"Islam, Md Ariful","last_name":"Islam"},{"first_name":"Scott A.","last_name":"Smolka","full_name":"Smolka, Scott A."},{"first_name":"Radu","last_name":"Grosu","full_name":"Grosu, Radu"}],"external_id":{"arxiv":["2012.07458"]},"article_processing_charge":"No","title":"Lagrangian reachtubes: The next generation","citation":{"chicago":"Gruenbacher, Sophie, Jacek Cyranka, Mathias Lechner, Md Ariful Islam, Scott A. Smolka, and Radu Grosu. “Lagrangian Reachtubes: The next Generation.” In Proceedings of the 59th IEEE Conference on Decision and Control, 2020:1556–63. IEEE, 2020. https://doi.org/10.1109/CDC42340.2020.9304042.","ista":"Gruenbacher S, Cyranka J, Lechner M, Islam MA, Smolka SA, Grosu R. 2020. Lagrangian reachtubes: The next generation. Proceedings of the 59th IEEE Conference on Decision and Control. CDC: Conference on Decision and Control vol. 2020, 1556–1563.","mla":"Gruenbacher, Sophie, et al. “Lagrangian Reachtubes: The next Generation.” Proceedings of the 59th IEEE Conference on Decision and Control, vol. 2020, IEEE, 2020, pp. 1556–63, doi:10.1109/CDC42340.2020.9304042.","apa":"Gruenbacher, S., Cyranka, J., Lechner, M., Islam, M. A., Smolka, S. A., & Grosu, R. (2020). Lagrangian reachtubes: The next generation. In Proceedings of the 59th IEEE Conference on Decision and Control (Vol. 2020, pp. 1556–1563). Jeju Islang, Korea (South): IEEE. https://doi.org/10.1109/CDC42340.2020.9304042","ama":"Gruenbacher S, Cyranka J, Lechner M, Islam MA, Smolka SA, Grosu R. Lagrangian reachtubes: The next generation. In: Proceedings of the 59th IEEE Conference on Decision and Control. Vol 2020. IEEE; 2020:1556-1563. doi:10.1109/CDC42340.2020.9304042","short":"S. Gruenbacher, J. Cyranka, M. Lechner, M.A. Islam, S.A. Smolka, R. Grosu, in:, Proceedings of the 59th IEEE Conference on Decision and Control, IEEE, 2020, pp. 1556–1563.","ieee":"S. Gruenbacher, J. Cyranka, M. Lechner, M. A. Islam, S. A. Smolka, and R. Grosu, “Lagrangian reachtubes: The next generation,” in Proceedings of the 59th IEEE Conference on Decision and Control, Jeju Islang, Korea (South), 2020, vol. 2020, pp. 1556–1563."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}]},{"language":[{"iso":"eng"}],"file":[{"file_name":"iclr_2020.pdf","date_created":"2022-01-26T07:35:17Z","creator":"mlechner","file_size":249431,"date_updated":"2022-01-26T07:35:17Z","success":1,"checksum":"ea13d42dd4541ddb239b6a75821fd6c9","file_id":"10677","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"publication_status":"published","oa_version":"Published Version","abstract":[{"lang":"eng","text":"The family of feedback alignment (FA) algorithms aims to provide a more biologically motivated alternative to backpropagation (BP), by substituting the computations that are unrealistic to be implemented in physical brains. While FA algorithms have been shown to work well in practice, there is a lack of rigorous theory proofing their learning capabilities. Here we introduce the first feedback alignment algorithm with provable learning guarantees. In contrast to existing work, we do not require any assumption about the size or depth of the network except that it has a single output neuron, i.e., such as for binary classification tasks. We show that our FA algorithm can deliver its theoretical promises in practice, surpassing the learning performance of existing FA methods and matching backpropagation in binary classification tasks. Finally, we demonstrate the limits of our FA variant when the number of output neurons grows beyond a certain quantity."}],"month":"03","main_file_link":[{"url":"https://openreview.net/forum?id=Bke61krFvS","open_access":"1"}],"scopus_import":"1","ddc":["000"],"date_updated":"2023-04-03T07:33:40Z","file_date_updated":"2022-01-26T07:35:17Z","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"_id":"10672","status":"public","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode","short":"CC BY-NC-ND (3.0)"},"conference":{"location":"Virtual ; Addis Ababa, Ethiopia","end_date":"2020-05-01","start_date":"2020-04-26","name":"ICLR: International Conference on Learning Representations"},"type":"conference","publication":"8th International Conference on Learning Representations","day":"11","year":"2020","has_accepted_license":"1","date_created":"2022-01-25T15:50:00Z","date_published":"2020-03-11T00:00:00Z","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23\r\n(Wittgenstein Award).\r\n","oa":1,"quality_controlled":"1","publisher":"ICLR","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Lechner M. 2020. Learning representations for binary-classification without backpropagation. 8th International Conference on Learning Representations. ICLR: International Conference on Learning Representations.","chicago":"Lechner, Mathias. “Learning Representations for Binary-Classification without Backpropagation.” In 8th International Conference on Learning Representations. ICLR, 2020.","ieee":"M. Lechner, “Learning representations for binary-classification without backpropagation,” in 8th International Conference on Learning Representations, Virtual ; Addis Ababa, Ethiopia, 2020.","short":"M. Lechner, in:, 8th International Conference on Learning Representations, ICLR, 2020.","apa":"Lechner, M. (2020). Learning representations for binary-classification without backpropagation. In 8th International Conference on Learning Representations. Virtual ; Addis Ababa, Ethiopia: ICLR.","ama":"Lechner M. Learning representations for binary-classification without backpropagation. In: 8th International Conference on Learning Representations. ICLR; 2020.","mla":"Lechner, Mathias. “Learning Representations for Binary-Classification without Backpropagation.” 8th International Conference on Learning Representations, ICLR, 2020."},"title":"Learning representations for binary-classification without backpropagation","article_processing_charge":"No","author":[{"first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","full_name":"Lechner, Mathias"}],"project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}]},{"article_processing_charge":"No","author":[{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco","last_name":"Giacobbe","full_name":"Giacobbe, Mirco","orcid":"0000-0001-8180-0904"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","full_name":"Lechner, Mathias"}],"title":"How many bits does it take to quantize your neural network?","citation":{"mla":"Giacobbe, Mirco, et al. “How Many Bits Does It Take to Quantize Your Neural Network?” International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 12079, Springer Nature, 2020, pp. 79–97, doi:10.1007/978-3-030-45237-7_5.","ama":"Giacobbe M, Henzinger TA, Lechner M. How many bits does it take to quantize your neural network? In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Vol 12079. Springer Nature; 2020:79-97. doi:10.1007/978-3-030-45237-7_5","apa":"Giacobbe, M., Henzinger, T. A., & Lechner, M. (2020). How many bits does it take to quantize your neural network? In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 12079, pp. 79–97). Dublin, Ireland: Springer Nature. https://doi.org/10.1007/978-3-030-45237-7_5","short":"M. Giacobbe, T.A. Henzinger, M. Lechner, in:, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2020, pp. 79–97.","ieee":"M. Giacobbe, T. A. Henzinger, and M. Lechner, “How many bits does it take to quantize your neural network?,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Dublin, Ireland, 2020, vol. 12079, pp. 79–97.","chicago":"Giacobbe, Mirco, Thomas A Henzinger, and Mathias Lechner. “How Many Bits Does It Take to Quantize Your Neural Network?” In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 12079:79–97. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-45237-7_5.","ista":"Giacobbe M, Henzinger TA, Lechner M. 2020. How many bits does it take to quantize your neural network? International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 12079, 79–97."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"page":"79-97","date_created":"2020-05-10T22:00:49Z","date_published":"2020-04-17T00:00:00Z","doi":"10.1007/978-3-030-45237-7_5","year":"2020","has_accepted_license":"1","publication":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","day":"17","oa":1,"publisher":"Springer Nature","quality_controlled":"1","file_date_updated":"2020-07-14T12:48:03Z","department":[{"_id":"ToHe"}],"date_updated":"2023-06-23T07:01:11Z","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"location":"Dublin, Ireland","end_date":"2020-04-30","start_date":"2020-04-25","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"type":"conference","status":"public","_id":"7808","volume":12079,"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"11362"}]},"publication_status":"published","publication_identifier":{"eissn":["16113349"],"isbn":["9783030452360"],"issn":["03029743"]},"language":[{"iso":"eng"}],"file":[{"date_created":"2020-05-26T12:48:15Z","file_name":"2020_TACAS_Giacobbe.pdf","date_updated":"2020-07-14T12:48:03Z","file_size":2744030,"creator":"dernst","checksum":"f19905a42891fe5ce93d69143fa3f6fb","file_id":"7893","content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"scopus_import":1,"alternative_title":["LNCS"],"intvolume":" 12079","month":"04","abstract":[{"text":"Quantization converts neural networks into low-bit fixed-point computations which can be carried out by efficient integer-only hardware, and is standard practice for the deployment of neural networks on real-time embedded devices. However, like their real-numbered counterpart, quantized networks are not immune to malicious misclassification caused by adversarial attacks. We investigate how quantization affects a network’s robustness to adversarial attacks, which is a formal verification question. We show that neither robustness nor non-robustness are monotonic with changing the number of bits for the representation and, also, neither are preserved by quantization from a real-numbered network. For this reason, we introduce a verification method for quantized neural networks which, using SMT solving over bit-vectors, accounts for their exact, bit-precise semantics. We built a tool and analyzed the effect of quantization on a classifier for the MNIST dataset. We demonstrate that, compared to our method, existing methods for the analysis of real-numbered networks often derive false conclusions about their quantizations, both when determining robustness and when detecting attacks, and that existing methods for quantized networks often miss attacks. Furthermore, we applied our method beyond robustness, showing how the number of bits in quantization enlarges the gender bias of a predictor for students’ grades.","lang":"eng"}],"oa_version":"Published Version"},{"project":[{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"},{"name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425"}],"citation":{"ista":"Avni G, Henzinger TA, Kupferman O. 2020. Dynamic resource allocation games. Theoretical Computer Science. 807, 42–55.","chicago":"Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation Games.” Theoretical Computer Science. Elsevier, 2020. https://doi.org/10.1016/j.tcs.2019.06.031.","ieee":"G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,” Theoretical Computer Science, vol. 807. Elsevier, pp. 42–55, 2020.","short":"G. Avni, T.A. Henzinger, O. Kupferman, Theoretical Computer Science 807 (2020) 42–55.","apa":"Avni, G., Henzinger, T. A., & Kupferman, O. (2020). Dynamic resource allocation games. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2019.06.031","ama":"Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. Theoretical Computer Science. 2020;807:42-55. doi:10.1016/j.tcs.2019.06.031","mla":"Avni, Guy, et al. “Dynamic Resource Allocation Games.” Theoretical Computer Science, vol. 807, Elsevier, 2020, pp. 42–55, doi:10.1016/j.tcs.2019.06.031."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","external_id":{"isi":["000512219400004"]},"article_processing_charge":"No","author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","last_name":"Avni","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"title":"Dynamic resource allocation games","oa":1,"publisher":"Elsevier","quality_controlled":"1","year":"2020","isi":1,"has_accepted_license":"1","publication":"Theoretical Computer Science","day":"06","page":"42-55","date_created":"2019-08-04T21:59:20Z","doi":"10.1016/j.tcs.2019.06.031","date_published":"2020-02-06T00:00:00Z","_id":"6761","type":"journal_article","article_type":"original","status":"public","date_updated":"2023-08-17T13:52:49Z","ddc":["000"],"department":[{"_id":"ToHe"}],"file_date_updated":"2020-10-09T06:31:22Z","abstract":[{"lang":"eng","text":"In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability."}],"oa_version":"Submitted Version","scopus_import":"1","intvolume":" 807","month":"02","publication_status":"published","publication_identifier":{"issn":["03043975"]},"language":[{"iso":"eng"}],"file":[{"date_created":"2020-10-09T06:31:22Z","file_name":"2020_TheoreticalCS_Avni.pdf","date_updated":"2020-10-09T06:31:22Z","file_size":1413001,"creator":"dernst","file_id":"8639","checksum":"e86635417f45eb2cd75778f91382f737","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"volume":807,"related_material":{"record":[{"id":"1341","status":"public","relation":"earlier_version"}]}},{"_id":"7505","status":"public","conference":{"name":"ECAI: European Conference on Artificial Intelligence","start_date":"2020-08-29","location":"Santiago de Compostela, Spain","end_date":"2020-09-08"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","image":"/images/cc_by_nc.png","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","short":"CC BY-NC (4.0)"},"type":"conference","ddc":["000"],"date_updated":"2023-08-18T06:38:16Z","department":[{"_id":"ToHe"}],"file_date_updated":"2020-09-21T07:12:32Z","oa_version":"Published Version","abstract":[{"lang":"eng","text":"Neural networks have demonstrated unmatched performance in a range of classification tasks. Despite numerous efforts of the research community, novelty detection remains one of the significant limitations of neural networks. The ability to identify previously unseen inputs as novel is crucial for our understanding of the decisions made by neural networks. At runtime, inputs not falling into any of the categories learned during training cannot be classified correctly by the neural network. Existing approaches treat the neural network as a black box and try to detect novel inputs based on the confidence of the output predictions. However, neural networks are not trained to reduce their confidence for novel inputs, which limits the effectiveness of these approaches. We propose a framework to monitor a neural network by observing the hidden layers. We employ a common abstraction from program analysis - boxes - to identify novel behaviors in the monitored layers, i.e., inputs that cause behaviors outside the box. For each neuron, the boxes range over the values seen in training. The framework is efficient and flexible to achieve a desired trade-off between raising false warnings and detecting novel inputs. We illustrate the performance and the robustness to variability in the unknown classes on popular image-classification benchmarks."}],"intvolume":" 325","month":"02","alternative_title":["Frontiers in Artificial Intelligence and Applications"],"language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"80642fa0b6cd7da95dcd87d63789ad5e","file_id":"8540","success":1,"date_updated":"2020-09-21T07:12:32Z","file_size":1692214,"creator":"dernst","date_created":"2020-09-21T07:12:32Z","file_name":"2020_ECAI_Henzinger.pdf"}],"publication_status":"published","ec_funded":1,"license":"https://creativecommons.org/licenses/by-nc/4.0/","volume":325,"project":[{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"mla":"Henzinger, Thomas A., et al. “Outside the Box: Abstraction-Based Monitoring of Neural Networks.” 24th European Conference on Artificial Intelligence, vol. 325, IOS Press, 2020, pp. 2433–40, doi:10.3233/FAIA200375.","short":"T.A. Henzinger, A. Lukina, C. Schilling, in:, 24th European Conference on Artificial Intelligence, IOS Press, 2020, pp. 2433–2440.","ieee":"T. A. Henzinger, A. Lukina, and C. Schilling, “Outside the box: Abstraction-based monitoring of neural networks,” in 24th European Conference on Artificial Intelligence, Santiago de Compostela, Spain, 2020, vol. 325, pp. 2433–2440.","apa":"Henzinger, T. A., Lukina, A., & Schilling, C. (2020). Outside the box: Abstraction-based monitoring of neural networks. In 24th European Conference on Artificial Intelligence (Vol. 325, pp. 2433–2440). Santiago de Compostela, Spain: IOS Press. https://doi.org/10.3233/FAIA200375","ama":"Henzinger TA, Lukina A, Schilling C. Outside the box: Abstraction-based monitoring of neural networks. In: 24th European Conference on Artificial Intelligence. Vol 325. IOS Press; 2020:2433-2440. doi:10.3233/FAIA200375","chicago":"Henzinger, Thomas A, Anna Lukina, and Christian Schilling. “Outside the Box: Abstraction-Based Monitoring of Neural Networks.” In 24th European Conference on Artificial Intelligence, 325:2433–40. IOS Press, 2020. https://doi.org/10.3233/FAIA200375.","ista":"Henzinger TA, Lukina A, Schilling C. 2020. Outside the box: Abstraction-based monitoring of neural networks. 24th European Conference on Artificial Intelligence. ECAI: European Conference on Artificial Intelligence, Frontiers in Artificial Intelligence and Applications, vol. 325, 2433–2440."},"title":"Outside the box: Abstraction-based monitoring of neural networks","external_id":{"isi":["000650971303002"],"arxiv":["1911.09032"]},"article_processing_charge":"No","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"},{"id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425","first_name":"Anna","last_name":"Lukina","full_name":"Lukina, Anna"},{"full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian"}],"acknowledgement":"We thank Christoph Lampert and Nikolaus Mayer for fruitful discussions. This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award) and the European Union’s Horizon 2020 research and innovation programme under the Marie SkłodowskaCurie grant agreement No. 754411.","oa":1,"publisher":"IOS Press","quality_controlled":"1","publication":"24th European Conference on Artificial Intelligence","day":"24","year":"2020","has_accepted_license":"1","isi":1,"date_created":"2020-02-21T16:44:03Z","date_published":"2020-02-24T00:00:00Z","doi":"10.3233/FAIA200375","page":"2433-2440"}]