{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:59:04Z","timestamp":1762459144954},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397172"},{"type":"electronic","value":"9783642397189"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39718-9_13","type":"book-chapter","created":{"date-parts":[[2013,8,30]],"date-time":"2013-08-30T03:01:54Z","timestamp":1377831714000},"page":"213-230","source":"Crossref","is-referenced-by-count":4,"title":["On Refinements of Boolean and Parametric Modal Transition Systems"],"prefix":"10.1007","author":[{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_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":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR \u201998 Concurrency Theory","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 163\u2013178. Springer, Heidelberg (1998)"},{"key":"13_CR3","first-page":"94","volume":"95","author":"A. Antonik","year":"2008","unstructured":"Antonik, A., Huth, M., Guldstrand Larsen, K., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bulletin of the EATCS\u00a095, 94\u2013129 (2008)","journal-title":"Bulletin of the EATCS"},{"key":"13_CR4","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":"13_CR5","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.\u00a06996, pp. 228\u2013242. Springer, Heidelberg (2011)"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., Delahaye, B., Fahrenberg, U., K\u0159et\u00ednsk\u00fd, J., Legay, A.: Hennessy-milner logic with maximal fixed points as a specification theory (to appear in CONCUR 2013)","DOI":"10.1007\/978-3-642-40184-8_7"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-24372-1_20","volume-title":"Automated Technology for Verification and Analysis","author":"N. Bene\u0161","year":"2011","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Guldstrand Larsen, K., M\u00f8ller, M.H., Srba, J.: Parametric modal transition systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 275\u2013289. Springer, Heidelberg (2011)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-28717-6_12","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"N. Bene\u0161","year":"2012","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Guldstrand Larsen, K., M\u00f8ller, M.H., Srba, J.: Dual-priced modal transition systems with time durations. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 122\u2013137. Springer, Heidelberg (2012)"},{"issue":"41","key":"13_CR9","doi-asserted-by":"publisher","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., Guldstrand Larsen, K., Srba, J.: On determinism in modal transition systems. Theor. Comput. Sci.\u00a0410(41), 4026\u20134043 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR10","doi-asserted-by":"publisher","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., Guldstrand Larsen, K., Srba, J.: Exptime-completeness of thorough refinement on modal transition systems. Inf. Comput.\u00a0218, 54\u201368 (2012)","journal-title":"Inf. Comput."},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-52590-4_40","volume-title":"CAAP \u201990","author":"G. Boudol","year":"1990","unstructured":"Boudol, G., Guldstrand Larsen, K.: Graphical versus logical specifications. In: Arnold, A. (ed.) CAAP 1990. LNCS, vol.\u00a0431, pp. 57\u201371. Springer, Heidelberg (1990)"},{"issue":"3","key":"13_CR12","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BF01384499","volume":"6","author":"A. B\u00f8rjesson","year":"1995","unstructured":"B\u00f8rjesson, A., Larsen, K.G., Skou, A.: Generality in design and compositional verification using TAV. Formal Methods in System Design\u00a06(3), 239\u2013258 (1995)","journal-title":"Formal Methods in System Design"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-642-24372-1_30","volume-title":"Automated Technology for Verification and Analysis","author":"S.S. Bauer","year":"2011","unstructured":"Bauer, S.S., Mayer, P., Legay, A.: MIO workbench: A tool for compositional design with modal input\/output interfaces. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 418\u2013421. Springer, Heidelberg (2011)"},{"issue":"1-2","key":"13_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0167-6423(96)00027-5","volume":"29","author":"G. Bruns","year":"1997","unstructured":"Bruns, G.: An industrial application of modal process logic. Sci. Comput. Program.\u00a029(1-2), 3\u201322 (1997)","journal-title":"Sci. Comput. Program."},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-04761-9_22","volume-title":"Automated Technology for Verification and Analysis","author":"A. Campetelli","year":"2009","unstructured":"Campetelli, A., Gruler, A., Leucker, M., Thoma, D.: Don\u2019t know for multi-valued systems. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 289\u2013305. Springer, Heidelberg (2009)"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC\/SIGSOFT FSE, pp. 109\u2013120 (2001)","DOI":"10.1145\/503271.503226"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Fischbein, D., Foster, H., Uchitel, S.: MTSA: Eclipse support for modal transition systems construction, analysis and elaboration. In: ETX, pp. 6\u201310 (2007)","DOI":"10.1145\/1328279.1328281"},{"issue":"2","key":"13_CR18","doi-asserted-by":"publisher","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.\u00a019(2), 253\u2013291 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR19","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"},{"issue":"1-2","key":"13_CR20","doi-asserted-by":"publisher","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. Log. Algebr. Program.\u00a077(1-2), 20\u201339 (2008)","journal-title":"J. Log. Algebr. Program."},{"key":"13_CR21","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 - 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.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional must program analysis: unleashing the power of alternation. In: POPL, pp. 43\u201356 (2010)","DOI":"10.1145\/1707801.1706307"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming Languages and Systems","author":"M. Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 155\u2013169. Springer, Heidelberg (2001)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45314-8_21","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Jacobs","year":"2001","unstructured":"Jacobs, B., Poll, E.: A logic for the java modeling language JML. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 284\u2013299. Springer, Heidelberg (2001)"},{"key":"13_CR25","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":"13_CR26","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":"K. Guldstrand Larsen","year":"2007","unstructured":"Guldstrand Larsen, K., Nyman, U., W\u0105sowski, A.: Modal I\/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 64\u201379. Springer, Heidelberg (2007)"},{"key":"13_CR27","unstructured":"Guldstrand Larsen, K., Thomsen, B.: A modal process logic. In: LICS, pp. 203\u2013210 (1988)"},{"issue":"6","key":"13_CR28","doi-asserted-by":"publisher","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.\u00a016(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR29","unstructured":"Guldstrand Larsen, K., Xinxin, L.: Equation solving using modal transition systems. In: LICS, pp. 108\u2013117 (1990)"},{"key":"13_CR30","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 (1988)","DOI":"10.21236\/ADA196047"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-45069-6_29","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2003","unstructured":"Namjoshi, K.S.: Abstraction for branching time properties. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 288\u2013300. Springer, Heidelberg (2003)"},{"key":"13_CR32","unstructured":"Nyman, U.: Modal Transition Systems as the Basis for Interface Theories and Product Lines. PhD thesis, Aalborg Universitet (2008)"},{"key":"13_CR33","unstructured":"Raclet, J.-B.: Quotient de sp\u00e9cifications pour la r\u00e9utilisation de composants. PhD thesis, Universit\u00e9 de Rennes I (December 2007) (in French)"},{"key":"13_CR34","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. IEEE Computer Society Press (2009)","DOI":"10.1109\/ACSD.2009.22"},{"issue":"1-2","key":"13_CR35","doi-asserted-by":"crossref","first-page":"119","DOI":"10.3233\/FI-2011-416","volume":"108","author":"J.-B. Raclet","year":"2011","unstructured":"Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fundamenta Informaticae\u00a0108(1-2), 119\u2013149 (2011)","journal-title":"Fundamenta Informaticae"},{"key":"13_CR36","doi-asserted-by":"crossref","unstructured":"Uchitel, S., Chechik, M.: Merging partial behavioural models. In: SIGSOFT FSE, pp. 43\u201352 (2004)","DOI":"10.1145\/1041685.1029904"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2013"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39718-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T20:40:23Z","timestamp":1596400823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39718-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397172","9783642397189"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39718-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}