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

Max KornMax Korn, Julián MéndezJulián Méndez, Sascha KlüppelholzSascha Klüppelholz, Ricardo LangnerRicardo Langner, Christel BaierChristel Baier, Raimund DachseltRaimund Dachselt

DOI Link

Max Korn, Julián Méndez, Sascha Klüppelholz, Ricardo Langner, Christel Baier, Raimund Dachselt
PMC-VIS: An Interactive Visualization Tool for Probabilistic Model Checking
In Ferreira, Carla and Willemse, Tim A. C., eds., Software Engineering and Formal Methods, 361--375, 2023. Springer Nature Switzerland

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{KMKLBD2023,
  author    = {Max Korn and Juli{\'{a}}n M{\'{e}}ndez and Sascha
               Kl{\"{u}}ppelholz and Ricardo Langner and Christel Baier and
               Raimund Dachselt},
  title     = {PMC-VIS: An Interactive Visualization Tool for Probabilistic
               Model Checking},
  editor    = {Ferreira and Carla\n               and Willemse and Tim A. C.},
  booktitle = {Software Engineering and Formal Methods},
  publisher = {Springer Nature Switzerland},
  year      = {2023},
  pages     = {361--375},
  doi       = {10.1007/978-3-031-47115-5_20}
}