---
res:
  bibo_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. @eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Krishnendu
      foaf_name: Chatterjee, Krishnendu
      foaf_surname: Chatterjee
      foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4561-241X
  - foaf_Person:
      foaf_givenName: Wolfgang
      foaf_name: Dvorák, Wolfgang
      foaf_surname: Dvorák
  - foaf_Person:
      foaf_givenName: Monika H
      foaf_name: Henzinger, Monika H
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=540c9bbd-f2de-11ec-812d-d04a5be85630
    orcid: 0000-0002-5008-6530
  - foaf_Person:
      foaf_givenName: Alexander
      foaf_name: Svozil, Alexander
      foaf_surname: Svozil
  bibo_doi: 10.4230/LIPICS.CONCUR.2019.7
  bibo_volume: 140
  dct_date: 2019^xs_gYear
  dct_language: eng
  dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
  dct_title: Near-linear time algorithms for Streett objectives in graphs and MDPs@
...