Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

PELÁNEK Radek LARSEN Kim G. BEHRMANN Gerd BOUYER Patricia

Year of publication 2006
Type Article in Periodical
Magazine / Source International Journal on Software Tools for Technology Transfer (STTT)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords model checking; timed automata; verification; abstraction; extrapolation
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.