Logic based abstractions of real-time systems