ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems

We present a new version of PROBDIVINE – a parallel tool for verification of probabilistic systems against properties formulated in linear temporal logic. Unlike the previous release [1], the new version of the tool allows for both quantitative and qualitative model-checking. It is also strictly multi-threaded, therefore, protects users from unwanted burden of parallel computing in a distributedmemory environment.

• Type: Conference
• Year: 2008
• Where: QEST
• Authors: Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova
• Keywords: Linear Temporal Logic, Parallel Tool, Probabilistic Systems, QEST 2008, Quantitative Evaluation Of Systems