- Abstract:
-
In earlier work we gave a game-based semantics for checkonly QVT-R transformations. We restricted when/ and where/ clauses to be conjunctions of relation invocations only, and like the OMG standard, we did not consider cases in which a relation might (directly or indirectly) invoke itself recursively. In this paper we show how to interpret checkonly QVT-R -- or any future model transformation language structured similarly -- in the modal mu calculus and use its well-understood model-checking game to lift these restrictions. The interpretation via fixpoints gives a principled argument for assigning semantics to recursive transformations. We demonstrate that a particular class of recursive transformations must be ruled out due to monotonicity considerations. We demonstrate and justify a corresponding extension to the rules of the QVT-R game.
- Links To Paper
- 1st Link
- 2nd Link
- Bibtex format
- @Misc{EDI-INF-RR-1410,
- author = {
Julian Bradfield
and Perdita Stevens
},
- title = {Recursive checkonly QVT-R transformations with general when and where clauses via the modal mu calculus},
- year = 2012,
- url = {http://homepages.inf.ed.ac.uk/jcb/Research/fase2012.pdf},
- }
|
