Details
| Originalsprache | Englisch |
|---|---|
| Titel des Sammelwerks | AiML |
| Herausgeber/-innen | David Fernandez-Duque, Alessandra Palmigiano, Alessandra Palmigiano, Sophie Pinchinat |
| Seiten | 391-406 |
| Seitenumfang | 16 |
| ISBN (elektronisch) | 9781848904132 |
| Publikationsstatus | Veröffentlicht - 2022 |
Publikationsreihe
| Name | Advances in Modal Logic |
|---|---|
| Band | 14 |
Abstract
Enumeration complexity (Johnson et al. 1988) is about finding algorithms that produce all solutions to a given problem. Moreover, one strives for a stream of solutions that should be as uniform as possible without much waiting time in between two output solutions and avoiding duplicates. In this paper, we study the problem of model checking in modal logic from this point of view. We consider a particular submodel satisfaction relation that keeps the reference to the transition relation of the original model. Then, we distinguish between enumerating subtrees and subgraphs of Kripke structures that satisfy a modal logic formula. We devise enumeration algorithms for both problems that sort them into the class DelayP.
ASJC Scopus Sachgebiete
- Mathematik (insg.)
- Computational Mathematics
- Mathematik (insg.)
- Logik
- Informatik (insg.)
- Theoretische Informatik und Mathematik
Zitieren
- Standard
- Harvard
- Apa
- Vancouver
- BibTex
- RIS
AiML. Hrsg. / David Fernandez-Duque; Alessandra Palmigiano; Alessandra Palmigiano; Sophie Pinchinat. 2022. S. 391-406 (Advances in Modal Logic; Band 14).
Publikation: Beitrag in Buch/Bericht/Sammelwerk/Konferenzband › Aufsatz in Konferenzband › Forschung › Peer-Review
}
TY - GEN
T1 - Submodel Enumeration of Kripke Structures in Modal Logic
AU - Fröhlich, Nicolas
AU - Meier, Arne
N1 - Publisher Copyright: © 2022 College Publications. All rights reserved.
PY - 2022
Y1 - 2022
N2 - Enumeration complexity (Johnson et al. 1988) is about finding algorithms that produce all solutions to a given problem. Moreover, one strives for a stream of solutions that should be as uniform as possible without much waiting time in between two output solutions and avoiding duplicates. In this paper, we study the problem of model checking in modal logic from this point of view. We consider a particular submodel satisfaction relation that keeps the reference to the transition relation of the original model. Then, we distinguish between enumerating subtrees and subgraphs of Kripke structures that satisfy a modal logic formula. We devise enumeration algorithms for both problems that sort them into the class DelayP.
AB - Enumeration complexity (Johnson et al. 1988) is about finding algorithms that produce all solutions to a given problem. Moreover, one strives for a stream of solutions that should be as uniform as possible without much waiting time in between two output solutions and avoiding duplicates. In this paper, we study the problem of model checking in modal logic from this point of view. We consider a particular submodel satisfaction relation that keeps the reference to the transition relation of the original model. Then, we distinguish between enumerating subtrees and subgraphs of Kripke structures that satisfy a modal logic formula. We devise enumeration algorithms for both problems that sort them into the class DelayP.
KW - DelayP
KW - Enumeration Complexity
KW - Kripke Structures
KW - Modal Logic
UR - http://www.scopus.com/inward/record.url?scp=85180562844&partnerID=8YFLogxK
M3 - Conference contribution
T3 - Advances in Modal Logic
SP - 391
EP - 406
BT - AiML
A2 - Fernandez-Duque, David
A2 - Palmigiano, Alessandra
A2 - Palmigiano, Alessandra
A2 - Pinchinat, Sophie
ER -