Cálculo μ modal

Extensión de la lógica modal proposicional

En informática teórica , el μ-cálculo modal ( Lμ , L _μ , a veces simplemente μ-cálculo , aunque puede tener un significado más general) es una extensión de la lógica modal proposicional (con muchas modalidades ) al agregar el operador de punto fijo menor μ y el operador de punto fijo mayor ν, por lo tanto una lógica de punto fijo .

El cálculo μ (proposicional, modal) tiene su origen en Dana Scott y Jaco de Bakker ^[1] y fue desarrollado por Dexter Kozen ^[2] hasta convertirse en la versión más utilizada en la actualidad. Se utiliza para describir propiedades de sistemas de transición etiquetados y para verificar estas propiedades. Muchas lógicas temporales se pueden codificar en el cálculo μ, incluyendo CTL* y sus fragmentos ampliamente utilizados : lógica temporal lineal y lógica de árbol computacional ^[3] .

Una visión algebraica es considerarlo como un álgebra de funciones monótonas sobre una red completa , con operadores que consisten en composición funcional más los operadores de punto fijo mínimo y máximo; desde este punto de vista, el μ-cálculo modal es sobre la red de un álgebra de conjuntos de potencias . ^[4] La semántica de juego del μ-cálculo está relacionada con juegos de dos jugadores con información perfecta , particularmente juegos de paridad infinita . ^[5]

Sintaxis

Sean P (proposiciones) y A (acciones) dos conjuntos finitos de símbolos, y sea Var un conjunto de variables numerablemente infinito. El conjunto de fórmulas del μ-cálculo (proposicional, modal) se define de la siguiente manera:

• cada proposición y cada variable es una fórmula;
• si y son fórmulas, entonces es una fórmula; ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \phi \wedge \psi }$
• si es una fórmula, entonces es una fórmula; ${\displaystyle \phi }$ ${\displaystyle \neg \phi }$
• Si es una fórmula y es una acción, entonces es una fórmula; (se pronuncia: box o after necesariamente ) ${\displaystyle \phi }$ ${\displaystyle a}$ ${\displaystyle [a]\phi }$ ${\displaystyle a}$ ${\displaystyle \phi }$ ${\displaystyle a}$ ${\displaystyle \phi }$
• si es una fórmula y una variable, entonces es una fórmula, siempre que cada ocurrencia libre de en ocurra positivamente, es decir, dentro del alcance de un número par de negaciones. ${\displaystyle \phi }$ ${\displaystyle Z}$ ${\displaystyle \nu Z.\phi }$ ${\displaystyle Z}$ ${\displaystyle \phi }$

(Las nociones de variables libres y ligadas son las habituales, donde es el único operador de ligadura). ${\displaystyle \nu }$

Dadas las definiciones anteriores, podemos enriquecer la sintaxis con:

• ${\displaystyle \phi \lor \psi }$significado ${\displaystyle \neg (\neg \phi \land \neg \psi )}$
• ${\displaystyle \langle a\rangle \phi }$(pronunciado: diamante o posiblemente después ) significado ${\displaystyle a}$ ${\displaystyle \phi }$ ${\displaystyle a}$ ${\displaystyle \phi }$ ${\displaystyle \neg [a]\neg \phi }$
• ${\displaystyle \mu Z.\phi }$significa , donde significa sustituir en todas las apariciones libres de en . ${\displaystyle \neg \nu Z.\neg \phi [Z:=\neg Z]}$ ${\displaystyle \phi [Z:=\neg Z]}$ ${\displaystyle \neg Z}$ ${\displaystyle Z}$ ${\displaystyle Z}$ ${\displaystyle \phi }$

Las dos primeras fórmulas son las conocidas del cálculo proposicional clásico y de la lógica multimodal mínima K , respectivamente .

La notación (y su dual) están inspiradas en el cálculo lambda ; la intención es denotar el punto fijo menor (y respectivamente mayor) de la expresión donde la "minimización" (y respectivamente la "maximización") están en la variable , de forma muy similar a como en el cálculo lambda es una función con fórmula en la variable ligada ; ^[6] vea la semántica denotacional a continuación para obtener más detalles. ${\displaystyle \mu Z.\phi }$ ${\displaystyle \phi }$ ${\displaystyle Z}$ ${\displaystyle \lambda Z.\phi }$ ${\displaystyle \phi }$ ${\displaystyle Z}$

Semántica denotacional

Los modelos de μ-cálculo (proposicional) se dan como sistemas de transición etiquetados donde: ${\displaystyle (S,R,V)}$

