Other formats:
BibTeX
LaTeX
RIS
@inproceedings{562991,
author = {Pelánek, Radek and Larsen, Kim G. and Behrmann, Gerd and Bouyer, Patricia},
address = {Barcelona (Španělsko)},
booktitle = {Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004)},
keywords = {model checking; timed automata; abstraction},
language = {eng},
location = {Barcelona (Španělsko)},
isbn = {3-540-21299-X},
pages = {312-326},
publisher = {Springer-Verlag},
title = {Lower and Upper Bounds in Zone Based Abstractions of Timed Automata},
year = {2004}
}
TY - JOUR
ID - 562991
AU - Pelánek, Radek - Larsen, Kim G. - Behrmann, Gerd - Bouyer, Patricia
PY - 2004
TI - Lower and Upper Bounds in Zone Based Abstractions of Timed Automata
PB - Springer-Verlag
CY - Barcelona (Španělsko)
SN - 354021299X
KW - model checking
KW - timed automata
KW - abstraction
N2 - Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions wrt. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds we can obtain significantly coarser abstractions. We show the soundness and completeness of the new abstractstions wrt. reachability and we experimentaly demonstrate their advantages. We demonstrate how information about lower and upper boudns 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.
ER -
PELÁNEK, Radek, Kim G. LARSEN, Gerd BEHRMANN and Patricia BOUYER. Lower and Upper Bounds in Zone Based Abstractions of Timed Automata. In \textit{Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004)}. Barcelona (Španělsko): Springer-Verlag, 2004, p.~312-326. ISBN~3-540-21299-X.
|
