Model checking of real-time reachability properties using abstractions (full version

Abstract. Practical real-time model checking suers from the state-explosion problem: the size of the state space grows exponentially with many system parameters: number of clocks, size of constants, number of system components. To cope with state explosion, we propose to use abstractions reducing the state-space while preserving reachability prop-erties. Four exact, plus one safe abstractions are dened. In the main abstraction (simulation) a concrete state is mapped to a symbolic ab-stract state (a set of concrete states). The other four abstractions are de ned on top of the simulation one. They can be computed on-the-fly in a completely orthogonal manner and thus can be combined to yield better reductions. A prototype implementation in the tool Kronos has permitted to verify two benchmark examples with a signicant scale-up in size.