{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T22:22:40Z","timestamp":1773526960805,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319108810","type":"print"},{"value":"9783319108827","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10882-7_11","type":"book-chapter","created":{"date-parts":[[2014,9,11]],"date-time":"2014-09-11T02:54:19Z","timestamp":1410404059000},"page":"169-187","source":"Crossref","is-referenced-by-count":6,"title":["Structural Refinement for the Modal nu-Calculus"],"prefix":"10.1007","author":[{"given":"Uli","family":"Fahrenberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Louis-Marie","family":"Traonouez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Reactive Systems. Cambridge Univ. Press (2007)","DOI":"10.1017\/CBO9780511814105"},{"key":"11_CR2","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":"S.S. 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: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering. LNCS, vol.\u00a07212, pp. 43\u201358. Springer, Heidelberg (2012)"},{"key":"11_CR3","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":"S.S. 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.\u00a06907, pp. 60\u201371. Springer, Heidelberg (2011)"},{"key":"11_CR4","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":"S.S. 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.\u00a07353, pp. 18\u201330. Springer, Heidelberg (2012)"},{"key":"11_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":"11_CR6","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 \u2013 Concurrency Theory. LNCS, vol.\u00a08052, pp. 76\u201390. Springer, Heidelberg (2013)"},{"key":"11_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., Larsen, K.G., 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":"11_CR8","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., Srba, J.: On determinism in modal transition systems. Th. Comp. Sci.\u00a0410(41), 4026\u20134043 (2009)","DOI":"10.1016\/j.tcs.2009.06.009"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., Srba, J.: EXPTIME-completeness of thorough refinement on modal transition systems. Inf. Comp.\u00a0218, 54\u201368 (2012)","DOI":"10.1016\/j.ic.2012.08.001"},{"issue":"3","key":"11_CR10","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1093\/jigpal\/8.3.339","volume":"8","author":"P. Blackburn","year":"2000","unstructured":"Blackburn, P.: Representation, reasoning, and relational structures: a hybrid logic manifesto. Log. J. IGPL\u00a08(3), 339\u2013365 (2000)","journal-title":"Log. J. IGPL"},{"issue":"1","key":"11_CR11","doi-asserted-by":"publisher","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. Th. Comp. Sci.\u00a0106(1), 3\u201320 (1992)","journal-title":"Th. Comp. Sci."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Bradfield, J., Stirling, C.: Modal mu-calculi. In: The Handbook of Modal Logic. Elsevier (2006)","DOI":"10.1016\/S1570-2464(07)80015-2"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Caires, L., Cardelli, L.: A spatial logic for concurrency. Inf. Comp.\u00a0186(2) (2003)","DOI":"10.1016\/S0890-5401(03)00137-8"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. 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.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-540-45187-7_7","volume-title":"CONCUR 2003 - Concurrency Theory","author":"L. Alfaro de","year":"2003","unstructured":"de Alfaro, L.: Quantitative verification and control via the mu-calculus. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 103\u2013127. Springer, Heidelberg (2003)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1022","DOI":"10.1007\/3-540-45061-0_79","volume-title":"Automata, Languages and Programming","author":"L. Alfaro de","year":"2003","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, pp. 1022\u20131037. Springer, Heidelberg (2003)"},{"key":"11_CR17","unstructured":"Fahrenberg, U., Legay, A., Traonouez, L.-M.: Structural refinement for the modal nu-calculus. CoRR, 1402.2143 (2014), \n                  \n                    http:\/\/arxiv.org\/abs\/1402.2143"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-642-32940-1_28","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"D. Gebler","year":"2012","unstructured":"Gebler, D., Fokkink, W.: Compositionality of probabilistic Hennessy-Milner logic through structural operational semantics. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 395\u2013409. Springer, Heidelberg (2012)"},{"issue":"4","key":"11_CR19","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1142\/S0218196702001048","volume":"12","author":"J.B. Hart","year":"2002","unstructured":"Hart, J.B., Rafter, L., Tsinakis, C.: The structure of commutative residuated lattices. Internat. J. Algebra Comput.\u00a012(4), 509\u2013524 (2002)","journal-title":"Internat. J. Algebra Comput."},{"issue":"4","key":"11_CR20","doi-asserted-by":"publisher","first-page":"896","DOI":"10.1145\/4221.4249","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M.: Acceptance trees. J. ACM\u00a032(4), 896\u2013928 (1985)","journal-title":"J. ACM"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Th. Comp. Sci.\u00a027 (1983)","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"11_CR22","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":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 232\u2013246. Springer, Heidelberg (1990)"},{"key":"11_CR23","series-title":"LNCS","first-page":"33","volume-title":"CONCUR 1990","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G.: Ideal specification formalism = expressivity + compositionality + decidability + testability +. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol.\u00a0458, pp. 33\u201356. Springer, Heidelberg (1990)"},{"issue":"2&3","key":"11_CR24","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. Th. Comp. Sci.\u00a072(2&3), 265\u2013288 (1990)","journal-title":"Th. Comp. Sci."},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-56496-9_4","volume-title":"Computer Aided Verification","author":"K.G. Larsen","year":"1993","unstructured":"Larsen, K.G.: Efficient local correctness checking. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 30\u201343. Springer, Heidelberg (1993)"},{"key":"11_CR26","unstructured":"Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: LICS. IEEE Computer Society (1990)"},{"key":"11_CR27","unstructured":"Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (1997)"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"11_CR29","volume-title":"Papers on Time and Tense","author":"A.N. Prior","year":"1968","unstructured":"Prior, A.N.: Papers on Time and Tense. Clarendon Press, Oxford (1968)"},{"key":"11_CR30","unstructured":"Raclet, J.-B.: Residual for component specifications. Publication interne 1843, IRISA, Rennes (2007)"},{"key":"11_CR31","doi-asserted-by":"publisher","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.\u00a0215, 93\u2013110 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"11_CR32","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS. IEEE Computer Society (2002)"},{"key":"11_CR33","unstructured":"Scott, D., de Bakker, J.W.: A theory of programs. IBM, Vienna (1969) (unpublished manuscript)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10882-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T17:40:48Z","timestamp":1558978848000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10882-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319108810","9783319108827"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10882-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}