Verifying Temporal Properties in GRAFCET