一种生物鲁棒性性质的正式表征与高效验证
形式语言与自动机理论
2021-04-29 v1
摘要
鲁棒性是一种可观测性质，化学反应网络 (CRN) 可借助该性质在不同扰动影响下维持其功能。一般而言，要验证一个网络是否鲁棒，必须考虑所有可能的参数配置。这是一个可能带来巨大计算量的过程。在 Rizk 等人的工作中，作者提出了线性时序逻辑 (LTL) 中的鲁棒性定义，基于此，通过考虑不同参数配置得到的多条数值定时轨迹，他们验证了反应网络的鲁棒性。在本文中，我们关注初始浓度鲁棒性（-鲁棒性）这一概念，它涉及某一物种（即输入）初始浓度的扰动对稳态下另一物种（即输出）浓度的影响。我们在 Rizk 等人提出的框架中表征了该鲁棒性概念，并表明对于单调反应网络，这使我们能够大幅减少验证 CRN 鲁棒性所需的轨迹数量。
引用
@article{arxiv.2104.13831,
title = {Formal characterization and efficient verification of a biological robustness property},
author = {Lucia Nasti and Roberta Gori and Paolo Milazzo},
journal= {arXiv preprint arXiv:2104.13831},
year = {2021}
}