Cálculo μ modal

En la ciencia de la computación teórica , el μ-cálculo modal ( Lμ , L _μ o mu-cálculo proposicional ^{[ 1 ]} , 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 fijo menor μ y el operador de punto fijo mayor ν, por lo tanto, una lógica de punto fijo .

El μ-cálculo (proposicional y modal) se originó con ^Dana Scott y Jaco de Bakker [ ^{2 ]} y fue desarrollado posteriormente por Dexter Kozen ^{[ 3 ]} hasta convertirse en la versión más utilizada actualmente. Se emplea para describir propiedades de sistemas de transición etiquetados y para verificar dichas propiedades. En el μ-cálculo se pueden codificar diversas lógicas temporales , incluyendo CTL* y sus fragmentos de uso común : la lógica temporal lineal y la lógica de árbol computacional ^{[ 4 ]} .

Una perspectiva algebraica consiste en verlo como un álgebra de funciones monótonas sobre un retículo completo , con operadores que consisten en la composición funcional más los operadores de punto fijo mínimo y máximo; desde este punto de vista, el μ-cálculo modal se encuentra sobre el retículo de un álgebra de conjuntos potencia . ^{[ 5 ]} La semántica de juegos del μ-cálculo está relacionada con juegos de dos jugadores con información perfecta , particularmente juegos de paridad infinita . ^{[ 6 ]}

Sean P (proposiciones) y A (acciones) dos conjuntos finitos de símbolos, y sea Var un conjunto infinito 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${\displaystyle \phi }$y${\displaystyle \psi }$son fórmulas, entonces${\displaystyle \phi \wedge \psi }$es una fórmula;
• si${\displaystyle \phi }$es una fórmula, entonces${\displaystyle \neg \phi }$es una fórmula;
• si${\displaystyle \phi }$es una fórmula y${\displaystyle a}$es una acción, entonces${\displaystyle [a]\phi }$es una fórmula; (se pronuncia de cualquiera de las siguientes maneras:${\displaystyle a}$caja${\displaystyle \phi }$o después${\displaystyle a}$necesariamente${\displaystyle \phi }$)
• si${\displaystyle \phi }$es una fórmula y${\displaystyle Z}$una variable, entonces${\displaystyle \nu Z.\phi }$es una fórmula, siempre que cada ocurrencia libre de${\displaystyle Z}$en${\displaystyle \phi }$ocurre de forma positiva, es decir, dentro del ámbito de un número par de negaciones.

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

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 }$(se pronuncia de cualquiera de las dos maneras:${\displaystyle a}$diamante${\displaystyle \phi }$o después${\displaystyle a}$probablemente${\displaystyle \phi }$) significado${\displaystyle \neg [a]\neg \phi }$
• ${\displaystyle \mu Z.\phi }$medio${\displaystyle \neg \nu Z.\neg \phi [Z:=\neg Z]}$, dónde${\displaystyle \phi [Z:=\neg Z]}$significa sustituir${\displaystyle \neg Z}$para${\displaystyle Z}$en todas las ocurrencias libres de${\displaystyle Z}$en${\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${\displaystyle \mu Z.\phi }$(y su dual) están inspirados en el cálculo lambda ; la intención es denotar el punto fijo menor (y respectivamente el mayor) de la expresión${\displaystyle \phi }$donde la "minimización" (y respectivamente la "maximización") se encuentran en la variable${\displaystyle Z}$, muy parecido al cálculo lambda${\displaystyle \lambda Z.\phi }$es una función con fórmula${\displaystyle \phi }$en variable ligada${\displaystyle Z}$; ^{[ 7 ]} consulte la semántica denotacional a continuación para obtener más detalles.

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

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

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

• ${\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]}\}}$, dónde${\displaystyle i[Z:=T]}$mapas${\displaystyle Z}$a${\displaystyle T}$mientras se preservan las asignaciones de${\displaystyle i}$en cualquier otro lugar.

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 mantiene en el conjunto de estados${\displaystyle V(p)}$;
• ${\displaystyle \phi \wedge \psi }$se celebra en todos los estados donde${\displaystyle \phi }$y${\displaystyle \psi }$ambos sostienen;
• ${\displaystyle \neg \phi }$se celebra en todos los estados donde${\displaystyle \phi }$no se sostiene.
• ${\displaystyle [a]\phi }$se mantiene en un estado${\displaystyle s}$si cada${\displaystyle a}$-transición que conduce a la salida${\displaystyle s}$conduce a un estado donde${\displaystyle \phi }$sostiene.
• ${\displaystyle \langle a\rangle \phi }$se mantiene en un estado${\displaystyle s}$si existe${\displaystyle a}$-transición que conduce a la salida${\displaystyle s}$que conduce a un estado donde${\displaystyle \phi }$sostiene.
• ${\displaystyle \nu Z.\phi }$se mantiene en cualquier estado en cualquier conjunto${\displaystyle T}$de tal manera que, cuando la variable${\displaystyle Z}$está configurado para${\displaystyle T}$, entonces${\displaystyle \phi }$se mantiene para todos${\displaystyle T}$. (Del teorema de Knaster-Tarski se deduce que${\displaystyle [\![\nu Z.\phi ]\!]_{i}}$es el punto fijo más grande de${\displaystyle T\mapsto [\![\phi ]\!]_{i[Z:=T]}}$, y${\displaystyle [\![\mu Z.\phi ]\!]_{i}}$su punto menos fijo .)

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

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

