Details
| Original language | English |
|---|---|
| Title of host publication | AiML |
| Editors | David Fernandez-Duque, Alessandra Palmigiano, Alessandra Palmigiano, Sophie Pinchinat |
| Pages | 391-406 |
| Number of pages | 16 |
| ISBN (electronic) | 9781848904132 |
| Publication status | Published - 2022 |
Publication series
| Name | Advances in Modal Logic |
|---|---|
| Volume | 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.
Keywords
- DelayP, Enumeration Complexity, Kripke Structures, Modal Logic
ASJC Scopus subject areas
- Mathematics(all)
- Computational Mathematics
- Mathematics(all)
- Logic
- Computer Science(all)
- Computational Theory and Mathematics
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
AiML. ed. / David Fernandez-Duque; Alessandra Palmigiano; Alessandra Palmigiano; Sophie Pinchinat. 2022. p. 391-406 (Advances in Modal Logic; Vol. 14).
Research output: Chapter in book/report/conference proceeding › Conference contribution › Research › 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 -