Search
 
loader loading subjects...
cover
A class of automata for computing reachability relations in timed systems
Cătălin Dima
69 - 89
NATO Security through Science Series - D: Information and Communication Security
Volume 1: Verification of Infinite-State Systems with Applications to Security
Abstract

We give an algorithmic calculus of the reachability relations on clock values defined by timed automata. Our approach is a modular one, by computing unions, compositions and reflexive-transitive closure (star) of “atomic” relations. The essential tool is a new representation technique for n-clock relations – the 2n-automata – and our strategy is to show the closure under union, composition and star of the class of 2n-automata that represent reachability relations in timed automata.

$35.00 / €27.50 / £22.00
Add PDF to cart