Lógicas modales con datos infinitos

Abstract

En este trabajo de licenciatura, extendemos la lógica dinámica proposicional (PDL, Propositional Dynamic Logic) con variables que toman valores en un dominio infinito. Esta extensión, llamada PDL parametrizada o PPDL es interpretada sobre sistemas de transición parametrizados cuyas aristas están etiquetadas con letras o variables y cuyos estados están etiquetados con proposiciones no parametrizadas. Nuestro resultado es demostrar que el problema de satisfactibilidad para PPDL es decidible cuando es interpretado sobre la subclase de sistemas de transición parametrizados en los cuales las variables pueden ser reseteadas.

We extend propositional dynamic logic (PDL) with variables ranging over an in nite domain. This extension, called parametrized PDL or PPDL for short, is interpreted over parametrized transitions systems whose edges are labeled with letters or variables and whose states are labeled with non-parametrized propositions. The result of this work shows that the satis ability problem for PPDL is decidable when interpreted over the subclass of parametrized transition systems in which variables can be reset.