PELÁNEK, Radek, Tomáš HANŽL, Ivana ČERNÁ a Luboš BRIM. Enhancing Random Walk State Space Exploration. In Formal Methods for Industrial Critical Systems. Lisbon: ACM SIGSOFT, 2005. s. 98-105, 8 s. ISBN 1-59593-148-1.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Enhancing Random Walk State Space Exploration
Název česky Zlepšení prohledávání stavového prostoru náhodnou procházkou
Autoři PELÁNEK, Radek (203 Česká republika, garant), Tomáš HANŽL (203 Česká republika), Ivana ČERNÁ (203 Česká republika) a Luboš BRIM (203 Česká republika).
Vydání Lisbon, Formal Methods for Industrial Critical Systems, od s. 98-105, 8 s. 2005.
Nakladatel ACM SIGSOFT
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Portugalsko
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/05:00012727
Organizační jednotka Fakulta informatiky
ISBN 1-59593-148-1
Klíčová slova anglicky random walk; state space exploration
Štítky random walk, state space exploration
Příznaky Recenzováno
Změnil Změnil: prof. RNDr. Luboš Brim, CSc., učo 197. Změněno: 21. 11. 2006 11:39.
Anotace
We study the behavior of the random walk method in the context of model checking and its capacity to explore a state space. We describe the methodology we have used for observing the random walk and report on the results obtained. We also describe many possible enhancements of the random walk and study their behavior and limits. Finally, we discuss some practically important but often neglected issues like counterexamples, coverage estimation, and setting of parameters. Similar methodology can be used for studying other state space exploration techniques like bit-state hashing, partial storage methods, or partial order reduction.
Anotace česky
Studujeme chování metody náhodné procházky v kontextu metody ověřování modelů a prohledávání stavového prostoru. Popisujeme metodologii, kterou jsme použili pro pozorování náhodných procházek na velkých grafech a kterou používáme pro shrnutí výsledků. Popisujeme také několik různých zlepšení náhodné procházky a studujeme jejich vlastnosti a limity. Na závěr diskutujeme několik důležitých, ale často opomíjených, témat, jako protipříklady, odhad pokrytí a nastavení parametrů. Podobná metodologie může být použita pro studium dalším metod prohledávání stavového prostoru jako například hašování stavů pomocí bitů, metody částečného ukládání, redukce částečných uspořádání.
Návaznosti
GA201/03/0509, projekt VaVNázev: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Standardní projekty
GD102/05/H050, projekt VaVNázev: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Doktorské granty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
VytisknoutZobrazeno: 19. 2. 2020 07:50