A *Cyber-Physical System (CPS)* can be viewed as a computer program that interacts with a physical environment. Such a system can be formalized by a *hybrid automaton *which equipped with finitely many discrete states and continuous variables. A state of a hybrid automaton can be denoted by a discrete state along with a valuation of the variables.

The *reachability problem* on hybrid automata can be defined as follows. Given a hybrid automaton , an initial set and a state , is reachable in from ? Reachability plays a key role in the verification of hybrid automata. For example, in safety verification, we want to check whether an unsafe state is reachable by the system.

The tool Flow* focuses on reachability-based verification of hybrid automata. Since the reachability problem on hybrid automata is *not decidable*, the tool computes an over-approximation for a reachable state set. If a given state is not included then it is absolutely unreachable. The over-approximation set is represented as a finite set of *Taylor models*.

## What is challenging in reachability computation?

Besides chaotic and stiff continuous dynamics defined by non-linear ODEs, the following difficulties still exist in all reachability computation problems for non-linear systems.

(1) **Large number of state variables.**

(2) **Large initial sets.**

(3) **Nondeterministic discrete transitions.**

Working on (1) and (2) allows us to verify more general properties. Only a combination of them gives a challenge. * Notice that computing reachable set over-approximations from a tiny initial set is often easy even on large scale systems, especially the initial values of some variables take single values. *

Considering (3) allows us to work on more realistic hybrid systems. The analysis of them often generates a large number of branches which could cause an exponential growth of the computation time.

**The techniques implemented in Flow* gives an effective way to handle these challenges.**