Tim Willemse: Variability Parity Games


Event Details


Parity games are two-player, infinite duration games that can be used answer whether a property holds true of a system with a yes or no. In several application domains, one is not only interested in a yes/no answer, but in computing some/all values to parameters in a system description for which a property holds true. A naive approach to this problem involves solving many parity games. In the hope of taking advantage of structural commonalities among a collection of games, thus avoiding many unnecessary computations, we introduce variability parity games as a generalisation of parity games. We will briefly discuss an algorithm that directly solves such variability parity games. As a motivation for, and an application of the developed theory, we suggest how it can be used in the setting of Software Product Lines for modal mu-calculus model checking for Featured Transition Systems. This is very much work in (slow) progress…