Deducing causes for the absence of states in supervised systems

A shortcoming of state-of-the-art synthesis algorithms is the lack of feedback to the user in case a supervisor cannot be synthesized or in case the supervisor is not according the expectations of the user. We present a collection of deduction rules that allow to derive reasons for the absence of a state in a supervised system and provide feedback to users. It is shown that all states for which a cause can be derived are actually omitted by synthesis and that for each omitted state a cause can be derived. An adaptation of a standard synthesis algorithm is provided that allows to automatically obtain a cause for each state that is omitted from a plant during synthesis.