Hi,
einige Fragen:
-LTL —-> PSPACE Vollständig
-CTL—–> exponentiell!? durch OBBDS —> polynomieller Komplexität?

-Wieso hat man überhaupt LTL im Skript angegeben?Die Komplexität ist
doch PSPACE Vollständig
-Exponentiell ist eine Schlechte Komplexität,Wieso sthet im Skript Formeln in CTL wegen besserer Komplexität?(besser als was? Als LTL?)
-Was hat die Faire Semantik mit all dem zutun.
In diesem Abschnitt des Skripts hab Ich die zusammenhänge nicht verstanden.Bitte um Hilfe.
Danke schonmal in voraus.

Hi,
einige Fragen:
-LTL —-> PSPACE Vollständig
-CTL—–> exponentiell!? durch OBBDS —> polynomieller Komplexität?

Wieso ist CTL denn exponentiell? Im Skript steht doch, dass eine Formel f in Zeitkomplexität O(|f|*(|S|+|R|) nachgeprüft werden kann! Das sieht für mich nicht allzu exponentiell aus. Die Komplexität wächst linear mit der Formel und linear mit der Grösse des Modells. Das Modell selber wächst exponentiell, oder?

-Wieso hat man überhaupt LTL im Skript angegeben?Die Komplexität ist
doch PSPACE Vollständig

Es gibt Formeln, die nicht durch CTL dargestellt werden können, vielleicht kommt man um LTL nicht immer herum?

-Exponentiell ist eine Schlechte Komplexität,Wieso sthet im Skript Formeln in CTL wegen besserer Komplexität?(besser als was? Als LTL?)

Besser als CTL*

-Was hat die Faire Semantik mit all dem zutun.

Fairness ist nicht ausdrückbar in CTL. Da man aber nach Möglichkeit trotzdem lieber CTL als CTL* benutzt (dort ist Fairness ausdrückbar), "erweitert" man sein Modell so, dass man Formeln aus CTL trotzdem auf Fairness überprüfen kann.

Alles ohne Gewähr auf Korrektheit natürlich [img]http://www.fb18.de/gfx/25.gif[/img]