Логика Хеннесси-Милнера

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

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

Синтаксис

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

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

То есть формула может быть

постоянная истина ${\textit {tt}}$

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

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

всегда ложь

формула союз

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

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

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

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

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

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

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

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

См. также

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

Источники

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