Model Checking with formula-dependent abstract models

Alexander Asteroth, Christel Baier, Ulrich A{\ss}mann

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


We present a model checking algorithm for $\forall {\it CTL}$ (and full $\CTL$) which uses an iterative abstraction refinement strategy. In each iteration we call a standard model checker for the abstract models ${\cal A}_i$. If ${\cal A}_i$ does not satisfy $\Phi$ we refine the abstract model ${\cal A}_i$ yielding another abstract model $\A_{i+1}$ and (re-)call the model checker to $\A_{i+1}$. Otherwise the formula holds for the original system $\M$. Our algorithm terminates at least for all transition systems ${\cal M}$ that have a finite simulation or bisimulation quotient. In contrast to other abstraction refinement algorithms, we always work with abstract models whose size just depend on the length of the formula $\Phi$ (but not on the size of the system which might be infinite). %In particular, our algorithm has the potential to handle %systems of arbitrary size %as the proper model checker just has to treat the small %abstract models ${\cal A}_i$.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Start Conference Manager
Conference Systems