Symbolic Model Checking for Timed Petri Nets