Incremental model checking in the modal Mu-calculus

Abstract

We present an incremental algorithm for model checking in the alternatlon-free fragment of the modal mu-calculus, the first incremental algorithm for model checking of which we are aware. The basis for oar 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 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-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.