Логика Хеннесси-Милнера - Hennessy–Milner logic

В Информатика, Логика Хеннесси-Милнера (HML) - это динамическая логика используется для указания свойств маркированная переходная система (LTS), структура похожая на автомат. Он был представлен в 1980 году Мэтью Хеннесси и Робин Милнер в своей статье «О наблюдении недетерминизма и параллелизма»^[1] (ИКАЛП ).

Другой вариант HML включает использование рекурсии для расширения выразимости логики и обычно называется «логикой Хеннесси-Милнера с рекурсией».^[2] Рекурсия включается с использованием максимальных и минимальных фиксированных точек.

Синтаксис

Формула определяется следующим Грамматика BNF за действовать некоторый набор действий:

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

То есть формулу можно

постоянная правда ${\displaystyle {\textit {tt}}}$

всегда правда

постоянная ложь ${\displaystyle {\textit {ff}}}$

всегда ложь

формула соединение

формула дизъюнкция

${\displaystyle \scriptstyle {[Act]\Phi }}$ формула

для всех действовать-производные, Φ должен держать

${\displaystyle \scriptstyle {\langle Act\rangle \Phi }}$ формула

для некоторых действовать-производная, Φ должен держать

Формальная семантика

Позволять ${\displaystyle L=(S,{\mathsf {Act}},\rightarrow )}$ быть маркированная переходная система, и разреши${\displaystyle {\mathsf {HML}}}$ - набор формул HML. Отношение выполнимости ${\displaystyle {}\models {}\subseteq (S\times {\mathsf {HML}})}$ связывает состояния LTS с формулами, которым они удовлетворяют, и определяется как наименьшее отношение, такое, что для всех состояний ${\displaystyle s\in S}$и формулы ${\displaystyle \phi ,\phi _{1},\phi _{2}\in {\mathsf {HML}}}$,

• ${\displaystyle s\models {\textit {tt}}}$,
• нет государства ${\displaystyle s\in S}$ для которого ${\displaystyle s\models {\textit {ff}}}$,
• если существует состояние ${\displaystyle s'\in S}$ такой, что ${\displaystyle s{\xrightarrow {a}}s'}$ и ${\displaystyle s'\models \phi }$, тогда ${\displaystyle s\models \langle a\rangle \phi }$,
• если для всех ${\displaystyle s'\in S}$ такой, что ${\displaystyle s{\xrightarrow {a}}s'}$ он считает, что ${\displaystyle s'\models \phi }$, тогда ${\displaystyle s\models [a]\phi }$,
• если ${\displaystyle s\models \phi _{1}}$, тогда ${\displaystyle s\models \phi _{1}\lor \phi _{2}}$,
• если ${\displaystyle s\models \phi _{2}}$, тогда ${\displaystyle s\models \phi _{1}\lor \phi _{2}}$,
• если ${\displaystyle s\models \phi _{1}}$ и ${\displaystyle s\models \phi _{2}}$, тогда ${\displaystyle s\models \phi _{1}\land \phi _{2}}$.

Смотрите также

• В модальное μ-исчисление, который расширяет HML с помощью операторы с фиксированной точкой
• Динамическая логика, мультимодальная логика с бесконечным множеством модальностей

Рекомендации

1. Хеннесси, Мэтью; Милнер, Робин (1980-07-14). О соблюдении недетерминизма и параллелизма. Автоматы, языки и программирование. Конспект лекций по информатике. Шпрингер, Берлин, Гейдельберг. С. 299–309. Дои:10.1007/3-540-10003-2_79. ISBN  978-3540100034.
2. Хольмстрем, Сорен (1990). «Логика Хеннесси-Милнера с рекурсией как язык спецификации и исчисление уточнения на его основе». Материалы семинара BCS-FACS по спецификации и верификации параллельных систем: 294–330.

Источники

• Колин П. Стирлинг (2001). Модальные и временные свойства процессов. Springer. стр.32 –39. ISBN  978-0-387-98717-0.
• Sören Holmström. 1988. "Логика Хеннесси-Милнера с рекурсией как язык спецификации и исчисление уточнения на его основе". В Материалы семинара BCS-FACS по спецификации и проверке параллельных систем, Чарльз Рэттрей (ред.). Springer-Verlag, Лондон, Великобритания, 294–330.