Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Article type: Research Article
Authors: Mogavero, Fabioa | Murano, Anielloa | Sorrentino, Loredanaa; ‡
Affiliations: [a] Università degli Studi di Napoli Federico II, Via Claudio, n.21, 80125, Napoli, Italy. fabiomogavero@gmail.com; murano@na.infn.it; loredanasorrentino@alice.it
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.
Keywords: Parity games, formal verification, liveness, promptness, cost-parity games, quantitative games, UPTIME ∩ COUPTIME
DOI: 10.3233/FI-2015-1235
Journal: Fundamenta Informaticae, vol. 139, no. 3, pp. 277-305, 2015
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl