[{"editor":[{"last_name":"Frehse","first_name":"Goran","full_name":"Frehse, Goran"},{"first_name":"Matthias","last_name":"Althoff","full_name":"Althoff, Matthias"}],"publisher":"EasyChair","file_date_updated":"2022-05-17T06:55:49Z","quality_controlled":"1","page":"1-13","intvolume":"        61","alternative_title":["EPiC Series in Computing"],"title":"ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics","date_created":"2022-03-18T12:29:23Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"last_name":"Frehse","first_name":"Goran","full_name":"Frehse, Goran"},{"full_name":"Abate, Alessandro","last_name":"Abate","first_name":"Alessandro"},{"last_name":"Adzkiya","first_name":"Dieky","full_name":"Adzkiya, Dieky"},{"full_name":"Becchi, Anna","first_name":"Anna","last_name":"Becchi"},{"first_name":"Lei","last_name":"Bu","full_name":"Bu, Lei"},{"last_name":"Cimatti","first_name":"Alessandro","full_name":"Cimatti, Alessandro"},{"orcid":"0000-0001-8180-0904","full_name":"Giacobbe, Mirco","first_name":"Mirco","last_name":"Giacobbe","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Griggio","first_name":"Alberto","full_name":"Griggio, Alberto"},{"full_name":"Mover, Sergio","first_name":"Sergio","last_name":"Mover"},{"full_name":"Mufid, Muhammad Syifa'ul","last_name":"Mufid","first_name":"Muhammad Syifa'ul"},{"last_name":"Riouak","first_name":"Idriss","full_name":"Riouak, Idriss"},{"last_name":"Tonetta","first_name":"Stefano","full_name":"Tonetta, Stefano"},{"full_name":"Zaffanella, Enea","last_name":"Zaffanella","first_name":"Enea"}],"scopus_import":"1","_id":"10877","ddc":["000"],"acknowledgement":"The authors gratefully acknowledge \fnancial support by the European Commission project\r\nUnCoVerCPS under grant number 643921. Lei Bu is supported by the National Natural Science\r\nFoundation of China (No.61572249).","volume":61,"abstract":[{"text":"This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In this third edition, six tools have been applied to solve five different benchmark problems in the category for piecewise constant dynamics: BACH, Lyse, Hy- COMP, PHAVer/SX, PHAVerLite, and VeriSiMPL. Compared to last year, a new tool has participated (HyCOMP) and PHAVerLite has replaced PHAVer-lite. The result is a snap- shot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.","lang":"eng"}],"day":"25","doi":"10.29007/rjwn","year":"2019","citation":{"short":"G. Frehse, A. Abate, D. Adzkiya, A. Becchi, L. Bu, A. Cimatti, M. Giacobbe, A. Griggio, S. Mover, M.S. Mufid, I. Riouak, S. Tonetta, E. Zaffanella, in:, G. Frehse, M. Althoff (Eds.), ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, EasyChair, 2019, pp. 1–13.","mla":"Frehse, Goran, et al. “ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.” <i>ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems</i>, edited by Goran Frehse and Matthias Althoff, vol. 61, EasyChair, 2019, pp. 1–13, doi:<a href=\"https://doi.org/10.29007/rjwn\">10.29007/rjwn</a>.","ista":"Frehse G, Abate A, Adzkiya D, Becchi A, Bu L, Cimatti A, Giacobbe M, Griggio A, Mover S, Mufid MS, Riouak I, Tonetta S, Zaffanella E. 2019. ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics. ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems, EPiC Series in Computing, vol. 61, 1–13.","ama":"Frehse G, Abate A, Adzkiya D, et al. ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics. In: Frehse G, Althoff M, eds. <i>ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems</i>. Vol 61. EasyChair; 2019:1-13. doi:<a href=\"https://doi.org/10.29007/rjwn\">10.29007/rjwn</a>","apa":"Frehse, G., Abate, A., Adzkiya, D., Becchi, A., Bu, L., Cimatti, A., … Zaffanella, E. (2019). ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics. In G. Frehse &#38; M. Althoff (Eds.), <i>ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems</i> (Vol. 61, pp. 1–13). Montreal, Canada: EasyChair. <a href=\"https://doi.org/10.29007/rjwn\">https://doi.org/10.29007/rjwn</a>","ieee":"G. Frehse <i>et al.</i>, “ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics,” in <i>ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems</i>, Montreal, Canada, 2019, vol. 61, pp. 1–13.","chicago":"Frehse, Goran, Alessandro Abate, Dieky Adzkiya, Anna Becchi, Lei Bu, Alessandro Cimatti, Mirco Giacobbe, et al. “ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.” In <i>ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems</i>, edited by Goran Frehse and Matthias Althoff, 61:1–13. EasyChair, 2019. <a href=\"https://doi.org/10.29007/rjwn\">https://doi.org/10.29007/rjwn</a>."},"date_updated":"2022-05-17T07:09:47Z","conference":{"start_date":"2019-04-15","name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems","end_date":"2019-04-15","location":"Montreal, Canada"},"language":[{"iso":"eng"}],"month":"05","oa_version":"Published Version","has_accepted_license":"1","publication":"ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"file_id":"11391","creator":"dernst","access_level":"open_access","success":1,"relation":"main_file","date_updated":"2022-05-17T06:55:49Z","content_type":"application/pdf","file_name":"2019_EPiCs_Frehse.pdf","date_created":"2022-05-17T06:55:49Z","file_size":346415,"checksum":"4b92e333db7b4e2349501a804dfede69"}],"oa":1,"publication_identifier":{"issn":["2398-7340"]},"type":"conference","date_published":"2019-05-25T00:00:00Z"},{"department":[{"_id":"KrCh"}],"date_created":"2022-03-18T12:46:32Z","article_processing_charge":"No","publication_status":"published","intvolume":"        57","alternative_title":["EPiC Series in Computing"],"title":"Quasipolynomial set-based symbolic algorithms for parity games","scopus_import":"1","_id":"10883","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Dvořák","first_name":"Wolfgang","full_name":"Dvořák, Wolfgang"},{"orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"first_name":"Alexander","last_name":"Svozil","full_name":"Svozil, Alexander"}],"publisher":"EasyChair","ec_funded":1,"quality_controlled":"1","page":"233-253","file_date_updated":"2022-05-17T07:51:08Z","day":"23","doi":"10.29007/5z5k","arxiv":1,"abstract":[{"text":"Solving parity games, which are equivalent to modal μ-calculus model checking, is a central algorithmic problem in formal methods, with applications in reactive synthesis, program repair, verification of branching-time properties, etc. Besides the standard compu- tation model with the explicit representation of games, another important theoretical model of computation is that of set-based symbolic algorithms. Set-based symbolic algorithms use basic set operations and one-step predecessor operations on the implicit description of games, rather than the explicit representation. The significance of symbolic algorithms is that they provide scalable algorithms for large finite-state systems, as well as for infinite-state systems with finite quotient. Consider parity games on graphs with n vertices and parity conditions with d priorities. While there is a rich literature of explicit algorithms for parity games, the main results for set-based symbolic algorithms are as follows: (a) the basic algorithm that requires O(nd) symbolic operations and O(d) symbolic space; and (b) an improved algorithm that requires O(nd/3+1) symbolic operations and O(n) symbolic space. In this work, our contributions are as follows: (1) We present a black-box set-based symbolic algorithm based on the explicit progress measure algorithm. Two important consequences of our algorithm are as follows: (a) a set-based symbolic algorithm for parity games that requires quasi-polynomially many symbolic operations and O(n) symbolic space; and (b) any future improvement in progress measure based explicit algorithms immediately imply an efficiency improvement in our set-based symbolic algorithm for parity games. (2) We present a set-based symbolic algorithm that requires quasi-polynomially many symbolic operations and O(d · log n) symbolic space. Moreover, for the important special case of d ≤ log n, our algorithm requires only polynomially many symbolic operations and poly-logarithmic symbolic space.","lang":"eng"}],"year":"2018","citation":{"ista":"Chatterjee K, Dvořák W, Henzinger MH, Svozil A. 2018. Quasipolynomial set-based symbolic algorithms for parity games. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. LPAR: Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC Series in Computing, vol. 57, 233–253.","short":"K. Chatterjee, W. Dvořák, M.H. Henzinger, A. Svozil, in:, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair, 2018, pp. 233–253.","mla":"Chatterjee, Krishnendu, et al. “Quasipolynomial Set-Based Symbolic Algorithms for Parity Games.” <i>22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i>, vol. 57, EasyChair, 2018, pp. 233–53, doi:<a href=\"https://doi.org/10.29007/5z5k\">10.29007/5z5k</a>.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvořák, Monika H Henzinger, and Alexander Svozil. “Quasipolynomial Set-Based Symbolic Algorithms for Parity Games.” In <i>22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i>, 57:233–53. EasyChair, 2018. <a href=\"https://doi.org/10.29007/5z5k\">https://doi.org/10.29007/5z5k</a>.","ieee":"K. Chatterjee, W. Dvořák, M. H. Henzinger, and A. Svozil, “Quasipolynomial set-based symbolic algorithms for parity games,” in <i>22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i>, Awassa, Ethiopia, 2018, vol. 57, pp. 233–253.","apa":"Chatterjee, K., Dvořák, W., Henzinger, M. H., &#38; Svozil, A. (2018). Quasipolynomial set-based symbolic algorithms for parity games. In <i>22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i> (Vol. 57, pp. 233–253). Awassa, Ethiopia: EasyChair. <a href=\"https://doi.org/10.29007/5z5k\">https://doi.org/10.29007/5z5k</a>","ama":"Chatterjee K, Dvořák W, Henzinger MH, Svozil A. Quasipolynomial set-based symbolic algorithms for parity games. In: <i>22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i>. Vol 57. EasyChair; 2018:233-253. doi:<a href=\"https://doi.org/10.29007/5z5k\">10.29007/5z5k</a>"},"date_updated":"2022-07-29T09:24:31Z","external_id":{"arxiv":["1909.04983"]},"volume":57,"acknowledgement":"A. S. is fully supported by the Vienna Science and Technology Fund (WWTF) through project ICT15-003. K.C. is supported by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC Starting grant (279307: Graph Games). For M.H the research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013) /ERC Grant Agreement no. 340506.","ddc":["000"],"project":[{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"oa_version":"Published Version","month":"10","has_accepted_license":"1","publication":"22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning","conference":{"location":"Awassa, Ethiopia","end_date":"2018-11-21","start_date":"2018-11-17","name":"LPAR: Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["2398-7340"]},"oa":1,"type":"conference","date_published":"2018-10-23T00:00:00Z","file":[{"date_updated":"2022-05-17T07:51:08Z","file_name":"2018_EPiCs_Chatterjee.pdf","content_type":"application/pdf","date_created":"2022-05-17T07:51:08Z","file_size":720893,"checksum":"1229aa8640bd6db610c85decf2265480","file_id":"11392","creator":"dernst","access_level":"open_access","relation":"main_file","success":1}],"user_id":"72615eeb-f1f3-11ec-aa25-d4573ddc34fd","status":"public"}]