We study model checking algorithms for infinite families of finite-state labeled transition systems against temporal properties written in CTL*. Such families arise, for example, as models of highly configurable systems or software product lines. We model families using context-free graph grammars. We then develop a state labeling algorithm that works compositionally on the grammar's production rules with limited information about the context in which the rule is applied. The result is a graph grammar modeling the same family but with extended labels. We leverage this grammar to decide whether all, some, or (in)finitely many members of a family satisfy a given temporal property. We have implemented our algorithms and present early experiments.

翻译：本文研究针对无限族有限状态标记转移系统的模型检验算法，这些系统需满足以CTL*书写的时序性质。此类系统族常出现于高度可配置系统或软件产品线的建模场景。我们采用上下文无关图文法对系统族进行建模，进而开发出一种状态标记算法，该算法可在仅掌握有限上下文信息的情况下，以组合方式作用于文法产生式规则。通过此算法可获得具有扩展标签的图文法，该文法仍对原系统族进行建模。我们利用该文法可判定系统族中全体、部分或（无）限多个成员是否满足给定时序性质。我们已实现相关算法并展示了初步实验结果。