CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report)

TL;DR

This work develops a state labeling algorithm that works compositionally on the graph grammar's production rules with limited information about the context in which the rule is applied, resulting in a graph grammar modeling the same family but with extended labels.

Abstract

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.