Temporal Logics and Model Checking for Fairly Correct Systems

Prelegent(ci)

Filip Murlak

Afiliacja

Uniwersytet Warszawski

Termin

21 marca 2007 14:15

Pokój

p. 5870

Seminarium

Seminarium „Teoria automatów”

---

I will present recent results on model checking for fairly correct systems (D. Varacca, H. Voelzer, LICS'06). A fair variant of a specfication is obtained by replacing "for all paths" by "for a large set of paths". For regular linear-time specifications, probabilistic and topological largness coincide. Hence, by results on probabilistic model checking, fair variants of LTL, omega-regular, and CTL* specifications are not harder to check than the originals. For CTL, the linear model checking algorithm can be adapted to the fair variant.

---