D 2002

Using Assumptions to Distribute CTL Model Checking

BRIM, Luboš, Jitka CRHOVÁ and Karen YORAV

Basic information

Original name

Using Assumptions to Distribute CTL Model Checking

Authors

BRIM, Luboš, Jitka CRHOVÁ and Karen YORAV

Edition

Brno, Czech Republic, p. 1-22, Technical Report FIMU-RS-2002-08. 2002

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

20206 Computer hardware and architecture

Country of publisher

Netherlands

Confidentiality degree

není předmětem státního či obchodního tajemství

Organization unit

Faculty of Informatics

Tags

International impact, Reviewed
Změněno: 22/11/2006 08:32, prof. RNDr. Luboš Brim, CSc.

Abstract

V originále

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

Links

GA201/00/1023, research and development project
Name: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Czech Science Foundation, Algorithms and tools for practical verification of concurrent systems.
MSM 143300001, plan (intention)
Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing