×

zbMATH — the first resource for mathematics

Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. (English) Zbl 1295.91019
Summary: The computation of the winning set for Büchi objectives in alternating games on graphs is a central problem in computer-aided verification with a large number of applications. The long-standing best known upper bound for solving the problem is \(\tilde{O}(n\cdot m)\), where \(n\) is the number of vertices and \(m\) is the number of edges in the graph. We are the first to break the \(\tilde{O}(n \cdot m)\) boundary by presenting a new technique that reduces the running time to \(O(n^{2})\). This bound also leads to \(O(n^{2})\)-time algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of \(\tilde{O}(n \cdot m))\), (2) in concurrent graph games with constant actions (improving an earlier bound of \(O(n^{3}))\), and (3) in Markov decision processes (improving for \(m>n^{4/3}\) an earlier bound of \(O(m \cdot \sqrt{m}))\). We then show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in \(O(n)\) amortized time per operation. Our algorithms are the first dynamic algorithms for this problem. We then consider another core graph theoretic problem in verification of probabilistic systems, namely computing the maximal end-component decomposition of a graph. We present two improved static algorithms for the maximal end-component decomposition problem. Our first algorithm is an \(O(m \cdot \sqrt{m})\)-time algorithm, and our second algorithm is an \(O(n^{2})\)-time algorithm which is obtained using the same technique as for alternating Büchi games. Thus, we obtain an \(O(\min \{m \cdot \sqrt{m},n^{2}\})\)-time algorithm improving the long-standing \(O(n \cdot m)\) time bound. Finally, we show how to maintain the maximal end-component decomposition of a graph under a sequence of edge insertions or a sequence of edge deletions in \(O(n)\) amortized time per edge deletion, and \(O(m)\) worst-case time per edge insertion. Again, our algorithms are the first dynamic algorithms for this problem.
Reviewer: Reviewer (Berlin)

