Local Quantitative LTL Model Checking

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. Local Quantitative LTL Model Checking. In 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008). L'Aquilla: ERCIM, 2008, s. 63-78. ISBN 978-3-642-03239-4.

Základní údaje

Originální název

Local Quantitative LTL Model Checking

Název česky

Lokální kvantitafivní ověřování modelů LTL

Autoři

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ

Vydání

L'Aquilla, 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), od s. 63-78, 16 s. 2008

Nakladatel

ERCIM

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Itálie

Utajení

není předmětem státního či obchodního tajemství

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-03239-4

UT WoS

000270704100004

Klíčová slova anglicky

LTL Model Checking; Probabilistic; Parallel

Štítky

LTL model checking, parallel, probabilistic

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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 reachable states 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 checking problem 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.

Česky

Kvantitativní analýza pravděpodobnostních systémů byla dosud studována zejména v kontextu globálních algoritmů pro model-checking. V tomto článku je popsán postup, jakým lze proceduru kvantitativní analýzy pravděpodobnostních systémů zdokonalit v případě, že se zajímáme o výsledek analýzy pouze pro iniciální stav systému. Experimentálně bylo ukázáno, že použitím nových metod dochází k redukci časové náročnosti procedury verifikace z řádu dnů na řády minut.

---

Návaznosti

GA201/06/1338, projekt VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky