{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:43:54Z","timestamp":1750308234493,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2005,3,1]],"date-time":"2005-03-01T00:00:00Z","timestamp":1109635200000},"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":[[2005,3]]},"abstract":"<jats:p>Both logic and stochastic analysis have strong theoretical underpinnings, but they have been traditionally relegated to separate areas of computer science, the former focusing on logic and discrete algorithms, the latter on exact or approximate numerical methods. In the last few years, though, there has been a convergence of research in these two areas, due to the realization that data structures used in one area can benefit the other and that, by merging the goals of the two areas, a more integrated approach to system analysis can be derived. In this paper, we describe some of the beneficial interactions between the two, and some of the research challenges ahead.<\/jats:p>","DOI":"10.1145\/1059816.1059818","type":"journal-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T18:32:02Z","timestamp":1169058722000},"page":"4-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Implicit data structures for logic and stochastic systems analysis"],"prefix":"10.1145","volume":"32","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"}]}],"member":"320","published-online":{"date-parts":[[2005,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733930"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/647883.738412"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.12.3.203.12634"},{"issue":"1","key":"e_1_2_1_7_1","first-page":"69","article-title":"Model-checking large structured Markov chains","volume":"56","author":"Buchholz P.","year":"2003","unstructured":"P. Buchholz , J. P. Katoen , P. Kemper , and C. Tepper . Model-checking large structured Markov chains . JLAP , 56 ( 1\/2 ): 69 -- 97 , 2003 .]] P. Buchholz, J. P. Katoen, P. Kemper, and C. Tepper. Model-checking large structured Markov chains. JLAP, 56(1\/2):69--97, 2003.]]","journal-title":"JLAP"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/826033.826780"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694474"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/826035.826829"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/646187.683254"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_4"},{"key":"e_1_2_1_14_1","first-page":"52","volume-title":"Proc. IBM Workshop on Logics of Programs, LNCS 131","author":"Clarke E. M.","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson . Design and synthesis of synchronization skeletons using branching time temporal logic . In Proc. IBM Workshop on Logics of Programs, LNCS 131 , pages 52 -- 71 . Springer-Verlag , 1981 .]] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. IBM Workshop on Logics of Programs, LNCS 131, pages 52--71. Springer-Verlag, 1981.]]"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1981.6312174"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/826034.826795"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.laa.2004.01.006"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647741.735971"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/278298.278303"},{"key":"e_1_2_1_20_1","first-page":"188","volume-title":"Proc. NSMC","author":"Hermanns H.","year":"1999","unstructured":"H. Hermanns , J. Meyer-Kayser , and M. Siegle . Multi terminal binary decision diagrams to represent and analyse continuous-time Markov chains . In Proc. NSMC , pages 188 -- 207 , Sept. 1999 . Prensas Universitarias de Zaragoza, Spain.]] H. Hermanns, J. Meyer-Kayser, and M. Siegle. Multi terminal binary decision diagrams to represent and analyse continuous-time Markov chains. In Proc. NSMC, pages 188--207, Sept. 1999. Prensas Universitarias de Zaragoza, Spain.]]"},{"key":"e_1_2_1_21_1","volume-title":"Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic, 4(1--2):9--62","author":"Kam T.","year":"1998","unstructured":"T. Kam , T. Villa , R. Brayton , and A. Sangiovanni-Vincentelli . Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic, 4(1--2):9--62 , 1998 .]] T. Kam, T. Villa, R. Brayton, and A. Sangiovanni-Vincentelli. Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic, 4(1--2):9--62, 1998.]]"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.541433"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2944225.2944369"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/647883.738245"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1025129.1026097"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/647746.734068"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/339331.339417"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/317795.317819"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["ACM SIGMETRICS Performance Evaluation Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1059816.1059818","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1059816.1059818","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:46Z","timestamp":1750264306000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1059816.1059818"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,3]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,3]]}},"alternative-id":["10.1145\/1059816.1059818"],"URL":"https:\/\/doi.org\/10.1145\/1059816.1059818","relation":{},"ISSN":["0163-5999"],"issn-type":[{"type":"print","value":"0163-5999"}],"subject":[],"published":{"date-parts":[[2005,3]]},"assertion":[{"value":"2005-03-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}