zbMATH — the first resource for mathematics

Tableaux and model checking for memory logics. (English) Zbl 1260.03036
Giese, Martin (ed.) et al., Automated reasoning with analytic tableaux and related methods. 18th international conference, TABLEAUX 2009, Oslo, Norway, July 6–10, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02715-4/pbk). Lecture Notes in Computer Science 5607. Lecture Notes in Artificial Intelligence, 47-61 (2009).
Summary: 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 $$\mathcal {ML}(\bigcirc_k, \bigcirc_r, \bigcirc_e)$$ (the basic modal language extended with the operator $$\bigcirc_r$$ used to memorize a state, the operator $$\bigcirc_e$$ used to wipe out the memory, and the operator $$\bigcirc_k$$ used to check if the current point of evaluation is memorized) and some of its sublanguages. As the satisfiability problem of $$\mathcal {ML}(\bigcirc_k, \bigcirc_r, \bigcirc_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.
For the entire collection see [Zbl 1173.68010].

MSC:
 03B45 Modal logic (including the logic of norms) 03B35 Mechanization of proofs and logical operations 03B70 Logic in computer science 68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: