Local Quantitative LTL Model Checking

Kód výsledku v 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>

Nalezeny alternativní kódy

RIV/00216224:14330/09:00028657 RIV/00216224:14330/09:00065775

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Local Quantitative LTL Model Checking

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Local Quantitative LTL Model Checking

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2009

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008)

ISBN

978-3-642-03239-4

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

—

Název nakladatele

ERCIM

Místo vydání

L'Aquilla

Místo konání akce

L'Aquilla

Datum konání akce

1. 1. 2008

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—