Progress verification for embedded systems

In many contexts it is important that a given embedded system will eventually reach a certain goal (e.g., the goal that a train eventually stops when the brakes are switched on). The thesis will involve the design and implementation of an algorithm for verifying that such a goal will eventually be reached.