The probabilistic model checker Storm

We present the probabilistic model checker Storm . Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the Jani and...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2022-08, Vol.24 (4), p.589-610
Main Authors: Hensel, Christian, Junges, Sebastian, Katoen, Joost-Pieter, Quatmann, Tim, Volk, Matthias
Format: Article
Language:English
Subjects:
Algorithms
Awards & honors
Command languages
Competitions and Challenges
Computer Science
Empirical analysis
Fault trees
Languages
Markov analysis
Markov chains
Petri nets
Probabilistic models
Probability theory
Rapid prototyping
Software Engineering
Software Engineering/Programming and Operating Systems
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c363t-cdcbae047ee83d39c3866cc6bab9a4e13aaca499dc16a071f0ae75cac921e7223
cites cdi_FETCH-LOGICAL-c363t-cdcbae047ee83d39c3866cc6bab9a4e13aaca499dc16a071f0ae75cac921e7223
container_end_page 610
container_issue 4
container_start_page 589
container_title International journal on software tools for technology transfer
container_volume 24
creator Hensel, Christian
Junges, Sebastian
Katoen, Joost-Pieter
Quatmann, Tim
Volk, Matthias
description We present the probabilistic model checker Storm . Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the Jani and Prism modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the probabilistic guarded command language. It has a modular setup in which solvers and symbolic engines can easily be exchanged. Its Python API allows for rapid prototyping by encapsulating Storm ’s fast and scalable algorithms. This paper reports on the main features of Storm and explains how to effectively use them. A description is provided of the main distinguishing functionalities of Storm . Finally, an empirical evaluation of different configurations of Storm on the QComp 2019 benchmark set is presented.
doi_str_mv 10.1007/s10009-021-00633-z
format article
fullrecord <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_journals_2697197132</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>2697197132</sourcerecordid><originalsourceid>FETCH-LOGICAL-c363t-cdcbae047ee83d39c3866cc6bab9a4e13aaca499dc16a071f0ae75cac921e7223</originalsourceid><addsrcrecordid>eNp9kE9PwzAMxSMEEmPwBThVQhwDTlKS5ogm_kmTODDOUeq6rKNdR9Id2KcnowhuSJbtw3vP1o-xcwFXAsBcx9TBcpCCA2il-O6ATUSeFmkKc_i7G3vMTmJcAQijjZ2wy8WSsk3oS182bROHBrOur6jNcEn4TiF7GfrQnbKj2reRzn7mlL3e3y1mj3z-_PA0u51zVFoNHCssPUFuiApVKYuq0BpRp3DrcxLKe_S5tRUK7cGIGjyZG_RopSAjpZqyizE3ffSxpTi4Vb8N63TSSW2NSKX2KjmqMPQxBqrdJjSdD59OgNvjcCMOl3C4bxxul0xqNMUkXr9R-Iv-x_UF61pivQ</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>2697197132</pqid></control><display><type>article</type><title>The probabilistic model checker Storm</title><source>Springer Nature</source><creator>Hensel, Christian ; Junges, Sebastian ; Katoen, Joost-Pieter ; Quatmann, Tim ; Volk, Matthias</creator><creatorcontrib>Hensel, Christian ; Junges, Sebastian ; Katoen, Joost-Pieter ; Quatmann, Tim ; Volk, Matthias</creatorcontrib><description>We present the probabilistic model checker Storm . Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the Jani and Prism modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the probabilistic guarded command language. It has a modular setup in which solvers and symbolic engines can easily be exchanged. Its Python API allows for rapid prototyping by encapsulating Storm ’s fast and scalable algorithms. This paper reports on the main features of Storm and explains how to effectively use them. A description is provided of the main distinguishing functionalities of Storm . Finally, an empirical evaluation of different configurations of Storm on the QComp 2019 benchmark set is presented.</description><identifier>ISSN: 1433-2779</identifier><identifier>EISSN: 1433-2787</identifier><identifier>DOI: 10.1007/s10009-021-00633-z</identifier><language>eng</language><publisher>Berlin/Heidelberg: Springer Berlin Heidelberg</publisher><subject>Algorithms ; Awards &amp; honors ; Command languages ; Competitions and Challenges ; Computer Science ; Empirical analysis ; Fault trees ; Languages ; Markov analysis ; Markov chains ; Petri nets ; Probabilistic models ; Probability theory ; Rapid prototyping ; Software Engineering ; Software Engineering/Programming and Operating Systems ; Theory of Computation</subject><ispartof>International journal on software tools for technology transfer, 2022-08, Vol.24 (4), p.589-610</ispartof><rights>The Author(s) 2021</rights><rights>The Author(s) 2021. This work is published under http://creativecommons.org/licenses/by/4.0/ (the “License”). Notwithstanding the ProQuest Terms and Conditions, you may use this content in accordance with the terms of the License.</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c363t-cdcbae047ee83d39c3866cc6bab9a4e13aaca499dc16a071f0ae75cac921e7223</citedby><cites>FETCH-LOGICAL-c363t-cdcbae047ee83d39c3866cc6bab9a4e13aaca499dc16a071f0ae75cac921e7223</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids></links><search><creatorcontrib>Hensel, Christian</creatorcontrib><creatorcontrib>Junges, Sebastian</creatorcontrib><creatorcontrib>Katoen, Joost-Pieter</creatorcontrib><creatorcontrib>Quatmann, Tim</creatorcontrib><creatorcontrib>Volk, Matthias</creatorcontrib><title>The probabilistic model checker Storm</title><title>International journal on software tools for technology transfer</title><addtitle>Int J Softw Tools Technol Transfer</addtitle><description>We present the probabilistic model checker Storm . Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the Jani and Prism modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the probabilistic guarded command language. It has a modular setup in which solvers and symbolic engines can easily be exchanged. Its Python API allows for rapid prototyping by encapsulating Storm ’s fast and scalable algorithms. This paper reports on the main features of Storm and explains how to effectively use them. A description is provided of the main distinguishing functionalities of Storm . Finally, an empirical evaluation of different configurations of Storm on the QComp 2019 benchmark set is presented.</description><subject>Algorithms</subject><subject>Awards &amp; honors</subject><subject>Command languages</subject><subject>Competitions and Challenges</subject><subject>Computer Science</subject><subject>Empirical analysis</subject><subject>Fault trees</subject><subject>Languages</subject><subject>Markov analysis</subject><subject>Markov chains</subject><subject>Petri nets</subject><subject>Probabilistic models</subject><subject>Probability theory</subject><subject>Rapid prototyping</subject><subject>Software Engineering</subject><subject>Software Engineering/Programming and Operating Systems</subject><subject>Theory of Computation</subject><issn>1433-2779</issn><issn>1433-2787</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2022</creationdate><recordtype>article</recordtype><recordid>eNp9kE9PwzAMxSMEEmPwBThVQhwDTlKS5ogm_kmTODDOUeq6rKNdR9Id2KcnowhuSJbtw3vP1o-xcwFXAsBcx9TBcpCCA2il-O6ATUSeFmkKc_i7G3vMTmJcAQijjZ2wy8WSsk3oS182bROHBrOur6jNcEn4TiF7GfrQnbKj2reRzn7mlL3e3y1mj3z-_PA0u51zVFoNHCssPUFuiApVKYuq0BpRp3DrcxLKe_S5tRUK7cGIGjyZG_RopSAjpZqyizE3ffSxpTi4Vb8N63TSSW2NSKX2KjmqMPQxBqrdJjSdD59OgNvjcCMOl3C4bxxul0xqNMUkXr9R-Iv-x_UF61pivQ</recordid><startdate>20220801</startdate><enddate>20220801</enddate><creator>Hensel, Christian</creator><creator>Junges, Sebastian</creator><creator>Katoen, Joost-Pieter</creator><creator>Quatmann, Tim</creator><creator>Volk, Matthias</creator><general>Springer Berlin Heidelberg</general><general>Springer Nature B.V</general><scope>C6C</scope><scope>AAYXX</scope><scope>CITATION</scope><scope>3V.</scope><scope>7SC</scope><scope>7XB</scope><scope>8AL</scope><scope>8AO</scope><scope>8FD</scope><scope>8FE</scope><scope>8FG</scope><scope>8FK</scope><scope>8G5</scope><scope>ABJCF</scope><scope>ABUWG</scope><scope>AFKRA</scope><scope>ARAPS</scope><scope>AZQEC</scope><scope>BENPR</scope><scope>BGLVJ</scope><scope>CCPQU</scope><scope>DWQXO</scope><scope>GNUQQ</scope><scope>GUQSH</scope><scope>HCIFZ</scope><scope>JQ2</scope><scope>K7-</scope><scope>L6V</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope><scope>M0N</scope><scope>M2O</scope><scope>M7S</scope><scope>MBDVC</scope><scope>P5Z</scope><scope>P62</scope><scope>PADUT</scope><scope>PQEST</scope><scope>PQQKQ</scope><scope>PQUKI</scope><scope>PRINS</scope><scope>PTHSS</scope><scope>Q9U</scope></search><sort><creationdate>20220801</creationdate><title>The probabilistic model checker Storm</title><author>Hensel, Christian ; Junges, Sebastian ; Katoen, Joost-Pieter ; Quatmann, Tim ; Volk, Matthias</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c363t-cdcbae047ee83d39c3866cc6bab9a4e13aaca499dc16a071f0ae75cac921e7223</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2022</creationdate><topic>Algorithms</topic><topic>Awards &amp; honors</topic><topic>Command languages</topic><topic>Competitions and Challenges</topic><topic>Computer Science</topic><topic>Empirical analysis</topic><topic>Fault trees</topic><topic>Languages</topic><topic>Markov analysis</topic><topic>Markov chains</topic><topic>Petri nets</topic><topic>Probabilistic models</topic><topic>Probability theory</topic><topic>Rapid prototyping</topic><topic>Software Engineering</topic><topic>Software Engineering/Programming and Operating Systems</topic><topic>Theory of Computation</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Hensel, Christian</creatorcontrib><creatorcontrib>Junges, Sebastian</creatorcontrib><creatorcontrib>Katoen, Joost-Pieter</creatorcontrib><creatorcontrib>Quatmann, Tim</creatorcontrib><creatorcontrib>Volk, Matthias</creatorcontrib><collection>SpringerOpen</collection><collection>CrossRef</collection><collection>ProQuest Central (Corporate)</collection><collection>Computer and Information Systems Abstracts</collection><collection>ProQuest Central (purchase pre-March 2016)</collection><collection>Computing Database (Alumni Edition)</collection><collection>ProQuest Pharma Collection</collection><collection>Technology Research Database</collection><collection>ProQuest SciTech Collection</collection><collection>ProQuest Technology Collection</collection><collection>ProQuest Central (Alumni) (purchase pre-March 2016)</collection><collection>Research Library (Alumni Edition)</collection><collection>Materials Science &amp; Engineering Collection</collection><collection>ProQuest Central (Alumni)</collection><collection>ProQuest Central UK/Ireland</collection><collection>Advanced Technologies &amp; Aerospace Database‎ (1962 - current)</collection><collection>ProQuest Central Essentials</collection><collection>ProQuest Central</collection><collection>Technology Collection</collection><collection>ProQuest One Community College</collection><collection>ProQuest Central</collection><collection>ProQuest Central Student</collection><collection>Research Library Prep</collection><collection>SciTech Premium Collection (Proquest) (PQ_SDU_P3)</collection><collection>ProQuest Computer Science Collection</collection><collection>Computer Science Database</collection><collection>ProQuest Engineering Collection</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><collection>Computing Database</collection><collection>ProQuest Research Library</collection><collection>ProQuest Engineering Database</collection><collection>Research Library (Corporate)</collection><collection>ProQuest Advanced Technologies &amp; Aerospace Database</collection><collection>ProQuest Advanced Technologies &amp; Aerospace Collection</collection><collection>Research Library China</collection><collection>ProQuest One Academic Eastern Edition (DO NOT USE)</collection><collection>ProQuest One Academic</collection><collection>ProQuest One Academic UKI Edition</collection><collection>ProQuest Central China</collection><collection>Engineering Collection</collection><collection>ProQuest Central Basic</collection><jtitle>International journal on software tools for technology transfer</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Hensel, Christian</au><au>Junges, Sebastian</au><au>Katoen, Joost-Pieter</au><au>Quatmann, Tim</au><au>Volk, Matthias</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>The probabilistic model checker Storm</atitle><jtitle>International journal on software tools for technology transfer</jtitle><stitle>Int J Softw Tools Technol Transfer</stitle><date>2022-08-01</date><risdate>2022</risdate><volume>24</volume><issue>4</issue><spage>589</spage><epage>610</epage><pages>589-610</pages><issn>1433-2779</issn><eissn>1433-2787</eissn><abstract>We present the probabilistic model checker Storm . Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the Jani and Prism modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the probabilistic guarded command language. It has a modular setup in which solvers and symbolic engines can easily be exchanged. Its Python API allows for rapid prototyping by encapsulating Storm ’s fast and scalable algorithms. This paper reports on the main features of Storm and explains how to effectively use them. A description is provided of the main distinguishing functionalities of Storm . Finally, an empirical evaluation of different configurations of Storm on the QComp 2019 benchmark set is presented.</abstract><cop>Berlin/Heidelberg</cop><pub>Springer Berlin Heidelberg</pub><doi>10.1007/s10009-021-00633-z</doi><tpages>22</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 1433-2779
ispartof International journal on software tools for technology transfer, 2022-08, Vol.24 (4), p.589-610
issn 1433-2779
1433-2787
language eng
recordid cdi_proquest_journals_2697197132
source Springer Nature
subjects Algorithms
Awards & honors
Command languages
Competitions and Challenges
Computer Science
Empirical analysis
Fault trees
Languages
Markov analysis
Markov chains
Petri nets
Probabilistic models
Probability theory
Rapid prototyping
Software Engineering
Software Engineering/Programming and Operating Systems
Theory of Computation
title The probabilistic model checker Storm
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-07T19%3A43%3A10IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=The%20probabilistic%20model%20checker%20Storm&rft.jtitle=International%20journal%20on%20software%20tools%20for%20technology%20transfer&rft.au=Hensel,%20Christian&rft.date=2022-08-01&rft.volume=24&rft.issue=4&rft.spage=589&rft.epage=610&rft.pages=589-610&rft.issn=1433-2779&rft.eissn=1433-2787&rft_id=info:doi/10.1007/s10009-021-00633-z&rft_dat=%3Cproquest_cross%3E2697197132%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c363t-cdcbae047ee83d39c3866cc6bab9a4e13aaca499dc16a071f0ae75cac921e7223%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=2697197132&rft_id=info:pmid/&rfr_iscdi=true