Using Assumptions to Distribute CTL Model Checking

BRIM, Luboš, Jitka CRHOVÁ a Karen YORAV. Using Assumptions to Distribute CTL Model Checking. Brno, Czech Republic, 2002, s. 1-22. Technical Report FIMU-RS-2002-08.

Základní údaje

• Originální název: Using Assumptions to Distribute CTL Model Checking
• Autoři: BRIM, Luboš, Jitka CRHOVÁ a Karen YORAV.
• Vydání: Brno, Czech Republic, s. 1-22, Technical Report FIMU-RS-2002-08. 2002.

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í
• Organizační jednotka: Fakulta informatiky
• Příznaky: Mezinárodní význam, Recenzováno

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 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ů