Tableaux and Model Checking for Memory Logics

C. Areces, D. Figueira, D. Gor\'in, and S. Mera. Tableaux and Model Checking for Memory Logics. In Automated Reasoning with Analytic Tableaux and Related Methods, LNAI, pp. 47–61, Springer Berling / Heidelberg, Oslo, Norway, 2009. Proceedings of Tableaux09

Download

[pdf] 

Abstract

Memory logics are modal logics whose semantics is specified in terms of relational models enriched with additional data structure to represent memory. The logical language is then extended with a collection of operations to access and modify the data structure. In this paper we study their satisfiability and the model checking problems. We first give sound and complete tableaux calculi for the memory logic  (k, r, e) (the basic modal language extended with the operator r used to memorize a state, the operator e used to wipe out the memory, and the operator k used to check if the current point of evaluation is memorized) and some of its sublanguages. As the satisfiability problem of  (k, r, e) is undecidable, the tableau calculus we present is non terminating. Hence, we furthermore study a variation that ensures termination, at the expense of completeness, and we use model checking to ensure soundness. Secondly, we show that the model checking problem is PSpace-complete.

BibTeX

@InCollection{Areces2009a,
  author =       "C. Areces and D. Figueira and D. Gor{\'i}n and S.
                 Mera",
  booktitle =    "Automated Reasoning with Analytic Tableaux and Related
                 Methods",
  title =        "Tableaux and Model Checking for Memory Logics",
  abstract =     "Memory logics are modal logics whose semantics is
                 specified in terms of relational models enriched with
                 additional data structure to represent memory. The
                 logical language is then extended with a collection of
                 operations to access and modify the data structure. In
                 this paper we study their satisfiability and the model
                 checking problems. We first give sound and complete
                 tableaux calculi for the memory logic  (k, r, e)
                 (the basic modal language extended with the operator r
                 used to memorize a state, the operator e used to wipe
                 out the memory, and the operator k used to check if the
                 current point of evaluation is memorized) and some of
                 its sublanguages. As the satisfiability problem of
                  (k, r, e) is undecidable, the tableau calculus
                 we present is non terminating. Hence, we furthermore
                 study a variation that ensures termination, at the
                 expense of completeness, and we use model checking to
                 ensure soundness. Secondly, we show that the model
                 checking problem is PSpace-complete.",
  year =         "2009",
  address =      "Oslo, Norway",
  note =         "Proceedings of Tableaux09",
  pages =        "47--61",
  publisher =    "Springer Berling / Heidelberg",
  series =       "LNAI",
  volume =       "5607",
  editors =      "M. Giese and A. Waaler",
  ISBN =         "978-3-642-02715-4",
}