BARNAT, Jiří, Luboš BRIM a Ivana ČERNÁ. Property Driven Distribution of Nested DFS. In M. Leuschel and U. Ultes-Nitsche (Eds.): Proceedings of the 3rd International Workshop on Verification and Computational Logic. Pittsburgh, PA, USA: Dept. of Electronics and Computer Science, University of Southampton. s. 1-10. 2002.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Property Driven Distribution of Nested DFS
Autoři BARNAT, Jiří (203 Česká republika), Luboš BRIM (203 Česká republika, garant) a Ivana ČERNÁ (203 Česká republika).
Vydání Pittsburgh, PA, USA, M. Leuschel and U. Ultes-Nitsche (Eds.): Proceedings of the 3rd International Workshop on Verification and Computational Logic, s. 1-10, 2002.
Nakladatel Dept. of Electronics and Computer Science, University of Southampton
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Velká Británie a Severní Irsko
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/02:00006603
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky model-checking; distributed model-checking; verification; verification tool
Štítky distributed model-checking, Model-Checking, verification, verification tool
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 22. 11. 2006 16:02.
Anotace
In this paper we propose a distributed algorithm for model-checking LTL formulas that works on a network of workstations and effectively uses the decomposition of the formula automaton to strongly connected components to achieve more efficient distribution of the verification problem. In particular, we explore the possibility of performing a distributed nested depth-first search algorithm.
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: 16. 4. 2024 16:59