In a tutorial style I would like to present the theory of two important temporal logics (CTL and LTL) and show how they can be efficiently implemented using BDDs.
