随机模型时间性质的鲁棒性研究
计算机科学中的逻辑
2013-09-05 v1 人工智能
机器学习
系统与控制
摘要
连续时间马尔可夫链 (CTMC) 和随机混合自动机 (SHA) 等随机模型是建模和推理生物系统动力学的强大形式化方法，因为它们能够捕捉生物过程固有的随机性。形式化建模中一个与生物建模密切相关经典问题是模型检测问题，即计算在给定随机过程中，由某一时序逻辑公式所表达的行为发生的概率。然而，人们可能不仅关注可满足性概念，还关注系统在不受扰动（例如由外在噪声引起）或模型参数微小变化影响的情况下维持特定涌现行为的能力。为解决这一问题，验证社区的研究人员最近提出了几种针对时序逻辑的鲁棒性概念，为 (确定性) 动力系统的轨迹与满足感兴趣性质的轨迹集边界之间提供了合适的距离定义。本文的贡献有两方面。首先，我们将鲁棒性概念扩展至随机系统，表明这自然导出了鲁棒性分数的分布。通过讨论两个实例，我们展示了如何近似鲁棒性分数的分布及其关键指标：平均鲁棒性和条件平均鲁棒性。其次，我们展示了如何将这些指标与满足概率相结合以解决系统设计问题，其目标是优化随机模型的某些控制参数，以最大限度地提高所需规范的鲁棒性。
引用
@article{arxiv.1309.0866,
title = {On the Robustness of Temporal Properties for Stochastic Models},
author = {Ezio Bartocci and Luca Bortolussi and Laura Nenzi and Guido Sanguinetti},
journal= {arXiv preprint arXiv:1309.0866},
year = {2013}
}
备注
In Proceedings HSB 2013, arXiv:1308.5724