Technical Reports

The report FIMU-RS-2002-08

Using Assumptions to Distribute CTL Model Checking

by Lubo¹ Brim, Jitka Crhová, Karen Yorav, This is a full version of the paper presented at PDMC`02. October 2002, 22 pages.

FIMU-RS-2002-08. Available as Postscript, PDF.

Abstract:

In this work we discuss the problem of performing distributed CTL model checking 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.