We consider here forbidden state specifications and special cases of
sequential specifications. Forbidden states in the NCES framework are
modeled by means of facts, which are a special class of
transitions that must be dead in the controlled system. It is known
that any Boolean expression over the marking of a safe net can be
represented by facts, and that each fact can be transformed into
facts which have only input places by adding complementary
places [4]. Figure 15 in Section 6.4
shows fact f for the forbidden state in which both pushers are in
their extended position. Thus, the specification model is adjoined to
the plant model by means of the new transitions (facts) and their
respective arcs. In the next section we describe the procedure for
obtaining the safety controller which is to impose these facts.
Forbidden and desired paths, or sequences of events, are types
of sequential specifications. With NCES, we can easily transform
forbidden path specifications to forbidden state specifications.
Suppose that we have a forbidden sequence of events defined by 
,
, ..., 
. We can construct a new module by creating a
simple Petri Net path using a copy of each of the events 
, call
them 
. See Figure 4 for an illustration.
Then, an event arc is added from to , and the last place
in this path - which indicates the completion of the forbidden path
- enables a fact f. The specification model for the forbidden path
can be thought of as an ``observer'' because the event arcs tell us when an
event in the path has occurred. This observer, as we will see in the
next section, will become the controller that is to ensure the
forbidden path is never completed.
Figure 4: Specification Model for Forbidden Paths
Notice that the above model accounts for the case when part of the the
forbidden path has been completed, and then a transition fires which
is not part of the forbidden path. In this case, the token from the
appropriate place in the forbidden path specification must be removed,
and so we will need copies of all transitions in the model which are
enabled if a transition is enabled. These ``copies'' are
triggered via event signals from the original plant transitions, as
illustrated in Figure 4. The set 
consists
of all those transitions that are enabled when is enabled.
Some work has also been done for desired paths based on NCES (see
[21]). In this framework, the desired behavior is a
sequence of transition firings that moves a token from an input place
to an output place. Although interim places may be specified, this is
not required as the algorithm synthesizing the sequential controller
finds a path by itself. In this case, however, we do not have an
``observer'' module since, instead of ``watching out'' for forbidden
behavior, we are trying to ``drive'' the system to accomplish a
certain task. A brief description of the algorithm for the sequential
controller is given in our next section.