Open AccessLTL transformation modulo positive transitions
Author(s) -
Bourahla Mustapha
Publication year - 2017
Publication title -
iet computers and digital techniques
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.219
H-Index - 46
ISSN - 1751-861X
DOI - 10.1049/iet-cdt.2017.0112
Subject(s) - modulo , automaton , correctness , linear temporal logic , model checking , computer science , translation (biology) , büchi automaton , temporal logic , theoretical computer science , discrete mathematics , algorithm , mathematics , deterministic automaton , biochemistry , chemistry , messenger rna , gene
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.