Tableaux and Model Checking for Memory Logics

Carlos Areces 1 Diego Figueira 2 Daniel Gorin Sergio Mera
1 TALARIS - Natural Language Processing: representation, inference and semantics
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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 ML(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 ML( 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.
Type de document :
Communication dans un congrès
Giese, Martin and Waaler, Arild. 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods - TABLEAUX 2009, Jul 2009, Oslo, Norway. Springer-Verlag, 5607, pp.47--61, 2009, Lecture Notes in Artificial Intelligence
Liste complète des métadonnées

https://hal.inria.fr/inria-00423049
Contributeur : Areces Carlos <>
Soumis le : vendredi 9 octobre 2009 - 11:39:51
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14

Identifiants

  • HAL Id : inria-00423049, version 1

Collections

Citation

Carlos Areces, Diego Figueira, Daniel Gorin, Sergio Mera. Tableaux and Model Checking for Memory Logics. Giese, Martin and Waaler, Arild. 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods - TABLEAUX 2009, Jul 2009, Oslo, Norway. Springer-Verlag, 5607, pp.47--61, 2009, Lecture Notes in Artificial Intelligence. 〈inria-00423049〉

Partager

Métriques

Consultations de la notice

276