ProbDiVinE: A Parallel Qualitative LTL Model Checker

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.

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United Kingdom of Great Britain and Northern Ireland

Confidentiality degree

není předmětem státního či obchodního tajemství

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

---

Abstract

V originále

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.

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 project	Name: 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 project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science