Publication details
Assumption
-based distribution of CTL model checking
| Basic information | |
|---|---|
| Original title: | Assumption -based distribution of CTL model checking |
| Authors: | Luboš Brim, Jitka Židková, Karen Yorav |
| Further information | |
|---|---|
| Citation: | BRIM, Luboš, Jitka ŽIDKOVÁ and Karen YORAV. Assumption -based
distribution of CTL model checking (Assumption -based
distribution of CTL model checking). International Journal on
Software Tools for Technology Transfer (STTT), Springer -Verlag
GmbH, 2005, vol. 7, No 1, p. 61 -73. ISSN 1433 -2779.Export BibTeX |
| Original language: | English |
| Field: | Informatics |
| Type: | Article in Periodical |
| Keywords: | model -checking |
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:
- Automated Verification of Parallel and Distributed Systems
- Highly Parallel and Distributed Computing Systems











