{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:04:55Z","timestamp":1762459495276},"publisher-location":"Cham","reference-count":176,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319631202"},{"type":"electronic","value":"9783319631219"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63121-9_3","type":"book-chapter","created":{"date-parts":[[2017,7,24]],"date-time":"2017-07-24T08:05:15Z","timestamp":1500883515000},"page":"36-74","source":"Crossref","is-referenced-by-count":8,"title":["30 Years of Modal Transition Systems: Survey of Extensions and Analysis"],"prefix":"10.1007","author":[{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,25]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-642-29320-7_18","volume-title":"Fundamentals of Software Engineering","author":"L Aceto","year":"2012","unstructured":"Aceto, L., F\u00e1bregas, I., Frutos Escrig, D., Ing\u00f3lfsd\u00f3ttir, A., Palomino, M.: Relating modal refinements, covariant-contravariant simulations and partial bisimulations. In: Arbab, F., Sirjani, M. (eds.) FSEN 2011. LNCS, vol. 7141, pp. 268\u2013283. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-29320-7_18"},{"key":"3_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., Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163\u2013178. Springer, Heidelberg (1998). doi: 10.1007\/BFb0055622"},{"key":"3_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":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-540-78499-9_9","volume-title":"Foundations of Software Science and Computational Structures","author":"A Antonik","year":"2008","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., W\u0105sowski, A.: Complexity of decision problems for mixed and modal specifications. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 112\u2013126. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78499-9_9"},{"issue":"1","key":"3_CR5","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/j.entcs.2009.06.011","volume":"242","author":"A Antonik","year":"2009","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: EXPTIME-complete decision problems for modal and mixed specifications. Electron. Notes Theor. Comput. Sci. 242(1), 19\u201333 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"3_CR6","unstructured":"Alrajeh, D., Kramer, J., Russo, A., Uchitel, S.: An inductive approach for modal transition system refinement. In: Gallagher, J.P., Gelfond, M. (eds) ICLP (Technical Communications). LIPIcs, vol. 11, pp. 106\u2013116. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)"},{"key":"3_CR7","unstructured":"Bauer, S.S:. Modal specification theories for component-based design. Ph.D. thesis, Ludwig Maximilians University Munich (2012)"},{"key":"3_CR8","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":"3_CR9","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). doi: 10.1007\/978-3-642-24372-1_17"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11813040_8","volume-title":"FM 2006: Formal Methods","author":"G Brunet","year":"2006","unstructured":"Brunet, G., Chechik, M., Uchitel, S.: Properties of behavioural model merging. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 98\u2013114. Springer, Heidelberg (2006). doi: 10.1007\/11813040_8"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-319-46520-3_19","volume-title":"Automated Technology for Verification and Analysis","author":"S Ben-David","year":"2016","unstructured":"Ben-David, S., Chechik, M., Uchitel, S.: Observational refinement and merge for disjunctive MTSs. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 287\u2013303. Springer, Cham (2016). doi: 10.1007\/978-3-319-46520-3_19"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-40184-8_8","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"S Ben-David","year":"2013","unstructured":"Ben-David, S., Chechik, M., Uchitel, S.: Merging partial behaviour models with different vocabularies. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 91\u2013105. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40184-8_8"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-40184-8_7","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"N Bene\u0161","year":"2013","unstructured":"Bene\u0161, N., Delahaye, B., Fahrenberg, U., K\u0159et\u00ednsk\u00fd, J., Legay, A.: Hennessy-milner logic with greatest fixed points as a complete behavioural specification theory. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 76\u201390. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40184-8_7"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-28872-2_3","volume-title":"Fundamental Approaches to Software Engineering","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., David, A., Hennicker, R., Guldstrand Larsen, K., Legay, A., Nyman, U., W\u0105sowski, A.: Moving from specifications to contracts in component-based design. In: Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 43\u201358. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28872-2_3"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., Daca, P., Henzinger, T.A., K\u0159et\u00ednsk\u00fd, J., Nickovic, D.: Complete composition operators for IOCO-testing theory. In: Kruchten, P., Becker, S., Schneider, J.-G. (eds.) Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering, CBSE 2015, Montreal, QC, Canada, 4\u20138 May 2015, pp. 101\u2013110. ACM (2015)","DOI":"10.1145\/2737166.2737175"},{"key":"3_CR16","unstructured":"Benveniste, A.: Multiple viewpoint contracts and residuation. In: 2nd International Workshop on Foundations of Interface Technologies (FIT) (2008)"},{"key":"3_CR17","unstructured":"Bene\u0161, N.: Disjunctive modal transition systems. Ph.D. thesis, Masaryk University (2012)"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-22993-0_9","volume-title":"Mathematical Foundations of Computer Science 2011","author":"SS Bauer","year":"2011","unstructured":"Bauer, S.S., Fahrenberg, U., Juhl, L., Larsen, K.G., Legay, A., Thrane, C.: Quantitative refinement for weighted modal transition systems. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 60\u201371. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22993-0_9"},{"issue":"2","key":"3_CR19","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s10703-012-0178-9","volume":"42","author":"SS Bauer","year":"2013","unstructured":"Bauer, S.S., Fahrenberg, U., Juhl, L., Larsen, K.G., Legay, A., Thrane, C.R.: Weighted modal transition systems. Formal Methods Syst. Des. 42(2), 193\u2013220 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-85778-5_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P Bouyer","year":"2008","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33\u201347. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-85778-5_4"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-30642-6_3","volume-title":"Computer Science \u2013 Theory and Applications","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., Fahrenberg, U., Legay, A., Thrane, C.: General quantitative specification theories with modalities. In: Hirsch, E.A., Karhum\u00e4ki, J., Lepist\u00f6, A., Prilutskii, M. (eds.) CSR 2012. LNCS, vol. 7353, pp. 18\u201330. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-30642-6_3"},{"key":"3_CR22","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1016\/j.tcs.2016.06.011","volume":"642","author":"F Bujtor","year":"2016","unstructured":"Bujtor, F., Fendrich, S., L\u00fcttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theor. Comput. Sci. 642, 24\u201353 (2016)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274\u2013287. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48683-6_25"},{"key":"3_CR24","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 \u2014 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). doi: 10.1007\/3-540-44618-4_14"},{"issue":"6A","key":"3_CR25","doi-asserted-by":"crossref","first-page":"638","DOI":"10.1007\/BF03180566","volume":"4","author":"JL Balc\u00e1zar","year":"1992","unstructured":"Balc\u00e1zar, J.L., Gabarr\u00f3, J., Santha, M.: Deciding bisimilarity is p-complete. Formal Asp. Comput. 4(6A), 638\u2013648 (1992)","journal-title":"Formal Asp. Comput."},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24372-1","volume-title":"Automated Technology for Verification and Analysis","year":"2011","unstructured":"Bultan, T., Hsiung, P.-A. (eds.): ATVA 2011. LNCS, vol. 6996. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24372-1"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-19829-8_6","volume-title":"Formal Methods: Foundations and Applications","author":"SS Bauer","year":"2011","unstructured":"Bauer, S.S., Hennicker, R., Bidoit, M.: A modal interface theory with data constraints. In: Davies, J., Silva, L., Simao, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 80\u201395. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19829-8_6"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Bauer, B.B., Hennicker, R., Janisch, S.: Interface theories for (a)synchronously communicating modal I\/O-transition systems. In: Legay, A., Caillaud, B. (eds.) FIT. EPTCS, vol. 46, pp. 1\u20138 (2010)","DOI":"10.4204\/EPTCS.46.1"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-28412-0_1","volume-title":"Recent Trends in Algebraic Development Techniques","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., Hennicker, R., Wirsing, M.: Building a modal interface theory for concurrency and data. In: Mossakowski, T., Kreowski, H.-J. (eds.) WADT 2010. LNCS, vol. 7137, pp. 1\u201312. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28412-0_1"},{"issue":"4","key":"3_CR30","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1017\/S0960129511000697","volume":"22","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., Juhl, L., Larsen, K.G., Legay, A., Srba, J.: Extending modal transition systems with structured labels. Math. Struct. Comput. Sci. 22(4), 581\u2013617 (2012)","journal-title":"Math. Struct. Comput. Sci."},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Bauer, S.S., Juhl, L., Larsen, K.G., Srba, J., Legay, A.: A logic for accumulated-weight reasoning on multiweighted modal automata. In: Margaria, T., Qiu, Z., Yang, H. (eds.) TASE, pp. 77\u201384. IEEE (2012)","DOI":"10.1109\/TASE.2012.9"},{"key":"3_CR32","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J.: Process algebra for modal transition systemses. In: Matyska, L., Kozubek, M., Vojnar, T., Zemcik, P., Antos, D. (eds.) MEMICS. OASICS, vol. 16, pp. 9\u201318. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (2010)"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J.: Modal process rewrite systems. In: Roychoudhury, A., D\u2019Souza, M. (eds.) [RD12], pp. 120\u2013135","DOI":"10.1007\/978-3-642-32943-2_9"},{"key":"3_CR34","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., Larsen, K.G., M\u00f8ller, M.H., Srba, J.: Parametric modal transition systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 275\u2013289. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24372-1_20"},{"key":"3_CR35","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 2012. LNCS, vol. 7180, pp. 122\u2013137. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28717-6_12"},{"issue":"2\u20133","key":"3_CR36","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/s00236-015-0215-4","volume":"52","author":"N Bene\u0161","year":"2015","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., M\u00f8ller, M.H., Sickert, S., Srba, J.: Refinement checking on parametric modal transition systems. Acta Inf. 52(2\u20133), 269\u2013297 (2015)","journal-title":"Acta Inf."},{"key":"3_CR37","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: Leucker, M., Morgan, C. (eds.) [LM09], pp. 112\u2013126","DOI":"10.1007\/978-3-642-03466-4_7"},{"issue":"41","key":"3_CR38","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":"3_CR39","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."},{"issue":"1","key":"3_CR40","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":"3_CR41","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1016\/j.scico.2013.06.003","volume":"83","author":"SS Bauer","year":"2014","unstructured":"Bauer, S.S., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: A modal specification theory for components with data. Sci. Comput. Program. 83, 106\u2013128 (2014)","journal-title":"Sci. Comput. Program."},{"key":"3_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1007\/978-3-642-10373-5_35","volume-title":"Formal Methods and Software Engineering","author":"N Bertrand","year":"2009","unstructured":"Bertrand, N., Legay, A., Pinchinat, S., Raclet, J.-B.: A compositional approach on modal specifications for timed systems. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 679\u2013697. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-10373-5_35"},{"issue":"12","key":"3_CR43","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)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"3_CR44","doi-asserted-by":"crossref","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 Syst. Des. 6(3), 239\u2013258 (1995)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR45","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":"SS 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. 6996, pp. 418\u2013421. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24372-1_30"},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-642-12002-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SS Bauer","year":"2010","unstructured":"Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175\u2013189. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-12002-2_15"},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-00982-2_13","volume-title":"Language and Automata Theory and Applications","author":"N Bertrand","year":"2009","unstructured":"Bertrand, N., Pinchinat, S., Raclet, J.-B.: Refinement and consistency of timed modal specifications. In: Dediu, A.H., Ionescu, A.M., Mart\u00edn-Vide, C. (eds.) LATA 2009. LNCS, vol. 5457, pp. 152\u2013163. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-00982-2_13"},{"issue":"1\u20132","key":"3_CR48","doi-asserted-by":"crossref","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. 29(1\u20132), 3\u201322 (1997)","journal-title":"Sci. Comput. Program."},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Bujtor, F., Sorokin, L., Vogler, W.: Testing preorders for DMTS: deadlock- and the new deadlock\/divergence-testing. In: 15th International Conference on Application of Concurrency to System Design, ACSD 2015, Brussels, Belgium, 21\u201326 June 2015, pp. 60\u201369. IEEE Computer Society (2015)","DOI":"10.1109\/ACSD.2015.21"},{"issue":"4","key":"3_CR50","doi-asserted-by":"crossref","first-page":"67:1","DOI":"10.1145\/2746336","volume":"14","author":"F Bujtor","year":"2015","unstructured":"Bujtor, F., Vogler, W.: Failure semantics for modal transition systems. ACM Trans. Embed. Comput. Syst. 14(4), 67:1\u201367:30 (2015)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"3_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1007\/978-3-642-14162-1_50","volume-title":"Automata, Languages and Programming","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L.: Energy parity games. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 599\u2013610. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14162-1_50"},{"key":"3_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-540-45212-6_9","volume-title":"Embedded Software","author":"A Chakrabarti","year":"2003","unstructured":"Chakrabarti, A., Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 117\u2013133. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45212-6_9"},{"issue":"4","key":"3_CR53","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/990010.990011","volume":"12","author":"M Chechik","year":"2003","unstructured":"Chechik, M., Devereux, B., Easterbrook, S.M., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12(4), 371\u2013408 (2003)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"3_CR54","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. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.23"},{"key":"3_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). doi: 10.1007\/BFb0025774"},{"key":"3_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/978-3-642-39799-8_37","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., Gaiser, A., K\u0159et\u00ednsk\u00fd, J.: Automata with generalized rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 559\u2013575. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_37"},{"key":"3_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-56922-7_21","volume-title":"Computer Aided Verification","author":"K \u010cer\u0101ns","year":"1993","unstructured":"\u010cer\u0101ns, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification\u2014theory and tools. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 253\u2013267. Springer, Heidelberg (1993). doi: 10.1007\/3-540-56922-7_21"},{"key":"3_CR58","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. 5799, pp. 289\u2013305. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04761-9_22"},{"key":"3_CR59","doi-asserted-by":"crossref","unstructured":"Caillaud, B., Raclet, J.-B.: Ensuring reachability by design. In: Roychoudhury, A., D\u2019Souza, M. (eds.) [RD12], pp. 213\u2013227","DOI":"10.1007\/978-3-642-32943-2_17"},{"issue":"41","key":"3_CR60","doi-asserted-by":"crossref","first-page":"4001","DOI":"10.1016\/j.tcs.2009.06.007","volume":"410","author":"M Carbone","year":"2009","unstructured":"Carbone, M., Sobocinski, P., Valencia, F.D.: Foreword: Festschrift for mogens nielsen\u2019s 60th birthday. Theor. Comput. Sci. 410(41), 4001\u20134005 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR61","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Velner, Y.: Mean-payoff pushdown games. In: LICS, pp. 195\u2013204. IEEE (2012)","DOI":"10.1109\/LICS.2012.30"},{"key":"3_CR62","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-valued abstractions of games: uncertainty, but with precision. In: LICS04 [LIC04], pp. 170\u2013179","DOI":"10.1109\/LICS.2004.1319611"},{"key":"3_CR63","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC\/SIGSOFT FSE, pp. 109\u2013120. ACM (2001)","DOI":"10.1145\/503209.503226"},{"key":"3_CR64","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Braberman, V.A., Piterman, N., Uchitel, S.: The modal transition system control problem. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) [GM12], pp. 155\u2013170","DOI":"10.1007\/978-3-642-32759-9_15"},{"key":"3_CR65","doi-asserted-by":"crossref","unstructured":"Darondeau, P., Dubreil, J., Marchand, H.: Supervisory control for modal specifications of services. In: WODES, pp. 428\u2013435 (2010)","DOI":"10.3182\/20100830-3-DE-4013.00069"},{"key":"3_CR66","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S.: MTSA: the modal transition system analyser. In: ASE, pp. 475\u2013476. IEEE (2008)","DOI":"10.1109\/ASE.2008.78"},{"key":"3_CR67","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: Cheng, L.-T., Orso, A., Robillard, M.P. (eds.) ETX, pp. 6\u201310. ACM (2007)","DOI":"10.1145\/1328279.1328281"},{"key":"3_CR68","doi-asserted-by":"crossref","unstructured":"Delahaye, B., Fahrenberg, U., Larsen, K.G., Legay, A.: Refinement and difference for probabilistic automata. Log. Methods Comput. Sci. 10(3) (2014)","DOI":"10.2168\/LMCS-10(3:11)2014"},{"issue":"2","key":"3_CR69","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":"3_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-18275-4_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Delahaye","year":"2011","unstructured":"Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., W\u0105sowski, A.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324\u2013339. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-18275-4_23"},{"key":"3_CR71","doi-asserted-by":"crossref","unstructured":"Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wasowski, A.: New results on abstract probabilistic automata. In: Caillaud, B., Carmona, J., Hiraishi, K. (eds.) 11th International Conference on Application of Concurrency to System Design, ACSD 2011, Newcastle Upon Tyne, UK, 20\u201324 June 2011, pp. 118\u2013127. IEEE Computer Society (2011)","DOI":"10.1109\/ACSD.2011.10"},{"key":"3_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-15643-4_29","volume-title":"Automated Technology for Verification and Analysis","author":"A David","year":"2010","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., W\u0105sowski, A.: ECDAR: an environment for compositional design and analysis of real time systems. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 365\u2013370. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15643-4_29"},{"key":"3_CR73","doi-asserted-by":"crossref","unstructured":"Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: APAC: a tool for reasoning about abstract probabilistic automata. In: Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5\u20138 September 2011, pp. 151\u2013152. IEEE Computer Society (2011)","DOI":"10.1109\/QEST.2011.28"},{"issue":"1","key":"3_CR74","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jlap.2013.05.006","volume":"83","author":"B Delahaye","year":"2014","unstructured":"Delahaye, B., Larsen, K.G., Legay, A.: Stuttering for abstract probabilistic automata. J. Log. Algebr. Program. 83(1), 1\u201319 (2014)","journal-title":"J. Log. Algebr. Program."},{"key":"3_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","year":"2013","unstructured":"D\u2019Argenio, P.R., Melgratti, H. (eds.): CONCUR 2013. LNCS, vol. 8052. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40184-8"},{"key":"3_CR76","doi-asserted-by":"crossref","unstructured":"Dams, D., Namjoshi, K.S.: The existence of finite abstractions for branching time model checking. In: LICS04 [LIC04], pp. 335\u2013344","DOI":"10.1109\/LICS.2004.1319628"},{"issue":"1","key":"3_CR77","first-page":"69","volume":"26","author":"Z Diskin","year":"2016","unstructured":"Diskin, Z., Safilian, A., Maibaum, T., Ben-David, S.: Faithful modeling of product lines with kripke structures and modal logic. Sci. Ann. Comput. Sci. 26(1), 69\u2013122 (2016)","journal-title":"Sci. Ann. Comput. Sci."},{"key":"3_CR78","unstructured":"Elhog-Benzina, D., Haddad, S., Hennicker, R.: Process refinement and asynchronous composition with modalities. In: Donatelli, S., Kleijn, J., Machado, R.J., Fernandes, J.M. (eds.) ACSD\/Petri Nets Workshops. CEUR Workshop Proceedings, vol. 827, pp. 385\u2013401. CEUR-WS.org (2010)"},{"key":"3_CR79","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/978-3-642-29072-5_4","volume":"5","author":"D Elhog-Benzina","year":"2012","unstructured":"Elhog-Benzina, D., Haddad, S., Hennicker, R.: Refinement and asynchronous composition of modal petri nets. Trans. Petri Nets Other Models Concurr. 5, 96\u2013120 (2012)","journal-title":"Trans. Petri Nets Other Models Concurr."},{"key":"3_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-319-08867-9_13","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2014","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J.: From LTL to deterministic automata: a safraless compositional approach. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 192\u2013208. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_13"},{"key":"3_CR81","doi-asserted-by":"crossref","unstructured":"Fischbein, D., Braberman, V.A., Uchitel, S.: A sound observational semantics for modal transition systems. In: Leucker, M., Morgan, C. (eds.) [LM09], pp. 215\u2013230","DOI":"10.1007\/978-3-642-03466-4_14"},{"key":"3_CR82","unstructured":"Fischbein, D.: Foundations for behavioural model elaboration using modal transition systems. Ph.D. thesis, Imperial College London, UK, (2012)"},{"key":"3_CR83","doi-asserted-by":"crossref","unstructured":"Fahrenberg, U., K\u0159et\u00ednsk\u00fd, J., Legay, A., Traonouez, L.-M.: Compositionality for quantitative specifications. In: Lanese, I., Madelaine, E. (eds.) [LM15], pp. 306\u2013324","DOI":"10.1007\/978-3-319-15317-9_19"},{"key":"3_CR84","doi-asserted-by":"crossref","unstructured":"Fahrenberg, U., Legay, A.: A robust specification theory for modal event-clock automata. In: Bauer, S.S., Raclet, J.-B. (eds) FIT. EPTCS, vol. 87, pp. 5\u201316 (2012)","DOI":"10.4204\/EPTCS.87.2"},{"issue":"5","key":"3_CR85","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s00236-014-0196-8","volume":"51","author":"U Fahrenberg","year":"2014","unstructured":"Fahrenberg, U., Legay, A.: General quantitative specification theories with modal transition systems. Acta Inf. 51(5), 261\u2013295 (2014)","journal-title":"Acta Inf."},{"key":"3_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-319-10882-7_11","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2014","author":"U Fahrenberg","year":"2014","unstructured":"Fahrenberg, U., Legay, A., Traonouez, L.-M.: Structural refinement for the modal nu-Calculus. In: Ciobanu, G., M\u00e9ry, D. (eds.) ICTAC 2014. LNCS, vol. 8687, pp. 169\u2013187. Springer, Cham (2014). doi: 10.1007\/978-3-319-10882-7_11"},{"key":"3_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/11691617_5","volume-title":"Model Checking Software","author":"H Fecher","year":"2006","unstructured":"Fecher, H., Leucker, M., Wolf, V.: Don\u2019t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71\u201388. Springer, Heidelberg (2006). doi: 10.1007\/11691617_5"},{"issue":"2","key":"3_CR88","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/s10626-006-0008-6","volume":"17","author":"G Feuillade","year":"2007","unstructured":"Feuillade, G., Pinchinat, S.: Modal specifications for the control theory of discrete event systems. Discret. Event Dyn. Syst. 17(2), 211\u2013232 (2007)","journal-title":"Discret. Event Dyn. Syst."},{"issue":"2","key":"3_CR89","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/j.entcs.2004.11.031","volume":"128","author":"H Fecher","year":"2005","unstructured":"Fecher, H., Steffen, M.: Characteristic $$\\mu $$ -calculus formulas for underspecified transition systems. Electr. Notes Theor. Comput. Sci. 128(2), 103\u2013116 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"3_CR90","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. Log. Algebr. Program. 77(1\u20132), 20\u201339 (2008)","journal-title":"J. Log. Algebr. Program."},{"key":"3_CR91","doi-asserted-by":"crossref","unstructured":"Fischbein, D., Uchitel, S.: On correct and complete strong merging of partial behaviour models. In: Harrold, M.J., Murphy, G.C. (eds.) SIGSOFT FSE, pp. 297\u2013307. ACM (2008)","DOI":"10.1145\/1453101.1453144"},{"key":"3_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-41071-0_9","volume-title":"Formal Methods: Foundations and Applications","author":"PT Guerra","year":"2013","unstructured":"Guerra, P.T., Andrade, A., Wassermann, R.: Toward the revision of CTL models through Kripke modal transition systems. In: Iyoda, J., Moura, L. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 115\u2013130. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-41071-0_9"},{"key":"3_CR93","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/11691372_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Chechik, M.: Why waste a perfectly good abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 212\u2013226. Springer, Heidelberg (2006). doi: 10.1007\/11691372_14"},{"key":"3_CR94","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). doi: 10.1007\/3-540-44685-0_29"},{"key":"3_CR95","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/3-540-36384-X_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Godefroid","year":"2003","unstructured":"Godefroid, P., Jagadeesan, R.: On the expressiveness of 3-valued models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 206\u2013222. Springer, Heidelberg (2003). doi: 10.1007\/3-540-36384-X_18"},{"key":"3_CR96","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9","volume-title":"FM 2012: Formal Methods","year":"2012","unstructured":"Giannakopoulou, D., M\u00e9ry, D. (eds.): FM 2012. LNCS, vol. 7436. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32759-9"},{"key":"3_CR97","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: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 43\u201356. ACM (2010)","DOI":"10.1145\/1706299.1706307"},{"key":"3_CR98","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Piterman, N.: LTL generalized model checking revisited. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) [JMO09], pp. 89\u2013104","DOI":"10.1007\/978-3-540-93900-9_11"},{"key":"3_CR99","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-58201-0_66","volume-title":"Automata, Languages and Programming","author":"R Gawlick","year":"1994","unstructured":"Gawlick, R., Segala, R., S\u00f8gaard-Andersen, J., Lynch, N.: Liveness in timed and untimed systems. In: Abiteboul, S., Shamir, E. (eds.) ICALP 1994. LNCS, vol. 820, pp. 166\u2013177. Springer, Heidelberg (1994). doi: 10.1007\/3-540-58201-0_66"},{"key":"3_CR100","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/11609773_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Gurfinkel","year":"2005","unstructured":"Gurfinkel, A., Wei, O., Chechik, M.: Systematic construction of abstractions for model-checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 381\u2013397. Springer, Heidelberg (2005). doi: 10.1007\/11609773_25"},{"key":"3_CR101","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11817963_18","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Wei, O., Chechik, M.: Yasm: a software model-checker for verification and refutation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 170\u2013174. Springer, Heidelberg (2006). doi: 10.1007\/11817963_18"},{"issue":"4","key":"3_CR102","doi-asserted-by":"crossref","first-page":"896","DOI":"10.1145\/4221.4249","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy, M.: Acceptance trees. J. ACM 32(4), 896\u2013928 (1985)","journal-title":"J. ACM"},{"issue":"3","key":"3_CR103","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1016\/j.tcs.2008.03.010","volume":"404","author":"A Hussain","year":"2008","unstructured":"Hussain, A., Huth, M.: On model checking multiple hybrid views. Theor. Comput. Sci. 404(3), 186\u2013201 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR104","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-05119-2_13","volume-title":"Trustworthy Global Computing","author":"S Haddad","year":"2014","unstructured":"Haddad, S., Hennicker, R., M\u00f8ller, M.H.: Specification of asynchronous component systems with modal I\/O-petri nets. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 219\u2013234. Springer, Cham (2014). doi: 10.1007\/978-3-319-05119-2_13"},{"key":"3_CR105","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.: Modal transition systems: a foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155\u2013169. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45309-1_11"},{"key":"3_CR106","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J.: Compositional verification and optimization of interactive Markov chains. In: D\u2019Argenio, P.R., Melgratti, H.C. (eds.) [DM13], pp. 364\u2013379","DOI":"10.1007\/978-3-642-40184-8_26"},{"key":"3_CR107","doi-asserted-by":"crossref","unstructured":"Han, T., Krause, C., Kwiatkowska, M.Z., Giese, H.: Modal specifications for probabilistic timed systems. In: Bortolussi, L., Wiklicky, H. (eds.) QAPL. EPTCS, vol. 117, pp. 66\u201380 (2013)","DOI":"10.4204\/EPTCS.117.5"},{"key":"3_CR108","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/3-540-51237-3_14","volume-title":"Logic at Botik \u201989","author":"H H\u00fcttel","year":"1989","unstructured":"H\u00fcttel, H., Larsen, K.G.: The use of static constructs in a model process logic. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 163\u2013180. Springer, Heidelberg (1989). doi: 10.1007\/3-540-51237-3_14"},{"issue":"3","key":"3_CR109","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/BF01887208","volume":"1","author":"S Holmstr\u00f6m","year":"1989","unstructured":"Holmstr\u00f6m, S.: A refinement calculus for specifications in Hennessy-Milner logic with recursion. Formal Asp. Comput. 1(3), 242\u2013272 (1989)","journal-title":"Formal Asp. Comput."},{"key":"3_CR110","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-46691-6_30","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"M Huth","year":"1999","unstructured":"Huth, M.: A unifying framework for model checking labeled kripke structures, modal transition systems, and interval transition systems. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 369\u2013380. Springer, Heidelberg (1999). doi: 10.1007\/3-540-46691-6_30"},{"key":"3_CR111","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-47813-2_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Huth","year":"2002","unstructured":"Huth, M.: Model checking modal transition systems using Kripke structures. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 302\u2013316. Springer, Heidelberg (2002). doi: 10.1007\/3-540-47813-2_21"},{"key":"3_CR112","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266\u2013277. IEEE Computer Society (1991)","DOI":"10.1109\/LICS.1991.151651"},{"issue":"4","key":"3_CR113","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":"3_CR114","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9","volume-title":"Verification, Model Checking, and Abstract Interpretation","year":"2009","unstructured":"Jones, N.D., M\u00fcller-Olm, M. (eds.): VMCAI 2009. LNCS, vol. 5403. Springer, Heidelberg (2009). doi: 10.1007\/978-3-540-93900-9"},{"key":"3_CR115","unstructured":"Juhl, L.: Quantities in games and modal transition systems. Ph.D. thesis, Department of Computer Science, Aalborg University (2013)"},{"key":"3_CR116","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-06410-9_26","volume-title":"FM 2014: Formal Methods","author":"I Krka","year":"2014","unstructured":"Krka, I., D\u2019Ippolito, N., Medvidovi\u0107, N., Uchitel, S.: Revisiting compatibility of input-output modal transition systems. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 367\u2013381. Springer, Cham (2014). doi: 10.1007\/978-3-319-06410-9_26"},{"key":"3_CR117","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-11936-6_17","volume-title":"Automated Technology for Verification and Analysis","author":"Z Kom\u00e1rkov\u00e1","year":"2014","unstructured":"Kom\u00e1rkov\u00e1, Z., K\u0159et\u00ednsk\u00fd, J.: Rabinizer 3: safraless translation of LTL to small deterministic automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 235\u2013241. Springer, Cham (2014). doi: 10.1007\/978-3-319-11936-6_17"},{"key":"3_CR118","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-73368-3_37","volume-title":"Computer Aided Verification","author":"J-P Katoen","year":"2007","unstructured":"Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time Markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311\u2013324. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73368-3_37"},{"issue":"4","key":"3_CR119","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1016\/j.jlap.2012.03.007","volume":"81","author":"J-P Katoen","year":"2012","unstructured":"Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for probabilistic systems. J. Log. Algebr. Program. 81(4), 356\u2013389 (2012)","journal-title":"J. Log. Algebr. Program."},{"key":"3_CR120","doi-asserted-by":"crossref","unstructured":"Krka I., Medvidovic, N.: Revisiting modal interface automata. In: Gnesi, S., Gruner, S., Plat, N., Rumpe, B. (eds.) Proceedings of the First International Workshop on Formal Methods in Software Engineering - Rigorous and Agile Approaches, FormSERA 2012, Zurich, Switzerland, 2 June 2012, pp. 30\u201336. IEEE (2012)","DOI":"10.1109\/FormSERA.2012.6229786"},{"issue":"4","key":"3_CR121","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real-Time Syst."},{"key":"3_CR122","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$ -calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR123","unstructured":"K\u0159et\u00ednsk\u00fd, J.: Modal transition systems: extensions and analysis. Ph.D. thesis, Masaryk University, Brno, Department of Computer Science (2014)"},{"key":"3_CR124","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/11590156_17","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"M K\u0159et\u00ednsk\u00fd","year":"2005","unstructured":"K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: Reachability of Hennessy-Milner properties for weakly extended PRS. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 213\u2013224. Springer, Heidelberg (2005). doi: 10.1007\/11590156_17"},{"issue":"1","key":"3_CR125","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"PC Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43\u201368 (1990)","journal-title":"Inf. Comput."},{"key":"3_CR126","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-319-02444-8_41","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2013","unstructured":"K\u0159et\u00ednsk\u00fd, J., Sickert, S.: MoTraS: a tool for modal transition systems and their extensions. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 487\u2013491. Springer, Cham (2013). doi: 10.1007\/978-3-319-02444-8_41"},{"key":"3_CR127","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-642-39718-9_13","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2013","author":"J K\u0159et\u00ednsk\u00fd","year":"2013","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 2013. LNCS, vol. 8049, pp. 213\u2013230. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39718-9_13"},{"key":"3_CR128","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u00fd, J., Sickert, S.: On refinements of Boolean and parametric modal transition systems. Technical report abs\/1304.5278, arXiv.org (2013)","DOI":"10.1007\/978-3-642-39718-9_13"},{"key":"3_CR129","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Automatic Verification Methods for Finite State Systems","author":"KG Larsen","year":"1990","unstructured":"Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232\u2013246. Springer, Heidelberg (1990). doi: 10.1007\/3-540-52148-8_19"},{"key":"3_CR130","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BFb0039050","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"K Guldstrand Larsen","year":"1990","unstructured":"Guldstrand Larsen, K.: Ideal specification formalism = expressivity + compositionality + decidability + testability +. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 33\u201356. Springer, Heidelberg (1990). doi: 10.1007\/BFb0039050"},{"key":"3_CR131","unstructured":"19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14\u201317 July 2004, Turku, Finland, Proceedings. IEEE Computer Society (2004)"},{"key":"3_CR132","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-37635-1_3","volume-title":"Recent Trends in Algebraic Development Techniques","author":"KG Larsen","year":"2013","unstructured":"Larsen, K.G., Legay, A.: Quantitative modal transition systems. In: Mart\u00ed-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 50\u201358. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-37635-1_3"},{"key":"3_CR133","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03466-4","volume-title":"Theoretical Aspects of Computing - ICTAC 2009","year":"2009","unstructured":"Leucker, M., Morgan, C. (eds.): ICTAC 2009. LNCS, vol. 5684. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03466-4"},{"key":"3_CR134","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-15317-9","volume-title":"Formal Aspects of Component Software","year":"2015","unstructured":"Lanese, I., Madelaine, E. (eds.): FACS 2014. LNCS, vol. 8997. Springer, Cham (2015). doi: 10.1007\/978-3-319-15317-9"},{"key":"3_CR135","doi-asserted-by":"crossref","unstructured":"Luthmann, L., Mennicke, S., Lochau, M.: Towards an I\/O conformance testing theory for software product lines based on modal interface automata. In: Atlee, J.M., Gnesi, S. (eds.) Proceedings 6th Workshop on Formal Methods and Analysis in SPL Engineering, FMSPLE@ETAPS 2015, London, UK, 11 April 2015. EPTCS, vol. 182, pp. 1\u201313 (2015)","DOI":"10.4204\/EPTCS.182.1"},{"key":"3_CR136","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: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64\u201379. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71316-6_6"},{"key":"3_CR137","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-540-74407-8_8","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"KG Larsen","year":"2007","unstructured":"Larsen, K.G., Nyman, U., W\u0105sowski, A.: On modal refinement and consistency. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 105\u2013119. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74407-8_8"},{"key":"3_CR138","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1007\/BFb0020979","volume-title":"Hybrid Systems III","author":"KG Larsen","year":"1996","unstructured":"Larsen, K.G., Steffen, B., Weise, C.: Fischer\u2019s protocol revisited: a simple proof using modal constraints. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 604\u2013615. Springer, Heidelberg (1996). doi: 10.1007\/BFb0020979"},{"key":"3_CR139","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":"3_CR140","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"},{"issue":"4\u20135","key":"3_CR141","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/s00236-014-0211-0","volume":"52","author":"G L\u00fcttgen","year":"2015","unstructured":"L\u00fcttgen, G., Vogler, W., Fendrich, S.: Richer interface automata with optimistic and pessimistic compatibility. Acta Inf. 52(4\u20135), 305\u2013336 (2015)","journal-title":"Acta Inf."},{"key":"3_CR142","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"},{"key":"3_CR143","unstructured":"Manta, A.: Implementation of algorithms for modal transition systems with durations. Bachelor\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen (2013)"},{"issue":"1\u20132","key":"3_CR144","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1006\/inco.1999.2826","volume":"156","author":"R Mayr","year":"2000","unstructured":"Mayr, R.: Process rewrite systems. Inf. Comput. 156(1\u20132), 264\u2013286 (2000)","journal-title":"Inf. Comput."},{"key":"3_CR145","unstructured":"M\u00f8ller, M.H.: Modal and component-based system specifications. Ph.D. thesis, Department of Computer Science, Aalborg University (2013)"},{"key":"3_CR146","unstructured":"Motras. http:\/\/www7.in.tum.de\/kretinsk\/motras.html"},{"key":"3_CR147","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":"KS Namjoshi","year":"2003","unstructured":"Namjoshi, K.S.: Abstraction for branching time properties. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 288\u2013300. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45069-6_29"},{"key":"3_CR148","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-540-69166-2_11","volume-title":"Static Analysis","author":"S Nanz","year":"2008","unstructured":"Nanz, S., Nielson, F., Riis Nielson, H.: Modal abstractions of concurrent behaviour. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 159\u2013173. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-69166-2_11"},{"key":"3_CR149","unstructured":"Nyman, U.: Modal transition systems as the basis for interface theories and product lines. Ph.D. thesis, Aalborg Universitet (2008)"},{"key":"3_CR150","doi-asserted-by":"crossref","unstructured":"Pnueli, A. The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"3_CR151","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: LICS, pp. 275\u2013284. IEEE Computer Society (2006)","DOI":"10.1109\/LICS.2006.23"},{"key":"3_CR152","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190. ACM Press (1989)","DOI":"10.1145\/75277.75293"},{"issue":"6","key":"3_CR153","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987)","journal-title":"SIAM J. Comput."},{"key":"3_CR154","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). doi: 10.1007\/3-540-11494-7_22"},{"key":"3_CR155","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":"3_CR156","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/j.entcs.2008.06.023","volume":"215","author":"J-B Raclet","year":"2008","unstructured":"Raclet, J.-B.: Residual for component specifications. Electr. Notes Theor. Comput. Sci. 215, 93\u2013110 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR157","doi-asserted-by":"crossref","unstructured":"Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: Modal interfaces: unifying interface automata and modal specifications. In:Chakraborty, S., Halbwachs, N., (eds.) EMSOFT, pp. 87\u201396. ACM (2009)","DOI":"10.1145\/1629335.1629348"},{"key":"3_CR158","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 Computer Society (2009)","DOI":"10.1109\/ACSD.2009.22"},{"issue":"1\u20132","key":"3_CR159","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. Fundam. Inform. 108(1\u20132), 119\u2013149 (2011)","journal-title":"Fundam. Inform."},{"key":"3_CR160","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32943-2","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","year":"2012","unstructured":"Roychoudhury, A., D\u2019Souza, M. (eds.): ICTAC 2012. LNCS, vol. 7521. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32943-2"},{"issue":"7","key":"3_CR161","doi-asserted-by":"crossref","first-page":"975","DOI":"10.1109\/TSE.2012.62","volume":"39","author":"GE Sibay","year":"2013","unstructured":"Sibay, G.E., Braberman, V.A., Uchitel, S., Kramer, J.: Synthesizing modal transition systems from triggered scenarios. IEEE Trans. Softw. Eng. 39(7), 975\u20131001 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR162","unstructured":"Schlachter, U.: Bounded petri net synthesis from modal transition systems is undecidable. In: Desharnais, J., Jagadeesan, R. (eds.), 27th International Conference on Concurrency Theory, CONCUR 2016, Qu\u00e9bec City, Canada, 23\u201326 August 2016. LIPIcs, vol. 59, pp. 15:1\u201315:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)"},{"issue":"1","key":"3_CR163","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/s10270-010-0148-x","volume":"10","author":"M Sassolas","year":"2011","unstructured":"Sassolas, M., Chechik, M., Uchitel, S.: Exploring inconsistencies between modal transition systems. Softw. Syst. Model. 10(1), 117\u2013142 (2011)","journal-title":"Softw. Syst. Model."},{"key":"3_CR164","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-24730-2_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Shoham","year":"2004","unstructured":"Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546\u2013560. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24730-2_40"},{"issue":"4","key":"3_CR165","doi-asserted-by":"crossref","first-page":"65:1","DOI":"10.1145\/2776892","volume":"14","author":"A Siirtola","year":"2015","unstructured":"Siirtola, A., Heljanko, K.: Parametrised modal interface automata. ACM Trans. Embed. Comput. Syst. 14(4), 65:1\u201365:25 (2015)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"3_CR166","doi-asserted-by":"crossref","unstructured":"Sharma, A., Katoen, J.-P.: Layered reduction for abstract probabilistic automata. In: 14th International Conference on Application of Concurrency to System Design, ACSD 2014, Tunis La Marsa, Tunisia, 23\u201327 June 2014, pp. 21\u201331. IEEE Computer Society (2014)","DOI":"10.1109\/ACSD.2014.10"},{"key":"3_CR167","doi-asserted-by":"crossref","unstructured":"Sibay, G.E., Uchitel, S., Braberman, V.A., Kramer, J.: Distribution of modal transition systems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) [GM12], pp. 403\u2013417","DOI":"10.1007\/978-3-642-32759-9_33"},{"key":"3_CR168","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-319-22969-0_24","volume-title":"Software Engineering and Formal Methods","author":"MH Beek","year":"2015","unstructured":"Beek, M.H., Damiani, F., Gnesi, S., Mazzanti, F., Paolini, L.: From featured transition systems to modal transition systems with variability constraints. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 344\u2013359. Springer, Cham (2015). doi: 10.1007\/978-3-319-22969-0_24"},{"issue":"2","key":"3_CR169","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/j.jlamp.2015.11.006","volume":"85","author":"MH Beek ter","year":"2016","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebr. Meth. Program. 85(2), 287\u2013315 (2016)","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"3_CR170","doi-asserted-by":"crossref","unstructured":"Uchitel, S., Brunet, G., Chechik, M.: Behaviour model synthesis from properties and scenarios. In: ICSE, pp. 34\u201343. IEEE Computer Society (2007)","DOI":"10.1109\/ICSE.2007.21"},{"issue":"3","key":"3_CR171","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1109\/TSE.2008.107","volume":"35","author":"S Uchitel","year":"2009","unstructured":"Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans. Softw. Eng. 35(3), 384\u2013406 (2009)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR172","doi-asserted-by":"crossref","unstructured":"Uchitel, S., Chechik, M.: Merging partial behavioural models. In: Taylor, R.N., Dwyer, M.B. (eds.) SIGSOFT FSE, pp. 43\u201352. ACM (2004)","DOI":"10.1145\/1029894.1029904"},{"key":"3_CR173","doi-asserted-by":"crossref","unstructured":"Verdier, G., Raclet, J.-B.: Maccs: a tool for reachability by design. In: Lanese, I., Madelaine, E. (eds.) [LM15], pp. 191\u2013197","DOI":"10.1007\/978-3-319-15317-9_12"},{"key":"3_CR174","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-319-15579-1_23","volume-title":"Language and Automata Theory and Applications","author":"G Verdier","year":"2015","unstructured":"Verdier, G., Raclet, J.-B.: Quotient of acceptance specifications under reachability constraints. In: Dediu, A.-H., Formenti, E., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2015. LNCS, vol. 8977, pp. 299\u2013311. Springer, Cham (2015). doi: 10.1007\/978-3-319-15579-1_23"},{"key":"3_CR175","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume-title":"Computer Aided Verification","author":"I Walukiewicz","year":"1996","unstructured":"Walukiewicz, I.: Pushdown processes: games and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 62\u201374. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61474-5_58"},{"key":"3_CR176","doi-asserted-by":"crossref","unstructured":"Wei, O., Gurfinkel, A., Chechik, M.: Mixed transition systems revisited. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) [JMO09], pp. 349\u2013365","DOI":"10.1007\/978-3-540-93900-9_28"}],"container-title":["Lecture Notes in Computer Science","Models, Algorithms, Logics and Tools"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63121-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,31]],"date-time":"2022-07-31T11:13:17Z","timestamp":1659265997000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63121-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631202","9783319631219"],"references-count":176,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63121-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}