Abstract

Computational complexity of model checking is the reason, why researchers are trying to find ways how to lower the amount of memory and time needed for the model checking procedure. When considering specification formulae for model checking only from the fragment LTL(F,G), there is a way how to translate the specification formula into a finite disjunction of formulae in special form called alpha-formulae. Then, instead of verifying the original formula, we verify every formula in the disjunction. The implementation of this translation of formulae from the fragment LTL(F,G) into the finite disjunction of alpha-formulae is the main objective of this thesis. Since every alpha-formula can be easily translated into a Büchi automaton and there is a strong probability that this automaton will be significantly smaller than the automaton obtained by traditional translation of LTL formulae into Büchi automata, the translation of alpha-formula into a Büchi automaton will be implemented as well. Afterwards, model checking of alpha-formulae will be evaluated within the DiVinE environment. …víceméně