Public talk within a professorship procedure of doc. Jan Křetínský, Ph.D. (TU Munich)
On behalf of the chairman of the evaluation committee, Prof. Kráľ, we would like to invite you to the public talk within a professorship procedure of doc. Dr.rer.nat RNDr. Mgr. Bc. Jan Křetínský, Ph.D. (TUM).
Title of the lecture: A story of checking LTL models
Abstract: Linear temporal logic (LTL) belongs to the most popular formalisms for specification of dynamic systems. Assuring that a safety-critical system behaves correctly can thus be formalized as the problem of LTL model checking, i.e., deciding whether an LTL formula is satisfied by the given system. Both the satisfaction definition and the techniques used in model checking differ depending on the type of the system. Nevertheless, a surprising commonality of most of the solutions is resorting to automata theory. In this talk, we survey the LTL model checking problems, focusing on the automata-theoretic solution approach. In particular, we highlight some of the recent advances for more complex systems, where the notion of determinism of automata plays a crucial role.
