En informática , la lógica de Hennessy-Milner (HML) es una lógica dinámica que se utiliza para especificar las propiedades de un sistema de transición etiquetado (LTS), una estructura similar a un autómata . Fue introducido en 1980 por Matthew Hennessy y Robin Milner en su artículo "Sobre la observación del no determinismo y la concurrencia" [1] ( ICALP ).
Otra variante del HML implica el uso de la recursividad para ampliar la expresibilidad de la lógica, y se la conoce comúnmente como "Lógica de Hennessy-Milner con recursividad". [2] La recursividad 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 actuar en un conjunto de acciones:
Es decir, una fórmula puede ser
- verdad constante
- siempre cierto
- constante falso
- siempre falso
- conjunción fórmula
- disyunción de la fórmula
- fórmula
- para todos los derivados de Act , Φ debe contener
- fórmula
- para algún derivado de Act , Φ debe contener
Semántica formal
Dejar ser un sistema de transición etiquetado , y dejarser el conjunto de fórmulas HML. La relación de satisfacibilidad relaciona los estados de la 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 ,
- ,
- no hay estado para cual ,
- si existe un estado tal que y , luego ,
- si por todos tal que sostiene eso , luego ,
- Si , luego ,
- Si , luego ,
- Si y , luego .
Ver 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
- ^ 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 conferencias en Ciencias de la Computación. Springer, Berlín, Heidelberg. págs. 299-309. doi : 10.1007 / 3-540-10003-2_79 . ISBN 978-3540100034.
- ^ Holmström, Sören (1990). "Lógica de Hennessy-Milner con la recursividad como lenguaje de especificación y un cálculo de refinamiento basado en ella". Actas del taller BCS-FACS sobre especificación y verificación de sistemas concurrentes : 294–330.
Fuentes
- Colin P. Stirling (2001). Propiedades modales y temporales de los procesos . Saltador. págs. 32 –39. ISBN 978-0-387-98717-0.
- Sören Holmström. 1988. "Lógica de Hennessy-Milner con la recursividad como lenguaje de especificación y un 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.