Synthesis

This plug-in provides functions related to controllability and normality of formal languages. The latter properties play a key role in the control of discrete event systems; see [S1] and [S2]. On this page, we give a pragmatic introduction by a simple example. Further details are organized as follows:



Copyright (C) 2006, Bernd Opitz.
Copyright (C) 2008, 2009 Thomas Moor, Klaus Schmidt, Sebastian Perk.
Copyright (C) 2010 - 2013 Thomas Moor.

Plant Model

For our example, we consider two very simple machines M1 and M2. Each machine can process one workpiece at a time. Per machine, our model distinguishes the two events alpha_* and beta_* to indicate the beginning and the end of processing a workpiece. Furthermore, we assume that the machines never fail, i.e. once the process is started, it is guaranteed to end within finite time.

The machines are modelled by the below Generators G1 and G2, respectively. The states I and B refer to the machine being idle or busy. The overall plant model is constructed as the shuffle product of both components, which is computed by the function Parallel.

Plant Component G1 Plant Component G2
Plant GPlant =G1 || G2

Note: in using Parallel for system composition, the overall plant model marks states that correspond to a simultanous marking of the components. Thus, we interpret the marking as a requirement to the legal operation of our two machines rather than a property of our plant configuration; see also OmegaParallel for an alternative approach.

Specification

While the plant model generates all strings that the plant can possibly exhibit, the specification model is meant to generate all strings that are acceptable.

In our sceneraio, the two machines shall be arranged with a buffer B to implement a two-stage production process. Each workpiece must first be processed by M1, then placed in the buffer B, and finaly processed by M2. The buffer capcity is restricet to one workpiece. While by our plant model both machines act independantly, the buffer imposes a condition regarding the interaction of both machines. We model the buffer as our specification, where the event beta_1 fills the buffer and alpha_2 empties the buffer.

Specification GSpec

The above specification is given for an alphabet which is a strict subset of the plant alphabet. Thus, events that are not specified may occur at any time. To restate the specifcation for the full alphabet, one may use an inverse projection or a self-loop operatiorn (see InvProject and SelfLoop).

Controllability and the Closed-Loop Configuration

For the closed loop, we consider all plant events to be synchronized with jet another generator, the supervisor. Our interpretation of this configuration is that at any instance of time the supervisor only allows those events to occur that are enabled in its current state. However, it is quite restrictive to assume that any event can be prevented. Therefore, the overall alphabet Sigma is decomposed in two disjoint subsets of controllable events Sigma_c and uncontrollable events Sigma_uc. At any instance of time, the supervisor is required to allow all uncontrollable events that are enabled in the plant.

For our scenario, we consider the alpha_* events to be controllable, i.e. a supervisor may decide not to start a process. In contrast, once the process has been started the subsequent beta_* event cannot be prevented. Hence, beta_* events are considered uncontrollable.

The task is to find a supervisor that
(1)  never prevents uncontrollable events, and
(2)  enforces the closed-loop to evolve within the specified behaviour.

In terms of the generated languages, condition (1) corresponds to the controllabilty condition proposed by P.J. Ramadge and W.M. Wonham, while (2) amounts to a language inclusion. The key observation is that the set of all closed-loop behaviours with supervisors that fulfill both conditions exhibits a unique supremal element (a largest language). This supremal element itself can serve as a supervisor: when run in parallel to the plant, it fulfills conditions (1) and (2) while imposing as little restriction to the plant behaviour as possible.

A realisation of the least restrictive supervisor can be computed by the function SupConNB (or SupCon when only the generated languages are to be considered and the marking is to be ignored). In our example, we obtain the below supervisor K.

Supervisor GSupervisor

Note that, if the machine M2 is still busy and the buffer is full (state I|B|F) the supervisor will prevent that machine M1 takes up a workpiece. If the supervisor did not prevent M1 from takeng up a workpiece in state I|B|F, it could happen, that M1 finishes processing before M2 and, hence, a buffer overflow would occur.

Literature

[S1] P.J. Ramadge and W.M. Wonham: The Control of discrete event systems, Proceedings of the IEEE, vol 77, issue 1, pp. 81-98, 1989.

[S2] R.D. Brandt, V. Garg, R. Kumar, F. Lin, S.I. Marcus, W.M. Wonham: Formulas for Calculating Supremal Controllable and Normal Sublanguages, System & Control Letters, vol 15, no 2, pp. 111-117, 1990.

[S3] P.J. Ramadge: Some tractable supervisory control problems for discrete-event systems modeled by Buchi automata, IEEE Transactions on Automatic Control, vol 34, no 1, pp. 10-19, 1989.

[S4] R. Kumar, V. Garg, S.I. Marcus: On supervisory control of sequential behaviors, IEEE Transactions on Automatic Control, vol 37, no 12, pp. 1978-1985, 1992.

[S5] J.G. Thistle, W.M. Wonham: Supervision of Infinite Behavior of Discrete-Event Systems, SIAM Journal on Control and Optimization, vol 32, no, 4, pp. 1098 - 1113, 1994.

[S6] R. Su, W.M. Wonham: Supervisor Reduction for Discrete-Event Systems, Discrete Event Dynamic Systems, vol. 14, no. 1, 2004.

[S7] T. Moor, Ch. Baier,T.-S. Yoo, F. Lin, S. Lafortune: On the Computation of Supremal Sublanguages Relevant to Supervisory Control, Workshop on Discrete Event Systems (WODES), 2012.

[S8] T.-S. Yoo, S. Lafortune: Solvability of Centralized Supervisory Control Under Partial Observation, Discrete Event Dynamic Systems, vol. 16, 2006.

[S9] R.M. Ziller, J.E.R. Cury: On the Supremal Lm-closed and the Supremal Lm-closed and L-controllable Sublanguages of a Given Language, Lecture Notes in Control and Information Sciences 199, Springer-Verlag, pp. 80-85, 1994.

[S10] T. Moor: Natural projections for the synthesis of non-conflicting supervisory controllers, Workshop on Discrete Event Systems (WODES), 2014.

libFAUDES 2.32b --- 2024.03.08 --- with "synthesis-observer-diagnosis-iosystem-hiosys-multitasking-coordinationcontrol-timed-iodevice-simulator-luabindings"

>>