Towards Abstract Interpretation of Epistemic Logic

Publikation: KonferencebidragKonferenceabstrakt til konferenceForskningpeer review

Resumé

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 φ.
OriginalsprogEngelsk
Publikationsdatoaug. 2012
Antal sider3
StatusUdgivet - aug. 2012
Begivenhed8th Scandinavian Logic Symposium - RUC, Roskilde, Danmark
Varighed: 20 aug. 201221 aug. 2012
http://scandinavianlogic.weebly.com/

Symposium

Symposium8th Scandinavian Logic Symposium
LokationRUC
LandDanmark
ByRoskilde
Periode20/08/201221/08/2012
Internetadresse

Citer dette

Ajspur, M., & Gallagher, J. P. (2012). Towards Abstract Interpretation of Epistemic Logic. Abstract fra 8th Scandinavian Logic Symposium, Roskilde, Danmark.
Ajspur, Mai ; Gallagher, John Patrick. / Towards Abstract Interpretation of Epistemic Logic. Abstract fra 8th Scandinavian Logic Symposium, Roskilde, Danmark.3 s.
@conference{e44e0c7e57dc4cbc9a0cb135f510ed54,
title = "Towards Abstract Interpretation of Epistemic Logic",
abstract = "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 φ.",
keywords = "modal logic, abstract interpretation",
author = "Mai Ajspur and Gallagher, {John Patrick}",
year = "2012",
month = "8",
language = "English",
note = "8th Scandinavian Logic Symposium, SLS 2012 ; Conference date: 20-08-2012 Through 21-08-2012",
url = "http://scandinavianlogic.weebly.com/",

}

Ajspur, M & Gallagher, JP 2012, 'Towards Abstract Interpretation of Epistemic Logic' 8th Scandinavian Logic Symposium, Roskilde, Danmark, 20/08/2012 - 21/08/2012, .

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

2012. Abstract fra 8th Scandinavian Logic Symposium, Roskilde, Danmark.

Publikation: KonferencebidragKonferenceabstrakt til konferenceForskningpeer 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 -

Ajspur M, Gallagher JP. Towards Abstract Interpretation of Epistemic Logic. 2012. Abstract fra 8th Scandinavian Logic Symposium, Roskilde, Danmark.