{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T13:46:10Z","timestamp":1694612770649},"reference-count":18,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,6,26]],"date-time":"2014-06-26T00:00:00Z","timestamp":1403740800000},"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":[[2014,8]]},"abstract":"<jats:p>In model transformations, where source models are automatically translated into target models or code, termination is necessary for the transformation to be well defined. There are a number of specific termination criteria that can be used when specifying model transformations by graph transformation, though termination is undecidable in general. Unfortunately, and particularly for large and heterogeneous specifications, it is often not possible to use a single termination criterion. In this paper, we propose an approach that applies different criteria to suitable subsets of rules so that termination can be shown locally using the most suitable technique for each subset. Global termination then follows if certain causal dependencies between rules in different subsets are acyclic. The theory is developed at the level of typed attributed graphs, and is motivated and illustrated by a case study translating UML activity diagrams to CSP.<\/jats:p>","DOI":"10.1017\/s0960129512000369","type":"journal-article","created":{"date-parts":[[2014,6,26]],"date-time":"2014-06-26T14:22:13Z","timestamp":1403792533000},"source":"Crossref","is-referenced-by-count":1,"title":["Combining termination proofs in model transformation systems"],"prefix":"10.1017","volume":"24","author":[{"given":"D\u00c9NES","family":"BISZTRAY","sequence":"first","affiliation":[]},{"given":"REIKO","family":"HECKEL","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,6,26]]},"reference":[{"key":"S0960129512000369_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/11841883_19"},{"key":"S0960129512000369_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59071-4_45"},{"key":"S0960129512000369_ref15","doi-asserted-by":"crossref","first-page":"201","DOI":"10.3233\/FI-1998-33204","article-title":"Termination of graph rewriting is undecidable.","volume":"33","author":"Plump","year":"1998","journal-title":"Fundamenta Informaticae"},{"key":"S0960129512000369_ref14","unstructured":"OMG (2006) Unified Modeling Language, version 2.1.1. http:\/\/www.omg.org\/technology\/documents\/formal\/uml.htm."},{"key":"S0960129512000369_ref11","doi-asserted-by":"crossref","first-page":"287","DOI":"10.3233\/FI-1996-263404","article-title":"Graph grammars with negative application conditions","volume":"26","author":"Habel","year":"1996","journal-title":"Fundamenta Informaticae"},{"key":"S0960129512000369_ref12","volume-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"S0960129512000369_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89020-1_36"},{"key":"S0960129512000369_ref8","volume-title":"Fundamentals of Algebraic Graph Transformation","author":"Ehrig","year":"2006"},{"key":"S0960129512000369_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.04.019"},{"key":"S0960129512000369_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"S0960129512000369_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15928-2_16"},{"key":"S0960129512000369_ref10","volume-title":"Discrete and Combinatorial Mathematics: An Applied Introduction","author":"Grimaldi","year":"1998"},{"key":"S0960129512000369_ref3","unstructured":"Bisztray D. (2009) Compositional Verification of Model-Level Refactorings Based on Graph Transformations, Ph.D. thesis, Department of Computer Science, University of Leicester."},{"key":"S0960129512000369_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16145-2_9"},{"key":"S0960129512000369_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15928-2_14"},{"key":"S0960129512000369_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.048"},{"key":"S0960129512000369_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31984-9_5"},{"key":"S0960129512000369_ref9","doi-asserted-by":"publisher","DOI":"10.1142\/9789812815149_0014"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129512000369","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,21]],"date-time":"2020-08-21T11:26:40Z","timestamp":1598009200000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129512000369\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,26]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["S0960129512000369"],"URL":"https:\/\/doi.org\/10.1017\/s0960129512000369","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,6,26]]},"article-number":"240407"}}