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.



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.