Model checking approaches to software product lines are doubly cursed. Not only high-dimensionality regarding the number of states may be troublesome, also the exponential number of options for a product raises a computational hindrance. In order to mitigate the latter, family-based verification, as opposed to product-based verification, has been proposed.

In this talk we consider so-called variability parity games (VPGs). Given a set of possible options, VPGs aggregate a corresponding set of parity games. We discuss how the well-known recursive algorithm to solve standard parity games attributed to Zielonka can be adapted to deal with VPGs. Experiments indicate that family-based verification based on VPGs outperforms product-based verification based on parity games. In a search for an explanation of this we conjecture a relationship between the number of recursive calls in Zielonka’s algorithm for the case of a VPG vs. the parity games its consists of.

Joint work with Maurice ter Beek (CNR/ISTI Pisa) and Tim Willemse.