Krishnendu Chatterjee ; Monika Henzinger ; Veronika Loitzenbauer - Improved Algorithms for Parity and Streett objectives

lmcs:3953 - Logical Methods in Computer Science, September 26, 2017, Volume 13, Issue 3 - https://doi.org/10.23638/LMCS-13(3:26)2017
Improved Algorithms for Parity and Streett objectivesArticle

Authors: Krishnendu Chatterjee ; Monika Henzinger ; Veronika Loitzenbauer

    The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formedness of specifications, and the synthesis of reactive systems. We show how to compute the winning set on $n$ vertices for (1) parity-3 (aka one-pair Streett) objectives in game graphs in time $O(n^{5/2})$ and for (2) k-pair Streett objectives in graphs in time $O(n^2 + nk \log n)$. For both problems this gives faster algorithms for dense graphs and represents the first improvement in asymptotic running time in 15 years.

    https://doi.org/10.23638/LMCS-13(3:26)2017
    Source: arXiv.org:1410.0833
    Volume: Volume 13, Issue 3
    Published on: September 26, 2017
    Accepted on: September 26, 2017
    Submitted on: September 26, 2017
    Keywords: Computer Science - Data Structures and Algorithms,Computer Science - Logic in Computer Science,F.2.2,F.3.1
    Licence: arXiv.org - Non-exclusive license to distribute
    Funding:
      Source : OpenAIRE Graph
    • Modern Graph Algorithmic Techniques in Formal Verification; Code: P 23499
    • Quantitative Graph Games: Theory and Applications; Funder: European Commission; Code: 279307
    • Challenges in Graph Algorithms with Applications; Funder: European Commission; Code: 340506

    Share and export

    Consultation statistics

    This page has been seen 1779 times.
    This article's PDF has been downloaded 374 times.