乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T02:30:08Z","timestamp":1726194608532},"publisher-location":"Cham","reference-count":18,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308222"},{"type":"electronic","value":"9783031308239"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"Abstract<\/jats:title>Parity games are two-player zero-sum games of infinite duration played on finite graphs for which no solution in polynomial time is still known. Solving a parity game is an

$$\\text{ NP }\\cap \\text{ co-NP }$$<\/jats:tex-math>\n \n \n NP<\/mml:mtext>\n \n \u2229<\/mml:mo>\n \n co-NP<\/mml:mtext>\n \n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> problem, with the best worst-case complexity algorithms available in the literature running in quasi-polynomial time. Given the importance of parity games within automated formal verification, several practical solutions have been explored showing that considerably large parity games can be solved somewhat efficiently. Here, we propose a new approach to solving parity games guided by the efficient manipulation of a suitable matrix-based representation of the games. Our results show that a sequential implementation of our approach offers very competitive performance, while a parallel implementation using GPUs outperforms the current state-of-the-art techniques. Our study considers both real-world benchmarks of structured games as well as parity games randomly generated. We also show that our matrix-based approach retains the optimal complexity bounds of the best recursive algorithm to solve large parity games in practice.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_34","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T20:19:12Z","timestamp":1682108352000},"page":"666-683","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Matrix-Based Approach to Parity Games"],"prefix":"10.1007","author":[{"given":"Saksham","family":"Aggarwal","sequence":"first","affiliation":[]},{"given":"Alejandro Stuckey","family":"de la Banda","sequence":"additional","affiliation":[]},{"given":"Luke","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Julian","family":"Gutierrez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"34_CR1","unstructured":"Aggarwal, S., Stuckey de la Banda, A., Yang, L., Gutierrez, J.: Parity games benchmarks: Implemenation and experiments. https:\/\/drive.google.com\/drive\/folders\/1z2eAGxU9jyn2ngnhM8c6f4Py4reW3toB?usp=sharing (January 2023)"},{"key":"34_CR2","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"Benerecetti, M., Dell\u2019Erba, D., Mogavero, F.: Solving parity games via priority promotion. Formal Methods Syst. Des. 52(2), 193\u2013226 (2018)","DOI":"10.1007\/s10703-018-0315-1"},{"key":"34_CR4","doi-asserted-by":"crossref","unstructured":"Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasi-polynomial time. SIAM J. Comput. 51(2), 17\u2013152 (2022)","DOI":"10.1137\/17M1145288"},{"key":"34_CR5","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model checking, 2nd Edition. MIT Press (2018)"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"D\u2019Amore, L., Murano, A., Sorrentino, L., Arcucci, R., Laccetti, G.: Toward a multilevel scalable parallel zielonka\u2019s algorithm for solving parity games. Concurr. Comput. Pract. Exp. 33(4) (2021)","DOI":"10.1002\/cpe.6043"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"van Dijk, T.: Oink: An implementation and evaluation of modern parity game solvers. In: Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018. LNCS, vol. 10805, pp. 291\u2013308. Springer (2018)","DOI":"10.1007\/978-3-319-89960-2_16"},{"key":"34_CR8","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: 32nd Annual Symposium on Foundations of Computer Science. pp. 368\u2013377. IEEE (1991)"},{"key":"34_CR9","doi-asserted-by":"crossref","unstructured":"Friedmann, O., Lange, M.: Solving parity games in practice. In: Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009. LNCS, vol.\u00a05799, pp. 182\u2013196. Springer (2009)","DOI":"10.1007\/978-3-642-04761-9_15"},{"key":"34_CR10","doi-asserted-by":"crossref","unstructured":"Hoffmann, P., Luttenberger, M.: Solving parity games on the GPU. In: Hung, D.V., Ogawa, M. (eds.) Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08172, pp. 455\u2013459. Springer (2013)","DOI":"10.1007\/978-3-319-02444-8_34"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"Jurdzinski, M.: Deciding the winner in parity games is in UP $$\\cap $$ co-UP. Inf. Process. Lett. 68(3), 119\u2013124 (1998)","DOI":"10.1016\/S0020-0190(98)00150-1"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Keiren, J.J.A.: Benchmarks for parity games. In: Dastani, M., Sirjani, M. (eds.) Fundamentals of Software Engineering. pp. 127\u2013142. Springer (2015)","DOI":"10.1007\/978-3-319-24644-4_9"},{"key":"34_CR13","doi-asserted-by":"crossref","unstructured":"Lehtinen, K., Parys, P., Schewe, S., Wojtczak, D.: A recursive approach to solving parity games in quasipolynomial time. Log. Methods Comput. Sci. 18(1) (2022)","DOI":"10.46298\/lmcs-18(1:8)2022"},{"key":"34_CR14","doi-asserted-by":"crossref","unstructured":"Martin, D.: Borel determinacy. Annals of Mathematics 102(2), 363\u2013371 (1975)","DOI":"10.2307\/1971035"},{"key":"34_CR15","doi-asserted-by":"crossref","unstructured":"Nickolls, J., Buck, I., Garland, M., Skadron, K.: Scalable parallel programming with cuda: Is cuda the parallel programming model that application developers have been waiting for? Queue 6(2), 40\u201353 (2008)","DOI":"10.1145\/1365490.1365500"},{"key":"34_CR16","unstructured":"Parys, P.: Parity Games: Another View on Lehtinen\u2019s Algorithm. In: Fern\u00e1ndez, M., Muscholl, A. (eds.) 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0152, pp. 32:1\u201332:15. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2020)"},{"key":"34_CR17","doi-asserted-by":"crossref","unstructured":"Stasio, A.D., Murano, A., Prignano, V., Sorrentino, L.: Solving parity games in scala. In: Lanese, I., Madelaine, E. (eds.) Formal Aspects of Component Software - 11th International Symposium, FACS 2014. LNCS, vol.\u00a08997, pp. 145\u2013161. Springer (2014)","DOI":"10.1007\/978-3-319-15317-9_9"},{"key":"34_CR18","doi-asserted-by":"crossref","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1-2), 135\u2013183 (1998)","DOI":"10.1016\/S0304-3975(98)00009-7"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,4]],"date-time":"2023-08-04T10:07:13Z","timestamp":1691143633000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}