机器人细胞注射系统在高阶逻辑中的形式化建模
计算机科学中的逻辑
2018-07-20 v1 机器人学
摘要
机器人细胞注射用于自动将物质递送至细胞内，是药物开发、基因工程以及细胞生物学许多其他领域不可或缺的组成部分。传统上，这些系统功能的正确性通过纸笔证明和计算机仿真方法来确认。然而，基于纸笔的证明容易出现人为错误，而仿真由于其基于采样的特性以及无法在计算机模型中捕捉连续行为，提供了不完整的分析。模型检测最近也被提倡用于细胞注射系统的分析。但它涉及对用于建模系统动力学的微分方程进行离散化，因此同样损害了分析的完整性。在本文中，我们提出使用高阶逻辑定理证明来对机器人细胞注射系统的动力学行为进行建模与分析。底层逻辑的高表达能力使我们能够以真实形式捕捉模型的连续细节。随后，可在证明助手的可靠核心内使用演绎推理对该模型进行分析。
引用
@article{arxiv.1807.07378,
title = {Formal Modeling of Robotic Cell Injection Systems in Higher-order Logic},
author = {Adnan Rashid and Osman Hasan},
journal= {arXiv preprint arXiv:1807.07378},
year = {2018}
}
备注
Formal Verification of Physical Systems (FVPS-2018), co-located with Conference on Intelligent Computer Mathematics (CICM-2018). arXiv admin note: text overlap with arXiv:1805.02858