PELÁNEK, Radek. Typical Structural Properties of State Spaces. In SPIN Workshop 2004. Barcelona (Španělsko): Springer-Verlag, 2004, s. 5-22, 15 s. ISBN 3-540-21314-7.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Typical Structural Properties of State Spaces
Název česky Typické strukturní vlastnosti stavových prostorů
Autoři PELÁNEK, Radek (203 Česká republika, garant).
Vydání Barcelona (Španělsko), SPIN Workshop 2004, od s. 5-22, 15 s. 2004.
Nakladatel Springer-Verlag
Další údaje
Originální 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í
Kód RIV RIV/00216224:14330/04:00010717
Organizační jednotka Fakulta informatiky
ISBN 3-540-21314-7
UT WoS 000189481700002
Klíčová slova anglicky explicit model checking; state space exploration
Štítky explicit model checking, state space exploration
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Změněno: 21. 11. 2006 14:02.
Anotace
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.
Anotace č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 VaVNá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ěrNá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ů
VytisknoutZobrazeno: 26. 4. 2024 14:15