BRIM, Luboš, Ivana ČERNÁ, Pavel KRČÁL a Radek PELÁNEK. Distributed LTL Model-Checking Based on Negative Cycle Detection. In FST-TCS 2001. Bangalore, India: Springer. s. 96-110. LNCS 2245. ISBN 3-540-43002-4. 2001.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Distributed LTL Model-Checking Based on Negative Cycle Detection
Název anglicky Distributed LTL Model-Checking Based on Negative Cycle Detection
Autoři BRIM, Luboš, Ivana ČERNÁ, Pavel KRČÁL a Radek PELÁNEK.
Vydání Bangalore, India, FST-TCS 2001, s. 96-110, LNCS 2245, 2001.
Nakladatel Springer
Další údaje
Typ výsledku Stať ve sborníku
Obor 20206 Computer hardware and architecture
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/01:00004500
Organizační jednotka Fakulta informatiky
ISBN 3-540-43002-4
Změnil Změnil: prof. RNDr. Luboš Brim, CSc., učo 197. Změněno: 3. 12. 2001 14:07.
Anotace
This paper addresses the state explosion problem in automata based LTL model checking. To deal with large space requirements we turn to use a distributed approach. All the known methods for automata based model checking are based on depth first traversal of the state space which is difficult to parallelise as the ordering in which vertices are visited plays an important role. We come up with entirely different approach which is dependent on locating cycles with negative length in a directed graph with real number length of edges. Our method allows reasonable distribution and the experimental results confirm its usefulness for distributed model checking.
Anotace anglicky
This paper addresses the state explosion problem in automata based LTL model checking. To deal with large space requirements we turn to use a distributed approach. All the known methods for automata based model checking are based on depth first traversal of the state space which is difficult to parallelise as the ordering in which vertices are visited plays an important role. We come up with entirely different approach which is dependent on locating cycles with negative length in a directed graph with real number length of edges. Our method allows reasonable distribution and the experimental results confirm its usefulness for distributed model checking.
Návaznosti
GA201/00/0400, projekt VaVNázev: Nekonečně stavové souběžné systémy - modely a verifikace
Investor: Grantová agentura ČR, Nekonečně stavové souběžné systémy - modely a verifikace
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: 29. 3. 2024 16:54