Logika Hennessy'ego-Milnera

W informatyce logika Hennessy'ego-Milnera (HML) to logika dynamiczna używana do określania właściwości oznakowanego systemu przejściowego (LTS), struktury podobnej do automatu . Został wprowadzony w 1980 roku przez Matthew Hennessy'ego i Robina Milnera w ich artykule „O obserwowaniu niedeterminizmu i współbieżności” ( ICALP ).

Inny wariant HML obejmuje użycie rekurencji w celu rozszerzenia wyrażalności logiki i jest powszechnie określany jako „logika Hennessy'ego-Milnera z rekurencją”. Rekurencja jest włączona z wykorzystaniem maksymalnych i minimalnych punktów stałych.

Składnia

Formuła jest zdefiniowana przez następującą gramatykę BNF dla wykonania pewnego zestawu działań:

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

Oznacza to, że formuła może być

stała prawda ${\ Displaystyle {\ textit {tt}}}$

zawsze prawdziwa

stała fałsz ${\ displaystyle {\ textit {ff}}}$

zawsze fałszywa

formuła koniunkcja

formuła dysjunkcja

${\ Displaystyle \ scriptstyle {[Akt ] \ Phi}}$ wzór

dla wszystkich pochodnych aktu , Φ musi być spełniony

$\ Displaystyle \ scriptstyle {\ langle Act \ rangle \ Phi}}$ wzór

na jakąś pochodną aktu , Φ musi być spełniony

Semantyka formalna

Niech ${\ Displaystyle L = (S, {\ mathsf {Akt}}, \ rightarrow )}$ będzie oznakowanym systemem przejściowym i niech ${\ Displaystyle {\ mathsf { HML}}}$ będzie zbiorem formuł HML. Relacja spełnialności ${\ Displaystyle {} \ modele {} \ subseteq (S \ razy {\ mathsf {HML}})}$ odnosi stany LTS do formuł, które spełniają, i jest definiowany jako najmniejsza relacja taka, że ​​dla wszystkich stanów i wzorów ${\ Displaystyle s \ in S}$ i formuł ${\ styl wyświetlania \ phi , \ phi _ {1}, \ phi _ {2} \ w {\ mathsf {HML}}}$ ,

• ${\ Displaystyle s \ modele {\ textit {tt}}}$ ,
• nie ma stanu, $\ Displaystyle s \ modele {\ textit {ff$ którego $}$ }
• jeśli istnieje stan taki, że $\ xrightarrow {a}} s'}$$Displaystyle s$$'\ modele \ phi }$ s , wtedy ${\ Displaystyle s \ modele \ langle a \ rangle \ phi}$ ,
• jeśli dla wszystkich ${\ Displaystyle s'\ w S}$ takie, że ${\ Displaystyle s {\ xrightarrow {a}} s'}$ utrzymuje, że ${\ Displaystyle s'\ modele \ phi }$ , wtedy ${\ Displaystyle s \ modele [a] \ phi}$ ,
• jeśli ${\ Displaystyle s \ modele \ phi _ {1}}$ , to ${\ Displaystyle s \ modele \ phi _ {1} \ lor \ phi _ {2}$ }
• jeśli ${\ Displaystyle s \ modele \ phi _ {2}}$ , to ${\ Displaystyle s \ modele \ phi _ {1} \ lor \ phi _ {2}$ }
• jeśli ${\ Displaystyle s \ modele \ phi _ {1}}$ i ${\ Displaystyle s \ modele \ phi _ {2}}$ , to ${\ Displaystyle s \ modele \phi _{1}\land \phi _{2}}$ .

Zobacz też

• modalny μ , który rozszerza HML o operatory punktów stałych
• Logika dynamiczna , logika multimodalna z nieskończenie wieloma modalnościami

Źródła

•   Colina P. Stirlinga (2001). Modalne i czasowe własności procesów . Skoczek. s. 32 –39. ISBN 978-0-387-98717-0 .
• Soren Holmström. 1988. „Logika Hennessy'ego-Milnera z rekurencją jako językiem specyfikacji i oparty na niej rachunek wyrafinowania”. W Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems , Charles Rattray (red.). Springer-Verlag, Londyn, Wielka Brytania, 294–330.