Recursive checkonly QVT-R transformations with general when and where clauses via the modal Mu calculus

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. © 2012 Springer-Verlag Berlin Heidelberg.