BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA and 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, p. 215-216. ISBN 0-7695-2883-X.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name ProbDiVinE: A Parallel Qualitative LTL Model Checker
Name in Czech ProbDiVinE: Paralelní qualitativní model checker
Authors BARNAT, Jiří (203 Czech Republic, guarantor), Luboš BRIM (203 Czech Republic), Ivana ČERNÁ (203 Czech Republic), Milan ČEŠKA (203 Czech Republic) and Jana TŮMOVÁ (203 Czech Republic).
Edition United States of America, Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07), p. 215-216, 2 pp. 2007.
Publisher IEEE Computer Society
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United Kingdom of Great Britain and Northern Ireland
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/07:00019472
Organization unit Faculty of Informatics
ISBN 0-7695-2883-X
UT WoS 000250951700029
Keywords in English ProbDiVinE; Qualitative LTL; Probabilistic; Model Checking
Tags Model checking, probabilistic, ProbDiVinE, Qualitative LTL
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 1/6/2009 21:07.
Abstract
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.
Abstract (in Czech)
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í.
Links
MSM0021622419, plan (intention)Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1ET408050503, research and development projectName: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development projectName: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science
PrintDisplayed: 22/6/2024 00:08