Formula based abstractions of transition systems for real-time model checking