Enhancing Random Walk State Space Exploration

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F05%3A00012727" target="_blank" >RIV/00216224:14330/05:00012727 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Enhancing Random Walk State Space Exploration

Original language description

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.

Czech name

Zlepšení prohledávání stavového prostoru náhodnou procházkou

Czech description

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ýtpouž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í.

Type

D - Article in proceedings

CEP classification

IN - Informatics

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2005

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Formal Methods for Industrial Critical Systems

ISBN

1-59593-148-1

ISSN

—

e-ISSN

—

Number of pages

8

Pages from-to

98-105

Publisher name

ACM SIGSOFT

Place of publication

Lisbon

Event location

Lisbon

Event date

Jan 1, 2005

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—