Benutzer:DerSpezialist/Hennessy-Milner-Logik

Dieser Artikel (Hennessy-Milner-Logik) ist im Entstehen begriffen und noch nicht Bestandteil der freien Enzyklopädie Wikipedia.

Wenn du dies liest:

• Der Text kann teilweise in einer Fremdsprache verfasst, unvollständig sein oder noch ungeprüfte Aussagen enthalten.
• Wenn du Fragen zum Thema hast, nimm am besten Kontakt mit dem Autor DerSpezialist auf.

Wenn du diesen Artikel überarbeitest:

• Bitte denke daran, die Angaben im Artikel durch geeignete Quellen zu belegen und zu prüfen, ob er auch anderweitig den Richtlinien der Wikipedia entspricht (siehe Wikipedia:Artikel).
• Nach erfolgter Übersetzung kannst du diese Vorlage entfernen und den Artikel in den Artikelnamensraum verschieben. Die entstehende Weiterleitung kannst du schnelllöschen lassen.
• Importe inaktiver Accounts, die länger als drei Monate völlig unbearbeitet sind, werden gelöscht.

Vorlage:Importartikel/Wartung-2019-07

In der theoretischen Informatik ist die Hennessy-Milner-Logic (kurz HML) eine dynamische Logik, um die Eigenschaften eines markierten Transitionssystems (englisch labeled transition system, kurz LTS) zu spezifizieren. Sie wurde von Matthew Hennessy und Robin Milner in ihrem Paper von 1980 eingeführt.

Eine Variante von HML verwendet Rekursion, um die Ausdrucksstärke zu erweitern. Sie ist bekannt als Hennessy-Milner Logic with recursion. Rekursion wird durch kleinste und größte Fixpunkte realisiert.

Syntax

Die Menge der HML-Formeln wird durch die folgende BNF-Grammatik definiert; dabei ist $Act$ eine gegebene Menge von Aktionen:

$\Phi ::=\mathrm {tt} \;|\;\mathrm {ff} \;|\;\Phi \land \Phi \;|\;\Phi \lor \Phi \;|\;\langle Act\rangle \Phi \;|\;[Act]\Phi$

Beispiele für Formeln sind also $\langle a\rangle [b]\mathrm {tt}$, $[a]([b]\mathrm {tt} \land \langle c\rangle \mathrm {ff}$).

Semantik

Sei $(S,{\mathit {Act}},\to )$ ein markiertes Transitionssystem. Die Relation $\to$ ist dreistellig: Sie bindet zwei Elemente $s,t\in S$ und ein $a\in {\mathit {Act}}$, was meist $s{\overset {a}{\to }}t$ oder vertikalen Platz sparend $s\to ^{a}t$ notiert wird.

Die Erfüllbarkeitsrelation $\models$ ist die kleinste Relation auf $S$ und der Menge der HML-Formeln, die die folgenden Bedingungen erfüllt. Dabei sind $s,t\in S$, $a\in {\mathit {Act}}$ und $\phi ,\phi _{0},\phi _{1}$ beliebige HML-Formeln.

• Stets gelte $s\models \mathrm {tt}$.
• Es gelte $s\models \langle a\rangle \phi$, falls $t\models \phi$ für ein $t\in S$ mit $s{\overset {a}{\to }}t$ gilt.
• Es gelte $s\models [a]\phi$, falls $t\models \phi$ für alle $t\in S$ mit $s{\overset {a}{\to }}t$ gilt.
• Es gelte $s\models \phi _{0}\land \phi _{1}$, falls $s\models \phi _{0}$ und $s\models \phi _{1}$.
• Es gelte $s\models \phi _{0}\lor \phi _{1}$, falls $s\models \phi _{0}$ oder $s\models \phi _{1}$.

Äquivalente LTS-Zustände erfüllen genau die gleichen HML-Formeln. Entsprechend können nicht-äquivalente LTS-Zustände durch eine geeignete HML-Formel unterschieden werden. Das gilt sowohl für Zustände desselben LTS als auch für Zustände in zwei verschiedenen LTS.

Ein hervorstechender Spezialfall ist $s\models [a]\phi$ in dem Fall, dass kein Zustand $t\in S$ mit $s{\overset {a}{\to }}t$ exisitert. Dann gilt $s\models [a]\phi$ trivialerweise nach der Interpretation des Wortes alle in Formalwissenschaften. Damit kann die Aussage, dass in $s$ kein Übergang mit $a$ zur Verfügung steht, mit $[a]\mathrm {ff}$ kodiert werden.

Es gibt keine Negation in der Syntax von HML. Die Negation einer HML-Formel kann jedoch berechnet werden.

• $\neg \mathrm {tt} =\mathrm {ff}$
• $\neg \mathrm {ff} =\mathrm {tt}$
• $\neg \langle a\rangle \phi =[a]\neg \phi$
• $\neg [a]\phi =\langle a\rangle \neg \phi$
• $\neg (\phi _{0}\land \phi _{1})=\neg \phi _{0}\lor \neg \phi _{1}$
• $\neg (\phi _{0}\lor \phi _{1})=\neg \phi _{0}\land \neg \phi _{1}$

Offenbar ist $\neg \neg \phi =\phi$. Insbesondere gilt $s\models \neg \phi$ genau dann, wenn $s\not \models \phi$.

Siehe auch

• Modaler μ-Kalkül, der HML um Fixpunktoperatoren ergänzt
• Dynamsche Logik, eine multi-modale Logik mit unendlich vielen Modalitäten

Quellen

• ISBN 978-0-387-98717-0.
• Sören Holmström. 1988. "Hennessy-Milner Logic with Recursion as a Specification Language, and a Refinement Calculus based on It". In Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, Charles Rattray (Ed.). Springer-Verlag, London, UK, 294–330.

[[:Kategorie:Informatik]] [[:Kategorie:Logik]] [[:Kategorie:Parallelverarbeitung]]