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, 16 s. ISBN 978-3-642-03239-4.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 29. 4. 2011 08:46.
Anotace
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.
Anotace č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 VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Standardní projekty
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 25. 9. 2020 01:33