{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:41:02Z","timestamp":1725928862126},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319723075"},{"type":"electronic","value":"9783319723082"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-72308-2_10","type":"book-chapter","created":{"date-parts":[[2017,12,14]],"date-time":"2017-12-14T13:25:15Z","timestamp":1513257915000},"page":"152-169","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Memory-Efficient Tactics for Randomized LTL Model Checking"],"prefix":"10.1007","author":[{"given":"Kim","family":"Larsen","sequence":"first","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]},{"given":"Sean","family":"Sedwards","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,15]]},"reference":[{"issue":"3","key":"10_CR1","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"11","author":"J Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. J. Algorithms 11(3), 441\u2013461 (1990)","journal-title":"J. Algorithms"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-44804-7_7","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"L Brim","year":"2001","unstructured":"Brim, L., \u010cern\u00e1, I., Ne\u010desal, M.: Randomization helps in LTL model checking. In: de Alfaro, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 105\u2013119. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44804-7_7"},{"key":"10_CR3","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing and Verification XV, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, pp. 3\u201318 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Grosu, R., Smolka, S.: Monte Carlo model checking. In: 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, pp. 271\u2013286 (2005)","DOI":"10.1007\/978-3-540-31980-1_18"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73\u201384. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_8"},{"key":"10_CR7","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., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441\u2013444. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_29"},{"key":"10_CR8","volume-title":"The SPIN Model Checker","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Pearson Education, Boston (2003)"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Lehmann, D.J., Rabin, M.O.: On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In: Conference Record of the Eighth Annual ACM Symposium on Principles of Programming Languages, Williamsburg, Virginia, USA, January 1981, pp. 133\u2013138 (1981)","DOI":"10.1145\/567532.567547"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: How to cook a temporal proof system for your pet language. In: Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983, pp. 141\u2013154 (1983)","DOI":"10.1145\/567067.567082"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Oudinet, J., Denise, A., Gaudel, M., Lassaigne, R., Peyronnet, S.: Uniform Monte-Carlo model checking. In: 14th International Conference on Fundamental Approaches to Software Engineering, FASE 2011, pp. 127\u2013140 (2011)","DOI":"10.1007\/978-3-642-19811-3_10"},{"issue":"2","key":"10_CR12","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"WJ Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177\u2013192 (1970)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"10_CR13","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"10_CR14","first-page":"133","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics","author":"W Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133\u2013192. MIT Press, Cambridge (1990)"},{"key":"10_CR15","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of IEEE Symposium on Logic in Computer Science, Boston, July 1986, pp. 332\u2013344 (1986)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223\u2013235. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_17"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72308-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,7]],"date-time":"2019-10-07T21:30:29Z","timestamp":1570483829000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72308-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319723075","9783319723082"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72308-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}