Loading [MathJax]/extensions/tex2jax.js

Submodel Enumeration for CTL Is Hard

Publikation: Beitrag in FachzeitschriftKonferenzaufsatz in FachzeitschriftForschungPeer-Review

Autorschaft

Details

OriginalspracheEnglisch
Seiten (von - bis)10517-10524
Seitenumfang8
FachzeitschriftProceedings of the AAAI Conference on Artificial Intelligence
Jahrgang38
Ausgabenummer9
PublikationsstatusVeröffentlicht - 25 Apr. 2024

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.

ASJC Scopus Sachgebiete

Zitieren

Submodel Enumeration for CTL Is Hard. / Fröhlich, Nicolas; Meier, Arne.
in: Proceedings of the AAAI Conference on Artificial Intelligence, Jahrgang 38, Nr. 9, 25.04.2024, S. 10517-10524.

Publikation: Beitrag in FachzeitschriftKonferenzaufsatz in FachzeitschriftForschungPeer-Review

Fröhlich, N & Meier, A 2024, 'Submodel Enumeration for CTL Is Hard', Proceedings of the AAAI Conference on Artificial Intelligence, Jg. 38, Nr. 9, S. 10517-10524. https://doi.org/10.1609/aaai.v38i9.28921, https://doi.org/10.48550/arXiv.2312.09868
Fröhlich, N., & Meier, A. (2024). Submodel Enumeration for CTL Is Hard. Proceedings of the AAAI Conference on Artificial Intelligence, 38(9), 10517-10524. https://doi.org/10.1609/aaai.v38i9.28921, https://doi.org/10.48550/arXiv.2312.09868
Fröhlich N, Meier A. Submodel Enumeration for CTL Is Hard. Proceedings of the AAAI Conference on Artificial Intelligence. 2024 Apr 25;38(9):10517-10524. doi: 10.1609/aaai.v38i9.28921, 10.48550/arXiv.2312.09868
Fröhlich, Nicolas ; Meier, Arne. / Submodel Enumeration for CTL Is Hard. in: Proceedings of the AAAI Conference on Artificial Intelligence. 2024 ; Jahrgang 38, Nr. 9. S. 10517-10524.
Download
@article{9371e77ae13749cfbcc9508b4e3ee456,
title = "Submodel Enumeration for CTL Is Hard",
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.",
author = "Nicolas Fr{\"o}hlich and Arne Meier",
note = "Publisher Copyright: Copyright {\textcopyright} 2024, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.",
year = "2024",
month = apr,
day = "25",
doi = "10.1609/aaai.v38i9.28921",
language = "English",
volume = "38",
pages = "10517--10524",
number = "9",

}

Download

TY - JOUR

T1 - Submodel Enumeration for CTL Is Hard

AU - Fröhlich, Nicolas

AU - Meier, Arne

N1 - Publisher Copyright: Copyright © 2024, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

PY - 2024/4/25

Y1 - 2024/4/25

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85189321591&partnerID=8YFLogxK

U2 - 10.1609/aaai.v38i9.28921

DO - 10.1609/aaai.v38i9.28921

M3 - Conference article

VL - 38

SP - 10517

EP - 10524

JO - Proceedings of the AAAI Conference on Artificial Intelligence

JF - Proceedings of the AAAI Conference on Artificial Intelligence

SN - 2159-5399

IS - 9

ER -

Von denselben Autoren