Parity games are abstract infinite-round games that take an important role in formal verification. In the basic setting, these games are two-player, turn-based, and played under perfect information on directed graphs, whose nodes are labeled with priorities. The winner of a play is determined according to the parities (even or odd) of the minimal priority occurring infinitely often in that play. The problem of finding a winning strategy in parity games is known to be in UPTime ∩ CoUPTime and deciding whether a polynomial time solution exists is a longstanding open question. In the last two decades, a variety of algorithms have been proposed. Many of them have been also implemented in a platform named PGSolver. This has enabled an empirical evaluation of these algorithms and a better understanding of their relative merits. In this paper, we further contribute to this subject by implementing, for the first time, an algorithm based on alternating automata. More precisely, we consider an algorithm introduced by Kupferman and Vardi that solves a parity game by solving the emptiness problem of a corresponding alternating parity automaton. Our empirical evaluation demonstrates that this algorithm outperforms other algorithms when the game has a small number of priorities relative to the size of the game. In many concrete applications, we do indeed end up with parity games where the number of priorities is relatively small. This makes the new algorithm quite useful in practice.

Solving parity games using an automata-based algorithm / Di Stasio, A.; Murano, A.; Perelli, G.; Vardi, M. Y.. - 9705:(2016), pp. 64-76. ((Intervento presentato al convegno 21st International Conference on Implementation and Application of Automata, CIAA 2016 tenutosi a Seoul; South Korea [10.1007/978-3-319-40946-7_6].

### Solving parity games using an automata-based algorithm

#### Abstract

Parity games are abstract infinite-round games that take an important role in formal verification. In the basic setting, these games are two-player, turn-based, and played under perfect information on directed graphs, whose nodes are labeled with priorities. The winner of a play is determined according to the parities (even or odd) of the minimal priority occurring infinitely often in that play. The problem of finding a winning strategy in parity games is known to be in UPTime ∩ CoUPTime and deciding whether a polynomial time solution exists is a longstanding open question. In the last two decades, a variety of algorithms have been proposed. Many of them have been also implemented in a platform named PGSolver. This has enabled an empirical evaluation of these algorithms and a better understanding of their relative merits. In this paper, we further contribute to this subject by implementing, for the first time, an algorithm based on alternating automata. More precisely, we consider an algorithm introduced by Kupferman and Vardi that solves a parity game by solving the emptiness problem of a corresponding alternating parity automaton. Our empirical evaluation demonstrates that this algorithm outperforms other algorithms when the game has a small number of priorities relative to the size of the game. In many concrete applications, we do indeed end up with parity games where the number of priorities is relatively small. This makes the new algorithm quite useful in practice.
##### Scheda breve Scheda completa
2016
21st International Conference on Implementation and Application of Automata, CIAA 2016
Parity Games; Automata;
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Solving parity games using an automata-based algorithm / Di Stasio, A.; Murano, A.; Perelli, G.; Vardi, M. Y.. - 9705:(2016), pp. 64-76. ((Intervento presentato al convegno 21st International Conference on Implementation and Application of Automata, CIAA 2016 tenutosi a Seoul; South Korea [10.1007/978-3-319-40946-7_6].
File allegati a questo prodotto
File
DiStasio_Posttprint_Solving_2016.pdf

accesso aperto

Tipologia: Documento in Post-print (versione successiva alla peer review e accettata per la pubblicazione)
Dimensione 482.9 kB
DiStasio_Solving_2016.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Dimensione 6.4 MB

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11573/1399941`
• ND
• 13
• 8