Name
Abstract | ||
|---|---|---|
We present Rabinizer, a tool for translating formulae of the fragment of linear temporal logic with the operators F (eventually) and G (globally) into deterministic Rabin automata. Contrary to tools like ltl2dstar, which translate the formula into a Büchi automaton and apply Safra's determinization procedure, Rabinizer uses a direct construction based on the logical structure of the formulae. We describe a number of optimizations of the basic procedure, crucial for the good performance of Rabinizer, and present an experimental comparison. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-33386-6_7 | ATVA |
Keywords | Field | DocType |
determinization procedure,small deterministic automaton,operators F,linear temporal logic,basic procedure,good performance,experimental comparison,direct construction,deterministic Rabin automaton,logical structure,chi automaton | Discrete mathematics,Deterministic automaton,Computer science,Automaton,Linear temporal logic,Structure (mathematical logic),Operator (computer programming),Probabilistic model checking,Büchi automaton | Conference |
Citations | PageRank | References |
18 | 0.84 | 10 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Gaiser | 1 | 42 | 1.93 |
| Jan Křetínský | 2 | 190 | 12.05 |
| Javier Esparza | 3 | 770 | 60.33 |