Bounded Model Checking for Timed Systems