Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems

Thomas Neele; Tim A.C. Willemse; Wieger Wesselink

doi:10.1007/978-3-030-45237-7_19

Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems

Thomas Neele, Tim A.C. Willemse, Wieger Wesselink

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

3 Citations (Scopus)

Abstract

Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal μ-calculus. Our technique is applied to, and implemented for the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments indicate that substantial reductions can be achieved.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II
Editors	Armin Biere, David Parker
Publisher	Springer
Pages	307-324
Number of pages	18
ISBN (Print)	9783030452360
DOIs	https://doi.org/10.1007/978-3-030-45237-7_19
Publication status	Published - 17 Apr 2020
Event	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland Duration: 25 Apr 2020 → 30 Apr 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12079 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Country/Territory	Ireland
City	Dublin
Period	25/04/20 → 30/04/20

Access to Document

10.1007/978-3-030-45237-7_19

Cite this

Neele, T., Willemse, T. A. C., & Wesselink, W. (2020). Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems. In A. Biere, & D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II (pp. 307-324). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12079 LNCS). Springer. https://doi.org/10.1007/978-3-030-45237-7_19

Neele, Thomas ; Willemse, Tim A.C. ; Wesselink, Wieger. / Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems. Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. editor / Armin Biere ; David Parker. Springer, 2020. pp. 307-324 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{00298b51ea574110b0fa910400354beb,

title = "Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems",

abstract = "Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal μ-calculus. Our technique is applied to, and implemented for the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments indicate that substantial reductions can be achieved.",

author = "Thomas Neele and Willemse, {Tim A.C.} and Wieger Wesselink",

year = "2020",

month = apr,

day = "17",

doi = "10.1007/978-3-030-45237-7_19",

language = "English",

isbn = "9783030452360",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "307--324",

editor = "Armin Biere and David Parker",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II",

address = "Germany",

note = "26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",

}

Neele, T , Willemse, TAC & Wesselink, W 2020, Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems. in A Biere & D Parker (eds), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12079 LNCS, Springer, pp. 307-324, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 25/04/20. https://doi.org/10.1007/978-3-030-45237-7_19

Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems. / Neele, Thomas ; Willemse, Tim A.C.; Wesselink, Wieger.
Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. ed. / Armin Biere; David Parker. Springer, 2020. p. 307-324 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12079 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems

AU - Neele, Thomas

AU - Willemse, Tim A.C.

AU - Wesselink, Wieger

PY - 2020/4/17

Y1 - 2020/4/17

N2 - Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal μ-calculus. Our technique is applied to, and implemented for the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments indicate that substantial reductions can be achieved.

AB - Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal μ-calculus. Our technique is applied to, and implemented for the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments indicate that substantial reductions can be achieved.

UR - http://www.scopus.com/inward/record.url?scp=85083969506&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-45237-7_19

DO - 10.1007/978-3-030-45237-7_19

M3 - Conference contribution

AN - SCOPUS:85083969506

SN - 9783030452360

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 307

EP - 324

BT - Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II

A2 - Biere, Armin

A2 - Parker, David

PB - Springer

T2 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020

Y2 - 25 April 2020 through 30 April 2020

ER -

Neele T , Willemse TAC , Wesselink W. Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems. In Biere A, Parker D, editors, Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. Springer. 2020. p. 307-324. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-45237-7_19

Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Dataset with experiments for 'Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems'

Cite this

Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Datasets

Dataset with experiments for 'Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems'

Cite this