Přednáška pro odbornou veřejnost v rámci řízení ke jmenování profesorem - doc. Jan Křetínský, Ph.D. (TUM)
Jménem předsedy hodnoticí komise prof. Kráľe si Vás dovolujeme pozvat na přednášku pro odbornou veřejnost v rámci řízení ke jmenování profesorem doc. Dr.rer. nat. RNDr. Mgr. Bc. Jana Křetínského, Ph.D. z TU Mnichov.
Přednáška doc. Křetínského proběhne v úterý 29. března 2022 ve 14 hod v posluchárně D2 v rámci Informatického kolokvia.
Název přednášky: A story of checking LTL models
Abstrakt: 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.
