Lower and upper bounds in zone-based abstractions of timed automata

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 ob...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2006-06, Vol.8 (3), p.204-215
Main Authors: Behrmann, Gerd, Bouyer, Patricia, Larsen, Kim G., Pelánek, Radek
Format: Article
Language:English
Subjects:
Algorithms
Automation
Scalability
Semantics
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 and 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 increase the scalability of the real-time model checker UPPAAL. [PUBLICATION ABSTRACT]
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-005-0190-0