Document Open Access Logo

Conditionally Optimal Algorithms for Generalized Büchi Games

Authors Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, Veronika Loitzenbauer

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2016.25.pdf
  • Filesize: 0.6 MB
  • 15 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
Wolfgang Dvorák
Monika Henzinger
Veronika Loitzenbauer

Cite AsGet BibTex

Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, and Veronika Loitzenbauer. Conditionally Optimal Algorithms for Generalized Büchi Games. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 25:1-25:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.MFCS.2016.25

Abstract

Games on graphs provide the appropriate framework to study several central problems in computer science, such as verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized Büchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized Büchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification. We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider graph games with n vertices, m edges, and generalized Büchi objectives with k conjunctions. First, we present an algorithm with running time O(k*n^2), improving the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm is optimal for dense graphs under (A1). Second, we show that the basic algorithm for the problem is optimal for sparse graphs when the target sets have constant size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1 k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time algorithm for m > n^{1.5}.
Keywords
  • generalized Büchi objective
  • GR(1) objective
  • conditional lower bounds
  • graph games
  • graph algorithms
  • computer-aided verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Amir Abboud, Arturs Backurs, and Virginia Vassilevska Williams. If the current clique algorithms are optimal, so is Valiant’s parser. In FOCS, pages 98-117, 2015. Google Scholar
  2. Amir Abboud, Arturs Backurs, and Virginia Vassilevska Williams. Tight Hardness Results For LCS and other Sequence Similarity Measures. In FOCS, pages 59-78, 2015. Google Scholar
  3. Amir Abboud and Virginia Vassilevska Williams. Popular conjectures imply strong lower bounds for dynamic problems. In FOCS, pages 434-443, 2014. Google Scholar
  4. Amir Abboud, Virginia Vassilevska Williams, and Oren Weimann. Consequences of faster alignment of sequences. In ICALP 2014, Proceedings, Part I, pages 39-51, 2014. Google Scholar
  5. Amir Abboud, Virginia Vassilevska Williams, and Huacheng Yu. Matching triangles and basing hardness on an extremely popular conjecture. In STOC, pages 41-50, 2015. Google Scholar
  6. Amir Abboud, Virginia Vassilevska Williams, and Joshua R. Wang. Approximation and fixed parameter subquadratic algorithms for radius and diameter in sparse graphs. In SODA, pages 377-391, 2016. Google Scholar
  7. Rajeev Alur and Thomas A. Henzinger. Computer-aided verification, 2004. Unpublished, available at URL: http://www.cis.upenn.edu/group/cis673/.
  8. Rajeev Alur, Thomas. A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. Journal of the ACM, 49:672-713, 2002. Google Scholar
  9. Rajeev Alur and Salvatore La Torre. Deterministic generators and games for ltl fragments. ACM Trans. Comput. Log., 5(1):1-25, 2004. Google Scholar
  10. Arturs Backurs and Piotr Indyk. Edit distance cannot be computed in strongly subquadratic time (unless SETH is false). In STOC, pages 51-58, 2015. Google Scholar
  11. Catriel Beeri. On the membership problem for functional and multivalued dependencies in relational databases. ACM Transactions on Database Systems, pages 241-259, 1980. Google Scholar
  12. Dietmar Berwanger, Anuj Dawar, Paul Hunter, and Stephan Kreutzer. Dag-width and parity games. In STACS, pages 524-536, 2006. Google Scholar
  13. Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, and Barbara Jobstmann. Robustness in the presence of liveness. In CAV, pages 410-424, 2010. Google Scholar
  14. Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Martin Weiglhofer. Interactive presentation: Automatic hardware synthesis from specifications: a case study. In DATE, pages 1188-1193, 2007. Google Scholar
  15. Karl Bringmann. Why walking the dog takes time: Frechet distance has no strongly subquadratic algorithms unless SETH fails. In FOCS, pages 661-670, 2014. Google Scholar
  16. Karl Bringmann and Marvin Künnemann. Quadratic Conditional Lower Bounds for String Problems and Dynamic Time Warping. In FOCS, pages 79-97, 2015. Google Scholar
  17. J. Richard Büchi. Weak second-order arithmetic and finite automata. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 6:66-92, 1960. Google Scholar
  18. J. Richard Büchi. On a decision method in restricted second-order arithmetic. In E. Nagel, P. Suppes, and A. Tarski, editors, Proceedings of the First International Congress on Logic, Methodology, and Philosophy of Science 1960, pages 1-11. Stanford University Press, 1962. Google Scholar
  19. J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the AMS, 138:295-311, 1969. Google Scholar
  20. Chris Calabro, Russell Impagliazzo, and Ramamohan Paturi. The complexity of satisfiability of small depth circuits. In IWPEC, pages 75-85, 2009. Google Scholar
  21. Krishnendu Chatterjee, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. Qualitative analysis of pomdps with temporal logic specifications for robotics applications. In IEEE International Conference on Robotics and Automation, ICRA, pages 325-330, 2015. Google Scholar
  22. Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, and Veronika Loitzenbauer. Model and objective separation with conditional lower bounds: Disjunction is harder than conjunction. In LICS, 2016. To appear, available at URL: http://arxiv.org/abs/1602.02670.
  23. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. In POPL, pages 733-747, 2016. Google Scholar
  24. Krishnendu Chatterjee and Monika Henzinger. Faster and Dynamic Algorithms For Maximal End-Component Decomposition And Related Graph Problems In Probabilistic Verification. In SODA, pages 1318-1336, 2011. Google Scholar
  25. Krishnendu Chatterjee and Monika Henzinger. An O(n²) Time Algorithm for Alternating Büchi Games. In SODA, pages 1386-1399, 2012. Google Scholar
  26. Krishnendu Chatterjee and Monika Henzinger. Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-component Decomposition. Journal of the ACM, 61(3):15, 2014. Google Scholar
  27. Krishnendu Chatterjee, Monika Henzinger, and Veronika Loitzenbauer. Improved Algorithms for One-Pair and k-Pair Streett Objectives. In LICS, pages 269-280, 2015. Google Scholar
  28. Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, and Prateesh Goyal. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. In POPL. ACM, 2015. Google Scholar
  29. Krishnendu Chatterjee, Marcin Jurdziński, and Thomas A. Henzinger. Simple stochastic parity games. In CSL, pages 100-113, 2003. Google Scholar
  30. Alonzo Church. Logic, arithmetic, and automata. In Proceedings of the International Congress of Mathematicians, pages 23-35. Institut Mittag-Leffler, 1962. Google Scholar
  31. Luca de Alfaro and Thomas A. Henzinger. Interface automata. In FSE'01, pages 109-120. ACM Press, 2001. Google Scholar
  32. David L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. The MIT Press, 1989. Google Scholar
  33. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy. In FOCS, pages 368-377, 1991. Google Scholar
  34. Kousha Etessami, Thomas Wilke, and Rebecca A. Schuller. Fair simulation relations, parity games, and state space reduction for büchi automata. SIAM J. Comput., 34(5):1159-1175, 2005. Google Scholar
  35. Georgios E. Fainekos, Hadas Kress-Gazit, and George J. Pappas. Temporal logic motion planning for mobile robots. In IEEE International Conference on Robotics and Automation, ICRA, pages 2020-2025, 2005. Google Scholar
  36. Yashdeep Godhal, Krishnendu Chatterjee, and Thomas A. Henzinger. Synthesis of AMBA AHB from formal specification: A case study. Journal of Software Tools Technology Transfer, 2011. Google Scholar
  37. Monika Henzinger, Valerie King, and Tandy Warnow. Constructing a Tree from Homeomorphic Subtrees, with Applications to Computational Evolutionary Biology. Algorithmica, 24(1):1-13, 1999. Google Scholar
  38. Monika Henzinger, Sebastian Krinninger, Danupon Nanongkai, and Thatchaphol Saranurak. Unifying and strengthening hardness for dynamic problems via the online matrix-vector multiplication conjecture. In STOC, pages 21-30, 2015. Google Scholar
  39. Neil Immerman. Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences, pages 384-406, 1981. Google Scholar
  40. Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4):512-530, 2001. Google Scholar
  41. Marcin Jurdziński. Small Progress Measures for Solving Parity Games. In STACS, pages 290-301, 2000. Google Scholar
  42. Marcin Jurdziński, Mike Paterson, and Uri Zwick. A Deterministic Subexponential Algorithm for Solving Parity Games. SIAM Journal on Computing, 38(4):1519-1532, 2008. Google Scholar
  43. Sudeep Juvekar and Nir Piterman. Minimizing generalized büchi automata. In CAV, pages 45-58, 2006. Google Scholar
  44. Sriram C. Krishnan, Anuj Puri, and Robert K. Brayton. Deterministic Ω automata vis-a-vis deterministic buchi automata. In ISAAC, pages 378-386, 1994. Google Scholar
  45. Wouter Kuijper and Jaco van de Pol. Computing weakest strategies for safety games of imperfect information. In TACAS, pages 92-106, 2009. Google Scholar
  46. Orna Kupferman and Moshe Y. Vardi. Freedom, weakness, and determinism: From linear-time to branching-time. In LICS, pages 81-92, 1998. Google Scholar
  47. Orna Kupferman and Moshe Y. Vardi. From linear time to branching time. ACM Transactions on Computational Logic, 6(2):273-294, 2005. Google Scholar
  48. François Le Gall. Powers of Tensors and Fast Matrix Multiplication. In ISSAC, pages 296-303, 2014. Google Scholar
  49. Lillian Lee. Fast context-free grammar parsing requires fast boolean matrix multiplication. J. ACM, 49(1):1-15, January 2002. Google Scholar
  50. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. Google Scholar
  51. Robert McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65(2):149-184, 1993. Google Scholar
  52. Mihai Patrascu and Ryan Williams. On the possibility of faster SAT algorithms. In SODA, pages 1065-1075, 2010. Google Scholar
  53. Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. In VMCAI, LNCS 3855, Springer, pages 364-380, 2006. Google Scholar
  54. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, pages 179-190. ACM Press, 1989. Google Scholar
  55. P.J. Ramadge and W.M. Wonham. Supervisory control of a class of discrete-event processes. SIAM Journal of Control and Optimization, 25(1):206-230, 1987. Google Scholar
  56. Sven Schewe. Solving Parity Games in Big Steps. In FSTTCS, pages 449-460, 2007. Google Scholar
  57. Mikkel Thorup. All Structured Programs Have Small Tree Width and Good Register Allocation. Information and Computation, 142(2):159 - 181, 1998. Google Scholar
  58. Virginia Vassilevska Williams and Ryan Williams. Subcubic equivalences between path, matrix and triangle problems. In FOCS, pages 645-654, 2010. Google Scholar
  59. Ryan Williams. A new algorithm for optimal 2-constraint satisfaction and its implications. Theor. Comput. Sci., 348(2-3):357-365, 2005. Announced at ICALP'04. Google Scholar
  60. Ryan Williams. Faster all-pairs shortest paths via circuit complexity. In STOC, pages 664-673, 2014. Google Scholar
  61. Ryan Williams. Faster decision of first-order graph properties. In CSL-LICS, pages 80:1-80:6, 2014. Google Scholar
  62. Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1-2):135-183, 1998. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact