 Dynamic Logics (DL) are modal logics for representing the states and the events of dynamic systems. The language of DLs is both an assertion language able to express properties of computation states, and a programming language able to express properties of system transitions between these states. DLs are logics of programs, and permit to talk and reason about states of affairs, processes, changes, and results. 