En informática teórica , el μ-cálculo modal ( Lμ , L μ , a veces solo μ-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 mínimo μ 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] en la versión más utilizada en la actualidad. Se utiliza para describir las propiedades de los sistemas de transición etiquetados y para verificar estas propiedades. Muchas lógicas temporales se pueden codificar en el cálculo μ, incluido CTL * y sus fragmentos ampliamente utilizados: lógica temporal lineal y lógica de árbol computacional . [3]
Una vista algebraica es verlo como un álgebra de funciones monótonas sobre un retículo completo , con operadores que consisten en composición funcional más los operadores de punto fijo mínimo y mayor; desde este punto de vista, el cálculo μ modal está sobre el entramado de un álgebra de conjuntos de potencias . [4] La semántica de juego de μ-calculus está relacionada con juegos de dos jugadores con información perfecta , particularmente juegos de paridad infinita . [5]
Sintaxis
Sea 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 de 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;
- Si es una fórmula, entonces es una fórmula;
- Si es una fórmula y es una acción, entonces es una fórmula; (pronunciado: caja o después necesariamente )
- Si es una fórmula y una variable, entonces es una fórmula, siempre que cada ocurrencia libre de en ocurre positivamente, es decir, dentro del alcance de un número par de negaciones.
(Las nociones de variables libres y ligadas son como de costumbre, donde es el único operador vinculante).
Dadas las definiciones anteriores, podemos enriquecer la sintaxis con:
- significado
- (pronunciado: diamante o después posiblemente ) significado
- medio , dónde significa sustituir por en todas las apariciones gratuitas de en .
Los primeros dos fórmulas son los familiares de la clásica cálculo de proposiciones y respectivamente el mínimo lógica multimodal K .
La notación (y su dual) están inspirados 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 , al igual que 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.
Semántica denotacional
Los modelos de cálculo μ (proposicional) se dan como sistemas de transición etiquetados dónde:
- es un conjunto de estados;
- se asigna a cada etiqueta una relación binaria en ;
- , mapea cada propuesta al conjunto de estados donde la proposición es verdadera.
Dado un sistema de transición etiquetado y una interpretación de las variables de El -cálculo, , es la función definida por las siguientes reglas:
- ;
- ;
- ;
- ;
- ;
- , dónde mapas a conservando las asignaciones de en todos lados.
Por dualidad, la interpretación de las otras fórmulas básicas es:
- ;
- ;
De manera menos formal, esto significa que, para un sistema de transición dado :
- se mantiene en el conjunto de estados ;
- se mantiene en todos los estados donde y ambos sostienen;
- se mantiene en todos los estados donde no se sostiene.
- se mantiene en un estado si cada -transición que conduce fuera de conduce a un estado donde sostiene.
- se mantiene en un estado si existe -transición que conduce fuera de que lleva a un estado donde sostiene.
- se mantiene en cualquier estado en cualquier conjunto tal que, cuando la variable se establece en , luego se mantiene para todos . (Del teorema de Knaster-Tarski se sigue quees el mayor punto fijo de, y su punto menos fijo .)
Las interpretaciones de y son de hecho los "clásicos" de la lógica dinámica . Además, el operadorpuede interpretarse como viveza ("algo bueno eventualmente sucede") ycomo seguridad ("nunca pasa nada malo") en la clasificación informal de Leslie Lamport . [7]
Ejemplos de
- se interpreta como "Es verdad lo largo de cada una -path " [7] La idea es que"es verdadero a lo largo de cada a -path "se puede definir axiomáticamente como esa oración (más débil) lo que implica y que sigue siendo cierto después de procesar cualquier una -label. [8]
- se interpreta como la existencia de un camino a lo largo de un -transitions a un estado dondesostiene. [9]
- La propiedad de que un sistema es libre de interbloqueo , lo que significa que no tiene estados sin transiciones salientes y, además, que no existe un camino a dicho estado, se expresa mediante la fórmula [9]
Problemas de decisión
La satisfacción de una fórmula de cálculo μ modal es EXPTIME-complete . [10] En cuanto a la lógica temporal lineal, [11] la verificación del modelo, la satisfacibilidad y los problemas de validez del cálculo μ modal lineal son PSPACE completos . [12]
Ver también
- Teoría de modelos finitos
- Cálculo μ modal sin alternancia
Notas
- ^ Scott, Dana ; Bakker, Jacobus (1969). "Una teoría de programas". Manuscrito inédito .
- ^ Kozen, Dexter (1982). "Resultados sobre el cálculo μ proposicional". Autómatas, lenguajes y programación . ICALP. 140 . págs. 348–359. doi : 10.1007 / BFb0012782 . ISBN 978-3-540-11576-2.
- ^ Clarke p. 108, Teorema 6; Emerson p. 196
- ^ Arnold y Niwiński, págs. Viii-x y capítulo 6
- ^ Arnold y Niwiński, págs. Viii-x y capítulo 4
- ^ Arnold y Niwiński, p. 14
- ↑ a b Bradfield y Stirling, p. 731
- ^ Bradfield y Stirling, p. 6
- ^ a b 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 . Saltador. pag. 159. ISBN 978-3-540-00428-8.
- ^ Klaus Schneider (2004). Verificación de sistemas reactivos: métodos formales y algoritmos . Saltador. pag. 521. ISBN 978-3-540-00296-3.
- ^ 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 .
- ^ 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: 250–259. doi : 10.1145 / 73560.73582 . ISBN 0897912527.
Referencias
- Clarke, Jr., Edmund M .; Orna Grumberg; Doron A. Peled (1999). Comprobación del modelo . Cambridge, Massachusetts, EE.UU .: MIT press. ISBN 0-262-03270-8., capítulo 7, Comprobación del modelo 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, Modal μ-calculus, págs. 103-128
- André Arnold; Damian Niwiński (2001). Rudimentos de μ-Calculus . 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 ; se presentó en la 18a 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.). El manual de lógica modal . Elsevier . págs. 721–756.
- Emerson, E. Allen (1996). "Verificación de modelos y el cálculo de Mu". Complejidad descriptiva y modelos finitos . Sociedad Matemática Estadounidense . págs. 185–214. ISBN 0-8218-0517-7.
- Kozen, Dexter (1983). "Resultados sobre el cálculo μ proposicional" . Informática Teórica . 27 (3): 333–354. doi : 10.1016 / 0304-3975 (82) 90125-6 .
enlaces externos
- Sophie Pinchinat, Logic, Automata & Games videograbación de una conferencia en ANU Logic Summer School '09