PMC-VIS: An Interactive Visualization Tool for Probabilistic Model Checking
Research output: Contribution to book/conference proceedings/anthology/report › Conference contribution › Contributed › peer-review
Contributors
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
Original language | English |
---|---|
Title of host publication | Software Engineering and Formal Methods |
Editors | Carla Ferreira, Tim A. C. Willemse |
Place of Publication | Cham |
Publisher | Springer, Cham |
Pages | 361-375 |
Number of pages | 15 |
ISBN (electronic) | 978-3-031-47115-5 |
ISBN (print) | 978-3-031-47114-8 |
Publication status | Published - 31 Oct 2023 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science, Volume 14323 |
---|---|
ISSN | 0302-9743 |
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 |
ORCID | /0000-0003-1724-2586/work/165453614 |
ORCID | /0000-0003-1029-7656/work/166324032 |