A two-part lecture that introduces temporal formulas and explains what it means for one specification to implement another.

…