[{"doi":"10.34727/2023/isbn.978-3-85448-060-0_20","conference":{"location":"Ames, IA, United States","start_date":"2023-10-25","end_date":"2023-10-27","name":"FMCAD: Conference on Formal Methods in Computer-aided design"},"language":[{"iso":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"project":[{"grant_number":"101034413","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"quality_controlled":"1","publication_identifier":{"isbn":["9783854480600"]},"month":"10","author":[{"last_name":"Pastva","first_name":"Samuel","orcid":"0000-0003-1993-0331","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","full_name":"Pastva, Samuel"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"date_created":"2023-12-31T23:01:03Z","date_updated":"2024-01-02T08:16:28Z","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.","year":"2023","department":[{"_id":"ToHe"}],"publisher":"TU Vienna Academic Press","publication_status":"published","ec_funded":1,"file_date_updated":"2024-01-02T08:14:23Z","date_published":"2023-10-01T00:00:00Z","citation":{"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.","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.","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.","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","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.","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","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."},"publication":"Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design","page":"122-131","article_processing_charge":"No","has_accepted_license":"1","day":"01","scopus_import":"1","file":[{"file_id":"14721","relation":"main_file","success":1,"checksum":"818d6e13dd508f3a04f0941081022e5d","date_updated":"2024-01-02T08:14:23Z","date_created":"2024-01-02T08:14:23Z","access_level":"open_access","file_name":"2023_FMCAD_Pastva.pdf","creator":"dernst","file_size":524321,"content_type":"application/pdf"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"14718","status":"public","title":"Binary decision diagrams on modern hardware","ddc":["000"],"abstract":[{"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. ","lang":"eng"}],"type":"conference"},{"related_material":{"record":[{"id":"14600","status":"public","relation":"earlier_version"}]},"author":[{"full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Lechner, Mathias","first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"volume":37,"date_updated":"2024-01-22T14:08:29Z","date_created":"2024-01-18T07:44:31Z","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.","year":"2023","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Association for the Advancement of Artificial Intelligence","publication_status":"published","ec_funded":1,"doi":"10.1609/aaai.v37i10.26407","conference":{"start_date":"2023-02-07","location":"Washington, DC, United States","end_date":"2023-02-14","name":"AAAI: Conference on Artificial Intelligence"},"language":[{"iso":"eng"}],"external_id":{"arxiv":["2210.05308"]},"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"},{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"}],"quality_controlled":"1","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"month":"06","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"14830","intvolume":" 37","status":"public","title":"Learning control policies for stochastic systems with reach-avoid guarantees","issue":"10","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."}],"type":"conference","date_published":"2023-06-26T00:00:00Z","citation":{"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.","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.","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","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","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.","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."},"publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","page":"11926-11935","article_processing_charge":"No","day":"26","keyword":["General Medicine"]},{"doi":"10.1007/s10009-023-00711-4","language":[{"iso":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"external_id":{"arxiv":["2009.06429"],"isi":["001020160000001"]},"project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"isi":1,"quality_controlled":"1","publication_identifier":{"issn":["1433-2779"],"eissn":["1433-2787"]},"month":"08","related_material":{"record":[{"id":"10206","status":"public","relation":"shorter_version"}]},"author":[{"orcid":"0000-0001-8974-2542","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner","first_name":"Konstantin","full_name":"Kueffner, Konstantin"},{"full_name":"Lukina, Anna","last_name":"Lukina","first_name":"Anna","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425"},{"full_name":"Schilling, Christian","last_name":"Schilling","first_name":"Christian","orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"volume":25,"date_updated":"2024-01-30T12:06:57Z","date_created":"2023-07-16T22:01:11Z","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.","year":"2023","publisher":"Springer Nature","department":[{"_id":"ToHe"}],"publication_status":"published","ec_funded":1,"file_date_updated":"2024-01-30T12:06:07Z","date_published":"2023-08-01T00:00:00Z","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","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.","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","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.","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.","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."},"publication":"International Journal on Software Tools for Technology Transfer","page":"575-592","article_type":"original","article_processing_charge":"Yes (in subscription journal)","has_accepted_license":"1","day":"01","scopus_import":"1","file":[{"creator":"dernst","content_type":"application/pdf","file_size":13387667,"file_name":"2023_JourSoftwareTools_Kueffner.pdf","access_level":"open_access","date_updated":"2024-01-30T12:06:07Z","date_created":"2024-01-30T12:06:07Z","success":1,"checksum":"3c4b347f39412a76872f9a6f30101f94","file_id":"14903","relation":"main_file"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13234","intvolume":" 25","ddc":["000"],"title":"Into the unknown: Active monitoring of neural networks (extended version)","status":"public","abstract":[{"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.","lang":"eng"}],"type":"journal_article"},{"article_number":"4","file_date_updated":"2024-02-05T10:19:35Z","ec_funded":1,"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"EPI Sciences","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.","year":"2023","date_created":"2024-01-31T13:40:49Z","date_updated":"2024-02-05T10:21:51Z","volume":2,"author":[{"first_name":"Tamajit","last_name":"Banerjee","full_name":"Banerjee, Tamajit"},{"last_name":"Majumdar","first_name":"Rupak","full_name":"Majumdar, Rupak"},{"full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","first_name":"Kaushik"},{"full_name":"Schmuck, Anne-Kathrin","last_name":"Schmuck","first_name":"Anne-Kathrin"},{"full_name":"Soudjani, Sadegh","last_name":"Soudjani","first_name":"Sadegh"}],"month":"02","publication_identifier":{"issn":["2751-4838"]},"quality_controlled":"1","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"external_id":{"arxiv":["2202.07480"]},"language":[{"iso":"eng"}],"doi":"10.46298/theoretics.23.4","type":"journal_article","abstract":[{"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.","lang":"eng"}],"title":"Fast symbolic algorithms for mega-regular games under strong transition fairness","ddc":["000"],"status":"public","intvolume":" 2","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"14920","oa_version":"Published Version","file":[{"creator":"dernst","content_type":"application/pdf","file_size":917076,"file_name":"2023_TheoretiCS_Banerjee.pdf","access_level":"open_access","date_created":"2024-02-05T10:19:35Z","date_updated":"2024-02-05T10:19:35Z","success":1,"checksum":"2972d531122a6f15727b396110fb3f5c","file_id":"14940","relation":"main_file"}],"day":"24","has_accepted_license":"1","article_processing_charge":"Yes","article_type":"original","publication":"TheoretiCS","citation":{"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.","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).","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.","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.","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","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"},"date_published":"2023-02-24T00:00:00Z"},{"article_processing_charge":"No","has_accepted_license":"1","day":"09","scopus_import":"1","date_published":"2023-09-09T00:00:00Z","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","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.","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.","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","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.","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."},"publication":"21st International Conference on Computational Methods in Systems Biology","page":"18-35","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."}],"type":"conference","alternative_title":["LNBI"],"oa_version":"Submitted Version","file":[{"file_name":"cmsb2023.pdf","access_level":"open_access","file_size":691582,"content_type":"application/pdf","creator":"spastva","relation":"main_file","file_id":"14997","date_updated":"2024-02-16T08:26:32Z","date_created":"2024-02-16T08:26:32Z","checksum":"6f71bdaedb770b52380222fd9f4d7937","success":1}],"_id":"14411","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 14137","ddc":["000"],"title":"Phenotype control of partially specified boolean networks","status":"public","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031426964"],"issn":["0302-9743"]},"month":"09","doi":"10.1007/978-3-031-42697-1_2","conference":{"name":"CMSB: Computational Methods in Systems Biology","location":"Luxembourg City, Luxembourg","start_date":"2023-09-13","end_date":"2023-09-15"},"language":[{"iso":"eng"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"project":[{"name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020","grant_number":"101034413","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"quality_controlled":"1","ec_funded":1,"file_date_updated":"2024-02-16T08:26:32Z","author":[{"last_name":"Beneš","first_name":"Nikola","full_name":"Beneš, Nikola"},{"last_name":"Brim","first_name":"Luboš","full_name":"Brim, Luboš"},{"orcid":"0000-0003-1993-0331","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","last_name":"Pastva","first_name":"Samuel","full_name":"Pastva, Samuel"},{"first_name":"David","last_name":"Šafránek","full_name":"Šafránek, David"},{"full_name":"Šmijáková, Eva","first_name":"Eva","last_name":"Šmijáková"}],"volume":14137,"date_created":"2023-10-08T22:01:18Z","date_updated":"2024-02-20T09:02:04Z","year":"2023","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.","publisher":"Springer Nature","department":[{"_id":"ToHe"}],"publication_status":"published"},{"date_published":"2023-07-16T00:00:00Z","page":"3-15","publication":"35th International Conference on Computer Aided Verification","citation":{"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.","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.","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.","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.","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","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"},"day":"16","has_accepted_license":"1","article_processing_charge":"Yes (in subscription journal)","scopus_import":"1","file":[{"file_id":"14765","relation":"main_file","success":1,"checksum":"1a361d83db0244fd32c03b544c294b5a","date_updated":"2024-01-09T10:01:07Z","date_created":"2024-01-09T10:01:07Z","access_level":"open_access","file_name":"2023_LNCSCAV_Majumdar.pdf","creator":"dernst","file_size":405147,"content_type":"application/pdf"}],"oa_version":"Published Version","title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","status":"public","ddc":["000"],"intvolume":" 13966","_id":"14758","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"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.","lang":"eng"}],"alternative_title":["LNCS"],"type":"conference","language":[{"iso":"eng"}],"conference":{"end_date":"2023-07-22","start_date":"2023-07-17","location":"Paris, France","name":"CAV: Computer Aided Verification"},"doi":"10.1007/978-3-031-37709-9_1","quality_controlled":"1","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"month":"07","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031377082"],"issn":["0302-9743"],"eisbn":["9783031377099"]},"date_updated":"2024-02-27T07:39:51Z","date_created":"2024-01-08T13:18:00Z","volume":13966,"author":[{"first_name":"Rupak","last_name":"Majumdar","full_name":"Majumdar, Rupak"},{"full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","first_name":"Kaushik"},{"first_name":"Mateusz","last_name":"Rychlicki","full_name":"Rychlicki, Mateusz"},{"full_name":"Schmuck, Anne-Kathrin","first_name":"Anne-Kathrin","last_name":"Schmuck"},{"first_name":"Sadegh","last_name":"Soudjani","full_name":"Soudjani, Sadegh"}],"related_material":{"record":[{"relation":"research_data","status":"public","id":"14994"}]},"publication_status":"published","publisher":"Springer Nature","department":[{"_id":"ToHe"}],"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.","year":"2023","file_date_updated":"2024-01-09T10:01:07Z","ec_funded":1},{"month":"04","day":"28","has_accepted_license":"1","article_processing_charge":"No","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.5281/zenodo.7877790"}],"citation":{"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.","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","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.","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","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.","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, (2023).","mla":"Majumdar, Rupak, et al. A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties. Zenodo, 2023, doi:10.5281/ZENODO.7877790."},"oa":1,"doi":"10.5281/ZENODO.7877790","date_published":"2023-04-28T00:00:00Z","type":"research_data_reference","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."}],"status":"public","ddc":["000"],"title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","department":[{"_id":"ToHe"}],"publisher":"Zenodo","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"14994","year":"2023","date_created":"2024-02-14T15:13:00Z","date_updated":"2024-02-27T07:39:51Z","oa_version":"Published Version","author":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","first_name":"Kaushik","last_name":"Mallik","full_name":"Mallik, Kaushik"},{"first_name":"Mateusz","last_name":"Rychlicki","full_name":"Rychlicki, Mateusz"},{"full_name":"Schmuck, Anne-Kathrin","first_name":"Anne-Kathrin","last_name":"Schmuck"},{"full_name":"Soudjani, Sadegh","last_name":"Soudjani","first_name":"Sadegh"}],"related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"14758"}]}},{"date_created":"2024-02-25T09:23:24Z","date_updated":"2024-02-28T12:20:11Z","oa_version":"Preprint","author":[{"full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"id":"a235593c-d7fa-11eb-a0c5-b22ca3c66ee6","first_name":"Abhinav","last_name":"Verma","full_name":"Verma, Abhinav"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger"}],"title":"Compositional policy learning in stochastic control systems with formal guarantees","status":"public","publication_status":"epub_ahead","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"_id":"15023","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS) and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt).","year":"2023","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."}],"ec_funded":1,"type":"conference","language":[{"iso":"eng"}],"conference":{"start_date":"2023-12-10","location":"New Orleans, LO, United States","end_date":"2023-12-16","name":"NeurIPS: Neural Information Processing Systems"},"date_published":"2023-12-15T00:00:00Z","quality_controlled":"1","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"publication":"37th Conference on Neural Information Processing Systems","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2312.01456","open_access":"1"}],"citation":{"short":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th Conference on Neural Information Processing Systems, 2023.","mla":"Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” 37th Conference on Neural Information Processing Systems, 2023.","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.","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.","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.","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.","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."},"external_id":{"arxiv":["2312.01456"]},"oa":1,"day":"15","month":"12","article_processing_charge":"No"},{"publication":"23nd International Conference on Runtime Verification","citation":{"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.","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.","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.","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","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.","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"},"page":"168-190","date_published":"2023-10-01T00:00:00Z","day":"01","article_processing_charge":"Yes (in subscription journal)","has_accepted_license":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"14076","ddc":["000"],"title":"Monitoring hyperproperties with prefix transducers","status":"public","intvolume":" 14245","oa_version":"Published Version","file":[{"checksum":"ee33bd6f1a26f4dae7a8192584869fd8","success":1,"date_created":"2023-10-16T07:15:11Z","date_updated":"2023-10-16T07:15:11Z","relation":"main_file","file_id":"14430","content_type":"application/pdf","file_size":867256,"creator":"dernst","access_level":"open_access","file_name":"2023_LNCS_RV_Chalupa.pdf"}],"type":"conference","alternative_title":["LNCS"],"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."}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"quality_controlled":"1","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"conference":{"name":"RV: Conference on Runtime Verification","end_date":"2023-10-07","location":"Thessaloniki, Greek","start_date":"2023-10-04"},"doi":"10.1007/978-3-031-44267-4_9","language":[{"iso":"eng"}],"month":"10","publication_identifier":{"eisbn":["978-3-031-44267-4"],"isbn":["978-3-031-44266-7"]},"year":"2023","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.","publication_status":"published","publisher":"Springer Nature","department":[{"_id":"ToHe"}],"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","first_name":"Marek","full_name":"Chalupa, Marek"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"id":"15035","relation":"research_data","status":"public"}]},"date_updated":"2024-02-28T12:33:08Z","date_created":"2023-08-16T20:46:08Z","volume":14245,"file_date_updated":"2023-10-16T07:15:11Z","ec_funded":1},{"publisher":"Zenodo","department":[{"_id":"ToHe"}],"status":"public","ddc":["000"],"title":"Monitoring hyperproperties with prefix transducers","year":"2023","_id":"15035","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","date_updated":"2024-02-28T12:33:09Z","date_created":"2024-02-28T07:34:34Z","related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"14076"}]},"author":[{"full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","first_name":"Marek"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"type":"research_data_reference","ec_funded":1,"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."}],"project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"citation":{"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).","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.8191723.","ama":"Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. 2023. doi:10.5281/ZENODO.8191723","ista":"Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers, Zenodo, 10.5281/ZENODO.8191723.","ieee":"M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers.” Zenodo, 2023.","apa":"Chalupa, M., & Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. Zenodo. https://doi.org/10.5281/ZENODO.8191723"},"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"main_file_link":[{"url":"https://doi.org/10.5281/zenodo.8191722","open_access":"1"}],"date_published":"2023-07-28T00:00:00Z","doi":"10.5281/ZENODO.8191723","article_processing_charge":"No","has_accepted_license":"1","day":"28","month":"07"}]