The synthesis of controllers to handle safety, and liveness for timed discrete-event systems-an example in nuclear reactor systems

The paper is concerned with the synthesis of controllers for timed discrete-event systems to meet safety specifications and a liveness requirement (deadlock freedom). To tackle the intended control problems, we present a synthesis method employing a dynamic programming like technique together with an algorithm for ensuring deadlock avoidance. The method presented can handle the problems efficiently. In addition, a derived solution for a timed discrete-event system is appropriate to any situation under which the preset timeouts of some events in the original system are substituted by other adequate defaults. The method is applied to an example in nuclear reactor systems