Tableaux and Model Checking for Memory Logics

13 years 11 months ago
Tableaux and Model Checking for Memory Logics
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. 1...
Carlos Areces, Diego Figueira, Daniel Gorín
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Authors Carlos Areces, Diego Figueira, Daniel Gorín, Sergio Mera
Comments (0)