Supervisory control with absent-state explanations for coloured finite automata

Nonblockingness in supervisory control synthesis guarantees that from every reachable state in the system, some marked (final) state is reachable. Situations, where nonblockingness of multiple sets of marked states (multiple tasks) is imposed, are common. Especially for composite systems, the marking of each subsystem usually has an individual meaning. To deal with these situations, multitasking supervisory control can be used. Currently, in multitasking supervisory control, there is no requirement-feedback when the synthesized supervisor shows unexpected or undesired behaviour (caused by wrong modelling of requirements for example). In this paper a framework is proposed to generate a cause for the absence of a state for multitasking supervisory control. In particular, we propose a pre-synthesis transformation that ensures that the influence of the requirements on the absence of a state is visible in the cause