--- _id: '14718' abstract: - lang: eng text: 'Binary decision diagrams (BDDs) are one of the fundamental data structures in formal methods and computer science in general. However, the performance of BDD-based algorithms greatly depends on memory latency due to the reliance on large hash tables and thus, by extension, on the speed of random memory access. This hinders the full utilisation of resources available on modern CPUs, since the absolute memory latency has not improved significantly for at least a decade. In this paper, we explore several implementation techniques that improve the performance of BDD manipulation either through enhanced memory locality or by partially eliminating random memory access. On a benchmark suite of 600+ BDDs derived from real-world applications, we demonstrate runtime that is comparable or better than parallelising the same operations on eight CPU cores. ' acknowledgement: "This work was supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413 and the\r\n“VAMOS” grant ERC-2020-AdG 101020093." article_processing_charge: No author: - first_name: Samuel full_name: Pastva, Samuel id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b last_name: Pastva orcid: 0000-0003-1993-0331 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Pastva S, Henzinger TA. Binary decision diagrams on modern hardware. In: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design. TU Vienna Academic Press; 2023:122-131. doi:10.34727/2023/isbn.978-3-85448-060-0_20' apa: 'Pastva, S., & Henzinger, T. A. (2023). Binary decision diagrams on modern hardware. In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (pp. 122–131). Ames, IA, United States: TU Vienna Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20' chicago: Pastva, Samuel, and Thomas A Henzinger. “Binary Decision Diagrams on Modern Hardware.” In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, 122–31. TU Vienna Academic Press, 2023. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20. ieee: S. Pastva and T. A. Henzinger, “Binary decision diagrams on modern hardware,” in Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, Ames, IA, United States, 2023, pp. 122–131. ista: 'Pastva S, Henzinger TA. 2023. Binary decision diagrams on modern hardware. Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design. FMCAD: Conference on Formal Methods in Computer-aided design, 122–131.' mla: Pastva, Samuel, and Thomas A. Henzinger. “Binary Decision Diagrams on Modern Hardware.” Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, TU Vienna Academic Press, 2023, pp. 122–31, doi:10.34727/2023/isbn.978-3-85448-060-0_20. short: S. Pastva, T.A. Henzinger, in:, Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, TU Vienna Academic Press, 2023, pp. 122–131. conference: end_date: 2023-10-27 location: Ames, IA, United States name: 'FMCAD: Conference on Formal Methods in Computer-aided design' start_date: 2023-10-25 date_created: 2023-12-31T23:01:03Z date_published: 2023-10-01T00:00:00Z date_updated: 2024-01-02T08:16:28Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.34727/2023/isbn.978-3-85448-060-0_20 ec_funded: 1 file: - access_level: open_access checksum: 818d6e13dd508f3a04f0941081022e5d content_type: application/pdf creator: dernst date_created: 2024-01-02T08:14:23Z date_updated: 2024-01-02T08:14:23Z file_id: '14721' file_name: 2023_FMCAD_Pastva.pdf file_size: 524321 relation: main_file success: 1 file_date_updated: 2024-01-02T08:14:23Z has_accepted_license: '1' language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: 122-131 project: - _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c call_identifier: H2020 grant_number: '101034413' name: 'IST-BRIDGE: International postdoctoral program' - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design publication_identifier: isbn: - '9783854480600' publication_status: published publisher: TU Vienna Academic Press quality_controlled: '1' scopus_import: '1' status: public title: Binary decision diagrams on modern hardware tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '14830' abstract: - lang: eng text: We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks. acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385. article_processing_charge: No author: - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: 'Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:11926-11935. doi:10.1609/aaai.v37i10.26407' apa: 'Zikelic, D., Lechner, M., Henzinger, T. A., & Chatterjee, K. (2023). Learning control policies for stochastic systems with reach-avoid guarantees. In Proceedings of the 37th AAAI Conference on Artificial Intelligence (Vol. 37, pp. 11926–11935). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v37i10.26407' chicago: Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” In Proceedings of the 37th AAAI Conference on Artificial Intelligence, 37:11926–35. Association for the Advancement of Artificial Intelligence, 2023. https://doi.org/10.1609/aaai.v37i10.26407. ieee: D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” in Proceedings of the 37th AAAI Conference on Artificial Intelligence, Washington, DC, United States, 2023, vol. 37, no. 10, pp. 11926–11935. ista: 'Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control policies for stochastic systems with reach-avoid guarantees. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 11926–11935.' mla: Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” Proceedings of the 37th AAAI Conference on Artificial Intelligence, vol. 37, no. 10, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–35, doi:10.1609/aaai.v37i10.26407. short: D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–11935. conference: end_date: 2023-02-14 location: Washington, DC, United States name: 'AAAI: Conference on Artificial Intelligence' start_date: 2023-02-07 date_created: 2024-01-18T07:44:31Z date_published: 2023-06-26T00:00:00Z date_updated: 2024-01-22T14:08:29Z day: '26' department: - _id: ToHe - _id: KrCh doi: 10.1609/aaai.v37i10.26407 ec_funded: 1 external_id: arxiv: - '2210.05308' intvolume: ' 37' issue: '10' keyword: - General Medicine language: - iso: eng month: '06' oa_version: Preprint page: 11926-11935 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 2564DBCA-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '665385' name: International IST Doctoral Program publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence publication_identifier: eissn: - 2374-3468 issn: - 2159-5399 publication_status: published publisher: Association for the Advancement of Artificial Intelligence quality_controlled: '1' related_material: record: - id: '14600' relation: earlier_version status: public status: public title: Learning control policies for stochastic systems with reach-avoid guarantees type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 37 year: '2023' ... --- _id: '13234' abstract: - lang: eng text: Neural-network classifiers achieve high accuracy when predicting the class of an input that they were trained to identify. Maintaining this accuracy in dynamic environments, where inputs frequently fall outside the fixed set of initially known classes, remains a challenge. We consider the problem of monitoring the classification decisions of neural networks in the presence of novel classes. For this purpose, we generalize our recently proposed abstraction-based monitor from binary output to real-valued quantitative output. This quantitative output enables new applications, two of which we investigate in the paper. As our first application, we introduce an algorithmic framework for active monitoring of a neural network, which allows us to learn new classes dynamically and yet maintain high monitoring performance. As our second application, we present an offline procedure to retrain the neural network to improve the monitor’s detection performance without deteriorating the network’s classification accuracy. Our experimental evaluation demonstrates both the benefits of our active monitoring framework in dynamic scenarios and the effectiveness of the retraining procedure. acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark, and by the Villum Investigator Grant S4OS. article_processing_charge: Yes (in subscription journal) article_type: original author: - first_name: Konstantin full_name: Kueffner, Konstantin id: 8121a2d0-dc85-11ea-9058-af578f3b4515 last_name: Kueffner orcid: 0000-0001-8974-2542 - first_name: Anna full_name: Lukina, Anna id: CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425 last_name: Lukina - first_name: Christian full_name: Schilling, Christian id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87 last_name: Schilling orcid: 0000-0003-3658-1065 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Kueffner K, Lukina A, Schilling C, Henzinger TA. Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. 2023;25:575-592. doi:10.1007/s10009-023-00711-4' apa: 'Kueffner, K., Lukina, A., Schilling, C., & Henzinger, T. A. (2023). Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. Springer Nature. https://doi.org/10.1007/s10009-023-00711-4' chicago: 'Kueffner, Konstantin, Anna Lukina, Christian Schilling, and Thomas A Henzinger. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” International Journal on Software Tools for Technology Transfer. Springer Nature, 2023. https://doi.org/10.1007/s10009-023-00711-4.' ieee: 'K. Kueffner, A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: Active monitoring of neural networks (extended version),” International Journal on Software Tools for Technology Transfer, vol. 25. Springer Nature, pp. 575–592, 2023.' ista: 'Kueffner K, Lukina A, Schilling C, Henzinger TA. 2023. Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. 25, 575–592.' mla: 'Kueffner, Konstantin, et al. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” International Journal on Software Tools for Technology Transfer, vol. 25, Springer Nature, 2023, pp. 575–92, doi:10.1007/s10009-023-00711-4.' short: K. Kueffner, A. Lukina, C. Schilling, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 25 (2023) 575–592. date_created: 2023-07-16T22:01:11Z date_published: 2023-08-01T00:00:00Z date_updated: 2024-01-30T12:06:57Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.1007/s10009-023-00711-4 ec_funded: 1 external_id: arxiv: - '2009.06429' isi: - '001020160000001' file: - access_level: open_access checksum: 3c4b347f39412a76872f9a6f30101f94 content_type: application/pdf creator: dernst date_created: 2024-01-30T12:06:07Z date_updated: 2024-01-30T12:06:07Z file_id: '14903' file_name: 2023_JourSoftwareTools_Kueffner.pdf file_size: 13387667 relation: main_file success: 1 file_date_updated: 2024-01-30T12:06:07Z has_accepted_license: '1' intvolume: ' 25' isi: 1 language: - iso: eng month: '08' oa: 1 oa_version: Published Version page: 575-592 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: International Journal on Software Tools for Technology Transfer publication_identifier: eissn: - 1433-2787 issn: - 1433-2779 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '10206' relation: shorter_version status: public scopus_import: '1' status: public title: 'Into the unknown: Active monitoring of neural networks (extended version)' tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 25 year: '2023' ... --- _id: '14920' abstract: - lang: eng text: "We consider fixpoint algorithms for two-player games on graphs with $\\omega$-regular winning conditions, where the environment is constrained by a strong transition fairness assumption. Strong transition fairness is a widely occurring special case of strong fairness, which requires that any execution is strongly fair with respect to a specified set of live edges: whenever the\r\nsource vertex of a live edge is visited infinitely often along a play, the edge itself is traversed infinitely often along the play as well. We show that, surprisingly, strong transition fairness retains the algorithmic characteristics of the fixpoint algorithms for $\\omega$-regular games -- the new algorithms have the same alternation depth as the classical algorithms but invoke a new type of predecessor operator. For Rabin games with $k$ pairs, the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is independent of the number of live edges in the strong transition fairness assumption. Further, we show that GR(1) specifications with strong transition fairness assumptions can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm. In contrast, strong fairness necessarily requires increasing the alternation depth depending on the number of fairness assumptions. We get symbolic algorithms for (generalized) Rabin, parity and GR(1) objectives under strong transition fairness assumptions as well as a direct symbolic algorithm for qualitative winning in stochastic\r\n$\\omega$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps, improving the state of the art. Finally, we have implemented a BDD-based synthesis engine based on our algorithm. We show on a set of synthetic and real benchmarks that our algorithm is scalable, parallelizable, and outperforms previous algorithms by orders of magnitude." acknowledgement: A previous version of this paper has appeared in TACAS 2022. Authors ordered alphabetically. T. Banerjee was interning with MPI-SWS when this research was conducted. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. article_number: '4' article_processing_charge: Yes article_type: original author: - first_name: Tamajit full_name: Banerjee, Tamajit last_name: Banerjee - first_name: Rupak full_name: Majumdar, Rupak last_name: Majumdar - first_name: Kaushik full_name: Mallik, Kaushik id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598 last_name: Mallik orcid: 0000-0001-9864-7475 - first_name: Anne-Kathrin full_name: Schmuck, Anne-Kathrin last_name: Schmuck - first_name: Sadegh full_name: Soudjani, Sadegh last_name: Soudjani citation: ama: Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. Fast symbolic algorithms for mega-regular games under strong transition fairness. TheoretiCS. 2023;2. doi:10.46298/theoretics.23.4 apa: Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., & Soudjani, S. (2023). Fast symbolic algorithms for mega-regular games under strong transition fairness. TheoretiCS. EPI Sciences. https://doi.org/10.46298/theoretics.23.4 chicago: Banerjee, Tamajit, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, and Sadegh Soudjani. “Fast Symbolic Algorithms for Mega-Regular Games under Strong Transition Fairness.” TheoretiCS. EPI Sciences, 2023. https://doi.org/10.46298/theoretics.23.4. ieee: T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani, “Fast symbolic algorithms for mega-regular games under strong transition fairness,” TheoretiCS, vol. 2. EPI Sciences, 2023. ista: Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. 2023. Fast symbolic algorithms for mega-regular games under strong transition fairness. TheoretiCS. 2, 4. mla: Banerjee, Tamajit, et al. “Fast Symbolic Algorithms for Mega-Regular Games under Strong Transition Fairness.” TheoretiCS, vol. 2, 4, EPI Sciences, 2023, doi:10.46298/theoretics.23.4. short: T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, TheoretiCS 2 (2023). date_created: 2024-01-31T13:40:49Z date_published: 2023-02-24T00:00:00Z date_updated: 2024-02-05T10:21:51Z day: '24' ddc: - '000' department: - _id: ToHe doi: 10.46298/theoretics.23.4 ec_funded: 1 external_id: arxiv: - '2202.07480' file: - access_level: open_access checksum: 2972d531122a6f15727b396110fb3f5c content_type: application/pdf creator: dernst date_created: 2024-02-05T10:19:35Z date_updated: 2024-02-05T10:19:35Z file_id: '14940' file_name: 2023_TheoretiCS_Banerjee.pdf file_size: 917076 relation: main_file success: 1 file_date_updated: 2024-02-05T10:19:35Z has_accepted_license: '1' intvolume: ' 2' language: - iso: eng month: '02' oa: 1 oa_version: Published Version project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: TheoretiCS publication_identifier: issn: - 2751-4838 publication_status: published publisher: EPI Sciences quality_controlled: '1' status: public title: Fast symbolic algorithms for mega-regular games under strong transition fairness tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 2 year: '2023' ... --- _id: '14411' abstract: - lang: eng text: "Partially specified Boolean networks (PSBNs) represent a promising framework for the qualitative modelling of biological systems in which the logic of interactions is not completely known. Phenotype control aims to stabilise the network in states exhibiting specific traits.\r\nIn this paper, we define the phenotype control problem in the context of asynchronous PSBNs and propose a novel semi-symbolic algorithm for solving this problem with permanent variable perturbations." acknowledgement: This work was supported by the Czech Foundation grant No. GA22-10845S, Grant Agency of Masaryk University grant No. MUNI/G/1771/2020, and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413. alternative_title: - LNBI article_processing_charge: No author: - first_name: Nikola full_name: Beneš, Nikola last_name: Beneš - first_name: Luboš full_name: Brim, Luboš last_name: Brim - first_name: Samuel full_name: Pastva, Samuel id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b last_name: Pastva orcid: 0000-0003-1993-0331 - first_name: David full_name: Šafránek, David last_name: Šafránek - first_name: Eva full_name: Šmijáková, Eva last_name: Šmijáková citation: ama: 'Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. Phenotype control of partially specified boolean networks. In: 21st International Conference on Computational Methods in Systems Biology. Vol 14137. Springer Nature; 2023:18-35. doi:10.1007/978-3-031-42697-1_2' apa: 'Beneš, N., Brim, L., Pastva, S., Šafránek, D., & Šmijáková, E. (2023). Phenotype control of partially specified boolean networks. In 21st International Conference on Computational Methods in Systems Biology (Vol. 14137, pp. 18–35). Luxembourg City, Luxembourg: Springer Nature. https://doi.org/10.1007/978-3-031-42697-1_2' chicago: Beneš, Nikola, Luboš Brim, Samuel Pastva, David Šafránek, and Eva Šmijáková. “Phenotype Control of Partially Specified Boolean Networks.” In 21st International Conference on Computational Methods in Systems Biology, 14137:18–35. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-42697-1_2. ieee: N. Beneš, L. Brim, S. Pastva, D. Šafránek, and E. Šmijáková, “Phenotype control of partially specified boolean networks,” in 21st International Conference on Computational Methods in Systems Biology, Luxembourg City, Luxembourg, 2023, vol. 14137, pp. 18–35. ista: 'Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. 2023. Phenotype control of partially specified boolean networks. 21st International Conference on Computational Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNBI, vol. 14137, 18–35.' mla: Beneš, Nikola, et al. “Phenotype Control of Partially Specified Boolean Networks.” 21st International Conference on Computational Methods in Systems Biology, vol. 14137, Springer Nature, 2023, pp. 18–35, doi:10.1007/978-3-031-42697-1_2. short: N. Beneš, L. Brim, S. Pastva, D. Šafránek, E. Šmijáková, in:, 21st International Conference on Computational Methods in Systems Biology, Springer Nature, 2023, pp. 18–35. conference: end_date: 2023-09-15 location: Luxembourg City, Luxembourg name: 'CMSB: Computational Methods in Systems Biology' start_date: 2023-09-13 date_created: 2023-10-08T22:01:18Z date_published: 2023-09-09T00:00:00Z date_updated: 2024-02-20T09:02:04Z day: '09' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-031-42697-1_2 ec_funded: 1 file: - access_level: open_access checksum: 6f71bdaedb770b52380222fd9f4d7937 content_type: application/pdf creator: spastva date_created: 2024-02-16T08:26:32Z date_updated: 2024-02-16T08:26:32Z file_id: '14997' file_name: cmsb2023.pdf file_size: 691582 relation: main_file success: 1 file_date_updated: 2024-02-16T08:26:32Z has_accepted_license: '1' intvolume: ' 14137' language: - iso: eng month: '09' oa: 1 oa_version: Submitted Version page: 18-35 project: - _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c call_identifier: H2020 grant_number: '101034413' name: 'IST-BRIDGE: International postdoctoral program' publication: 21st International Conference on Computational Methods in Systems Biology publication_identifier: eissn: - 1611-3349 isbn: - '9783031426964' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Phenotype control of partially specified boolean networks tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 14137 year: '2023' ... --- _id: '14758' abstract: - lang: eng text: 'We present a flexible and efficient toolchain to symbolically solve (standard) Rabin games, fair-adversarial Rabin games, and 2 1/2 license type-player Rabin games. To our best knowledge, our tools are the first ones to be able to solve these problems. Furthermore, using these flexible game solvers as a back-end, we implemented a tool for computing correct-by-construction controllers for stochastic dynamical systems under LTL specifications. Our implementations use the recent theoretical result that all of these games can be solved using the same symbolic fixpoint algorithm but utilizing different, domain specific calculations of the involved predecessor operators. The main feature of our toolchain is the utilization of two programming abstractions: one to separate the symbolic fixpoint computations from the predecessor calculations, and another one to allow the integration of different BDD libraries as back-ends. In particular, we employ a multi-threaded execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan, which leads to enormous computational savings.' acknowledgement: 'Authors ordered alphabetically. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248-CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. M. Rychlicki is supported by the EPSRC project EP/V00252X/1. S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047.' alternative_title: - LNCS article_processing_charge: Yes (in subscription journal) author: - first_name: Rupak full_name: Majumdar, Rupak last_name: Majumdar - first_name: Kaushik full_name: Mallik, Kaushik id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598 last_name: Mallik orcid: 0000-0001-9864-7475 - first_name: Mateusz full_name: Rychlicki, Mateusz last_name: Rychlicki - first_name: Anne-Kathrin full_name: Schmuck, Anne-Kathrin last_name: Schmuck - first_name: Sadegh full_name: Soudjani, Sadegh last_name: Soudjani citation: ama: 'Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In: 35th International Conference on Computer Aided Verification. Vol 13966. Springer Nature; 2023:3-15. doi:10.1007/978-3-031-37709-9_1' apa: 'Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., & Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In 35th International Conference on Computer Aided Verification (Vol. 13966, pp. 3–15). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37709-9_1' chicago: Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” In 35th International Conference on Computer Aided Verification, 13966:3–15. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37709-9_1. ieee: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties,” in 35th International Conference on Computer Aided Verification, Paris, France, 2023, vol. 13966, pp. 3–15. ista: 'Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 35th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 3–15.' mla: Majumdar, Rupak, et al. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” 35th International Conference on Computer Aided Verification, vol. 13966, Springer Nature, 2023, pp. 3–15, doi:10.1007/978-3-031-37709-9_1. short: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, in:, 35th International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 3–15. conference: end_date: 2023-07-22 location: Paris, France name: 'CAV: Computer Aided Verification' start_date: 2023-07-17 date_created: 2024-01-08T13:18:00Z date_published: 2023-07-16T00:00:00Z date_updated: 2024-02-27T07:39:51Z day: '16' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-031-37709-9_1 ec_funded: 1 file: - access_level: open_access checksum: 1a361d83db0244fd32c03b544c294b5a content_type: application/pdf creator: dernst date_created: 2024-01-09T10:01:07Z date_updated: 2024-01-09T10:01:07Z file_id: '14765' file_name: 2023_LNCSCAV_Majumdar.pdf file_size: 405147 relation: main_file success: 1 file_date_updated: 2024-01-09T10:01:07Z has_accepted_license: '1' intvolume: ' 13966' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: 3-15 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 35th International Conference on Computer Aided Verification publication_identifier: eisbn: - '9783031377099' eissn: - 1611-3349 isbn: - '9783031377082' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '14994' relation: research_data status: public scopus_import: '1' status: public title: A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13966 year: '2023' ... --- _id: '14994' abstract: - lang: eng text: This resource contains the artifacts for reproducing the experimental results presented in the paper titled "A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties" that has been submitted in CAV 2023. article_processing_charge: No author: - first_name: Rupak full_name: Majumdar, Rupak last_name: Majumdar - first_name: Kaushik full_name: Mallik, Kaushik id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598 last_name: Mallik orcid: 0000-0001-9864-7475 - first_name: Mateusz full_name: Rychlicki, Mateusz last_name: Rychlicki - first_name: Anne-Kathrin full_name: Schmuck, Anne-Kathrin last_name: Schmuck - first_name: Sadegh full_name: Soudjani, Sadegh last_name: Soudjani citation: ama: Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 2023. doi:10.5281/ZENODO.7877790 apa: Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., & Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. Zenodo. https://doi.org/10.5281/ZENODO.7877790 chicago: Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.7877790. ieee: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties.” Zenodo, 2023. ista: Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties, Zenodo, 10.5281/ZENODO.7877790. mla: Majumdar, Rupak, et al. A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties. Zenodo, 2023, doi:10.5281/ZENODO.7877790. short: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, (2023). date_created: 2024-02-14T15:13:00Z date_published: 2023-04-28T00:00:00Z date_updated: 2024-02-27T07:39:51Z day: '28' ddc: - '000' department: - _id: ToHe doi: 10.5281/ZENODO.7877790 has_accepted_license: '1' main_file_link: - open_access: '1' url: https://doi.org/10.5281/zenodo.7877790 month: '04' oa: 1 oa_version: Published Version publisher: Zenodo related_material: record: - id: '14758' relation: used_in_publication status: public status: public title: A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: research_data_reference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '15023' abstract: - lang: eng text: Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph’s sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment. acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS) and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt)." article_processing_charge: No author: - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Abhinav full_name: Verma, Abhinav id: a235593c-d7fa-11eb-a0c5-b22ca3c66ee6 last_name: Verma - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. Compositional policy learning in stochastic control systems with formal guarantees. In: 37th Conference on Neural Information Processing Systems. ; 2023.' apa: Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., & Henzinger, T. A. (2023). Compositional policy learning in stochastic control systems with formal guarantees. In 37th Conference on Neural Information Processing Systems. New Orleans, LO, United States. chicago: Zikelic, Dorde, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A Henzinger. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” In 37th Conference on Neural Information Processing Systems, 2023. ieee: D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger, “Compositional policy learning in stochastic control systems with formal guarantees,” in 37th Conference on Neural Information Processing Systems, New Orleans, LO, United States, 2023. ista: 'Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional policy learning in stochastic control systems with formal guarantees. 37th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems.' mla: Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” 37th Conference on Neural Information Processing Systems, 2023. short: D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th Conference on Neural Information Processing Systems, 2023. conference: end_date: 2023-12-16 location: New Orleans, LO, United States name: 'NeurIPS: Neural Information Processing Systems' start_date: 2023-12-10 date_created: 2024-02-25T09:23:24Z date_published: 2023-12-15T00:00:00Z date_updated: 2024-02-28T12:20:11Z day: '15' department: - _id: ToHe - _id: KrCh ec_funded: 1 external_id: arxiv: - '2312.01456' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2312.01456 month: '12' oa: 1 oa_version: Preprint project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 37th Conference on Neural Information Processing Systems publication_status: epub_ahead quality_controlled: '1' status: public title: Compositional policy learning in stochastic control systems with formal guarantees type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '14076' abstract: - lang: eng text: Hyperproperties are properties that relate multiple execution traces. Previous work on monitoring hyperproperties focused on synchronous hyperproperties, usually specified in HyperLTL. When monitoring synchronous hyperproperties, all traces are assumed to proceed at the same speed. We introduce (multi-trace) prefix transducers and show how to use them for monitoring synchronous as well as, for the first time, asynchronous hyperproperties. Prefix transducers map multiple input traces into one or more output traces by incrementally matching prefixes of the input traces against expressions similar to regular expressions. The prefixes of different traces which are consumed by a single matching step of the monitor may have different lengths. The deterministic and executable nature of prefix transducers makes them more suitable as an intermediate formalism for runtime verification than logical specifications, which tend to be highly non-deterministic, especially in the case of asynchronous hyperproperties. We report on a set of experiments about monitoring asynchronous version of observational determinism. acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank Ana Oliveira da Costa for commenting on a draft of the paper. alternative_title: - LNCS article_processing_charge: Yes (in subscription journal) author: - first_name: Marek full_name: Chalupa, Marek id: 87e34708-d6c6-11ec-9f5b-9391e7be2463 last_name: Chalupa - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. In: 23nd International Conference on Runtime Verification. Vol 14245. Springer Nature; 2023:168-190. doi:10.1007/978-3-031-44267-4_9' apa: 'Chalupa, M., & Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. In 23nd International Conference on Runtime Verification (Vol. 14245, pp. 168–190). Thessaloniki, Greek: Springer Nature. https://doi.org/10.1007/978-3-031-44267-4_9' chicago: Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” In 23nd International Conference on Runtime Verification, 14245:168–90. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_9. ieee: M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers,” in 23nd International Conference on Runtime Verification, Thessaloniki, Greek, 2023, vol. 14245, pp. 168–190. ista: 'Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers. 23nd International Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS, vol. 14245, 168–190.' mla: Chalupa, Marek, and Thomas A. Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” 23nd International Conference on Runtime Verification, vol. 14245, Springer Nature, 2023, pp. 168–90, doi:10.1007/978-3-031-44267-4_9. short: M. Chalupa, T.A. Henzinger, in:, 23nd International Conference on Runtime Verification, Springer Nature, 2023, pp. 168–190. conference: end_date: 2023-10-07 location: Thessaloniki, Greek name: 'RV: Conference on Runtime Verification' start_date: 2023-10-04 date_created: 2023-08-16T20:46:08Z date_published: 2023-10-01T00:00:00Z date_updated: 2024-02-28T12:33:08Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-031-44267-4_9 ec_funded: 1 file: - access_level: open_access checksum: ee33bd6f1a26f4dae7a8192584869fd8 content_type: application/pdf creator: dernst date_created: 2023-10-16T07:15:11Z date_updated: 2023-10-16T07:15:11Z file_id: '14430' file_name: 2023_LNCS_RV_Chalupa.pdf file_size: 867256 relation: main_file success: 1 file_date_updated: 2023-10-16T07:15:11Z has_accepted_license: '1' intvolume: ' 14245' language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: 168-190 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 23nd International Conference on Runtime Verification publication_identifier: eisbn: - 978-3-031-44267-4 isbn: - 978-3-031-44266-7 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '15035' relation: research_data status: public status: public title: Monitoring hyperproperties with prefix transducers tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 14245 year: '2023' ... --- _id: '15035' abstract: - lang: eng text: "This artifact aims to reproduce experiments from the paper Monitoring Hyperproperties With Prefix Transducers accepted at RV'23, and give further pointers to implementation of prefix transducers.\r\nIt has two parts: a pre-compiled docker image and sources that one can use to compile (locally or in docker) the software and run the experiments." article_processing_charge: No author: - first_name: Marek full_name: Chalupa, Marek id: 87e34708-d6c6-11ec-9f5b-9391e7be2463 last_name: Chalupa - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. 2023. doi:10.5281/ZENODO.8191723 apa: Chalupa, M., & Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. Zenodo. https://doi.org/10.5281/ZENODO.8191723 chicago: Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.8191723. ieee: M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers.” Zenodo, 2023. ista: Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers, Zenodo, 10.5281/ZENODO.8191723. mla: Chalupa, Marek, and Thomas A. Henzinger. Monitoring Hyperproperties with Prefix Transducers. Zenodo, 2023, doi:10.5281/ZENODO.8191723. short: M. Chalupa, T.A. Henzinger, (2023). date_created: 2024-02-28T07:34:34Z date_published: 2023-07-28T00:00:00Z date_updated: 2024-02-28T12:33:09Z day: '28' ddc: - '000' department: - _id: ToHe doi: 10.5281/ZENODO.8191723 ec_funded: 1 has_accepted_license: '1' main_file_link: - open_access: '1' url: https://doi.org/10.5281/zenodo.8191722 month: '07' oa: 1 oa_version: Published Version project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publisher: Zenodo related_material: record: - id: '14076' relation: used_in_publication status: public status: public title: Monitoring hyperproperties with prefix transducers tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: research_data_reference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '10774' abstract: - lang: eng text: We study the problem of specifying sequential information-flow properties of systems. Information-flow properties are hyperproperties, as they compare different traces of a system. Sequential information-flow properties can express changes, over time, in the information-flow constraints. For example, information-flow constraints during an initialization phase of a system may be different from information-flow constraints that are required during the operation phase. We formalize several variants of interpreting sequential information-flow constraints, which arise from different assumptions about what can be observed of the system. For this purpose, we introduce a first-order logic, called Hypertrace Logic, with both trace and time quantifiers for specifying linear-time hyperproperties. We prove that HyperLTL, which corresponds to a fragment of Hypertrace Logic with restricted quantifier prefixes, cannot specify the majority of the studied variants of sequential information flow, including all variants in which the transition between sequential phases (such as initialization and operation) happens asynchronously. Our results rely on new equivalences between sets of traces that cannot be distinguished by certain classes of formulas from Hypertrace Logic. This presents a new approach to proving inexpressiveness results for HyperLTL. acknowledgement: This work was funded in part by the Wittgenstein Award Z211-N23 of the Austrian Science Fund (FWF) and by the FWF project W1255-N23. alternative_title: - LNCS article_processing_charge: No author: - first_name: Ezio full_name: Bartocci, Ezio last_name: Bartocci - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Ana Oliveira full_name: Da Costa, Ana Oliveira last_name: Da Costa citation: ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential information flow. In: Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 13182. Springer Nature; 2022:1-19. doi:10.1007/978-3-030-94583-1_1' apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa, A. O. (2022). Flavors of sequential information flow. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13182, pp. 1–19). Philadelphia, PA, United States: Springer Nature. https://doi.org/10.1007/978-3-030-94583-1_1' chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 13182:1–19. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-94583-1_1. ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Flavors of sequential information flow,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Philadelphia, PA, United States, 2022, vol. 13182, pp. 1–19. ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Flavors of sequential information flow. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 13182, 1–19.' mla: Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13182, Springer Nature, 2022, pp. 1–19, doi:10.1007/978-3-030-94583-1_1. short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:, Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2022, pp. 1–19. conference: end_date: 2022-01-18 location: Philadelphia, PA, United States name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation' start_date: 2022-01-16 date_created: 2022-02-20T23:01:34Z date_published: 2022-01-14T00:00:00Z date_updated: 2022-08-05T09:02:56Z day: '14' department: - _id: ToHe doi: 10.1007/978-3-030-94583-1_1 external_id: arxiv: - '2105.02013' intvolume: ' 13182' language: - iso: eng main_file_link: - open_access: '1' url: ' https://doi.org/10.48550/arXiv.2105.02013' month: '01' oa: 1 oa_version: Preprint page: 1-19 project: - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) publication_identifier: eissn: - '16113349' isbn: - '9783030945824' issn: - '03029743' publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Flavors of sequential information flow type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13182 year: '2022' ... --- _id: '12010' abstract: - lang: eng text: World models learn behaviors in a latent imagination space to enhance the sample-efficiency of deep reinforcement learning (RL) algorithms. While learning world models for high-dimensional observations (e.g., pixel inputs) has become practicable on standard RL benchmarks and some games, their effectiveness in real-world robotics applications has not been explored. In this paper, we investigate how such agents generalize to real-world autonomous vehicle control tasks, where advanced model-free deep RL algorithms fail. In particular, we set up a series of time-lap tasks for an F1TENTH racing robot, equipped with a high-dimensional LiDAR sensor, on a set of test tracks with a gradual increase in their complexity. In this continuous-control setting, we show that model-based agents capable of learning in imagination substantially outperform model-free agents with respect to performance, sample efficiency, successful task completion, and generalization. Moreover, we show that the generalization ability of model-based agents strongly depends on the choice of their observation model. We provide extensive empirical evidence for the effectiveness of world models provided with long enough memory horizons in sim2real tasks. acknowledgement: L.B. was supported by the Doctoral College Resilient Embedded Systems. M.L. was supported in part by the ERC2020-AdG 101020093 and the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). R.H. and D.R. were supported by The Boeing Company and the Office of Naval Research (ONR) Grant N00014-18-1-2830. R.G. was partially supported by the Horizon-2020 ECSEL Project grant No. 783163 (iDev40) and A.B. by FFG Project ADEX. article_processing_charge: No author: - first_name: Axel full_name: Brunnbauer, Axel last_name: Brunnbauer - first_name: Luigi full_name: Berducci, Luigi last_name: Berducci - first_name: Andreas full_name: Brandstatter, Andreas last_name: Brandstatter - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Ramin full_name: Hasani, Ramin last_name: Hasani - first_name: Daniela full_name: Rus, Daniela last_name: Rus - first_name: Radu full_name: Grosu, Radu last_name: Grosu citation: ama: 'Brunnbauer A, Berducci L, Brandstatter A, et al. Latent imagination facilitates zero-shot transfer in autonomous racing. In: 2022 International Conference on Robotics and Automation. IEEE; 2022:7513-7520. doi:10.1109/ICRA46639.2022.9811650' apa: 'Brunnbauer, A., Berducci, L., Brandstatter, A., Lechner, M., Hasani, R., Rus, D., & Grosu, R. (2022). Latent imagination facilitates zero-shot transfer in autonomous racing. In 2022 International Conference on Robotics and Automation (pp. 7513–7520). Philadelphia, PA, United States: IEEE. https://doi.org/10.1109/ICRA46639.2022.9811650' chicago: Brunnbauer, Axel, Luigi Berducci, Andreas Brandstatter, Mathias Lechner, Ramin Hasani, Daniela Rus, and Radu Grosu. “Latent Imagination Facilitates Zero-Shot Transfer in Autonomous Racing.” In 2022 International Conference on Robotics and Automation, 7513–20. IEEE, 2022. https://doi.org/10.1109/ICRA46639.2022.9811650. ieee: A. Brunnbauer et al., “Latent imagination facilitates zero-shot transfer in autonomous racing,” in 2022 International Conference on Robotics and Automation, Philadelphia, PA, United States, 2022, pp. 7513–7520. ista: 'Brunnbauer A, Berducci L, Brandstatter A, Lechner M, Hasani R, Rus D, Grosu R. 2022. Latent imagination facilitates zero-shot transfer in autonomous racing. 2022 International Conference on Robotics and Automation. ICRA: International Conference on Robotics and Automation, 7513–7520.' mla: Brunnbauer, Axel, et al. “Latent Imagination Facilitates Zero-Shot Transfer in Autonomous Racing.” 2022 International Conference on Robotics and Automation, IEEE, 2022, pp. 7513–20, doi:10.1109/ICRA46639.2022.9811650. short: A. Brunnbauer, L. Berducci, A. Brandstatter, M. Lechner, R. Hasani, D. Rus, R. Grosu, in:, 2022 International Conference on Robotics and Automation, IEEE, 2022, pp. 7513–7520. conference: end_date: 2022-05-27 location: Philadelphia, PA, United States name: 'ICRA: International Conference on Robotics and Automation' start_date: 2022-05-23 date_created: 2022-09-04T22:02:02Z date_published: 2022-07-12T00:00:00Z date_updated: 2022-09-05T08:46:12Z day: '12' department: - _id: ToHe doi: 10.1109/ICRA46639.2022.9811650 ec_funded: 1 external_id: arxiv: - '2103.04909' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2103.04909 month: '07' oa: 1 oa_version: Preprint page: 7513-7520 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: 2022 International Conference on Robotics and Automation publication_identifier: isbn: - '9781728196817' issn: - 1050-4729 publication_status: published publisher: IEEE quality_controlled: '1' scopus_import: '1' status: public title: Latent imagination facilitates zero-shot transfer in autonomous racing type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2022' ... --- _id: '12171' abstract: - lang: eng text: 'We propose an algorithmic approach for synthesizing linear hybrid automata from time-series data. Unlike existing approaches, our approach provides a whole family of models with the same discrete structure but different dynamics. Each model in the family is guaranteed to capture the input data up to a precision error ε, in the following sense: For each time series, the model contains an execution that is ε-close to the data points. Our construction allows to effectively choose a model from this family with minimal precision error ε. We demonstrate the algorithm’s efficiency and its ability to find precise models in two case studies.' acknowledgement: This work was supported in part by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement no. 847635, by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark, and by the Villum Investigator Grant S4OS. alternative_title: - LNCS article_processing_charge: No author: - first_name: Miriam full_name: Garcia Soto, Miriam id: 4B3207F6-F248-11E8-B48F-1D18A9856A87 last_name: Garcia Soto orcid: 0000-0003-2936-5719 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Christian full_name: Schilling, Christian id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87 last_name: Schilling orcid: 0000-0003-3658-1065 citation: ama: 'Garcia Soto M, Henzinger TA, Schilling C. Synthesis of parametric hybrid automata from time series. In: 20th International Symposium on Automated Technology for Verification and Analysis. Vol 13505. Springer Nature; 2022:337-353. doi:10.1007/978-3-031-19992-9_22' apa: 'Garcia Soto, M., Henzinger, T. A., & Schilling, C. (2022). Synthesis of parametric hybrid automata from time series. In 20th International Symposium on Automated Technology for Verification and Analysis (Vol. 13505, pp. 337–353). Virtual: Springer Nature. https://doi.org/10.1007/978-3-031-19992-9_22' chicago: Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis of Parametric Hybrid Automata from Time Series.” In 20th International Symposium on Automated Technology for Verification and Analysis, 13505:337–53. Springer Nature, 2022. https://doi.org/10.1007/978-3-031-19992-9_22. ieee: M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of parametric hybrid automata from time series,” in 20th International Symposium on Automated Technology for Verification and Analysis, Virtual, 2022, vol. 13505, pp. 337–353. ista: 'Garcia Soto M, Henzinger TA, Schilling C. 2022. Synthesis of parametric hybrid automata from time series. 20th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 13505, 337–353.' mla: Garcia Soto, Miriam, et al. “Synthesis of Parametric Hybrid Automata from Time Series.” 20th International Symposium on Automated Technology for Verification and Analysis, vol. 13505, Springer Nature, 2022, pp. 337–53, doi:10.1007/978-3-031-19992-9_22. short: M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, 20th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2022, pp. 337–353. conference: end_date: 2022-10-28 location: Virtual name: 'ATVA: Automated Technology for Verification and Analysis' start_date: 2022-10-25 date_created: 2023-01-12T12:11:16Z date_published: 2022-10-21T00:00:00Z date_updated: 2023-02-13T09:27:55Z day: '21' department: - _id: ToHe doi: 10.1007/978-3-031-19992-9_22 ec_funded: 1 external_id: arxiv: - '2208.06383' intvolume: ' 13505' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2208.06383 month: '10' oa: 1 oa_version: Preprint page: 337-353 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 20th International Symposium on Automated Technology for Verification and Analysis publication_identifier: eisbn: - '9783031199929' eissn: - 1611-3349 isbn: - '9783031199912' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Synthesis of parametric hybrid automata from time series type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13505 year: '2022' ... --- _id: '12508' abstract: - lang: eng text: "We explore the notion of history-determinism in the context of timed automata (TA). History-deterministic automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and history-deterministic specifications allow for game-based verification without an expensive determinization step.\r\nWe show yet another characterisation of history-determinism in terms of fair simulation, at the general level of labelled transition systems: a system is history-deterministic precisely if and only if it fairly simulates all language smaller systems.\r\nFor timed automata over infinite timed words it is known that universality is undecidable for Büchi TA. We show that for history-deterministic TA with arbitrary parity acceptance, timed universality, inclusion, and synthesis all remain decidable and are ExpTime-complete.\r\nFor the subclass of TA with safety or reachability acceptance, we show that checking whether such an automaton is history-deterministic is decidable (in ExpTime), and history-deterministic TA with safety acceptance are effectively determinizable without introducing new automata states." acknowledgement: "Thomas A. Henzinger: This work was supported in part by the ERC-2020-AdG 101020093.\r\nPatrick Totzke: acknowledges support from the EPSRC, project no. EP/V025848/1.\r\n" alternative_title: - LIPIcs article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Karoliina full_name: Lehtinen, Karoliina last_name: Lehtinen - first_name: Patrick full_name: Totzke, Patrick last_name: Totzke citation: ama: 'Henzinger TA, Lehtinen K, Totzke P. History-deterministic timed automata. In: 33rd International Conference on Concurrency Theory. Vol 243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022:14:1-14:21. doi:10.4230/LIPIcs.CONCUR.2022.14' apa: 'Henzinger, T. A., Lehtinen, K., & Totzke, P. (2022). History-deterministic timed automata. In 33rd International Conference on Concurrency Theory (Vol. 243, p. 14:1-14:21). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2022.14' chicago: Henzinger, Thomas A, Karoliina Lehtinen, and Patrick Totzke. “History-Deterministic Timed Automata.” In 33rd International Conference on Concurrency Theory, 243:14:1-14:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.CONCUR.2022.14. ieee: T. A. Henzinger, K. Lehtinen, and P. Totzke, “History-deterministic timed automata,” in 33rd International Conference on Concurrency Theory, Warsaw, Poland, 2022, vol. 243, p. 14:1-14:21. ista: 'Henzinger TA, Lehtinen K, Totzke P. 2022. History-deterministic timed automata. 33rd International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 243, 14:1-14:21.' mla: Henzinger, Thomas A., et al. “History-Deterministic Timed Automata.” 33rd International Conference on Concurrency Theory, vol. 243, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, p. 14:1-14:21, doi:10.4230/LIPIcs.CONCUR.2022.14. short: T.A. Henzinger, K. Lehtinen, P. Totzke, in:, 33rd International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, p. 14:1-14:21. conference: end_date: 2022-09-16 location: Warsaw, Poland name: 'CONCUR: Conference on Concurrency Theory' start_date: 2022-09-13 date_created: 2023-02-05T17:24:23Z date_published: 2022-09-06T00:00:00Z date_updated: 2023-02-06T09:23:31Z day: '06' ddc: - '000' department: - _id: ToHe doi: 10.4230/LIPIcs.CONCUR.2022.14 ec_funded: 1 file: - access_level: open_access checksum: 9e97e15628f66b2ad77f535bb0327dee content_type: application/pdf creator: dernst date_created: 2023-02-06T09:21:09Z date_updated: 2023-02-06T09:21:09Z file_id: '12520' file_name: 2022_LIPICs_Henzinger2.pdf file_size: 717940 relation: main_file success: 1 file_date_updated: 2023-02-06T09:21:09Z has_accepted_license: '1' intvolume: ' 243' language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: 14:1-14:21 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 33rd International Conference on Concurrency Theory publication_identifier: isbn: - '9783959772464' issn: - 1868-8969 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' scopus_import: '1' status: public title: History-deterministic timed automata tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 243 year: '2022' ... --- _id: '12509' abstract: - lang: eng text: A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We summarize how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games. acknowledgement: "Guy Avni: Work partially supported by the Israel Science Foundation, ISF grant agreement\r\nno 1679/21.\r\nThomas A. Henzinger: This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe would like to thank all our collaborators Milad Aghajohari, Ventsislav Chonev, Rasmus Ibsen-Jensen, Ismäel Jecker, Petr Novotný, Josef Tkadlec, and Ðorđe Žikelić; we hope the collaboration was as fun and meaningful for you as it was for us." article_processing_charge: No author: - first_name: Guy full_name: Avni, Guy id: 463C8BC2-F248-11E8-B48F-1D18A9856A87 last_name: Avni orcid: 0000-0001-5588-8287 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Avni G, Henzinger TA. An updated survey of bidding games on graphs. In: 47th International Symposium on Mathematical Foundations of Computer Science. Vol 241. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022:3:1-3:6. doi:10.4230/LIPIcs.MFCS.2022.3' apa: 'Avni, G., & Henzinger, T. A. (2022). An updated survey of bidding games on graphs. In 47th International Symposium on Mathematical Foundations of Computer Science (Vol. 241, p. 3:1-3:6). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2022.3' chicago: 'Avni, Guy, and Thomas A Henzinger. “An Updated Survey of Bidding Games on Graphs.” In 47th International Symposium on Mathematical Foundations of Computer Science, 241:3:1-3:6. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.MFCS.2022.3.' ieee: G. Avni and T. A. Henzinger, “An updated survey of bidding games on graphs,” in 47th International Symposium on Mathematical Foundations of Computer Science, Vienna, Austria, 2022, vol. 241, p. 3:1-3:6. ista: 'Avni G, Henzinger TA. 2022. An updated survey of bidding games on graphs. 47th International Symposium on Mathematical Foundations of Computer Science. MFCS: Symposium on Mathematical Foundations of Computer ScienceLeibniz International Proceedings in Informatics (LIPIcs) vol. 241, 3:1-3:6.' mla: Avni, Guy, and Thomas A. Henzinger. “An Updated Survey of Bidding Games on Graphs.” 47th International Symposium on Mathematical Foundations of Computer Science, vol. 241, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, p. 3:1-3:6, doi:10.4230/LIPIcs.MFCS.2022.3. short: G. Avni, T.A. Henzinger, in:, 47th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2022, p. 3:1-3:6. conference: end_date: 2022-08-26 location: Vienna, Austria name: 'MFCS: Symposium on Mathematical Foundations of Computer Science' start_date: 2022-08-22 date_created: 2023-02-05T17:26:01Z date_published: 2022-08-22T00:00:00Z date_updated: 2023-02-06T09:16:54Z day: '22' ddc: - '000' department: - _id: ToHe doi: 10.4230/LIPIcs.MFCS.2022.3 ec_funded: 1 file: - access_level: open_access checksum: 1888ec9421622f9526fbec2de035f132 content_type: application/pdf creator: dernst date_created: 2023-02-06T09:13:04Z date_updated: 2023-02-06T09:13:04Z file_id: '12519' file_name: 2022_LIPICs_Avni.pdf file_size: 624586 relation: main_file success: 1 file_date_updated: 2023-02-06T09:13:04Z has_accepted_license: '1' intvolume: ' 241' language: - iso: eng month: '08' oa: 1 oa_version: Published Version page: 3:1-3:6 place: Dagstuhl, Germany project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 47th International Symposium on Mathematical Foundations of Computer Science publication_identifier: isbn: - '9783959772563' issn: - 1868-8969 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' scopus_import: '1' series_title: Leibniz International Proceedings in Informatics (LIPIcs) status: public title: An updated survey of bidding games on graphs tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 241 year: '2022' ... --- _id: '11366' abstract: - lang: eng text: "Adversarial training (i.e., training on adversarially perturbed input data) is a well-studied method for making neural networks robust to potential adversarial attacks during inference. However, the improved robustness does not\r\ncome for free but rather is accompanied by a decrease in overall model accuracy and performance. Recent work has shown that, in practical robot learning applications, the effects of adversarial training do not pose a fair trade-off\r\nbut inflict a net loss when measured in holistic robot performance. This work revisits the robustness-accuracy trade-off in robot learning by systematically analyzing if recent advances in robust training methods and theory in\r\nconjunction with adversarial robot learning can make adversarial training suitable for real-world robot applications. We evaluate a wide variety of robot learning tasks ranging from autonomous driving in a high-fidelity environment\r\namenable to sim-to-real deployment, to mobile robot gesture recognition. Our results demonstrate that, while these techniques make incremental improvements on the trade-off on a relative scale, the negative side-effects caused by\r\nadversarial training still outweigh the improvements by an order of magnitude. We conclude that more substantial advances in robust learning methods are necessary before they can benefit robot learning tasks in practice." acknowledgement: "This work was supported in parts by the ERC-2020-AdG 101020093, National Science Foundation (NSF), and JP\r\nMorgan Graduate Fellowships. We thank Christoph Lampert for inspiring this work.\r\n" article_number: '2204.07373' article_processing_charge: No author: - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Alexander full_name: Amini, Alexander last_name: Amini - first_name: Daniela full_name: Rus, Daniela last_name: Rus - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. arXiv. doi:10.48550/arXiv.2204.07373 apa: Lechner, M., Amini, A., Rus, D., & Henzinger, T. A. (n.d.). Revisiting the adversarial robustness-accuracy tradeoff in robot learning. arXiv. https://doi.org/10.48550/arXiv.2204.07373 chicago: Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2204.07373. ieee: M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial robustness-accuracy tradeoff in robot learning,” arXiv. . ista: Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy tradeoff in robot learning. arXiv, 2204.07373. mla: Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” ArXiv, 2204.07373, doi:10.48550/arXiv.2204.07373. short: M. Lechner, A. Amini, D. Rus, T.A. Henzinger, ArXiv (n.d.). date_created: 2022-05-12T13:20:17Z date_published: 2022-04-15T00:00:00Z date_updated: 2023-08-01T13:36:50Z day: '15' department: - _id: ToHe doi: 10.48550/arXiv.2204.07373 ec_funded: 1 external_id: arxiv: - '2204.07373' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2204.07373 month: '04' oa: 1 oa_version: Preprint project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: arXiv publication_status: submitted related_material: record: - id: '11362' relation: dissertation_contains status: public - id: '12704' relation: later_version status: public status: public title: Revisiting the adversarial robustness-accuracy tradeoff in robot learning type: preprint user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2022' ... --- _id: '10891' abstract: - lang: eng text: We present a formal framework for the online black-box monitoring of software using monitors with quantitative verdict functions. Quantitative verdict functions have several advantages. First, quantitative monitors can be approximate, i.e., the value of the verdict function does not need to correspond exactly to the value of the property under observation. Second, quantitative monitors can be quantified universally, i.e., for every possible observed behavior, the monitor tries to make the best effort to estimate the value of the property under observation. Third, quantitative monitors can watch boolean as well as quantitative properties, such as average response time. Fourth, quantitative monitors can use non-finite-state resources, such as counters. As a consequence, quantitative monitors can be compared according to how many resources they use (e.g., the number of counters) and how precisely they approximate the property under observation. This allows for a rich spectrum of cost-precision trade-offs in monitoring software. acknowledgement: The formal framework for quantitative monitoring which is presented in this invited talk was defined jointly with N. Ege Saraç at LICS 2021. This work was supported in part by the Wittgenstein Award Z211-N23 of the Austrian Science Fund. article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Henzinger TA. Quantitative monitoring of software. In: Software Verification. Vol 13124. LNCS. Springer Nature; 2022:3-6. doi:10.1007/978-3-030-95561-8_1' apa: 'Henzinger, T. A. (2022). Quantitative monitoring of software. In Software Verification (Vol. 13124, pp. 3–6). New Haven, CT, United States: Springer Nature. https://doi.org/10.1007/978-3-030-95561-8_1' chicago: Henzinger, Thomas A. “Quantitative Monitoring of Software.” In Software Verification, 13124:3–6. LNCS. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-95561-8_1. ieee: T. A. Henzinger, “Quantitative monitoring of software,” in Software Verification, New Haven, CT, United States, 2022, vol. 13124, pp. 3–6. ista: 'Henzinger TA. 2022. Quantitative monitoring of software. Software Verification. NSV: Numerical Software VerificationLNCS vol. 13124, 3–6.' mla: Henzinger, Thomas A. “Quantitative Monitoring of Software.” Software Verification, vol. 13124, Springer Nature, 2022, pp. 3–6, doi:10.1007/978-3-030-95561-8_1. short: T.A. Henzinger, in:, Software Verification, Springer Nature, 2022, pp. 3–6. conference: end_date: 2021-10-19 location: New Haven, CT, United States name: 'NSV: Numerical Software Verification' start_date: 2021-10-18 date_created: 2022-03-20T23:01:40Z date_published: 2022-02-22T00:00:00Z date_updated: 2023-08-03T06:11:55Z day: '22' department: - _id: ToHe doi: 10.1007/978-3-030-95561-8_1 external_id: isi: - '000771713200001' intvolume: ' 13124' isi: 1 language: - iso: eng month: '02' oa_version: None page: 3-6 project: - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: Software Verification publication_identifier: eissn: - 1611-3349 isbn: - '9783030955601' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' series_title: LNCS status: public title: Quantitative monitoring of software type: conference user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 volume: 13124 year: '2022' ... --- _id: '11355' abstract: - lang: eng text: "Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees.\r\nAlthough there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory that is designed for ensuring system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. We illustrate the applicability of our framework with an example inspired from the automotive domain." acknowledgement: This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 956123 and was funded in part by the FWF project W1255-N23 and by the ERC-2020-AdG 101020093. alternative_title: - LNCS article_processing_charge: No author: - first_name: Ezio full_name: Bartocci, Ezio last_name: Bartocci - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Ana Oliveira full_name: Da Costa, Ana Oliveira last_name: Da Costa citation: ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Information-flow interfaces. In: Fundamental Approaches to Software Engineering. Vol 13241. Springer Nature; 2022:3-22. doi:10.1007/978-3-030-99429-7_1' apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa, A. O. (2022). Information-flow interfaces. In Fundamental Approaches to Software Engineering (Vol. 13241, pp. 3–22). Munich, Germany: Springer Nature. https://doi.org/10.1007/978-3-030-99429-7_1' chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Information-Flow Interfaces.” In Fundamental Approaches to Software Engineering, 13241:3–22. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-99429-7_1. ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Information-flow interfaces,” in Fundamental Approaches to Software Engineering, Munich, Germany, 2022, vol. 13241, pp. 3–22. ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Information-flow interfaces. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13241, 3–22.' mla: Bartocci, Ezio, et al. “Information-Flow Interfaces.” Fundamental Approaches to Software Engineering, vol. 13241, Springer Nature, 2022, pp. 3–22, doi:10.1007/978-3-030-99429-7_1. short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2022, pp. 3–22. conference: end_date: 2022-04-07 location: Munich, Germany name: 'FASE: Fundamental Approaches to Software Engineering' start_date: 2022-04-02 date_created: 2022-05-08T22:01:44Z date_published: 2022-03-29T00:00:00Z date_updated: 2023-08-03T07:03:40Z day: '29' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-030-99429-7_1 ec_funded: 1 external_id: isi: - '000782393600001' file: - access_level: open_access checksum: 7f6f860b20b8de2a249e9c1b4eee15cf content_type: application/pdf creator: dernst date_created: 2022-05-09T06:52:44Z date_updated: 2022-05-09T06:52:44Z file_id: '11357' file_name: 2022_LNCS_Bartocci.pdf file_size: 479146 relation: main_file success: 1 file_date_updated: 2022-05-09T06:52:44Z has_accepted_license: '1' intvolume: ' 13241' isi: 1 language: - iso: eng month: '03' oa: 1 oa_version: Published Version page: 3-22 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: Fundamental Approaches to Software Engineering publication_identifier: eissn: - 1611-3349 isbn: - '9783030994280' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Information-flow interfaces tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 volume: 13241 year: '2022' ... --- _id: '11775' abstract: - lang: eng text: 'Quantitative monitoring can be universal and approximate: For every finite sequence of observations, the specification provides a value and the monitor outputs a best-effort approximation of it. The quality of the approximation may depend on the resources that are available to the monitor. By taking to the limit the sequences of specification values and monitor outputs, we obtain precision-resource trade-offs also for limit monitoring. This paper provides a formal framework for studying such trade-offs using an abstract interpretation for monitors: For each natural number n, the aggregate semantics of a monitor at time n is an equivalence relation over all sequences of at most n observations so that two equivalent sequences are indistinguishable to the monitor and thus mapped to the same output. This abstract interpretation of quantitative monitors allows us to measure the number of equivalence classes (or “resource use”) that is necessary for a certain precision up to a certain time, or at any time. Our framework offers several insights. For example, we identify a family of specifications for which any resource-optimal exact limit monitor is independent of any error permitted over finite traces. Moreover, we present a specification for which any resource-optimal approximate limit monitor does not minimize its resource use at any time. ' acknowledgement: We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093. alternative_title: - LNCS article_processing_charge: Yes author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Nicolas Adrien full_name: Mazzocchi, Nicolas Adrien id: b26baa86-3308-11ec-87b0-8990f34baa85 last_name: Mazzocchi - first_name: Naci E full_name: Sarac, Naci E id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425 last_name: Sarac citation: ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Abstract monitors for quantitative specifications. In: 22nd International Conference on Runtime Verification. Vol 13498. Springer Nature; 2022:200-220. doi:10.1007/978-3-031-17196-3_11' apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2022). Abstract monitors for quantitative specifications. In 22nd International Conference on Runtime Verification (Vol. 13498, pp. 200–220). Tbilisi, Georgia: Springer Nature. https://doi.org/10.1007/978-3-031-17196-3_11' chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Abstract Monitors for Quantitative Specifications.” In 22nd International Conference on Runtime Verification, 13498:200–220. Springer Nature, 2022. https://doi.org/10.1007/978-3-031-17196-3_11. ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Abstract monitors for quantitative specifications,” in 22nd International Conference on Runtime Verification, Tbilisi, Georgia, 2022, vol. 13498, pp. 200–220. ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2022. Abstract monitors for quantitative specifications. 22nd International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 13498, 200–220.' mla: Henzinger, Thomas A., et al. “Abstract Monitors for Quantitative Specifications.” 22nd International Conference on Runtime Verification, vol. 13498, Springer Nature, 2022, pp. 200–20, doi:10.1007/978-3-031-17196-3_11. short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 22nd International Conference on Runtime Verification, Springer Nature, 2022, pp. 200–220. conference: end_date: 2022-09-30 location: Tbilisi, Georgia name: 'RV: Runtime Verification' start_date: 2022-09-28 date_created: 2022-08-08T17:09:09Z date_published: 2022-09-23T00:00:00Z date_updated: 2023-08-03T13:38:46Z day: '23' ddc: - '000' department: - _id: GradSch - _id: ToHe doi: 10.1007/978-3-031-17196-3_11 ec_funded: 1 external_id: isi: - '000866539700011' file: - access_level: open_access checksum: 05c7dcfbb9053a98f46441fb2eccb213 content_type: application/pdf creator: dernst date_created: 2023-01-20T07:34:50Z date_updated: 2023-01-20T07:34:50Z file_id: '12317' file_name: 2022_LNCS_RV_Henzinger.pdf file_size: 477110 relation: main_file success: 1 file_date_updated: 2023-01-20T07:34:50Z has_accepted_license: '1' intvolume: ' 13498' isi: 1 language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: 200-220 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 22nd International Conference on Runtime Verification publication_identifier: issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Abstract monitors for quantitative specifications tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 volume: 13498 year: '2022' ... --- _id: '12147' abstract: - lang: eng text: Continuous-time neural networks are a class of machine learning systems that can tackle representation learning on spatiotemporal decision-making tasks. These models are typically represented by continuous differential equations. However, their expressive power when they are deployed on computers is bottlenecked by numerical differential equation solvers. This limitation has notably slowed down the scaling and understanding of numerous natural physical phenomena such as the dynamics of nervous systems. Ideally, we would circumvent this bottleneck by solving the given dynamical system in closed form. This is known to be intractable in general. Here, we show that it is possible to closely approximate the interaction between neurons and synapses—the building blocks of natural and artificial neural networks—constructed by liquid time-constant networks efficiently in closed form. To this end, we compute a tightly bounded approximation of the solution of an integral appearing in liquid time-constant dynamics that has had no known closed-form solution so far. This closed-form solution impacts the design of continuous-time and continuous-depth neural models. For instance, since time appears explicitly in closed form, the formulation relaxes the need for complex numerical solvers. Consequently, we obtain models that are between one and five orders of magnitude faster in training and inference compared with differential equation-based counterparts. More importantly, in contrast to ordinary differential equation-based continuous networks, closed-form networks can scale remarkably well compared with other deep learning instances. Lastly, as these models are derived from liquid networks, they show good performance in time-series modelling compared with advanced recurrent neural network models. acknowledgement: This research was supported in part by the AI2050 program at Schmidt Futures (grant G-22-63172), the Boeing Company, and the United States Air Force Research Laboratory and the United States Air Force Artificial Intelligence Accelerator and was accomplished under cooperative agreement number FA8750-19-2-1000. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the United States Air Force or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes, notwithstanding any copyright notation herein. This work was further supported by The Boeing Company and Office of Naval Research grant N00014-18-1-2830. M.T. is supported by the Poul Due Jensen Foundation, grant 883901. M.L. was supported in part by the Austrian Science Fund under grant Z211-N23 (Wittgenstein Award). A.A. was supported by the National Science Foundation Graduate Research Fellowship Program. We thank T.-H. Wang, P. Kao, M. Chahine, W. Xiao, X. Li, L. Yin and Y. Ben for useful suggestions and for testing of CfC models to confirm the results across other domains. article_processing_charge: No article_type: original author: - first_name: Ramin full_name: Hasani, Ramin last_name: Hasani - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Alexander full_name: Amini, Alexander last_name: Amini - first_name: Lucas full_name: Liebenwein, Lucas last_name: Liebenwein - first_name: Aaron full_name: Ray, Aaron last_name: Ray - first_name: Max full_name: Tschaikowski, Max last_name: Tschaikowski - first_name: Gerald full_name: Teschl, Gerald last_name: Teschl - first_name: Daniela full_name: Rus, Daniela last_name: Rus citation: ama: Hasani R, Lechner M, Amini A, et al. Closed-form continuous-time neural networks. Nature Machine Intelligence. 2022;4(11):992-1003. doi:10.1038/s42256-022-00556-7 apa: Hasani, R., Lechner, M., Amini, A., Liebenwein, L., Ray, A., Tschaikowski, M., … Rus, D. (2022). Closed-form continuous-time neural networks. Nature Machine Intelligence. Springer Nature. https://doi.org/10.1038/s42256-022-00556-7 chicago: Hasani, Ramin, Mathias Lechner, Alexander Amini, Lucas Liebenwein, Aaron Ray, Max Tschaikowski, Gerald Teschl, and Daniela Rus. “Closed-Form Continuous-Time Neural Networks.” Nature Machine Intelligence. Springer Nature, 2022. https://doi.org/10.1038/s42256-022-00556-7. ieee: R. Hasani et al., “Closed-form continuous-time neural networks,” Nature Machine Intelligence, vol. 4, no. 11. Springer Nature, pp. 992–1003, 2022. ista: Hasani R, Lechner M, Amini A, Liebenwein L, Ray A, Tschaikowski M, Teschl G, Rus D. 2022. Closed-form continuous-time neural networks. Nature Machine Intelligence. 4(11), 992–1003. mla: Hasani, Ramin, et al. “Closed-Form Continuous-Time Neural Networks.” Nature Machine Intelligence, vol. 4, no. 11, Springer Nature, 2022, pp. 992–1003, doi:10.1038/s42256-022-00556-7. short: R. Hasani, M. Lechner, A. Amini, L. Liebenwein, A. Ray, M. Tschaikowski, G. Teschl, D. Rus, Nature Machine Intelligence 4 (2022) 992–1003. date_created: 2023-01-12T12:07:21Z date_published: 2022-11-15T00:00:00Z date_updated: 2023-08-04T09:00:10Z day: '15' ddc: - '000' department: - _id: ToHe doi: 10.1038/s42256-022-00556-7 external_id: arxiv: - '2106.13898' isi: - '000884215600003' file: - access_level: open_access checksum: b4789122ce04bfb4ac042390f59aaa8b content_type: application/pdf creator: dernst date_created: 2023-01-24T09:49:44Z date_updated: 2023-01-24T09:49:44Z file_id: '12355' file_name: 2022_NatureMachineIntelligence_Hasani.pdf file_size: 3259553 relation: main_file success: 1 file_date_updated: 2023-01-24T09:49:44Z has_accepted_license: '1' intvolume: ' 4' isi: 1 issue: '11' keyword: - Artificial Intelligence - Computer Networks and Communications - Computer Vision and Pattern Recognition - Human-Computer Interaction - Software language: - iso: eng month: '11' oa: 1 oa_version: Published Version page: 992-1003 project: - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: Nature Machine Intelligence publication_identifier: issn: - 2522-5839 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: link: - relation: erratum url: https://doi.org/10.1038/s42256-022-00597-y scopus_import: '1' status: public title: Closed-form continuous-time neural networks tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 volume: 4 year: '2022' ...