| Identifikační kód |
RIV/00216224:14330/06:00015564 |
| Název v anglickém jazyce |
Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata |
| Druh |
J - Recenzovaný odborný článek (Jimp, Jsc a Jost) |
| Poddruh |
- |
| Jazyk |
eng - angličtina |
| Obor - skupina |
I - Informatika |
| Obor |
IN - Informatika |
| Rok uplatnění |
2006 |
| 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 |
6 |
| Počet tvůrců celkem |
4 |
| Počet domácích tvůrců |
1 |
| Výčet všech uvedených jednotlivých tvůrců |
Radek Pelánek (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 4686128)
Gerd Behrmann (státní příslušnost: DK - Dánské království)
Patricia Bouyer (státní příslušnost: FR - Francouzská republika)
Kim G. Larsen (státní příslušnost: DK - Dánské království) |
| Popis výsledku v anglickém jazyce |
Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions w.r.t. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t. reachability. We demonstrate how information about lower and upper bounds can be used to optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker Uppaal. |
| Klíčová slova oddělená středníkem |
model checking; timed automata; verification; abstraction; extrapolation |
| Stránka www, na které se nachází výsledek |
- |
| Odkaz na údaje z výzkumu |
- |