BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. Local Quantitative LTL Model Checking. In Formal Methods for Industrial Critical Systems. Neuveden: Springer Berlin / Heidelberg. s. 53-68. ISBN 978-3-642-03239-4. doi:10.1007/978-3-642-03240-0_8. 2009.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Local Quantitative LTL Model Checking
Název česky Lokální kvantitativní ověřování modelu pro LTL
Autoři BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, domácí), Milan ČEŠKA (203 Česká republika, domácí) a Jana TŮMOVÁ (203 Česká republika, domácí).
Vydání Neuveden, Formal Methods for Industrial Critical Systems, od s. 53-68, 16 s. 2009.
Nakladatel Springer Berlin / Heidelberg
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í
Forma vydání tištěná verze "print"
WWW URL
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/09:00065775
Organizační jednotka Fakulta informatiky
ISBN 978-3-642-03239-4
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-642-03240-0_8
UT WoS 000270704100004
Klíčová slova česky Kvantitativní ověřování modelu; LTL; Pravděpodobnostní systémy
Klíčová slova anglicky Quantitative Model Checking; Linear Temporal Logic; Probabilistic systems
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnila: prof. RNDr. Ivana Černá, CSc., učo 1419. Změněno: 13. 10. 2020 09:36.
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 call be significantly outperformed by a dedicated local model checking one. In this paper we present 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ěpodonostsních systémů byla studována především z pohledu metody globálního ověřování modelu (určení pravděpodobnosti pro každý stav systému). V článku ukazujeme jak lze výpočetní náročnost problému redukovat, pokud se zajímáme pouze o pravděpodobnost splnění formule v počátečním stavu (lokální ověřování modelu). V článku je popsáno několik technik, které redukují čas potřebný pro výpočet pravděpodobnosti z řádu dnů na řády minut.
Návaznosti
GA201/06/1338, projekt VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
1ET408050503, projekt VaVNá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ů
VytisknoutZobrazeno: 23. 4. 2024 10:57