In model checking, properties are typically defined in linear temporal logic (LTL) and are translated into non-deterministic Biichi automata (NBA). In this paper, we propose a new, efficient translation method that is different from those used in LTL2BA, Spot and LTL3BA. Our method produces non-transition-based generalised Biichi automata (GBA) as an intermediate object, whereas LTL2BA, Spot, and LTL3BA use transition-based generalised Biichi automata (TGBA). Our method enables fast conversion because the data structure representing the object is simpler than that used in conversions via TGBA. Furthermore, we have developed techniques to reduce the number of states, similar to techniques that have heretofore only been available for conversions via TGBA. We also propose a technique to suppress the increase in the number of states that normally occurs while GBA is converted into NBA, using characteristics of strongly connected components of the GBA. We implemented our method with these techniques and experimentally compared our method with LTL2BA, Spot, and LTL3BA, which are the fastest translators to date. Our conversion method was much faster than LTL2BA and Spot, and was competitive with LTL3BA. In addition, the number of states in the NBA resulting from our method was comparable to that produced by LTL2BA, Spot, and LTL3BA.
展开▼
