zbMATH — the first resource for mathematics

The expressive power of memory logics. (English) Zbl 1247.03027
This paper studies memory logics, a particular kind of propositional modal logics where a relational structure \(\langle D,\mathcal I\rangle\), with \(\mathcal I\) denoting an interpretation of all propositional symbols in the language at each member of \(D\) and an interpretation of a binary accessibility relation \(r\) between members of \(D\), is extended with a memory \(M\), that is, a subset of \(D\) meant to represent the set of members of \(D\) which have been “explored” and “remembered”. The modal operators considered include the classical operator \(\langle r\rangle\) and some of the unary operators \(\langle\!\langle r\rangle\!\rangle\) and \({\mathtt r}\mkern-14mu\bigcirc\) and the nullary operator \({\mathtt k}\mkern-14mu\bigcirc\), with the following interpretation in \(\mathcal M=\langle D,\mathcal I,M\rangle\) at \(w\in D\), writing \(\mathcal M[w]\) for \(\langle D,\mathcal I, M\cup\{w\}\rangle\):
\(\mathcal M,w\models\langle r\rangle\varphi\) iff there exists \(w'\in D\) with \((w,w')\in\mathcal I\langle r \rangle\) and \(\mathcal M,w'\models\varphi\)
\(\mathcal M,w\models\langle\!\langle r\rangle\!\rangle\varphi\) iff there exists \(w'\in D\) with \((w,w')\in\mathcal I\langle r \rangle\) and \(\mathcal M[w],w'\models\varphi\)
\(\mathcal M,w\models{\mathtt r}\mkern-14mu\bigcirc\varphi\) iff \(\mathcal M[w],w\models\varphi\)
\(\mathcal M,w\models{\mathtt k}\mkern-14mu\bigcirc\) iff \(w\in M\).
So \(\langle\!\langle r\rangle\!\rangle\), besides moving to a successor state as \(\langle r\rangle\) does, remembers the state being left, \({\mathtt r}\mkern-14mu\bigcirc\) remembers the current state, and \({\mathtt k}\mkern-14mu\bigcirc\) checks whether the current state has been remembered (is “known”). For instance, the formula \[ {\mathtt r}\mkern-14mu\bigcirc\langle r\rangle \;{\mathtt k}\mkern-14mu\bigcirc \] is true at \(\langle D,\mathcal I,\emptyset\rangle\) iff \(r\) has a reflexive loop at \(w\), which demonstrates that the proposed language is more expressive than basic modal logic.
The authors explain that memory logics have been inspired by hybrid logics like \(\mathcal H\mathcal L(\downarrow)\) whose language contains nominals and formulas of the form \(\downarrow \;\!\!i.\varphi\) with \(i\) a nominal, interpreted in such a way that they dynamically use the name \(i\) to denote the current state. So \({\mathtt r}\mkern-14mu\bigcirc\) and \({\mathtt k}\mkern-14mu\bigcirc\) have less discerning power, in contrast to what can be done in \(\mathcal H\mathcal L(\downarrow)\), they cannot provide direct access to the memory and do not allow for each stored element to be unequivocally retrieved.
The authors generalise Ehrenfeucht-Fraïssé games and the notion of bisimulation to memory logics and show that both notions are equivalent. Then they study the difference in expressive power between various logics in the important case where the memory \(M\) is initially empty. They verify that the modal operators \(\langle r\rangle\), \({\mathtt r}\mkern-14mu\bigcirc\) and \({\mathtt k}\mkern-14mu\bigcirc\) yield more expressive power than the modal operators \(\langle\!\langle r\rangle\!\rangle\), \({\mathtt r}\mkern-14mu\bigcirc\) and \({\mathtt k}\mkern-14mu\bigcirc\): if \(r\) in \(\mathcal M_1\) is fully described by \(r(w,v)\), \(r(v,x)\) and \(r(x,w)\) and \(r\) in \(\mathcal M_2\) is fully described by \(r(w,v)\), \(r(v,x)\) and \(r(x,v)\) (and \(M\) is empty for both \(\mathcal M_1\) and \(\mathcal M_{2}\)) then the formula \(\langle r\rangle{\mathtt r}\mkern-14mu\bigcirc\langle r\rangle\langle r\rangle \;{\mathtt k}\mkern-14mu\bigcirc\) is true in \(\mathcal M_2\) at \(w\) but false in \(\mathcal M_{1}\) at \(w\), whereas since in both models every state has a unique successor, a formula over the language \(\langle\!\langle r\rangle\!\rangle\), \({\mathtt r}\mkern-14mu\bigcirc\) and \({\mathtt k}\mkern-14mu\bigcirc\) is true in \(\mathcal M_1\) at \(w\) iff it is true in \(\mathcal M_2\) at \(w\). It is as easily verified that the modal operators \(\langle\!\langle r\rangle\!\rangle\) and \({\mathtt k}\mkern-14mu\bigcirc\) yield more expressive power than the single modal operator \(\langle r\rangle\) of basic modal logic. Then the authors show that the modal operators \(\langle r\rangle\), \({\mathtt r}\mkern-14mu\bigcirc\) and \({\mathtt k}\mkern-14mu\bigcirc\) do not yield the expressive power of \(\mathcal H\mathcal L(\downarrow)\) with respect to a natural translation of formulas in the former language into formulas in the latter language which (1) creates bindings with new names when mapping formulas of the form \({\mathtt r}\mkern-14mu\bigcirc\varphi\) and (2) looks at whether the current state is denoted by one of the bound names when mapping the formula \({\mathtt k}\mkern-14mu\bigcirc\), a result which is also shown to hold with respect to the class of finite models.
In the second part of the paper, a modal operator \({\mathtt f}\mkern-14mu\bigcirc\) to remove (forget) the current state from memory, in case it has been memorised, and a modal operator \({\mathtt e}\mkern-14mu\bigcirc\) to completely wipe out the memory, are introduced, the notions of Ehrenfeucht-Fraïssé games and bisimulation generalised, and further results on expressive power are proved. Then a more sophisticated model of memory is proposed, using a stack rather than a set and adding to the syntax of basic modal logic the unary modal operators \((\mathtt{push})\) and \((\mathtt{pop})\). When the stack is initially empty, the resulting logic is shown to be equally expressive as \(\mathcal H\mathcal L(\downarrow)\). The paper ends with results on the decidability or undecidability, the finite model property or lack thereof, and the complexity of the satisfiability problem for some of the memory logics.

03B45 Modal logic (including the logic of norms)
Full Text: DOI
[1] DOI: 10.1016/j.ic.2006.04.006 · Zbl 1120.03012 · doi:10.1016/j.ic.2006.04.006
[2] DOI: 10.1007/BFb0018433 · doi:10.1007/BFb0018433
[3] van Benthem, TARK’01: Proceedings of the 8th Conference on Theoretical Aspects of Rationality and Knowledge pp 51– (2001)
[4] DOI: 10.1007/BF00628304 · Zbl 0726.03024 · doi:10.1007/BF00628304
[5] Floyd, Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19 pp 19– (1967)
[6] Ebbinghaus, Mathematical Logic (1984)
[7] Börger, The Classical Decision Problem (1997) · doi:10.1007/978-3-642-59207-2
[8] Areces, Proceedings of LFCS 2009, pp 16– (2009)
[9] Blackburn, Handbook of Modal Logics (2006)
[10] DOI: 10.1007/978-3-642-02716-1_5 · Zbl 1260.03036 · doi:10.1007/978-3-642-02716-1_5
[11] DOI: 10.1007/BF01049415 · Zbl 0847.03009 · doi:10.1007/BF01049415
[12] DOI: 10.1007/978-3-540-69937-8_7 · Zbl 1156.03029 · doi:10.1007/978-3-540-69937-8_7
[13] Blackburn, Modal Logic (2001) · doi:10.1017/CBO9781107050884
[14] DOI: 10.2307/2695090 · Zbl 0984.03018 · doi:10.2307/2695090
[15] DOI: 10.1016/0304-3975(81)90102-X · Zbl 0468.68039 · doi:10.1016/0304-3975(81)90102-X
[16] DOI: 10.1093/jigpal/8.5.653 · Zbl 0959.03011 · doi:10.1093/jigpal/8.5.653
[17] Areces, Handbook of Modal Logics pp 821– (2006)
[18] Areces, Proceedings of LogKCA-07, San Sebastian, Spain pp 15– (2007)
[19] Alur, Journal of the ACM pp 164– (1989)
[20] DOI: 10.1145/227595.227602 · Zbl 0882.68021 · doi:10.1145/227595.227602
[21] DOI: 10.1006/inco.1993.1024 · Zbl 0783.68076 · doi:10.1006/inco.1993.1024
[22] Plaza, 4th International Symposium on Methodologies for Intelligent Systems pp 201– (1989)
[23] DOI: 10.1109/LICS.2005.33 · doi:10.1109/LICS.2005.33
[24] Meier, Proceedings 34th International Symposium on Mathematical Foundations of Computer Science (MFCS), pp 587– (2009)
[25] DOI: 10.1007/BF01995674 · doi:10.1007/BF01995674
[26] DOI: 10.1145/363235.363259 · Zbl 0179.23105 · doi:10.1145/363235.363259
[27] DOI: 10.1145/93385.93429 · doi:10.1145/93385.93429
[28] Harel, Proceedings of LICS’90 pp 402– (1990)
[29] Harel, Handbook of Philosophical Logic. Vol. II, pp 497– (1984) · doi:10.1007/978-94-009-6259-0_10
[30] van Ditmarsch, Dynamic Epistemic Logic (2007) · Zbl 1156.03015 · doi:10.1007/978-1-4020-5839-4
[31] DOI: 10.1007/978-3-540-32254-2_16 · doi:10.1007/978-3-540-32254-2_16
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.