Local Quantitative LTL Model Checking
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F08%3A00024320" target="_blank" >RIV/00216224:14330/08:00024320 - isvavai.cz</a>
Alternative codes found
RIV/00216224:14330/09:00028657 RIV/00216224:14330/09:00065775
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Local Quantitative LTL Model Checking
Original language description
Quantitative analysis of probabilistic systems has been studied mainly from the global model checking point of view. In the global model-checking, the goal of verification is to decide the probability of satisfaction of a given property for all reachablestates in the state space of the system under investigation. On the other hand, in local model checking approach the probability of satisfaction is computed only for the set of initial states. In theory, it is possible to solve the local model checkingproblem using the global model checking approach. However, the global model checking procedure can be significantly outperformed by a dedicated local model checking one. In this paper we resent several particular local model checking techniques that if applied to global model checking procedure reduce the runtime needed from days to minutes.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
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
2009
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
Article name in the collection
13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008)
ISBN
978-3-642-03239-4
ISSN
—
e-ISSN
—
Number of pages
16
Pages from-to
—
Publisher name
ERCIM
Place of publication
L'Aquilla
Event location
L'Aquilla
Event date
Jan 1, 2008
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—