Realizations and witnesses for Kripke models.