You are not logged in | Log in

Temporal Logics and Model Checking for Fairly Correct Systems

Filip Murlak
Uniwersytet Warszawski
March 21, 2007, 2:15 p.m.
room 5870
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.