On Promptness in Parity Games

• Autorzy: Mogavero F. , Murano A. , Sorrentino L.

Identyfikatory

DOI

10.3233/FI-2015-1235

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

parity games; formal verification; liveness; promptness; cost-parity games; quantitative games; UPTIME ∩ COUPTIME

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2015
• Tom: Vol. 139, nr 3
• Strony: 277--305
• Opis fizyczny: Bibliogr. 44 poz., rys., tab.

Twórcy

autor

Mogavero F.

• Università degli Studi di Napoli Federico II Via Claudio, n.21, 80125, Napoli, Italy

autor

Murano A.

• Università degli Studi di Napoli Federico II Via Claudio, n.21, 80125, Napoli, Italy

autor

Sorrentino L.

• Università degli Studi di Napoli Federico II Via Claudio, n.21, 80125, Napoli, Italy

Bibliografia

• [1] Almagor, S., Hirshfeld, Y., Kupferman,O.: Promptness in omega-RegularAutomata., Automated Technology for Verification and Analysis’10, LNCS 7388, Springer, 2010.
• [2] Alur, R., Henzinger, T.: Finitary Fairness., Transactions on Programming Languages and Systems, 20(6), 1998, 1171–1194.
• [3] Aminof, B., Kupferman, O., Murano, A.: Improved Model Checking of Hierarchical Systems., Information and Computation, 210, 2012, 68–86.
• [4] Aminof, B., Mogavero, F., Murano, A.: Synthesis of Hierarchical Systems., Science of Computer Programming, 83, 2014, 56–79.
• [5] B. Aminof and A. Legay and A. Murano and O. Serre and M.Y. Vardi: Pushdown Module Checking with Imperfect Information., Information and Computation, 223, 2013, 1–17.
• [6] van der Berg, F.: Solving Parity Games on the Playstation 3., Twente Student Conference on IT’10, 2010.
• [7] Berwanger, D.: Admissibility in Infinite Games., Symposium on Theoretical Aspects of Computer Science’07, LNCS 4393, Springer, 2007.
• [8] Bouquet, A.-J., Serre, O., Walukiewicz, I.: Pushdown Games with Unboundedness and Regular Conditions., Foundations of Software Technology and Theoretical Computer Science’03, LNCS 2914, Springer, 2003.
• [9] Čermák, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications., Computer Aided Verification’14, LNCS 8559, Springer, 2014.
• [10] Chatterjee, K., Doyen, L.: Energy Parity Games., Theoretical Computer Science, 458, 2012, 49–60.
• [11] Chatterjee, K., Doyen, L., Henzinger, T., Raskin, J.-F.: Generalized Mean-payoff and Energy Games., Foundations of Software Technology and Theoretical Computer Science’10, LIPIcs 8, Leibniz-Zentrumfuer Informatik, 2010.
• [12] Chatterjee, K., Henzinger, T., Horn, F.: Finitary Winning in omega-Regular Games., Transactions On Computational Logic, 11(1), 2010, 1:1–26.
• [13] Chatterjee, K., Henzinger, T., Jurdzinski, M.: Mean-Payoff Parity Games., Logic in Computer Science’05, IEEE Computer Society, 2005.
• [14] Chatterjee, K., Henzinger, T., Piterman, N.: Strategy Logic., Information and Computation, 208(6), 2010, 677–693.
• [15] Chatterjee, K., Jurdzinski,M., Henzinger, T.: Quantitative Stochastic Parity Games., Symposium on Discrete Algorithms’04, Association for Computing Machinery, 2004.
• [16] Clarke, E., Emerson, E.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic., Logic of Programs’81, LNCS 131, Springer, 1981.
• [17] Clarke, E., Grumberg, O., Peled, D.: Model Checking., MIT Press, 2002.
• [18] Ehrenfeucht, A.,Mycielski, J.: Positional Strategies forMean Payoff Games., International Journal of Game Theory, 8(2), 1979.
• [19] Emerson, E., Jutla, C.: Tree Automata, muCalculus, and Determinacy., Foundation of Computer Science’91, IEEE Computer Society, 1991.
• [20] Fijalkow, N., Zimmermann, M.: Cost-Parity and Cost-Streett Games., Foundations of Software Technology and Theoretical Computer Science’12, LIPIcs 18, Leibniz-Zentrum fuer Informatik, 2012.
• [21] Fijalkow, N., Zimmermann,M.: Cost-Parity and Cost-Streett Games., LogicalMethods in Computer Science, 10(2), 2014, 1–29.
• [22] Friedmann, O., Lange, M.: Solving Parity Games in Practice., Automated Technology for Verification and Analysis’09, LNCS 5799, Springer, 2009.
• [23] Hoffmann, P., Luttenberger,M.: Solving Parity Games on the GPU., Automated Technology for Verification and Analysis’13, LNCS 8172, Springer, 2013.
• [24] Horn, F., Thomas, W., Wallmeier, N.: Optimal Strategy Synthesis in Request-Response Games., Automated Technology for Verification and Analysis’08, LNCS 5311, Springer, 2008.
• [25] Jurdzinski, M.: Deciding the Winner in Parity Games is in UP ∩ co-Up., Information Processing Letters, 68(3), 1998, 119–124.
• [26] Jurdzinski, M.: Small Progress Measures for Solving Parity Games., Symposium on Theoretical Aspects of Computer Science’00, LNCS 1770, Springer, 2000.
• [27] Jurdzinski, M., Paterson, M., Zwick, U.: A Deterministic Subexponential Algorithm for Solving Parity Games., Symposium on Discrete Algorithms’06, Association for Computing Machinery, 2006.
• [28] Jurdzinski, M., Paterson, M., Zwick, U.: A Deterministic Subexponential Algorithm for Solving Parity Games., SIAM Journal on Computing, 38(4), 2008, 1519–1532.
• [29] Kozen, D.: Results on the Propositional muCalculus., Theoretical Computer Science, 27(3), 1983, 333–354.
• [30] Kupferman, O., Morgenstern, G., Murano, A.: Typeness for omega-Regular Automata., International Journal of Foundations of Computer Science, 17(4), 2006, 869–884.
• [31] Kupferman, O., Piterman, N., Vardi, M.: From Liveness to Promptness., Formal Methods in System Design, 34(2), 2009, 83–103.
• [32] Kupferman, O., Vardi, M.: Module Checking Revisited., Computer Aided Verification’97, LNCS 1254, Springer, 1997.
• [33] Kupferman, O., Vardi, M., Wolper, P.: An Automata Theoretic Approach to Branching-Time Model Checking., Journal of the ACM, 47(2), 2000, 312–360.
• [34] Kupferman, O., Vardi, M., Wolper, P.: Module Checking., Information and Computation, 164(2), 2001, 322–344.
• [35] Mogavero, F., Murano, A., Perelli, G., Vardi, M.: Reasoning About Strategies: On the Model-Checking Problem., Transactions On Computational Logic, 15(4), 2014, 34:1–42.
• [36] Mogavero, F., Murano, A., Sauro, L.: A Behavioral Hierarchy of Strategy Logic., Computational Logic in Multi-Agent Systems’14, LNCS 8624, Springer, 2014.
• [37] Mogavero, F.,Murano, A., Sorrentino, L.: On Promptness in Parity Games., Logic for Programming Artificial Intelligence and Reasoning’13, LNCS 8312, Springer, 2013.
• [38] Mogavero, F., Murano, A., Vardi,M.: Reasoning About Strategies., Foundations of Software Technology and Theoretical Computer Science’10, LIPIcs 8, Leibniz-Zentrum fuer Informatik, 2010.
• [39] Pnueli, A.: The Temporal Logic of Programs., Foundation of Computer Science’77, IEEE Computer Society, 1977.
• [40] Queille, J., Sifakis, J.: Specification and Verification of Concurrent Programs in Cesar., Symposium on Programming’81, LNCS 137, Springer, 1981.
• [41] Stasio, A. D., Murano, A., Prignano, V., Sorrentino, L.: Solving Parity Games in Scala., Formal Aspects of Component Software’14, LNCS 8997, Springer, 2014.
• [42] Vöge, J., Jurdzinski, M.: A Discrete Strategy Improvement Algorithm for Solving Parity Games., Computer Aided Verification’00, LNCS 1855, Springer, 2000.
• [43] Walukiewicz, I.: Pushdown Processes: Games and Model-Checking., Information and Computation, 164(2), 2001, 234–263.
• [44] Zielonka, W.: Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees., Theoretical Computer Science, 200(1-2), 1998, 135–183.