{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:54:01Z","timestamp":1762458841844},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642169007"},{"type":"electronic","value":"9783642169014"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_26","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T12:40:06Z","timestamp":1289220006000},"page":"388-403","source":"Crossref","is-referenced-by-count":24,"title":["Model Checking Hierarchical Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Jun","family":"Sun","sequence":"first","affiliation":[]},{"given":"Songzheng","family":"Song","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"26_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing Safety and Liveness. Distributed Computing\u00a02(3), 117\u2013126 (1987)","journal-title":"Distributed Computing"},{"issue":"1","key":"26_CR2","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive Modules. Formal Methods in System Design\u00a015(1), 7\u201348 (1999)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"26_CR3","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"15","author":"J. Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast Randomized Consensus Using Shared Memory. Journal of Algorithms\u00a015(1), 441\u2013460 (1990)","journal-title":"Journal of Algorithms"},{"key":"26_CR4","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"26_CR5","doi-asserted-by":"publisher","DOI":"10.1002\/9780470750728","volume-title":"Cardiac Pacemakers Step by Step: an Illustrated Guide","author":"S.S. Barold","year":"2004","unstructured":"Barold, S.S., Stroopbandt, R.X., Sinnaeve, A.F.: Cardiac Pacemakers Step by Step: an Illustrated Guide. Blackwell Publishing, Malden (2004)"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Bellman, R.: A Markovian Decision Process. Journal of Mathematics of Mechanics\u00a06 (1957)","DOI":"10.1512\/iumj.1957.6.56038"},{"issue":"2","key":"26_CR7","doi-asserted-by":"publisher","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.\u00a098(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/Event-Based Software Model Checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 128\u2013147. Springer, Heidelberg (2004)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-642-05089-3_30","volume-title":"FM 2009: Formal Methods","author":"Y. Chen","year":"2009","unstructured":"Chen, Y., Sanders, J.W.: Unifying Probability with Nondeterminism. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 467\u2013482. Springer, Heidelberg (2009)"},{"key":"26_CR10","first-page":"131","volume-title":"QEST","author":"F. Ciesinski","year":"2006","unstructured":"Ciesinski, F., Baier, C.: LiQuor: A Tool for Qualitative and Quantitative Linear Time Analysis of Reactive Systems. In: QEST, pp. 131\u2013132. IEEE Computer Society, Los Alamitos (2006)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Geilen, M.: On the Construction of Monitors for Temporal Logic Properties. Electr. Notes Theor. Comput. Sci.\u00a055(2) (2001)","DOI":"10.1016\/S1571-0661(04)00252-X"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Rosu, G.: Synthesizing Monitors for Safety Properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 342\u2013356. Springer, Heidelberg (2002)"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"26_CR15","series-title":"International Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"C. Hoare","year":"1985","unstructured":"Hoare, C.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"26_CR16","first-page":"167","volume-title":"QEST","author":"J. Katoen","year":"2009","unstructured":"Katoen, J., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The Ins and Outs of the Probabilistic Model Checker MRMC. In: QEST, pp. 167\u2013176. IEEE Computer Society, Los Alamitos (2009)"},{"issue":"3","key":"26_CR17","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model Checking of Safety Properties. Formal Methods in System Design\u00a019(3), 291\u2013314 (2001)","journal-title":"Formal Methods in System Design"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-44829-2_5","volume-title":"Model Checking Software","author":"T. Latvala","year":"2003","unstructured":"Latvala, T.: Efficient Model Checking of Safety Properties. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 74\u201388. Springer, Heidelberg (2003)"},{"key":"26_CR19","first-page":"133","volume-title":"POPL","author":"D. Lehmann","year":"1981","unstructured":"Lehmann, D., Rabin, M.: On the Advantage of Free Choice: A Symmetric and Fully Distributed Solution to the Dining Philosophers Problem (Extended Abstract). In: POPL, pp. 133\u2013138. ACM, New York (1981)"},{"issue":"16","key":"26_CR20","doi-asserted-by":"publisher","first-page":"1901","DOI":"10.1001\/jama.295.16.1901","volume":"295","author":"W.H. Maisel","year":"2006","unstructured":"Maisel, W.H., Moynahan, M., Zuckerman, B.D., Gross, T.P., Tovar, O.H., Tillman, D., Schultz, D.B.: Pacemaker and ICD Generator Malfunctions. The Journal of American Medical Association\u00a0295(16), 1901\u20131906 (2006)","journal-title":"The Journal of American Medical Association"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11415787_10","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"C. Morgan","year":"2005","unstructured":"Morgan, C., Hoang, T.S., Abrial, J.: The Challenge of Probabilistic Event B - Extended Abstract. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455, pp. 162\u2013171. Springer, Heidelberg (2005)"},{"issue":"6","key":"26_CR22","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/BF01213492","volume":"8","author":"C. Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-Oriented Probability for CSP. Formal Asp. Comput.\u00a08(6), 617\u2013647 (1996)","journal-title":"Formal Asp. Comput."},{"issue":"9","key":"26_CR23","doi-asserted-by":"publisher","first-page":"794","DOI":"10.1109\/32.159837","volume":"18","author":"X. Nicollin","year":"1992","unstructured":"Nicollin, X., Sifakis, J., Yovine, S.: Compiling Real-time Specifications into Extended Automata. IEEE Transactions on Software Engineering\u00a018(9), 794\u2013804 (1992)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"26_CR24","first-page":"46","volume-title":"FOCS","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: FOCS, pp. 46\u201357. IEEE, Los Alamitos (1977)"},{"issue":"1","key":"26_CR25","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.: Verification of Multiprocess Probabilistic Protocols. Distributed Computing\u00a01(1), 53\u201372 (1986)","journal-title":"Distributed Computing"},{"key":"26_CR26","unstructured":"Roscoe, A.W.: Model-checking CSP, pp. 353\u2013378 (1994)"},{"key":"26_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-60630-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A.W. Roscoe","year":"1995","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical Compression for Model-Checking CSP or How to Check 1020 Dining Philosophers for Deadlock. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 133\u2013152. Springer, Heidelberg (1995)"},{"issue":"5","key":"26_CR28","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, Liveness and Fairness in Temporal Logic. Formal Asp. Comput.\u00a06(5), 495\u2013512 (1994)","journal-title":"Formal Asp. Comput."},{"key":"26_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi Automata from LTL Formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"key":"26_CR30","first-page":"127","volume-title":"TASE","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Chen, C.Q.: Integrating Specification and Programs for System Modeling and Verification. In: TASE, pp. 127\u2013135. IEEE Computer Society, Los Alamitos (2009)"},{"key":"26_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol.\u00a05643, pp. 709\u2013714. Springer, Heidelberg (2009)"},{"key":"26_CR32","first-page":"332","volume-title":"LICS","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: LICS, pp. 332\u2013344. IEEE Computer Society, Los Alamitos (1986)"},{"issue":"4","key":"26_CR33","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s11334-009-0100-9","volume":"5","author":"H. Zhu","year":"2009","unstructured":"Zhu, H., Qin, S., He, J., Bowen, J.: PTSC: Probability, Time and Shared-Variable Concurrency. International Journal on Innovations in Systems and Software Engineering\u00a05(4), 271\u2013294 (2009)","journal-title":"International Journal on Innovations in Systems and Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T00:12:41Z","timestamp":1559779961000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}