Kann jemand denn zusammenhang zwischen Fixpunkt und Mu-Kalkül erklären?

Hey…

kannst du die Frage mehr ausführen, bitte? (Bitte auch mit Quelle (also Seitenzahl etc.), wenn
es etwas mit dem FGI-3 Skript zu tun haben sollte.) Sonst weiss ich nämlich nicht so recht, was
ich schreiben soll ;-)

Der mu-Calculus ist ja eine Logik, die auf der Berechnung von Fixpunkten von Funktionen 2^S -> 2^S
basiert. (S ist dabei die Menge von Zustaenden einer Kripke-Struktur.) Es macht dann Sinn Fixpunkte
solcher Funktionen zu suchen/zu betrachten und um diese Fixpunkte auszudrücken gibt es in der
Logik selbst (also in den Formeln des mu-Calculus) ja auch Operatoren.

Was genau willst du jetzt wissen, bzw. wo gibt es Probleme? Sinn des mu-Calculus (sprich: Motivation)?
Syntax vom mu-Calculus? Semantik vom mu-Caluculs? Was ist ein Fixpunkt? Wie kann man die berechnen?
Tarski/Knaster Fixpunkttheorem? …

Frank :)

Wenn wir automatisiert verifizieren wollen, benutzen wir dann immer den mu-kalkül oder reicht auch CTL? (Wie hängt CTL mit dem mu-kalkül zusammen?)

Lässt sich mit CTL auch Sicherheit und Lebendigkeit prüfen oder geht das nur mit dem mu-kalkül?

Ist der kleinste Fixpunkt zum zeigen der Lebendigkeit und der größte zum zeigen der Sicherheit da? Und wieso sagt der Fixpunkt etwas über die Lebendigkeit/Sicherheit aus?

Wie hängt das automatisierte verifizieren mit dem Fixpunkt zusammen?

Hey…

sorry, ich kam die Woche über nicht zum Schreiben. Ist dir denn eigentlich die Syntax und Semantik
vom mu-Kalkül klar? Sonst müsste man weit ausholen, um das sinnvoll zu erklären. Und welche
Literatur benutzt du überhaupt?

Wenn wir automatisiert verifizieren wollen, benutzen wir dann immer den mu-kalkül oder reicht auch CTL?

Du benutzt natürlich nicht *immer* den mü-Kalkül. So wie sich die Systeme/Eigenschaften, die du
verifizieren willst unterscheiden, musst du da auch mit unterschiedlichen Werkzeugen rangehen.
Bei probabilistischen Systemen z.B. anders…

(Wie hängt CTL mit dem mu-kalkül zusammen?)

Kann man als Teillogik ansehen.

Lässt sich mit CTL auch Sicherheit und Lebendigkeit prüfen oder geht das nur mit dem mu-kalkül?

Was meinst du mit Sicherheit und Lebendigkeit? Das sind keine festen Begriffe. Meinst du Lebendigkeit
im "Petri-Netz-Sinn"? Und Sicherheit?

Ich weiss irgendwie immer noch nicht so recht, was ich schreiben soll…. soll ich Fixpunkte allgemein
und dann Syntax und Semantik des mü-Kalküls erklären?

Wofür brauchst du das eigentlich? In FGI3 kommt das doch gar nicht dran, oder?
Wobei ich Lernende nicht aufhalten will ;-)

Frank :)

Frank hat wohl Recht: im Logikteil (von FGI-3) sah ich im Skript nichts vom mu-Kalkül und im Semantikteil (von FGI-3) kamen zwar Fixpunkte vor, aber nicht im Zusammenhang, mit dem mu-Kalkül. Wenn schon im Zusammenhang mit Kalkülen, dann eher noch mit dem Lambda-Kalkül, wo gezeigt wurde, dass auch dort Fixpunkte von Funktionen existieren und ein Fixpunktoperator durch einen Lambda-Ausdruck dargestellt werden kann. Dadurch wird deutlich, dass jede µ-rekursive Funktion im Lambda-Kalkül berechnet werden kann…

Grundlage ist Emerson und Clarke (Model Checking). Es geht also nicht direkt um den Vorlesungsstoff.

Wenn wir mit dem mu-kalkül einem Fixpunkt einer Formel berechnen: Womit vergleichen wir den um zu sehen ob die Formel gültig ist? Bzw. was sagt der Fixpunkt aus?

Hey…

sorry, ich hatte etwas viel um die Ohren und bin hierzu nicht mehr gekommen.

Wie steht's denn? Ist dir mittlerweile einiges klarer? Soll ich noch was schreiben?

Frank :)

Okey, scheinbar hat die Frage sich von alleine geklärt. Falls mal jemand anderes
auf diesen Thread stösst, noch zwei schöne Literaturtipps hierfür:

1) Logic in Computer Science: Modelling and Reasoning about Systems
von Michael Huth und Mark Ryan
Cambridge University Press, 2nd Ed., 2004
* sehr schönes Buch allgemein zum Thema Logik und Verifikation.
Steht z.B. viel zu CTL und LTL drin und zu den Model-Checking
Algorithmen. Enthält einen sehr schöner Abschnitt zum Thema Fixpunkt-
Theorie (und CTL) und darum steht das hier ;-)

2) Verification of Reactive Systems. Formal Methods and Algorithms
von Klaus Schneider
Springer, 2004
* Sehr ausführliches und tief gehendes Buch zum Thema Verifikation.
Der mü-Kalkül wird hier intensiv behandelt.

Viel Spass beim Lesen! :-)

Frank :)