Model Transformation has become central to most software engineering activities. It
refers to the process of modifying a (usually graphical) model for the purpose of
analysis (by its transformation to some other domain), optimization, evolution, migration
or even code generation. In this work, we show termination criteria for model transformation
based on graph transformation. This framework offers visual and formal techniques
based on rules, in such a way that model transformations can be subject to analysis.
Previous results on graph transformation are extended by proving the termination of
a transformation if the rules applied meet certain criteria. We show the suitability
of the approach by an example in which we translate a simplified version of Statecharts
into Petri nets for functional correctness analysis.