{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T07:29:47Z","timestamp":1742974187647,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030763831"},{"type":"electronic","value":"9783030763848"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-76384-8_12","type":"book-chapter","created":{"date-parts":[[2021,5,18]],"date-time":"2021-05-18T23:50:53Z","timestamp":1621381853000},"page":"180-197","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Scalable Reliability Analysis by Lazy Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5549-7809","authenticated-orcid":false,"given":"Shahid","family":"Khan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3810-4185","authenticated-orcid":false,"given":"Matthias","family":"Volk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5500-2949","authenticated-orcid":false,"given":"Marc","family":"Bouissou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,5,19]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-030-01090-4_19","volume-title":"Automated Technology for Verification and Analysis","author":"P Ashok","year":"2018","unstructured":"Ashok, P., Butkova, Y., Hermanns, H., K\u0159et\u00ednsk\u00fd, J.: Continuous-time Markov decisions based on partial exploration. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 317\u2013334. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_19"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of Model Checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"issue":"4","key":"12_CR3","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1017\/S0960129512000254","volume":"23","author":"C Baier","year":"2013","unstructured":"Baier, C., Hahn, E.M., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model checking for performability. Math. Struct. Comput. Sci. 23(4), 751\u2013795 (2013)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"6","key":"12_CR4","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 Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"12_CR6","unstructured":"Bouissou, M.: A generalization of dynamic fault trees through Boolean logic driven markov processes (BDMP). In: Proceedings of the 16th European Safety and Reliability Conference (ESREL) (2007)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Bouissou, M.: A simple yet efficient acceleration technique for Monte Carlo simulation. In: Proceedings of the 22nd European Safety and Reliability Conference (ESREL), pp. 27\u201336 (2013)","DOI":"10.1201\/b15938-207"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Bouissou, M.: A benchmark on reliability of complex discrete systems: emergency power supply of a nuclear power plant. arXiv:1703.06575 (2017)","DOI":"10.4204\/EPTCS.244.8"},{"issue":"2","key":"12_CR9","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0951-8320(03)00143-1","volume":"82","author":"M Bouissou","year":"2003","unstructured":"Bouissou, M., Bon, J.L.: A new formalism that combines advantages of fault-trees and Markov models: Boolean logic Driven Markov Processes. Rel. Eng. Sys. Safety 82(2), 149\u2013163 (2003)","journal-title":"Rel. Eng. Sys. Safety"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Bouissou, M., Hernu, O.: Boolean approximation for calculating the reliability of a very large repairable system with dependencies among components. In: Proceedings of the 25th European Safety and Reliability Conference (ESREL) (2016)","DOI":"10.1201\/9781315374987-230"},{"key":"12_CR11","unstructured":"Bouissou, M., Hernu, O.: Estimation de la fiabilite d\u2019un systeme industriel. French Patent FR3044787A1, June 2017. https:\/\/worldwide.espacenet.com\/patent\/search\/family\/056321980\/publication\/FR3044787A1?q=FR3044787"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Bouissou, M., Khan, S., Katoen, J., Krc\u00e1l, P.: Various ways to quantify BDMPs. In: MARS@ETAPS. EPTCS, vol. 316, pp. 1\u201314 (2020)","DOI":"10.4204\/EPTCS.316.1"},{"issue":"5","key":"12_CR13","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M Bozzano","year":"2011","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. Comput. J. 54(5), 754\u2013775 (2011)","journal-title":"Comput. J."},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"12_CR15","unstructured":"Collet, J., Bruy\u00e8re, F.: An efficient tool for taking repairs into account in Boolean Models. In: Probabilistic Safety Assessment and Management, vol. 4 (1998)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Distefano, S., Puliafito, A.: Dynamic reliability block diagrams vs dynamic fault trees. In: Annual Reliability and Maintainability Symposium (RAMS), pp. 71\u201376. IEEE (2007)","DOI":"10.1109\/RAMS.2007.328095"},{"issue":"3","key":"12_CR17","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1109\/24.159800","volume":"41","author":"JB Dugan","year":"1992","unstructured":"Dugan, J.B., Bavuso, S.J., Boyd, M.A.: Dynamic fault-tree models for fault-tolerant computer systems. IEEE Trans. Rel. 41(3), 363\u2013377 (1992)","journal-title":"IEEE Trans. Rel."},{"issue":"4","key":"12_CR18","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1016\/j.ress.2008.09.007","volume":"94","author":"K Durga Rao","year":"2009","unstructured":"Durga Rao, K., Gopika, V., Sanyasi Rao, V., Kushwaha, H., Verma, A., Srividya, A.: Dynamic fault tree analysis using Monte Carlo simulation in probabilistic safety assessment. Reliab. Eng. Syst. Saf. 94(4), 872\u2013883 (2009)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.ress.2019.02.005","volume":"186","author":"M Ghadhab","year":"2019","unstructured":"Ghadhab, M., Junges, S., Katoen, J.P., Kuntz, M., Volk, M.: Safety analysis for vehicle guidance systems with dynamic fault trees. Reliab. Eng. Syst. Saf. 186, 37\u201350 (2019)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"12_CR20","unstructured":"Guck, D., Katoen, J.P., Stoelinga, M.I., Luiten, T., Romijn, J.: Smart railroad maintenance engineering with stochastic model checking. In: Proceedings of Railways, pp. 950\u2013953. Saxe-Coburg Publications (2014)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-030-17502-3_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2019","unstructured":"Hahn, E.M., et al.: The 2019 comparison of tools for the analysis of quantitative formal models. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 69\u201392. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_5"},{"key":"12_CR22","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm. CoRR abs\/2002.07080 (2020). https:\/\/arxiv.org\/abs\/2002.07080"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Junges, S., Guck, D., Katoen, J.P., Stoelinga, M.: Uncovering dynamic fault trees. In: DSN, pp. 299\u2013310. IEEE Computer Society (2016)","DOI":"10.1109\/DSN.2016.35"},{"issue":"11","key":"12_CR24","doi-asserted-by":"publisher","first-page":"1521","DOI":"10.1016\/j.ress.2006.10.010","volume":"92","author":"B Kaiser","year":"2007","unstructured":"Kaiser, B., Gramlich, C., F\u00f6rster, M.: State\/event fault trees - a safety analysis model for software-controlled systems. Reliab. Eng. Syst. Saf. 92(11), 1521\u20131537 (2007)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: LICS, pp. 31\u201345. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934574","DOI":"10.1145\/2933575.2934574"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-030-54549-9_6","volume-title":"Computer Safety, Reliability, and Security","author":"S Khan","year":"2020","unstructured":"Khan, S., Katoen, J.-P., Bouissou, M.: A compositional semantics for repairable BDMPs. In: Casimiro, A., Ortmeier, F., Bitsch, F., Ferreira, P. (eds.) SAFECOMP 2020. LNCS, vol. 12234, pp. 82\u201398. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-54549-9_6"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Khan, S., Katoen, J.P., Bouissou, M.: Explaining Boolean-logic driven Markov processes using GSPNs. In: EDCC, pp. 119\u2013126. IEEE (2020)","DOI":"10.1109\/EDCC51268.2020.00028"},{"key":"12_CR28","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). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"12_CR29","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1109\/TII.2017.2710316","volume":"14","author":"M Volk","year":"2018","unstructured":"Volk, M., Junges, S., Katoen, J.P.: Fast dynamic fault tree analysis by model checking techniques. IEEE Trans. Ind. Inf. 14(1), 370\u2013379 (2018)","journal-title":"IEEE Trans. Ind. Inf."},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-030-27008-7_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"M Volk","year":"2019","unstructured":"Volk, M., Weik, N., Katoen, J.-P., Nie\u00dfen, N.: A DFT modeling approach for infrastructure reliability analysis of railway station areas. In: Larsen, K.G., Willemse, T. (eds.) FMICS 2019. LNCS, vol. 11687, pp. 40\u201358. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-27008-7_3"},{"key":"12_CR31","unstructured":"Walker, M.D.: Pandora: a logic for the qualitative analysis of temporal fault trees. Ph.D. dissertation, University of Hull, Kingston upon Hull, UK (2009)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-76384-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,18]],"date-time":"2021-05-18T23:55:19Z","timestamp":1621382119000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-76384-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030763831","9783030763848"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-76384-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 May 2021","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 May 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"66","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}