Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs

Authors Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, Alexander Svozil



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.7.pdf
  • Filesize: 0.69 MB
  • 16 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
  • IST Austria, Klosterneuburg, Austria
Wolfgang Dvořák
  • Institute of Logic and Computation, TU Wien, Austria
Monika Henzinger
  • Theory and Application of Algorithms, University of Vienna, Austria
Alexander Svozil
  • Theory and Application of Algorithms, University of Vienna, Austria

Cite AsGet BibTex

Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, and Alexander Svozil. Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.7

Abstract

The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes (MDPs). A basic specification formalism in the verification of reactive systems is the strong fairness (aka Streett) objective, where given different types of requests and corresponding grants, the requirement is that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All omega-regular objectives can be expressed as Streett objectives and hence they are canonical in verification. Consider graphs/MDPs with n vertices, m edges, and a Streett objectives with k pairs, and let b denote the size of the description of the Streett objective for the sets of requests and grants. The current best-known algorithm for the problem requires time O(min(n^2, m sqrt{m log n}) + b log n). In this work we present randomized near-linear time algorithms, with expected running time O~(m + b), where the O~ notation hides poly-log factors. Our randomized algorithms are near-linear in the size of the input, and hence optimal up to poly-log factors.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial algorithms
  • Software and its engineering → Formal software verification
Keywords
  • model checking
  • graph games
  • Streett games

Metrics

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

References

  1. R. Alur and T.A. Henzinger. Computer-Aided Verification. unpublished., 2004. URL: https://web.archive.org/web/20041207121830/http://www.cis.upenn.edu/group/cis673/.
  2. C. Baier and J.P. Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. C. Beeri. On the Membership Problem for Functional and Multivalued Dependencies in Relational Databases. ACM Trans. Database Syst., 5(3):241-259, 1980. URL: http://dx.doi.org/10.1145/320613.320614.
  4. A. Bernstein, M. Probst, and C. Wulff-Nilsen. Decremental Strongly-Connected Components and Single-Source Reachability in Near-Linear Time. In STOC, pages 365-376, 2019. URL: http://dx.doi.org/10.1145/3313276.3316335.
  5. K. Chatterjee, W. Dvořák, M. Henzinger, and V. Loitzenbauer. Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction. In LICS, pages 197-206, 2016. URL: http://dx.doi.org/10.1145/2933575.2935304.
  6. K. Chatterjee, A. Gaiser, and J. Kretínský. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. In CAV, pages 559-575, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39799-8_37.
  7. K. Chatterjee and M. Henzinger. Faster and Dynamic Algorithms for Maximal End-Component Decomposition and Related Graph Problems in Probabilistic Verification. In SODA, pages 1318-1336, 2011. URL: http://dx.doi.org/10.1137/1.9781611973082.101.
  8. K. Chatterjee and M. Henzinger. An O(n²) Time Algorithm for Alternating Büchi Games. In SODA, pages 1386-1399, 2012. URL: http://portal.acm.org/citation.cfm?id=2095225&CFID=63838676&CFTOKEN=79617016.
  9. K. Chatterjee and M. Henzinger. Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition. J. ACM, 61(3):15.1-15.40, 2014. URL: http://dx.doi.org/10.1145/2597631.
  10. K. Chatterjee, M. Henzinger, and V. Loitzenbauer. Improved Algorithms for One-Pair and k-Pair Streett Objectives. In LICS, pages 269-280, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.34.
  11. K. Chatterjee, M. Henzinger, and V. Loitzenbauer. Improved Algorithms for Parity and Streett objectives. Logical Methods in Computer Science, 13(3):1-27, 2017. URL: http://dx.doi.org/10.23638/LMCS-13(3:26)2017.
  12. S. Chechik, T. D. Hansen, G. F. Italiano, J. Lacki, and N. Parotsidis. Decremental Single-Source Reachability and Strongly Connected Components in Õ(m\surdn) Total Update Time. In FOCS, pages 315-324, 2016. URL: http://dx.doi.org/10.1109/FOCS.2016.42.
  13. F. Ciesinski and C. Baier. LiQuor: A Tool for Qualitative and Quantitative Linear Time Analysis of Reactive Systems. In QEST, pages 131-132, 2006. URL: http://dx.doi.org/10.1109/QEST.2006.25.
  14. A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NUSMV: A new Symbolic Model Checker. International Journal on Software Tools for Technology Transfer (STTT), 2(4):410-425, 2000. URL: http://dx.doi.org/10.1007/s100090050046.
  15. E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999. Google Scholar
  16. C. Courcoubetis and M. Yannakakis. The Complexity of Probabilistic Verification. J. ACM, 42(4):857-907, 1995. URL: http://dx.doi.org/10.1145/210332.210339.
  17. C. Dehnert, S. Junges, J.P. Katoen, and M. Volk. A Storm is Coming: A Modern Probabilistic Model Checker. In CAV, pages 592-600, 2017. URL: http://dx.doi.org/10.1007/978-3-319-63390-9_31.
  18. J. Esparza and J. Kretínský. From LTL to Deterministic Automata: A Safraless Compositional Approach. In CAV, pages 192-208, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08867-9_13.
  19. M. Rauch Henzinger and J. A. Telle. Faster Algorithms for the Nonemptiness of Streett Automata and for Communication Protocol Pruning. In SWAT, pages 16-27, 1996. URL: http://dx.doi.org/10.1007/3-540-61422-2_117.
  20. G. J. Holzmann. The Model Checker SPIN. IEEE Trans. Softw. Eng., 23(5):279-295, 1997. URL: http://dx.doi.org/10.1109/32.588521.
  21. N. Immerman. Number of Quantifiers is Better Than Number of Tape Cells. J. Comput. Syst. Sci., 22(3):384-406, 1981. URL: http://dx.doi.org/10.1016/0022-0000(81)90039-8.
  22. Z. Komárková and J. Kretínský. Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. In ATVA, pages 235-241, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11936-6_17.
  23. M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV, pages 585-591, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22110-1_47.
  24. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Progress (Draft), 1996. URL: http://theory.stanford.edu/~zm/tvors3.html.
  25. S. Safra. On the Complexity of ω-Automata. In FOCS, pages 319-327, 1988. URL: http://dx.doi.org/10.1109/SFCS.1988.21948.
  26. R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, 1995. Google Scholar
  27. R. Tarjan. Depth-First Search and Linear Graph Algorithms. SIAM J. Comput., 1(2):146-160, 1972. Google Scholar
  28. M. Y. Vardi. Automatic Verification of Probabilistic Concurrent Finite-State Programs. In FOCS, pages 327-338, 1985. URL: http://dx.doi.org/10.1109/SFCS.1985.12.
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