 Formulas in basic propositional modal language are built from Atoms, classical connectives and modal operators, \(\square\) (box) and \(\Diamond\) (diamond). Modal formulas are interpreted in Kripke structures