论文标题
特色游戏
Featured Games
论文作者
论文摘要
基于功能的SPL分析和基于家庭的模型检查已经快速发展。许多模型检查问题可以简化为有限图上的两人游戏。一个突出的例子是MU-Calculus模型检查，通常是通过转化为平等游戏来完成的，但是许多定量模型检查问题也可以简化为（定量）游戏。 在他们的Fase'20论文中，Ter Beek等人\引入具有可变性的平等游戏，以开发基于家庭的MU-Calculus模型检查特色过渡系统。我们将他们的模型推广到一般特色游戏，并显示如何以家庭方式分析这些模型。 我们介绍了精选的可及性游戏，最低触及性游戏，特色折扣游戏，特色能源游戏和特色平价游戏。我们展示了如何以家庭方式计算此类游戏的获奖者和价值观。我们还表明，所有这些特色游戏都允许最佳特色策略，这些策略将为任何产品提供最佳策略。此外，我们开发了基于家庭的算法，使用后期分裂，以计算我们引入的所有特色游戏的获奖者，价值观和最佳策略。
Feature-based SPL analysis 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. In their FASE'20 paper, ter Beek et al.\ introduce parity games with variability in order to develop family-based mu-calculus model checking of featured transition systems. We generalize their model to general featured games and show how these may be analysed in a family-based manner. We introduce featured reachability games, featured minimum reachability games, featured discounted games, featured energy games, and featured parity games. We show how to compute winners and values of such games in a family-based manner. We also show that all these featured games admit optimal featured strategies, which project to optimal strategies for any product. Further, we develop family-based algorithms, using late splitting, to compute winners, values, and optimal strategies for all the featured games we have introduced.
