Assumption-based distribution of CTL model checking

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BRIM Luboš ŽIDKOVÁ Jitka YORAV Karen

Year of publication 2005
Type Article in Periodical
Magazine / Source International Journal on Software Tools for Technology Transfer (STTT)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords model-checking
Description In this paper we discuss the problem of performing distributed CTL model checking by splitting the given state space into several ldquopartial 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 truth values of formulas and the computers exchange assumptions about relevant states to compute more precise information.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.