Flow* works on the systems which can be modeled by hybrid automata. A hybrid automaton is denoted by such that
- is a finite set of discrete states which are also called modes.
- consists of real-valued variables for some integer .
- associates each mode an invariant.
- associates each mode a continuous dynamics which are defined by Ordinary Differential Equations (ODE).
- is the set of jumps which are discrete transitions between modes.
- assigns a guard to a jump. A jump can be made if the guard is satisfied.
- 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.
- 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,
such that the variable represents the membrane potential of the neuron, and is a membrane recovery variable which provides negative feedback to , that is, whenever , its value is updated to while the value of is updated to . The typical values for the constant parameters are given as
The hybrid automaton for the spiking neuron model is presented by the following figure.
wherein the condition , is the initial set.