Reachability of Hybrid Systems in Space-Time

In set-based reachability, a cover of the reachable states of a hybrid system is obtained by repeatedly computing one-step successor states. It can be used to show safety or to obtain quantitative information, e.g., for measuring the jitter in an oscillator circuit. In general, one-step successors can only be computed approximately and are difficult to scale in the number of continuous variables. The approximation error requires particular attention since it can accumulate rapidly, leading to a coarse cover, prohibitive state explosion, or preventing termination. In this paper, we propose an approach with precise control over the balance between approximation error and scalability. By lazy evaluation of set representations, the precision can be increased in a targeted manner, e.g., to show that a particular transition is spurious. Each evaluation step scales well in the number of continuous variables. The set representations are particularly suited for clustering and containment checking, which are essential for reducing the state explosion. This provides the building blocks for refining the cover of the reachable set just enough to show a property of interest. The approach is illustrated on several examples.