Temporal Logics for Real-Time System Specication