{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,23]],"date-time":"2025-05-23T05:08:07Z","timestamp":1747976887445,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662468227"},{"type":"electronic","value":"9783662468234"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-662-46823-4_25","type":"book-chapter","created":{"date-parts":[[2015,4,18]],"date-time":"2015-04-18T01:40:54Z","timestamp":1429321254000},"page":"304-319","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Model Checking Value-Passing Modal Specifications"],"prefix":"10.1007","author":[{"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[]},{"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[]},{"given":"Franco","family":"Mazzanti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,19]]},"reference":[{"key":"25_CR1","first-page":"94","volume":"95","author":"A Antonik","year":"2008","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., W\u0105sowski, A.: 20 Years of modal and mixed specifications. Bull. EATCS 95, 94\u2013129 (2008)","journal-title":"Bull. EATCS"},{"key":"25_CR2","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-94-010-0387-2_3","volume-title":"Handbook of Philosophical Logic","author":"L \u00c5qvist","year":"2002","unstructured":"\u00c5qvist, L.: Deontic logic. Handbook of Philosophical Logic, 2nd edn, pp. 147\u2013264. Kluwer, Dordrecht (2002)","edition":"2"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-16265-7_5","volume-title":"Integrated Formal Methods","author":"P Asirelli","year":"2010","unstructured":"Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A logical framework to deal with variability. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 43\u201358. Springer, Heidelberg (2010)"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: Formal description of variability in product families. In: SPLC 2011, pp. 130\u2013139. IEEE (2011)","DOI":"10.1109\/SPLC.2011.34"},{"issue":"2","key":"25_CR5","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"MH ter Beek","year":"2011","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state\/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119\u2013135 (2011)","journal-title":"Sci. Comput. Program."},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Gnesi, S., Mazzanti, F.: Demonstration of a model checker for the analysis of product variability. In: SPLC 2012, pp. 242\u2013245. ACM (2012)","DOI":"10.1145\/2364412.2364454"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Lluch Lafuente, A., Petrocchi, M.: Combining declarative and procedural views in the specification and analysis of product families. In: SPLC 2013, Vol. 2, pp. 10\u201317. ACM (2013)","DOI":"10.1145\/2499777.2500722"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-32759-9_36","volume-title":"FM 2012: Formal Methods","author":"MH ter Beek","year":"2012","unstructured":"ter Beek, M.H., Mazzanti, F., Sulova, A.: VMC: a tool for product variability analysis. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 450\u2013454. Springer, Heidelberg (2012)"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Mazzanti, F.: VMC: recent advances and challenges ahead. In: SPLC 2014, Vol. 2, pp. 70\u201377. ACM (2014)","DOI":"10.1145\/2647908.2655969"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., de Vink. E.P.: Using mCRL2 for the analysis of software product lines. In: FormaliSE 2014, IEEE (2014)","DOI":"10.1145\/2593489.2593493"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., de Vink, E.P.: Software product line analysis with mCRL2. In: SPLC 2014, vol. 2, pp. 78\u201385. ACM (2014)","DOI":"10.1145\/2647908.2655970"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/978-3-662-45234-9_26","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"MH ter Beek","year":"2014","unstructured":"ter Beek, M.H., de Vink, E.P.: Towards modular verification of software product lines with mCRL2. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 368\u2013385. Springer, Heidelberg (2014)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-24372-1_17","volume-title":"Automated Technology for Verification and Analysis","author":"N Bene\u0161","year":"2011","unstructured":"Bene\u0161, N., \u010cern\u00e1, I., K\u0159et\u00ednsk\u00fd, J.: Modal transition systems: composition and LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 228\u2013242. Springer, Heidelberg (2011)"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-44618-4_14","volume-title":"CONCUR 2000 - Concurrency Theory","author":"G Bruns","year":"2000","unstructured":"Bruns, G., Godefroid, P.: Generalized model checking: reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168\u2013182. Springer, Heidelberg (2000)"},{"issue":"2","key":"25_CR15","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications. ACM TOPLAS 8(2), 244\u2013263 (1986)","journal-title":"ACM TOPLAS"},{"issue":"8","key":"25_CR16","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. IEEE TSE 39(8), 1069\u20131089 (2013)","journal-title":"IEEE TSE"},{"issue":"4","key":"25_CR17","doi-asserted-by":"publisher","first-page":"41","DOI":"10.5038\/2375-0901.12.4.3","volume":"12","author":"P DeMaio","year":"2009","unstructured":"DeMaio, P.: Bike-sharing: history, impacts, models of provision, and future. J. Public Transp. 12(4), 41\u201356 (2009)","journal-title":"J. Public Transp."},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Semantics of Systems of Concurrent Processes","author":"R De Nicola","year":"1990","unstructured":"De Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407\u2013419. Springer, Heidelberg (1990)"},{"issue":"2","key":"25_CR19","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R De Nicola","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458\u2013487 (1995)","journal-title":"J. ACM"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S.: MTSA: the modal transition system analyser. In: ASE 2008, pp. 475\u2013476. IEEE (2008)","DOI":"10.1109\/ASE.2008.78"},{"issue":"3","key":"25_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2211616.2211619","volume":"21","author":"A Fantechi","year":"2012","unstructured":"Fantechi, A., Lapadula, A., Pugliese, R., Tiezzi, F., Gnesi, S., Mazzanti, F.: A logical verification methodology for service-oriented computing. ACM TOSEM 21(3), 1\u201346 (2012). Article 16","journal-title":"ACM TOSEM"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Fischbein, D., Uchitel, S., Braberman, V.A.: A foundation for behavioural conformance in software product line architectures. In: ROSATEA 2006, pp. 39\u201348. ACM (2006)","DOI":"10.1145\/1147249.1147254"},{"key":"25_CR23","unstructured":"Fricker, C., Gast, N.: Incentives and redistribution in homogeneous bike-sharing systems with stations of finite capacity. EURO J. Transp. Logistics, 1\u201331 (2014)"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Gnesi, S., Petrocchi, M.: Towards an executable algebra for product lines. In: SPLC 2012, Vol. 2, pp. 66\u201373. ACM (2012)","DOI":"10.1145\/2364412.2364424"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49253-4_8","volume-title":"Algebraic Methodology and Software Technology","author":"JF Groote","year":"1998","unstructured":"Groote, J.F., Mateescu, R.: Verification of temporal properties of processes in a setting with data. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 74\u201390. Springer, Heidelberg (1998)"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Krka, I., Edwards, G., Brun, Y., Medvidovic, N.: From system specifications to component behavioral models. In: ICSE 2009, pp. 315\u2013318. IEEE (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071010"},{"issue":"2\u20133","key":"25_CR27","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"KG Larsen","year":"1990","unstructured":"Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoret. Comput. Sci. 72(2\u20133), 265\u2013288 (1990)","journal-title":"Theoret. Comput. Sci."},{"key":"25_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-71316-6_6","volume-title":"Programming Languages and Systems","author":"KG Larsen","year":"2007","unstructured":"Larsen, K.G., Nyman, U., W\u0105sowski, A.: Modal I\/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64\u201379. Springer, Heidelberg (2007)"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS 1988, pp. 203\u2013210. IEEE (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Lauenroth, K., Pohl, K., T\u00f6hning, S.: Model checking of domain artifacts in product line engineering. In: ASE 2009, pp. 269\u2013280. IEEE (2009)","DOI":"10.1109\/ASE.2009.16"},{"key":"25_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/978-3-642-34026-0_11","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"M Leucker","year":"2012","unstructured":"Leucker, M., Thoma, D.: A formal approach to software product families. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 131\u2013145. Springer, Heidelberg (2012)"},{"issue":"6","key":"25_CR32","doi-asserted-by":"publisher","first-page":"1542","DOI":"10.1016\/j.ins.2007.10.023","volume":"178","author":"R Meolic","year":"2008","unstructured":"Meolic, R., Kapus, T., Brezocnik, Z.: ACTLW: an action-based computation tree logic with unless operator. Inf. Sci. 178(6), 1542\u20131557 (2008)","journal-title":"Inf. Sci."},{"key":"25_CR33","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall (1989)"},{"key":"25_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28901-1","volume-title":"Software Product Line Engineering: Foundations, Principles, and Techniques","author":"K Pohl","year":"2005","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer, Heidelberg (2005)"},{"key":"25_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-642-32759-9_33","volume-title":"FM 2012: Formal Methods","author":"GE Sibay","year":"2012","unstructured":"Sibay, G.E., Uchitel, S., Braberman, V., Kramer, J.: Distribution of modal transition systems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 403\u2013417. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46823-4_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T18:24:12Z","timestamp":1747938252000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-46823-4_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662468227","9783662468234"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46823-4_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}