{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T16:30:31Z","timestamp":1774801831085,"version":"3.50.1"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,10,24]],"date-time":"2012-10-24T00:00:00Z","timestamp":1351036800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,4]]},"DOI":"10.1007\/s10703-012-0178-9","type":"journal-article","created":{"date-parts":[[2012,10,23]],"date-time":"2012-10-23T11:17:53Z","timestamp":1350991073000},"page":"193-220","source":"Crossref","is-referenced-by-count":17,"title":["Weighted modal transition systems"],"prefix":"10.1007","volume":"42","author":[{"given":"Sebastian S.","family":"Bauer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uli","family":"Fahrenberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Line","family":"Juhl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claus","family":"Thrane","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,10,24]]},"reference":[{"issue":"2","key":"178_CR1","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1109\/TSE.2008.106","volume":"35","author":"L Alfaro de","year":"2009","unstructured":"de Alfaro L, Faella M, Stoelinga M (2009) Linear and branching system metrics. IEEE Trans Softw Eng 35(2):258\u2013273","journal-title":"IEEE Trans Softw Eng"},{"key":"178_CR2","series-title":"NATO science series II: mathematics, physics and chemistry","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/1-4020-3532-2_3","volume-title":"Engineering theories of software intensive systems","author":"L Alfaro de","year":"2005","unstructured":"de Alfaro L, Henzinger T (2005) Interface-based design. In: Broy M, Gr\u00fcnbauer J, Harel D, Hoare T (eds) Engineering theories of software intensive systems. NATO science series II: mathematics, physics and chemistry, vol 195. Springer, Berlin, pp 83\u2013104"},{"key":"178_CR3","volume-title":"Infinite dimensional analysis: a hitchhiker\u2019s guide","author":"CD Aliprantis","year":"2007","unstructured":"Aliprantis CD, Border KC (2007) Infinite dimensional analysis: a hitchhiker\u2019s guide. Springer, Berlin"},{"key":"178_CR4","first-page":"94","volume":"95","author":"A Antonik","year":"2008","unstructured":"Antonik A, Huth M, Larsen KG, Nyman U, W\u0105sowski A (2008) 20 years of modal and mixed specifications. Bull Eur Assoc Theor Comput Sci 95:94\u2013129","journal-title":"Bull Eur Assoc Theor Comput Sci"},{"key":"178_CR5","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/978-3-642-13464-7_4","volume-title":"FMOODS\/FORTE","author":"A Basu","year":"2010","unstructured":"Basu A, Bensalem S, Bozga M, Caillaud B, Delahaye B, Legay A (2010) Statistical abstraction and model-checking of large heterogeneous systems. In: Hatcliff J, Zucca E (eds) FMOODS\/FORTE. Lecture notes in computer science, vol 6117. Springer, Berlin, pp 32\u201346"},{"key":"178_CR6","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/978-3-642-22993-0_9","volume-title":"MFCS","author":"SS Bauer","year":"2011","unstructured":"Bauer SS, Fahrenberg U, Juhl L, Larsen KG, Legay A, Thrane C (2011) Quantitative refinement for weighted modal transition systems. In: Murlak F, Sankowski P (eds) MFCS. Lecture notes in computer science, vol 6907. Springer, Berlin, pp 60\u201371"},{"issue":"4","key":"178_CR7","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1017\/S0960129511000697","volume":"22","author":"SS Bauer","year":"2012","unstructured":"Bauer SS, Juhl L, Larsen KG, Legay A, Srba J (2012) Extending modal transition systems with structured labels. Math Struct Comput Sci 22(4):581\u2013617","journal-title":"Math Struct Comput Sci"},{"key":"178_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/978-3-642-24372-1_17","volume-title":"ATVA","author":"N Bene\u0161","year":"2011","unstructured":"Bene\u0161 N, \u010cern\u00e1 I, K\u0159et\u00ednsk\u00fd J (2011) Modal transition systems: composition and LTL model checking. In: Bultan T, Hsiung P-A (eds) ATVA. Lecture notes in computer science, vol 6996. Springer, Berlin, pp\u00a0228\u2013242"},{"key":"178_CR9","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/978-3-642-03466-4_7","volume-title":"ICTAC","author":"N Bene\u0161","year":"2009","unstructured":"Bene\u0161 N, K\u0159et\u00ednsk\u00fd J, Larsen KG, Srba J (2009) Checking thorough refinement on modal transition systems is EXPTIME-complete. In: Leucker M, Morgan C (eds) ICTAC. Lecture notes in computer science, vol 5684. Springer, Berlin, pp\u00a0112\u2013126"},{"issue":"1\u20132","key":"178_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(97)00042-X","volume":"193","author":"MM Bonsangue","year":"1998","unstructured":"Bonsangue MM, van Breugel F, Rutten JJMM (1998) Generalized metric spaces: completion, topology, and powerdomains via the Yoneda embedding. Theor Comput Sci 193(1\u20132):1\u201351","journal-title":"Theor Comput Sci"},{"issue":"1","key":"178_CR11","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/j.tcs.2011.08.002","volume":"413","author":"P \u010cern\u00fd","year":"2012","unstructured":"\u010cern\u00fd P, Henzinger TA, Radhakrishna A (2012) Simulation distances. Theor Comput Sci 413(1):21\u201335","journal-title":"Theor Comput Sci"},{"key":"178_CR12","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1007\/3-540-45657-0_34","volume-title":"CAV","author":"A Chakrabarti","year":"2002","unstructured":"Chakrabarti A, de Alfaro L, Henzinger TA, Mang FYC (2002) Synchronous and bidirectional component interfaces. In: Brinksma E, Larsen KG (eds) CAV. Lecture notes in computer science, vol 2404. Springer, Berlin, pp\u00a0414\u2013427"},{"key":"178_CR13","doi-asserted-by":"crossref","unstructured":"Chatterjee K, de Alfaro L, Majumdar R, Raman V (2010) Algorithms for game metrics. Log Methods Comput Sci 6(3)","DOI":"10.2168\/LMCS-6(3:13)2010"},{"key":"178_CR14","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Doyen L, Henzinger TA (2010) Expressiveness and closure properties for quantitative languages. Log Methods Comput Sci 6(3)","DOI":"10.2168\/LMCS-6(3:10)2010"},{"key":"178_CR15","unstructured":"STREP COMBEST (COMponent-Based Embedded Systems Design Techniques). http:\/\/www.combest.eu\/home\/"},{"issue":"2","key":"178_CR16","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A Condon","year":"1992","unstructured":"Condon A (1992) The complexity of stochastic games. Inf Comput 96(2):203\u2013224","journal-title":"Inf Comput"},{"key":"178_CR17","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1145\/1755952.1755967","volume-title":"HSCC","author":"A David","year":"2010","unstructured":"David A, Larsen KG, Legay A, Nyman U, W\u0105sowski A (2010) Timed I\/O automata: a complete specification theory for real-time systems. In: Johansson KH, Yi W (eds) HSCC. ACM, New York, pp\u00a091\u2013100"},{"key":"178_CR18","series-title":"Lecture notes in computer science","first-page":"102","volume-title":"CONCUR","author":"L Alfaro de","year":"2003","unstructured":"de Alfaro L (2003) Quantitative verification and control via the mu-calculus. In: Amadio RM, Lugiez D (eds) CONCUR. Lecture notes in computer science, vol 2761. Springer, Berlin, pp\u00a0102\u2013126"},{"key":"178_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"1022","DOI":"10.1007\/3-540-45061-0_79","volume-title":"ICALP","author":"L Alfaro de","year":"2003","unstructured":"de Alfaro L, Henzinger TA, Majumdar R (2003) Discounting the future in systems theory. In: Baeten JCM, Karel Lenstra J, Parrow J, Woeginger GJ (eds) ICALP. Lecture notes in computer science, vol 2719. Springer, Berlin, pp\u00a01022\u20131037"},{"key":"178_CR20","doi-asserted-by":"crossref","unstructured":"de Alfaro L, Majumdar R, Raman V, Stoelinga M (2008) Game refinement relations and metrics. Log Methods Comput Sci 4(3)","DOI":"10.2168\/LMCS-4(3:7)2008"},{"key":"178_CR21","unstructured":"Delahaye B (2010) Modular specification and compositional analysis of stochastic systems. PhD thesis, Universit\u00e9 de Rennes 1"},{"issue":"3","key":"178_CR22","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/j.tcs.2003.09.013","volume":"318","author":"J Desharnais","year":"2004","unstructured":"Desharnais J, Gupta V, Jagadeesan R, Panangaden P (2004) Metrics for labelled Markov processes. Theor Comput Sci 318(3):323\u2013354","journal-title":"Theor Comput Sci"},{"issue":"1\u20132","key":"178_CR23","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/j.tcs.2007.02.055","volume":"380","author":"M Droste","year":"2007","unstructured":"Droste M, Gastin P (2007) Weighted automata and weighted logics. Theor Comput Sci 380(1\u20132):69\u201386","journal-title":"Theor Comput Sci"},{"key":"178_CR24","series-title":"EATCS monographs in theoretical computer science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-01492-5","volume-title":"Handbook of weighted automata","author":"M Droste","year":"2009","unstructured":"Droste M, Kuich W, Vogler H (2009) Handbook of weighted automata. EATCS monographs in theoretical computer science. Springer, Berlin"},{"issue":"37","key":"178_CR25","doi-asserted-by":"crossref","first-page":"3481","DOI":"10.1016\/j.tcs.2009.03.029","volume":"410","author":"M Droste","year":"2009","unstructured":"Droste M, Rahonis G (2009) Weighted automata and weighted logics with discounting. Theor Comput Sci 410(37):3481\u20133494","journal-title":"Theor Comput Sci"},{"issue":"6+","key":"178_CR26","first-page":"1311","volume":"29","author":"U Fahrenberg","year":"2010","unstructured":"Fahrenberg U, Larsen KG, Thrane C (2010) A quantitative characterization of weighted Kripke structures in temporal logic. Comput Inform 29(6+):1311\u20131324","journal-title":"Comput Inform"},{"key":"178_CR27","series-title":"LIPIcs","first-page":"103","volume-title":"FSTTCS","author":"U Fahrenberg","year":"2011","unstructured":"Fahrenberg U, Legay A, Thrane C (2011) The quantitative linear-time\u2013branching-time spectrum. In: Chakraborty S, Kumar A (eds) FSTTCS. LIPIcs, vol 13. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Leibniz, pp\u00a0103\u2013114"},{"key":"178_CR28","series-title":"Electronic proceedings in theoretical computer science","first-page":"134","volume-title":"QAPL","author":"U Fahrenberg","year":"2011","unstructured":"Fahrenberg U, Thrane C, Larsen KG (2011) Distances for weighted transition systems: games and properties. In: Massink M, Norman G (eds) QAPL. Electronic proceedings in theoretical computer science, vol 57, pp\u00a0134\u2013147"},{"key":"178_CR29","first-page":"67","volume-title":"FIW","author":"RJ Hall","year":"2000","unstructured":"Hall RJ (2000) Feature interactions in electronic mail. In: Calder M, Magill EH (eds) FIW. IOS Press, Amsterdam, pp\u00a067\u201382"},{"issue":"4","key":"178_CR30","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 KG, Srba J (2012) Modal transition systems with weight intervals. J\u00a0Log Algebr Program 81(4):408\u2013421","journal-title":"J\u00a0Log Algebr Program"},{"key":"178_CR31","series-title":"Lecture notes in computer science","first-page":"232","volume-title":"Automatic verification methods for finite state systems","author":"KG Larsen","year":"1989","unstructured":"Larsen KG (1989) Modal specifications. In: Sifakis J (ed) Automatic verification methods for finite state systems. Lecture notes in computer science, vol 407. Springer, Berlin, pp\u00a0232\u2013246"},{"issue":"28","key":"178_CR32","doi-asserted-by":"crossref","first-page":"3358","DOI":"10.1016\/j.tcs.2011.04.003","volume":"412","author":"KG Larsen","year":"2011","unstructured":"Larsen KG, Fahrenberg U, Thrane C (2011) Metrics for weighted transition systems: axiomatization and complexity. Theor Comput Sci 412(28):3358\u20133369","journal-title":"Theor Comput Sci"},{"key":"178_CR33","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/BF02924844","volume":"XLIII","author":"FW Lawvere","year":"1973","unstructured":"Lawvere FW (1973) Metric spaces, generalized logic, and closed categories. Rend Semin Mat Fis Milano XLIII:135\u2013166","journal-title":"Rend Semin Mat Fis Milano"},{"key":"178_CR34","first-page":"147","volume":"XX","author":"F William\u00a0Lawvere","year":"1986","unstructured":"William\u00a0Lawvere F (1986) Taking categories seriously. Rev Colomb Mat XX:147\u2013178","journal-title":"Rev Colomb Mat"},{"key":"178_CR35","unstructured":"Lynch N, Tuttle MR (1989) An introduction to input\/output automata. Quart - Cent Wiskd Inform 2(3)"},{"key":"178_CR36","unstructured":"Majumdar R (2003) Symbolic algorithms for verification and control. PhD thesis, University of California, Berkeley"},{"key":"178_CR37","unstructured":"Nyman U (2008) Modal transition systems as the basis for interface theories and product lines. PhD thesis, Aalborg University"},{"key":"178_CR38","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 (2008) Residual for component specifications. Electron Notes Theor Comput Sci 215:93\u2013110","journal-title":"Electron Notes Theor Comput Sci"},{"key":"178_CR39","doi-asserted-by":"crossref","unstructured":"Davide S (2009) On the origins of bisimulation and coinduction. ACM Trans Program Lang Syst 31(4)","DOI":"10.1145\/1516507.1516510"},{"issue":"1","key":"178_CR40","doi-asserted-by":"crossref","first-page":"108","DOI":"10.2478\/s13537-011-0008-y","volume":"1","author":"J Sifakis","year":"2011","unstructured":"Sifakis J (2011) A vision for computer science\u2014the system perspective. Cent. Eur. J. Comput. Sci. 1(1):108\u2013116","journal-title":"Cent. Eur. J. Comput. Sci."},{"key":"178_CR41","unstructured":"SPEEDS (SPEculative and Exploratory Design in Systems Engineering). http:\/\/www.speeds.eu.com"},{"key":"178_CR42","unstructured":"Thrane C (2011) Quantitative models and analysis for reactive systems. PhD thesis, Aalborg University"},{"issue":"7","key":"178_CR43","doi-asserted-by":"crossref","first-page":"689","DOI":"10.1016\/j.jlap.2010.07.010","volume":"79","author":"C Thrane","year":"2010","unstructured":"Thrane C, Fahrenberg U, Larsen KG (2010) Quantitative simulations of weighted transition systems. J\u00a0Log Algebr Program 79(7):689\u2013703","journal-title":"J\u00a0Log Algebr Program"},{"key":"178_CR44","unstructured":"van Breugel F, (1994) Topological models in comparative semantics. PhD thesis, Vrije Universiteit, Amsterdam"},{"issue":"1","key":"178_CR45","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1111\/j.1749-6632.1996.tb49160.x","volume":"806","author":"F Breugel van","year":"1996","unstructured":"van Breugel F, (1996) A theory of metric labelled transition systems. Ann NY Acad Sci 806(1):69\u201387","journal-title":"Ann NY Acad Sci"},{"key":"178_CR46","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BFb0030814","volume-title":"COCOON","author":"U Zwick","year":"1995","unstructured":"Zwick U, Paterson M (1995) The complexity of mean payoff games. In: Du D-Z, Li M (eds) COCOON. Lecture notes in computer science, vol 959. Springer, Berlin, pp\u00a01\u201310"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0178-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0178-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0178-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,4]],"date-time":"2019-07-04T18:59:54Z","timestamp":1562266794000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0178-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,24]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["178"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0178-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,24]]}}}