Featured Games

Authors

Uli Fahrenberg, Axel Legay

Journal

Science of Computer Programming

Type

article

Projects

AA"AA" is not in the list (Vaucanson, Spot, URBI, Olena, APMC, Tiger, Climb, Speaker ID, Transformers, Bison, ...) of allowed values for the "Related project" property.

Date

2022-11-01

Abstract

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.

Documents

• Paper

Bibtex (lrde.bib)

@Article{	  fahrenberg.22.scp,
  title		= {Featured Games},
  journal	= {Science of Computer Programming},
  volume	= {223},
  pages		= {102874},
  year		= {2022},
  issn		= {0167-6423},
  doi		= {https://doi.org/10.1016/j.scico.2022.102874},
  url		= {https://www.sciencedirect.com/science/article/pii/S0167642322001071},
  author	= {Uli Fahrenberg and Axel Legay},
  keywords	= {Featured transition system, Two-player game, Family-based
		  model checking},
  abstract	= {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.}
}