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 esto 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 mínimo fijo. μ y el mayor operador de punto fijo ν, por lo tanto una lógica de punto fijo .

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

Una visión algebraica es verlo como un álgebra de funciones monótonas sobre una red completa , con operadores que consisten en una composición funcional más los operadores de punto fijo menor y mayor; Desde este punto de vista, el cálculo modal μ está sobre la red de un álgebra de conjuntos de potencias . ^[4] La semántica del 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 infinito y numerable de variables. 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; (pronunciado: cuadro o después 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 aparición libre de in 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 vinculadas son las habituales, donde está el único operador vinculante). ${\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 después de posiblemente ) significado ${\displaystyle a}$ ${\displaystyle \phi }$ ${\displaystyle a}$ ${\displaystyle \phi }$ ${\displaystyle \neg [a]\neg \phi }$
• ${\displaystyle \mu Z.\phi }$medios , donde medios sustituyendo por 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, respectivamente , de la lógica multimodal mínima K.

La notación (y su dual) están inspiradas en el cálculo lambda ; la intención es denotar el punto fijo mínimo (y respectivamente mayor) de la expresión donde la "minimización" (y respectivamente la "maximización") están en la variable , muy parecido a como en el cálculo lambda es una función con fórmula en variable ligada ; ^[6] consulte 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]}\}}$, hacia dónde se asigna y al mismo tiempo se conservan las asignaciones 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 determinado : ${\displaystyle (S,R,V)}$

• ${\displaystyle p}$se cumple en el conjunto de estados ; ${\displaystyle V(p)}$
• ${\displaystyle \phi \wedge \psi }$se mantiene en todos los estados donde y ambos se mantienen; ${\displaystyle \phi }$ ${\displaystyle \psi }$
• ${\displaystyle \neg \phi }$se mantiene en todos los estados donde no se cumple. ${\displaystyle \phi }$
• ${\displaystyle [a]\phi }$se mantiene en un estado si cada transición que conduce a un estado en el que se mantiene. ${\displaystyle s}$ ${\displaystyle a}$ ${\displaystyle s}$ ${\displaystyle \phi }$
• ${\displaystyle \langle a\rangle \phi }$se mantiene en un estado si existe ; la transición que sale de eso conduce a un estado en el que se mantiene. ${\displaystyle s}$ ${\displaystyle a}$ ${\displaystyle s}$ ${\displaystyle \phi }$
• ${\displaystyle \nu Z.\phi }$se mantiene en cualquier estado en cualquier conjunto de modo que, cuando la variable se establece en , se cumple para todos . (Del teorema de Knaster-Tarski se deduce que es el mayor punto fijo de y su punto mínimo 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 en realidad las "clásicas" de la lógica dinámica . Además, el operador puede interpretarse como vivacidad ("algo bueno eventualmente sucede") y como seguridad ("nunca sucede nada malo") 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 cierto en cada camino a". ^[7] La ​​idea es que " es verdadero en cada camino a " puede definirse axiomáticamente como esa 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 -transiciones hacia un estado en el que se mantiene. ^[9] ${\displaystyle \phi }$
• La propiedad de un estado de estar libre de puntos muertos , es decir, ningún camino desde ese estado llega 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 satisfacción 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, satisfacibilidad y validez del modelo del cálculo μ modal lineal son PSPACE-completos . ^[12]

Ver también

• Teoría del modelo finito
• Cálculo μ modal sin alternancia

Notas

1. Scott, Dana ; Bakker, Jacobus (1969). "Una teoría de los 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ág. 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, pag. 14
7. Bradfield y Stirling, pág. 731
8. Bradfield y Stirling, pag. 6
9. Erich Grädel; Phokion G. Kolaitis; Leónidas Libkin ; Martín Marx; Joel Spencer ; Moshé Y. Vardi ; Ydé Venema; Scott Weinstein (2007). Teoría de modelos finitos y sus aplicaciones. Saltador. pag. 159.ISBN​ 978-3-540-00428-8.
10. Klaus Schneider (2004). Verificación de sistemas reactivos: métodos formales y algoritmos. Saltador. pag. 521.ISBN​ 978-3-540-00296-3.
11. Sistla, AP; Clarke, EM (1 de julio de 1985). "La complejidad de la lógica temporal lineal proposicional". J. ACM . 32 (3): 733–749. doi : 10.1145/3828.3837 . ISSN  0004-5411.
12. Vardi, MI (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, Estados Unidos: ACM. págs. 250-259. doi : 10.1145/73560.73582 . ISBN 0897912527.

Referencias

• Clarke, Edmund M. Jr.; Orna Grumberg; Dorón A. Peled (1999). Comprobación de modelos . Cambridge, Massachusetts, EE.UU.: prensa del MIT. 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., capítulo 6, El cálculo μ sobre álgebras de conjuntos de potencias, págs. 141-153 trata sobre el cálculo μ modal
• Yde Venema (2008) Conferencias sobre el cálculo modal μ; fue presentado en la 18ª Escuela Europea de Verano en Lógica, Lenguaje e Información
• Bradfield, Julian y Stirling, Colin (2006). "Mucálculos modales". En P. Blackburn; J. van Benthem y F. Wolter (eds.). El manual de lógica modal . Elsevier . págs. 721–756.
• Emerson, E.Allen (1996). "Verificación de modelos y cálculo Mu". Complejidad Descriptiva y Modelos Finitos . Sociedad Matemática Estadounidense . págs. 185-214. ISBN 0-8218-0517-7.
• Kozen, Dexter (1983). "Resultados del cálculo μ proposicional". Informática Teórica . 27 (3): 333–354. doi :10.1016/0304-3975(82)90125-6.

enlaces externos

• Sophie Pinchinat, grabación de vídeo de Logic, Automata & Games de una conferencia en la ANU Logic Summer School '09