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 satisfiab...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Areces, C., Figueira, D., Gorín, D., Mera, S.
Formato: SER
Materias:
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
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v5607LNAI_n_p47_Areces
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_03029743_v5607LNAI_n_p47_Areces
record_format dspace
spelling todo:paper_03029743_v5607LNAI_n_p47_Areces2023-10-03T15:19:08Z Tableaux and model checking for memory logics Areces, C. Figueira, D. Gorín, D. Mera, S. 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 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. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v5607LNAI_n_p47_Areces
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic 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
spellingShingle 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
Areces, C.
Figueira, D.
Gorín, D.
Mera, S.
Tableaux and model checking for memory logics
topic_facet 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
description 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.
format SER
author Areces, C.
Figueira, D.
Gorín, D.
Mera, S.
author_facet Areces, C.
Figueira, D.
Gorín, D.
Mera, S.
author_sort Areces, C.
title Tableaux and model checking for memory logics
title_short Tableaux and model checking for memory logics
title_full Tableaux and model checking for memory logics
title_fullStr Tableaux and model checking for memory logics
title_full_unstemmed Tableaux and model checking for memory logics
title_sort tableaux and model checking for memory logics
url http://hdl.handle.net/20.500.12110/paper_03029743_v5607LNAI_n_p47_Areces
work_keys_str_mv AT arecesc tableauxandmodelcheckingformemorylogics
AT figueirad tableauxandmodelcheckingformemorylogics
AT gorind tableauxandmodelcheckingformemorylogics
AT meras tableauxandmodelcheckingformemorylogics
_version_ 1807322285015564288

Ejemplares similares