Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-25T08:16:41.440Z Has data issue: false hasContentIssue false
  • English
  • Français

THE EXPRESSIVE POWER OF MEMORY LOGICS

Published online by Cambridge University Press:  08 June 2011

CARLOS ARECES ,
DIEGO FIGUEIRA ,
SANTIAGO FIGUEIRA  and
SERGIO MERA
CARLOS ARECES*
Affiliation:
INRIA Nancy Grand Est
DIEGO FIGUEIRA*
Affiliation:
INRIA Saclay, ENS Cachan, LSV
SANTIAGO FIGUEIRA*
Affiliation:
Departamento de Computación, FCEyN, UBA and CONICET
SERGIO MERA*
Affiliation:
Departamento de Computación, FCEyN, UBA
*
*CARLOS ARECES, INRIA NANCY GRAND EST NANCY, FRANCE. E-mail:[email protected]
†DIEGO FIGUEIRA, INRIA SACLAY, ENS CACHAN, LSV CACHAN, FRANCE. E-mail:[email protected]
‡SANTIAGO FIGUEIRA, DEPARTAMENTO DE COMPUTACIÓN, FCEyN, UNIVERSIDAD DE BUENOS AIRES BUENOS AIRES, ARGENTINA CONSEJO NACIONAL DE INVESTIGACIONES CIENTÍFICAS Y TÉCNICAS (CONICET), ARGENTINA. E-mail:[email protected]
§SERGIO MERA, DEPARTAMENTO DE COMPUTACIÓN, FCEyN, UNIVERSIDAD DE BUENOS AIRES BUENOS AIRES, ARGENTINA. E-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We investigate the expressive power of memory logics. These are modal logics extended with the possibility to store (or remove) the current node of evaluation in (or from) a memory, and to perform membership tests on the current memory. From this perspective, the hybrid logic ℋℒ (↓), for example, can be thought of as a particular case of a memory logic where the memory is an indexed list of elements of the domain.

This work focuses in the case where the memory is a set, and we can test whether the current node belongs to the set or not. We prove that, in terms of expressive power, the memory logics we discuss here lie between the basic modal logic and ℋℒ (↓). We show that the satisfiability problem of most of the logics we cover is undecidable. The only logic with a decidable satisfiability problem is obtained by imposing strong constraints on which elements can be memorized.

Type
Research Article
Information
The Review of Symbolic Logic , Volume 4 , Issue 2 , June 2011 , pp. 290 - 318
Copyright
Copyright © Association for Symbolic Logic 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

