Abstract

The intended thesis is focused on properties of Linear time logic (LTL) and possible solutions of state explosion problem in context of LTL model checking. Although current partial order reduction algorithms solve the problem for stutter-invariant fragment of LTL, the problem for the general case remains open. Recently introduced n-stuttering and general stuttering principles provide a theoretical background for reductions applicable to full LTL. Moreover, for stutter-invariant fragment the reduced system can be even smaller than the output of current reduction algorithms. Besides theoretical research on LTL properties we aim to develop reduction algorithms based on new stuttering principles as well. …víceméně