Attracting tangles to solve parity games

Tom van Dijk*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

15 Citations (Scopus)
14 Downloads (Pure)

Abstract

Parity games have important practical applications in formal verification and synthesis, especially to solve the model-checking problem of the modal mu-calculus. They are also interesting from the theory perspective, because they are widely believed to admit a polynomial solution, but so far no such algorithm is known. We propose a new algorithm to solve parity games based on learning tangles, which are strongly connected subgraphs for which one player has a strategy to win all cycles in the subgraph. We argue that tangles play a fundamental role in the prominent parity game solving algorithms. We show that tangle learning is competitive in practice and the fastest solver for large random games.

Original languageEnglish
Title of host publicationComputer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
EditorsGeorg Weissenbacher, Hana Chockler
PublisherSpringer
Pages198-215
Number of pages18
ISBN (Print)9783319961415
DOIs
Publication statusPublished - 2018
Externally publishedYes
Event30th International Conference on Computer Aided Verification, CAV 2018 - Oxford, United Kingdom
Duration: 14 Jul 201817 Jul 2018
Conference number: 30

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10982 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference30th International Conference on Computer Aided Verification, CAV 2018
Abbreviated titleCAV 2018
Country/TerritoryUnited Kingdom
CityOxford
Period14/07/1817/07/18
OtherHeld as Part of the Federated Logic Conference, FloC 2018

Fingerprint

Dive into the research topics of 'Attracting tangles to solve parity games'. Together they form a unique fingerprint.

Cite this