对秀丽隐杆线虫Tap Withdrawal行为的模型检查
Model Checking Tap Withdrawal in C. Elegans
AI总结：
本文首次对多细胞生物中神经回路的非线性微分方程模型进行形式验证，通过可达性分析估计关键参数，并展示结果与实验一致，揭示参数范围对三种行为的影响。
摘要：
我们提出了一种对生物真实（非线性微分方程）神经回路模型的形式验证，针对秀丽隐杆线虫的Tap Withdrawal行为。该行为是对移动表面振动的反射性反应，其神经回路是研究对象。具体而言，我们对Wicks等人（1996）提出的TW回路模型进行可达性分析，从而估计关键回路参数。我们的方法基于Fan和Mitra最近开发的技术，自动计算一般非线性系统的局部不一致（收敛和发散速率）。我们展示所获得的结果与Wicks等人（1995）的实验结果一致。与大多数生物模型中固定的参数不同，我们的技术表征了产生（和不产生）三种观察到的行为（运动方向反转、加速和无反应）的参数范围。
英文摘要：
We present what we believe to be the first formal verification of a biologically realistic (nonlinear ODE) model of a neural circuit in a multicellular organism: Tap Withdrawal (TW) in \emph{C. Elegans}, the common roundworm. TW is a reflexive behavior exhibited by \emph{C. Elegans} in response to vibrating the surface on which it is moving; the neural circuit underlying this response is the subject of this investigation. Specifically, we perform reachability analysis on the TW circuit model of Wicks et al. (1996), which enables us to estimate key circuit parameters. Underlying our approach is the use of Fan and Mitra's recently developed technique for automatically computing local discrepancy (convergence and divergence rates) of general nonlinear systems. We show that the results we obtain are in agreement with the experimental results of Wicks et al. (1995). As opposed to the fixed parameters found in most biological models, which can only produce the predominant behavior, our techniques characterize ranges of parameters that produce (and do not produce) all three observed behaviors: reversal of movement, acceleration, and lack of response.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
