Goran Frehse

Date: 16:00, Thursday, August 6, 2015
Speaker: Goran Frehse
Venue: IST Austria


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. We present an approach with
precise control over the balance between approximation error and
scalability. By lazy evaluation of abstract 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

Posted in RiSE Seminar