Es ist bekannt, dass die zeitliche Logik LTL, CTL, CTL * in den Kalkül übersetzt / eingebettet werden kann. Mit anderen Worten, der (modale) Kalkül fasst diese Logik zusammen (dh er ist ausdrucksvoller).
Könnten Sie mir bitte erklären / auf Papiere / Bücher verweisen, die diese Angelegenheit näher erläutern? Gibt es insbesondere konkrete Eigenschaften für Fairness, Lebendigkeit usw., die nicht in der zeitlichen Logik, sondern im Kalkül zum Ausdruck kommen?
Der Kalkül ist streng ausdrucksstärker als LTL, CTL und CTL *. Dies ist eine Folge einiger unterschiedlicher Ergebnisse.μ
Der erste Schritt besteht darin zu zeigen, dass der Kalkül so ausdrucksstark ist wie die zeitliche Logik. Die Hauptidee für die Codierung dieser Logiken besteht darin, zeitliche Eigenschaften als Fixpunkte zu erkennen. Auf einer sehr informellen Ebene können Sie mit den kleinsten Fixpunkten Eigenschaften endlicher Natur ausdrücken, und die größten Fixpunkte gelten für unendliche Eigenschaften. Zum Beispiel definiert schließlich φ in LTL, dass es in der endlichen Zukunft einen Moment gibt, zu dem φ wahr ist, während φ immer angibt, dass φμ φ φ φ φ ist wahr in einer unendlichen Anzahl von zukünftigen Zeitschritten. In Bezug auf Fixpunkte würde die Eigenschaft eventuell unter Verwendung eines kleinsten Fixpunkts und die Eigenschaft always unter Verwendung eines größten Fixpunkts ausgedrückt. Nach einer solchen Intuition können zeitliche Operatoren als Festpunktoperatoren codiert werden.
Der nächste Schritt besteht darin zu zeigen, dass der Kalkül ausdrucksvoller ist. Die Hauptidee ist die Wechseltiefe. Fixpunkte wechseln sich ab, wenn ein kleinster Fixpunkt den größten Fixpunkt beeinflusst und umgekehrt. Die Wechseltiefe einer μ- Kalkülformel zählt die Anzahl der darin auftretenden Wechsel. Die Operatoren in CTL können durch μ- Kalkülformeln mit Wechseltiefe 1 codiert werden . Die Operatoren in CTL * und LTL können durch μ- Kalkülformeln mit einer Wechseltiefe von höchstens 2 codiert werden . Die Wechselhierarchie der μμ μ μ 1 μ 2 μ -calculus ist streng, was bedeutet, dass Sie mit zunehmender Wechseltiefe in einer Formel streng mehr Eigenschaften ausdrücken können. Aus diesem Grund sagen die Leute, dass der Kalkül ausdrucksvoller ist als diese zeitliche Logik.μ
Einige Referenzen:
quelle
Es ist gut bekannt, dassμ EIN μ X.. A ∧ □ □ X.
quelle