| Identifikační kód | RIV/00216224:14330/13:00066204 |
|---|
| Název v anglickém jazyce | Rabinizer 2: Small Deterministic Automata for LTLGU |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2013 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 2 |
|---|
| Počet tvůrců celkem | 2 |
|---|
| Počet domácích tvůrců | 1 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Jan Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3503054)
Ruslan Ledesma Garza (státní příslušnost: MX - Spojené státy mexické) |
|---|
| Popis výsledku v anglickém jazyce | We present a tool that generates automata for LTL(X,F,G,U) where U does not occur in any G-formula (but F still can). The tool generates deterministic generalized Rabin automata (DGRA) significantly smaller than deterministic Rabin automata (DRA) generated by state-of-the-art tools. For complex properties such as fairness constraints, the difference is in orders of magnitude. DGRA have been recently shown to be as useful in probabilistic model checking as DRA, hence the difference in size directly translates to a speed up of the model checking procedures. |
|---|
| Klíčová slova oddělená středníkem | linear temporal logic; automata; determinism; synthesis; probabilistic model checking |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-319-02444-8_32 |
|---|