{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:05Z","timestamp":1776333425738,"version":"3.51.2"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319899596","type":"print"},{"value":"9783319899602","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89960-2_17","type":"book-chapter","created":{"date-parts":[[2018,4,11]],"date-time":"2018-04-11T10:14:43Z","timestamp":1523441683000},"page":"309-327","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["More Scalable LTL Model Checking via Discovering Design-Space Dependencies ( $$D^{3}$$ D 3 )"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7152-8115","authenticated-orcid":false,"given":"Rohit","family":"Dureja","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,12]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54804-8_1","volume-title":"Fundamental Approaches to Software Engineering","author":"C Baier","year":"2014","unstructured":"Baier, C., Dubslaff, C., Kl\u00fcppelholz, S., Daum, M., Klein, J., M\u00e4rcker, S., Wunderlich, S.: Probabilistic model checking and non-standard multi-objective reasoning. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 1\u201316. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-642-54804-8_1"},{"issue":"4","key":"17_CR2","doi-asserted-by":"publisher","first-page":"1023","DOI":"10.2514\/1.26311","volume":"30","author":"C Bauer","year":"2007","unstructured":"Bauer, C., Lagadec, K., B\u00e8s, C., Mongeau, M.: Flight control system architecture optimization for fly-by-wire airliners. J. Guidance, Control Dyn. 30(4), 1023\u20131029 (2007)","journal-title":"J. Guidance, Control Dyn."},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-319-21690-4_36","volume-title":"Computer Aided Verification","author":"M Bozzano","year":"2015","unstructured":"Bozzano, M., Cimatti, A., Fernandes Pires, A., Jones, D., Kimberly, G., Petri, T., Robinson, R., Tonetta, S.: Formal design and safety analysis of AIR6110 wheel brake system. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 518\u2013535. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21690-4_36"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., Garcia, L., Murciano, M., Nocco, S., Quer, S.: Speeding up model checking by exploiting explicit and hidden verification constraints. In: DATE (2009)","DOI":"10.1109\/DATE.2009.5090934"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P.E., Loiacono, C., Palena, M., Pasini, P., Patti, D., Quer, S.: To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking. Int. J. Softw. Tools Technol. Transfer (2017). \n                      https:\/\/doi.org\/10.1007\/s10009-017-0451-8","DOI":"10.1007\/s10009-017-0451-8"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Nocco, S.: Optimized model checking of multiple properties. In: DATE (2011)","DOI":"10.1109\/DATE.2011.5763279"},{"issue":"3","key":"17_CR7","first-page":"382","volume":"29","author":"G Cabodi","year":"2010","unstructured":"Cabodi, G., Garcia, L.A., Murciano, M., Nocco, S., Quer, S.: Partitioning interpolant-based verification for effective unbounded model checking. TCAD 29(3), 382\u2013395 (2010)","journal-title":"TCAD"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Parameter synthesis with IC3. In: FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679406"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: A tool for checking the refinement of temporal contracts. In: ASE (2013)","DOI":"10.1109\/ASE.2013.6693137"},{"issue":"5","key":"17_CR11","first-page":"589","volume":"14","author":"A Classen","year":"2012","unstructured":"Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y.: Model checking software product lines with SNIP. JSTTT 14(5), 589\u2013612 (2012)","journal-title":"JSTTT"},{"issue":"8","key":"17_CR12","first-page":"1069","volume":"39","author":"A Classen","year":"2013","unstructured":"Classen, A., Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A., Raskin, J.F.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. TSE 39(8), 1069\u20131089 (2013)","journal-title":"TSE"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. In: ICSE (2011)","DOI":"10.1145\/1985793.1985838"},{"key":"17_CR14","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: ICSE (2010)","DOI":"10.1145\/1806799.1806850"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., \u00c1brah\u00e1m, E.: PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21690-4_13"},{"key":"17_CR16","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.P., \u00c1brah\u00e1m, E.: Parameter synthesis for probabilistic systems. In: MBMV (2016)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-319-23404-5_18","volume-title":"Model Checking Software","author":"AS Dimovski","year":"2015","unstructured":"Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., W\u0105sowski, A.: Family-based model checking without a family-based model checker. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 282\u2013299. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-23404-5_18"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Dureja, R., Rozier, K.Y.: FuseIC3: an algorithm for checking large design spaces. In: FMCAD (2017)","DOI":"10.23919\/FMCAD.2017.8102255"},{"key":"17_CR19","unstructured":"Dureja, R., Rozier, K.Y.: More Scalable LTL Model Checking via Discovering Design-Space Dependencies (Artifact) (2018). \n                      https:\/\/doi.org\/10.6084\/m9.figshare.5913013.v1"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"EA Emerson","year":"2000","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 236\u2013254. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/10721959_19"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-71209-1_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Etessami","year":"2007","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of markov decision processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 50\u201365. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-71209-1_6"},{"key":"17_CR22","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., 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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41540-6_1","volume-title":"Computer Aided Verification","author":"M Gario","year":"2016","unstructured":"Gario, M., Cimatti, A., Mattarei, C., Tonetta, S., Rozier, K.Y.: Model checking at scale: automated air traffic control design space exploration. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part II. LNCS, vol. 9780, pp. 3\u201322. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-41540-6_1"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-20398-5_12","volume-title":"NASA Formal Methods","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 146\u2013161. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-20398-5_12"},{"issue":"3","key":"17_CR25","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/j.scico.2014.04.005","volume":"96","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: On modelling and verifying railway interlockings: tracking train lengths. Sci. Comput. Program. 96(3), 315\u2013336 (2014)","journal-title":"Sci. Comput. Program."},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-34188-5_9","volume-title":"Hardware and Software: Verification and Testing","author":"Z Khasidashvili","year":"2012","unstructured":"Khasidashvili, Z., Nadel, A.: Implicative simultaneous satisfiability and applications. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 66\u201379. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-34188-5_9"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/11678779_5","volume-title":"Hardware and Software, Verification and Testing","author":"Z Khasidashvili","year":"2006","unstructured":"Khasidashvili, Z., Nadel, A., Palti, A., Hanna, Z.: Simultaneous SAT-based model checking of safety properties. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) HVC 2005. LNCS, vol. 3875, pp. 56\u201375. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11678779_5"},{"key":"17_CR28","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.ic.2013.10.001","volume":"232","author":"M Kwiatkowska","year":"2013","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38\u201365 (2013)","journal-title":"Inf. Comput."},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Mattarei, C., Cimatti, A., Gario, M., Tonetta, S., Rozier, K.Y.: Comparing different functional allocations in automated air traffic control design. In: FMCAD (2015)","DOI":"10.1109\/FMCAD.2015.7542260"},{"key":"17_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-39611-3_20","volume-title":"Hardware and Software: Verification and Testing","author":"F Moller","year":"2013","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and model checking abstractions of complex railway models using CSP\n                      \n                        \n                      \n                      $$||$$\n                      \n                        \n                          \n                            |\n                            |\n                          \n                        \n                      \n                    B. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 193\u2013208. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39611-3_20"},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-46520-3_4","volume-title":"Automated Technology for Verification and Analysis","author":"T Quatmann","year":"2016","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50\u201367. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-46520-3_4"},{"key":"17_CR32","first-page":"123","volume":"10","author":"M Rosenm\u00fcller","year":"2010","unstructured":"Rosenm\u00fcller, M., Siegmund, N.: Automating the configuration of multi software product lines. VaMoS 10, 123\u2013130 (2010)","journal-title":"VaMoS"},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"KY Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149\u2013167. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-73370-6_11"},{"key":"17_CR34","unstructured":"Schirmeier, H., Spinczyk, O.: Challenges in software product line composition. In: HICSS. IEEE (2009)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89960-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T03:14:53Z","timestamp":1583205293000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89960-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899596","9783319899602"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89960-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"12 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","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":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}