Temporal logic specifications are the subject of quiz 9. Much as in the homework, you should be able to encode relatively simple English-language constraints in CTL.