Document Open Access Logo

Faster Algorithms for Bounded Liveness in Graphs and Game Graphs

Authors Krishnendu Chatterjee, Monika Henzinger, Sagar Sudhir Kale, Alexander Svozil

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.124.pdf
  • Filesize: 0.81 MB
  • 21 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
  • IST Austria, Klosterneuburg, Austria
Monika Henzinger
  • Faculty of Computer Science, University of Vienna, Austria
Sagar Sudhir Kale
  • Faculty of Computer Science, University of Vienna, Austria
Alexander Svozil
  • Faculty of Computer Science, University of Vienna, Austria

Funding

  • Chatterjee, Krishnendu: Supported by the ERC CoG 863818 (ForM-SMArt).
  • Henzinger, Monika: Supported by the Austrian Science Fund (FWF) and netIDEE SCIENCE project P 33775-N.
  • Kale, Sagar Sudhir: Partially supported by the Vienna Science and Technology Fund (WWTF) through project ICT15-003.
  • Svozil, Alexander: Fully supported by the Vienna Science and Technology Fund (WWTF) through project ICT15-003.

Cite As Get BibTex

Krishnendu Chatterjee, Monika Henzinger, Sagar Sudhir Kale, and Alexander Svozil. Faster Algorithms for Bounded Liveness in Graphs and Game Graphs. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 124:1-124:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ICALP.2021.124

Abstract

Graphs and games on graphs are fundamental models for the analysis of reactive systems, in particular, for model-checking and the synthesis of reactive systems. The class of ω-regular languages provides a robust specification formalism for the desired properties of reactive systems. In the classical infinitary formulation of the liveness part of an ω-regular specification, a "good" event must happen eventually without any bound between the good events. A stronger notion of liveness is bounded liveness, which requires that good events happen within d transitions. Given a graph or a game graph with n vertices, m edges, and a bounded liveness objective, the previous best-known algorithmic bounds are as follows: (i) O(dm) for graphs, which in the worst-case is O(n³); and (ii) O(n² d²) for games on graphs. Our main contributions improve these long-standing algorithmic bounds. For graphs we present: (i) a randomized algorithm with one-sided error with running time O(n^{2.5} log n) for the bounded liveness objectives; and (ii) a deterministic linear-time algorithm for the complement of bounded liveness objectives. For games on graphs, we present an O(n² d) time algorithm for the bounded liveness objectives.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Graphs
  • Game Graphs
  • Büchi

Metrics

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

References

  1. Amir Abboud and Virginia Vassilevska Williams. Popular conjectures imply strong lower bounds for dynamic problems. In FOCS, pages 434-443. IEEE Computer Society, 2014. URL: https://doi.org/10.1109/FOCS.2014.53.
  2. Amir Abboud, Virginia Vassilevska Williams, and Huacheng Yu. Matching triangles and basing hardness on an extremely popular conjecture. SIAM J. Comput., 47(3):1098-1122, 2018. URL: https://doi.org/10.1137/15M1050987.
  3. Bowen Alpern and Fred B. Schneider. Defining Liveness. Information Processing Letters, 21(4):181-185, 1985. Google Scholar
  4. Rajeev Alur and Thomas A. Henzinger. Finitary Fairness. ACM Transactions on Programming Languages and Systems, 20(6):1171-1194, 1998. Google Scholar
  5. C. Beeri. On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Datab. Sys., 5(3):241-259, 1980. Google Scholar
  6. A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. Advances in Computers, 58:117-148, 2003. Google Scholar
  7. Mikolaj Bojanczyk and Thomas Colcombet. Bounds in ω-Regularity. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, LICS'06, pages 285-296. IEEE Computer Society, 2006. Google Scholar
  8. Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, and Veronika Loitzenbauer. Conditionally optimal algorithms for generalized büchi games. In MFCS, volume 58 of LIPIcs, pages 25:1-25:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.MFCS.2016.25.
  9. Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, and Veronika Loitzenbauer. Model and objective separation with conditional lower bounds: Disjunction is harder than conjunction. In LICS, pages 197-206. ACM, 2016. URL: https://doi.org/10.1145/2933575.2935304.
  10. Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, and Alexander Svozil. Algorithms and conditional lower bounds for planning problems. In Mathijs de Weerdt, Sven Koenig, Gabriele Röger, and Matthijs T. J. Spaan, editors, Proceedings of the Twenty-Eighth International Conference on Automated Planning and Scheduling, ICAPS 2018, Delft, The Netherlands, June 24-29, 2018, pages 56-64. AAAI Press, 2018. URL: https://aaai.org/ocs/index.php/ICAPS/ICAPS18/paper/view/17639.
  11. Krishnendu Chatterjee and Monika Henzinger. Efficient and dynamic algorithms for alternating büchi games and maximal end-component decomposition. J. ACM, 2014. Google Scholar
  12. Krishnendu Chatterjee, Thomas A. Henzinger, and Florian Horn. Finitary Winning in ω-regular Games. ACM Transactions on Computational Logic, 11(1), 2009. Google Scholar
  13. Alonzo Church. Logic, arithmetic, and automata. In Proceedings of the International Congress of Mathematicians, pages 23-35, 1962. Google Scholar
  14. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. Google Scholar
  15. E. A. Emerson, A. K. Mok, A. P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. Real-Time Systems, 4(4):331-352, 1992. Google Scholar
  16. N. Immerman. Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences, pages 384-406, 1981. URL: https://doi.org/10.1016/0022-0000(81)90039-8.
  17. Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. From liveness to promptness. Formal Methods Syst. Des., 34(2):83-103, 2009. Google Scholar
  18. Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992. Google Scholar
  19. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. Google Scholar
  20. Amir Pnueli and Roni Rosner. On the Synthesis of a Reactive Module. In Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages, POPL'89, pages 179-190, 1989. Google Scholar
  21. Michael Oser Rabin. Automata on Infinite Objects and Church’s Problem. Transactions of the American Mathematical Society, 141:1-35, 1969. Google Scholar
  22. Robert E. Tarjan. Depth first search and linear graph algorithms. SIAM J. Comput., 1(2):146-160, 1972. Google Scholar
  23. Wolfgang Thomas. Languages, Automata, and Logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 3, Beyond Words. Springer, 1997. Google Scholar
  24. Virginia Vassilevska Williams. On some fine-grained questions in algorithms and complexity. In Proceedings of the ICM, volume 3, pages 3431-3472, 2018. Google Scholar
  25. W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1-2):135-183, 1998. URL: https://doi.org/10.1016/S0304-3975(98)00009-7.
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 About DROPS Imprint Privacy Contact