Abstract. We present an incremental algorithm for model checking in the alternation-free fragment of the modal mu-calculus, the rst 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 Ste en that performs global (non-incremental) computation of xed points. MCI takes as input a set of changes 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-Ste en 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.
Incremental model checking has been studied previously, with REF presenting the first incremental model checking algorithm, for alternation-free µ-calculus.
Incremental Model Checking in the Modal Mu-Calculus
CAV
Computer Science