Supervisory Control - The Unknown Component Problem: Theory and Applications - page 236

15.2.1.2 Equation Solving Approach

When casting the supervisory control problem as solving a language equation, the
language equation

P \ X D S h as to be solved. If the equation is solvable then

there exists the lar ge st solution P [ S . The equation is solvable if and only if the

composition P \ .P [ S/ of the plant and of the largest solution is equal to S .The

latter happens if and only if . If the language of

the largest controlle r i s not prefix-closed , w e extract the largest prefix-closed subset
contained in the set

P \ S D S , i.e., if and only if S P

.P [ S/ Pref .

P [ S , denoted by

Proposition 15.3. There exists a solution of the equation P \ X D S if and only

if S P . If the equation P \ X D S is solvable then each prefix-closed language

L such that S L P [ S is a controller solution of the language equation

P \ X D S .

If the e quation is not solvable then the supremal controllable sublanguage of S

is P \ .P [ S/ , i.e., it is P \ S .

15.2.2 General Case: S and P Not Prefix-Closed

Consider the general case when P and S are not required to be prefix-closed

languages. Given a language S , we denote by Pref .S / the prefix closure of S ,and

Pref

by S the largest prefix-closed sublanguage of S .

15.2.2.1 Supervisory Control Approach

In supervisory control (with full controllability and observability) solvability is
equivalent to the fact that Pref .S / is a solution.

P \ X D S

Theorem 15.4. A solution of the supervisory control problem exists if

P \ Pref .S / D S

and only if .

P \ Pref .S / D S

Proof. If If then by definition the controller C given by Pref .S /

is a solution because Pref .S / is prefix-closed.

Only if We must prove that if there is a controller C then P \ Pref .S / D S .

Suppose by contradiction that P \ Pref .S / ¤ S , then it must be P \ Pref .S /

S (because for a solution to exist it must be S P and so it cannot be P \

Pref .S / S , given that Pref .S / S ),andsotheremustbeastring ˛ 2 P \

Pref .S / , ˛ 62 S . Then there must be a string ˇ ¤ such that D ˛ˇ 2 S , because

˛ 2 Pref .S / and so it can be extended to 2 S .Since C is a controller and so