Verifying Temporal Properties of Systems