Minimal refinements of specifications in modal and temporal logics

Minimal refinement, a method for changing a given model so that the result refines it minimally while satisfying a new requirement, can allow a designer to obtain a revised design out of an old one and a new requirement. Minimal refinement has been studied under various frameworks including modal logic, where minimal refinement was studied over the class of m-saturated models with sets of sentences as the requirements, and minimal refinement over transition systems with fairness constraints with formulae of ACTL as requirements. Minimal refinement over finite structure has also been studied, in modal logic, with modal formulae as requirements. For the temporal logics, it would desirable to extend the set of results to languages that are not universally quantified and therefore are not preserved by refinement.