Improved algorithms for parity and Streett objectives

Chatterjee, Krishnendu; Henzinger, Monika H; Loitzenbauer, Veronika

Improved algorithms for parity and Streett objectives

Chatterjee K, Henzinger MH, Loitzenbauer V. 2017. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 13(3), 26.

Download

IST-2018-956-v1+1_2017_Chatterjee_Improved_algorithms.pdf 582.94 KB [Published Version]

DOI

10.23638/LMCS-13(3:26)2017

Journal Article | Published | English

Scopus indexed

Author

Chatterjee, Krishnendu^ISTA ; Henzinger, Monika^ISTA ; Loitzenbauer, Veronika

Department

Chatterjee Group

Grant

Modern Graph Algorithmic Techniques in Formal Verification
Game Theory
Efficient Algorithms for Computer Aided Verification
Quantitative Graph Games: Theory and Applications

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.

Publishing Year

2017

Date Published

2017-09-26

Journal Title

Logical Methods in Computer Science

Publisher

International Federation of Computational Logic

Volume

Issue

Article Number

ISSN

1860-5974

IST-REx-ID

464

Cite this

Chatterjee K, Henzinger MH, Loitzenbauer V. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 2017;13(3). doi:10.23638/LMCS-13(3:26)2017

Chatterjee, K., Henzinger, M. H., & Loitzenbauer, V. (2017). Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(3:26)2017

Chatterjee, Krishnendu, Monika H Henzinger, and Veronika Loitzenbauer. “Improved Algorithms for Parity and Streett Objectives.” Logical Methods in Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(3:26)2017.

K. Chatterjee, M. H. Henzinger, and V. Loitzenbauer, “Improved algorithms for parity and Streett objectives,” Logical Methods in Computer Science, vol. 13, no. 3. International Federation of Computational Logic, 2017.

Chatterjee K, Henzinger MH, Loitzenbauer V. 2017. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 13(3), 26.

Chatterjee, Krishnendu, et al. “Improved Algorithms for Parity and Streett Objectives.” Logical Methods in Computer Science, vol. 13, no. 3, 26, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(3:26)2017.

All files available under the following license(s):

Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0):