• ${\displaystyle S}$es un conjunto de estados;
• ${\displaystyle R}$asigna a cada etiqueta una relación binaria en ; ${\displaystyle a}$ ${\displaystyle S}$
• ${\displaystyle V:P\to 2^{S}}$, asigna cada proposición al conjunto de estados donde la proposición es verdadera. ${\displaystyle p\in P}$

Dado un sistema de transición etiquetado y una interpretación de las variables del cálculo, , es la función definida por las siguientes reglas: ${\displaystyle (S,R,V)}$ ${\displaystyle i}$ ${\displaystyle Z}$ ${\displaystyle \mu }$ ${\displaystyle [\![\cdot ]\!]_{i}:\phi \to 2^{S}}$

• ${\displaystyle [\![p]\!]_{i}=V(p)}$;
• ${\displaystyle [\![Z]\!]_{i}=i(Z)}$;
• ${\displaystyle [\![\phi \wedge \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cap [\![\psi ]\!]_{i}}$;
• ${\displaystyle [\![\neg \phi ]\!]_{i}=S\smallsetminus [\![\phi ]\!]_{i}}$;
• ${\displaystyle [\![[a]\phi ]\!]_{i}=\{s\in S\mid \forall t\in S,(s,t)\in R_{a}\rightarrow t\in [\![\phi ]\!]_{i}\}}$;
• ${\displaystyle [\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{i[Z:=T]}\}}$, donde se asignan los mapas mientras se preservan los mapeos de todos los demás lugares. ${\displaystyle i[Z:=T]}$ ${\displaystyle Z}$ ${\displaystyle T}$ ${\displaystyle i}$

Por dualidad, la interpretación de las demás fórmulas básicas es:

• ${\displaystyle [\![\phi \vee \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cup [\![\psi ]\!]_{i}}$;
• ${\displaystyle [\![\langle a\rangle \phi ]\!]_{i}=\{s\in S\mid \exists t\in S,(s,t)\in R_{a}\wedge t\in [\![\phi ]\!]_{i}\}}$;
• ${\displaystyle [\![\mu Z.\phi ]\!]_{i}=\bigcap \{T\subseteq S\mid [\![\phi ]\!]_{i[Z:=T]}\subseteq T\}}$

De manera menos formal, esto significa que, para un sistema de transición dado : ${\displaystyle (S,R,V)}$

• ${\displaystyle p}$se cumple en el conjunto de estados ; ${\displaystyle V(p)}$
• ${\displaystyle \phi \wedge \psi }$se cumple en cada estado donde y ambos se cumplen; ${\displaystyle \phi }$ ${\displaystyle \psi }$
• ${\displaystyle \neg \phi }$Se aplica en todos los estados donde no se aplica. ${\displaystyle \phi }$
• ${\displaystyle [a]\phi }$se mantiene en un estado si cada transición que sale de conduce a un estado donde se mantiene. ${\displaystyle s}$ ${\displaystyle a}$ ${\displaystyle s}$ ${\displaystyle \phi }$
• ${\displaystyle \langle a\rangle \phi }$se mantiene en un estado si existe -transición que conduce fuera de ese estado a un estado donde se mantiene. ${\displaystyle s}$ ${\displaystyle a}$ ${\displaystyle s}$ ${\displaystyle \phi }$
• ${\displaystyle \nu Z.\phi }$se cumple en cualquier estado en cualquier conjunto tal que, cuando la variable se establece en , entonces se cumple para todos los . (Del teorema de Knaster-Tarski se deduce que es el mayor punto fijo de , y su menor punto fijo .) ${\displaystyle T}$ ${\displaystyle Z}$ ${\displaystyle T}$ ${\displaystyle \phi }$ ${\displaystyle T}$ ${\displaystyle [\![\nu Z.\phi ]\!]_{i}}$ ${\displaystyle T\mapsto [\![\phi ]\!]_{i[Z:=T]}}$ ${\displaystyle [\![\mu Z.\phi ]\!]_{i}}$

Las interpretaciones de y son, de hecho, las "clásicas" de la lógica dinámica . Además, el operador puede interpretarse como vitalidad ("algo bueno eventualmente sucede") y como seguridad ("nada malo sucede nunca") en la clasificación informal de Leslie Lamport . ^[7] ${\displaystyle [a]\phi }$ ${\displaystyle \langle a\rangle \phi }$ ${\displaystyle \mu }$ ${\displaystyle \nu }$

Ejemplos

• ${\displaystyle \nu Z.\phi \wedge [a]Z}$se interpreta como " es verdadero a lo largo de cada camino a ". ^[7] La ​​idea es que " es verdadero a lo largo de cada camino a " se puede definir axiomáticamente como aquella oración (más débil) que implica y que sigue siendo verdadera después de procesar cualquier etiqueta a . ^[8] ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle Z}$ ${\displaystyle \phi }$
• ${\displaystyle \mu Z.\phi \vee \langle a\rangle Z}$se interpreta como la existencia de un camino a lo largo de una -transición hacia un estado donde se cumple. ^[9] ${\displaystyle \phi }$
• La propiedad de que un estado no tenga puntos muertos , es decir, que ningún camino desde ese estado llegue a un callejón sin salida, se expresa mediante la fórmula ^[9]. $${\displaystyle \nu Z.\left(\bigvee _{a\in A}\langle a\rangle \top \wedge \bigwedge _{a\in A}[a]Z\right)}$$

Problemas de decisión

La satisfacibilidad de una fórmula de μ-cálculo modal es EXPTIME-completa . ^[10] Al igual que para la lógica temporal lineal, ^[11] los problemas de verificación de modelos , satisfacibilidad y validez del μ-cálculo modal lineal son PSPACE-completos . ^[12]

Véase también

• Teoría de modelos finitos
• Cálculo μ modal sin alternancia

Notas

1. Scott, Dana ; Bakker, Jacobus (1969). "Una teoría de programas". Manuscrito inédito .
2. Kozen, Dexter (1982). "Resultados del cálculo μ proposicional". Autómatas, lenguajes y programación . ICALP. Vol. 140. págs. 348–359. doi :10.1007/BFb0012782. ISBN. 978-3-540-11576-2.
3. Clarke p.108, Teorema 6; Emerson p. 196
4. Arnold y Niwiński, págs. viii-x y capítulo 6
5. Arnold y Niwiński, págs. viii-x y capítulo 4
6. Arnold y Niwiński, pág. 14
7. Bradfield y Stirling, pág. 731
8. Bradfield y Stirling, pág. 6
9. Erich Grädel; Phokion G. Kolaitis; Leonid Libkin ; Maarten Marx; Joel Spencer ; Moshe Y. Vardi ; Yde Venema; Scott Weinstein (2007). Teoría de modelos finitos y sus aplicaciones. Springer. pág. 159. ISBN 978-3-540-00428-8.
10. Klaus Schneider (2004). Verificación de sistemas reactivos: métodos formales y algoritmos. Springer. pág. 521. ISBN 978-3-540-00296-3.
11. Sistla, AP; Clarke, EM (1 de julio de 1985). "La complejidad de las lógicas temporales lineales proposicionales". J. ACM . 32 (3): 733–749. doi : 10.1145/3828.3837 . ISSN  0004-5411.
12. Vardi, MY (1 de enero de 1988). "Un cálculo de punto fijo temporal". Actas del 15.º simposio ACM SIGPLAN-SIGACT sobre Principios de lenguajes de programación - POPL '88 . Nueva York, NY, EE. UU.: ACM. pp. 250–259. doi : 10.1145/73560.73582 . ISBN . 0897912527.

Referencias

• Clarke, Edmund M. Jr.; Orna Grumberg; Doron A. Peled (1999). Model Checking . Cambridge, Massachusetts, EE. UU.: MIT Press. ISBN 0-262-03270-8., capítulo 7, Comprobación de modelos para el cálculo μ, págs. 97–108
• Stirling, Colin. (2001). Propiedades modales y temporales de los procesos . Nueva York, Berlín, Heidelberg: Springer Verlag. ISBN 0-387-98717-7., capítulo 5, Cálculo modal μ, págs. 103-128
• André Arnold; Damián Niwiński (2001). Rudimentos del cálculo μ . Elsevier. ISBN 978-0-444-50620-7., el capítulo 6, El cálculo μ sobre álgebras de conjuntos potencia, págs. 141-153, trata sobre el cálculo μ modal
• Yde Venema (2008) Conferencias sobre el cálculo modal μ; se presentó en la 18ª Escuela Europea de Verano en Lógica, Lenguaje e Información
• Bradfield, Julian y Stirling, Colin (2006). "Modal mu-calculi". En P. Blackburn; J. van Benthem y F. Wolter (eds.). The Handbook of Modal Logic . Elsevier . págs. 721–756.
• Emerson, E. Allen (1996). "Verificación de modelos y cálculo Mu". Complejidad descriptiva y modelos finitos . American Mathematical Society . págs. 185–214. ISBN. 0-8218-0517-7.
• Kozen, Dexter (1983). "Resultados del cálculo μ proposicional". Ciencias de la computación teórica . 27 (3): 333–354. doi :10.1016/0304-3975(82)90125-6.

Enlaces externos

• Sophie Pinchinat, Logic, Automata & Games, grabación en video de una conferencia en la Escuela de verano de lógica de la ANU '09