A logical characterization of timed regular languages