### Abstract

In this work we present a model-checking algorithm for a multiagent epistemic logic contain- ing operators for common and distributed knowledge. The model-checker is developed as a function directly from the semantics of the logic, in a style that could be applied straight- forwardly to derive model-checkers for other logics. Secondly, we consider how to abstract the model-checker using abstract interpretation, yielding a procedure applicable to infinite models. The abstract model-checker allows model-checking with infinite-state models. When applied to the problem of whether M |= φ, it terminates and returns the set of states in M at which φ might hold. If the set is empty, then M definitely does not satisfy φ, while if the set is non-empty then M possibly satisfies φ.

Original language | English |
---|---|

Publication date | Aug 2012 |

Number of pages | 3 |

Publication status | Published - Aug 2012 |

Event | 8th Scandinavian Logic Symposium - RUC, Roskilde, Denmark Duration: 20 Aug 2012 → 21 Aug 2012 http://scandinavianlogic.weebly.com/ |

### Symposium

Symposium | 8th Scandinavian Logic Symposium |
---|---|

Location | RUC |

Country | Denmark |

City | Roskilde |

Period | 20/08/2012 → 21/08/2012 |

Internet address |

### Keywords

- modal logic
- abstract interpretation

### Cite this

*Towards Abstract Interpretation of Epistemic Logic*. Abstract from 8th Scandinavian Logic Symposium, Roskilde, Denmark.

}

**Towards Abstract Interpretation of Epistemic Logic.** / Ajspur, Mai; Gallagher, John Patrick.

Research output: Contribution to conference › Conference abstract for conference › Research › peer-review

TY - ABST

T1 - Towards Abstract Interpretation of Epistemic Logic

AU - Ajspur, Mai

AU - Gallagher, John Patrick

PY - 2012/8

Y1 - 2012/8

N2 - The model-checking problem is to decide, given a formula φ and an interpretation M, whether M satisfies φ, written M |= φ. Model-checking algorithms for temporal logics were initially developed with finite models (such as models of hardware) in mind so that M |= φ is decidable. As interest grew in model-checking infinite systems, other approaches were developed based on approximating the model-checking algorithm so that it still terminates with some useful output.In this work we present a model-checking algorithm for a multiagent epistemic logic contain- ing operators for common and distributed knowledge. The model-checker is developed as a function directly from the semantics of the logic, in a style that could be applied straight- forwardly to derive model-checkers for other logics. Secondly, we consider how to abstract the model-checker using abstract interpretation, yielding a procedure applicable to infinite models. The abstract model-checker allows model-checking with infinite-state models. When applied to the problem of whether M |= φ, it terminates and returns the set of states in M at which φ might hold. If the set is empty, then M definitely does not satisfy φ, while if the set is non-empty then M possibly satisfies φ.

AB - The model-checking problem is to decide, given a formula φ and an interpretation M, whether M satisfies φ, written M |= φ. Model-checking algorithms for temporal logics were initially developed with finite models (such as models of hardware) in mind so that M |= φ is decidable. As interest grew in model-checking infinite systems, other approaches were developed based on approximating the model-checking algorithm so that it still terminates with some useful output.In this work we present a model-checking algorithm for a multiagent epistemic logic contain- ing operators for common and distributed knowledge. The model-checker is developed as a function directly from the semantics of the logic, in a style that could be applied straight- forwardly to derive model-checkers for other logics. Secondly, we consider how to abstract the model-checker using abstract interpretation, yielding a procedure applicable to infinite models. The abstract model-checker allows model-checking with infinite-state models. When applied to the problem of whether M |= φ, it terminates and returns the set of states in M at which φ might hold. If the set is empty, then M definitely does not satisfy φ, while if the set is non-empty then M possibly satisfies φ.

KW - modal logic

KW - abstract interpretation

M3 - Conference abstract for conference

ER -