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

TL;DR

This paper introduces a new model checking approach for infinite families of finite-state systems using context-free graph grammars, enabling analysis of highly configurable systems against CTL* properties.

Contribution

It develops a compositional state labeling algorithm for graph grammars representing system families, facilitating temporal property verification.

Findings

Algorithm successfully models system families with extended labels.

Decides satisfaction of properties for all, some, or finitely many family members.

Initial experiments demonstrate practical applicability.

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.