Name
Abstract | ||
|---|---|---|
In model checking, properties are typically defined in linear temporal logic (LTL) and are translated into non-deterministic Buchi 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 Buchi automata (GBA) as an intermediate object, whereas LTL2BA, Spot, and LTL3BA usetransition-based generalised Buchi 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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-11737-9_24 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Data structure,Model checking,Computer science,Automaton,Linear temporal logic,Theoretical computer science,Strongly connected component,Büchi automaton | Conference | 8829 |
ISSN | Citations | PageRank |
0302-9743 | 1 | 0.37 |
References | Authors | |
11 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shohei Mochizuki | 1 | 1 | 0.70 |
| Masaya Shimakawa | 2 | 41 | 7.54 |
| Shigeki Hagihara | 3 | 78 | 12.33 |
| Naoki Yonezaki | 4 | 107 | 20.02 |