Recursive Checkonly QVT-R Transformations with General when and where Clauses via the Modal Mu Calculus

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationFundamental Approaches to Software Engineering
Subtitle of host publication15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings
EditorsJuan de Lara, Andrea Zisman
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Print)978-3-642-28871-5
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Recursive Checkonly QVT-R Transformations with General when and where Clauses via the Modal Mu Calculus'. Together they form a unique fingerprint.

Cite this