Abstract
We present a discrete formal model of the central pattern generator (CPG) located in the buccal ganglia of Aplysia that is responsible for mediating the rhythmic movements of its foregut during feeding. Our starting point is the continuous dynamical model for pattern generation underlying fictive feeding in Aplysia proposed by Baxter et. al. [4]. The discrete model is obtained as a composition of discrete models of ten individual neurons in the CPG. The individual neurons are interconnected through excitatory and inhibitory synaptic connections and electric connections. We used Symbolic Analysis Laboratory (SAL) to formally build the model and analyzed it using the SAL model checkers. Using abstract discrete models of the individual neurons helps in understanding the buccal motor programs generated by the network in terms of the network connection topology. It also eliminates the need for detailed knowledge of the unknown parameters in the continuous model of Baxter et. al.
