Formula Based Abstractions of Transition Systems for Real-time Model Checking