2009
Local Quantitative LTL Model Checking
BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA, Jana TŮMOVÁ et. al.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
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"
Odkazy
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
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ěněno: 13. 10. 2020 09:36, prof. RNDr. Ivana Černá, CSc.
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 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.
Č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 VaV |
| ||
| 1ET408050503, projekt VaV |
|