Family-based model checking for Software Product Lines (SPLs) concerns the simultaneous verification of multiple product models. This approach to verification is based on the hypothesis that commonalities among different products in an SPL can be exploited to improve over a naive product-based verification, in which each product is model checked independently. Variability Parity Games (VPGs) [1] have been proposed as a formalism that can be used to encode and answer family-based model checking problems. These VPGs extend parity games with conditional edges labelled with configurations. The encoding of the family-based model checking problem is detailed in [1,2], along with two algorithms for solving VPGs, viz., a recursive algorithm [1,2] and an algorithm based on fixed point iteration [2]. These algorithms exploit BDDs to symbolically represent the families that are dynamically manipulated and uncovered in computations.

In [3], a third algorithm, based on Jurdzinski's small progress measures, was coined, along with algorithms for reachability games, minimum reachability games, discounted games and energy games. These algorithms, however, have not been implemented and compared to those of [1,2]. In this assignment, you're asked to investigate which of the algorithms perform best in practice, or under which circumstances. As a starting point, the code of [2] can be used. Time permitting, new algorithms can be implemented and compared. The assignment is to be carried out under the supervision of dr. Willemse and can be conducted in close collaboration with the authors of [1] and [3], and a research visit to one of the involved institutes abroad might be an option in case the situation at that moment would allow so.

[1] Maurice H. ter Beek, Sjef van Loo, Erik de Vink, and Tim Willemse. Family-Based SPL Model Checking Using Parity Games with Variability. In FASE 2020. https://doi.org/10.1007/978-3-030-45234-6_12

[2] Sjef van Loo.  Verifying SPLs using parity games expressing variability. MSc thesis TU/e. https://www.win.tue.nl/~timw/downloads/VanLoo_thesis.pdf

[3] Uli Fahrenberg and Axel Legay. Featured Games. Submitted for publication. https://arxiv.org/pdf/2005.05666.pdf