Typical Structural Properties of State Spaces

PELÁNEK, Radek. Typical Structural Properties of State Spaces. In SPIN Workshop 2004. Barcelona (Španělsko): Springer-Verlag, 2004, p. 5-22, 15 pp. ISBN 3-540-21314-7.

Basic information

Original name

Typical Structural Properties of State Spaces

Name in Czech

Typické strukturní vlastnosti stavových prostorů

Authors

PELÁNEK, Radek (203 Czech Republic, guarantor)

Edition

Barcelona (Španělsko), SPIN Workshop 2004, p. 5-22, 15 pp. 2004

Publisher

Springer-Verlag

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/04:00010717

Organization unit

Faculty of Informatics

ISBN

3-540-21314-7

UT WoS

000189481700002

Keywords in English

explicit model checking; state space exploration

Tags

explicit model checking, state space exploration

Tags

International impact, Reviewed

---

Abstract

V originále

Explicit model checking algorithms explore the full state space of a system. We have gathered a large collection of state spaces and performed an extensive study of their structural properties. The results show that state spaces have several typical properties and that they differ significantly from both random graphs and regular graphs. We point out how to exploit these typical properties in practical model checking algorithms.

In Czech

Explicitní algoritmy pro ověřování modelů jsou založeny na prohledávání celého stavového prostoru. Shromáždili jsme velkou kolekci takovýchto stavových prostorů a provedli studii jejich vlastností. Výsledky ukazují, že stavové prostory mají několik typických vlastností a že se výrazně liší jak od náhodných, tak od pravidelných grafů. Také ukazujeme, jak je možné využít těchto vlastností při praktickém ověřování modelů.

---

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
MSM 143300001, plan (intention)	Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing