The following paper has been published in Science of Computer Programming:
Featured Games
Uli Fahrenberg, Axel Legay
Feature-based analysis of software product lines and family-based model
checking have seen rapid development. Many model checking problems can be
reduced to two-player games on finite graphs. A prominent example is
mu-calculus model checking, which is generally done by translating to parity
games, but also many quantitative model-checking problems can be reduced to
(quantitative) games. As part of a program to make game-based model checking
available for software product lines, we introduce featured reachability
games, featured minimum reachability games, featured discounted games,
featured energy games, and featured parity games. We show that all these
admit optimal featured strategies, which project to optimal strategies for
any product, and how to compute winners and values of such games in a
family-based manner.
https://www.lrde.epita.fr/wiki/Publications/fahrenberg.22.scp