Terminology overview
The terminology below applies to supervisory controller synthesis,
and is used frequently in the documentation. Both event-based and data-based
synthesis terminology is included. The descriptions are informative only. For
formal definitions, we refer to the theory of supervisory control synthesis.
The terms are listed in alphabetical order. The following purely event-based
CIF 3 model serves as an example, and is shown both graphically and textually:
|
plant Button:
uncontrollable u_pushed, u_released;
location Released:
initial; marked;
edge u_pushed goto Pushed;
location Pushed:
edge u_released goto Released;
end
plant Lamp:
controllable c_on, c_off;
location Off:
initial; marked;
edge c_on goto On;
location On:
edge c_off goto Off;
end
requirement LampOnWhileButtonPushed:
location Released:
initial; marked;
edge Button.u_pushed goto Pushed;
edge Lamp.c_off;
location Pushed:
edge Button.u_released goto Released;
edge Lamp.c_on;
end
|
|
|
- Active location
- The active location of an
automaton, or
state of an automaton is the
current location in which the automaton resides. Initially, the
initial location of an automaton
is also its active location. The active location can change as a result of
taking edges, when
events occur.
- Alphabet
The alphabet of an automaton is the
finite set of events over which it
synchronizes. The alphabet consists
of at least the events that occur on the
edges of the automaton (excluding
sends/receives). If the alphabet contains events that are not on any of the
edges of that automaton, then the automaton never
enables that event, thus
disabling it within the automaton, and thus globally.
In CIF, if the alphabet of an automaton is not specified, it defaults to the
events that occur on the edges of the automaton (excluding sends/receives).
Note that it does not matter where events are declared, as that has no effect
on the alphabet of the automata. That is, only the events that occur on the
edges affect the default alphabet, regardless of where those events are
declared.
The alphabet of the entire system consists of all the events of the alphabets
of all its automata.
In the example above, the alphabet of automaton Button consists of the
events u_pushed and u_released, the alphabet of automaton Lamp
consists of the events c_on and c_off, and the alphabet of automaton
LampOnWhileButtonPushed consists of events u_pushed and
u_released from automaton Button and events c_on and c_off
from automaton Lamp.
- Automaton
- An automaton (plural: automata) is a
model of discrete behavior, also
known as a finite state machine. Automata consist of
locations and
edges. In the example above,
Button and Lamp are
plant automata, while
LampOnWhileButtonPushed is a
requirement automaton.
- Component
- A component is a part of the system, or
controller. Since the system itself
can be controlled by a higher-level controller, the entire system is a
considered a component as well. That is, a component may be an individual
sensor or actuator, a part of a machine, a entire machine, or even a factory.
A component is usually modeled as
an automaton or a group of automata.
- Controllable event
- A controllable event is an event
that is initiated by the
controller/supervisor. For low-level
controllers, controllable events map directly to actuators. For instance, if
a lamp could be turned on or off, the ‘on’ and ‘off’ events would be
controllable. Controllable events in CIF are usually prefixed with c_.
In the example above, events c_on and c_off of
plant automaton Lamp are
controllable events.
- Data-based synthesis
- Data-based synthesis is
supervisory control synthesis
using the data-based synthesis tool. It supports a
relatively rich subset of CIF models, including those with
variables,
guards,
updates,
invariants, etc.
- Edge
- An edge represents the possibility for an
event to occur, possibly resulting
in a state change. In the example
above, automaton
LampOnWhileButtonPushed has a
location named Released. This
location has two edges. The first edge has an
edge label for event
u_pushed of automaton Button, and when the event occurs the
active location changes from
Released (the source location) to Pushed (the target location).
The second edge is a self loop,
for event c_off from automaton Lamp, and when the event occurs the
active location remains the same.
- Edge labeling
- Edges can be labeled with
events. That is, the events that
occur on an edge may be referred to as the labels of the edge. The events
that occur on the edge indicate that one of those events must occur, in order
for the edge to be enabled, so
that it may be taken. If an edge is labeled with multiple events, this is
equivalent to having multiple events (with the same source and target
locations, guards, and
updates, as the original edge), each
with a single event (from the original labeling).
- Enabledness
An event is enabled in a system, if
it is enabled in all automata of that
system. If an automaton does not have a certain event in its
alphabet, the automaton does not
restrict the event, and the automaton thus always enables that event. If an
automaton does have an event in its alphabet, the automaton only enables
(allows) the event if there is an outgoing edge from its
active location. If the edge has
a guard, the guard must hold for the
edge to enable the event.
In the example above, event u_on of automaton Lamp is in the alphabet
of automata Lamp and LampOnWhileButtonPushed. It is not restricted
by automaton Button. The event is only enabled if automaton Lamp is
in location Off, and automaton LampOnWhileButtonPushed is in location
Pushed, as those two location have outgoing edges for that event.
- Event
- An event represents behavior of a system. Whenever an event occurs, something
happens in the system, usually resulting in a
state change. There are two
types of events, controllable
events and uncontrollable
events. In the example above, u_pushed and u_released are declared as
uncontrollable events in automaton
Button. They also appear on the
edges, as
edge labels.
- Event-based synthesis
- Event-based synthesis is
supervisory control synthesis
using the event-based synthesis toolset. It
is a very basic form of synthesis, and doesn’t support
variables,
guards,
updates,
invariants, etc.
- Guard
- An edge can optionally have a guard
property, usually simply called a
guard. If an edge has a guard, the property must hold and the source
location of the edge must be the
active location of the
automaton, for the
event on the edge to be
enabled by the edge. That is, the
edge can only be taken if the guard holds.
- Initial location
- The initial location of an
automaton, is its first
active location or
state. When the system starts, it
begins in the initial state, possibly after an initialization procedure, if
that is not explicitly modeled. In the example above, the initial location
of automaton Button is location Released.
- Invariant
- There are two types of invariants: state (exclusion) invariants, and
state/event exclusion invariants. State invariants are
properties that must hold in all
states, thereby disabling states
that don’t satisfy the properties. State/event exclusion invariants can be
used to disable certain events in certain states.
- Location
- A location of an automaton
represents a possible state of the
automaton. Of all the locations of an automaton, only one can be
active at any time. In the
example above, Released and Pushed are the locations of automaton
Button. A location may optionally be
initial and
marked.
- Marked location
- A marked location is a location that
is defined as being marked. In the example above, the Released location
of automaton Button is marked.
Marked locations play an important role in
marking, which is used to ensure
progress, and prevent livelocks.
- Marking
- Marking is very weak form of liveness, and is used to prevent livelocks, to
ensure progress. A supervisor per
definition ensures that a marked
state can always be reached, for
the entire system. A system is marked if all its
automata are marked. An automaton is
marked if its active location
is a marked location.
- Model
A model is a representation of something real/physical. Models are
abstractions, in the sense they usually contain just enough details of
reality to express the desired behavior or properties. The irrelevant details
are left out.
Factories may consist of machines, machines may consist of parts, and those
parts may again consist of smaller parts, etc. We usually consider the
individual actuators and sensors as the lowest level, but theoretically there
is no reason we can’t model anything smaller, such as the individual atoms.
Each of these physical entities can be modeled. The entirety of what is
modeled (the system) is usually called the model. Each CIF 3 file
represents such a model of a (sub-)system. CIF 3 files consist mainly of
automata, which model the smaller
parts of the system.
- Monolithic, modular, and distributed supervisory control
- Traditional supervisory control synthesis results in a single
supervisor. A single supervisor that
controls the system is called a monolithic supervisor, and the synthesis
approach is referred to as monolithic supervisory control. It is the
simplest and most basic form of supervisor synthesis. For larger systems
however, this approach suffers from
state space explosions, making it
practically infeasible. Alternatives include modular supervisory control
and distributed supervisory control, both of which exist in several
variants. These different forms of synthesis are available regardless of the
synthesis algorithm that is used.
- Plant
- The plant is the physical system ‘as is’, with or without any integrated
control, to which additional (higher-level) control is to be added. The plant
is also called the uncontrolled system. It describes the capabilities or
behavior of the system, if no additional control were to be added. The plant
is modeled using
plant automata.
- Plant automaton
- A plant automaton is an automaton
that models the behavior of (a
part of) the plant. If
supervisory control is used for
low-level control, a single plant automaton could represent a single sensor
or actuator. If however supervisory control is used for higher-level control,
a single plant could represent a part of a machine, an entire machine, or
even an entire factory. Plant automata are also called plants. In the
example above, Button and Lamp are plant automata.
- Property
- A property or predicate is a statement over the
state of the system that either holds
or doesn’t hold in a current state. If the property holds, it is also said to
be satisfied. If it doesn’t hold, it is also said to be violated. An example
of a property can be that an automaton
has a certain active location or
a variable has a certain
value. Combinations of property are
possible, for instance that two properties must both hold, or that only one
of them needs to hold.
- Requirement
- A requirement models (a part of) the
functions a system is supposed to perform. It represents behavior that is
allowed in the controlled system, or more precisely, it represents the
behavior that is not allowed in the controlled system. Multiple
requirements may be defined that together restricts the behavior of the
plant, to ensure that only the
desired behavior remains. Requirements are modeled as either
requirement automata or
requirement invariants.
- Requirement automaton
- A requirement automaton is a
requirement
modeled as an
automaton. A requirement automaton
synchronizes with the
plant automata, restricting their
behavior. In the example above, LampOnWhileButtonPushed is a requirement
automaton.
- Requirement invariant
- A requirement invariant is a
requirement
modeled as an
invariant. A requirement state
(exclusion) invariant specifies a
property that must hold in all
states. The
synthesized
supervisor will prevent that the system
ends up in a state that violates a state invariant. A requirement state/event
exclusion invariant can be used to disable certain events in certain states.
The synthesized supervisor will ensure the events are actually disabled.
- Self loop
- A self loop is an edge that has the
same source location and target
location. When the event of such
an edge occurs, the
active location of the
automaton does not change as a result
of taking that edge. In the example above, automaton
LampOnWhileButtonPushed has two self loops, one in each of the two
locations.
- State
- The state of an automaton is the
active or current
location of the automaton. The state
of an entire system is the collection of active states of the automata
that are part of the system, and the current
values of all the
variables of the system. As the active
locations and values of the variables change, the state of the system changes
as well. The state space consists
of all the states of the system.
- Supervisor
A supervisor is an automaton that
represents a controller. It is usually synthesized from the
plants and
requirements, using
supervisory control synthesis
tooling. It is possible to synthesize a single supervisor to control the
system, by using monolithic
supervisory control. It is however also possible to synthesize multiple
supervisors to control a system, using for instance
modular supervisory control or
distributed supervisory control.
A supervisor, per definition, is correct, non-blocking, and optimal. Correct
means that it satisfies the requirements, and forces the system to behave
according to the behavior as defined by those requirements. Non-blocking
means that it is free of deadlocks (states in which no
transitions are possible).
Optimal, or maximally permissive, means that a supervisor does not restrict
more of the system behavior than necessary. Progress is ensured through
marking.
- Supervisory control synthesis
- Synthesis, ‘supervisor synthesis’, or ‘supervisory controller synthesis’, is
a generative technique, where one derives a
(supervisor)
automaton from a collection of
plants and
requirements. The resulting
supervisor satisfies various useful properties. Multiple synthesis
algorithms exist.
- Synchronization
- Events are synchronized over the
entire system. That is, an event is only
enabled if all
automata allow the event. If an event
is enabled, an it occurs, all automata simultaneously take their associated
edges (if they have the event in
their alphabet), and update
their state to the target
locations of those edges. They also perform any
updates of those edges. In the
example above, event u_pushed of automaton Button is used in
automaton Button as well as in automaton LampOnWhileButtonPushed, but
not in automaton Lamp.
- Synthesis algorithm
- Several different supervisory controller synthesis algorithms exist. The different
algorithms can each be used to synthesize a
supervisor from
plants and
requirements. The main differences are
the features of the CIF language that are supported by the different
algorithms, and the performance of the algorithms. This part of the CIF 3
documentation applies to both
event-based synthesis and
data-based synthesis.
- Transition
A transition is a concrete occurrence of an
event. By taking a transition,
at the occurrence of the event, when it is
enabled, all
automata that
synchronize over the event take
their corresponding edges, and
update their state accordingly.
In the example above, event c_on of automaton Lamp is only enabled
if automaton Lamp is in location Off, and automaton
LampOnWhileButtonPushed is in location Pushed. When those two
automata have the indicated locations as their
active locations, the
result of taking the transition for event c_on is that automaton Lamp
will have location On as its active location, and automaton
LampOnWhileButtonPushed will remain in location Pushed, as its
edge with event c_on is a
self loop.
- Uncontrollable event
- A uncontrollable event is an event
that is not initiated by the
controller/supervisor. For low-level
controllers, uncontrollable events map directly to sensors. Uncontrollable
events in CIF are usually prefixed with u_. For instance, in the example
above, the button can be pushed or released. The u_pushed and
u_released events of
plant automaton Button are
uncontrollable events.
- Update
- The update of an edge indicates how to
change or update the values of
variables when the edge is taken. The
updates of an edge usually consist of assignments, that indicate the new
values of one or more variables. For instance, x := 1 gives variable
x value 1.
- Variable
- A variable can store a value. A
variable with several potential values can be seen as the dual of an
automaton with several potential
locations.
- Value
- A variable can store a value. In other
words, one of the possible values of a variable is stored. For instance, a
variable could have an integer value, e.g. 1, 2, 3, etc.
