Model Checking via Reachability Testing for Timed Automata
Luca Aceto November 1997 |

## Abstract:In this paper we develop an approach to model-checking for
timed automata via reachability testing. As our specification formalism, we
consider a dense-time logic with clocks. This logic may be used to express
safety and bounded liveness properties of real-time systems. We show how to
automatically synthesize, for every logical formula , a so-called
The testable logic we consider is both of practical and
theoretical interest. On the practical side, we have used the logic, and the
associated approach to model-checking via reachability testing it supports,
in the specification and verification in UPPAAL of a collision
avoidance protocol. On the theoretical side, we show that the logic is
powerful enough to permit the definition of
Available as |

Last modified: 2003-06-08 by webmaster.