Symmetry reduction in infinite games with finite branching

Abstract

Symmetry reductions have been applied extensively for the verification of finite-state concurrent systems and hardware designs using model-checking of temporal logics such as LTL, CTL and CTL ∗, as well as real-time and probabilistic-system model-checking. In this paper we extend the technique to handle infinite-state games on graphs with finite branching where the objectives of the players can be very general. As particular applications, it is shown that the technique can be applied to reduce the state space in parity games as well as when doing model-checking of the temporal logic ATL*.