A Description and Reasoning of Plant Controllers in Temporal Logic

1. Eventuality

Eventuality is a requirement that the control should realize a desirable state sometime in future, so that the eventuality corresponds to the transient behavior in system thoery. This is represented by

Initial condition :J o(the final &tate)

2. Stability

Stability requires the system to keep some state- forever after the state is attained. Namely, stability is formulated as

Usually eventuality and stability are used together in the following way :

Initial condition :J oo(the final ~tate) .

3. Observability

Observability means a requirement that the value of a state of the controlled system can be known to the controller in the allowable delay. Namely, for every state E of the controlled system, there exists a state F of the controller such that

where a is any state value and R is a condition of delay.

A state of the controlled system may be known to the controller before it is reached. This condition is represented as

o[(F =a) :J (·R U (E =a) 1\ o(E =a))] where E is a Jtate of the controlled system. The observability of the state E is the essential requirement if E is a state to be controlled.

Ill. REASONING METHOD

A. An w - graph

In order to reason about the system represented in TL, we construct its model by making a graph calleq ·w- graph · which is essentially based upon the tableau method [2]. First, for a temporal formula F, we decompose F into the part of present instant and the rest. The decomposition rules are as follows :

Note that the above rule for oF contains a term (oF, F). We call such terms "marked formulas· and we put this mark in order to express the eventuality property that F will be fulfilled in future.

An w -graph is a graphical representation of the model of a temporal formula whose nodes are corresponding to formulas and whose edges are labeled literals (we call ·handles of those edges") . In an w -graph, nodes which correspond to marked formulae are called "transitive nodes· and the other nodes ·w -nodes· . We call a path of thew -graph ofF ·a behavior ofF" and especially the behavior passing cycles at most one time is called ·a skeleton behavior ofF". Note that if an w -node has a cycle, then the infinite sequence of handles on its edges can be a model of the temporal formula. An w -graph can be regarded as a finite state automaton for w -language[3] . Therefore, let F and G 1 be a temporal formula and its w -graph and L(F) the language accepted by the automaton corresponding to G 1 , then the following relations clearly hold :

• (i) F = F1 1\ F2 < > L(F) = L(F1) n L(F2)

• (v) Fl :::> F2 < > L(Ft) ~ L(F2),

where E is a set of the alphabet. From the property of w -language, it follows that the containment relation of (v) is decidable.

Using these correspondence, we have developed the follow­ ing "containment algorithm" to decide the above relation (v) . Let F1 and F2 be temporal formulae and G; and L(F;)(i = 1, 2) corresponding w -graphs and w -languages, respectively. Then in order to decide whether L(Fd 2 L(F2) or not (for con­ venience, we say ·G1 contains G2 · if L(Fd 2 L(F2) holds), we perform the following two checking rules :

(1) [Checking Rule 1]

Consider the handles H;; on edges E;; which are outgo­ ing from each initial node N; of G;(i = 1,2 and j = 1, ... , m;) . Check whether

If this relation doesn't hold, then the above L(Ft) 2 L(F2) doesn't hold. Otherwise, for each pair of the handles (Ha, H2z), if Ha 1\ H21 is not false , then check whether L(Ga) 2 L(G2z), where Ga and G2z are formulae cor­ responding to the nodes to which the edges Ea and E21 lead, respectively. This checking rule is applied iteratively until no new pair of nodes appears.

(2) [Checking Rule 2]

When N2 is an w -node and it contains a behavior of which node-sequence is in a form (N2, T1, .. . , T;, ... , T~r;, N2), then check whether in G1, we can find a w -node W; and a behavior B1 in a form : (N1, ... , Sm, W;, ... , S,., W;) which satisfy the condition such that for the infinte behaviors whose node-sequences are (N1, ... , Sm) · (W;, ... , S,., W;)"' and (N2 , T1, ... , T;, ... , T~r;,N2)"', the corresponding pairs of nodes satisfy the condition ( *) of the above (checking rule 1] . Note that this procedure always terminates because such pairs of the nodes are finite.

B. Reasoning on an w -graph

A lot of reasonings about the behaviors of plant controllers can be reduced to a simple procedure of the w -graphs for the dynamics of the plant controllers. We examine the typical reasonings which often appear in practical applications.

1. Automatic Synthesis of Controls

An automatic synthesis of controls means a mechanical derivation of the control rules which guide the system to the desirable state. More specifically, it means to determine the unknown control rules which satisfy the following condition :

D11namics 1\ Unknown Control Rule. :::> Goal. The unknown control rules can be determined by the process of checking the requirement that the w -graph of Goal must contain the w -graph corresponding to D11namics 1\ Unknown Control Rule&. This process will be explained in section IV. Furthermore, we can check the ob­ servability and the stability of the system in the same way.

2. Qualitative Simulation and Causal Arguments

A qualitative simulation([4]) is a reasoning about how the system is going to be in future. Namely, it means to find out the qualitatively distinct states which can be reached from the current state. This reasoning is corresponding to determining the sequence of unknown states X11 X2 , ··· such that

where the predicate P specifies the current state. The simple way to solve this problem is to examine a set of skeleton behaviors with respect to the initial condition P, because a skeleton behavior contains all the distinct states which can be reached in that behavior.

A causal argument([4]) means to find out the past state which has caused the present state. Namely, it is a repetition of the process to determine the past states X 1, X2, ... such that

so that it corresponds to performing the qualitative simulation backwardly.

IV. An Example

In order to illustrate the procedure of the control synthesis on an w -graph, we construct the control rules for the example of the boiler described in section II.

Figure 2 shows an w -graph GD which corresponds to the dynamics D and the frame axioms for the boiler. By using GD, we try to find the control rules to guide the system to the stable situation of some states, for instance E2 V E3 V E 4 · Controls C should satisfy the formula :

D11namics D 1\ Controls C :::> oo(E2 V E 3 V E 4 ) The control rules for the boiler are represented in the form:

• if E; then H+-ONfOFF (i= 1, ... ,5) where H+-ON /OFF means that His set to be ON or OFF This is transformed to the temporal formula C:

The w -graph Gc corresponding to C 1\ D can be built by substituting E;H; forE; appearing in GD.

We try to extract the control rules to achieve the even­ tuality OEs . Thew -graph Gg for this goal shown in Figure 3 should contain the w -graph Gc, in order to establish

By using the containment algorithm for w -graphs, we can decide the desired control rules in the following way. Assume that the edge labeled E1H1HF1 + E2H2HF1 exists. Then we have to check the pair of nodes (T0 , wl) . And if the edge labeled E1H1HFo exists, again we go to check (T0 , wt) . Since w1 is an w -node, it contains the infinite behavior of (E1H1HFo)"' . On the other hand, To contains no infinite behaviors of the form (E3)"'. (D 1\ C :::> oEt) is not satisfied if

Namely, H1 =H. By repeating the similar procedure for the other. edges, we get the following value assignments of H; .

As for the stability and observability, we can build the w -graph, and controls synthesis can be done similarly. In this way, we get the following desired control rules by combining with the above control rules altogether.

V. Concluding Remarks

A method for description and reasoning of plant control­ lers is discussed in the framework of temporal logic. As a method of reasoning about a dynamical system, we present an w -graph approach. Since the w -graph representation gives the inner model of the dynamical system and we can perform various kinds of reasoning on it, it appears to be more effective than usual theorem proving methods such as natural deduction or tableau method. A system which manipulates an w -graph is currently under development for practical applications.

Although the major concern of this paper is in the com­ plicated plant system, the temporal framework which is devel­ oped here can be extended to the other species of dynamical systems.