LTL Formulae to Buchi Automata Translation Using on-the-Fly De-generalization

摘要

In this paper, we present a conversion algorithm to translate a Linear temporal logic (LTL) formula to a Buchi automaton (BA) directly. Acceptance degree (AD) is presented to record acceptance conditions satisfied in each state and transition of the BA. According to AD, on-the-fly de-generalization algorithm, which is different from the standard de-generalization algorithm, is conceived and implemented. On-the-fly de-generalization algorithm is performed in the case of the given LTL formula containing U-subformulae or F-subformulae, that is, it is performed as required during the expansion of the given LTL formula. We compare the conversion algorithm presented in this paper to previous works, and show that it is more efficient for a series of LTL formulae in common use.