Modal logic over finite structures

We investigate properties of prepositional modal logic over the class of finite structures. In particular, we show that certain known preservation theorems remain true over this class. We prove that a class of finite models is defined by a first-order sentence and closed under bisimulations if and only if it is definable by a modal formula. We also prove that a class of finite models defined by a modal formula is closed under extensions if and only if it is defined by a ◇-modal formula. © 1997 Kluwer Academic Publishers.