{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:29:15Z","timestamp":1761596955089},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4-5","license":[{"start":{"date-parts":[[2006,4,4]],"date-time":"2006-04-04T00:00:00Z","timestamp":1144108800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2006,8]]},"DOI":"10.1007\/s10009-005-0216-7","type":"journal-article","created":{"date-parts":[[2006,4,4]],"date-time":"2006-04-04T12:00:29Z","timestamp":1144152029000},"page":"397-409","source":"Crossref","is-referenced-by-count":16,"title":["Finite horizon analysis of Markov Chains with the Mur\u03d5 verifier"],"prefix":"10.1007","volume":"8","author":[{"given":"Giuseppe Della","family":"Penna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benedetto","family":"Intrigila","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Melatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marisa Venturini","family":"Zilli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,4,4]]},"reference":[{"key":"216_CR1","doi-asserted-by":"crossref","unstructured":"Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In: ICCAD \u201993: Proceedings of the 1993 IEEE\/ACM International Conference on Computer-Aided Design, pp. 188\u2013191. IEEE Computer Society Press, Los Alamitos, CA, USA (1993)","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"216_CR2","doi-asserted-by":"crossref","unstructured":"Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, P., Marchetti-Spaccamela, A. (eds.) Automata, Languages and Programming, 24th International Colloquium, ICALP\u201997, Bologna, Italy, Proceedings, vol. 1256 of Lecture Notes in Computer Science, pp. 430\u2013440. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63165-8_199"},{"key":"216_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90157-6","volume-title":"Introduction to Markov Chains","author":"E. Behrends","year":"2000","unstructured":"Behrends, E.: Introduction to Markov Chains, Vieweg. Germany (2000)"},{"key":"216_CR4","doi-asserted-by":"crossref","unstructured":"Bianco, de Alfaro: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) Foundations of Software Technology and Theoretical Computer Science, 15th Conference, Bangalore, India, Proceedings, vol. 1026 of Lecture Notes in Computer Science, pp. 499\u2013513. Springer, Berlin (1995)","DOI":"10.1007\/3-540-60692-0_70"},{"key":"216_CR5","doi-asserted-by":"crossref","unstructured":"Bobbio, A., Ciancamerla, E., Franceschinis, G., Gaeta, R., Minichino, M., Portinale, L.: Methods of increasing modelling power for safety analysis, applied to a turbine digital control system. In: Anderson, S., Bologna, S., Felici, M. (eds.) Computer Safety, Reliability and Security 21st International Conference, SAFECOMP 2002, Catania, Italy, Proceedings, vol. 2434 of Lecture Notes in Computer Science, pp. 212\u2013223. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45732-1_21"},{"key":"216_CR6","doi-asserted-by":"crossref","unstructured":"Bobbio, A., Ciancamerla, E., Gribaudo, M., Horvath, A., Minichino, M., Tronci, E.: Model Checking based on fluid petri nets for the temperature control system of the icaro co-generative Planti. In: Anderson, S., Bologna, S., Felici, M. (eds.) Computer Safety, Reliability and Security, 21st International Conference, SAFECOMP 2002, Catania, Italy, Proceedings, vol. 2434 of Lecture Notes in Computer Science, pp. 273\u2013283. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45732-1_27"},{"key":"216_CR7","unstructured":"Bobbio, A., Bologna, S., Minichino, M., Ciancamerla, E., Incalcaterra, P., Kropp, C., Tronci, E.: Advanced techniques for safety analysis applied to the gas turbine control system of Icaro co generative plant. In: Proceedings of X Convegno TESEC, Genova, Italy (2001)"},{"issue":"8","key":"216_CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35 (8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"216_CR9","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98 (2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"216_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., McMillan, K.L., Zhao, X., Fujita, M., Yang, J.: Spectral transforms for large Boolean functions with applications to technology mapping. In: Proceedings of the 30th International on Design automation conference, pp. 54\u201360. ACM Press, New York (1993)","DOI":"10.1145\/157485.164569"},{"key":"216_CR11","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: Proceedings of the IEEE Conference on Decision and Control, pp. 338\u2013345. IEEE Press, Piscataway, NJ (1988)","DOI":"10.1109\/SFCS.1988.21950"},{"issue":"4","key":"216_CR12","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM. 42(4), 857\u2013907 (1995)","journal-title":"J. ACM."},{"key":"216_CR13","unstructured":"CUDD Web Page: http:\/\/vlsi.colorado.edu\/~fabio\/ (2004)"},{"key":"216_CR14","unstructured":"de Alfaro, L.: Formal verification of performance and reliability of real-time systems. Technical Report STAN-CS-TR-96-1571, Stanford University (1996)"},{"key":"216_CR15","doi-asserted-by":"crossref","unstructured":"Della Penna, G., Intrigila, B., Melatti, I., Minichino, M., Ciancamerla, E., Parisse, A., Tronci, E., Venturini Zilli, M.: Automatic verification of a turbogas control system with the mur\u03c6 verifier. In: Maler, O., Pnueli, A. (eds.) Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, Proceedings, vol. 2623 of Lecture Notes in Computer Science, pp. 141\u2013155. Springer, Berlin (2003)","DOI":"10.1007\/3-540-36580-X_13"},{"key":"216_CR16","doi-asserted-by":"crossref","unstructured":"Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Venturini Zilli, M.: Finite horizon analysis of markov chains with the Mur\u03c6 verifier. In: Geist, D., Tronci, E. (eds.) Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L\u2019Aquila, Italy, Proceedings, vol. 2860 of Lecture Notes in Computer Science, pp. 394\u2013409. Springer (2003)","DOI":"10.1007\/978-3-540-39724-3_34"},{"key":"216_CR17","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer and Processors, pp. 522\u2013525. IEEE Computer Society, Washington, DC (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"216_CR18","unstructured":"ENEA: Proprietary ICARO Documentation (2001)"},{"key":"216_CR19","volume-title":"Time and Probability in Formal Design of Distributed Systems","author":"H. Hansson","year":"1994","unstructured":"Hansson, H.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)"},{"issue":"5","key":"216_CR20","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and probability. Formal Aspects Comput 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput"},{"key":"216_CR21","doi-asserted-by":"crossref","unstructured":"Hart, S., Sharir, M.: Probabilistic temporal logics for finite and bounded models. In: Proceedings of the sixteenth annual ACM symposium on Theory of computing, pp. 1\u201313. ACM Press, New York (1984)","DOI":"10.1145\/800057.808660"},{"key":"216_CR22","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann,G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Upper Saddle River, NJ (1991)"},{"issue":"5","key":"216_CR23","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The spin model checker. IEEE Trans. Software Eng. 23(5), 279\u2013295, (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"216_CR24","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J.T., Harder, U. (eds.) Computer Performance Evaluation, Modelling Techniques and Tools 12th International Conference, TOOLS 2002, London, UK, Proceedings, vol. 2324 of Lecture Notes in Computer Science, pp. 200\u2013204. Springer, Berlin (2002)","DOI":"10.1007\/3-540-46029-2_13"},{"key":"216_CR25","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8\u201312, 2002, Proceedings, vol. 2280 of Lecture Notes in Computer Science, pp. 52\u201366. Springer, Berlin (2002)","DOI":"10.1007\/3-540-46002-0_5"},{"issue":"1","key":"216_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"216_CR27","doi-asserted-by":"crossref","unstructured":"Lehmann, D., Rabin, M.: On the advantages of free choice: A symmetric fully distributed solution to the dining philosophers problem (extended abstract). In: Proceedings of 8th Symposium on Principles of Programming Languages, pp. 133\u2013138 (1981)","DOI":"10.1145\/567532.567547"},{"key":"216_CR28","doi-asserted-by":"crossref","unstructured":"Lynch, N., Saias, I., Segala, R.: Proving time bounds for randomized distributed algorithms. In: Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, pp. 314\u2013323. ACM Press, New York (1994)","DOI":"10.1145\/197917.198117"},{"key":"216_CR29","unstructured":"Murphi Web Page: http:\/\/sprout.stanford.edu\/dill\/murphi.html (2004)"},{"issue":"1","key":"216_CR30","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1), 53\u201372 (1986)","journal-title":"Distrib. Comput."},{"issue":"1","key":"216_CR31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"Pnueli, A., Zuck, L.D.: Probabilistic verification. Inf. Comput. 103(1), 1\u201329 (1993)","journal-title":"Inf. Comput."},{"key":"216_CR32","unstructured":"PRISM Web Page: http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/ (2004)"},{"key":"216_CR33","doi-asserted-by":"crossref","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR \u201994, Concurrency Theory, 5th International Conference, Uppsala, Sweden, Proceedings, vol. 836 of Lecture Notes in Computer Science, pp. 481\u2013496. Springer, Berlin (1994)","DOI":"10.1007\/978-3-540-48654-1_35"},{"key":"216_CR34","unstructured":"SPIN Web Page: http:\/\/spinroot.com (2004)"},{"key":"216_CR35","doi-asserted-by":"crossref","unstructured":"Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M.: Exploiting transition locality in automatic verification. In: Margaria, T., Melham, T.F. (eds.) Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, Proceedings, vol. 2144 of Lecture Notes in Computer Science, pp. 259\u2013274. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44798-9_22"},{"key":"216_CR36","doi-asserted-by":"crossref","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: 26th Annual Symposium on Foundations of Computer Science, pp. 327\u2013338, IEEE CS Press, Portland, OR (1985)","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-005-0216-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-005-0216-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-005-0216-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:22Z","timestamp":1559114722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-005-0216-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,4,4]]},"references-count":36,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2006,8]]}},"alternative-id":["216"],"URL":"https:\/\/doi.org\/10.1007\/s10009-005-0216-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,4,4]]}}}