Signal Temporal Logic