Solving parity games is a core problem in formal verification, specifically when using model checking and synthesis methods, which have several industrial-scale applications. In this paper, we propose a constraint-based approach for parity games, built upon a new propagation algorithm that eliminates opponent cycles from the game graph. This approach results in an efficient method that exploits the duality between the players in a parity game. Our implementation within a Lazy Clause Generation framework outperforms all existing constraint-based methods for parity games and performs competitively against the most specialized non-CP-based algorithms—often matching and sometimes exceeding their performance—while retaining the flexibility inherent to general constraint-based approaches. Since new constraints can be easily added, our method provides a flexible framework for refining existing problem formulations to search for preferred solutions by satisfying additional constraints. This feature can also be used to solve parity games where additional quantitative constraints (e.g., cost or resource-bounded requirements) need to be satisfied. We present the theoretical foundations of the approach, an experimental evaluation, and a discussion of the results, including an analysis of different versions of the new propagator.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

No-Opponent-Cycle Propagators for Solving Parity Games

  • Gonzalo Hernandez,
  • Julian Garcia,
  • Julian Gutierrez,
  • Guido Tack

摘要

Solving parity games is a core problem in formal verification, specifically when using model checking and synthesis methods, which have several industrial-scale applications. In this paper, we propose a constraint-based approach for parity games, built upon a new propagation algorithm that eliminates opponent cycles from the game graph. This approach results in an efficient method that exploits the duality between the players in a parity game. Our implementation within a Lazy Clause Generation framework outperforms all existing constraint-based methods for parity games and performs competitively against the most specialized non-CP-based algorithms—often matching and sometimes exceeding their performance—while retaining the flexibility inherent to general constraint-based approaches. Since new constraints can be easily added, our method provides a flexible framework for refining existing problem formulations to search for preferred solutions by satisfying additional constraints. This feature can also be used to solve parity games where additional quantitative constraints (e.g., cost or resource-bounded requirements) need to be satisfied. We present the theoretical foundations of the approach, an experimental evaluation, and a discussion of the results, including an analysis of different versions of the new propagator.