Properties of State Spaces and Their Applications
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F08%3A00025025" target="_blank" >RIV/00216224:14330/08:00025025 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Properties of State Spaces and Their Applications
Original language description
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.
Czech name
Vlastnosti stavových prostorů a jejich aplikace
Czech description
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 jejichvlastnosti 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ů.
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2008
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
International Journal on Software Tools for Technology Transfer (STTT)
ISSN
1433-2779
e-ISSN
—
Volume of the periodical
10
Issue of the periodical within the volume
5
Country of publishing house
DE - GERMANY
Number of pages
12
Pages from-to
—
UT code for WoS article
—
EID of the result in the Scopus database
—