Embedding time granularity in a logical specification language for synchronous real-time systems