conference paper published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Wolfgang Dvorák author Monika H Henzinger author 540c9bbd-f2de-11ec-812d-d04a5be856300000-0002-5008-6530 Alexander Svozil author KrCh department CONCUR: Conference on Concurrency Theory Game Theory project Quantitative Graph Games: Theory and Applications project 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. https://research-explorer.ista.ac.at/download/6887/6922/2019_LIPIcs_Chatterjee.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ Schloss Dagstuhl - Leibniz-Zentrum für Informatik2019Amsterdam, Netherlands eng 10.4230/LIPICS.CONCUR.2019.7 140 Chatterjee, K., Dvorák, W., Henzinger, M., &#38; Svozil, A. (2019). Near-linear time algorithms for Streett objectives in graphs and MDPs. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 140). Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPICS.CONCUR.2019.7">https://doi.org/10.4230/LIPICS.CONCUR.2019.7</a> Chatterjee, Krishnendu, et al. “Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs.” <i>Leibniz International Proceedings in Informatics</i>, vol. 140, 7, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:<a href="https://doi.org/10.4230/LIPICS.CONCUR.2019.7">10.4230/LIPICS.CONCUR.2019.7</a>. K. Chatterjee, W. Dvorák, M. Henzinger, A. Svozil, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. K. Chatterjee, W. Dvorák, M. Henzinger, and A. Svozil, “Near-linear time algorithms for Streett objectives in graphs and MDPs,” in <i>Leibniz International Proceedings in Informatics</i>, Amsterdam, Netherlands, 2019, vol. 140. Chatterjee, Krishnendu, Wolfgang Dvorák, Monika Henzinger, and Alexander Svozil. “Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. <a href="https://doi.org/10.4230/LIPICS.CONCUR.2019.7">https://doi.org/10.4230/LIPICS.CONCUR.2019.7</a>. Chatterjee K, Dvorák W, Henzinger M, Svozil A. Near-linear time algorithms for Streett objectives in graphs and MDPs. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:<a href="https://doi.org/10.4230/LIPICS.CONCUR.2019.7">10.4230/LIPICS.CONCUR.2019.7</a> Chatterjee K, Dvorák W, Henzinger M, Svozil A. 2019. Near-linear time algorithms for Streett objectives in graphs and MDPs. Leibniz International Proceedings in Informatics. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 140, 7. 68872019-09-18T08:07:58Z2025-07-10T11:53:59Z