{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:55:28Z","timestamp":1762458928912},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642243714"},{"type":"electronic","value":"9783642243721"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24372-1_17","type":"book-chapter","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T05:41:14Z","timestamp":1317274874000},"page":"228-242","source":"Crossref","is-referenced-by-count":20,"title":["Modal Transition Systems: Composition and LTL Model Checking"],"prefix":"10.1007","author":[{"given":"Nikola","family":"Bene\u0161","sequence":"first","affiliation":[]},{"given":"Ivana","family":"\u010cern\u00e1","sequence":"additional","affiliation":[]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"5-6","key":"17_CR1","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/s10009-007-0046-x","volume":"9","author":"K.G. Larsen","year":"2007","unstructured":"Larsen, K.G., Nyman, U., Wasowski, A.: Modeling software product lines using color-blind transition systems. STTT\u00a09(5-6), 471\u2013487 (2007)","journal-title":"STTT"},{"key":"17_CR2","first-page":"203","volume-title":"LICS","author":"K.G. Larsen","year":"1988","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203\u2013210. IEEE Computer Society, Los Alamitos (1988)"},{"key":"17_CR3","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bulletin of the EATCS\u00a0(95), 94\u2013129 (2008)"},{"key":"17_CR4","unstructured":"Raclet, J.B.: Residual for component specifications. In: Proc. of the 4th International Workshop on Formal Aspects of Component Software (2007)"},{"key":"17_CR5","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.\u00a05457, pp. 152\u2013163. Springer, Heidelberg (2009)"},{"key":"17_CR6","first-page":"119","volume-title":"ACSD","author":"J.B. Raclet","year":"2009","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, Los Alamitos (2009)"},{"key":"17_CR7","first-page":"43","volume-title":"Proc. of FSE 2004","author":"S. Uchitel","year":"2004","unstructured":"Uchitel, S., Chechik, M.: Merging partial behavioural models. In: Proc. of FSE 2004, pp. 43\u201352. ACM, New York (2004)"},{"key":"17_CR8","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":"17_CR9","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":"17_CR10","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., Nielson, H.R.: Modal abstractions of concurrent behaviour. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 159\u2013173. Springer, Heidelberg (2008)"},{"key":"17_CR11","first-page":"108","volume-title":"LICS","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: LICS, pp. 108\u2013117. IEEE Computer Society, Los Alamitos (1990)"},{"issue":"2","key":"17_CR12","first-page":"103","volume":"128","author":"H. Fecher","year":"2005","unstructured":"Fecher, H., Steffen, M.: Characteristic mu-calculus formulas for underspecified transition systems. ENTCS\u00a0128(2), 103\u2013116 (2005)","journal-title":"ENTCS"},{"issue":"1-2","key":"17_CR13","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. of Logic and Alg. Program.\u00a077(1-2), 20\u201339 (2008)","journal-title":"J. of Logic and Alg. Program."},{"key":"17_CR14","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: EXPTIME-complete decision problems for mixed and modal specifications. In: 15th International Workshop on Expressiveness in Concurrency (2008)"},{"issue":"41","key":"17_CR15","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., Larsen, K., Srba, J.: On determinism in modal transition systems. Theoretical Computer Science\u00a0410(41), 4026\u20134043 (2009)","journal-title":"Theoretical Computer Science"},{"key":"17_CR16","unstructured":"Juhl, L., Larsen, K.G., Srba, J.: Introducing modal transition systems with weight intervals (submitted)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-44618-4_14","volume-title":"CONCUR 2000 - Concurrency Theory","author":"G. Bruns","year":"2000","unstructured":"Bruns, G., Godefroid, P.: Generalized model checking: Reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 168\u2013182. Springer, Heidelberg (2000)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-540-93900-9_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Godefroid","year":"2009","unstructured":"Godefroid, P., Piterman, N.: LTL generalized model checking revisited. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 89\u2013104. Springer, Heidelberg (2009)"},{"issue":"3","key":"17_CR19","doi-asserted-by":"publisher","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. Software Eng.\u00a035(3), 384\u2013406 (2009)","journal-title":"IEEE Trans. Software Eng."},{"key":"17_CR20","first-page":"475","volume-title":"Proc. of ASE 2008","author":"N. D\u2019Ippolito","year":"2008","unstructured":"D\u2019Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S.: MTSA: The modal transition system analyser. In: Proc. of ASE 2008, pp. 475\u2013476. IEEE, Los Alamitos (2008)"},{"key":"17_CR21","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":"17_CR22","series-title":"OASICS","first-page":"9","volume-title":"MEMICS","author":"N. Bene\u0161","year":"2010","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J.: Process algebra for modal transition systemses. In: MEMICS. OASICS, vol.\u00a016, pp. 9\u201318. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (2010)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-03466-4_7","volume-title":"Theoretical Aspects of Computing - ICTAC 2009","author":"N. Bene\u0161","year":"2009","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.) ICTAC 2009. LNCS, vol.\u00a05684, pp. 112\u2013126. Springer, Heidelberg (2009)"},{"key":"17_CR24","first-page":"46","volume-title":"FOCS","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE, Los Alamitos (1977)"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 128\u2013147. Springer, Heidelberg (2004)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-45657-0_11","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 137\u2013151. Springer, Heidelberg (2002)"},{"key":"17_CR27","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":"2002","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.\u00a02575, pp. 206\u2013222. Springer, Heidelberg (2002)"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"Automata, Languages and Programming","author":"A. Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372, pp. 652\u2013671. Springer, Heidelberg (1989)"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-30579-8_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Dams","year":"2005","unstructured":"Dams, D., Namjoshi, K.S.: Automata as abstractions. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 216\u2013232. Springer, Heidelberg (2005)"},{"issue":"1","key":"17_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/963927.963928","volume":"5","author":"R. Alur","year":"2004","unstructured":"Alur, R., Torre, S.L.: Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log.\u00a05(1), 1\u201325 (2004)","journal-title":"ACM Trans. Comput. Log."},{"key":"17_CR31","first-page":"275","volume-title":"Proceedings of LICS 2006","author":"N. Piterman","year":"2006","unstructured":"Piterman, N., Pnueli, A.: Faster solution of rabin and streett games. In: Proceedings of LICS 2006, pp. 275\u2013284. IEEE press, Los Alamitos (2006)"},{"key":"17_CR32","volume-title":"Principles of model checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press, Cambridge (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24372-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T02:42:43Z","timestamp":1554691363000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24372-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642243714","9783642243721"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24372-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}