{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T04:53:03Z","timestamp":1726030383145},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030206512"},{"type":"electronic","value":"9783030206529"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-20652-9_20","type":"book-chapter","created":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:03:25Z","timestamp":1558983805000},"page":"298-315","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Symbolic Model Checking of Weighted PCTL Using Dependency Graphs"],"prefix":"10.1007","author":[{"given":"Mathias","family":"Claus Jensen","sequence":"first","affiliation":[]},{"given":"Anders","family":"Mariegaard","sequence":"additional","affiliation":[]},{"given":"Kim","family":"Guldstrand Larsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,5,28]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-40903-8_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Andova","year":"2004","unstructured":"Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 88\u2013104. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-40903-8_8"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-319-99154-2_5","volume-title":"Quantitative Evaluation of Systems","author":"G Bacci","year":"2018","unstructured":"Bacci, G., Hansen, M., Larsen, K.G.: On the verification of weighted kripke structures under uncertainty. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 71\u201386. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-99154-2_5"},{"key":"20_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11539452_9","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"F Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66\u201380. Springer, Heidelberg (2005). \n                    https:\/\/doi.org\/10.1007\/11539452_9"},{"key":"20_CR5","doi-asserted-by":"publisher","unstructured":"Christoffersen, P., Hansen, M., Mariegaard, A., Ringsmose, J.T., Larsen, K.G., Mardare, R.: Parametric verification of weighted systems. In: 2nd International Workshop on Synthesis of Complex Parameters, SynCoP 2015, London, United Kingdom, 11 April 2015, pp. 77\u201390 (2015). \n                    https:\/\/doi.org\/10.4230\/OASIcs.SynCoP.2015.77","DOI":"10.4230\/OASIcs.SynCoP.2015.77"},{"issue":"4","key":"20_CR6","doi-asserted-by":"publisher","first-page":"351","DOI":"10.3233\/FI-2018-1707","volume":"161","author":"AE Dalsgaard","year":"2018","unstructured":"Dalsgaard, A.E., et al.: A distributed fixed-point algorithm for extended dependency graphs. Fundam. Inform. 161(4), 351\u2013381 (2018). \n                    https:\/\/doi.org\/10.3233\/FI-2018-1707","journal-title":"Fundam. Inform."},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017, Part II. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"issue":"5","key":"20_CR8","doi-asserted-by":"publisher","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 reliability. Formal Asp. Comput. 6(5), 512\u2013535 (1994). \n                    https:\/\/doi.org\/10.1007\/BF01211866","journal-title":"Formal Asp. Comput."},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Types for Proofs and Programs","author":"L Helmink","year":"1994","unstructured":"Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127\u2013165. Springer, Heidelberg (1994). \n                    https:\/\/doi.org\/10.1007\/3-540-58085-9_75"},{"issue":"1","key":"20_CR10","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/0890-5401(90)90004-2","volume":"88","author":"A Itai","year":"1990","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60\u201387 (1990). \n                    https:\/\/doi.org\/10.1016\/0890-5401(90)90004-2","journal-title":"Inf. Comput."},{"issue":"4","key":"20_CR11","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/s10009-014-0359-5","volume":"18","author":"JF Jensen","year":"2016","unstructured":"Jensen, J.F., Larsen, K.G., Srba, J., Oestergaard, L.K.: Efficient model-checking of weighted CTL with upper-bound constraints. STTT 18(4), 409\u2013426 (2016). \n                    https:\/\/doi.org\/10.1007\/s10009-014-0359-5","journal-title":"STTT"},{"key":"20_CR12","doi-asserted-by":"publisher","unstructured":"Katoen, J., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005), Torino, Italy, 19\u201322 September 2005, pp. 243\u2013244 (2005). \n                    https:\/\/doi.org\/10.1109\/QEST.2005.2","DOI":"10.1109\/QEST.2005.2"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220\u2013270. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-72522-0_6"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012, London, United Kingdom, 17\u201320 September 2012, pp. 203\u2013204 (2012). \n                    https:\/\/doi.org\/10.1109\/QEST.2012.14","DOI":"10.1109\/QEST.2012.14"},{"issue":"1\u20132","key":"20_CR16","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1\u20132), 134\u2013152 (1997). \n                    https:\/\/doi.org\/10.1007\/s100090050010","journal-title":"STTT"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BFb0055040","volume-title":"Automata, Languages and Programming","author":"X Liu","year":"1998","unstructured":"Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 53\u201366. Springer, Heidelberg (1998). \n                    https:\/\/doi.org\/10.1007\/BFb0055040"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-319-65765-3_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Mariegaard","year":"2017","unstructured":"Mariegaard, A., Larsen, K.G.: Symbolic dependency graphs for \n                    \n                      \n                    \n                    $$\\text{ PCTL }^{>}_{\\le }$$\n                   model-checking. In: Abate, A., Geeraerts, G. (eds.) FORMATS 2017. LNCS, vol. 10419, pp. 153\u2013169. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-65765-3_9"},{"key":"20_CR19","doi-asserted-by":"publisher","unstructured":"Strehl, K., Thiele, L.: Symbolic model checking of process networks using interval diagram techniques. In: Proceedings of the 1998 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 1998, San Jose, CA, USA, 8\u201312 November 1998, pp. 686\u2013692 (1998). \n                    https:\/\/doi.org\/10.1145\/288548.289117","DOI":"10.1145\/288548.289117"},{"issue":"2","key":"20_CR20","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A., et al.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285\u2013309 (1955)","journal-title":"Pac. J. Math."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-20652-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:18:27Z","timestamp":1558984707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-20652-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030206512","9783030206529"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-20652-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 May 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 May 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/robonaut.jsc.nasa.gov\/R2\/pages\/nfm2019.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}