Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

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	2004
Type	Article in Proceedings
Conference	Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004)
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	model checking; timed automata; abstraction
Description	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.
Related projects:	Automated Verification of Parallel and Distributed Systems Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing