ProbDiVinE: A Parallel Qualitative LTL Model Checker

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	BARNAT Jiří BRIM Luboš ČERNÁ Ivana ČEŠKA Milan TŮMOVÁ Jana
Year of publication	2007
Type	Article in Proceedings
Conference	Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07)
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	ProbDiVinE; Qualitative LTL; Probabilistic; Model Checking
Description	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.
Related projects:	Techniques for automatic verification and validation of software nad hardware systems Institute for Theoretical Computer Science Highly Parallel and Distributed Computing Systems