TY - GEN
T1 - Incremental model checking in the modal Mu-calculus
AU - Sokolsky, Oleg V.
AU - Smolka, Scott A.
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1994.
PY - 1994
Y1 - 1994
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84947984355
U2 - 10.1007/3-540-58179-0_67
DO - 10.1007/3-540-58179-0_67
M3 - Conference contribution
AN - SCOPUS:84947984355
SN - 9783540581796
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 351
EP - 363
BT - Computer Aided Verification - 6th International Conference, CAV 1994, Proceedings
A2 - Dill, David L.
PB - Springer Verlag
T2 - 6th International Conference on Computer Aided Verification, CAV 1994
Y2 - 21 June 1994 through 23 June 1994
ER -