摘要：AbstractGiven a plant and a specification, both represented as formal languages, the controllability prefix is defined as the set of event sequences from which on a supervisor can control the plant according to the specification. The controllability prefix was first introduced in the context of ω-languages, where it plays a crucial role in the solution of the supervisory controller synthesis problem. In the present paper, we address the controllability prefix for *-languages. In our discussion, we (a) present a novel characterisation of the supremal controllable and relatively closed sublanguage in terms of the controllability prefix; we (b) derive a fixpoint characterisation of winning states from a game theoretic interpretation of a specific state feedback synthesis problem; and (c) we establish a one-to-one correspondence between winning states and the controllability prefix. In summary, we obtain an efficient algorithm for the computation of the controllability prefix.
