{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:43Z","timestamp":1761611263686},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540408147"},{"type":"electronic","value":"9783540452324"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45232-4_6","type":"book-chapter","created":{"date-parts":[[2010,6,23]],"date-time":"2010-06-23T19:19:34Z","timestamp":1277320774000},"page":"78-97","source":"Crossref","is-referenced-by-count":26,"title":["Logical and Stochastic Modeling with Smart"],"prefix":"10.1007","author":[{"given":"G.","family":"Ciardo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R. L.","family":"Jones","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. S.","family":"Miner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Siminiceanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/10722167_28","volume-title":"Computer Aided Verification","author":"C. Baier","year":"2000","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 358\u2013372. Springer, Heidelberg (2000)"},{"key":"6_CR2","unstructured":"Bengtsson, J., et al.: New Generation of Uppaal. In: Int. Workshop on Software Tools for Technology Transfer (June 1998)"},{"key":"6_CR3","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1109\/TCS.1978.1084534","volume":"CAS-25","author":"J.W. Brewer","year":"1978","unstructured":"Brewer, J.W.: Kronecker products and matrix calculus in system theory. IEEE Trans. Circ. and Syst.\u00a0CAS-25, 772\u2013781 (1978)","journal-title":"IEEE Trans. Circ. and Syst."},{"issue":"8","key":"6_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp.\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comp."},{"issue":"3","key":"6_CR5","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1287\/ijoc.12.3.203.12634","volume":"12","author":"P. Buchholz","year":"2000","unstructured":"Buchholz, P., Ciardo, G., Donatelli, S., Kemper, P.: Complexity of memory efficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comp.\u00a012(3), 203\u2013222 (2000)","journal-title":"INFORMS J. Comp."},{"issue":"7","key":"6_CR6","first-page":"506","volume":"20","author":"G. Ciardo","year":"1994","unstructured":"Ciardo, G., German, R., Lindemann, C.: A characterization of the stochastic process underlying a stochastic Petri net. IEEE TSE\u00a020(7), 506\u2013515 (1994)","journal-title":"IEEE TSE"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-44988-4_8","volume-title":"Application and Theory of Petri Nets 2000","author":"G. Ciardo","year":"2000","unstructured":"Ciardo, G., Luettgen, G., Siminiceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825, pp. 103\u2013122. Springer, Heidelberg (2000)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-45319-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Ciardo","year":"2001","unstructured":"Ciardo, G., Luettgen, G., Siminiceanu, R.: Saturation: An efficient iteration strategy for symbolic state space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 328\u2013342. Springer, Heidelberg (2001)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/3-540-36577-X_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Ciardo","year":"2003","unstructured":"Ciardo, G., Marmorstein, R., Siminiceanu, R.: Saturation unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 379\u2013393. Springer, Heidelberg (2003) (to appear)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/BFb0022196","volume-title":"Computer Performance Evaluation Modelling Techniques and Tools","author":"G. Ciardo","year":"1997","unstructured":"Ciardo, G., Miner, A.S.: Storage alternatives for large structured state spaces. In: Marie, R., Plateau, B., Calzarossa, M.C., Rubino, G.J. (eds.) TOOLS 1997. LNCS, vol.\u00a01245, pp. 44\u201357. Springer, Heidelberg (1997)"},{"key":"6_CR11","first-page":"22","volume-title":"Proc. PNPM","author":"G. Ciardo","year":"1999","unstructured":"Ciardo, G., Miner, A.S.: A data structure for the efficient Kronecker solution of GSPNs. In: Proc. PNPM, pp. 22\u201331. IEEE Comp. Soc. Press, Los Alamitos (1999)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/3-540-36126-X_16","volume-title":"Formal Methods in Computer-Aided Design","author":"G. Ciardo","year":"2002","unstructured":"Ciardo, G., Siminiceanu, R.: Using edge-valued decision diagrams for symbolic generation of shortest paths. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 256\u2013273. Springer, Heidelberg (2002)"},{"issue":"1","key":"6_CR13","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0166-5316(93)90026-Q","volume":"18","author":"G. Ciardo","year":"1993","unstructured":"Ciardo, G., Trivedi, K.S.: A decomposition approach for stochastic reward net models. Perf. Eval.\u00a018(1), 37\u201359 (1993)","journal-title":"Perf. Eval."},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. IBM Workshop on Logics of Programs, pp. 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Couvillion, J.A., et al.: Performability modeling with UltraSAN. IEEE Software, pp. 69\u201380 (September 1991)","DOI":"10.1109\/52.84218"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/3-540-46429-8_25","volume-title":"Computer Performance Evaluation. Modelling Techniques and Tools","author":"D. Daly","year":"2000","unstructured":"Daly, D., Deavours, D.D., Doyle, J.M., Webster, P.G., Sanders, W.H.: M\u00f6bius: an extensible tool for performance and dependability modeling. In: Haverkort, B.R., Bohnenkamp, H.C., Smith, C.U. (eds.) TOOLS 2000. LNCS, vol.\u00a01786, pp. 332\u2013336. Springer, Heidelberg (2000)"},{"key":"6_CR18","unstructured":"Jones, R.L.: Analysis of Phase-Type Stochastic Petri Nets with Discrete and Continuous Timing. Tech. Rep. CR-2000-210296, NASA Langley (June 2000)"},{"key":"6_CR19","first-page":"165","volume-title":"Proc. PNPM","author":"R.L. Jones","year":"2001","unstructured":"Jones, R.L., Ciardo, G.: On phased delay stochastic Petri nets: Definition and an application. In: Proc. PNPM, pp. 165\u2013174. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"6_CR20","unstructured":"Jones III., R.L.: Simulation and Numerical Solution of Stochastic Petri Nets with Discrete and Continuous Timing. Ph.D. thesis, College of William and Mary, Department of Computer Science, Williamsburg, VA (2002)"},{"issue":"1\u20132","key":"6_CR21","first-page":"9","volume":"4","author":"T. Kam","year":"1998","unstructured":"Kam, T., Villa, T., Brayton, R., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic\u00a04(1\u20132), 9\u201362 (1998)","journal-title":"Multiple-Valued Logic"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Proc. Comp. Perf. Eval. \/ TOOLS, April 2003, pp. 200\u2013204 (2003)","DOI":"10.1007\/3-540-46029-2_13"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Miner, A.S.: Efficient state space generation of GSPNs using decision diagrams. In: Proc. DSN, Washington, DC, June 2002, pp. 637\u2013646 (2002)","DOI":"10.1109\/DSN.2002.1029009"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-48745-X_2","volume-title":"Application and Theory of Petri Nets 1999","author":"A.S. Miner","year":"1999","unstructured":"Miner, A.S., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol.\u00a01639, pp. 6\u201325. Springer, Heidelberg (1999)"},{"key":"6_CR25","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/339331.339417","volume-title":"Proc. ACM SIGMETRICS","author":"A.S. Miner","year":"2000","unstructured":"Miner, A.S., Ciardo, G., Donatelli, S.: Using the exact state space of a Markov model to compute approximate stationary measures. In: Proc. ACM SIGMETRICS, pp. 207\u2013216. ACM Press, New York (2000)"},{"issue":"4","key":"6_CR26","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T. Murata","year":"1989","unstructured":"Murata, T.: Petri Nets: properties, analysis and applications. Proc. of the IEEE\u00a077(4), 541\u2013579 (1989)","journal-title":"Proc. of the IEEE"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1007\/3-540-58152-9_23","volume-title":"Application and Theory of Petri Nets 1994","author":"E. Pastor","year":"1994","unstructured":"Pastor, E., Roig, O., Cortadella, J., Badia, R.: Petri net analysis using Boolean manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol.\u00a0815, pp. 416\u2013435. Springer, Heidelberg (1994)"},{"key":"6_CR28","unstructured":"Tilgner, M., Takahashi, Y., Ciardo, G.: SNS 1.0: Synchronized Network Solver. In: Int. Workshop on Manufacturing and Petri Nets, June 1996, pp. 215\u2013234 (1996)"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Yovine, S.: Model checking timed automata. In: European Educational Forum: School on Embedded Systems, pp. 114\u2013152 (1996)","DOI":"10.1007\/3-540-65193-4_20"}],"container-title":["Lecture Notes in Computer Science","Computer Performance Evaluation. Modelling Techniques and Tools"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45232-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T06:55:02Z","timestamp":1559199302000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45232-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540408147","9783540452324"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45232-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}