迈向通路的模块化验证：公平性与假设

模块化验证是一种用于应对复杂系统（如并发交互系统）属性验证中常遇到的状态爆炸问题的技术。模块化方法基于这样的观察：感兴趣的属性通常仅涉及系统的一小部分。因此，可以构建近似整体系统行为的简化模型，从而实现更高效的验证。生化通路可被视为复杂的并发交互系统。因此，对其属性的验证通常在计算上非常昂贵，并可受益于模块化方法。在本文中，我们报告了开发生化通路模块化验证框架的初步结果。我们将生化通路视为竞争分子资源的反应并发系统。模块化验证技术可基于仅包含涉及感兴趣分子资源的反应的简化模型。为了正确描述系统行为，我们认为考虑适当的公平性概念至关重要，这是并发理论中既定的概念，但在通路建模领域尚属新颖。我们提出了一种包含公平性的建模方法，并确定了可在模块化方式进行属性验证的假设。我们证明了该方法的正确性，并通过 Schoeberl 等人提出的 EGF 受体诱导的 MAP 激酶级联模型进行了演示。