论文部分内容阅读
In this paper, we present a conversion algorithm to translate a Linear temporal logic(LTL) formula to a Bu¨chi 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.
In this paper, we present a conversion algorithm to translate a Linear temporal logic (LTL) formula to a Bu¨chi 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 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.