Using Model Checking to Guarantee Safety in Automatically-Synthesized Real-Time Controllers