Note: [*] Partially supported by FP7 EU project 600958-SHERPA and Embedded System Project CUP B25B09090100007.
Note: [†] This article is an extended version of the paper [37] appeared in LPAR 2013.
Note: [‡] Address for correspondence: Via Claudio, n.21, 80125, Napoli, Italy.
Abstract: Parity games are infinite-duration two-player turn-based games that provide powerful formal-method techniques for the automatic synthesis and verification of distributed and reactive systems. This kind of game emerges as a natural evaluation technique for the solution of the μ-calculus model-checking problem and is closely related to alternating ω-automata. Due to these strict connections, parity games are a well-established environment to describe liveness properties such as “every request that occurs infinitely often is eventually responded”. Unfortunately, the classical form of such a condition suffers from the strong drawback that there is no bound on the effective time that separates a request from its response, i.e., responses are not promptly provided. Recently, to overcome this limitation, several variants of parity game have been proposed, in which quantitative requirements are added to the classic qualitative ones. In this paper, we make a general study of the concept of promptness in parity games that allows to put under a unique theoretical framework several of the cited variants along with new ones. Also, we describe simple polynomial reductions from all these conditions to either Büchi or parity games, which simplify all previous known procedures. In particular, they allow to lower the complexity class of cost and bounded-cost parity games recently introduced. Indeed, we provide solution algorithms showing that determining the winner of these games is in UPTIME ∩ COUPTIME.
