×

On omega-languages defined by mean-payoff conditions. (English) Zbl 1234.68248

de Alfaro, Luca (ed.), Foundations of software science and computational structures. 12th international conference, FOSSACS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22–29, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-00595-4/pbk). Lecture Notes in Computer Science 5504, 333-347 (2009).
Summary: In quantitative verification, system states/transitions have associated payoffs, and these are used to associate mean-payoffs with infinite behaviors. In this paper, we propose to define \(\omega \)-languages via Boolean queries over mean-payoffs. Requirements concerning averages such as “the number of messages lost is negligible” are not \(\omega \)-regular, but specifiable in our framework. We show that, for closure under intersection, one needs to consider multi-dimensional payoffs. We argue that the acceptance condition needs to examine the set of accumulation points of sequences of mean-payoffs of prefixes, and give a precise characterization of such sets. We propose the class of multi-threshold mean-payoff languages using acceptance conditions that are Boolean combinations of inequalities comparing the minimal or maximal accumulation point along some coordinate with a constant threshold. For this class of languages, we study expressiveness, closure properties, analyzability, and Borel complexity.
For the entire collection see [Zbl 1157.68009].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alur, R., Kanade, A., Weiss, G.: Ranking automata and games for prioritized requirements. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 240–253. Springer, Heidelberg (2008) · Zbl 1155.68414 · doi:10.1007/978-3-540-70545-1_23
[2] Chatterjee, K.: Concurrent games with tail objectives. Theor. Comput. Sci. 388(1-3), 181–198 (2007) · Zbl 1177.91031 · doi:10.1016/j.tcs.2007.07.047
[3] Chatterjee, K., de Alfaro, L., Henzinger, T.: The complexity of quantitative concurrent parity games. In: Proceedings of the 17th ACM-SIAM Symposium on Discrete Algorithms, pp. 678–687 (2006) · Zbl 1192.68430 · doi:10.1145/1109557.1109631
[4] Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 385–400. Springer, Heidelberg (2008) · Zbl 1156.68449 · doi:10.1007/978-3-540-87531-4_28
[5] Chatterjee, K., Henzinger, T., Jurdziński, M.: Mean-payoff parity games. In: Proceedings of the 20th Annual Symposium on Logic in Computer Science, pp. 178–187. IEEE Computer Society Press, Los Alamitos (2005)
[6] Gimbert, H., Zielonka, W.: Deterministic priority mean-payoff games as limits of discounted games. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 312–323. Springer, Heidelberg (2006) · Zbl 1133.91318 · doi:10.1007/11787006_27
[7] Kupferman, O., Lustig, Y.: Lattice automata. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 199–213. Springer, Heidelberg (2007) · Zbl 1132.68455 · doi:10.1007/978-3-540-69738-1_14
[8] Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: Specification. Springer, Heidelberg (1991) · Zbl 0753.68003
[9] Pnueli, A.: The temporal logic of programs. In: 18th IEEE Symposium on the Foundations of Computer Science (FOCS 1977), pp. 46–57 (1977) · doi:10.1109/SFCS.1977.32
[10] Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–191. Elsevier, Amsterdam (1990) · Zbl 0900.68316
[11] Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994) · Zbl 0827.03009 · doi:10.1006/inco.1994.1092
[12] Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theoretical Computer Science 158, 343–359 (1996) · Zbl 0871.68138 · doi:10.1016/0304-3975(95)00188-3
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.