[{"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)"},"alternative_title":["LNCS"],"ddc":["000"],"year":"2023","doi":"10.1007/978-3-031-30820-8_15","title":"Computing adequately permissive assumptions for synthesis","article_processing_charge":"No","date_updated":"2023-06-19T08:49:46Z","volume":13994,"oa":1,"oa_version":"Published Version","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031308192"],"issn":["0302-9743"]},"_id":"13141","citation":{"chicago":"Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, 13994:211–28. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">https://doi.org/10.1007/978-3-031-30820-8_15</a>.","apa":"Anand, A., Mallik, K., Nayak, S. P., &#38; Schmuck, A. K. (2023). Computing adequately permissive assumptions for synthesis. In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13994, pp. 211–228). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">https://doi.org/10.1007/978-3-031-30820-8_15</a>","ieee":"A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately permissive assumptions for synthesis,” in <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, 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.","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.","ama":"Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions for synthesis. In: <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13994. Springer Nature; 2023:211-228. doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">10.1007/978-3-031-30820-8_15</a>","mla":"Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.” <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13994, Springer Nature, 2023, pp. 211–28, doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">10.1007/978-3-031-30820-8_15</a>."},"publication_status":"published","author":[{"first_name":"Ashwani","last_name":"Anand","full_name":"Anand, Ashwani"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","last_name":"Mallik"},{"first_name":"Satya Prakash","last_name":"Nayak","full_name":"Nayak, Satya Prakash"},{"last_name":"Schmuck","full_name":"Schmuck, Anne Kathrin","first_name":"Anne Kathrin"}],"abstract":[{"lang":"eng","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."}],"department":[{"_id":"ToHe"}],"has_accepted_license":"1","date_created":"2023-06-18T22:00:47Z","file":[{"creator":"dernst","file_id":"13151","content_type":"application/pdf","relation":"main_file","success":1,"date_updated":"2023-06-19T08:43:21Z","access_level":"open_access","date_created":"2023-06-19T08:43:21Z","checksum":"60dcafc1b4f6f070be43bad3fe877974","file_name":"2023_LNCS_Anand.pdf","file_size":521425}],"conference":{"end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Paris, France","start_date":"2023-04-22"},"date_published":"2023-04-20T00:00:00Z","month":"04","language":[{"iso":"eng"}],"scopus_import":"1","publisher":"Springer Nature","file_date_updated":"2023-06-19T08:43:21Z","page":"211-228","publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","type":"conference","day":"20","status":"public","intvolume":"     13994"},{"publisher":"Springer Nature","language":[{"iso":"eng"}],"month":"04","date_published":"2023-04-20T00:00:00Z","conference":{"end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Paris, France","start_date":"2023-04-22"},"file":[{"file_id":"12864","creator":"dernst","content_type":"application/pdf","relation":"main_file","success":1,"date_updated":"2023-04-25T06:58:36Z","access_level":"open_access","date_created":"2023-04-25T06:58:36Z","checksum":"120d2c2a38384058ad0630fdf8288312","file_name":"2023_LNCS_Chalupa.pdf","file_size":16096413}],"date_created":"2023-04-20T08:22:53Z","has_accepted_license":"1","department":[{"_id":"ToHe"}],"intvolume":"     13994","status":"public","day":"20","type":"conference","publication":"Tools and Algorithms for the Construction and Analysis of Systems","file_date_updated":"2023-04-25T06:58:36Z","page":"535-540","title":"Bubaak: Runtime monitoring of program verifiers","doi":"10.1007/978-3-031-30820-8_32","year":"2023","ec_funded":1,"ddc":["000"],"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)"},"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"}],"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","full_name":"Chalupa, Marek","first_name":"Marek"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"}],"citation":{"mla":"Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13994, Springer Nature, 2023, pp. 535–40, doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">10.1007/978-3-031-30820-8_32</a>.","ama":"Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers. In: <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13994. Springer Nature; 2023:535-540. doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">10.1007/978-3-031-30820-8_32</a>","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.","short":"M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 535–540.","ieee":"M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Paris, France, 2023, vol. 13994, pp. 535–540.","apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Bubaak: Runtime monitoring of program verifiers. In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">https://doi.org/10.1007/978-3-031-30820-8_32</a>","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 13994:535–40. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">https://doi.org/10.1007/978-3-031-30820-8_32</a>."},"publication_status":"published","publication_identifier":{"eisbn":["9783031308208"],"isbn":["9783031308192"],"issn":["0302-9743"],"eissn":["1611-3349"]},"_id":"12854","oa_version":"Published Version","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","acknowledgement":"This work was supported by the ERC-2020-AdG 10102009 grant.","article_processing_charge":"No","volume":13994,"date_updated":"2023-04-25T07:02:43Z","oa":1}]