Hennessy–Milner logic とは

コンピュータサイエンスでは、ヘネシーミルナーロジック(HML)は、オートマトンに似た構造のラベル付き遷移システム(LTS)のプロパティを指定するために使用される動的ロジックです。 Matthew HennessyとRobin Milnerが1980年に「非決定性と並行性を観察する」(ICALP)の論文で紹介されました。
HMLのもう一つの変種は、論理の表現可能性を拡張するための再帰の使用を含み、一般に「再帰を伴うHennessy-Milner論理」と呼ばれる。再帰は、最大および最小の固定小数点を使用して有効になります。