{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,17]],"date-time":"2026-09-17T03:11:37Z","timestamp":1789614697571,"version":"build-2803163510"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2015,3,19]],"date-time":"2015-03-19T00:00:00Z","timestamp":1426723200000},"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":["Acta Informatica"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s00236-015-0215-4","type":"journal-article","created":{"date-parts":[[2015,3,18]],"date-time":"2015-03-18T18:07:07Z","timestamp":1426702027000},"page":"269-297","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Refinement checking on parametric modal transition systems"],"prefix":"10.1007","volume":"52","author":[{"given":"Nikola","family":"Bene\u0161","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mikael H.","family":"M\u00f8ller","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ji\u0159\u00ed","family":"Srba","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,3,19]]},"reference":[{"key":"215_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., F\u00e1bregas, I., de Frutos-Escrig, D., Ing\u00f3lfsd\u00f3ttir, A., Palomino, M.: Graphical representation of covariant-contravariant modal formulae. In: EXPRESS, pp. 1\u201315 (2011)","DOI":"10.4204\/EPTCS.64.1"},{"key":"215_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: CONCUR, pp. 163\u2013178 (1998)","DOI":"10.1007\/BFb0055622"},{"key":"215_CR3","first-page":"94","volume":"95","author":"A Antonik","year":"2008","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bull. EATCS 95, 94\u2013129 (2008)","journal-title":"Bull. EATCS"},{"key":"215_CR4","doi-asserted-by":"crossref","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: Complexity of decision problems for mixed and modal specifications. In: Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FOSSACS\u201908), LNCS, vol. 4962, pp. 112\u2013126 (2008)","DOI":"10.1007\/978-3-540-78499-9_9"},{"key":"215_CR5","doi-asserted-by":"crossref","unstructured":"Balcazar, J.L., Gabarr\u00f3, J., Santha, M.: Deciding bisimilarity is P-complete. Form. Asp. Comput. 4(6 A), 638\u2013648 (1992)","DOI":"10.1007\/BF03180566"},{"key":"215_CR6","doi-asserted-by":"crossref","unstructured":"Bauer, S.S., Fahrenberg, U., Juhl, L., Larsen, K.G., Legay, A., Thrane, C.R.: Quantitative refinement for weighted modal transition systems. In: MFCS, LNCS, vol. 6907, pp. 60\u201371. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22993-0_9"},{"key":"215_CR7","unstructured":"Bene\u0161, N., \u010cern\u00e1, I., K\u0159et\u00ednsk\u00fd, J.: Disjunctive Modal Transition Systems and Generalized LTL Model Checking. Technical report FIMU-RS-2010-12, Faculty of Informatics, Masaryk University, Brno (2010)"},{"key":"215_CR8","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., Delahaye, B., Fahrenberg, U., K\u0159et\u00ednsk\u00fd, J., Legay, A.: Hennessy\u2013Milner logic with greatest fixed points as a complete behavioural specification theory. In: D\u2019Argenio, P.R., Melgratti, H.C. (eds.) CONCUR, Lecture Notes in Computer Science, vol. 8052, pp. 76\u201390. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-40184-8_7"},{"key":"215_CR9","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., M\u00f8ller, M.H., Srba, J.: Parametric Modal Transition Systems. Technical report FIMU-RS-2011-03, Faculty of Informatics, Masaryk University, Brno (2011)","DOI":"10.1007\/978-3-642-24372-1_20"},{"key":"215_CR10","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1016\/j.ic.2012.08.001","volume":"218","author":"N Bene\u0161","year":"2012","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., Srba, J.: EXPTIME-completeness of thorough refinement on modal transition systems. Inf. Comput. 218, 54\u201368 (2012)","journal-title":"Inf. Comput."},{"key":"215_CR11","first-page":"9","volume-title":"MEMICS, OASICS","author":"N Bene\u0161","year":"2010","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J.: Process algebra for modal transition systemses. In: Matyska, L., Kozubek, M., Vojnar, T., Zemc\u00edk, P., Antos, D. (eds.) MEMICS, OASICS, vol. 16, pp. 9\u201318. Schloss Dagstuh\u2014Leibniz-Zentrum fuer Informatik, Germany (2010)"},{"key":"215_CR12","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1016\/j.ic.2012.08.001","volume":"218","author":"N Bene\u0161","year":"2012","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K., Srba, J.: EXPTIME-completeness of thorough refinement on modal transition systems. Inf. Comput. 218, 54\u201368 (2012)","journal-title":"Inf. Comput."},{"key":"215_CR13","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., M\u00f8ller, M.H., Srba, J.: Parametric modal transition systems. In: ATVA, pp. 275\u2013289 (2011)","DOI":"10.1007\/978-3-642-24372-1_20"},{"key":"215_CR14","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., M\u00f8ller, M.H., Srba, J.: Dual-priced modal transition systems with time durations. In: LPAR, pp. 122\u2013137 (2012)","DOI":"10.1007\/978-3-642-28717-6_12"},{"key":"215_CR15","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., Srba, J.: Checking thorough refinement on modal transition systems is EXPTIME-complete. In: Proceedings of the Theoretical Aspects of Computing\u2014ICTAC 2009, 6th International Colloquium, LNCS, vol. 5684. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03466-4_7"},{"issue":"41","key":"215_CR16","doi-asserted-by":"crossref","first-page":"4026","DOI":"10.1016\/j.tcs.2009.06.009","volume":"410","author":"N Bene\u0161","year":"2009","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., Srba, J.: On determinism in modal transition systems. Theor. Comput. Sci. 410(41), 4026\u20134043 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"215_CR17","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., \u010cern\u00e1, I., K\u0159et\u00ednsk\u00fd, J.: Modal transition systems: Composition and LTL model checking. In: ATVA, pp. 228\u2013242 (2011)","DOI":"10.1007\/978-3-642-24372-1_17"},{"issue":"12","key":"215_CR18","doi-asserted-by":"crossref","first-page":"1212","DOI":"10.1016\/j.scico.2011.01.007","volume":"77","author":"N Bertrand","year":"2012","unstructured":"Bertrand, N., Legay, A., Pinchinat, S., Raclet, J.B.: Modal event-clock specifications for timed component-based design. Sci. Comput. Program. 77(12), 1212\u20131234 (2012). doi: 10.1016\/j.scico.2011.01.007","journal-title":"Sci. Comput. Program."},{"key":"215_CR19","doi-asserted-by":"crossref","unstructured":"Boudol, G., Larsen, K.G.: Graphical versus logical specifications. In: CAAP, pp. 57\u201371 (1990)","DOI":"10.1007\/3-540-52590-4_40"},{"issue":"1","key":"215_CR20","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(92)90276-L","volume":"106","author":"G Boudol","year":"1992","unstructured":"Boudol, G., Larsen, K.G.: Graphical versus logical specifications. Theor. Comput. Sci. 106(1), 3\u201320 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"215_CR21","doi-asserted-by":"crossref","unstructured":"Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Compositional design methodology with constraint markov chains. In: QEST, pp. 123\u2013132 (2010)","DOI":"10.1109\/QEST.2010.23"},{"key":"215_CR22","doi-asserted-by":"crossref","unstructured":"Campetelli, A., Gruler, A., Leucker, M., Thoma, D.: Don\u2019t Know for multi-valued systems. In: ATVA, pp. 289\u2013305 (2009)","DOI":"10.1007\/978-3-642-04761-9_22"},{"key":"215_CR23","doi-asserted-by":"crossref","unstructured":"\u010cer\u0101ns, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification\u2014theory and tools. In: CAV, pp. 253\u2013267 (1993)","DOI":"10.1007\/3-540-56922-7_21"},{"key":"215_CR24","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC\/SIGSOFT FSE, pp. 109\u2013120 (2001)","DOI":"10.1145\/503225.503226"},{"issue":"2","key":"215_CR25","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19(2), 253\u2013291 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"215_CR26","doi-asserted-by":"crossref","unstructured":"Dams, D., Namjoshi, K.S.: The existence of finite abstractions for branching time model checking. In: LICS, pp. 335\u2013344 (2004)","DOI":"10.1109\/LICS.2004.1319628"},{"key":"215_CR27","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: ECDAR: An environment for compositional design and analysis of real time systems. In: ATVA, pp. 365\u2013370 (2010)","DOI":"10.1007\/978-3-642-15643-4_29"},{"issue":"1\u20132","key":"215_CR28","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1016\/j.jlap.2008.05.003","volume":"77","author":"H Fecher","year":"2008","unstructured":"Fecher, H., Schmidt, H.: Comparing disjunctive modal transition systems with an one-selecting variant. J. Logic Algebr. Program. 77(1\u20132), 20\u201339 (2008)","journal-title":"J. Logic Algebr. Program."},{"issue":"2","key":"215_CR29","first-page":"103","volume":"128","author":"H Fecher","year":"2005","unstructured":"Fecher, H., Steffen, M.: Characteristic mu-calculus formulas for underspecified transition systems. ENTCS 128(2), 103\u2013116 (2005)","journal-title":"ENTCS"},{"key":"215_CR30","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Proceedings of the CONCUR\u201901, LNCS, vol. 2154, pp. 426\u2013440. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44685-0_29"},{"key":"215_CR31","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: POPL, pp. 43\u201356 (2010)","DOI":"10.1145\/1706299.1706307"},{"key":"215_CR32","doi-asserted-by":"crossref","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.D.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS, Lecture Notes in Computer Science, vol. 5051, pp. 113\u2013131. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-68863-1_8"},{"key":"215_CR33","doi-asserted-by":"crossref","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: a foundation for three-valued program analysis. In: Proceedings of the ESOP\u201901, LNCS, vol. 2028, pp. 155\u2013169. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45309-1_11"},{"key":"215_CR34","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Poll, E.: A logic for the java modeling language JML. In: FASE, pp. 284\u2013299 (2001)","DOI":"10.1007\/3-540-45314-8_21"},{"issue":"4","key":"215_CR35","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1016\/j.jlap.2012.03.008","volume":"81","author":"L Juhl","year":"2012","unstructured":"Juhl, L., Larsen, K.G., Srba, J.: Modal transition systems with weight intervals. J. Log. Algebr. Program. 81(4), 408\u2013421 (2012)","journal-title":"J. Log. Algebr. Program."},{"key":"215_CR36","unstructured":"K\u0159et\u00ednsk\u00fd, J., Sickert, S.: MoTraS: A tool for modal transition systems and their extensions. In: Hung, D.V., Ogawa, M. (eds.) ATVA, Lecture Notes in Computer Science, vol. 8172, pp. 487\u2013491. Springer, Berlin (2013). Tool accessible at https:\/\/www7.in.tum.de\/kretinsk\/motras.html"},{"key":"215_CR37","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u00fd, J., Sickert, S.: On refinements of Boolean and parametric modal transition systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC, Lecture Notes in Computer Science, vol. 8049, pp. 213\u2013230. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39718-9_13"},{"key":"215_CR38","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u00fd, J., Sickert, S.: On refinements of Boolean and parametric modal transition systems. CoRR abs\/1304.5278 (2013)","DOI":"10.1007\/978-3-642-39718-9_13"},{"key":"215_CR39","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Nyman, U., Wasowski, A.: Modal I\/O automata for interface and product line theories. In: ESOP, pp. 64\u201379 (2007)","DOI":"10.1007\/978-3-540-71316-6_6"},{"key":"215_CR40","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Nyman, U., Wasowski, A.: On modal refinement and consistency. In: Proceedings of the CONCUR\u201907, LNCS, vol. 4703, pp. 105\u2013119. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-74407-8_8"},{"key":"215_CR41","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203\u2013210. IEEE Computer Society (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"215_CR42","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: LICS, pp. 108\u2013117. IEEE Computer Society (1990)","DOI":"10.1109\/LICS.1990.113738"},{"issue":"6","key":"215_CR43","doi-asserted-by":"crossref","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"215_CR44","doi-asserted-by":"crossref","unstructured":"L\u00fcttgen, G., Vogler, W.: Modal interface automata. Log. Methods Comput. Sci. 9(3) (2013). doi: 10.2168\/LMCS-9(3:4)2013","DOI":"10.2168\/LMCS-9(3:4)2013"},{"key":"215_CR45","doi-asserted-by":"crossref","unstructured":"Lynch, N.: I\/O automata: A model for discrete event systems. In: 22nd Annual Conference on Information Sciences and Systems, pp. 29\u201338. Princeton University, Princeton (1988)","DOI":"10.21236\/ADA196047"},{"key":"215_CR46","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S.: Abstraction for branching time properties. In: CAV, pp. 288\u2013300 (2003)","DOI":"10.1007\/978-3-540-45069-6_29"},{"key":"215_CR47","doi-asserted-by":"crossref","unstructured":"Nanz, S., Nielson, F., Nielson, H.R.: Modal abstractions of concurrent behaviour. In: Proceeding of the SAS\u201908, LNCS, vol. 5079, pp. 159\u2013173. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-69166-2_11"},{"key":"215_CR48","volume-title":"Computational Complexity","author":"CH Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"215_CR49","unstructured":"Raclet, J.B.: Quotient de Sp\u00e9cifications pour la R\u00e9utilisation de Composants. Ph.D. thesis, Universit\u00e9 de Rennes I (2007); (in French)"},{"key":"215_CR50","doi-asserted-by":"crossref","unstructured":"Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fundamenta Informaticae 108(1\u20132), 119\u2013149 (2011)","DOI":"10.3233\/FI-2011-416"},{"key":"215_CR51","doi-asserted-by":"crossref","unstructured":"Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Passerone, R.: Why are modalities good for interface theories? In: ACSD, pp. 119\u2013127. IEEE (2009)","DOI":"10.1109\/ACSD.2009.22"},{"issue":"5","key":"215_CR52","first-page":"513","volume":"24","author":"Z Sawa","year":"2005","unstructured":"Sawa, Z., Jan\u010dar, P.: Behavioural equivalences on finite-state systems are PTIME-hard. Comput. Inf. 24(5), 513\u2013528 (2005)","journal-title":"Comput. Inf."},{"key":"215_CR53","doi-asserted-by":"crossref","unstructured":"Uchitel, S., Chechik, M.: Merging partial behavioural models. In: Proceedings of the FSE\u201904, pp. 43\u201352. ACM (2004)","DOI":"10.1145\/1029894.1029904"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0215-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-015-0215-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0215-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T02:37:31Z","timestamp":1747795051000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-015-0215-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,19]]},"references-count":53,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["215"],"URL":"https:\/\/doi.org\/10.1007\/s00236-015-0215-4","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,19]]}}}