L08: Model checking examples