Improved algorithms for parity and Streett objectives Journal Article


Author(s): Chatterjee, Krishnendu; Henzinger, Monika; Loitzenbauer, Veronika
Article Title: Improved algorithms for parity and Streett objectives
Affiliation IST Austria
Abstract: 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(n5/2) and for (2) k-pair Streett objectives in graphs in time O(n2+nklogn). For both problems this gives faster algorithms for dense graphs and represents the first improvement in asymptotic running time in 15 years.
Keywords: synthesis; Computer-aided verification; Graph games; Parity games; Graph algorithms; Streett automata
Journal Title: Logical Methods in Computer Science
Volume: 13
Issue 3
ISSN: 1860-5974
Publisher: International Federation of Computational Logic  
Date Published: 2017-09-26
Start Page: Article number: lmcs:3953
Copyright Statement: CC BY-ND
Sponsor: WWTF grant ICT15-003 and ICT10-002; FWF: P23499-N23 and S11407-N23; ERC RiSE/SHiNE, ERC Start Grant 279307:Graph Games and FP/2007-2013/ ERC Grant Agreement no.340506; Microsoft Faculty Fellows Award
URL:
DOI: 10.23638/LMCS-13(3:26)2017
Open access: yes (OA journal)
IST Austria Authors
Related IST Austria Work