| Identifikační kód | RIV/00216224:14330/12:00062426 |
|---|
| Název v anglickém jazyce | Time-Darts: A Data Structure for Verification of Closed Timed Automata |
|---|
| Druh | J - Článek v odborném periodiku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2012 |
|---|
| 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 | 1 |
|---|
| Počet tvůrců celkem | 3 |
|---|
| Počet domácích tvůrců | 1 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Kenneth Yrke Joergensen (státní příslušnost: DK - Dánské království)
Kim G. Larsen (státní příslušnost: DK - Dánské království)
Jiří Srba (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2753057) |
|---|
| Popis výsledku v anglickém jazyce | Symbolic data structures for model checking timed systems have been subject to a significant research, with Difference Bound Matrices (DBMs) still being the preferred data structure in several mature verification tools. In comparison, discretization offers an easy alternative, with all operations having linear-time complexity in the number of clocks, and yet valid for a large class of closed systems. Unfortunately, fine-grained discretization causes itself a state-space explosion. We introduce a new data structure called time-darts for the symbolic representation of state-spaces of timed automata. Compared with the complete discretization, a single time-dart allows to represent an arbitrary large set of states, yet the time complexity of operations ontime-darts remain linear in the number of clocks. We prove the correctness of the suggested reachability algorithm and perform several experiments in order to compare the performance of time-darts and the complete discretization. |
|---|
| Klíčová slova oddělená středníkem | verification; timed automata; reachability; discretization |
|---|
| Stránka www, na které se nachází výsledek | http://dx.doi.org/10.4204/EPTCS.102.13 |
|---|
| DOI výsledku | 10.4204/EPTCS.102.13 |
|---|