论文标题
无限国家化学反应网络的反例
Counterexample Generation for Infinite-State Chemical Reaction Networks
论文作者
论文摘要
反示例生成是模型检查过程中必不可少的一部分。在随机模型检查中，反示例生成是一个具有挑战性的问题，因为它不足以找到违反给定属性的单个跟踪。取而代之的是，需要找到一套可能违反该物业的概率的大型痕迹。本文考虑了具有潜在无限状态空间的化学反应网络（CRN）模型的反例产生。开发了基于使用SMT求解的有界模型检查的方法，为CRN的反示例生成开发。它打算找到一小部分违反给定模型的属性路径，以便它们的总概率高于给定的阈值。一个独特的挑战是由于CRN的高度连接状态空间，其中反例仅是所有违反所有财产的小部分。为了应对此类挑战，本文提出了许多优化，包括一种分隔和拼接技术，以扩大大型CRN模型的反例生成方法。本文报告了许多无限状态CRN模型的实验。
Counterexample generation is an indispensable part of model checking process. In stochastic model checking, counterexample generation is a challenging problem as it is not enough to find a single trace that violates the given property. Instead, a potentially large set of traces with enough probability to violate the property needs to be found. This paper considers counterexample generation for chemical reaction network (CRN) models with potentially infinite state space. A method based on bounded model checking using SMT solving is developed for counterexample generation for CRNs. It intends to find a small set of property violating paths of a given model such that they collectively have a total probability that is above a given threshold. A unique challenge is due to the highly connected state space of CRNs where a counterexample is only a tiny subset of all property violating paths. To address such challenges, this paper presents a number of optimizations including a divide-and-conquer technique to scale up the counterexample generation method for large CRN models. This paper reports results from experiments on a number of infinite-state CRN models.
