In explicit-state model checking, system proper- ties are typically expressed in linear temporal logic （LTL）, and translated into a BUchi automaton （BA） to be checked. In order to improve performance of the conver...In explicit-state model checking, system proper- ties are typically expressed in linear temporal logic （LTL）, and translated into a BUchi automaton （BA） to be checked. In order to improve performance of the conversion algo- rithm, some model checkers involve the intermediate au- tomata, such as a generalized Btichi automaton （GBA）. The de-generalization is a translation from a GBA to a BA. In this paper, we present a conversion algorithm to translate an LTL formula to a BA directly. A labeling, acceptance degree, is presented to record acceptance conditions sat- isfied in each state and transition. Acceptance degree is a set of U-subformulae or F-subformulae of the given LTL formula. According to the acceptance degree, 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 carried out during the expansion of the given LTL formula. It is performed in the case of the given LTL formula contains U-subformulae and F-subformulae, that is, the on-the-fly de-generalization algorithm is performed as required. In order to get a more deterministic BA, the shannon expansion is used recursively during expanding LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae. We compare the conversion algorithm presented in this paper to previous works, and show that it is more efficient for five families LTL formulae in common use and four setsof random formulae generated by LBTT （an LTL-to-BUchi translator testbench）.展开更多
文摘In explicit-state model checking, system proper- ties are typically expressed in linear temporal logic （LTL）, and translated into a BUchi automaton （BA） to be checked. In order to improve performance of the conversion algo- rithm, some model checkers involve the intermediate au- tomata, such as a generalized Btichi automaton （GBA）. The de-generalization is a translation from a GBA to a BA. In this paper, we present a conversion algorithm to translate an LTL formula to a BA directly. A labeling, acceptance degree, is presented to record acceptance conditions sat- isfied in each state and transition. Acceptance degree is a set of U-subformulae or F-subformulae of the given LTL formula. According to the acceptance degree, 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 carried out during the expansion of the given LTL formula. It is performed in the case of the given LTL formula contains U-subformulae and F-subformulae, that is, the on-the-fly de-generalization algorithm is performed as required. In order to get a more deterministic BA, the shannon expansion is used recursively during expanding LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae. We compare the conversion algorithm presented in this paper to previous works, and show that it is more efficient for five families LTL formulae in common use and four setsof random formulae generated by LBTT （an LTL-to-BUchi translator testbench）.
