PLTL: Algorithmen

Satz: die folgenden Fragen sind entscheidbar:

Beweis-Idee: die Mengen {wΣω | 1 = wert(F, w, 0)}

sind ω-regulär (Def. auf nächster Folie)

und lassen sich durch endliche Automaten beschreiben.

(J. R. Büchi 1962, A. Pnueli 1977)



Johannes Waldmann 2013-06-18