{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T16:30:30Z","timestamp":1774801830234,"version":"3.50.1"},"reference-count":47,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2012,5,8]],"date-time":"2012-05-08T00:00:00Z","timestamp":1336435200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2012,8]]},"abstract":"<jats:p>We introduce a novel formalism of label-structured modal transition systems that combines the classical may\/must modalities on transitions with structured labels that represent quantitative aspects of the model. On the one hand, the specification formalism is general enough to include models like weighted modal transition systems and allows system developers to employ more complex label refinement than in previously studied theories. On the other hand, the formalism maintains the desirable properties required by any specification theory supporting compositional reasoning. In particular, we study modal and thorough refinement, determinisation, parallel composition, conjunction, quotient and logical characterisation of label-structured modal transition systems.<\/jats:p>","DOI":"10.1017\/s0960129511000697","type":"journal-article","created":{"date-parts":[[2012,5,8]],"date-time":"2012-05-08T06:12:02Z","timestamp":1336457522000},"page":"581-617","source":"Crossref","is-referenced-by-count":17,"title":["Extending modal transition systems with structured labels"],"prefix":"10.1017","volume":"22","author":[{"given":"SEBASTIAN S.","family":"BAUER","sequence":"first","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":"JI\u0158\u00cd","family":"SRBA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2012,5,8]]},"reference":[{"key":"S0960129511000697_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-006-0008-6"},{"key":"S0960129511000697_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_23"},{"key":"S0960129511000697_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1147249.1147254"},{"key":"S0960129511000697_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015763"},{"key":"S0960129511000697_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45828-X_9"},{"key":"S0960129511000697_ref12","first-page":"109","volume-title":"Proceedings of the 8th ESEC and 9th ACM SIGSOFT FSE","author":"de Alfaro","year":"2001"},{"key":"S0960129511000697_ref11","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1145\/1755952.1755967","volume-title":"HSCC","author":"David","year":"2010"},{"key":"S0960129511000697_ref26","unstructured":"Juhl L. , Larsen K. G. and Srba J. (2010) Modal Transition Systems with Weight Intervals."},{"key":"S0960129511000697_ref46","volume-title":"Denotational Semantics: The Scott\u2013Strachey Approach to Progamming Language Theory","author":"Stoy","year":"1977"},{"key":"S0960129511000697_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_35"},{"key":"S0960129511000697_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.009"},{"key":"S0960129511000697_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"S0960129511000697_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03466-4_7"},{"key":"S0960129511000697_ref10","first-page":"123","volume-title":"Proceedings of 7th International Conference on Quantitative Evaluation of SysTems (QEST)","author":"Caillaud","year":"2010"},{"key":"S0960129511000697_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.004"},{"key":"S0960129511000697_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90007-7"},{"key":"S0960129511000697_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18088-5_11"},{"key":"S0960129511000697_ref17","unstructured":"Delahaye B. , Larsen K. , Legay A. and Wasowski A. (2010) On greatest lower bound of modal transition systems. Technical report, INRIA."},{"key":"S0960129511000697_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_14"},{"key":"S0960129511000697_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90276-L"},{"key":"S0960129511000697_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017309"},{"key":"S0960129511000697_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44685-0_29"},{"key":"S0960129511000697_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_6"},{"key":"S0960129511000697_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-3532-2_3"},{"key":"S0960129511000697_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00982-2_13"},{"key":"S0960129511000697_ref34","first-page":"203","volume-title":"LICS","author":"Larsen","year":"1988"},{"key":"S0960129511000697_ref42","unstructured":"Plotkin G. (1981) A structural approach to operational semantics. FN 19, DAIMI. Computer Science Department, Aarhus University, Denmark."},{"key":"S0960129511000697_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039066"},{"key":"S0960129511000697_ref22","first-page":"203","volume-title":"SPLC","author":"Gruler","year":"2008"},{"key":"S0960129511000697_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_15"},{"key":"S0960129511000697_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/337244.337261"},{"key":"S0960129511000697_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"S0960129511000697_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"S0960129511000697_ref25","volume-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"S0960129511000697_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52148-8_19"},{"key":"S0960129511000697_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90025-B"},{"key":"S0960129511000697_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017164"},{"key":"S0960129511000697_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31984-9_13"},{"key":"S0960129511000697_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31848-4_6"},{"key":"S0960129511000697_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"S0960129511000697_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.023"},{"key":"S0960129511000697_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04368-0_16"},{"key":"S0960129511000697_ref44","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90012-0"},{"key":"S0960129511000697_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52148-8_14"},{"key":"S0960129511000697_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-6228-2"},{"key":"S0960129511000697_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_8"},{"key":"S0960129511000697_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/11559306_5"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129511000697","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,25]],"date-time":"2019-04-25T15:01:28Z","timestamp":1556204488000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129511000697\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5,8]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["S0960129511000697"],"URL":"https:\/\/doi.org\/10.1017\/s0960129511000697","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,5,8]]}}}