MSC:
91A43 Games involving graphs
05C85 Graph algorithms (graph-theoretic aspects)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
68R10 Graph theory (including graph drawing) in computer science
91A10 Noncooperative games
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] R. Alur, T. Henzinger, and O. Kupferman. 2002. Alternating-time temporal logic. J. ACM 49, 672–713. · Zbl 1326.68181 · doi:10.1145/585265.585270
[2] R. Alur and S. L. Torre. 2004. Deterministic generators and games for LTL fragments. ACM Trans. Comput. Logic 5, 1, 1–25. · Zbl 1366.03181 · doi:10.1145/963927.963928
[3] C. Beeri. 1980. On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Datab. Syst. 5, 241–259. · Zbl 0441.68118 · doi:10.1145/320613.320614
[4] A. Bianco and L. de Alfaro. 1995. Model checking of probabilistic and nondeterministic systems. In Proceedings of the Symposium on Software Technology and Theoretical Computer Science (FSTTCS 95). Lecture Notes in Computer Science Series, vol. 1026, Springer-Verlag, 499–513. · Zbl 1354.68167
[5] R. Bloem, S. J. Galler, B. Jobstmann, N. Piterman, A. Pnueli, and M. Weiglhofer. 2007. Interactive presentation: Automatic hardware synthesis from specifications: A case study. In Proceedings of DATE. 1188–1193.
[6] T. Brázdil, V. Brozek, K. Chatterjee, V. Forejt, and A. Kučera. 2011. Two views on multiple mean-payoff objectives in Markov decision processes. In Proceedings of LICS. 33–42.
[7] T. Brázdil, K. Chatterjee, V. Forejt, and A. Kucera. 2013. Trading performance for stability in Markov decision processes. In Proceedings of LICS. 331–340. · Zbl 1366.68087
[8] J. Büchi. 1960. Weak second-order arithmetic and finite automata. Zeits. Math. Logik Grund. Math. 6, 66–92. · Zbl 0103.24705
[9] J. Büchi. 1962. On a decision method in restricted second-order arithmetic. In Proceedings of the 1st International Congress on Logic, Methodology, and Philosophy of Science 1960. E. Nagel, P. Suppes, and A. Tarski, Eds., Stanford University Press, 1–11.
[10] J. Büchi and L. Landweber. 1969. Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295–311. · Zbl 0182.02302
[11] A. K. Chandra, D. Kozen, and L. J. Stockmeyer. 1981. Alternation. J. ACM 28, 1, 114–133. · Zbl 0473.68043 · doi:10.1145/322234.322243
[12] K. Chatterjee and M. Henzinger. 2011. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In Proceedings of SODA’11. SIAM. · Zbl 1374.68272
[13] K. Chatterjee and M. Henzinger. 2012. An O(n<sup>2</sup>) algorithm for alternating Büchi games. In Proceedings of SODA. ACM-SIAM.
[14] K. Chatterjee, T. Henzinger, and N. Piterman. 2006. Algorithms for Büchi games. In Proceedings of the Symposium on Games in Design and Verification (GDV).
[15] K. Chatterjee and T. A. Henzinger. 2007a. Assume-guarantee synthesis. In Proceedings of TACAS. Lecture Notes in Computer Science, vol. 4424, Springer, 261–275. · Zbl 1186.68284
[16] K. Chatterjee and T. A. Henzinger. 2007b. Probabilistic systems with limsup and liminf objectives. In Proceedings of ILC. 32–45. · Zbl 1258.68099
[17] K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh. 2010. Measuring and synthesizing systems in probabilistic environments. In Proceedings of CAV 10. Springer. · Zbl 1321.68344
[18] K. Chatterjee, M. Jurdziński, and T. Henzinger. 2003. Simple stochastic parity games. In Proceedings of CSL’03. Lecture Notes in Computer Science, vol. 2803, Springer, 100–113. · Zbl 1116.68493
[19] K. Chatterjee, M. Jurdziński, and T. Henzinger. 2004. Quantitative stochastic parity games. In Proceedings of SODA’04. SIAM, 121–130. · Zbl 1318.91027
[20] K. Chatterjee and J. Lacki. 2013. Faster algorithms for Markov decision processes with low treewidth. In Proceedings of CAV. 543–558.
[21] K. Chatterjee and V. Raman. 2012. Synthesizing protocols for digital contract signing. In Proceedings of VMCAI. Lecture Notes in Computer Science, vol. 7148, Springer, 152–168. · Zbl 1325.94115
[22] A. Church. 1962. Logic, arithmetic, and automata. In Proceedings of the International Congress of Mathematicians. Institut Mittag-Leffler, 23–35.
[23] A. Condon. 1992. The complexity of stochastic games. Inf. Comput. 96, 2, 203–224. · Zbl 0756.90103 · doi:10.1016/0890-5401(92)90048-K
[24] C. Courcoubetis and M. Yannakakis. 1995. The complexity of probabilistic verification. J. ACM 42, 4, 857–907. · Zbl 0885.68109 · doi:10.1145/210332.210339
[25] L. de Alfaro. 1997. Formal verification of probabilistic systems. Ph.D. dissertation, Stanford Univ.
[26] L. de Alfaro, M. Faella, R. Majumdar, and V. Raman. 2005. Code-aware resource management. In Proceedings of EMSOFT 05. ACM. · Zbl 1291.68137
[27] L. de Alfaro and T. Henzinger. 2001. Interface automata. In Proceedings of FSE’01. ACM Press, 109–120.
[28] D. Dill. 1989. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. The MIT Press.
[29] E. Emerson and C. Jutla. 1991. Tree automata, mu-calculus and determinacy. In Proceedings of FOCS’91. IEEE, 368–377.
[30] K. Etessami, M. Z. Kwiatkowska, M. Y. Vardi, and M. Yannakakis. 2008. Multi-objective model checking of Markov decision processes. Log. Meth. Comput. Sci. 4, 4. · Zbl 1161.68565 · doi:10.2168/LMCS-4(4:8)2008
[31] S. Even and Y. Shiloach. 1981. An on-line edge-deletion problem. J. ACM 28, 1, 1–4. · Zbl 0454.68075 · doi:10.1145/322234.322235
[32] J. Filar and K. Vrieze. 1997. Competitive Markov Decision Processes. Springer-Verlag. · Zbl 0934.91002
[33] Y. Godhal, K. Chatterjee, and T. A. Henzinger. 2011. Synthesis of AMBA AHB from formal specification: A case study. J. Softw. Tools Techn. Transfer.
[34] M. R. Henzinger, V. King, and T. Warnow. 1999. Constructing a tree from homeomorphic subtrees, with applications to computational evolutionary biology. Algorithmica 24, 1, 1–13. · Zbl 0936.68026 · doi:10.1007/PL00009268
[35] H. Howard. 1960. Dynamic Programming and Markov Processes. MIT Press. · Zbl 0091.16001
[36] N. Immerman. 1981. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 384–406. · Zbl 0486.03019 · doi:10.1016/0022-0000(81)90039-8
[37] M. Jurdziński. 2000. Small progress measures for solving parity games. In Proceedings of STACS’00. Lecture Notes in Computer Science, vol. 1770, Springer, 290–301. · Zbl 0962.68111
[38] M. Jurdziński, O. Kupferman, and T. A. Henzinger. 2002. Trading probability for fairness. In CSL: Computer Science Logic. Lecture Notes in Computer Science, vol. 2471, Springer, 292–305. · Zbl 1020.68060
[39] A. Kechris. 1995. Classical Descriptive Set Theory. Springer. · Zbl 0819.04002 · doi:10.1007/978-1-4612-4190-4
[40] S. C. Krishnan, A. Puri, and R. K. Brayton. 1994. Deterministic w automata vis-a-vis deterministic Büchi automata. In Proceedings of ISAAC. Lecture Notes in Computer Science, vol. 834, Springer, 378–386. · Zbl 0953.68563
[41] O. Kupferman and M. Vardi. 2005. From linear time to branching time. ACM Trans. Computat. Logic 6, 2, 273–294. · Zbl 1367.68195 · doi:10.1145/1055686.1055689
[42] O. Kupferman and M. Y. Vardi. 1998. Freedom, weakness, and determinism: From linear-time to branching-time. In Proceedings of LICS. 81–92. · Zbl 0945.68522
[43] M. Kwiatkowska, G. Norman, and D. Parker. 2000. Verifying randomized distributed algorithms with prism. In Proceedings of the Workshop on Advances in Verification (WAVE’00).
[44] J. Lacki. 2011. Improved deterministic algorithms for decremental transitive closure and strongly connected components. In Proceedings of SODA. 1438–1445. · Zbl 1376.05152
[45] A. Mahanti and A. Bagchi. 1985. AND/OR graph heuristic search methods. JACM 32, 1, 28–51. · Zbl 0633.68098 · doi:10.1145/2455.2459
[46] R. McNaughton. 1993. Infinite games played on finite graphs. Ann. Pure Appl. Logic 65, 149–184. · Zbl 0798.90151 · doi:10.1016/0168-0072(93)90036-D
[47] N. Piterman, A. Pnueli, and Y. Sa’ar. 2006. Synthesis of reactive(1) designs. In Proceedings of VMCAI. Lecture Notes in Computer Science, vol. 3855, Springer, 364–380. · Zbl 1176.68126
[48] A. Pnueli and R. Rosner. 1989. On the synthesis of a reactive module. In Proceedings of POPL’89. ACM, 179–190. · Zbl 0686.68015
[49] A. Pogosyants, R. Segala, and N. Lynch. 2000. Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distrib. Comput. 13, 3, 155–186. · doi:10.1007/PL00008917
[50] P. Ramadge and W. Wonham. 1987. Supervisory control of a class of discrete-event processes. SIAM J. Control Optim. 25, 1, 206–230. · Zbl 0618.93033 · doi:10.1137/0325013
[51] R. Segala. 1995. Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, MIT. (Technical Report MIT/LCS/TR-676.)
[52] M. Stoelinga. 2002. Fun with FireWire: Experiments with verifying the IEEE 1394 root contention protocol. In Formal Aspects of Computing. · Zbl 1029.68022
[53] R. E. Tarjan. 1972. Depth first search and linear graph algorithms. SIAM J. Comput. 1, 2, 146–160. · Zbl 0251.05107 · doi:10.1137/0201010
[54] W. Thomas. 1997. Languages, automata, and logic. In Handbook of Formal Languages, G. Rozenberg and A. Salomaa, Eds., Vol. 3, Beyond Words, Springer, 389–455.
[55] M. Vardi. 2007a. Automata-theoretic model checking revisited. In Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 4349, Springer, 137–150. · Zbl 1132.68483
[56] M. Vardi. 2007b. The Büchi complementation saga. In Proceedings of the Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 4393, Springer, 12–22. · Zbl 1186.03062
[57] W. Zielonka. 1998. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoret. Comput. Sci. 200, 1–2, 135–183. · Zbl 0915.68120 · doi:10.1016/S0304-3975(98)00009-7
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.