Se sabe que las lógicas temporales LTL, CTL, CTL * se pueden traducir / incrustar en el cálculo . En otras palabras, el cálculo (modal) subsume estas lógicas (es decir, es más expresivo).
¿Podría por favor explicarme / señalarme artículos / libros que detallen este asunto? En particular, ¿hay propiedades concretas de equidad, vitalidad, etc. que no se puedan expresar en la lógica temporal sino en el cálculo ?
losμ -cálculo es estrictamente más expresivo que LTL, CTL y CTL *. Esto es consecuencia de algunos resultados diferentes.
El primer paso es demostrar que elμ El cálculo es tan expresivo como la lógica temporal. La idea principal para codificar estas lógicas proviene de reconocer las propiedades temporales como puntos fijos. En un nivel muy informal, los puntos menos fijos le permiten expresar propiedades de naturaleza finitaria y los puntos fijos más grandes se aplican a propiedades infinitas. Por ejemplo, eventualmenteφ en LTL define que hay un instante en el futuro finito en el que φ es cierto, mientras que siempreφ Establece que φ es cierto en un número infinito de pasos de tiempo futuros. En términos de puntos fijos, la propiedad eventualmente se expresaría usando un punto fijo mínimo y la propiedad siempre usando un punto fijo máximo. Siguiendo esa intuición, los operadores temporales pueden codificarse como operadores de punto fijo.
El siguiente paso es demostrar que elμ -El cálculo es más expresivo. La idea principal es la profundidad de alternancia. Los puntos fijos se alternan si un punto menos fijo influye en el punto fijo más grande, y viceversa. La profundidad de alternancia de unμ -la fórmula de cálculo cuenta el número de alternancias que ocurren en ella. Los operadores en CTL pueden ser codificados porμ -cálculos con profundidad de alternancia 1 . Los operadores en CTL * y LTL pueden ser codificados porμ - fórmulas de cálculo con profundidad de alternancia como máximo 2 . Sin embargo, la jerarquía de alternancia de laμ -cálculo es estricto, lo que significa que aumentar la profundidad de alternancia en una fórmula le permite expresar estrictamente más propiedades. Es por eso que la gente diceμ El cálculo es más expresivo que estas lógicas temporales.
Algunas referencias:
Todo esto se trata de expresividad, no de utilidad. En la práctica, las personas no suelen especificar propiedades comoμ -expresiones de cálculo porque podrían encontrar lógicas temporales más fáciles de trabajar. Los lenguajes de especificación industrial difieren tanto de la lógica temporal como de laμ -cálculo en su sintaxis y su poder expresivo.
fuente
Es bien sabido queμ -calculi puede expresar propiedades que "cuentan módulo a constante", por ejemplo, " todos los pasos pares visitan unUNA -state "que es capturado por algo comoμ X. A ∧ □ □ X . Dichas propiedades no se pueden establecer con las modalidades TL estándar Hasta y Siguiente, ya que estas modalidades son definibles de primer orden. Ver el artículo de 1983 de DC Kozen .
fuente