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

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

Другой вариант 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 }}$формула

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

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

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

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

Пусть будет помеченной системой переходов , и пусть будет множеством формул HML. Отношение выполнимости связывает состояния LTS с формулами, которым они удовлетворяют, и определяется как наименьшее отношение, такое что для всех состояний и формул , ${\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}}}$,
• нет такого государства , для которого , ${\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). «О наблюдении недетерминизма и параллелизма». Автоматы, языки и программирование . Конспект лекций по информатике. Том 85. Springer, Берлин, Гейдельберг. С. 299–309. doi :10.1007/3-540-10003-2_79. ISBN 978-3540100034.
2. Хольмстрём, Сёрен (1990). «Логика Хеннесси-Милнера с рекурсией как языком спецификации и исчислением уточнения на его основе». Спецификация и проверка параллельных систем . Практикумы по вычислениям. стр. 294–330. doi :10.1007/978-1-4471-3534-0_15. ISBN 978-3-540-19581-8.

Источники

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