• Skip the Organizational structure panel
• Organizational structure

  On selecting a constituent part of MU the "Overview of publishing activities" page will be displayed with information relevant to the selected constituent part. The "Overview of publishing activities" page is not available for non-activated items.

  Masaryk University

  • Faculties
  • Law
  • Medicine
  • Science
  • Arts
  • Education
  • Economics
  • Informatics
  • Social Studies
  • Sports Studies

  • Institutes
  • Computer Science
  • CEITEC MU
  • Politica
  • Specialized Units
  • Hostels & Canteens
  • University Press
  • Telč Centre
  • UCB Management

  • Rector`s Office
  • Rectorate
  • Other Units
  • Archive
  • Language Centre
  • International Studies
  • Disabled Students
  • Technology Transfer
  • Biostatistics
  • Mendel Museum
  • CERIT
  • Civic Education
  • Project Team CEITEC

   

Publication details

ProbDiVinE: A Parallel Qualitative LTL Model Checker

Further information
Citation:	BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - TŮMOVÁ, Jana. 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. ISBN 0-7695-2883-X, pp. 215-216. 2007, Edinburgh, Scotland.
Original language:	English
Field:	Informatika
Type:	Article in Proceedings
Keywords:	ProbDiVinE; Qualitative LTL; Probabilistic; Model Checking

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