秀丽隐杆线虫触碰撤回反应的模型检测
计算机科学中的逻辑
2015-03-24 v1 计算工程、金融与科学
系统与控制
神经元与认知
摘要
我们提出了我们认为首个对多细胞生物中生物逼真(非线性常微分方程)神经回路模型的形式化验证:即常见线虫秀丽隐杆线虫 (\emph{C. Elegans}) 的触碰撤回 (TW) 反应。TW 是秀丽隐杆线虫对其运动表面振动产生的反射行为;本研究针对的是该反应背后的神经回路。具体而言,我们对 Wicks 等人 (1996) 的 TW 回路模型进行了可达性分析,使我们能够估计关键的回路参数。我们方法的基础是利用 Fan 和 Mitra 最近开发的技术,自动计算一般非线性系统的局部差异(收敛和发散速率)。我们表明,所获结果与 Wicks 等人 (1995) 的实验结果一致。与大多数生物模型中只能产生主要行为的固定参数不同,我们的技术刻画了能产生(以及不能产生)所有三种观测行为(运动反转、加速和无反应)的参数范围。
引用
@article{arxiv.1503.06480,
title = {Model Checking Tap Withdrawal in C. Elegans},
author = {Md. Ariful Islam and Richard DeFrancisco and Chuchu Fan and Radu Grosu and Sayan Mitra and Scott A. Smolka},
journal= {arXiv preprint arXiv:1503.06480},
year = {2015}
}