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, 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 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ů |
VytisknoutZobrazeno: 1. 10. 2024 15:34