De hecho, la complejidad del problema de satisfacibilidad del μ-cálculo modal graduado también es EXPTIME-completa, incluso si el número en las modalidades se escribe en binario (el μ-cálculo modal graduado es una extensión del μ-cálculo modal estándar con modalidades "hay al menos k sucesores tales que..."). ^{[ 14 ]}

Recordemos que la lógica modal se puede traducir a lógica de primer orden (FO) mediante la traducción estándar denotada por${\displaystyle ST}$y indexado por una variable de primer orden${\displaystyle x}$que denota el estado actual:

${\displaystyle {\begin{aligned}ST_{x}(p)&:=p(x)\\ST_{x}(\lnot \phi )&:=\lnot ST_{x}(\phi )\\ST_{x}(\phi \land \psi )&:=ST_{x}(\phi )\land ST_{y}(\psi )\\ST_{x}([a]\phi )&:=\forall y,xR_{a}y\rightarrow ST_{y}(\phi )\end{aligned}}}$

Recordemos que la lógica monádica de segundo orden (MSO) extiende la lógica de primer orden (FO) con cuantificaciones de segundo orden sobre subconjuntos. La traducción estándar se extiende al cálculo mu, que puede traducirse en lógica monádica de segundo orden añadiendo las siguientes reglas de traducción para los operadores de punto fijo ^{[ 15 ]} :

${\displaystyle {\begin{aligned}ST_{x}(\mu X.\phi )&:=\forall X,(\forall y,ST_{y}(\phi )\rightarrow y\in X)\rightarrow x\in X)\\ST_{x}(\nu X.\phi )&:=\exists X,(\forall y,y\in X\rightarrow ST_{y}(\phi ))\land x\in X)\end{aligned}}}$

Janin y Walukiewicz demostraron en 1996 que cualquier fórmula monádica de segundo orden que sea invariante por bisimilación es equivalente a alguna fórmula de cálculo mu ^{[ 1 ]} .

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

• 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, Verificació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 potencia, pp.  141–153 trata sobre el μ-cálculo modal
• Yde Venema (2008) Lecciones sobre el μ-cálculo modal ; fue presentada en la 18.ª Escuela Europea de Verano en Lógica, Lenguaje e Información.
• Bradfield, Julian y Stirling, Colin (2006). "Cálculos modales mu" . En P. Blackburn; J. van Benthem y F. Wolter (eds.). Manual de lógica modal . Elsevier . págs. 721–756 . 
• Emerson, E. Allen (1996). «Verificación de modelos y el cálculo Mu». Complejidad descriptiva y modelos finitos . Sociedad Matemática Americana . págs. 185–214 . ISBN  0-8218-0517-7.
• Kozen, Dexter (1983). "Resultados sobre el μ-cálculo proposicional". Theoretical Computer Science . 27 (3): 333– 354. doi : 10.1016/0304-3975(82)90125-6 .

• Sophie Pinchinat, Lógica, Autómatas y Juegos: grabación en vídeo de una conferencia en la Escuela de Verano de Lógica de la ANU '09.