{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T01:10:36Z","timestamp":1768266636907,"version":"3.49.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2009,3,25]],"date-time":"2009-03-25T00:00:00Z","timestamp":1237939200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGMETRICS Perform. Eval. Rev."],"published-print":{"date-parts":[[2009,3,25]]},"abstract":"<jats:p>We describe some of the advanced features of the software tool SmArT, the Stochastic Model checking Analyzer for Reliability and Timing. Initially conceived as a software package for numerical solution and discrete-event simulation of stochastic models, SmArT now also provides powerful modelchecking capabilities, thanks to its extensive use of various forms of decision diagrams, which in turn also greatly increase the efficiency of its stochastic analysis algorithms. These aspects make it an excellent choice when tackling systems with extremely large state spaces.<\/jats:p>","DOI":"10.1145\/1530873.1530885","type":"journal-article","created":{"date-parts":[[2009,4,21]],"date-time":"2009-04-21T14:14:44Z","timestamp":1240323284000},"page":"58-63","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Advanced features in SMART"],"prefix":"10.1145","volume":"36","author":[{"given":"Gianfranco","family":"Ciardo","sequence":"first","affiliation":[{"name":"University of California, Riverside"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew S.","family":"Miner","sequence":"additional","affiliation":[{"name":"Iowa State University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Min","family":"Wan","sequence":"additional","affiliation":[{"name":"Yahoo! Inc."}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,3,25]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"132","volume-title":"Adv. in Petri Nets","author":"Ajmone Marsan M.","year":"1987","unstructured":"M. Ajmone Marsan and G. Chiola . On Petri nets with deterministic and exponentially distributed firing times . In Adv. in Petri Nets 1987 , LNCS 266, pages 132 -- 145 . Springer-Verlag , 1987. M. Ajmone Marsan and G. Chiola. On Petri nets with deterministic and exponentially distributed firing times. In Adv. in Petri Nets 1987, LNCS 266, pages 132--145. Springer-Verlag, 1987."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.12.3.203.12634"},{"key":"e_1_2_1_4_1","volume-title":"Performance '93","author":"Choi H.","year":"1993","unstructured":"H. Choi , V.G. Kulkarni , and K.S. Trivedi . Markov regenerative stochastic Petri nets . In Performance '93 . North-Holland , Sept. 1993 . H. Choi, V.G. Kulkarni, and K.S. Trivedi. Markov regenerative stochastic Petri nets. In Performance '93. North-Holland, Sept. 1993."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/978-3-540-72522-0_9","volume-title":"Formal Methods for Performance Evaluation, LNCS 4486","author":"Ciardo G.","year":"2007","unstructured":"G. Ciardo . Data representation and efficient solution: a decision diagram approach . In Formal Methods for Performance Evaluation, LNCS 4486 , pages 371 -- 394 , May 2007 . Springer-Verlag . G. Ciardo. Data representation and efficient solution: a decision diagram approach. In Formal Methods for Performance Evaluation, LNCS 4486, pages 371--394, May 2007. Springer-Verlag."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.297939"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/PNPM.1993.393454"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694474"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220917.3221217"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/826035.826829"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328690.1328697"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_4"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_13"},{"key":"e_1_2_1_14_1","volume-title":"Model Checking","author":"Clarke E.M.","year":"1999","unstructured":"E.M. Clarke , O. Grumberg , and D.A. Peled . Model Checking . MIT Press , 1999 . E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 1999."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/278298.278303"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/882474.883471"},{"key":"e_1_2_1_17_1","first-page":"23","volume-title":"Proc. PMCCS","author":"Jones R.L.","year":"2003","unstructured":"R.L. Jones and G. Ciardo . Regenerative simulation of stochastic Petri nets with discrete and continuous timing . In Proc. PMCCS , pages 23 -- 26 , Sept. 2003 . R.L. Jones and G. Ciardo. Regenerative simulation of stochastic Petri nets with discrete and continuous timing. In Proc. PMCCS, pages 23--26, Sept. 2003."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/882474.883484"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/339331.339417"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/978-3-540-24611-4_9","volume-title":"Validation of Stochastic Systems, LNCS 2925","author":"Miner A.S.","year":"2004","unstructured":"A.S. Miner and D. Parker . Symbolic representations and analysis of large state spaces . In Validation of Stochastic Systems, LNCS 2925 , pages 296 -- 338 . Springer-Verlag , 2004 . A.S. Miner and D. Parker. Symbolic representations and analysis of large state spaces. In Validation of Stochastic Systems, LNCS 2925, pages 296--338. Springer-Verlag, 2004."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/317795.317819"},{"key":"e_1_2_1_22_1","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"Stewart W.J.","year":"1994","unstructured":"W.J. Stewart . Introduction to the Numerical Solution of Markov Chains . Princeton University Press , 1994 . W.J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-95891-8_52"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-95891-8_53"},{"key":"e_1_2_1_25_1","unstructured":"M. Wan G. Ciardo and A.S. Miner. Decision-diagram-based approximate steady-state analysis of large structured Markov models. In preparation.  M. Wan G. Ciardo and A.S. Miner. Decision-diagram-based approximate steady-state analysis of large structured Markov models. In preparation."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763573"}],"container-title":["ACM SIGMETRICS Performance Evaluation Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1530873.1530885","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1530873.1530885","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:23Z","timestamp":1750253423000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1530873.1530885"}},"subtitle":["the stochastic model checking analyzer for reliability and timing"],"short-title":[],"issued":{"date-parts":[[2009,3,25]]},"references-count":26,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,3,25]]}},"alternative-id":["10.1145\/1530873.1530885"],"URL":"https:\/\/doi.org\/10.1145\/1530873.1530885","relation":{},"ISSN":["0163-5999"],"issn-type":[{"value":"0163-5999","type":"print"}],"subject":[],"published":{"date-parts":[[2009,3,25]]},"assertion":[{"value":"2009-03-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}