Name
Abstract | ||
|---|---|---|
We present Rabinizer 4, a tool set for translating formulae of linear temporal logic to different types of deterministic omega-automata. The tool set implements and optimizes several recent constructions, including the first implementation translating the frequency extension of LTL. Further, we provide a distribution of PRISM that links Rabinizer and offers model checking procedures for probabilistic systems that are not in the official PRISM distribution. Finally, we evaluate the performance and in cases with any previous implementations we show enhancements both in terms of the size of the automata and the computational time, due to algorithmic as well as implementation improvements. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-96145-3_30 | COMPUTER AIDED VERIFICATION (CAV 2018), PT I |
Field | DocType | Volume |
Model checking,Deterministic automaton,Computer science,Automaton,Algorithm,Linear temporal logic,Implementation,Theoretical computer science,Probabilistic logic | Conference | 10981 |
ISSN | Citations | PageRank |
0302-9743 | 2 | 0.37 |
References | Authors | |
33 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jan Křetínský | 1 | 190 | 12.05 |
| Tobias Meggendorfer | 2 | 15 | 3.90 |
| Salomon Sickert | 3 | 34 | 8.01 |
| Christopher Ziegler | 4 | 2 | 0.37 |