Transformation from PLTL to automata via NFGs

A new linear transformation from PLTL formulas to alternating automata is proposed in this paper. To this end, C-F normal forms and normal form graphs (NFGs) are defined for PLTL formulas. Further, based on NFGs, generalized alternating Büchi automata (GABA) of PLTL formulas are built. Beside the conciseness in theoretical aspect, the new transformation is useful in improving the scalability of LTL model checking tools in practise. Also, based on the new transformation, an intuitive on-the-fly model checking approach can be implemented.