{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:55:26Z","timestamp":1725900926648},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642380877"},{"type":"electronic","value":"9783642380884"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38088-4_21","type":"book-chapter","created":{"date-parts":[[2013,5,8]],"date-time":"2013-05-08T20:38:27Z","timestamp":1368045507000},"page":"307-321","source":"Crossref","is-referenced-by-count":6,"title":["A Probabilistic Quantitative Analysis of Probabilistic-Write\/Copy-Select"],"prefix":"10.1007","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Engel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sascha","family":"Kl\u00fcppelholz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steffen","family":"M\u00e4rcker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hendrik","family":"Tews","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcus","family":"V\u00f6lp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"21_CR1","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Model checking continuous-time Markov chains. ACM Transactions on Computational Logic\u00a01(1), 162\u2013170 (2000)","journal-title":"ACM Transactions on Computational Logic"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Baier, C., Daum, M., Engel, B., H\u00e4rtig, H., Klein, J., Kl\u00fcppelholz, S., M\u00e4rcker, S., Tews, H., V\u00f6lp, M.: Chiefly symmetric: Results on the scalability of probabilistic model checking for operating-system code. In: SSV 2012. EPTCS, vol.\u00a0102, pp. 156\u2013166 (2012)","DOI":"10.4204\/EPTCS.102.14"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-32469-7_4","volume-title":"Formal Methods for Industrial Critical Systems","author":"C. Baier","year":"2012","unstructured":"Baier, C., Daum, M., Engel, B., H\u00e4rtig, H., Klein, J., Kl\u00fcppelholz, S., M\u00e4rcker, S., Tews, H., V\u00f6lp, M.: Waiting for locks: How long does it usually take? In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol.\u00a07437, pp. 47\u201362. Springer, Heidelberg (2012)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1007\/3-540-45022-X_65","volume-title":"Automata, Languages and Programming","author":"C. Baier","year":"2000","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the logical characterisation of performability properties. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 780\u2013792. Springer, Heidelberg (2000)"},{"issue":"6","key":"21_CR5","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-16561-0_18","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"N. Coste","year":"2010","unstructured":"Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten years of performance evaluation for concurrent systems using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol.\u00a06416, pp. 128\u2013142. Springer, Heidelberg (2010)"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Gafni, E., Mitzenmacher, M.: Analysis of timing-based mutual exclusion with random times. In: 18th Annual ACM Symposium on Principles of Distributed Computing (PODC), pp. 13\u201321. ACM (1999)","DOI":"10.1145\/301308.301318"},{"key":"21_CR8","unstructured":"Mc Guire, N.: Probabilistic write copy select. In: 13th Real-Time Linux Workshop, pp. 195\u2013206 (October 2011)"},{"issue":"2","key":"21_CR9","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","volume":"6","author":"M.Z. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. STTT\u00a06(2), 128\u2013142 (2004)","journal-title":"STTT"},{"issue":"4","key":"21_CR10","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/1059816.1059820","volume":"32","author":"M.Z. Kwiatkowska","year":"2005","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic model checking in practice: case studies with prism. SIGMETRICS Performance Evaluation Review\u00a032(4), 16\u201321 (2005)","journal-title":"SIGMETRICS Performance Evaluation Review"},{"issue":"4","key":"21_CR11","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1530873.1530882","volume":"36","author":"M.Z. Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: probabilistic model checking for performance and reliability analysis. SIGMETRICS Performance Evaluation Review\u00a036(4), 40\u201345 (2009)","journal-title":"SIGMETRICS Performance Evaluation Review"},{"key":"21_CR12","unstructured":"Kemeny, J., Snell, J.: Finite Markov Chains. D. Van Nostrand (1960)"},{"key":"21_CR13","unstructured":"Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman & Hall (1995)"},{"issue":"2","key":"21_CR14","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J.-P. Katoen","year":"2011","unstructured":"Katoen, J.-P., Zapreev, I.S., Moritz Hahn, E., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Performance Evaluation\u00a068(2), 90\u2013104 (2011)","journal-title":"Performance Evaluation"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Mellor-Crummey, J., Scott, M.: Scalable reader-writer synchronization for shared-memory multiprocessors. In: PPOPP 1991, pp. 106\u2013113. ACM (April 1991)","DOI":"10.1145\/109626.109637"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-15898-8_12","volume-title":"Formal Methods for Industrial Critical Systems","author":"R. Mateescu","year":"2010","unstructured":"Mateescu, R., Serwe, W.: A study of shared-memory mutual exclusion protocols using CADP. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol.\u00a06371, pp. 180\u2013197. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38088-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T19:36:20Z","timestamp":1557689780000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38088-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642380877","9783642380884"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38088-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}