Submodel Enumeration for CTL Is Hard

TL;DR

This paper proves that enumerating submodels satisfying CTL formulas is computationally hard in general, but identifies specific fragments where efficient enumeration is possible.

Contribution

It establishes the complexity of model enumeration for CTL and introduces restricted fragments that enable faster enumeration algorithms.

Findings

Model enumeration for CTL is computationally hard in general.

Certain fragments with restricted Boolean functions allow for efficient enumeration.

The work delineates the boundary between hard and tractable cases in CTL model enumeration.

Abstract

Expressing system specifications using Computation Tree Logic (CTL) formulas, formalising programs using Kripke structures, and then model checking the system is an established workflow in program verification and has wide applications in AI. In this paper, we consider the task of model enumeration, which asks for a uniform stream of output systems that satisfy the given specification. We show that, given a CTL formula and a system (potentially falsified by the formula), enumerating satisfying submodels is always hard for CTL - regardless of which subset of CTL operators is considered. As a silver lining on the horizon, we present fragments via restrictions on the allowed Boolean functions that still allow for fast enumeration.