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

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Abstract

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.

Details

OriginalspracheEnglisch
TitelSoftware Engineering and Formal Methods
Redakteure/-innenCarla Ferreira, Tim A. C. Willemse
ErscheinungsortCham
Herausgeber (Verlag)Springer, Cham
Seiten361-375
Seitenumfang15
ISBN (elektronisch)978-3-031-47115-5
ISBN (Print)978-3-031-47114-8
PublikationsstatusVeröffentlicht - 31 Okt. 2023
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 14323
ISSN0302-9743

Externe IDs

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

Schlagworte