A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
Partial-order reduction for parity games and parameterised Boolean equation systems (2022)
Neele, T., Willemse, T. A. C., Wesselink, W., & Valmari, A. (2022). Partial-order reduction for parity games and parameterised Boolean equation systems. International Journal on Software Tools for Technology Transfer, 24(5), 735-756. https://doi.org/10.1007/s10009-022-00672-0
JYU-tekijät tai -toimittajat
Julkaisun tiedot
Julkaisun kaikki tekijät tai toimittajat: Neele, Thomas; Willemse, Tim A. C.; Wesselink, Wieger; Valmari, Antti
Lehti tai sarja: International Journal on Software Tools for Technology Transfer
ISSN: 1433-2779
eISSN: 1433-2787
Julkaisuvuosi: 2022
Ilmestymispäivä: 02.10.2022
Volyymi: 24
Lehden numero: 5
Artikkelin sivunumerot: 735-756
Kustantaja: Springer
Julkaisumaa: Saksa
Julkaisun kieli: englanti
DOI: https://doi.org/10.1007/s10009-022-00672-0
Julkaisun avoin saatavuus: Avoimesti saatavilla
Julkaisukanavan avoin saatavuus: Osittain avoin julkaisukanava
Julkaisu on rinnakkaistallennettu (JYX): https://jyx.jyu.fi/handle/123456789/83478
Tiivistelmä
In model checking, reduction techniques can be helpful tools to fight the state-space explosion problem. Partial-order reduction (POR) is a well-known example, and many POR variants have been developed over the years. However, none of these can be used in the context of model checking stutter-sensitive temporal properties. We propose POR techniques for parity games, a well-established formalism for solving a variety of decision problems, including model checking. As a result, we obtain the first POR method that is sound for the full modal μ-calculus. We show how our technique can be applied to the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments with our implementation indicate that substantial reductions can be achieved.
YSO-asiasanat: tietojenkäsittely; verifiointi; Boolen algebra; peliteoria
Vapaat asiasanat: partial-order reduction; parity games; parameterised Boolean equation systems; stubborn sets
Liittyvät organisaatiot
OKM-raportointi: Kyllä
Raportointivuosi: 2022
JUFO-taso: 1
