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

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 s...

Descripción completa

Detalles Bibliográficos
Autores principales: Neele, Thomas, Willemse, Tim A. C., Wesselink, Wieger
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480682/
http://dx.doi.org/10.1007/978-3-030-45237-7_19
_version_ 1783580458229956608
author Neele, Thomas
Willemse, Tim A. C.
Wesselink, Wieger
author_facet Neele, Thomas
Willemse, Tim A. C.
Wesselink, Wieger
author_sort Neele, Thomas
collection PubMed
description 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 [Formula: see text]-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.
format Online
Article
Text
id pubmed-7480682
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-74806822020-09-10 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 Article 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 [Formula: see text]-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. 2020-03-13 /pmc/articles/PMC7480682/ http://dx.doi.org/10.1007/978-3-030-45237-7_19 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Neele, Thomas
Willemse, Tim A. C.
Wesselink, Wieger
Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems
title Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems
title_full Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems
title_fullStr Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems
title_full_unstemmed Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems
title_short Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems
title_sort partial-order reduction for parity games with an application on parameterised boolean equation systems
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480682/
http://dx.doi.org/10.1007/978-3-030-45237-7_19
work_keys_str_mv AT neelethomas partialorderreductionforparitygameswithanapplicationonparameterisedbooleanequationsystems
AT willemsetimac partialorderreductionforparitygameswithanapplicationonparameterisedbooleanequationsystems
AT wesselinkwieger partialorderreductionforparitygameswithanapplicationonparameterisedbooleanequationsystems

Ejemplares similares