Properties of State Spaces and Their Applications

PELÁNEK, Radek. Properties of State Spaces and Their Applications. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2008, roč. 10, č. 5, s. 443-454. ISSN 1433-2779.

Základní údaje

Originální název

Properties of State Spaces and Their Applications

Název česky

Vlastnosti stavových prostorů a jejich aplikace

Autoři

PELÁNEK, Radek (203 Česká republika, garant)

Vydání

International Journal on Software Tools for Technology Transfer (STTT), Springer-Verlag GmbH, 2008, 1433-2779

---

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Kód RIV

RIV/00216224:14330/08:00025025

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

state space; explicit model checking; graph; experimental evaluation

Štítky

experimental evaluation, explicit model checking, graph, state space

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

Explicit model checking algorithms explore the full state space of a system. State spaces are usually treated as directed graphs without any specific features. We gather a large collection of state spaces and extensively study their structural properties. Our results show that state spaces have several typical properties, i.e., they are not arbitrary graphs. We also demonstrate that state spaces differ significantly from random graphs and that different classes of models (application domains, academic vs industrial) have different properties. We discuss consequences of these results for model checking experiments and we point out how to exploit typical properties of state spaces in practical model checking algorithms.

Česky

Při explicitním ověřování modelu je prohledáván celý stavový prostor systému. Tento stavový prostor je většinou uvažován jako orientovaný graf bez jakýchkoliv specifických vlastností. Shromáždili jsme velkou sbírku stavových prostorů a analyzovali jejich vlastnosti a výsledky ukazují, že reálné stavové prostory vykazují řadu typických vlastností. Ukazuje se také, že stavové prostory se výrazně liší od náhodných grafů a že existují významné rozdíly mezi různými typy stavových prostorů. Diskutujeme také důsledky těchto zjištění pro návrh a experimentální vyhodnocování algoritmů pro ověřování modelů.

---

Návaznosti

GP201/07/P035, projekt VaV	Název: Automatická analýza modelů pomocí procházení stavového prostoru Investor: Grantová agentura ČR, Automatická analýza modelů pomocí procházení stavového prostoru
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky