Attracting tangles to solve parity games

Tom van Dijk

doi:10.1007/978-3-319-96142-2_14

Attracting tangles to solve parity games

Tom van Dijk^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

18 Citations (Scopus)

6 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 language	English
Title of host publication	Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
Editors	Georg Weissenbacher, Hana Chockler
Publisher	Springer
Pages	198-215
Number of pages	18
ISBN (Print)	9783319961415
DOIs	https://doi.org/10.1007/978-3-319-96142-2_14
Publication status	Published - 2018
Externally published	Yes
Event	30th International Conference on Computer Aided Verification, CAV 2018 - Oxford, United Kingdom Duration: 14 Jul 2018 → 17 Jul 2018 Conference number: 30

Publication series

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

Conference

Conference	30th International Conference on Computer Aided Verification, CAV 2018
Abbreviated title	CAV 2018
Country/Territory	United Kingdom
City	Oxford
Period	14/07/18 → 17/07/18
Other	Held as Part of the Federated Logic Conference, FloC 2018

Access to Document

10.1007/978-3-319-96142-2_14Licence: CC BY

978-3-319-96142-2_14Final published version, 724 KBLicence: CC BY

Cite this

van Dijk, T. (2018). Attracting tangles to solve parity games. In G. Weissenbacher, & H. Chockler (Eds.), Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 198-215). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10982 LNCS). Springer. https://doi.org/10.1007/978-3-319-96142-2_14

van Dijk, Tom. / Attracting tangles to solve parity games. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. editor / Georg Weissenbacher ; Hana Chockler. Springer, 2018. pp. 198-215 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{8a1cc22cf4ad4f3c8b6bb3307b6cc12f,

title = "Attracting tangles to solve parity games",

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.",

author = "{van Dijk}, Tom",

note = "Funding Information: T. van Dijk—The author is supported by the FWF, NFN Grant S11408-N23 (RiSE). Publisher Copyright: {\textcopyright} The Author(s) 2018.; 30th International Conference on Computer Aided Verification, CAV 2018 , CAV 2018 ; Conference date: 14-07-2018 Through 17-07-2018",

year = "2018",

doi = "10.1007/978-3-319-96142-2_14",

language = "English",

isbn = "9783319961415",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "198--215",

editor = "Georg Weissenbacher and Hana Chockler",

booktitle = "Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",

address = "Germany",

}

van Dijk, T 2018, Attracting tangles to solve parity games. in G Weissenbacher & H Chockler (eds), Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10982 LNCS, Springer, pp. 198-215, 30th International Conference on Computer Aided Verification, CAV 2018 , Oxford, United Kingdom, 14/07/18. https://doi.org/10.1007/978-3-319-96142-2_14

Attracting tangles to solve parity games. / van Dijk, Tom.
Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. ed. / Georg Weissenbacher; Hana Chockler. Springer, 2018. p. 198-215 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10982 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Attracting tangles to solve parity games

AU - van Dijk, Tom

N1 - Conference code: 30

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85051105685&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-96142-2_14

DO - 10.1007/978-3-319-96142-2_14

M3 - Conference contribution

AN - SCOPUS:85051105685

SN - 9783319961415

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 198

EP - 215

BT - Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings

A2 - Weissenbacher, Georg

A2 - Chockler, Hana

PB - Springer

T2 - 30th International Conference on Computer Aided Verification, CAV 2018

Y2 - 14 July 2018 through 17 July 2018

ER -

van Dijk T. Attracting tangles to solve parity games. In Weissenbacher G, Chockler H, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer. 2018. p. 198-215. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-96142-2_14

Attracting tangles to solve parity games

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this