| PELÁNEK, Radek, Kim G. LARSEN, Gerd BEHRMANN and Patricia BOUYER. Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2006, vol. 8, No 3, p. 204-215. ISSN 1433-2779. |
Other formats:
BibTeX
LaTeX
RIS
@article{585922,
author = {Pelánek, Radek and Larsen, Kim G. and Behrmann, Gerd and Bouyer, Patricia},
article_number = {3},
keywords = {model checking; timed automata; verification; abstraction; extrapolation},
language = {eng},
issn = {1433-2779},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
title = {Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata},
volume = {8},
year = {2006}
}
TY - JOUR
ID - 585922
AU - Pelánek, Radek - Larsen, Kim G. - Behrmann, Gerd - Bouyer, Patricia
PY - 2006
TI - Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata
JF - International Journal on Software Tools for Technology Transfer (STTT)
VL - 8
IS - 3
SP - 204-215
EP - 204-215
PB - Springer-Verlag GmbH
SN - 14332779
KW - model checking
KW - timed automata
KW - verification
KW - abstraction
KW - extrapolation
N2 - 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.
ER -
PELÁNEK, Radek, Kim G. LARSEN, Gerd BEHRMANN and Patricia BOUYER. Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata. \textit{International Journal on Software Tools for Technology Transfer (STTT)}. Springer-Verlag GmbH, 2006, vol.~8, No~3, p.~204-215. ISSN~1433-2779.
|
