Incremental Model Checking in the Modal Mu-Calculus
Incremental Model Checking in the Modal Mu-Calculus
复制标题
模态 Mu 微积分中的增量模型检查
DOI：
--
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
S. Smolka
中科院分区：
文献类型：
--
作者：
O. Sokolsky;S. Smolka
我们提出了一种用于模型检查的增量算法，该算法是模态MU-Calculus的替代片段，这是我们知道我们算法的基础的模型检查的第一个增量算法。 ，是由于Cleaveland和Steffen引起的线性时间算法删除的过渡几乎没有额外的成本，也可以像Cleaveland stegrand算法一样插入和删除的状态。 。
We present an incremental algorithm for model checking in the alternation-free fragment of the modal mu-calculus, the first incremental algorithm for model checking of which we are aware. The basis for our algorithm, which we call MCI (for Model Checking Incrementally), is a linear-time algorithm due to Cleaveland and Steffen that performs global (non-incremental) computation of fixed points. MCI takes as input a set δ of change) to the labeled transition system under investigation, where a change constitutes an inserted or deleted transition; with virtually no additional cost, inserted and deleted states can also be accommodated. Like the Cleaveland-Steffen algorithm, MCI requires time linear in the size of the LTS in the worst case, but only time linear in δ in the best case. We give several examples to illustrate MCI in action, and discuss its implementation in the Concurrency Factory, an interactive design environment for concurrent systems.