Enhancing Random Walk State Space Exploration

PELÁNEK, Radek, Tomáš HANŽL, Ivana ČERNÁ and Luboš BRIM. Enhancing Random Walk State Space Exploration. In Formal Methods for Industrial Critical Systems. Lisbon: ACM SIGSOFT, 2005, p. 98-105. ISBN 1-59593-148-1.

Basic information

• Original name: Enhancing Random Walk State Space Exploration
• Name in Czech: Zlepšení prohledávání stavového prostoru náhodnou procházkou
• Authors: PELÁNEK, Radek (203 Czech Republic, guarantor), Tomáš HANŽL (203 Czech Republic), Ivana ČERNÁ (203 Czech Republic) and Luboš BRIM (203 Czech Republic).
• Edition: Lisbon, Formal Methods for Industrial Critical Systems, p. 98-105, 8 pp. 2005.
• Publisher: ACM SIGSOFT

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Portugal
• Confidentiality degree: is not subject to a state or trade secret
• RIV identification code: RIV/00216224:14330/05:00012727
• Organization unit: Faculty of Informatics
• ISBN: 1-59593-148-1
• Keywords in English: random walk; state space exploration
• Tags: random walk, state space exploration
• Tags: Reviewed

Abstract

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.

Abstract (in Czech)

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í.

Links

• GA201/03/0509, research and development project: Name: Automatizovaná verifikace paralelních a distribuovaných systémů

Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems

• GD102/05/H050, research and development project: Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů

Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1ET408050503, research and development project: Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems