What is it about?
This algorithm is used to translate Linear Temporal Logic (LTL) formulas to automata, which can be used by an LTL model checker. The principle of this algorithm is based on generating alternating automata that contain only positive transitions without generating the intermediate generalized automata.
Featured Image
Why is it important?
This translator is different from the others and it is very competitive with the most efficient translators. This LTL translator generates small and more deterministic automata in time that is less than the time spent by the other translators.
Perspectives
The perspective of this work is to use this algorithm with different LTL model checkers
Mustapha Bourahla
Computer Science Department, University of M'Sila, Algeria
Read the Original
This page is a summary of: LTL Transformation Modulo Positive Transitions , IET Computers & Digital Techniques, August 2017, the Institution of Engineering and Technology (the IET),
DOI: 10.1049/iet-cdt.2017.0112.
You can read the full text:
Resources
Contributors
The following have contributed to this page
