Informace o publikaci

Using Assumptions to Distribute CTL Model Checking

Logo poskytovatele
Autoři

BRIM Luboš CRHOVÁ Jitka YORAV Karen

Rok publikování 2002
Druh Článek ve sborníku
Konference 1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Počítačový hardware a software
Klíčová slova verification; model checking
Popis 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 precis
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info