PMC-VIS: An Interactive Visualization Tool for Probabilistic Model Checking

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review


State-of-the-art Probabilistic Model Checking (PMC) offers multiple engines for the quantitative analysis of Markov Decision Processes (MDPs), including rewards modeling cost or utility values. Despite the huge amount of internally computed information, support for debugging and facilities that enhance the understandability of PMC models and results are very limited. As a first step to improve on that, we present the basic principles of PMC-VIS, a tool that supports the exploration of large MDPs together with the computed PMC results per MDP-state through interactive visualization. By combining visualization techniques, such as node-link diagrams and parallel coordinates, with quantitative analysis capabilities, PMC-VIS supports users in gaining insights into the probabilistic behavior of MDPs and PMC results and enables different ways to explore the behaviour of schedulers of multiple target properties. The usefulness of PMC-VIS is demonstrated through three different application scenarios.


Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods
EditorsCarla Ferreira, Tim A. C. Willemse
Place of PublicationCham
PublisherSpringer, Cham
Number of pages15
ISBN (electronic)978-3-031-47115-5
ISBN (print)978-3-031-47114-8
Publication statusPublished - 31 Oct 2023

Publication series

SeriesLecture Notes in Computer Science, Volume 14323

External IDs

Scopus 85177440177
ORCID /0000-0002-5321-9343/work/154190607
ORCID /0000-0002-2176-876X/work/154191006
ORCID /0000-0003-4519-2168/work/154193031