**Date: **
16:00,
Thursday, August 6, 2015

**Speaker: **
Goran Frehse

**Venue: **IST Austria

**Notes: **

16:00

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

examples.