# Models

### Hybrid automata

Flow* works on the systems which can be modeled by hybrid automata. A hybrid automaton is denoted by $(\textit{loc}, \textit{var}, \textit{inv}, \textit{flow}, \textit{trans}, \textit{guard}, \textit{reset}, \textit{init})$ such that

• $\textit{loc}$ is a finite set of discrete states which are also called modes.
• $\textit{var}$ consists of $n$ real-valued variables for some integer $n>0$.
• $\textit{inv}$ associates each mode an invariant.
• $\textit{flow}$ associates each mode a continuous dynamics which are defined by Ordinary Differential Equations (ODE).
• $\textit{trans}$ is the set of jumps which are discrete transitions between modes.
• $\textit{guard}$ assigns a guard to a jump. A jump can be made if the guard is satisfied.
• $\textit{reset}$ assigns a reset mapping to a jump. After a jump is made, the values of the continuous variables will be updated by the reset mapping.
• $\textit{init}$ is the initial set of the automaton.

### Example

We show that a spiking neuron model can be defined by a hybrid automaton. A simple model for reproducing spiking and bursting behavior of cortical neurons can be defined by the following ODE, $\left\{ \begin{array}{lcl} \dot{v} & = & 0.04v^2 + 5v + 140 - u + I \\ \dot{u} & = & a(bv - u) \end{array} \right.$
such that the variable $v$ represents the membrane potential of the neuron, and $u$ is a membrane recovery variable which provides negative feedback to $v$, that is, whenever $v \geq 30$, its value is updated to $c$ while the value of $u$ is updated to $u + d$. The typical values for the constant parameters are given as $a = 0.02,\qquad b = 0.2,\qquad c = -65,\qquad d = 8,\qquad I = 40.$
The hybrid automaton for the spiking neuron model is presented by the following figure. wherein the condition $v(0) \in [-65,-60]$, $u(0) \in [-0.2,0.2]$ is the initial set.