[{"article_processing_charge":"No","has_accepted_license":"1","day":"20","citation":{"chicago":"Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” In Tools and Algorithms for the Construction and Analysis of Systems, 13994:535–40. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_32.","short":"M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 535–540.","mla":"Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” Tools and Algorithms for the Construction and Analysis of Systems, vol. 13994, Springer Nature, 2023, pp. 535–40, doi:10.1007/978-3-031-30820-8_32.","apa":"Chalupa, M., & Henzinger, T. A. (2023). Bubaak: Runtime monitoring of program verifiers. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_32","ieee":"M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,” in Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994, pp. 535–540.","ista":"Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 535–540.","ama":"Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers. In: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13994. Springer Nature; 2023:535-540. doi:10.1007/978-3-031-30820-8_32"},"publication":"Tools and Algorithms for the Construction and Analysis of Systems","page":"535-540","date_published":"2023-04-20T00:00:00Z","type":"conference","alternative_title":["LNCS"],"abstract":[{"text":"The main idea behind BUBAAK is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis.\r\nAt SV-COMP 2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why BUBAAK only ran several analyses in parallel, without any coordination. Still, BUBAAK won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition.","lang":"eng"}],"_id":"12854","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 13994","ddc":["000"],"status":"public","title":"Bubaak: Runtime monitoring of program verifiers","oa_version":"Published Version","file":[{"file_name":"2023_LNCS_Chalupa.pdf","access_level":"open_access","content_type":"application/pdf","file_size":16096413,"creator":"dernst","relation":"main_file","file_id":"12864","date_updated":"2023-04-25T06:58:36Z","date_created":"2023-04-25T06:58:36Z","checksum":"120d2c2a38384058ad0630fdf8288312","success":1}],"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031308192"],"issn":["0302-9743"],"eisbn":["9783031308208"]},"month":"04","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":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"quality_controlled":"1","doi":"10.1007/978-3-031-30820-8_32","conference":{"location":"Paris, France","start_date":"2023-04-22","end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"language":[{"iso":"eng"}],"ec_funded":1,"file_date_updated":"2023-04-25T06:58:36Z","license":"https://creativecommons.org/licenses/by/4.0/","acknowledgement":"This work was supported by the ERC-2020-AdG 10102009 grant.","year":"2023","publisher":"Springer Nature","department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger"}],"volume":13994,"date_created":"2023-04-20T08:22:53Z","date_updated":"2023-04-25T07:02:43Z"},{"file_date_updated":"2023-04-25T07:16:36Z","ec_funded":1,"publication_status":"published","publisher":"Springer Nature","department":[{"_id":"ToHe"}],"year":"2023","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank the anonymous FASE reviewers for their valuable feedback and suggestions.","date_updated":"2023-04-25T07:19:07Z","date_created":"2023-04-20T08:29:42Z","volume":13991,"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","first_name":"Marek","full_name":"Chalupa, Marek"},{"first_name":"Fabian","last_name":"Mühlböck","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian"},{"full_name":"Muroya Lei, Stefanie","first_name":"Stefanie","last_name":"Muroya Lei","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger"}],"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"12407"}]},"month":"04","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783031308260"],"isbn":["9783031308253"],"eissn":["1611-3349"]},"quality_controlled":"1","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","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"},"language":[{"iso":"eng"}],"conference":{"name":"FASE: Fundamental Approaches to Software Engineering","end_date":"2023-04-27","start_date":"2023-04-22","location":"Paris, France"},"doi":"10.1007/978-3-031-30826-0_15","alternative_title":["LNCS"],"type":"conference","abstract":[{"text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch.","lang":"eng"}],"title":"Vamos: Middleware for best-effort third-party monitoring","ddc":["000"],"status":"public","intvolume":" 13991","_id":"12856","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"checksum":"17a7c8e08be609cf2408d37ea55e322c","success":1,"date_created":"2023-04-25T07:16:36Z","date_updated":"2023-04-25T07:16:36Z","relation":"main_file","file_id":"12865","content_type":"application/pdf","file_size":580828,"creator":"dernst","access_level":"open_access","file_name":"2023_LNCS_ChalupaM.pdf"}],"oa_version":"Published Version","day":"20","has_accepted_license":"1","article_processing_charge":"No","page":"260-281","publication":"Fundamental Approaches to Software Engineering","citation":{"mla":"Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” Fundamental Approaches to Software Engineering, vol. 13991, Springer Nature, 2023, pp. 260–81, doi:10.1007/978-3-031-30826-0_15.","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2023, pp. 260–281.","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” In Fundamental Approaches to Software Engineering, 13991:260–81. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30826-0_15.","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort third-party monitoring. In: Fundamental Approaches to Software Engineering. Vol 13991. Springer Nature; 2023:260-281. doi:10.1007/978-3-031-30826-0_15","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. Vamos: Middleware for best-effort third-party monitoring. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13991, 260–281.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023). Vamos: Middleware for best-effort third-party monitoring. In Fundamental Approaches to Software Engineering (Vol. 13991, pp. 260–281). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30826-0_15","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware for best-effort third-party monitoring,” in Fundamental Approaches to Software Engineering, Paris, France, 2023, vol. 13991, pp. 260–281."},"date_published":"2023-04-20T00:00:00Z"},{"project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"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,"language":[{"iso":"eng"}],"doi":"10.15479/AT:ISTA:12407","month":"01","publication_identifier":{"eissn":["2664-1690"]},"publication_status":"published","publisher":"Institute of Science and Technology Austria","department":[{"_id":"ToHe"}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. \r\nThe authors would like to thank the anonymous FASE reviewers for their valuable feedback and suggestions.","year":"2023","date_created":"2023-01-27T03:18:08Z","date_updated":"2023-04-25T07:19:06Z","author":[{"full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","last_name":"Chalupa"},{"first_name":"Fabian","last_name":"Mühlböck","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian"},{"first_name":"Stefanie","last_name":"Muroya Lei","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","full_name":"Muroya Lei, Stefanie"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"related_material":{"record":[{"status":"public","relation":"later_version","id":"12856"}]},"file_date_updated":"2023-01-27T03:18:34Z","ec_funded":1,"page":"38","citation":{"chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria, 2023. https://doi.org/10.15479/AT:ISTA:12407.","mla":"Chalupa, Marek, et al. VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria, 2023, doi:10.15479/AT:ISTA:12407.","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, VAMOS: Middleware for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria, 2023.","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. VAMOS: Middleware for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria, 38p.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023). VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:12407","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria, 2023.","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria; 2023. doi:10.15479/AT:ISTA:12407"},"date_published":"2023-01-27T00:00:00Z","keyword":["runtime monitoring","best effort","third party"],"day":"27","has_accepted_license":"1","article_processing_charge":"No","status":"public","title":"VAMOS: Middleware for Best-Effort Third-Party Monitoring","ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"12407","file":[{"creator":"fmuehlbo","file_size":662409,"content_type":"application/pdf","access_level":"open_access","file_name":"main.pdf","success":1,"checksum":"55426e463fdeafe9777fc3ff635154c7","date_updated":"2023-01-27T03:18:34Z","date_created":"2023-01-27T03:18:34Z","file_id":"12408","relation":"main_file"}],"oa_version":"Published Version","alternative_title":["IST Austria Technical Report"],"type":"technical_report","abstract":[{"lang":"eng","text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\n\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch."}]},{"alternative_title":["LNCS"],"type":"conference","abstract":[{"text":"Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.","lang":"eng"}],"intvolume":" 13993","ddc":["000"],"status":"public","title":"A learner-verifier framework for neural network controllers and certificates of stochastic systems","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13142","file":[{"relation":"main_file","file_id":"13150","date_created":"2023-06-19T08:29:30Z","date_updated":"2023-06-19T08:29:30Z","checksum":"3d8a8bb24d211bc83360dfc2fd744307","success":1,"file_name":"2023_LNCS_Chatterjee.pdf","access_level":"open_access","content_type":"application/pdf","file_size":528455,"creator":"dernst"}],"oa_version":"Published Version","scopus_import":"1","has_accepted_license":"1","article_processing_charge":"No","day":"22","page":"3-25","citation":{"ista":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier framework for neural network controllers and certificates of stochastic systems. Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 3–25.","ieee":"K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “A learner-verifier framework for neural network controllers and certificates of stochastic systems,” in Tools and Algorithms for the Construction and Analysis of Systems , Paris, France, 2023, vol. 13993, pp. 3–25.","apa":"Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic, D. (2023). A learner-verifier framework for neural network controllers and certificates of stochastic systems. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_1","ama":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: Tools and Algorithms for the Construction and Analysis of Systems . Vol 13993. Springer Nature; 2023:3-25. doi:10.1007/978-3-031-30823-9_1","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Mathias Lechner, and Dorde Zikelic. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” In Tools and Algorithms for the Construction and Analysis of Systems , 13993:3–25. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_1.","mla":"Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” Tools and Algorithms for the Construction and Analysis of Systems , vol. 13993, Springer Nature, 2023, pp. 3–25, doi:10.1007/978-3-031-30823-9_1.","short":"K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2023, pp. 3–25."},"publication":"Tools and Algorithms for the Construction and Analysis of Systems ","date_published":"2023-04-22T00:00:00Z","ec_funded":1,"file_date_updated":"2023-06-19T08:29:30Z","publisher":"Springer Nature","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","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","volume":13993,"date_created":"2023-06-18T22:00:47Z","date_updated":"2023-06-19T08:30:54Z","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias"},{"full_name":"Zikelic, Dorde","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308222"]},"month":"04","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"}],"quality_controlled":"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"},"oa":1,"language":[{"iso":"eng"}],"doi":"10.1007/978-3-031-30823-9_1","conference":{"location":"Paris, France","start_date":"2023-04-22","end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"}},{"file_date_updated":"2023-06-19T08:43:21Z","publisher":"Springer Nature","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2023","volume":13994,"date_created":"2023-06-18T22:00:47Z","date_updated":"2023-06-19T08:49:46Z","author":[{"full_name":"Anand, Ashwani","first_name":"Ashwani","last_name":"Anand"},{"full_name":"Mallik, Kaushik","last_name":"Mallik","first_name":"Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"first_name":"Satya Prakash","last_name":"Nayak","full_name":"Nayak, Satya Prakash"},{"first_name":"Anne Kathrin","last_name":"Schmuck","full_name":"Schmuck, Anne Kathrin"}],"publication_identifier":{"isbn":["9783031308192"],"eissn":["1611-3349"],"issn":["0302-9743"]},"month":"04","quality_controlled":"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"},"oa":1,"language":[{"iso":"eng"}],"doi":"10.1007/978-3-031-30820-8_15","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2023-04-27","start_date":"2023-04-22","location":"Paris, France"},"alternative_title":["LNCS"],"type":"conference","abstract":[{"text":"We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an ω-regular winning condition Φ for the system player, we compute an ω-regular assumption Ψ for the environment player, such that (i) every environment strategy compliant with Ψ allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ψ does not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games, which are canonical representations of ω-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches—both theoretically and empirically. To the best of our knowledge, for ω\r\n-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.","lang":"eng"}],"intvolume":" 13994","status":"public","ddc":["000"],"title":"Computing adequately permissive assumptions for synthesis","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13141","oa_version":"Published Version","file":[{"relation":"main_file","file_id":"13151","checksum":"60dcafc1b4f6f070be43bad3fe877974","success":1,"date_created":"2023-06-19T08:43:21Z","date_updated":"2023-06-19T08:43:21Z","access_level":"open_access","file_name":"2023_LNCS_Anand.pdf","file_size":521425,"content_type":"application/pdf","creator":"dernst"}],"scopus_import":"1","article_processing_charge":"No","has_accepted_license":"1","day":"20","page":"211-228","citation":{"short":"A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 211–228.","mla":"Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.” TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, vol. 13994, Springer Nature, 2023, pp. 211–28, doi:10.1007/978-3-031-30820-8_15.","chicago":"Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, 13994:211–28. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_15.","ama":"Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions for synthesis. In: TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13994. Springer Nature; 2023:211-228. doi:10.1007/978-3-031-30820-8_15","apa":"Anand, A., Mallik, K., Nayak, S. P., & Schmuck, A. K. (2023). Computing adequately permissive assumptions for synthesis. In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13994, pp. 211–228). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_15","ieee":"A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately permissive assumptions for synthesis,” in TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994, pp. 211–228.","ista":"Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 211–228."},"publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","date_published":"2023-04-20T00:00:00Z"}]