[{"file":[{"success":1,"file_name":"16496-Article Text-19990-1-2-20210518 (1).pdf","date_created":"2022-01-26T07:41:16Z","file_size":137235,"checksum":"2bc8155b2526a70fba5b7301bc89dbd1","access_level":"open_access","content_type":"application/pdf","date_updated":"2022-01-26T07:41:16Z","creator":"mlechner","file_id":"10684","relation":"main_file"}],"oa":1,"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"page":"3787-3795","publisher":"AAAI Press","status":"public","alternative_title":["Technical Tracks"],"publication":"Proceedings of the AAAI Conference on Artificial Intelligence","external_id":{"arxiv":["2012.08185"]},"quality_controlled":"1","ddc":["000"],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein\r\nAward), ERC CoG 863818 (FoRM-SMArt), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.\r\n","article_processing_charge":"No","_id":"10665","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://ojs.aaai.org/index.php/AAAI/article/view/16496"}],"day":"28","date_created":"2022-01-25T15:15:02Z","issue":"5A","intvolume":"        35","publication_status":"published","ec_funded":1,"date_published":"2021-05-28T00:00:00Z","volume":35,"corr_author":"1","project":[{"call_identifier":"H2020","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"file_date_updated":"2022-01-26T07:41:16Z","has_accepted_license":"1","language":[{"iso":"eng"}],"scopus_import":"1","month":"05","oa_version":"Published Version","conference":{"end_date":"2021-02-09","start_date":"2021-02-02","location":"Virtual","name":"AAAI: Association for the Advancement of Artificial Intelligence"},"author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","last_name":"Lechner"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic"}],"citation":{"mla":"Henzinger, Thomas A., et al. “Scalable Verification of Quantized Neural Networks.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 35, no. 5A, AAAI Press, 2021, pp. 3787–95.","ieee":"T. A. Henzinger, M. Lechner, and D. Zikelic, “Scalable verification of quantized neural networks,” in <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, Virtual, 2021, vol. 35, no. 5A, pp. 3787–3795.","ista":"Henzinger TA, Lechner M, Zikelic D. 2021. Scalable verification of quantized neural networks. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks, vol. 35, 3787–3795.","chicago":"Henzinger, Thomas A, Mathias Lechner, and Dorde Zikelic. “Scalable Verification of Quantized Neural Networks.” In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, 35:3787–95. AAAI Press, 2021.","short":"T.A. Henzinger, M. Lechner, D. Zikelic, in:, Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, 2021, pp. 3787–3795.","apa":"Henzinger, T. A., Lechner, M., &#38; Zikelic, D. (2021). Scalable verification of quantized neural networks. In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i> (Vol. 35, pp. 3787–3795). Virtual: AAAI Press.","ama":"Henzinger TA, Lechner M, Zikelic D. Scalable verification of quantized neural networks. In: <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Vol 35. AAAI Press; 2021:3787-3795."},"abstract":[{"text":"Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle. However, most methods are designed for verification of an idealized model of the actual network which works over real arithmetic and ignores rounding imprecisions. This idealization is in stark contrast to network quantization, which is a technique that trades numerical precision for computational efficiency and is, therefore, often applied in practice. Neglecting rounding errors of such low-bit quantized neural networks has been shown to lead to wrong conclusions about the network’s correctness. Thus, the desired approach for verifying quantized neural networks would be one that takes these rounding errors\r\ninto account. In this paper, we show that verifying the bitexact implementation of quantized neural networks with bitvector specifications is PSPACE-hard, even though verifying idealized real-valued networks and satisfiability of bit-vector specifications alone are each in NP. Furthermore, we explore several practical heuristics toward closing the complexity gap between idealized and bit-exact verification. In particular, we propose three techniques for making SMT-based verification of quantized neural networks more scalable. Our experiments demonstrate that our proposed methods allow a speedup of up to three orders of magnitude over existing approaches.","lang":"eng"}],"date_updated":"2026-04-07T14:21:58Z","arxiv":1,"type":"conference","publication_identifier":{"isbn":["978-1-57735-866-4"],"issn":["2159-5399"],"eissn":["2374-3468"]},"title":"Scalable verification of quantized neural networks","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"11362"}]},"year":"2021"},{"license":"https://creativecommons.org/licenses/by-nc-nd/3.0/","month":"07","date_published":"2021-07-01T00:00:00Z","volume":139,"project":[{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"file_date_updated":"2022-01-26T07:38:32Z","has_accepted_license":"1","language":[{"iso":"eng"}],"date_updated":"2025-05-19T11:28:08Z","type":"conference","arxiv":1,"publication_identifier":{"issn":["2640-3498"]},"title":"On-off center-surround receptive fields for accurate and robust image classification","year":"2021","conference":{"name":"ML: Machine Learning","start_date":"2021-07-18","location":"Virtual","end_date":"2021-07-24"},"oa_version":"Published Version","author":[{"full_name":"Babaiee, Zahra","first_name":"Zahra","last_name":"Babaiee"},{"full_name":"Hasani, Ramin","first_name":"Ramin","last_name":"Hasani"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"full_name":"Rus, Daniela","last_name":"Rus","first_name":"Daniela"},{"full_name":"Grosu, Radu","first_name":"Radu","last_name":"Grosu"}],"citation":{"short":"Z. Babaiee, R. Hasani, M. Lechner, D. Rus, R. Grosu, in:, Proceedings of the 38th International Conference on Machine Learning, ML Research Press, 2021, pp. 478–489.","ieee":"Z. Babaiee, R. Hasani, M. Lechner, D. Rus, and R. Grosu, “On-off center-surround receptive fields for accurate and robust image classification,” in <i>Proceedings of the 38th International Conference on Machine Learning</i>, Virtual, 2021, vol. 139, pp. 478–489.","mla":"Babaiee, Zahra, et al. “On-off Center-Surround Receptive Fields for Accurate and Robust Image Classification.” <i>Proceedings of the 38th International Conference on Machine Learning</i>, vol. 139, ML Research Press, 2021, pp. 478–89.","chicago":"Babaiee, Zahra, Ramin Hasani, Mathias Lechner, Daniela Rus, and Radu Grosu. “On-off Center-Surround Receptive Fields for Accurate and Robust Image Classification.” In <i>Proceedings of the 38th International Conference on Machine Learning</i>, 139:478–89. ML Research Press, 2021.","ista":"Babaiee Z, Hasani R, Lechner M, Rus D, Grosu R. 2021. On-off center-surround receptive fields for accurate and robust image classification. Proceedings of the 38th International Conference on Machine Learning. ML: Machine Learning, PMLR, vol. 139, 478–489.","ama":"Babaiee Z, Hasani R, Lechner M, Rus D, Grosu R. On-off center-surround receptive fields for accurate and robust image classification. In: <i>Proceedings of the 38th International Conference on Machine Learning</i>. Vol 139. ML Research Press; 2021:478-489.","apa":"Babaiee, Z., Hasani, R., Lechner, M., Rus, D., &#38; Grosu, R. (2021). On-off center-surround receptive fields for accurate and robust image classification. In <i>Proceedings of the 38th International Conference on Machine Learning</i> (Vol. 139, pp. 478–489). Virtual: ML Research Press."},"abstract":[{"text":"Robustness to variations in lighting conditions is a key objective for any deep vision system. To this end, our paper extends the receptive field of convolutional neural networks with two residual components, ubiquitous in the visual processing system of vertebrates: On-center and off-center pathways, with an excitatory center and inhibitory surround; OOCS for short. The On-center pathway is excited by the presence of a light stimulus in its center, but not in its surround, whereas the Off-center pathway is excited by the absence of a light stimulus in its center, but not in its surround. We design OOCS pathways via a difference of Gaussians, with their variance computed analytically from the size of the receptive fields. OOCS pathways complement each other in their response to light stimuli, ensuring this way a strong edge-detection capability, and as a result an accurate and robust inference under challenging lighting conditions. We provide extensive empirical evidence showing that networks supplied with OOCS pathways gain accuracy and illumination-robustness from the novel edge representation, compared to other baselines.","lang":"eng"}],"quality_controlled":"1","external_id":{"arxiv":["2106.07091"]},"ddc":["000"],"acknowledgement":"Z.B. is supported by the Doctoral College Resilient Embedded Systems, which is run jointly by the TU Wien’s Faculty of Informatics and the UAS Technikum Wien. R.G. is partially supported by the Horizon 2020 Era-Permed project Persorad, and ECSEL Project grant no. 783163 (iDev40). R.H and D.R were partially supported by Boeing and MIT. M.L. is supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","_id":"10668","article_processing_charge":"No","file":[{"success":1,"date_created":"2022-01-26T07:38:32Z","file_size":4246561,"checksum":"d30eae62561bb517d9f978437d7677db","file_name":"babaiee21a.pdf","content_type":"application/pdf","date_updated":"2022-01-26T07:38:32Z","access_level":"open_access","creator":"mlechner","relation":"main_file","file_id":"10681"}],"oa":1,"page":"478-489","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publisher":"ML Research Press","alternative_title":["PMLR"],"status":"public","publication":"Proceedings of the 38th International Conference on Machine Learning","intvolume":"       139","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://proceedings.mlr.press/v139/babaiee21a"}],"day":"01","date_created":"2022-01-25T15:46:33Z","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","short":"CC BY-NC-ND (3.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode","image":"/images/cc_by_nc_nd.png"}},{"intvolume":"        35","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://ojs.aaai.org/index.php/AAAI/article/view/17372"}],"day":"28","date_created":"2022-01-25T15:47:20Z","issue":"13","ddc":["000"],"external_id":{"arxiv":["2012.08863"]},"quality_controlled":"1","acknowledgement":"The authors would like to thank the reviewers for their insightful comments. RH and RG were partially supported by\r\nHorizon-2020 ECSEL Project grant No. 783163 (iDev40). RH was partially supported by Boeing. ML was supported\r\nin part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). SG was funded by FWF\r\nproject W1255-N23. JC was partially supported by NAWA Polish Returns grant PPN/PPO/2018/1/00029. SS was supported by NSF awards DCL-2040599, CCF-1918225, and CPS-1446832.\r\n","article_processing_charge":"No","_id":"10669","file":[{"file_id":"10680","relation":"main_file","creator":"mlechner","access_level":"open_access","date_updated":"2022-01-26T07:38:08Z","content_type":"application/pdf","file_name":"17372-Article Text-20866-1-2-20210518.pdf","checksum":"468d07041e282a1d46ffdae92f709630","date_created":"2022-01-26T07:38:08Z","file_size":286906,"success":1}],"oa":1,"publisher":"AAAI Press","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"page":"11525-11535","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","status":"public","alternative_title":["Technical Tracks"],"date_updated":"2025-04-15T06:25:56Z","publication_identifier":{"eissn":["2374-3468"],"isbn":["978-1-57735-866-4"],"issn":["2159-5399"]},"type":"conference","arxiv":1,"title":"On the verification of neural ODEs with stochastic guarantees","year":"2021","conference":{"name":"AAAI: Association for the Advancement of Artificial Intelligence","end_date":"2021-02-09","location":"Virtual","start_date":"2021-02-02"},"oa_version":"Published Version","author":[{"first_name":"Sophie","last_name":"Grunbacher","full_name":"Grunbacher, Sophie"},{"last_name":"Hasani","first_name":"Ramin","full_name":"Hasani, Ramin"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"full_name":"Cyranka, Jacek","last_name":"Cyranka","first_name":"Jacek"},{"full_name":"Smolka, Scott A","last_name":"Smolka","first_name":"Scott A"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"}],"abstract":[{"text":"We show that Neural ODEs, an emerging class of timecontinuous neural networks, can be verified by solving a set of global-optimization problems. For this purpose, we introduce Stochastic Lagrangian Reachability (SLR), an\r\nabstraction-based technique for constructing a tight Reachtube (an over-approximation of the set of reachable states\r\nover a given time-horizon), and provide stochastic guarantees in the form of confidence intervals for the Reachtube bounds. SLR inherently avoids the infamous wrapping effect (accumulation of over-approximation errors) by performing local optimization steps to expand safe regions instead of repeatedly forward-propagating them as is done by deterministic reachability methods. To enable fast local optimizations, we introduce a novel forward-mode adjoint sensitivity method to compute gradients without the need for backpropagation. Finally, we establish asymptotic and non-asymptotic convergence rates for SLR.","lang":"eng"}],"citation":{"chicago":"Grunbacher, Sophie, Ramin Hasani, Mathias Lechner, Jacek Cyranka, Scott A Smolka, and Radu Grosu. “On the Verification of Neural ODEs with Stochastic Guarantees.” In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, 35:11525–35. AAAI Press, 2021.","ista":"Grunbacher S, Hasani R, Lechner M, Cyranka J, Smolka SA, Grosu R. 2021. On the verification of neural ODEs with stochastic guarantees. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks, vol. 35, 11525–11535.","mla":"Grunbacher, Sophie, et al. “On the Verification of Neural ODEs with Stochastic Guarantees.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 35, no. 13, AAAI Press, 2021, pp. 11525–35.","ieee":"S. Grunbacher, R. Hasani, M. Lechner, J. Cyranka, S. A. Smolka, and R. Grosu, “On the verification of neural ODEs with stochastic guarantees,” in <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, Virtual, 2021, vol. 35, no. 13, pp. 11525–11535.","short":"S. Grunbacher, R. Hasani, M. Lechner, J. Cyranka, S.A. Smolka, R. Grosu, in:, Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, 2021, pp. 11525–11535.","apa":"Grunbacher, S., Hasani, R., Lechner, M., Cyranka, J., Smolka, S. A., &#38; Grosu, R. (2021). On the verification of neural ODEs with stochastic guarantees. In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i> (Vol. 35, pp. 11525–11535). Virtual: AAAI Press.","ama":"Grunbacher S, Hasani R, Lechner M, Cyranka J, Smolka SA, Grosu R. On the verification of neural ODEs with stochastic guarantees. In: <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Vol 35. AAAI Press; 2021:11525-11535."},"month":"05","date_published":"2021-05-28T00:00:00Z","volume":35,"file_date_updated":"2022-01-26T07:38:08Z","has_accepted_license":"1","project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"}],"corr_author":"1","language":[{"iso":"eng"}]},{"language":[{"iso":"eng"}],"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"}],"file_date_updated":"2022-01-26T07:36:03Z","has_accepted_license":"1","corr_author":"1","date_published":"2021-05-28T00:00:00Z","volume":35,"month":"05","abstract":[{"text":"We introduce a new class of time-continuous recurrent neural network models. Instead of declaring a learning system’s dynamics by implicit nonlinearities, we construct networks of linear first-order dynamical systems modulated via nonlinear interlinked gates. The resulting models represent dynamical systems with varying (i.e., liquid) time-constants coupled to their hidden state, with outputs being computed by numerical differential equation solvers. These neural networks exhibit stable and bounded behavior, yield superior expressivity within the family of neural ordinary differential equations, and give rise to improved performance on time-series prediction tasks. To demonstrate these properties, we first take a theoretical approach to find bounds over their dynamics, and compute their expressive power by the trajectory length measure in a latent trajectory space. We then conduct a series of time-series prediction experiments to manifest the approximation capability of Liquid Time-Constant Networks (LTCs) compared to classical and modern RNNs.","lang":"eng"}],"citation":{"apa":"Hasani, R., Lechner, M., Amini, A., Rus, D., &#38; Grosu, R. (2021). Liquid time-constant networks. In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i> (Vol. 35, pp. 7657–7666). Virtual: AAAI Press.","ama":"Hasani R, Lechner M, Amini A, Rus D, Grosu R. Liquid time-constant networks. In: <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Vol 35. AAAI Press; 2021:7657-7666.","ista":"Hasani R, Lechner M, Amini A, Rus D, Grosu R. 2021. Liquid time-constant networks. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks, vol. 35, 7657–7666.","chicago":"Hasani, Ramin, Mathias Lechner, Alexander Amini, Daniela Rus, and Radu Grosu. “Liquid Time-Constant Networks.” In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, 35:7657–66. AAAI Press, 2021.","mla":"Hasani, Ramin, et al. “Liquid Time-Constant Networks.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 35, no. 9, AAAI Press, 2021, pp. 7657–66.","ieee":"R. Hasani, M. Lechner, A. Amini, D. Rus, and R. Grosu, “Liquid time-constant networks,” in <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, Virtual, 2021, vol. 35, no. 9, pp. 7657–7666.","short":"R. Hasani, M. Lechner, A. Amini, D. Rus, R. Grosu, in:, Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, 2021, pp. 7657–7666."},"author":[{"first_name":"Ramin","last_name":"Hasani","full_name":"Hasani, Ramin"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"last_name":"Amini","first_name":"Alexander","full_name":"Amini, Alexander"},{"last_name":"Rus","first_name":"Daniela","full_name":"Rus, Daniela"},{"full_name":"Grosu, Radu","last_name":"Grosu","first_name":"Radu"}],"conference":{"name":"AAAI: Association for the Advancement of Artificial Intelligence","location":"Virtual","start_date":"2021-02-02","end_date":"2021-02-09"},"oa_version":"Published Version","year":"2021","title":"Liquid time-constant networks","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"],"isbn":["978-1-57735-866-4"]},"type":"conference","arxiv":1,"date_updated":"2025-04-15T06:25:56Z","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","status":"public","alternative_title":["Technical Tracks"],"publisher":"AAAI Press","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"page":"7657-7666","file":[{"creator":"mlechner","file_id":"10678","relation":"main_file","access_level":"open_access","content_type":"application/pdf","date_updated":"2022-01-26T07:36:03Z","file_name":"16936-Article Text-20430-1-2-20210518 (1).pdf","date_created":"2022-01-26T07:36:03Z","file_size":4302669,"checksum":"0f06995fba06dbcfa7ed965fc66027ff","success":1}],"oa":1,"_id":"10671","article_processing_charge":"No","acknowledgement":"R.H. and D.R. are partially supported by Boeing. R.H. and R.G. were partially supported by the Horizon-2020 ECSEL\r\nProject grant No. 783163 (iDev40). M.L. was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). A.A. is supported by the National Science Foundation (NSF) Graduate Research Fellowship Program. This research work is partially drawn from the PhD dissertation of R.H.","ddc":["000"],"quality_controlled":"1","external_id":{"arxiv":["2006.04439"]},"issue":"9","date_created":"2022-01-25T15:48:36Z","day":"28","main_file_link":[{"open_access":"1","url":"https://ojs.aaai.org/index.php/AAAI/article/view/16936"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","intvolume":"        35"},{"title":"The Civl verifier","year":"2021","date_updated":"2025-04-15T06:25:56Z","publication_identifier":{"isbn":["978-3-85448-046-4"]},"type":"conference","abstract":[{"lang":"eng","text":"Civl is a static verifier for concurrent programs designed around the conceptual framework of layered refinement,\r\nwhich views the task of verifying a program as a sequence of program simplification steps each justified by its own invariant. Civl verifies a layered concurrent program that compactly expresses all the programs in this sequence and the supporting invariants. This paper presents the design and implementation of the Civl verifier."}],"citation":{"apa":"Kragl, B., &#38; Qadeer, S. (2021). The Civl verifier. In P. Ruzica &#38; M. W. Whalen (Eds.), <i>Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design</i> (Vol. 2, pp. 143–152). Virtual: TU Wien Academic Press. <a href=\"https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23\">https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23</a>","ama":"Kragl B, Qadeer S. The Civl verifier. In: Ruzica P, Whalen MW, eds. <i>Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design</i>. Vol 2. TU Wien Academic Press; 2021:143–152. doi:<a href=\"https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23\">10.34727/2021/isbn.978-3-85448-046-4_23</a>","ieee":"B. Kragl and S. Qadeer, “The Civl verifier,” in <i>Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design</i>, Virtual, 2021, vol. 2, pp. 143–152.","mla":"Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” <i>Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design</i>, edited by Piskac Ruzica and Michael W. Whalen, vol. 2, TU Wien Academic Press, 2021, pp. 143–152, doi:<a href=\"https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23\">10.34727/2021/isbn.978-3-85448-046-4_23</a>.","ista":"Kragl B, Qadeer S. 2021. The Civl verifier. Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, Conference Series, vol. 2, 143–152.","chicago":"Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” In <i>Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design</i>, edited by Piskac Ruzica and Michael W. Whalen, 2:143–152. TU Wien Academic Press, 2021. <a href=\"https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23\">https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23</a>.","short":"B. Kragl, S. Qadeer, in:, P. Ruzica, M.W. Whalen (Eds.), Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press, 2021, pp. 143–152."},"conference":{"name":"FMCAD: Formal Methods in Computer-Aided Design","end_date":"2021-10-22","location":"Virtual","start_date":"2021-10-20"},"oa_version":"Published Version","author":[{"orcid":"0000-0001-7745-9117","first_name":"Bernhard","last_name":"Kragl","full_name":"Kragl, Bernhard","id":"320FC952-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Shaz","last_name":"Qadeer","full_name":"Qadeer, Shaz"}],"editor":[{"first_name":"Piskac","last_name":"Ruzica","full_name":"Ruzica, Piskac"},{"first_name":"Michael W.","last_name":"Whalen","full_name":"Whalen, Michael W."}],"license":"https://creativecommons.org/licenses/by/4.0/","month":"10","doi":"10.34727/2021/isbn.978-3-85448-046-4_23","scopus_import":"1","language":[{"iso":"eng"}],"date_published":"2021-10-01T00:00:00Z","volume":2,"file_date_updated":"2022-01-26T08:04:29Z","has_accepted_license":"1","project":[{"name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF"}],"corr_author":"1","intvolume":"         2","publication_status":"published","day":"01","date_created":"2022-01-26T08:01:30Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","acknowledgement":"This research was performed while Bernhard Kragl was at IST Austria, supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","article_processing_charge":"No","_id":"10688","ddc":["000"],"quality_controlled":"1","publication":"Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design","alternative_title":["Conference Series"],"status":"public","oa":1,"file":[{"content_type":"application/pdf","date_updated":"2022-01-26T08:04:29Z","access_level":"open_access","creator":"cchlebak","relation":"main_file","file_id":"10689","success":1,"date_created":"2022-01-26T08:04:29Z","file_size":390555,"checksum":"35438ac9f9750340b7f8ae4ae3220d9f","file_name":"2021_FCAD2021_Kragl.pdf"}],"publisher":"TU Wien Academic Press","department":[{"_id":"ToHe"}],"page":"143–152"},{"date_updated":"2026-04-16T09:15:47Z","publication_identifier":{"issn":["0957-4174"],"eissn":["1873-6793"]},"type":"journal_article","title":"Boosting expensive synchronizing heuristics","year":"2021","oa_version":"Submitted Version","author":[{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E","last_name":"Sarac","first_name":"Naci E"},{"last_name":"Altun","first_name":"Ömer Faruk","full_name":"Altun, Ömer Faruk"},{"first_name":"Kamil Tolga","last_name":"Atam","full_name":"Atam, Kamil Tolga"},{"first_name":"Sertac","last_name":"Karahoda","full_name":"Karahoda, Sertac"},{"full_name":"Kaya, Kamer","last_name":"Kaya","first_name":"Kamer"},{"last_name":"Yenigün","first_name":"Hüsnü","full_name":"Yenigün, Hüsnü"}],"abstract":[{"text":"For automata, synchronization, the problem of bringing an automaton to a particular state regardless of its initial state, is important. It has several applications in practice and is related to a fifty-year-old conjecture on the length of the shortest synchronizing word. Although using shorter words increases the effectiveness in practice, finding a shortest one (which is not necessarily unique) is NP-hard. For this reason, there exist various heuristics in the literature. However, high-quality heuristics such as SynchroP producing relatively shorter sequences are very expensive and can take hours when the automaton has tens of thousands of states. The SynchroP heuristic has been frequently used as a benchmark to evaluate the performance of the new heuristics. In this work, we first improve the runtime of SynchroP and its variants by using algorithmic techniques. We then focus on adapting SynchroP for many-core architectures,\r\nand overall, we obtain more than 1000× speedup on GPUs compared to naive sequential implementation that has been frequently used as a benchmark to evaluate new heuristics in the literature. We also propose two SynchroP variants and evaluate their performance.","lang":"eng"}],"citation":{"mla":"Sarac, Naci E., et al. “Boosting Expensive Synchronizing Heuristics.” <i>Expert Systems with Applications</i>, vol. 167, no. 4, 114203, Elsevier, 2021, doi:<a href=\"https://doi.org/10.1016/j.eswa.2020.114203\">10.1016/j.eswa.2020.114203</a>.","ieee":"N. E. Sarac, Ö. F. Altun, K. T. Atam, S. Karahoda, K. Kaya, and H. Yenigün, “Boosting expensive synchronizing heuristics,” <i>Expert Systems with Applications</i>, vol. 167, no. 4. Elsevier, 2021.","ista":"Sarac NE, Altun ÖF, Atam KT, Karahoda S, Kaya K, Yenigün H. 2021. Boosting expensive synchronizing heuristics. Expert Systems with Applications. 167(4), 114203.","chicago":"Sarac, Naci E, Ömer Faruk Altun, Kamil Tolga Atam, Sertac Karahoda, Kamer Kaya, and Hüsnü Yenigün. “Boosting Expensive Synchronizing Heuristics.” <i>Expert Systems with Applications</i>. Elsevier, 2021. <a href=\"https://doi.org/10.1016/j.eswa.2020.114203\">https://doi.org/10.1016/j.eswa.2020.114203</a>.","short":"N.E. Sarac, Ö.F. Altun, K.T. Atam, S. Karahoda, K. Kaya, H. Yenigün, Expert Systems with Applications 167 (2021).","apa":"Sarac, N. E., Altun, Ö. F., Atam, K. T., Karahoda, S., Kaya, K., &#38; Yenigün, H. (2021). Boosting expensive synchronizing heuristics. <i>Expert Systems with Applications</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.eswa.2020.114203\">https://doi.org/10.1016/j.eswa.2020.114203</a>","ama":"Sarac NE, Altun ÖF, Atam KT, Karahoda S, Kaya K, Yenigün H. Boosting expensive synchronizing heuristics. <i>Expert Systems with Applications</i>. 2021;167(4). doi:<a href=\"https://doi.org/10.1016/j.eswa.2020.114203\">10.1016/j.eswa.2020.114203</a>"},"article_number":"114203","scopus_import":"1","doi":"10.1016/j.eswa.2020.114203","month":"04","date_published":"2021-04-01T00:00:00Z","volume":167,"has_accepted_license":"1","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"}],"file_date_updated":"2020-12-02T13:33:51Z","corr_author":"1","language":[{"iso":"eng"}],"article_type":"original","intvolume":"       167","publication_status":"published","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","day":"01","date_created":"2020-12-02T13:34:25Z","issue":"4","ddc":["000"],"quality_controlled":"1","external_id":{"isi":["000640531100038"]},"acknowledgement":"This work was supported by The Scientific and Technological Research Council of Turkey (TUBITAK) [grant number 114E569]. This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). We would like to thank the authors of (Roman & Szykula, 2015) for providing their heuristics implementations, which we used to compare our SynchroP implementation as given in Table 11.","_id":"8912","article_processing_charge":"No","isi":1,"file":[{"checksum":"600c2f81bc898a725bcfa7cf26ff4fed","date_created":"2020-12-02T13:33:51Z","file_size":634967,"file_name":"synchroPaperRevised.pdf","date_updated":"2020-12-02T13:33:51Z","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"8913","creator":"esarac"}],"oa":1,"publisher":"Elsevier","department":[{"_id":"ToHe"}],"publication":"Expert Systems with Applications","status":"public"},{"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"day":"01","date_created":"2021-02-26T16:30:39Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","keyword":["hybrid automaton","membership","system identification"],"publication":"HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control","status":"public","publisher":"Association for Computing Machinery","department":[{"_id":"ToHe"}],"page":"2102.12734","oa":1,"file":[{"success":1,"checksum":"4c1202c1abf71384c3ee6fea88c2f80e","file_size":1474786,"date_created":"2021-05-25T13:53:22Z","file_name":"2021_HSCC_Soto.pdf","date_updated":"2021-05-25T13:53:22Z","content_type":"application/pdf","access_level":"open_access","file_id":"9424","relation":"main_file","creator":"kschuh"}],"_id":"9200","article_processing_charge":"No","isi":1,"acknowledgement":"This research was supported 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łodowska-Curie grant agreement No. 754411.","ddc":["000"],"external_id":{"arxiv":["2102.12734"],"isi":["000932821700028"]},"quality_controlled":"1","abstract":[{"text":"Formal design of embedded and cyber-physical systems relies on mathematical modeling. In this paper, we consider the model class of hybrid automata whose dynamics are defined by affine differential equations. Given a set of time-series data, we present an algorithmic approach to synthesize a hybrid automaton exhibiting behavior that is close to the data, up to a specified precision, and changes in synchrony with the data. A fundamental problem in our synthesis algorithm is to check membership of a time series in a hybrid automaton. Our solution integrates reachability and optimization techniques for affine dynamical systems to obtain both a sufficient and a necessary condition for membership, combined in a refinement framework. The algorithm processes one time series at a time and hence can be interrupted, provide an intermediate result, and be resumed. We report experimental results demonstrating the applicability of our synthesis approach.","lang":"eng"}],"citation":{"apa":"Garcia Soto, M., Henzinger, T. A., &#38; Schilling, C. (2021). Synthesis of hybrid automata with affine dynamics from time-series data. In <i>HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control</i> (p. 2102.12734). Nashville, TN, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3447928.3456704\">https://doi.org/10.1145/3447928.3456704</a>","ama":"Garcia Soto M, Henzinger TA, Schilling C. Synthesis of hybrid automata with affine dynamics from time-series data. In: <i>HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control</i>. Association for Computing Machinery; 2021:2102.12734. doi:<a href=\"https://doi.org/10.1145/3447928.3456704\">10.1145/3447928.3456704</a>","ista":"Garcia Soto M, Henzinger TA, Schilling C. 2021. Synthesis of hybrid automata with affine dynamics from time-series data. HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 2102.12734.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis of Hybrid Automata with Affine Dynamics from Time-Series Data.” In <i>HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control</i>, 2102.12734. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3447928.3456704\">https://doi.org/10.1145/3447928.3456704</a>.","ieee":"M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of hybrid automata with affine dynamics from time-series data,” in <i>HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control</i>, Nashville, TN, United States, 2021, p. 2102.12734.","mla":"Garcia Soto, Miriam, et al. “Synthesis of Hybrid Automata with Affine Dynamics from Time-Series Data.” <i>HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control</i>, Association for Computing Machinery, 2021, p. 2102.12734, doi:<a href=\"https://doi.org/10.1145/3447928.3456704\">10.1145/3447928.3456704</a>.","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, Association for Computing Machinery, 2021, p. 2102.12734."},"author":[{"full_name":"Garcia Soto, Miriam","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2936-5719","first_name":"Miriam","last_name":"Garcia Soto"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling","full_name":"Schilling, Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"}],"conference":{"name":"HSCC: Hybrid Systems - Computation and Control","location":"Nashville, TN, United States","start_date":"2021-05-19","end_date":"2021-05-21"},"oa_version":"Published Version","year":"2021","title":"Synthesis of hybrid automata with affine dynamics from time-series data","publication_identifier":{"isbn":["9781450383394"]},"arxiv":1,"type":"conference","date_updated":"2025-07-10T12:01:40Z","language":[{"iso":"eng"}],"has_accepted_license":"1","file_date_updated":"2021-05-25T13:53:22Z","project":[{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","call_identifier":"H2020"}],"corr_author":"1","date_published":"2021-05-01T00:00:00Z","ec_funded":1,"doi":"10.1145/3447928.3456704","month":"05","scopus_import":"1"},{"publication_status":"published","intvolume":"       119","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.1905.03835"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","issue":"8","day":"03","date_created":"2021-03-14T23:01:32Z","quality_controlled":"1","external_id":{"isi":["000634149800009"],"arxiv":["1905.03835"]},"isi":1,"article_processing_charge":"No","_id":"9239","department":[{"_id":"ToHe"}],"page":"133-144","publisher":"Elsevier","oa":1,"status":"public","publication":"Journal of Computer and System Sciences","arxiv":1,"type":"journal_article","publication_identifier":{"issn":["0022-0000"],"eissn":["1090-2724"]},"date_updated":"2025-07-10T11:53:57Z","year":"2021","title":"Bidding mechanisms in graph games","related_material":{"record":[{"id":"6884","relation":"earlier_version","status":"public"}]},"author":[{"last_name":"Avni","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"first_name":"Đorđe","last_name":"Žikelić","full_name":"Žikelić, Đorđe"}],"oa_version":"Preprint","citation":{"short":"G. Avni, T.A. Henzinger, Đ. Žikelić, Journal of Computer and System Sciences 119 (2021) 133–144.","mla":"Avni, Guy, et al. “Bidding Mechanisms in Graph Games.” <i>Journal of Computer and System Sciences</i>, vol. 119, no. 8, Elsevier, 2021, pp. 133–44, doi:<a href=\"https://doi.org/10.1016/j.jcss.2021.02.008\">10.1016/j.jcss.2021.02.008</a>.","ieee":"G. Avni, T. A. Henzinger, and Đ. Žikelić, “Bidding mechanisms in graph games,” <i>Journal of Computer and System Sciences</i>, vol. 119, no. 8. Elsevier, pp. 133–144, 2021.","ista":"Avni G, Henzinger TA, Žikelić Đ. 2021. Bidding mechanisms in graph games. Journal of Computer and System Sciences. 119(8), 133–144.","chicago":"Avni, Guy, Thomas A Henzinger, and Đorđe Žikelić. “Bidding Mechanisms in Graph Games.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2021. <a href=\"https://doi.org/10.1016/j.jcss.2021.02.008\">https://doi.org/10.1016/j.jcss.2021.02.008</a>.","ama":"Avni G, Henzinger TA, Žikelić Đ. Bidding mechanisms in graph games. <i>Journal of Computer and System Sciences</i>. 2021;119(8):133-144. doi:<a href=\"https://doi.org/10.1016/j.jcss.2021.02.008\">10.1016/j.jcss.2021.02.008</a>","apa":"Avni, G., Henzinger, T. A., &#38; Žikelić, Đ. (2021). Bidding mechanisms in graph games. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2021.02.008\">https://doi.org/10.1016/j.jcss.2021.02.008</a>"},"abstract":[{"lang":"eng","text":"A graph game proceeds as follows: two players move a token through a graph to produce a finite or infinite path, which determines the payoff of the game. We study bidding games in which in each turn, an auction determines which player moves the token. Bidding games were largely studied in combination with two variants of first-price auctions called “Richman” and “poorman” bidding. We study taxman bidding, which span the spectrum between the two. The game is parameterized by a constant : portion τ of the winning bid is paid to the other player, and portion  to the bank. While finite-duration (reachability) taxman games have been studied before, we present, for the first time, results on infinite-duration taxman games: we unify, generalize, and simplify previous equivalences between bidding games and a class of stochastic games called random-turn games."}],"scopus_import":"1","doi":"10.1016/j.jcss.2021.02.008","month":"03","date_published":"2021-03-03T00:00:00Z","volume":119,"article_type":"original","language":[{"iso":"eng"}]},{"title":"Formal verification of Zagier's one-sentence proof","related_material":{"record":[{"relation":"other","status":"public","id":"9946"}]},"year":"2021","publication_status":"submitted","date_updated":"2025-04-15T06:26:12Z","type":"preprint","arxiv":1,"day":"21","date_created":"2021-03-23T05:38:48Z","article_number":"2103.11389","citation":{"ama":"Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2103.11389\">10.48550/arXiv.2103.11389</a>","apa":"Dubach, G., &#38; Mühlböck, F. (n.d.). Formal verification of Zagier’s one-sentence proof. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2103.11389\">https://doi.org/10.48550/arXiv.2103.11389</a>","short":"G. Dubach, F. Mühlböck, ArXiv (n.d.).","mla":"Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence Proof.” <i>ArXiv</i>, 2103.11389, doi:<a href=\"https://doi.org/10.48550/arXiv.2103.11389\">10.48550/arXiv.2103.11389</a>.","ieee":"G. Dubach and F. Mühlböck, “Formal verification of Zagier’s one-sentence proof,” <i>arXiv</i>. .","ista":"Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. arXiv, 2103.11389.","chicago":"Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence Proof.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2103.11389\">https://doi.org/10.48550/arXiv.2103.11389</a>."},"abstract":[{"lang":"eng","text":"We comment on two formal proofs of Fermat's sum of two squares theorem, written using the Mathematical Components libraries of the Coq proof assistant. The first one follows Zagier's celebrated one-sentence proof; the second follows David Christopher's recent new proof relying on partition-theoretic arguments. Both formal proofs rely on a general property of involutions of finite sets, of independent interest. The proof technique consists for the most part of automating recurrent tasks (such as case distinctions and computations on natural numbers) via ad hoc tactics."}],"oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2103.11389"}],"author":[{"id":"D5C6A458-10C4-11EA-ABF4-A4B43DDC885E","full_name":"Dubach, Guillaume","last_name":"Dubach","orcid":"0000-0001-6892-8137","first_name":"Guillaume"},{"last_name":"Mühlböck","orcid":"0000-0003-1548-0177","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","full_name":"Mühlböck, Fabian"}],"month":"03","_id":"9281","doi":"10.48550/arXiv.2103.11389","article_processing_charge":"No","external_id":{"arxiv":["2103.11389"]},"status":"public","language":[{"iso":"eng"}],"publication":"arXiv","oa":1,"ec_funded":1,"date_published":"2021-03-21T00:00:00Z","corr_author":"1","department":[{"_id":"LaEr"},{"_id":"ToHe"}],"project":[{"call_identifier":"H2020","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships"}]},{"scopus_import":"1","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","month":"06","doi":"10.1016/j.tcs.2021.05.023","date_published":"2021-06-04T00:00:00Z","volume":893,"file_date_updated":"2022-05-12T12:13:27Z","has_accepted_license":"1","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"}],"corr_author":"1","language":[{"iso":"eng"}],"article_type":"original","date_updated":"2025-04-15T06:25:56Z","publication_identifier":{"issn":["0304-3975"]},"type":"journal_article","title":"Long lived transients in gene regulation","year":"2021","oa_version":"Published Version","author":[{"full_name":"Petrov, Tatjana","last_name":"Petrov","first_name":"Tatjana"},{"last_name":"Igler","first_name":"Claudia","id":"46613666-F248-11E8-B48F-1D18A9856A87","full_name":"Igler, Claudia"},{"last_name":"Sezgin","first_name":"Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","full_name":"Sezgin, Ali"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","full_name":"Guet, Calin C","last_name":"Guet","orcid":"0000-0001-6220-2052","first_name":"Calin C"}],"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."}],"citation":{"mla":"Petrov, Tatjana, et al. “Long Lived Transients in Gene Regulation.” <i>Theoretical Computer Science</i>, vol. 893, Elsevier, 2021, pp. 1–16, doi:<a href=\"https://doi.org/10.1016/j.tcs.2021.05.023\">10.1016/j.tcs.2021.05.023</a>.","ieee":"T. Petrov, C. Igler, A. Sezgin, T. A. Henzinger, and C. C. Guet, “Long lived transients in gene regulation,” <i>Theoretical Computer Science</i>, vol. 893. Elsevier, pp. 1–16, 2021.","ista":"Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. 2021. Long lived transients in gene regulation. Theoretical Computer Science. 893, 1–16.","chicago":"Petrov, Tatjana, Claudia Igler, Ali Sezgin, Thomas A Henzinger, and Calin C Guet. “Long Lived Transients in Gene Regulation.” <i>Theoretical Computer Science</i>. Elsevier, 2021. <a href=\"https://doi.org/10.1016/j.tcs.2021.05.023\">https://doi.org/10.1016/j.tcs.2021.05.023</a>.","short":"T. Petrov, C. Igler, A. Sezgin, T.A. Henzinger, C.C. Guet, Theoretical Computer Science 893 (2021) 1–16.","apa":"Petrov, T., Igler, C., Sezgin, A., Henzinger, T. A., &#38; Guet, C. C. (2021). Long lived transients in gene regulation. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2021.05.023\">https://doi.org/10.1016/j.tcs.2021.05.023</a>","ama":"Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. Long lived transients in gene regulation. <i>Theoretical Computer Science</i>. 2021;893:1-16. doi:<a href=\"https://doi.org/10.1016/j.tcs.2021.05.023\">10.1016/j.tcs.2021.05.023</a>"},"ddc":["004"],"external_id":{"isi":["000710180500002"]},"quality_controlled":"1","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).","_id":"9647","article_processing_charge":"No","isi":1,"oa":1,"file":[{"creator":"dernst","relation":"main_file","file_id":"11364","date_updated":"2022-05-12T12:13:27Z","content_type":"application/pdf","access_level":"open_access","file_size":2566504,"date_created":"2022-05-12T12:13:27Z","checksum":"d3aef34cfb13e53bba4cf44d01680793","file_name":"2021_TheoreticalComputerScience_Petrov.pdf","success":1}],"publisher":"Elsevier","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"page":"1-16","publication":"Theoretical Computer Science","status":"public","intvolume":"       893","publication_status":"published","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","date_created":"2021-07-11T22:01:18Z","day":"04","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"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"}},{"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","day":"01","date_created":"2021-08-20T20:00:37Z","keyword":["run-time verification","software engineering","implicit specification"],"publication_status":"published","publisher":"IST Austria","page":"17","department":[{"_id":"ToHe"}],"oa":1,"file":[{"file_size":"320453","date_created":"2021-08-20T19:59:44Z","checksum":"0f9aafd59444cb6bdca6925d163ab946","file_name":"differentialmonitoring-techreport.pdf","creator":"fmuehlbo","relation":"main_file","file_id":"9948","date_updated":"2021-09-03T12:34:28Z","content_type":"application/pdf","access_level":"open_access"}],"status":"public","alternative_title":["IST Austria Technical Report"],"ddc":["005"],"_id":"9946","article_processing_charge":"No","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.","author":[{"last_name":"Mühlböck","first_name":"Fabian","orcid":"0000-0003-1548-0177","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","full_name":"Mühlböck, Fabian"},{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Published Version","abstract":[{"lang":"eng","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."}],"citation":{"mla":"Mühlböck, Fabian, and Thomas A. Henzinger. <i>Differential Monitoring</i>. IST Austria, 2021, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:9946\">10.15479/AT:ISTA:9946</a>.","ieee":"F. Mühlböck and T. A. Henzinger, <i>Differential monitoring</i>. IST Austria, 2021.","chicago":"Mühlböck, Fabian, and Thomas A Henzinger. <i>Differential Monitoring</i>. IST Austria, 2021. <a href=\"https://doi.org/10.15479/AT:ISTA:9946\">https://doi.org/10.15479/AT:ISTA:9946</a>.","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring, IST Austria, 17p.","short":"F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021.","apa":"Mühlböck, F., &#38; Henzinger, T. A. (2021). <i>Differential monitoring</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:9946\">https://doi.org/10.15479/AT:ISTA:9946</a>","ama":"Mühlböck F, Henzinger TA. <i>Differential Monitoring</i>. IST Austria; 2021. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:9946\">10.15479/AT:ISTA:9946</a>"},"publication_identifier":{"issn":["2664-1690"]},"type":"technical_report","date_updated":"2025-04-15T06:55:00Z","year":"2021","related_material":{"record":[{"relation":"shorter_version","status":"public","id":"10108"},{"id":"9281","relation":"other","status":"public"}]},"title":"Differential monitoring","file_date_updated":"2021-09-03T12:34:28Z","project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"}],"has_accepted_license":"1","date_published":"2021-09-01T00:00:00Z","language":[{"iso":"eng"}],"doi":"10.15479/AT:ISTA:9946","month":"09"},{"year":"2021","title":"Determinacy in discrete-bidding infinite-duration games","publication_identifier":{"eissn":["1860-5974"]},"type":"journal_article","arxiv":1,"date_updated":"2026-07-06T13:21:45Z","abstract":[{"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.","lang":"eng"}],"citation":{"ieee":"M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding infinite-duration games,” <i>Logical Methods in Computer Science</i>, vol. 17, no. 1. EPI Sciences, p. 10:1-10:23, 2021.","mla":"Aghajohari, Milad, et al. “Determinacy in Discrete-Bidding Infinite-Duration Games.” <i>Logical Methods in Computer Science</i>, vol. 17, no. 1, EPI Sciences, 2021, p. 10:1-10:23, doi:<a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">10.23638/LMCS-17(1:10)2021</a>.","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.” <i>Logical Methods in Computer Science</i>. EPI Sciences, 2021. <a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">https://doi.org/10.23638/LMCS-17(1:10)2021</a>.","short":"M. Aghajohari, G. Avni, T.A. Henzinger, Logical Methods in Computer Science 17 (2021) 10:1-10:23.","apa":"Aghajohari, M., Avni, G., &#38; Henzinger, T. A. (2021). Determinacy in discrete-bidding infinite-duration games. <i>Logical Methods in Computer Science</i>. EPI Sciences. <a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">https://doi.org/10.23638/LMCS-17(1:10)2021</a>","ama":"Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration games. <i>Logical Methods in Computer Science</i>. 2021;17(1):10:1-10:23. doi:<a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">10.23638/LMCS-17(1:10)2021</a>"},"author":[{"first_name":"Milad","last_name":"Aghajohari","full_name":"Aghajohari, Milad"},{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy","last_name":"Avni","orcid":"0000-0001-5588-8287","first_name":"Guy"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"oa_version":"Published Version","month":"02","doi":"10.23638/LMCS-17(1:10)2021","scopus_import":"1","article_type":"original","language":[{"iso":"eng"}],"file_date_updated":"2022-01-26T08:04:50Z","project":[{"name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","call_identifier":"FWF"},{"grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems"}],"has_accepted_license":"1","corr_author":"1","date_published":"2021-02-03T00:00:00Z","volume":17,"publication_status":"published","keyword":["computer science","computer science and game theory","logic in computer science"],"intvolume":"        17","issue":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"date_created":"2022-01-25T16:32:13Z","day":"03","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","_id":"10674","isi":1,"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","das_tickbox":"1","ddc":["510"],"external_id":{"arxiv":["1905.03588"],"isi":["000658724600010"]},"quality_controlled":"1","publication":"Logical Methods in Computer Science","status":"public","publisher":"EPI Sciences","department":[{"_id":"ToHe"}],"page":"10:1-10:23","oa":1,"file":[{"creator":"alisjak","relation":"main_file","file_id":"10690","access_level":"open_access","date_updated":"2022-01-26T08:04:50Z","content_type":"application/pdf","file_name":"2021_LMCS_AGHAJOHAR.pdf","file_size":819878,"date_created":"2022-01-26T08:04:50Z","checksum":"b35586a50ed1ca8f44767de116d18d81","success":1}]},{"doi":"10.1109/ICRA48506.2021.9561036","month":"06","scopus_import":"1","language":[{"iso":"eng"}],"has_accepted_license":"1","project":[{"call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems"}],"date_published":"2021-06-01T00:00:00Z","year":"2021","related_material":{"record":[{"id":"11362","status":"public","relation":"dissertation_contains"}]},"title":"Adversarial training is not ready for robot learning","publication_identifier":{"eisbn":["978-1-7281-9077-8"],"isbn":["978-1-7281-9078-5"],"issn":["1050-4729"],"eissn":["2577-087X"]},"arxiv":1,"type":"conference","date_updated":"2026-07-07T06:20:35Z","abstract":[{"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.","lang":"eng"}],"citation":{"short":"M. Lechner, R. Hasani, R. Grosu, D. Rus, T.A. Henzinger, in:, 2021 IEEE International Conference on Robotics and Automation, IEEE, 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 <i>2021 IEEE International Conference on Robotics and Automation</i>, 4140–47. IEEE, 2021. <a href=\"https://doi.org/10.1109/ICRA48506.2021.9561036\">https://doi.org/10.1109/ICRA48506.2021.9561036</a>.","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 Automation, 4140–4147.","mla":"Lechner, Mathias, et al. “Adversarial Training Is Not Ready for Robot Learning.” <i>2021 IEEE International Conference on Robotics and Automation</i>, IEEE, 2021, pp. 4140–47, doi:<a href=\"https://doi.org/10.1109/ICRA48506.2021.9561036\">10.1109/ICRA48506.2021.9561036</a>.","ieee":"M. Lechner, R. Hasani, R. Grosu, D. Rus, and T. A. Henzinger, “Adversarial training is not ready for robot learning,” in <i>2021 IEEE International Conference on Robotics and Automation</i>, Xi’an, China, 2021, pp. 4140–4147.","ama":"Lechner M, Hasani R, Grosu R, Rus D, Henzinger TA. Adversarial training is not ready for robot learning. In: <i>2021 IEEE International Conference on Robotics and Automation</i>. IEEE; 2021:4140-4147. doi:<a href=\"https://doi.org/10.1109/ICRA48506.2021.9561036\">10.1109/ICRA48506.2021.9561036</a>","apa":"Lechner, M., Hasani, R., Grosu, R., Rus, D., &#38; Henzinger, T. A. (2021). Adversarial training is not ready for robot learning. In <i>2021 IEEE International Conference on Robotics and Automation</i> (pp. 4140–4147). Xi’an, China: IEEE. <a href=\"https://doi.org/10.1109/ICRA48506.2021.9561036\">https://doi.org/10.1109/ICRA48506.2021.9561036</a>"},"author":[{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"full_name":"Hasani, Ramin","last_name":"Hasani","first_name":"Ramin"},{"full_name":"Grosu, Radu","last_name":"Grosu","first_name":"Radu"},{"first_name":"Daniela","last_name":"Rus","full_name":"Rus, Daniela"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger"}],"conference":{"end_date":"2021-06-05","location":"Xi'an, China","start_date":"2021-05-30","name":"ICRA: International Conference on Robotics and Automation"},"oa_version":"Preprint","article_processing_charge":"No","_id":"10666","OA_type":"green","isi":1,"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).","das_tickbox":"1","ddc":["000"],"external_id":{"arxiv":["2103.08187"],"isi":["000765738803040"]},"quality_controlled":"1","OA_place":"repository","publication":"2021 IEEE International Conference on Robotics and Automation","status":"public","publisher":"IEEE","page":"4140-4147","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"oa":1,"publication_status":"published","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","short":"CC BY-NC-ND (3.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode","image":"/images/cc_by_nc_nd.png"},"day":"01","date_created":"2022-01-25T15:44:54Z","main_file_link":[{"url":"https://arxiv.org/abs/2103.08187","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"corr_author":"1","project":[{"name":"International IST Doctoral Program","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"},{"name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF"}],"has_accepted_license":"1","file_date_updated":"2022-01-26T07:39:59Z","ec_funded":1,"date_published":"2021-12-01T00:00:00Z","language":[{"iso":"eng"}],"month":"12","doi":"10.48550/arXiv.2111.03165","author":[{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"full_name":"Žikelić, Ðorđe","first_name":"Ðorđe","last_name":"Žikelić"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger"}],"conference":{"name":"NeurIPS: Neural Information Processing Systems","location":"Virtual","start_date":"2021-12-06","end_date":"2021-12-10"},"oa_version":"Published Version","citation":{"short":"M. Lechner, Ð. Žikelić, K. Chatterjee, T.A. Henzinger, in:, 35th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2021.","ista":"Lechner M, Žikelić Ð, Chatterjee K, Henzinger TA. 2021. Infinite time horizon safety of Bayesian neural networks. 35th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems,  Advances in Neural Information Processing Systems, .","chicago":"Lechner, Mathias, Ðorđe Žikelić, Krishnendu Chatterjee, and Thomas A Henzinger. “Infinite Time Horizon Safety of Bayesian Neural Networks.” In <i>35th Conference on Neural Information Processing Systems</i>. Neural Information Processing Systems Foundation, 2021. <a href=\"https://doi.org/10.48550/arXiv.2111.03165\">https://doi.org/10.48550/arXiv.2111.03165</a>.","ieee":"M. Lechner, Ð. Žikelić, K. Chatterjee, and T. A. Henzinger, “Infinite time horizon safety of Bayesian neural networks,” in <i>35th Conference on Neural Information Processing Systems</i>, Virtual, 2021.","mla":"Lechner, Mathias, et al. “Infinite Time Horizon Safety of Bayesian Neural Networks.” <i>35th Conference on Neural Information Processing Systems</i>, Neural Information Processing Systems Foundation, 2021, doi:<a href=\"https://doi.org/10.48550/arXiv.2111.03165\">10.48550/arXiv.2111.03165</a>.","ama":"Lechner M, Žikelić Ð, Chatterjee K, Henzinger TA. Infinite time horizon safety of Bayesian neural networks. In: <i>35th Conference on Neural Information Processing Systems</i>. Neural Information Processing Systems Foundation; 2021. doi:<a href=\"https://doi.org/10.48550/arXiv.2111.03165\">10.48550/arXiv.2111.03165</a>","apa":"Lechner, M., Žikelić, Ð., Chatterjee, K., &#38; Henzinger, T. A. (2021). Infinite time horizon safety of Bayesian neural networks. In <i>35th Conference on Neural Information Processing Systems</i>. Virtual: Neural Information Processing Systems Foundation. <a href=\"https://doi.org/10.48550/arXiv.2111.03165\">https://doi.org/10.48550/arXiv.2111.03165</a>"},"abstract":[{"text":"Bayesian neural networks (BNNs) place distributions over the weights of a neural network to model uncertainty in the data and the network's prediction. We consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with infinite time horizon systems. Compared to the existing sampling-based approaches, which are inapplicable to the infinite time horizon setting, we train a separate deterministic neural network that serves as an infinite time horizon safety certificate. In particular, we show that the certificate network guarantees the safety of the system over a subset of the BNN weight posterior's support. Our method first computes a safe weight set and then alters the BNN's weight posterior to reject samples outside this set. Moreover, we show how to extend our approach to a safe-exploration reinforcement learning setting, in order to avoid unsafe trajectories during the training of the policy. We evaluate our approach on a series of reinforcement learning benchmarks, including non-Lyapunovian safety specifications.","lang":"eng"}],"arxiv":1,"type":"conference","publication_identifier":{"issn":["1049-5258"]},"date_updated":"2026-07-07T06:49:10Z","year":"2021","title":"Infinite time horizon safety of Bayesian neural networks","related_material":{"record":[{"id":"11362","status":"public","relation":"dissertation_contains"}]},"department":[{"_id":"GradSch"},{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Neural Information Processing Systems Foundation","oa":1,"file":[{"file_name":"infinite_time_horizon_safety_o.pdf","checksum":"0fc0f852525c10dda9cc9ffea07fb4e4","date_created":"2022-01-26T07:39:59Z","file_size":452492,"success":1,"file_id":"10682","relation":"main_file","creator":"mlechner","access_level":"open_access","date_updated":"2022-01-26T07:39:59Z","content_type":"application/pdf"}],"status":"public","alternative_title":[" Advances in Neural Information Processing Systems"],"publication":"35th Conference on Neural Information Processing Systems","das_tickbox":"1","external_id":{"arxiv":["2111.03165"]},"quality_controlled":"1","ddc":["000"],"article_processing_charge":"No","_id":"10667","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), ERC CoG 863818 (FoRM-SMArt), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","main_file_link":[{"url":"https://proceedings.neurips.cc/paper/2021/hash/544defa9fddff50c53b71c43e0da72be-Abstract.html","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","short":"CC BY-NC-ND (3.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode","image":"/images/cc_by_nc_nd.png"},"date_created":"2022-01-25T15:45:58Z","day":"01","publication_status":"published"},{"type":"conference","arxiv":1,"publication_identifier":{"issn":["1049-5258"]},"date_updated":"2026-07-07T06:49:46Z","year":"2021","title":"Causal navigation by continuous-time neural networks","author":[{"full_name":"Vorbach, Charles J","first_name":"Charles J","last_name":"Vorbach"},{"first_name":"Ramin","last_name":"Hasani","full_name":"Hasani, Ramin"},{"full_name":"Amini, Alexander","last_name":"Amini","first_name":"Alexander"},{"first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Rus, Daniela","first_name":"Daniela","last_name":"Rus"}],"oa_version":"Published Version","conference":{"name":"NeurIPS: Neural Information Processing Systems","end_date":"2021-12-10","start_date":"2021-12-06","location":"Virtual"},"citation":{"ama":"Vorbach CJ, Hasani R, Amini A, Lechner M, Rus D. Causal navigation by continuous-time neural networks. In: <i>35th Conference on Neural Information Processing Systems</i>. Neural Information Processing Systems Foundation; 2021.","apa":"Vorbach, C. J., Hasani, R., Amini, A., Lechner, M., &#38; Rus, D. (2021). Causal navigation by continuous-time neural networks. In <i>35th Conference on Neural Information Processing Systems</i>. Virtual: Neural Information Processing Systems Foundation.","short":"C.J. Vorbach, R. Hasani, A. Amini, M. Lechner, D. Rus, in:, 35th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2021.","ista":"Vorbach CJ, Hasani R, Amini A, Lechner M, Rus D. 2021. Causal navigation by continuous-time neural networks. 35th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems,  Advances in Neural Information Processing Systems, .","chicago":"Vorbach, Charles J, Ramin Hasani, Alexander Amini, Mathias Lechner, and Daniela Rus. “Causal Navigation by Continuous-Time Neural Networks.” In <i>35th Conference on Neural Information Processing Systems</i>. Neural Information Processing Systems Foundation, 2021.","ieee":"C. J. Vorbach, R. Hasani, A. Amini, M. Lechner, and D. Rus, “Causal navigation by continuous-time neural networks,” in <i>35th Conference on Neural Information Processing Systems</i>, Virtual, 2021.","mla":"Vorbach, Charles J., et al. “Causal Navigation by Continuous-Time Neural Networks.” <i>35th Conference on Neural Information Processing Systems</i>, Neural Information Processing Systems Foundation, 2021."},"abstract":[{"text":"Imitation learning enables high-fidelity, vision-based learning of policies within rich, photorealistic environments. However, such techniques often rely on traditional discrete-time neural models and face difficulties in generalizing to domain shifts by failing to account for the causal relationships between the agent and the environment. In this paper, we propose a theoretical and experimental framework for learning causal representations using continuous-time neural networks, specifically over their discrete-time counterparts. We evaluate our method in the context of visual-control learning of drones over a series of complex tasks, ranging from short- and long-term navigation, to chasing static and dynamic objects through photorealistic environments. Our results demonstrate that causal continuous-time\r\ndeep models can perform robust navigation tasks, where advanced recurrent models fail. These models learn complex causal control representations directly from raw visual inputs and scale to solve a variety of tasks using imitation learning.","lang":"eng"}],"month":"12","has_accepted_license":"1","file_date_updated":"2022-01-26T07:37:24Z","project":[{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"date_published":"2021-12-01T00:00:00Z","language":[{"iso":"eng"}],"publication_status":"published","main_file_link":[{"url":"https://proceedings.neurips.cc/paper/2021/hash/67ba02d73c54f0b83c05507b7fb7267f-Abstract.html","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","short":"CC BY-NC-ND (3.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode","image":"/images/cc_by_nc_nd.png"},"day":"01","date_created":"2022-01-25T15:47:50Z","das_tickbox":"1","quality_controlled":"1","external_id":{"arxiv":["2106.08314"]},"ddc":["000"],"_id":"10670","article_processing_charge":"No","acknowledgement":"C.V., R.H. A.A. and D.R. are partially supported by Boeing and MIT. A.A. is supported by the National Science Foundation (NSF) Graduate Research Fellowship Program. M.L. is supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). Research was sponsored by the United States Air Force Research Laboratory and the United States Air Force Artificial Intelligence Accelerator and was accomplished under Cooperative Agreement Number FA8750-19-2-1000. The views and conclusions contained in this document are those of the authors\r\nand should not be interpreted as representing the official policies, either expressed or implied, of the United States Air Force or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright notation herein.\r\n","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publisher":"Neural Information Processing Systems Foundation","oa":1,"file":[{"success":1,"file_name":"NeurIPS-2021-causal-navigation-by-continuous-time-neural-networks-Paper.pdf","checksum":"be81f0ade174a8c9b2d4fe09590b2021","date_created":"2022-01-26T07:37:24Z","file_size":6841228,"access_level":"open_access","content_type":"application/pdf","date_updated":"2022-01-26T07:37:24Z","relation":"main_file","file_id":"10679","creator":"mlechner"}],"alternative_title":[" Advances in Neural Information Processing Systems"],"status":"public","publication":"35th Conference on Neural Information Processing Systems"},{"status":"public","publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publisher":"Institute of Electrical and Electronics Engineers","oa":1,"file":[{"access_level":"open_access","content_type":"application/pdf","date_updated":"2021-06-16T08:23:54Z","creator":"esarac","file_id":"9557","relation":"main_file","success":1,"file_name":"qam.pdf","file_size":641990,"date_created":"2021-06-16T08:23:54Z","checksum":"6e4cba3f72775f479c5b1b75d1a4a0c4"}],"isi":1,"article_processing_charge":"No","_id":"9356","acknowledgement":"We thank the anonymous reviewers for their helpful comments. This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","quality_controlled":"1","external_id":{"arxiv":["2105.08353"],"isi":["000947350400021"]},"ddc":["000"],"date_created":"2021-04-30T17:30:47Z","day":"29","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"has_accepted_license":"1","file_date_updated":"2021-06-16T08:23:54Z","date_published":"2021-06-29T00:00:00Z","doi":"10.1109/LICS52264.2021.9470547","month":"06","scopus_import":"1","citation":{"short":"T.A. Henzinger, N.E. Sarac, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2021.","chicago":"Henzinger, Thomas A, and Naci E Sarac. “Quantitative and Approximate Monitoring.” In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Institute of Electrical and Electronics Engineers, 2021. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470547\">https://doi.org/10.1109/LICS52264.2021.9470547</a>.","ista":"Henzinger TA, Sarac NE. 2021. Quantitative and approximate monitoring. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 9470547.","ieee":"T. A. Henzinger and N. E. Sarac, “Quantitative and approximate monitoring,” in <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Online, 2021.","mla":"Henzinger, Thomas A., and Naci E. Sarac. “Quantitative and Approximate Monitoring.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 9470547, Institute of Electrical and Electronics Engineers, 2021, doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470547\">10.1109/LICS52264.2021.9470547</a>.","ama":"Henzinger TA, Sarac NE. Quantitative and approximate monitoring. In: <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Institute of Electrical and Electronics Engineers; 2021. doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470547\">10.1109/LICS52264.2021.9470547</a>","apa":"Henzinger, T. A., &#38; Sarac, N. E. (2021). Quantitative and approximate monitoring. In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Online: Institute of Electrical and Electronics Engineers. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470547\">https://doi.org/10.1109/LICS52264.2021.9470547</a>"},"article_number":"9470547","abstract":[{"lang":"eng","text":"In runtime verification, a monitor watches a trace of a system and, if possible, decides after observing each finite prefix whether or not the unknown infinite trace satisfies a given specification. We generalize the theory of runtime verification to monitors that attempt to estimate numerical values of quantitative trace properties (instead of attempting to conclude boolean values of trace specifications), such as maximal or average response time along a trace. Quantitative monitors are approximate: with every finite prefix, they can improve their estimate of the infinite trace's unknown property value. Consequently, quantitative monitors can be compared with regard to a precision-cost trade-off: better approximations of the property value require more monitor resources, such as states (in the case of finite-state monitors) or registers, and additional resources yield better approximations. We introduce a formal framework for quantitative and approximate monitoring, show how it conservatively generalizes the classical boolean setting for monitoring, and give several precision-cost trade-offs for monitors. For example, we prove that there are quantitative properties for which every additional register improves monitoring precision."}],"author":[{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E","last_name":"Sarac","first_name":"Naci E"}],"oa_version":"Published Version","conference":{"name":"LICS: Logic in Computer Science","start_date":"2021-06-29","location":"Online","end_date":"2021-07-02"},"year":"2021","title":"Quantitative and approximate monitoring","related_material":{"record":[{"id":"20147","relation":"dissertation_contains","status":"public"}]},"type":"conference","arxiv":1,"date_updated":"2026-07-27T12:48:18Z"},{"month":"08","doi":"10.1007/s10009-020-00582-z","scopus_import":"1","language":[{"iso":"eng"}],"article_type":"original","date_published":"2020-08-03T00:00:00Z","volume":22,"related_material":{"record":[{"id":"299","relation":"earlier_version","status":"public"}]},"title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","year":"2020","date_updated":"2024-10-09T20:58:18Z","publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"type":"journal_article","abstract":[{"text":"We introduce in this paper AMT2.0, a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended signal temporal logic, which integrates timed regular expressions within signal temporal logic. The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal. We demonstrate the tool functionality on several running examples and case studies, and evaluate its performance.","lang":"eng"}],"citation":{"ama":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. 2020;22(6):741-758. doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., &#38; Ulus, D. (2020). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>","short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal on Software Tools for Technology Transfer 22 (2020) 741–758.","ista":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2020. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer. 22(6), 741–758.","chicago":"Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>.","mla":"Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58, doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>.","ieee":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic,” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6. Springer Nature, pp. 741–758, 2020."},"oa_version":"None","author":[{"full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan","last_name":"Nickovic"},{"full_name":"Lebeltel, Olivier","first_name":"Olivier","last_name":"Lebeltel"},{"full_name":"Maler, Oded","first_name":"Oded","last_name":"Maler"},{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","last_name":"Ferrere","first_name":"Thomas","orcid":"0000-0001-5199-3143"},{"full_name":"Ulus, Dogan","first_name":"Dogan","last_name":"Ulus"}],"_id":"10861","article_processing_charge":"No","isi":1,"external_id":{"isi":["000555398600001"]},"quality_controlled":"1","publication":"International Journal on Software Tools for Technology Transfer","status":"public","publisher":"Springer Nature","department":[{"_id":"ToHe"}],"page":"741-758","intvolume":"        22","publication_status":"published","keyword":["Information Systems","Software"],"day":"03","date_created":"2022-03-18T10:10:53Z","issue":"6","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1"},{"title":"Learning representations for binary-classification without backpropagation","year":"2020","date_updated":"2025-04-15T06:25:56Z","type":"conference","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 <i>8th International Conference on Learning Representations</i>. ICLR, 2020.","mla":"Lechner, Mathias. “Learning Representations for Binary-Classification without Backpropagation.” <i>8th International Conference on Learning Representations</i>, ICLR, 2020.","ieee":"M. Lechner, “Learning representations for binary-classification without backpropagation,” in <i>8th International Conference on Learning Representations</i>, 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 <i>8th International Conference on Learning Representations</i>. Virtual ; Addis Ababa, Ethiopia: ICLR.","ama":"Lechner M. Learning representations for binary-classification without backpropagation. In: <i>8th International Conference on Learning Representations</i>. ICLR; 2020."},"abstract":[{"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.","lang":"eng"}],"conference":{"name":"ICLR: International Conference on Learning Representations","end_date":"2020-05-01","start_date":"2020-04-26","location":"Virtual ; Addis Ababa, Ethiopia"},"oa_version":"Published Version","author":[{"last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"}],"month":"03","scopus_import":"1","language":[{"iso":"eng"}],"date_published":"2020-03-11T00:00:00Z","corr_author":"1","file_date_updated":"2022-01-26T07:35:17Z","project":[{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"has_accepted_license":"1","publication_status":"published","date_created":"2022-01-25T15:50:00Z","day":"11","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","short":"CC BY-NC-ND (3.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode","image":"/images/cc_by_nc_nd.png"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://openreview.net/forum?id=Bke61krFvS"}],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23\r\n(Wittgenstein Award).\r\n","_id":"10672","article_processing_charge":"No","quality_controlled":"1","ddc":["000"],"status":"public","publication":"8th International Conference on Learning Representations","oa":1,"file":[{"file_name":"iclr_2020.pdf","date_created":"2022-01-26T07:35:17Z","file_size":249431,"checksum":"ea13d42dd4541ddb239b6a75821fd6c9","success":1,"creator":"mlechner","relation":"main_file","file_id":"10677","access_level":"open_access","date_updated":"2022-01-26T07:35:17Z","content_type":"application/pdf"}],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publisher":"ICLR"},{"has_accepted_license":"1","project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"}],"file_date_updated":"2022-01-26T11:08:51Z","date_published":"2020-01-01T00:00:00Z","language":[{"iso":"eng"}],"scopus_import":"1","author":[{"full_name":"Hasani, Ramin","first_name":"Ramin","last_name":"Hasani"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"full_name":"Amini, Alexander","last_name":"Amini","first_name":"Alexander"},{"first_name":"Daniela","last_name":"Rus","full_name":"Rus, Daniela"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"}],"conference":{"name":"ML: Machine Learning","end_date":"2020-07-18","location":"Virtual","start_date":"2020-07-12"},"oa_version":"Published Version","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."}],"citation":{"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.","chicago":"Hasani, Ramin, Mathias Lechner, Alexander Amini, Daniela Rus, and Radu Grosu. “A Natural Lottery Ticket Winner: Reinforcement Learning with Ordinary Neural Circuits.” In <i>Proceedings of the 37th International Conference on Machine Learning</i>, 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.” <i>Proceedings of the 37th International Conference on Machine Learning</i>, 2020, pp. 4082–93.","ieee":"R. Hasani, M. Lechner, A. Amini, D. Rus, and R. Grosu, “A natural lottery ticket winner: Reinforcement learning with ordinary neural circuits,” in <i>Proceedings of the 37th International Conference on Machine Learning</i>, Virtual, 2020, pp. 4082–4093.","ama":"Hasani R, Lechner M, Amini A, Rus D, Grosu R. A natural lottery ticket winner: Reinforcement learning with ordinary neural circuits. In: <i>Proceedings of the 37th International Conference on Machine Learning</i>. PMLR. ; 2020:4082-4093.","apa":"Hasani, R., Lechner, M., Amini, A., Rus, D., &#38; Grosu, R. (2020). A natural lottery ticket winner: Reinforcement learning with ordinary neural circuits. In <i>Proceedings of the 37th International Conference on Machine Learning</i> (pp. 4082–4093). Virtual."},"publication_identifier":{"issn":["2640-3498"]},"type":"conference","date_updated":"2025-04-15T06:25:56Z","year":"2020","title":"A natural lottery ticket winner: Reinforcement learning with ordinary neural circuits","series_title":"PMLR","page":"4082-4093","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file":[{"file_id":"10691","relation":"main_file","creator":"cchlebak","date_updated":"2022-01-26T11:08:51Z","content_type":"application/pdf","access_level":"open_access","checksum":"c9a4a29161777fc1a89ef451c040e3b1","date_created":"2022-01-26T11:08:51Z","file_size":2329798,"file_name":"2020_PMLR_Hasani.pdf","success":1}],"oa":1,"publication":"Proceedings of the 37th International Conference on Machine Learning","alternative_title":["PMLR"],"status":"public","ddc":["000"],"quality_controlled":"1","_id":"10673","article_processing_charge":"No","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","main_file_link":[{"open_access":"1","url":"http://proceedings.mlr.press/v119/hasani20a.html"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","short":"CC BY-NC-ND (3.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode","image":"/images/cc_by_nc_nd.png"},"date_created":"2022-01-25T15:50:34Z","publication_status":"published"},{"scopus_import":"1","month":"04","doi":"10.1007/978-3-030-45237-7_5","date_published":"2020-04-17T00:00:00Z","volume":12079,"corr_author":"1","has_accepted_license":"1","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"}],"file_date_updated":"2020-07-14T12:48:03Z","language":[{"iso":"eng"}],"date_updated":"2026-04-16T09:46:07Z","type":"conference","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783030452360"]},"title":"How many bits does it take to quantize your neural network?","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"11362"}]},"year":"2020","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2020-04-25","location":"Dublin, Ireland","end_date":"2020-04-30"},"oa_version":"Published Version","author":[{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","full_name":"Giacobbe, Mirco","last_name":"Giacobbe","first_name":"Mirco","orcid":"0000-0001-8180-0904"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"}],"citation":{"chicago":"Giacobbe, Mirco, Thomas A Henzinger, and Mathias Lechner. “How Many Bits Does It Take to Quantize Your Neural Network?” In <i>International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 12079:79–97. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-45237-7_5\">https://doi.org/10.1007/978-3-030-45237-7_5</a>.","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.","ieee":"M. Giacobbe, T. A. Henzinger, and M. Lechner, “How many bits does it take to quantize your neural network?,” in <i>International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Dublin, Ireland, 2020, vol. 12079, pp. 79–97.","mla":"Giacobbe, Mirco, et al. “How Many Bits Does It Take to Quantize Your Neural Network?” <i>International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 12079, Springer Nature, 2020, pp. 79–97, doi:<a href=\"https://doi.org/10.1007/978-3-030-45237-7_5\">10.1007/978-3-030-45237-7_5</a>.","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.","apa":"Giacobbe, M., Henzinger, T. A., &#38; Lechner, M. (2020). How many bits does it take to quantize your neural network? In <i>International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 12079, pp. 79–97). Dublin, Ireland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-45237-7_5\">https://doi.org/10.1007/978-3-030-45237-7_5</a>","ama":"Giacobbe M, Henzinger TA, Lechner M. How many bits does it take to quantize your neural network? In: <i>International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 12079. Springer Nature; 2020:79-97. doi:<a href=\"https://doi.org/10.1007/978-3-030-45237-7_5\">10.1007/978-3-030-45237-7_5</a>"},"abstract":[{"lang":"eng","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."}],"quality_controlled":"1","external_id":{"isi":["001288734300005"]},"ddc":["000"],"isi":1,"article_processing_charge":"No","_id":"7808","file":[{"file_name":"2020_TACAS_Giacobbe.pdf","checksum":"f19905a42891fe5ce93d69143fa3f6fb","date_created":"2020-05-26T12:48:15Z","file_size":2744030,"access_level":"open_access","date_updated":"2020-07-14T12:48:03Z","content_type":"application/pdf","file_id":"7893","relation":"main_file","creator":"dernst"}],"oa":1,"page":"79-97","department":[{"_id":"ToHe"}],"publisher":"Springer Nature","status":"public","alternative_title":["LNCS"],"publication":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","intvolume":"     12079","publication_status":"published","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","day":"17","date_created":"2020-05-10T22:00:49Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"}}]