μ-chart-based specification and refinement

We introduce two new notions of refinement for mu-charts and compare them with the existing notion due to Scholz. The two notions are interesting and important because one gives rise (via a logic) to a calculus for constructing refinements and the other gives rise (via model checking) to a way of checking that refinements hold. Thus we bring together the two competing worlds of model checking and proof.