Model checking of real-time reachability properties using abstractions

Practical real-time model checking suffers 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 properties. Four exact, plus one safe abstractions are defined. In the main abstraction (simulation) a concrete state is mapped to a symbolic abstract state (a set of concrete states). The other four abstractions are defined 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 significant scale-up in size.