Categoría: Investigación

Charla invitada de José Meseguer en el DSIC. Puede que sea útil para la formalización que queremos hacer de los servicios semánticos para Thomas incluyendo aspectos normativos. Como aún no ha empezado, os dejo el resumen.

In this talk, we present the temporal logic of rewriting TLR*. Syntactically, TLR* is a very simple extension of CTL* which just adds action atoms, in the form of spatial action patterns, to CTL*. Semantically and pragmatically, however, when used together with rewriting logic as a «tandem» of system specification and property specification logics, it has substantially more expressive power than purely state-based logics like CTL* , or purely action-based logics like A-CTL*. Furthermore, it avoids the system/property mismatch problem experienced in state-based or action-based logics, which makes many useful properties inexpressible in those frameworks without unnatural changes to a system’s specification. The advantages in expresiveness of TLR* are gained without losing the ability to use existing tools and algorithms to model check its properties: a faithful translation of models and formulas is given that allows verifying TLR* properties with CTL* model checkers.

El model checking se ha usado con éxito sobre lógicas modales (LTL, CTL y CTL*) basadas en estados. Por otro lado, las lógicas de acción como HML ó A-CTL* permiten superar algunas de sus limitaciones, pero sin poder expresar propiedades sobre estados.

Las especificaciones formales tienen dos tareas:

1. especificación del sistema
2. especificación de las propiedades

Y la verificación trata de demostrar que una especificación satisface una determinada propiedad \(\mathcal{S} \models \varphi\). El problema es que las lógicas usadas en cada parte no «encajan» bien, de forma que en ocasiones es necesario inventarse unas especificaciones y unas fórmulas distintas. Por ejemplo, en una lógica basada en estados como CTL no se puede hablar de acciones, por lo que es necesario añadir artificialmente variables con historia para realizar una traza de las acciones que se han aplicado. Los tandems de lógicas, como Kripke/CTL*, ó LTS/HML son muy utilizados pero adolecen de este problema. Se busca un tandem \(\mathcal{L}/ \mathcal{L}\)’ más expresivo que permita en ambos casos expresar propiedades basadas en estados y en acciones. La propuesta es usar un tandem RewritingLogic/TLR*. Con una teoría de reescritura \(\mathcal{R}=(\Sigma, E, R)\) que generaliza la representación de estados y acciones además de concurrencia real. Y por otra parte TRL* es una generalización de CTL* y A-CTL*.

TRL* es una lógica muy sencilla y muy semejante a CTL*. Simplemente añade una acción espacial \(\delta\) que indica cómo y donde se aplican las reglas (reglas de reescritura etiquetadas) \(l:t(x_1,\ldots,x_n) \rightarrow t\)’\((x_1,\ldots,x_n)\).

Los modelos de TRL* se interpretan sobre una teoría de reescritura \(\mathcal{R}\). Las fórmulas de camino se interpretan sobre computaciones \((\pi,\gamma)\) de la forma

\(\pi(0) \xrightarrow{\gamma(0)_1} \pi(1) \xrightarrow{\gamma(1)_1}\pi(2)\) \(\ldots \pi(n) \xrightarrow{\gamma(n)_1} \pi(n+1)\) \(\ldots\)

La semántica de nuevo es la misma que CTL*, añadiendo la interpretación de la nueva primitiva \(\delta\). La expresividad se muestra con un ejemplo simple: un protocolo cliente-servidor con paso de mensajes asíncrono y tolerante a fallos. Por ejemplo, con una lógica como CTL* no se puede demostrar una propiedad de equidad (fairness) como que eventualmente un cliente b va a recibir un mensaje de confirmación del servidor a. Con lógicas basadas en estados no podemos hablar de qué reglas se han aplicado para llegar hasta allí (de forma directa).

Pero el model checking sobre CTL* es muy eficiente, así que es interesante poder reducir automáticamente las propiedades en TRL* a una lógica temporal basada en estados. Muestra de nuevo el ejemplo anterior, adaptado al nuevo sistema de reescritura. Lo interesante es cómo añade una componente con «memoria» que indica quién ha realizado la última acción.

\(\mathcal{R},t \models \varphi\) \(\iff\) \(\mathcal{R}_w, (t,\delta) \models \) \(\widetilde{\varphi}\)

Básicamente, lo que hace es sustituir las acciones por un \(\bigcirc\) (next) con un predicado del mismo nombre que se considera no como la ejecución de la acción, sino como una comprobación de que la acción se ha ejecutado. Este sistema genera estados infinitos, pero puede solucionarse mediante una abstracción ecuacional que lo reduzca a un sistema de estados finitos (eliminando la «recursividad»). Pero esto puede hacer que el sistema colapse determinados estados que hagan que el sistema ya no sea coherente, por lo que será necesario añadir manualmente algunas reglas (en el ejemplo, acerca de la posible pérdida de los mensajes.

Esta no es la única aproximación que permite integrar estados y acciones. Nombra

• modal \(\mu\)-calculus
• extensiones de A-CTL* (Fantechi y también Pecheur y Raimondi)
• Propositional dynamic logic
• VLRL
• Spacial logic for concurrency (Caires y Cardelli)
• Temporal Action Logic (Lamport)

Uno de los trabajos pendientes es poder comprobar las propiedades directamente sobre TRL*. Con eso se eliminarían las etiquetas que ahora es necesario incluir en los estados de CTL*. Además, sería mucho más eficiente y se podrían eliminar también los problemas/transformaciones necesarias para tratar con los estados infinitos. Por cierto, que los demostradores están escritos en C++.

Después de oirlo (y de recordar muchas cosas que casi se me habían olvidado), se me ocurren muchas cosas, y no todas aplicables a la especificación de servicios.

Una de ellas es ver cómo «casa» esta forma de especificar los problemas con la TBox y la ABox de las lógicas DL. Posiblemente sea suficiente con usar LTL como extensión temporal. ¿Y qué tal un sistema de reescritura que pase de TRL al formalismo de SWRL-Tab?

Para saber más…

J. Meseguer: The Temporal Logic of Rewriting.- Tech. Report UIUCDCS-R-2007-2815. Dept of Computer Science. Univ. Illinois. Feb.  2007: Urbana-Champaign