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.