{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:16:25Z","timestamp":1743023785990,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030613617"},{"type":"electronic","value":"9783030613624"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-61362-4_13","type":"book-chapter","created":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T13:02:36Z","timestamp":1603890156000},"page":"240-261","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Components in Probabilistic Systems: Suitable by Construction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5321-9343","authenticated-orcid":false,"given":"Christel","family":"Baier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5718-8276","authenticated-orcid":false,"given":"Clemens","family":"Dubslaff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2766-9615","authenticated-orcid":false,"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6353-227X","authenticated-orcid":false,"given":"Michaela","family":"Klauck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1724-2586","authenticated-orcid":false,"given":"Sascha","family":"Kl\u00fcppelholz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2551-2814","authenticated-orcid":false,"given":"Maximilian A.","family":"K\u00f6hl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,29]]},"reference":[{"key":"13_CR1","unstructured":"Test-ablauf - So testet die Stiftung Warentest. https:\/\/www.test.de\/unternehmen\/testablauf-5017344-0\/ . Accessed 30 June 2020"},{"key":"13_CR2","unstructured":"The Official Site of The European New Car Assessment Programme. https:\/\/www.euroncap.com\/en\/ . Accessed 30 June 2020"},{"key":"13_CR3","volume-title":"Principles of Cyber-Physical Systems","author":"R Alur","year":"2015","unstructured":"Alur, R.: Principles of Cyber-Physical Systems. The MIT Press, Cambridge (2015)"},{"key":"13_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37521-7","volume-title":"Feature-Oriented Software Product Lines: Concepts and Implementation","author":"S Apel","year":"2013","unstructured":"Apel, S., Batory, D., K\u00e4stner, C., Saake, G.: Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37521-7"},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"49","DOI":"10.5381\/jot.2009.8.5.c5","volume":"8","author":"S Apel","year":"2009","unstructured":"Apel, S., K\u00e4stner, C.: An overview of feature-oriented software development. J. Object Technol. 8, 49\u201384 (2009)","journal-title":"J. Object Technol."},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Baier, C., Dubslaff, C., Hermanns, H., Klauck, M., Kl\u00fcppelholz, S., K\u00f6hl, M.A.: Tooling, Data and Results for \u201cComponents in Probabilistic Systems: Suitable by Construction\u201d (2020). https:\/\/doi.org\/10.5281\/zenodo.3970766","DOI":"10.5281\/zenodo.3970766"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Baier, C., Dubslaff, C., Kl\u00fcppelholz, S.: Trade-off analysis meets probabilistic model checking. In: Proceedings of the 23rd Conference on Computer Science Logic and the 29th Symposium on Logic in Computer Science (CSL-LICS), pp. 1:1\u20131:10. ACM (2014)","DOI":"10.1145\/2603088.2603089"},{"issue":"1","key":"13_CR8","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.1145\/2108242.2108243","volume":"59","author":"C Baier","year":"2012","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Bertrand, N.: Probabilistic $$\\omega $$-automata. J. ACM 59(1), 1:1\u20131:52 (2012)","journal-title":"J. ACM"},{"issue":"1\u20132","key":"13_CR9","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/0004-3702(94)00011-O","volume":"72","author":"AG Barto","year":"1995","unstructured":"Barto, A.G., Bradtke, S.J., Singh, S.P.: Learning to act using real-time dynamic programming. Artif. Intell. 72(1\u20132), 81\u2013138 (1995)","journal-title":"Artif. Intell."},{"key":"13_CR10","unstructured":"Bonet, B., Geffner, H.: Labeled RTDP: improving the convergence of real-time dynamic programming. In: ICAPS, pp. 12\u201321 (2003)"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.jcss.2017.09.007","volume":"94","author":"R Canetti","year":"2018","unstructured":"Canetti, R., et al.: Task-structured probabilistic I\/O automata. J. Comput. Syst. Sci. 94, 63\u201397 (2018). https:\/\/doi.org\/10.1016\/j.jcss.2017.09.007","journal-title":"J. Comput. Syst. Sci."},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.: Markov decision processes with multiple objectives. In: STACS, February 2006. http:\/\/chess.eecs.berkeley.edu\/pubs\/81.html","DOI":"10.1007\/11672142_26"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-40313-2_25","volume-title":"Mathematical Foundations of Computer Science 2013","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 266\u2013277. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40313-2_25"},{"issue":"1\u20132","key":"13_CR14","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.tcs.2006.07.033","volume":"365","author":"L Cheung","year":"2006","unstructured":"Cheung, L., Lynch, N.A., Segala, R., Vaandrager, F.W.: Switched PIOA: parallel composition via distributed scheduling. Theor. Comput. Sci. 365(1\u20132), 83\u2013108 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.07.033","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"13_CR15","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s00165-017-0432-4","volume":"30","author":"P Chrszon","year":"2018","unstructured":"Chrszon, P., Dubslaff, C., Kl\u00fcppelholz, S., Baier, C.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Aspects Comput. 30(1), 45\u201375 (2018). https:\/\/doi.org\/10.1007\/s00165-017-0432-4","journal-title":"Formal Aspects Comput."},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of ICSE 2010, pp. 335\u2013344. ACM (2010)","DOI":"10.1145\/1806799.1806850"},{"key":"13_CR17","volume-title":"Generative Programming: Methods, Tools, and Applications","author":"K Czarnecki","year":"2000","unstructured":"Czarnecki, K., Eisenecker, U.W.: Generative Programming: Methods, Tools, and Applications. ACM Press\/Addison-Wesley Publishing Co., New York (2000)"},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-662-46734-3_5","volume":"12","author":"C Dubslaff","year":"2015","unstructured":"Dubslaff, C., Baier, C., Kl\u00fcppelholz, S.: Probabilistic model checking for feature-oriented systems. Trans. Aspect-Oriented Softw. Dev. 12, 180\u2013220 (2015). https:\/\/doi.org\/10.1007\/978-3-662-46734-3_5","journal-title":"Trans. Aspect-Oriented Softw. Dev."},{"issue":"4","key":"13_CR19","first-page":"1","volume":"4","author":"K Etessami","year":"2008","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4(4), 1\u201321 (2008)","journal-title":"Log. Methods Comput. Sci."},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"V Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 317\u2013332. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_25"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112\u2013127. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11"},{"key":"13_CR22","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1038\/scientificamerican1273-118","volume":"229","author":"M Gardner","year":"1973","unstructured":"Gardner, M.: Mathematical games. Sci. Am. 229, 118\u2013121 (1973)","journal-title":"Sci. Am."},{"key":"13_CR23","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1016\/j.tcs.2013.07.017","volume":"538","author":"S Giro","year":"2014","unstructured":"Giro, S., D\u2019Argenio, P.R., Fioriti, L.M.F.: Distributed probabilistic input\/output automata: expressiveness, (un)decidability and algorithms. Theor. Comput. Sci. 538, 84\u2013102 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2013.07.017 . Quantitative Aspects of Programming Languages and Systems (2011\u201312)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"13_CR24","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1006\/inco.1995.1123","volume":"121","author":"RJ van Glabbeek","year":"1995","unstructured":"van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121(1), 59\u201380 (1995). https:\/\/doi.org\/10.1006\/inco.1995.1123","journal-title":"Inf. Comput."},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-030-50086-3_6","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"TP Gros","year":"2020","unstructured":"Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Steinmetz, M.: Deep statistical model checking. In: Gotsman, A., Sokolova, A. (eds.) FORTE 2020. LNCS, vol. 12136, pp. 96\u2013114. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50086-3_6"},{"issue":"8","key":"13_CR26","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978). https:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun. ACM"},{"issue":"2","key":"13_CR27","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10009-017-0456-3","volume":"20","author":"J Klein","year":"2017","unstructured":"Klein, J., et al.: Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic B\u00fcchi automata. Int. J. Softw. Tools Technol. Transf. 20(2), 179\u2013194 (2017). https:\/\/doi.org\/10.1007\/s10009-017-0456-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-030-03769-7_17","volume-title":"Runtime Verification","author":"MA K\u00f6hl","year":"2018","unstructured":"K\u00f6hl, M.A., Hermanns, H., Biewer, S.: Efficient monitoring of real driving emissions. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 299\u2013315. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_17"},{"key":"13_CR29","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"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Lee, E.A.: Cyber physical systems: design challenges. In: 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC), pp. 363\u2013369 (2008)","DOI":"10.1109\/ISORC.2008.25"},{"issue":"1","key":"13_CR31","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/BF02055574","volume":"28","author":"WS Lovejoy","year":"1991","unstructured":"Lovejoy, W.S.: A survey of algorithmic methods for partially observable Markov decision processes. Ann. Oper. Res. 28(1), 47\u201365 (1991)","journal-title":"Ann. Oper. Res."},{"issue":"3","key":"13_CR32","first-page":"219","volume":"2","author":"N Lynch","year":"1989","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. CWI Q. 2(3), 219\u2013246 (1989)","journal-title":"CWI Q."},{"issue":"1\u20132","key":"13_CR33","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0004-3702(02)00378-8","volume":"147","author":"O Madani","year":"2003","unstructured":"Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell. 147(1\u20132), 5\u201334 (2003)","journal-title":"Artif. Intell."},{"key":"13_CR34","series-title":"PHI Series in Computer Science","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)"},{"issue":"3","key":"13_CR35","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1287\/moor.12.3.441","volume":"12","author":"C Papadimitriou","year":"1987","unstructured":"Papadimitriou, C., Tsitsiklis, J.: The complexity of Markov decision processes. Math. Oper. Res. 12(3), 441\u2013450 (1987)","journal-title":"Math. Oper. Res."},{"key":"13_CR36","doi-asserted-by":"crossref","unstructured":"Pineda, L.E., Zilberstein, S.: Planning under uncertainty using reduced models: revisiting determinization. In: ICAPS (2014)","DOI":"10.1609\/icaps.v24i1.13636"},{"key":"13_CR37","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M Puterman","year":"1994","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)"},{"key":"13_CR38","unstructured":"Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology (1995)"},{"issue":"1s","key":"13_CR39","first-page":"6:1","volume":"47","author":"T Th\u00fcm","year":"2014","unstructured":"Th\u00fcm, T., Apel, S., K\u00e4stner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1s), 6:1\u20136:45 (2014)","journal-title":"ACM Comput. Surv."},{"issue":"1\u20132","key":"13_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00056-X","volume":"176","author":"S Wu","year":"1997","unstructured":"Wu, S., Smolka, S.A., Stark, E.W.: Composition and behaviors of probabilistic I\/O automata. Theor. Comput. Sci. 176(1\u20132), 1\u201338 (1997). https:\/\/doi.org\/10.1016\/S0304-3975(97)00056-X","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61362-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,25]],"date-time":"2022-11-25T04:42:33Z","timestamp":1669351353000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61362-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030613617","9783030613624"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61362-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"29 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}