D 2004

Typical Structural Properties of State Spaces

PELÁNEK, Radek

Základní údaje

Originální název

Typical Structural Properties of State Spaces

Název česky

Typické strukturní vlastnosti stavových prostorů

Autoři

Vydání

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

Nakladatel

Springer-Verlag

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/04:00010717

Organizační jednotka

Fakulta informatiky

ISBN

3-540-21314-7

Klíčová slova anglicky

explicit model checking; state space exploration

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 21. 11. 2006 14:02, doc. Mgr. Radek Pelánek, Ph.D.

Anotace

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.

Česky

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

Návaznosti

GA201/03/0509, projekt VaV
Název: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 143300001, záměr
Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů