Probabilistic reachability analysis of the tap withdrawal circuit in caenorhabditis elegans

Md Ariful Islam, Qinsi Wang, Ramin M. Hasani, Ondrej Balun, Edmund M. Clarke, Radu Grosu, Scott A. Smolka

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publication2016 IEEE International High Level Design Validation and Test Workshop, HLDVT 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages170-177
Number of pages8
ISBN (Electronic)9781509042708
DOIs
StatePublished - Nov 17 2016
Event18th IEEE International High Level Design Validation and Test Workshop, HLDVT 2016 - Santa Cruz, United States
Duration: Oct 7 2016Oct 8 2016

Publication series

Name2016 IEEE International High Level Design Validation and Test Workshop, HLDVT 2016

Conference

Conference18th IEEE International High Level Design Validation and Test Workshop, HLDVT 2016
Country/TerritoryUnited States
CitySanta Cruz
Period10/7/1610/8/16

Keywords

  • C. elegans
  • Formal Methods
  • Probabilistic Reachability Analysis
  • Tap Withdrawal Circuit

Fingerprint

Dive into the research topics of 'Probabilistic reachability analysis of the tap withdrawal circuit in caenorhabditis elegans'. Together they form a unique fingerprint.

Cite this