Using Assumptions to Distribute CTL Model Checking Lubos Brim, Jitka Crhova and Karen Yorav
In this work we discuss the problem of performing distributed CTL model
checking algorithm by splitting the given state space into several ``partial
state spaces''. The partial state space is modelled as a Kripke structure
with border states. Each computer involved in the distributed computation
owns a partial state space and performs a model checking algorithm on this
incomplete structure. To be able to proceed, the border states are
augmented by assumptions about the truth of formulas and the computers
exchange assumptions about relevant states as they compute more precise
information. In the paper we give the basic definitions and
present the distributed algorithm.
|