In general, two different classes of specifications are considered:
safety specifications and sequential specifications.
Safety specifications normally refer to forbidden states, whereas
sequential specifications refer to desired or forbidden event
sequences. With R&W, both types of specifications can be used for
purposes of control synthesis. We should remark, however, that
creating the state machines describing specifications need not be a
trivial or intuitive task. Desired paths are usually easy to specify,
but we must keep in mind that there may be other paths that accomplish
the same task. For instance, in our Two-Pusher Example, we have
specified
as the desired sequence of events to move the
workpiece to position 3. Notice that in this sequence, pusher 2 is
not allowed to move until the workpiece has reached position 2. But
this is clearly not the only way to achieve our goal. We could allow,
for example, pusher 2 to move to its middle position and then back to
its initial position, and then follow the path in
. This
might be considered unnecessary work for pusher 2, but the point we
wish to make is that, when specifying the sequence of events to
accomplish a task, care must be taken not to restrict the system
behavior more than necessary by only considering some of the possible
paths. Expressing forbidden paths in the R&W framework can be even
more difficult, since the specification model is to be the
recognizer for desired behavior. In the case of a forbidden
path specification, we would have to have to consider the
``complementary'' desired paths, and then describe them using state
machines.
Because of the expressive power of Temporal Logic, any kind of
specification can be described in Ostroff's TTM framework.
However, unlike the case of R&W and NCES, this specification language
is not directly used in the synthesis procedure of the controller. Also,
as explained earlier, the controller synthesis procedure in this
case only handles safety specifications. With Petri Nets, the common
specifications used for control synthesis are those related to
markings (i.e. safety specifications). However, we cannot describe
sequential specifications, in general, in terms of marking
constraints. (See the Petri Net model of the Three-Machine Example in
Section 8.3.) But we are not aware of formal methods based on Petri
Nets to describe general sequential specifications.
With NCES, safety specifications are easily described by means of
facts. Forbidden paths can also be described in a straight forward
manner by forbidding the state which indicates the path
completion. In either case, the specification model is also a net
structure which is composed with the plant model, by means of the event
and condition signals, for purposes of controller synthesis. In this
sense, the modeling framework is similar to that of R&W. However, the
interpretation of the composition of P and
are quite
different: in R&W, the intersection of the plant and specification
models gives us all of the events that will be allowed - the legal
language - whereas the specification model in NCES acts as an
``observer'' of only those events that are constrained by the
specifications.