Lógica de Hennessy-Milner

En informática , la lógica de Hennessy-Milner (HML) es una lógica dinámica que se utiliza para especificar propiedades de un sistema de transición etiquetado (LTS), una estructura similar a un autómata . Fue introducida en 1980 por Matthew Hennessy y Robin Milner en su artículo "On observation nondeterminism and concurrency" ^[1] ( ICALP ).

Otra variante del HML implica el uso de recursión para ampliar la expresividad de la lógica, y se conoce comúnmente como "Lógica de Hennessy-Milner con recursión". ^[2] La recursión se habilita con el uso de puntos fijos máximos y mínimos.

Sintaxis

Una fórmula se define mediante la siguiente gramática BNF para un conjunto de acciones :

${\displaystyle \Phi ::={\textit {tt}}\,\,\,|\,\,\,{\textit {ff}}\,\,\,|\,\,\,\Phi _{1}\land \Phi _{2}\,\,\,|\,\,\,\Phi _{1}\lor \Phi _{2}\,\,\,|\,\,\,[Act]\Phi \,\,\,|\,\,\,\langle Act\rangle \Phi }$

Es decir, una fórmula puede ser

verdad constante ${\displaystyle {\textit {tt}}}$

Siempre cierto

constante falso ${\displaystyle {\textit {ff}}}$

siempre falso

fórmula conjuntiva

fórmula disyuntiva

${\displaystyle \scriptstyle {[Act]\Phi }}$fórmula

Para todas las derivadas de Act , Φ debe cumplirse

${\displaystyle \scriptstyle {\langle Act\rangle \Phi }}$fórmula

Para alguna derivada de acto , Φ debe cumplirse

Semántica formal

Sea un sistema de transición etiquetado y sea el conjunto de fórmulas HML. La relación de satisfacibilidad relaciona los estados del LTS con las fórmulas que satisfacen y se define como la relación más pequeña tal que, para todos los estados y fórmulas , ${\displaystyle L=(S,{\mathsf {Act}},\rightarrow )}$ ${\displaystyle {\mathsf {HML}}}$ ${\displaystyle {}\models {}\subseteq (S\times {\mathsf {HML}})}$ ${\displaystyle s\in S}$ ${\displaystyle \phi ,\phi _{1},\phi _{2}\in {\mathsf {HML}}}$

• ${\displaystyle s\models {\textit {tt}}}$,
• no existe estado para el cual , ${\displaystyle s\in S}$ ${\displaystyle s\models {\textit {ff}}}$
• Si existe un estado tal que y , entonces , ${\displaystyle s'\in S}$ ${\displaystyle s{\xrightarrow {a}}s'}$ ${\displaystyle s'\models \phi }$ ${\displaystyle s\models \langle a\rangle \phi }$
• si para todos tales que se cumple que , entonces , ${\displaystyle s'\in S}$ ${\displaystyle s{\xrightarrow {a}}s'}$ ${\displaystyle s'\models \phi }$ ${\displaystyle s\models [a]\phi }$
• Si , entonces , ${\displaystyle s\models \phi _{1}}$ ${\displaystyle s\models \phi _{1}\lor \phi _{2}}$
• Si , entonces , ${\displaystyle s\models \phi _{2}}$ ${\displaystyle s\models \phi _{1}\lor \phi _{2}}$
• Si y , entonces . ${\displaystyle s\models \phi _{1}}$ ${\displaystyle s\models \phi _{2}}$ ${\displaystyle s\models \phi _{1}\land \phi _{2}}$

Véase también

• El cálculo modal μ , que extiende HML con operadores de punto fijo
• Lógica dinámica , una lógica multimodal con infinitas modalidades

Referencias

1. Hennessy, Matthew; Milner, Robin (14 de julio de 1980). "Sobre la observación del no determinismo y la concurrencia". Autómatas, lenguajes y programación . Apuntes de clase en informática. Vol. 85. Springer, Berlín, Heidelberg. págs. 299–309. doi :10.1007/3-540-10003-2_79. ISBN. 978-3540100034.
2. Holmström, Sören (1990). "Lógica de Hennessy-Milner con recursión como lenguaje de especificación y cálculo de refinamiento basado en ella". Especificación y verificación de sistemas concurrentes . Talleres de informática. pp. 294–330. doi :10.1007/978-1-4471-3534-0_15. ISBN 978-3-540-19581-8.

Fuentes

• Colin P. Stirling (2001). Propiedades modales y temporales de los procesos . Springer. Págs. 32-39. ISBN. 978-0-387-98717-0.
• Sören Holmström. 1988. "Lógica de Hennessy-Milner con recursión como lenguaje de especificación y cálculo de refinamiento basado en ella". En Actas del taller BCS-FACS sobre especificación y verificación de sistemas concurrentes , Charles Rattray (Ed.). Springer-Verlag, Londres, Reino Unido, 294–330.