2013 | OriginalPaper | Buchkapitel
On Promptness in Parity Games
verfasst von : Fabio Mogavero, Aniello Murano, Loredana Sorrentino
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Parity games
are a powerful formalism for the automatic synthesis and verification of reactive systems. They are closely related to alternating
ω
-automata and emerge as a natural method for the solution of the
μ
-calculus model checking problem. 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 parity game variants 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 improve the complexity results of
cost
and
bounded-cost parity games
. Indeed, we provide solution algorithms showing that determining the winner of these games lies in
UPTime
∩
CoUPTime
.