BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE: A Parallel Qualitative LTL Model Checker. In Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07). United States of America: IEEE Computer Society, 2007. s. 215-216, 2 s. ISBN 0-7695-2883-X.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název ProbDiVinE: A Parallel Qualitative LTL Model Checker
Název česky ProbDiVinE: Paralelní qualitativní model checker
Autoři BARNAT, Jiří (203 Česká republika, garant), Luboš BRIM (203 Česká republika), Ivana ČERNÁ (203 Česká republika), Milan ČEŠKA (203 Česká republika) a Jana TŮMOVÁ (203 Česká republika).
Vydání United States of America, Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07), od s. 215-216, 2 s. 2007.
Nakladatel IEEE Computer Society
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené království
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/07:00019472
Organizační jednotka Fakulta informatiky
ISBN 0-7695-2883-X
UT WoS 000250951700029
Klíčová slova anglicky ProbDiVinE; Qualitative LTL; Probabilistic; Model Checking
Štítky Model checking, probabilistic, ProbDiVinE, Qualitative LTL
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 1. 6. 2009 21:07.
Anotace
We introduce a parallel model checker for checking Markov decision Processes against linear time properties. The model checker extends the parallel model checker DiVinE and supports verification of qualitative properties.
Anotace česky
Prezentujeme paralelní model checker pro ověřování Markovových rozhodovacích procesů (MDP) na vlastnosti formulované v lineární temporální logice. Nástroj rozšiřuje paralelní model checker DiVinE a podporuje verifikaci qualitativních vlastností.
Návaznosti
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
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: 21. 1. 2020 10:38