Partial-order reduction for parity games and parameterised Boolean equation systems
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
© The Author(s) 2022
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.
Publication in research information system
MetadataShow full item record
Showing items with similar title or keywords.
Neele, Thomas; Valmari, Antti; Willemse, Tim A. C (Springer, 2020)In model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One ...
A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction Neele, Thomas; Valmari, Antti; Willemse, Tim A. C. (Logical Methods in Computer Science e.V., 2021)One of the most popular state-space reduction techniques for model checking is partial-order reduction (POR). Of the many different POR implementations, stubborn sets are a very versatile variant and have thus seen many ...
Valmari, Antti; Vogler, Walter (IOS Press, 2021)Many partial order methods use some special condition for ensuring that the analysis is not terminated prematurely. In the case of stubborn set methods for safety properties, implementation of the condition is usually based ...
On solving separable block tridiagonal linear systems using a GPU implementation of radix-4 PSCR method Myllykoski, Mirko; Rossi, Tuomo; Toivanen, Jari (Academic Press, 2018)Partial solution variant of the cyclic reduction (PSCR) method is a direct solver that can be applied to certain types of separable block tridiagonal linear systems. Such linear systems arise, e.g., from the Poisson and ...
Analysis of errors caused by incomplete knowledge of material data in mathematical models of elastic media Mali, Olli (University of Jyväskylä, 2011)