Parity game reductions

S. Cranen, J.J.A. Keiren, T.A.C. Willemse

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

Parity games play a central role in model checking and satisfiability checking. Solving parity games is computationally expensive, among others due to the size of the games, which, for model checking problems, can easily contain 109 vertices or beyond. Equivalence relations can be used to reduce the size of a parity game, thereby potentially alleviating part of the computational burden. We reconsider (governed) bisimulation and (governed) stuttering bisimulation, and we give detailed proofs that these relations are equivalences, have unique quotients and they approximate the winning regions of parity games. Furthermore, we present game-based characterisations of these relations. Using these characterisations our equivalences are compared to relations for parity games that can be found in the literature, such as direct simulation equivalence and delayed simulation equivalence. To complete the overview we develop coinductive characterisations of direct- and delayed simulation equivalence and we establish a lattice of equivalences for parity games.
Original languageEnglish
Pages (from-to)401-444
Number of pages44
JournalActa Informatica
Volume55
Issue number5
DOIs
Publication statusPublished - Aug 2018

Fingerprint

Model checking

Keywords

  • parity games
  • model checking
  • formal methods
  • bisimulation
  • SIMULATION RELATIONS
  • MODEL-CHECKING
  • BOOLEAN EQUATION SYSTEMS
  • BRANCHING BISIMILARITY
  • INFINITE GAMES
  • BUCHI AUTOMATA
  • GRAPHS

Cite this

Cranen, S. ; Keiren, J.J.A. ; Willemse, T.A.C. / Parity game reductions. In: Acta Informatica. 2018 ; Vol. 55, No. 5. pp. 401-444.
@article{9ed7bda5ef45434c82b85e3b12a21674,
title = "Parity game reductions",
abstract = "Parity games play a central role in model checking and satisfiability checking. Solving parity games is computationally expensive, among others due to the size of the games, which, for model checking problems, can easily contain 109 vertices or beyond. Equivalence relations can be used to reduce the size of a parity game, thereby potentially alleviating part of the computational burden. We reconsider (governed) bisimulation and (governed) stuttering bisimulation, and we give detailed proofs that these relations are equivalences, have unique quotients and they approximate the winning regions of parity games. Furthermore, we present game-based characterisations of these relations. Using these characterisations our equivalences are compared to relations for parity games that can be found in the literature, such as direct simulation equivalence and delayed simulation equivalence. To complete the overview we develop coinductive characterisations of direct- and delayed simulation equivalence and we establish a lattice of equivalences for parity games.",
keywords = "parity games, model checking, formal methods, bisimulation, SIMULATION RELATIONS, MODEL-CHECKING, BOOLEAN EQUATION SYSTEMS, BRANCHING BISIMILARITY, INFINITE GAMES, BUCHI AUTOMATA, GRAPHS",
author = "S. Cranen and J.J.A. Keiren and T.A.C. Willemse",
year = "2018",
month = "8",
doi = "10.1007/s00236-017-0301-x",
language = "English",
volume = "55",
pages = "401--444",
journal = "Acta Informatica",
issn = "0001-5903",
publisher = "Springer New York",
number = "5",

}

Cranen, S, Keiren, JJA & Willemse, TAC 2018, 'Parity game reductions', Acta Informatica, vol. 55, no. 5, pp. 401-444. https://doi.org/10.1007/s00236-017-0301-x

Parity game reductions. / Cranen, S.; Keiren, J.J.A.; Willemse, T.A.C.

In: Acta Informatica, Vol. 55, No. 5, 08.2018, p. 401-444.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Parity game reductions

AU - Cranen, S.

AU - Keiren, J.J.A.

AU - Willemse, T.A.C.

PY - 2018/8

Y1 - 2018/8

N2 - Parity games play a central role in model checking and satisfiability checking. Solving parity games is computationally expensive, among others due to the size of the games, which, for model checking problems, can easily contain 109 vertices or beyond. Equivalence relations can be used to reduce the size of a parity game, thereby potentially alleviating part of the computational burden. We reconsider (governed) bisimulation and (governed) stuttering bisimulation, and we give detailed proofs that these relations are equivalences, have unique quotients and they approximate the winning regions of parity games. Furthermore, we present game-based characterisations of these relations. Using these characterisations our equivalences are compared to relations for parity games that can be found in the literature, such as direct simulation equivalence and delayed simulation equivalence. To complete the overview we develop coinductive characterisations of direct- and delayed simulation equivalence and we establish a lattice of equivalences for parity games.

AB - Parity games play a central role in model checking and satisfiability checking. Solving parity games is computationally expensive, among others due to the size of the games, which, for model checking problems, can easily contain 109 vertices or beyond. Equivalence relations can be used to reduce the size of a parity game, thereby potentially alleviating part of the computational burden. We reconsider (governed) bisimulation and (governed) stuttering bisimulation, and we give detailed proofs that these relations are equivalences, have unique quotients and they approximate the winning regions of parity games. Furthermore, we present game-based characterisations of these relations. Using these characterisations our equivalences are compared to relations for parity games that can be found in the literature, such as direct simulation equivalence and delayed simulation equivalence. To complete the overview we develop coinductive characterisations of direct- and delayed simulation equivalence and we establish a lattice of equivalences for parity games.

KW - parity games

KW - model checking

KW - formal methods

KW - bisimulation

KW - SIMULATION RELATIONS

KW - MODEL-CHECKING

KW - BOOLEAN EQUATION SYSTEMS

KW - BRANCHING BISIMILARITY

KW - INFINITE GAMES

KW - BUCHI AUTOMATA

KW - GRAPHS

U2 - 10.1007/s00236-017-0301-x

DO - 10.1007/s00236-017-0301-x

M3 - Article

VL - 55

SP - 401

EP - 444

JO - Acta Informatica

JF - Acta Informatica

SN - 0001-5903

IS - 5

ER -