LTL transformation modulo positive transitions

摘要

In this study, the author presents a new efficient algorithm for translating linear temporal logic (LTL) formulas to Büchi automata, which are used by LTL model checkers. The general idea of this algorithm is to generate Büchi automata from LTL formulas, using the principle of alternating automata and keeping only the positive transitions without generating the intermediate generalised automata. The LTL translation is the heart of any LTL model checker, which affects its performance. The translation performance is measured in addition to its speed and the size of the produced Büchi automaton (number of states and number of transitions), by correctness of produced Büchi automaton and its level of determinism. The author will show that this method is different from the others and it is very competitive with the most efficient translators to date.