Alur, R., Courcoubetis, C., & Dill, D. (1993). Model-checking in dense real-time. Information and Computation, 104(1), 2–34.Google Scholar
Alur, R., Feder, T., & Henzinger, T. (1996). The benefits of relaxing punctuality. Journal of the ACM, 43(1), 116–146.Google Scholar
Alur, R., & Henzinger, T. (1989). A really temporal logic. In Journal of the ACM, IEEE Computer Society Press, pp. 164–169.Google Scholar
Areces, C. (2007). Hybrid logics: The old and the new. In Arrazola, X., and Larrazabal, J., editors. Proceedings of LogKCA-07, San Sebastian, Spain, Universidad del pais Vasco, Servicio Editorial, pp. 15–29.Google Scholar
Areces, C., Blackburn, P., & Marx, M. (2000). The computational complexity of hybrid temporal logics. Logic Journal of the IGPL, 8(5), 653–679.CrossRefGoogle Scholar
Areces, C., Blackburn, P., & Marx, M. (2001). Hybrid logics: Characterization, interpolation and complexity. The Journal of Symbolic Logic, 66(3), 977–1010.Google Scholar
Areces, C., Figueira, D., Figueira, S., & Mera, S. (2008). Expressive power and decidability for memory logics. In Logic, Language, Information and Computation, Vol. 5110 of Lecture Notes in Computer Science. Berlin: Springer, Proceedings of WoLLIC 2008, pp. 56–68.Google Scholar
Areces, C., Figueira, D., Gorín, D., & Mera, S. (2009a). Tableaux and model checking for memory logics. In Automated Reasoning with Analytic Tableaux and Related Methods, Vol. 5607 of LNAI, Oslo, Norway. Berlin: Springer, Proceedings of Tableaux09, pp. 47–61.Google Scholar
Areces, C., Figueira, S., & Mera, S. (2009b). Completeness results for memory logics. In Proceedings of LFCS 2009, Vol. 5407 of LNCS. Deerfield Beach, FL: Springer, pp. 16–30.Google Scholar
Areces, C., & ten Cate, B. (2006). Hybrid logics. In Blackburn, P., Wolter, F., and van Benthem, J., editors. Handbook of Modal Logics, Elsevier, pp. 821–868.Google Scholar
Berman, F., & Paterson, M. (1981). Propositional dynamic logic is weaker without tests. Theoretical Computer Science, 16, 321–328.CrossRefGoogle Scholar
Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal Logic. Cambridge University Press.CrossRefGoogle Scholar
Blackburn, P., & Seligman, J. (1995). Hybrid languages. Journal of Logic, Language and Information, 4, 251–272.CrossRefGoogle Scholar
Blackburn, P., Wolter, F., & van Benthem, J., editors. (2006). Handbook of Modal Logics. Elsevier.Google Scholar
Börger, E., Grädel, E., & Gurevich, Y. (1997). The Classical Decision Problem. Springer-Verlag.CrossRefGoogle Scholar
Ebbinghaus, H., Flum, J., & Thomas, W. (1984). Mathematical Logic. Springer-Verlag.Google Scholar
Floyd, R. (1967). Assigning meanings to programs. In Schwartz, J., editor. Proceedings of the American Mathematical Society Symposia on Applied Mathematics, Vol. 19. Providence: A.M.S., pp. 19–31.Google Scholar
Gerbrandy, J. (1999). Bisimulations on Planet Kripke. PhD Thesis, University of Amsterdam. ILLC Dissertation series DS-1999-01.Google Scholar
Groenendijk, J., & Stokhof, M. (1991a). Dynamic predicate logic. Linguistics and Philosophy, 14, 39–100.Google Scholar
Groenendijk, J., & Stokhof, M. (1991b). Two theories of dynamic semantics. In van Eijck, J., editor. Logics in AI — European Workshop JELIA’90, Lecture Notes in Artificial Intelligence, Amsterdam: Springer-Verlag, pp. 55–64.Google Scholar
Harel, D. (1984). Dynamic logic. In Gabbay, D., and Guenthner, F., editors. Handbook of Philosophical Logic. Vol. II, Vol. 165 of Synthese Library. Dordrecht, The Netherlands: D. Reidel Publishing Co. Extensions of classical logic, pp. 497–604.Google Scholar
Harel, E., Lichtenstein, O., & Pnueli, A. (1990). Explicit clock temporal logic. In Proceedings of LICS’90, Philadelphia: IEEE Computer Society, pp. 402–413.Google Scholar
Henzinger, T. (1990). Half-order modal logic: How to prove real-time properties. In Proceedings of the Ninth Annual Symposium on Principles of Distributed Computing, ACM Press, pp. 281–296.Google Scholar
Hoare, C. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12(10), 576–583.CrossRefGoogle Scholar
Koymans, R. (1990). Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4), 255–299.Google Scholar
Meier, A., Mundhenk, M., Schneider, T., Thomas, M., Weber, V., & Weiss, F. (2009). The complexity of satisfiability for fragments of hybrid logic—Part I. In Proceedings 34th International Symposium on Mathematical Foundations of Computer Science (MFCS), Vol. 5734 of LNCS, Novy Smokovec, Slovakia: Springer, pp.587–599.Google Scholar
Mera, S. (2009). Modal memory logics. PhD thesis, Universidad de Buenos Aires and Université Henri Poincaré.Google Scholar
Ouaknine, J., & Worrell, J. (2005). On the decidability of metric temporal logic. In Proceedings of the 20th IEEE Symposium of Logic in Computer Science (LICS 2005), Chicago, IL: IEEE USA: IEEE Comp. Soc. Press, pp. 188–197.Google Scholar
Plaza, J. (1989). Logics of public communications. In Emrich, M., Pfeifer, M., and Hadzikadic, M., editors. 4th International Symposium on Methodologies for Intelligent Systems, Oak Ridge National Laboratory, pp. 201–216.Google Scholar
Schneider, T. (2007). The complexity of hybrid logics over restricted classes of frames. PhD thesis, University of Jena.Google Scholar
van Benthem, J. (2001). Logics for information update. In TARK’01: Proceedings of the 8th Conference on Theoretical Aspects of Rationality and Knowledge, Siena: Morgan Kaufmann Publishers Inc, pp. 51–67.Google Scholar
van Benthem, J. (2005). An essay on sabotage and obstruction. In Hutter, D., and Stephan, W., editors. Mechanizing Mathematical Reasoning, Springer, pp. 268–276.Google Scholar
van Benthem, J., van Eijck, J., & Kooi, B. (2006). Logics of communication and change. Information and Computation, 204(11), 1620–1662.Google Scholar
van Ditmarsch, H., van der Hoek, W., & Kooi, B. (2007). Dynamic Epistemic Logic. Kluwer academic publishers.Google Scholar