Analyzing a Discrete Model of Aplysia Central Pattern Generator

Ashish Tiwari and Carolyn Talcott


We present a discrete formal model of the central pattern generator (CPG) located in the buccal ganglia of {\em 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 {\em Aplysia} proposed by Baxter et. al.~\cite{baxter06}. The discrete model is obtained as a composition of discrete models of ten individual neurons in the CPG. The individual neurons are inter-connected 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.~\cite{baxter06}.


SAL Model

Click here to download the complete SAL model.

BibTeX Entry

        title = "Analyzing a Discrete Model of Aplysia Central Pattern Generator",
        author = "Tiwari, A. and Talcott, C.",
        booktitle = "Proc. Comp. Meth. in Sys. Bio., CMSB",
        year = 2008,
        pages = "347--366",
        publisher = "Springer",
	series = "LNBI",
	volume = 5307,

Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page