{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:40:52Z","timestamp":1767984052327,"version":"3.49.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107930","type":"print"},{"value":"9783032107947","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-10794-7_5","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:18Z","timestamp":1763188998000},"page":"81-98","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["CTL Model Checking Partially Specified Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-5680-5509","authenticated-orcid":false,"given":"Eshita","family":"Zaman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7671-2720","authenticated-orcid":false,"given":"Christopher","family":"Johannsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7737-6888","authenticated-orcid":false,"given":"Andrew S.","family":"Miner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4906-6145","authenticated-orcid":false,"given":"Gianfranco","family":"Ciardo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2430-6827","authenticated-orcid":false,"given":"Samik","family":"Basu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Ben-David, S., Sterin, B., Atlee, J.M., Beidu, S.: Symbolic model checking of product-line requirements using sat-based methods. In: 2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering, vol.\u00a01, pp. 189\u2013199. IEEE (2015)","DOI":"10.1109\/ICSE.2015.40"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/11431855_34","volume-title":"Advanced Information Systems Engineering","author":"D Benavides","year":"2005","unstructured":"Benavides, D., Trinidad, P., Ruiz-Cort\u00e9s, A.: Automated reasoning on feature models. In: Pastor, O., Falc\u00e3o e Cunha, J. (eds.) CAiSE 2005. LNCS, vol. 3520, pp. 491\u2013503. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11431855_34"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Proceedings of the 11th International Conference on Computer Aided Verification, pp. 274\u2013287. CAV 1999, Springer-Verlag, London, UK (1999). http:\/\/dl.acm.org\/citation.cfm?id=647768.733795","DOI":"10.1007\/3-540-48683-6_25"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Bruns, G., Godefroid, P.: Generalized model checking: Reasoning about partial state spaces. In: Concurrency Theory, pp. 168\u2013182. CONCUR, Springer-Verlag, Heidelberg (2000). http:\/\/dl.acm.org\/citation.cfm?id=646735.701611","DOI":"10.1007\/3-540-44618-4_14"},{"key":"5_CR5","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-27836-8_26","volume-title":"Automata, Languages and Programming","author":"G Bruns","year":"2004","unstructured":"Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) Automata, Languages and Programming, pp. 281\u2013293. Springer, Berlin Heidelberg, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27836-8_26"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking 12(4) (2003). https:\/\/doi.org\/10.1145\/990010.990011","DOI":"10.1145\/990010.990011"},{"issue":"4","key":"5_CR7","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1530873.1530885","volume":"36","author":"G Ciardo","year":"2009","unstructured":"Ciardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the stochastic model checking analyzer for reliability and timing. ACM SIGMETRICS Perf. Eval. Rev. 36(4), 58\u201363 (2009)","journal-title":"ACM SIGMETRICS Perf. Eval. Rev."},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Procedings IBM Workshop on Logics of Programs, pp. 52\u201371. LNCS 131, Springer (1981). https:\/\/doi.org\/10.1007\/bfb0025774","DOI":"10.1007\/bfb0025774"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. In: Proceedings of the 33rd International Conference on Software Engineering, pp. 321\u2013330 (2011)","DOI":"10.1145\/1985793.1985838"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Dureja, R., Rozier, K.Y.: FuseIC3: an algorithm for checking large design spaces. In: 2017 Formal Methods in Computer Aided Design (FMCAD), pp. 164\u2013171. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102255"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-319-89960-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Dureja","year":"2018","unstructured":"Dureja, R., Rozier, K.Y.: More scalable LTL model checking via discovering design-space dependencies ($$D^{3}$$). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 309\u2013327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_17"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Famelis, M., Salay, R., Chechik, M.: Partial models: towards modeling and reasoning with uncertainty. In: 2012 34th International Conference on Software Engineering (ICSE), pp. 573\u2013583 (2012). https:\/\/doi.org\/10.1109\/ICSE.2012.6227159","DOI":"10.1109\/ICSE.2012.6227159"},{"key":"5_CR14","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. LNCS, vol. 9780, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_1"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 \u2014 Concurrency Theory","author":"P Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-Based Model Checking Using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426\u2013440. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44685-0_29"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-68863-1_8","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"A Gruler","year":"2008","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) Formal Methods for Open Object-Based Distributed Systems, pp. 113\u2013131. Springer, Berlin Heidelberg, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68863-1_8"},{"key":"5_CR17","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley (2003)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: a foundation for three-valued program analysis. In: European Symposium on Programming Languages and Systems, pp. 155\u2013169. ESOP 2001, Springer-Verlag, London, UK, UK (2001). http:\/\/dl.acm.org\/citation.cfm?id=645395.651926","DOI":"10.1007\/3-540-45309-1_11"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-21292-5_3","volume-title":"Foundations of Computer Software. Modeling, Development, and Verification of Adaptive Systems","author":"E Kang","year":"2011","unstructured":"Kang, E., Jackson, E., Schulte, W.: An approach for effective design space exploration. In: Calinescu, R., Jackson, E. (eds.) Monterey Workshop 2010. LNCS, vol. 6662, pp. 33\u201354. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21292-5_3"},{"key":"5_CR20","unstructured":"Kleene, S.C.: Introduction to Metamathematics. North Holland (1987)"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation: Modelling Techniques and Tools","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200\u2013204. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46029-2_13"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Nyman, U., Wasowski, A.: On Modal refinement and consistency. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 105\u2013119. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_8","DOI":"10.1007\/978-3-540-74407-8_8"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Manolios, P., Vroon, D., Subramanian, G.: Automating component-based system assembly. In: Proceedings of the 2007 International Symposium on Software Testing and Analysis, pp. 61\u201372 (2007)","DOI":"10.1145\/1273463.1273473"},{"issue":"4","key":"5_CR24","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013579 (1989)","journal-title":"Proc. IEEE"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-45212-6_19","volume-title":"Embedded Software","author":"S Neema","year":"2003","unstructured":"Neema, S., Sztipanovits, J., Karsai, G., Butts, K.: Constraint-based design-space exploration and model synthesis. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 290\u2013305. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45212-6_19"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-74128-2_8","volume-title":"Model Checking and Artificial Intelligence","author":"C Pecheur","year":"2007","unstructured":"Pecheur, C., Raimondi, F.: Symbolic model checking of logics with actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt 2006. LNCS (LNAI), vol. 4428, pp. 113\u2013128. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74128-2_8"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10794-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:59:19Z","timestamp":1767967159000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2025.ens.psl.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}