## 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

**Submodel Enumeration of Kripke Structures in Modal Logic.**/ Fröhlich, Nicolas; Meier, Arne.

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

*AiML.*Advances in Modal Logic, vol. 14, pp. 391-406.

*AiML*(pp. 391-406). (Advances in Modal Logic; Vol. 14).

}

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 -