摘要:AbstractAutomated systems require controllers which guarantee machine safety and specified functionality even in case of occurring defects. In literature, several methods can be found for formally deriving a supervisor providing such guarantees, including the existence of failure recovery. In this paper, an extension is proposed so that the derived supervisor not only guarantees the existence of failure recovery, but also enforces a shortest path for it. To this end, a two-step procedure is defined for supervisor derivation, in which two algorithms are involved.