BRIM, Luboš, Jitka CRHOVÁ a Karen YORAV. Using Assumptions to Distribute CTL Model Checking. In 1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002). Brno, Czech Republic: Elsevier, 2002, s. 80-95. ISBN 0444512918.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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 Model checking, verification
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Luboš Brim, CSc., učo 197. Změněno: 22. 11. 2006 08:32.
Anotace
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 VaVNá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ěrNá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ů
VytisknoutZobrazeno: 25. 4. 2024 14:40