Programación en lógica temporal basada en los operadores Since y Until

Abstract

Debido al creciente interés en diversas áreas de las Ciencias de la Computación en el estudio y manejo de nociones temporales, en los últimos años se han propuesto lenguajes de programación en lógica temporal. A pesar de esta diversidad de propuestas no hay implementaciones de las mismas accesibles públicamente. El objetivo dl presente trabajo es explicar los aspectos salientes de un nuevo lenguaje de programación en lógica temporal, que utiliza los operadores Since y Until, tanto en sus fundamentos como en lo concerniente a su implementación. Este nuevo lenguaje de programación, denominado SU-TP, se basa en el aspecto lógico en una lógica temporal presentada en [BFG+96] y en el aspecto algorítmico en una propuesta realizada por Dov Gabbay en [Gab87] para obtener una extensión a Prolog [SS86] denominada Temporal Prolog. La novedad de este trabajo con respecto a la presentación de Gabbay está en que se utilizan como operadores temporales básicos un conjunto de operadores más expresivos sobre estructuras lineales, que los que tomaron como básicos en la mencionada propuesta. Además se ha demostrado que este conjunto de operadores es completo sobre la clase de flujos lineales isomorfos a los enteros o a los reales (ver [Kam68] y [GHR87]). Si bien por limitaciones de espacio no se incluirá aquí el código, el mismo puede obtenerse de [Cob98]. No obstante explicaremos detalladamente los fundamentos lógicos de la propuesta, el algoritmo utilizado como base en la implementación y se brindarán ejemplos de su uso. Finalmente se realizarán comentarios relativos a la implementación tanto en lo que respecta a problemas solucionados como a aquellos aspectos que podrían constituir futuras mejoras. También se demostrará que el algoritmo computa una función total (siempre se detiene). Otro punto que es importante resaltar es que si bien no se conocen implementaciones de este tipo de lenguajes, como se mencionó previamente, este utiliza los operadores Since y Until usualmente citados en determinadas clases de problemas. Algunas áreas en las que se han propuesto lógicas temporales basadas en estos operadores incluyen: análisis de correctitud de programas, bases de datos deductivas temporales y generación de documentos multimediales ([Gal87]).