Details
| Originalsprache | Englisch |
|---|---|
| Titel des Sammelwerks | Proceedings of the AAAI Conference on Artificial Intelligence |
| Herausgeber/-innen | Michael Wooldridge, Jennifer Dy, Sriraam Natarajan |
| Seiten | 10517-10524 |
| Seitenumfang | 8 |
| Auflage | 9 |
| Publikationsstatus | Veröffentlicht - 25 Apr. 2024 |
Publikationsreihe
| Name | AAAI-24 Technical Tracks |
|---|---|
| Nummer | 9 |
| Band | 38 |
| ISSN (Print) | 2159-5399 |
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
- Informatik (insg.)
- Artificial intelligence
Zitieren
- Standard
- Harvard
- Apa
- Vancouver
- BibTex
- RIS
Proceedings of the AAAI Conference on Artificial Intelligence. Hrsg. / Michael Wooldridge; Jennifer Dy; Sriraam Natarajan. 9. Aufl. 2024. S. 10517-10524 (AAAI-24 Technical Tracks; Band 38, Nr. 9).
Publikation: Beitrag in Buch/Bericht/Sammelwerk/Konferenzband › Aufsatz in Konferenzband › Forschung › Peer-Review
}
TY - GEN
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 contribution
T3 - AAAI-24 Technical Tracks
SP - 10517
EP - 10524
BT - Proceedings of the AAAI Conference on Artificial Intelligence
A2 - Wooldridge, Michael
A2 - Dy, Jennifer
A2 - Natarajan, Sriraam
ER -