Ronald de Haan

Date: 17:00, Thursday, December 17, 2015
Speaker: Ronald de Haan
Venue: TU Wien

The model checking problem for temporal logics is an important problem with applications in key areas of computer science. Indispensable for the state-of-the-art in solving this problem in large-scale settings is the technique of bounded model checking. We investigate the theoretical possibilities of this technique using parameterized complexity. In particular, we provide a complete parameterized complexity classification for the model checking problem for symbolically represented Kripke structures for various fragments of the temporal logics LTL, CTL and CTL*. We argue that a known result from the literature for a restricted fragment of LTL can be seen as an fpt-time encoding into SAT, and show that such encodings are not possible for any of the other fragments of the temporal logics that we consider.

Posted in RiSE Seminar