2016 IEEE International High Level Design Validation and Test Workshop (HLDVT) (2016)
Santa Cruz, CA, USA
Oct. 7, 2016 to Oct. 8, 2016
Md. Ariful Islam , Deparment of Computer Science, Carnegie Mellon University
Qinsi Wang , Deparment of Computer Science, Carnegie Mellon University
Ramin M. Hasani , Department of Computer Science, Stony Brook University
Ondrej Balun , Department of Computer Science, Stony Brook University
Edmund M. Clarke , Deparment of Computer Science, Carnegie Mellon University
Radu Grosu , Department of Informatics, Vienna University of Technology
Scott A. Smolka , Department of Computer Science, Stony Brook University
We present a probabilistic reachability analysis of a (nonlinear ODE) model of a neural circuit in Caeorhabditis elegans (C. elegans), the common roundworm. In particular, we consider Tap Withdrawal (TW), a reflexive behavior exhibited by a C. elegans worm in response to vibrating the surface on which it is moving. The neural circuit underlying this response is the subject of this investigation. Specially, we perform boundedtime reachability analysis on the TW circuit model of Wicks et al. (1996) to estimate the probability of various TW responses. The Wicks et al. model has a number of parameters, and we demonstrate that the various TW responses and their probability of occurrence in a population of worms can be viewed as a problem of parameter uncertainty. Our approach to this problem rests on encoding each TW response as a hybrid automaton with parametric uncertainty. We then perform probabilistic reachability analysis on these automata using a technique that combines a δ-decision procedure with statistical tests. The results we obtain are a significant extension of those of Wicks et al. (1996), who equip their model with fixed parameter values that reproduce a single TW response. In contrast, our technique allow us to more thoroughly explore the models parameter space using statistical sampling theory, identifying in the process the distribution of TW responses. Wicks et al. conducted a number of ablation experiments on a population of worms in which one or more of the neurons in the TW circuit are surgically ablated (removed). We show that our technique can be used to correctly estimate TW responseprobabilities for four of these ablation groups. We also use our technique to predict TW response behavior for two ablation groups not previously considered by Wicks et al.
Neurons, Integrated circuit modeling, Grippers, Computational modeling, Animals, Reachability analysis, Automata
M. A. Islam et al., "Probabilistic reachability analysis of the tap withdrawal circuit in caenorhabditis elegans," 2016 IEEE International High Level Design Validation and Test Workshop (HLDVT), Santa Cruz, CA, USA, 2016, pp. 170-177.