Navegar

Colección

Datos Estadísticas

Artículo

Areces, C.; Figueira, D.; Gorín, D.; Mera, S. "Tableaux and model checking for memory logics" (2009) 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009. 5607 LNAI:47-61
El editor solo permite decargar el artículo en su versión post-print desde el repositorio. Por favor, si usted posee dicha versión, enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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Κ,®, (the basic modal language extended with the operator ® used to memorize a state, the operator used to wipe out the memory, and the operator Kappa; used to check if the current point of evaluation is memorized) and some of its sublanguages. As the satisfiability problem of (MLΚ,®,) 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. © 2009 Springer-Verlag Berlin Heidelberg.

Registro:

Documento: Artículo
Título:Tableaux and model checking for memory logics
Autor:Areces, C.; Figueira, D.; Gorín, D.; Mera, S.
Ciudad:Oslo
Filiación:INRIA Nancy Grand Est, Nancy, France
INRIA Saclay, ENS Cachan, LSV, France
Departamento de Computación, UBA, Argentina
Palabras clave:Logical language; Modal language; Modal logic; Model checking problem; Relational Model; Satisfiability; Satisfiability problems; Sublanguages; Automata theory; Biomineralization; Data structures; Linguistics; Problem solving; Model checking
Año:2009
Volumen:5607 LNAI
Página de inicio:47
Página de fin:61
DOI: http://dx.doi.org/10.1007/978-3-642-02716-1_5
Título revista:18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5607LNAI_n_p47_Areces

Referencias:

  • Areces, C., Hybrid logics: The old and the new (2007) Proc. of LogKCA 2007, , San Sebastian, Spain
  • Areces, C., Figueira, D., Figueira, S., Mera, S., Expressive power and decidability for memory logics (2008) Logic, Language, Information and Computation. LNCS, 5110, pp. 56-68. , Hodges, W., de Queiroz, R. eds., Springer, Heidelberg
  • Areces, C., Figueira, D., Figueira, S., Mera, S., Expressive power and decidability for memory logics (2008) Technical Report, , INRIA Nancy, Grand Est, Extended version of 2
  • Areces, C., Figueira, S., Mera, S., Completeness results for memory logics (2009) LFCS 2009. LNCS, 5407. , Springer, Heidelberg
  • Blackburn, P., De Rijke, M., Venema, Y., (2001) Modal Logic, , Cambridge University Press, Cambridge
  • (2006) Handbook of Modal Logics, , Blackburn, P., Wolter, F., van Benthem, J. eds.:, Elsevier, Amsterdam
  • Areces, C., Cate, T.B., Hybrid Logics, pp. 821-868. , 6
  • Van Ditmarsch, H., Van Der Hoek, W., Kooi, B., (2007) Dynamic Epistemic Logic, , Kluwer Academic Publishers, Dordrecht
  • Harel, E., Lichtenstein, O., Pnueli, A., Explicit clock temporal logic (1990) Proc. of LICS 1990, pp. 402-413
  • Plaza, J., Logics of public communications (1989) Proc. of 4th International Symp. on Methodologies for Intelligent Systems, pp. 201-216
  • Van Benthem, J., Logics for information update (2001) Proc. of TARK 2001, pp. 51-67. , Morgan Kaufmann Pub., San Francisco
  • Van Benthem, J., Van Eijck, J., Kooi, B., Logics of communication and change (2006) Information and Computation, 204 (11), pp. 1620-1662
  • Chandra, A., Merlin, P., Optimal implementation of conjunctive queries in relational databases (1977) Proc. of 9th ACM Symp. on Theory of Computing, pp. 77-90
  • Bolander, T., Blackburn, P., Termination for hybrid tableaus (2007) Journal of Logic and Computation, 17, pp. 517-554
  • Papadimitriou, C., (1994) Computational Complexity, , Addison-Wesley, Reading
  • Franceschet, M., De Rijke, M., Model checking hybrid logics (with an application to semistructured data) (2006) Journal of Applied Logic, 4 (3), pp. 279-304
  • Clarke, E., Grumberg, O., Peled, D., (1999) Model Checking, , MIT Press, CambridgeA4 - The Norwegian Research Council; The Norwegian Oil Industry Association, OLF; Gaz de France SUEZ; DNV; Computas AS

Citas:

---------- APA ----------
Areces, C., Figueira, D., Gorín, D. & Mera, S. (2009) . Tableaux and model checking for memory logics. 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009, 5607 LNAI, 47-61.
http://dx.doi.org/10.1007/978-3-642-02716-1_5
---------- CHICAGO ----------
Areces, C., Figueira, D., Gorín, D., Mera, S. "Tableaux and model checking for memory logics" . 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009 5607 LNAI (2009) : 47-61.
http://dx.doi.org/10.1007/978-3-642-02716-1_5
---------- MLA ----------
Areces, C., Figueira, D., Gorín, D., Mera, S. "Tableaux and model checking for memory logics" . 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009, vol. 5607 LNAI, 2009, pp. 47-61.
http://dx.doi.org/10.1007/978-3-642-02716-1_5
---------- VANCOUVER ----------
Areces, C., Figueira, D., Gorín, D., Mera, S. Tableaux and model checking for memory logics. Lect. Notes Comput. Sci. 2009;5607 LNAI:47-61.
http://dx.doi.org/10.1007/978-3-642-02716-1_5