{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T16:33:34Z","timestamp":1783096414452,"version":"3.54.6"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031471148","type":"print"},{"value":"9783031471155","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,10,31]],"date-time":"2023-10-31T00:00:00Z","timestamp":1698710400000},"content-version":"vor","delay-in-days":303,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 <jats:sc>PMC-VIS<\/jats:sc>, 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, <jats:sc>PMC-VIS<\/jats:sc> 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 <jats:sc>PMC-VIS<\/jats:sc> is demonstrated through three different application scenarios.\n<\/jats:p>","DOI":"10.1007\/978-3-031-47115-5_20","type":"book-chapter","created":{"date-parts":[[2023,10,30]],"date-time":"2023-10-30T15:04:38Z","timestamp":1698678278000},"page":"361-375","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["PMC-VIS: An Interactive Visualization Tool for\u00a0Probabilistic Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3049-2539","authenticated-orcid":false,"given":"Max","family":"Korn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1029-7656","authenticated-orcid":false,"given":"Juli\u00e1n","family":"M\u00e9ndez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1724-2586","authenticated-orcid":false,"given":"Sascha","family":"Kl\u00fcppelholz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4519-2168","authenticated-orcid":false,"given":"Ricardo","family":"Langner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5321-9343","authenticated-orcid":false,"given":"Christel","family":"Baier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2176-876X","authenticated-orcid":false,"given":"Raimund","family":"Dachselt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,10,31]]},"reference":[{"issue":"5","key":"20_CR1","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1109\/TVCG.2006.120","volume":"12","author":"J Abello","year":"2006","unstructured":"Abello, J., van Ham, F., Krishnan, N.: ASK-GraphView: a large scale graph visualization system. IEEE TVCG 12(5), 669\u2013676 (2006). https:\/\/doi.org\/10.1109\/TVCG.2006.120","journal-title":"IEEE TVCG"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-319-91908-9_21","volume-title":"Computing and Software Science","author":"C Baier","year":"2019","unstructured":"Baier, C., Hermanns, H., Katoen, J.-P.: The 10,000 facets of MDP model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 420\u2013451. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_21"},{"key":"20_CR3","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL \u2014 a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020949"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-17465-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bunte","year":"2019","unstructured":"Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21\u201339. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2 ISBN 9783030174651"},{"key":"20_CR6","unstructured":"Card, S.K., Shneiderman, B., MacKinlay, J.D.: Readings in Information Visualization-Using Vision to Think. Series in Interactive Technologies. Morgan Kaufmann Publishers (1999). ISBN 1-55860-533-9"},{"key":"20_CR7","doi-asserted-by":"publisher","unstructured":"Dai, J., Cheng, J.: HMMEditor: a visual editing tool for profile hidden Markov model. BMC Genom. 9(1), S8 (2008). https:\/\/doi.org\/10.1186\/1471-2164-9-S1-S8. ISSN 1471\u20132164","DOI":"10.1186\/1471-2164-9-S1-S8"},{"key":"20_CR8","doi-asserted-by":"publisher","unstructured":"Elmqvist, N., et al.: ZAME: interactive large-scale graph visualization. In: 2008 IEEE PacificVis, pp. 215\u2013222 (2008). https:\/\/doi.org\/10.1109\/PACIFICVIS.2008.4475479","DOI":"10.1109\/PACIFICVIS.2008.4475479"},{"key":"20_CR9","doi-asserted-by":"publisher","unstructured":"Franz, M., et al.: Cytoscape.js 2023 update: a graph theory library for visualization and analysis. Bioinformatics 39(1) (2023). https:\/\/doi.org\/10.1093\/bioinformatics\/btad031. ISSN 1367\u20134811","DOI":"10.1093\/bioinformatics\/btad031"},{"key":"20_CR10","doi-asserted-by":"publisher","unstructured":"Garavel, H., et al.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89\u2013107 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0244-z. ISSN 1433\u20132787","DOI":"10.1007\/s10009-012-0244-z"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1007\/11880240_49","volume-title":"Model Driven Engineering Languages and Systems","author":"H Goldsby","year":"2006","unstructured":"Goldsby, H., Cheng, B.H.C., Konrad, S., Kamdoum, S.: A visualization framework for the modeling and formal analysis of high assurance systems. In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds.) MODELS 2006. LNCS, vol. 4199, pp. 707\u2013721. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11880240_49"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-03367-4_30","volume-title":"Algorithms and Data Structures","author":"R G\u00f6rke","year":"2009","unstructured":"G\u00f6rke, R., Hartmann, T., Wagner, D.: Dynamic graph clustering using minimum-cut trees. In: Dehne, F., Gavrilova, M., Sack, J.-R., T\u00f3th, C.D. (eds.) WADS 2009. LNCS, vol. 5664, pp. 339\u2013350. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03367-4_30 ISBN 978-3-642-03367-4"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-030-83723-5_3","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends","author":"TP Gros","year":"2021","unstructured":"Gros, T.P., Gro\u00df, D., Gumhold, S., Hoffmann, J., Klauck, M., Steinmetz, M.: TraceVis: towards visualization for deep statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12479, pp. 27\u201346. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_3"},{"issue":"6","key":"20_CR14","doi-asserted-by":"publisher","first-page":"953","DOI":"10.1109\/TVCG.2009.108","volume":"15","author":"F van Ham","year":"2009","unstructured":"van Ham, F., Perer, A.: Search, show context, expand on demand: supporting large graph exploration with degree-of-interest. IEEE TVCG 15(6), 953\u2013960 (2009). https:\/\/doi.org\/10.1109\/TVCG.2009.108","journal-title":"IEEE TVCG"},{"key":"20_CR15","unstructured":"Hensel, C., et al.: The probabilistic model checker storm (2020). arXiv: 2002.07080 [cs.SE]"},{"key":"20_CR16","unstructured":"Horak, T., Dachselt, R.: Hierarchical graphs on mobile devices: a lane-based approach. In: CHI MobileVis Workshop (2018)"},{"key":"20_CR17","doi-asserted-by":"publisher","unstructured":"Horak, T., et al.: Visual analysis of hyperproperties for understanding model checking results. IEEE TVCG 28(1), 357\u2013367 (2022). https:\/\/doi.org\/10.1109\/TVCG.2021.3114866. ISSN 1941\u20130506","DOI":"10.1109\/TVCG.2021.3114866"},{"issue":"1","key":"20_CR18","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1109\/TVCG.2015.2466992","volume":"22","author":"J Johansson","year":"2016","unstructured":"Johansson, J., Forsell, C.: Evaluation of parallel coordinates: overview, categorization and guidelines for future research. IEEE TVCG 22(1), 579\u2013588 (2016). https:\/\/doi.org\/10.1109\/TVCG.2015.2466992","journal-title":"IEEE TVCG"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-49519-3_19","volume-title":"Formal Methods in Computer-Aided Design","author":"G Kamhi","year":"1998","unstructured":"Kamhi, G., Fix, L., Binyamini, Z.: Symbolic model checking visualization. In: Gopalakrishnan, G., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 290\u2013302. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49519-3_19 ISBN9783540495192"},{"key":"20_CR20","doi-asserted-by":"publisher","unstructured":"Katoen, J.-P., et al.: The ins and outs of the probabilistic model checker MRMC. IPerform. Eval. 68(2), 90\u2013104 (2011). https:\/\/doi.org\/10.1016\/j.peva.2010.04.001. ISSN 0166\u20135316","DOI":"10.1016\/j.peva.2010.04.001"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06793-3","volume-title":"Multivariate Network Visualization","year":"2014","unstructured":"Kerren, A., Purchase, H.C., Ward, M.O. (eds.): Multivariate Network Visualization. LNCS, vol. 8380. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06793-3"},{"key":"20_CR22","doi-asserted-by":"publisher","unstructured":"Korn, M., et al.: Interactive Visualization Meets Probabilistic Model Checking Artifact (2023). https:\/\/doi.org\/10.5281\/zenodo.8172531","DOI":"10.5281\/zenodo.8172531"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"20_CR24","doi-asserted-by":"publisher","unstructured":"Liu, Y., et al.: HybridVis: an adaptive hybrid-scale visualization of multivariate graphs. JVLC 41, 100\u2013110 (2017). https:\/\/doi.org\/10.1016\/j.jvlc.2017.03.008. ISSN 1045\u2013926X","DOI":"10.1016\/j.jvlc.2017.03.008"},{"key":"20_CR25","doi-asserted-by":"publisher","unstructured":"McGregor, S., et al.: Facilitating testing and debugging of Markov Decision Processes with interactive visualization. In: IEEE VL\/HCC 2015, pp. 53\u201361 (2015). https:\/\/doi.org\/10.1109\/VLHCC.2015.7357198","DOI":"10.1109\/VLHCC.2015.7357198"},{"issue":"3","key":"20_CR26","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1111\/cgf.13728","volume":"38","author":"C Nobre","year":"2019","unstructured":"Nobre, C., et al.: The state of the art in visualizing multivariate networks. CGF 38(3), 807\u2013832 (2019). https:\/\/doi.org\/10.1111\/cgf.13728","journal-title":"CGF"},{"issue":"2","key":"20_CR27","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1080\/10691898.2016.1207404","volume":"24","author":"M Pfannkuch","year":"2016","unstructured":"Pfannkuch, M., Budgett, S.: Markov processes: exploring the use of dynamic visualizations to enhance student understanding. JSE 24(2), 63\u201373 (2016). https:\/\/doi.org\/10.1080\/10691898.2016.1207404","journal-title":"JSE"},{"key":"20_CR28","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.envsoft.2019.03.005","volume":"116","author":"WJ Raseman","year":"2019","unstructured":"Raseman, W.J., Jacobson, J., Kasprzyk, J.R.: Parasol: an open source, interactive parallel coordinates library for multi-objective decision making. EMS 116, 153\u2013163 (2019). https:\/\/doi.org\/10.1016\/j.envsoft.2019.03.005","journal-title":"EMS"},{"key":"20_CR29","doi-asserted-by":"publisher","unstructured":"Tan, Y.-Q., et al.: VecRoad: point-based iterative graph exploration for road graphs extraction. In: 2020 IEEE\/CVF CVPR, pp. 8907\u20138915 (2020). https:\/\/doi.org\/10.1109\/CVPR42600.2020.00893","DOI":"10.1109\/CVPR42600.2020.00893"},{"issue":"1","key":"20_CR30","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1109\/TVCG.2018.2864911","volume":"25","author":"Y Wang","year":"2019","unstructured":"Wang, Y., et al.: Structure-aware fisheye views for efficient large graph exploration. IEEE TVCG 25(1), 566\u2013575 (2019). https:\/\/doi.org\/10.1109\/TVCG.2018.2864911","journal-title":"IEEE TVCG"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-47115-5_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,4]],"date-time":"2023-11-04T00:04:21Z","timestamp":1699056261000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-47115-5_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031471148","9783031471155"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-47115-5_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"31 October 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Eindhoven","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 November 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 November 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}