Model generation and minimal model generation are useful for tasks such as model checking, query answering and for debugging of logical specifications. Due to this variety of applications, several minimality criteria and model generation methods for classical logics have been studied. Minimal model generation for modal logics however did not receive the same attention from the research community.

This thesis aims to fill this gap by investigating minimality criteria and designing
minimal model generation procedures for all the sublogics of the multi-modal logic S5(m) and their extensions with universal modalities. All the procedures are minimal
model sound and complete, in the sense that they generate all and only minimal models.
The starting point of the investigation is the definition of a Herbrand semantics for
modal logics on which a syntactic minimality criterion is devised. The syntactic nature
of the minimality criterion allows for an efficient minimal model generation procedure,
but, on the other hand, the resulting minimal models can be redundant or semantically
non minimal with respect to each other.

To overcome the syntactic limitations of the first minimality criterion, the thesis
moves from minimal modal Herbrand models to semantic minimality criteria based on subset-simulation. At first, theoretical procedures for the generation of models minimal modulo subset-simulation are presented. These procedures for the generation of models minimal modulo subset-simulation are minimal model sound and complete, but they might not terminate. The minimality criterion and the procedures are then refined in such a way that termination can be ensured while preserving minimal model soundness and completeness.