CIF 3

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:

../../_images/terminology_graphical.png
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.