Submodel Enumeration for CTL Is Hard

verfasst von

Nicolas Fröhlich, Arne Meier

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.

Organisationseinheit(en)

Institut für Theoretische Informatik

Typ

Aufsatz in Konferenzband

Seiten

10517-10524

Anzahl der Seiten

8

Publikationsdatum

25.04.2024

Publikationsstatus

Veröffentlicht

Peer-reviewed

Ja

ASJC Scopus Sachgebiete

Artificial intelligence

Elektronische Version(en)

https://doi.org/10.48550/arXiv.2312.09868 (Zugang: Offen)
https://doi.org/10.1609/aaai.v38i9.28921 (Zugang: Geschlossen)