Temporal Logics and Model Checking for Fairly Correct Systems

Speaker(s)

Filip Murlak

Affiliation

Uniwersytet Warszawski

Date

March 21, 2007, 2:15 p.m.

Room

room 5870

Seminar

Seminar Automata Theory

---

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.

---