D 2002

Using Assumptions to Distribute CTL Model Checking

BRIM, Luboš, Jitka CRHOVÁ a Karen YORAV

Základní údaje

Originální název

Using Assumptions to Distribute CTL Model Checking

Autoři

BRIM, Luboš (203 Česká republika, garant), Jitka CRHOVÁ (203 Česká republika) a Karen YORAV (376 Izrael)

Vydání

Brno, Czech Republic, 1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002), s. 80-95, 2002

Nakladatel

Elsevier

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

20206 Computer hardware and architecture

Stát vydavatele

Nizozemské království

Utajení

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

Kód RIV

RIV/00216224:14330/02:00006432

Organizační jednotka

Fakulta informatiky

ISBN

0444512918

Klíčová slova anglicky

verification; model checking

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 08:32, prof. RNDr. Luboš Brim, CSc.

Anotace

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

Návaznosti

GA201/00/1023, projekt VaV
Název: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Grantová agentura ČR, Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
MSM 143300001, záměr
Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů