A reachability synthesis procedure for discrete event systems in a temporal logic framework

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS, VOL. 24, NO. 9, SEPTEMBER 1994

A Reachability Synthesis Procedure for Discrete Event Systems in a Temporal Logic Framework Jing-Yue Lin and Dan Ionescu, Senior Member, IEEE Abstract-A temporal logic model is introduced to the modeling and design of discrete event systems. Within such a model, the relationship between the reachability of states and the validity of formulas is given to provide a basis for the composition and synthesis of discrete event systems in a temporal logic framework. The composition of temporal logic models is accomplished by formulating a temporal logic model as a process algebra and defining projection applications within the temporal logic models. k e d u r e s are developed for reachability synthesis and a controller logic model is designed to ensure that the required behavior of the system is met. An example of a system of read-write processes is demonstrated to illustrate the novelty of this approach.

I. INTRODUCTION Discrete Event Systems (DESs) are classes of processes which are driven by the occurrences of discrete events. Examples of such systems can be found in communication networks, computer programs, operating systems, real-time systems, and manufacturing processes. There are many approaches to the modeling and control of DESs. Among them are: automata and formal languages [24], [27], finitely recursive processes [lo], min-max algebra [14], perturbation analysis [9], Petri nets [4], [22], and temporal logic [11]-[15]. In the development of a theory for DESs, given a model of a DES considered as a plant and the requirement of its behavior, the basic objective of the theory is to design and synthesize an appropriate controller to realize the specified closed-loop behavior. Once such a theory is developed, it will be used to implement various applications. Temporal logic is a formalism that has been proposed in computer science by Manna and Pnueli [18], [19], and others [2], [7], for software verification, particularly for the analysis and synthesis of concurrent programs, operating systems, and distributed systems. Recently, it has been applied into the control problems of DESs by Fusaoka et al. [6], Thistle and Wonham [25], and others [ l l ] , [12], [13], [15]. Real time systems have been specified in a real time temporal logic frame work by Ostroff [20], [21]. However, among the growing literature that discusses DESs, relatively little work regarding the design procedures has been done in the temporal logic approach. Having a temporal pattern on its logic features, temporal logic has been used as an investigation framework in many applications in DESs, in particular, computer-related systems. Currently, computation algorithms in a temporal logic approach are badly needed for application development. To implement such algorithms, a temporal logic model for DESs is in demand and has not yet been established. A bounded stochastic model has been introduced by Lin and Ionescu [13], [15] as a structure for reasoning about a class of nondeterministic DESs. In that model, apparently there is a lack of dynamical notion for the DES analysis; and hence, it needs to be modified to establish dynamics of DESs by introducing transition functions. In other words, the motivation of this paper is derived from the need to build a general model as well as a related Manusript received October 7, 1991; revised October 3, 1992, April 6, 1993 and October 25, 1993. This work was supported in part by the Natural Science and Engineering Research Council of Canada under Grant No. A6684. The authors are with the Department of Electrical Engineering,University of Ottawa, Ottawa, Ontario, Canada K1N 6N5. IEEE Log Number 9402999.

1391

theory. Eventually, it is also motivated by the need to implement computation algorithms for DESs in a temporal logic approach. This involves modeling the dynamic behavior of DESs such as reachability properties, and synthesizing a controller to prevent the undesired behavior in the controlled DES system. Therefore, the main objective of the paper is to develop procedures for the controller design and synthesis of DESs in a temporal logic framework. In this paper, dynamic behavior of DESs is characterized by temporal logic models which consist of mainly a set of events and a set of temporal logic formulas describing the enable conditions of the events. Procedures are developed for reachability analysis, composition and synthesis of subsystems by applying Hennessy’s process algebra. One of the important results is that reachability of states is equivalent to validity of logic formulas of specifications for the system. It simplifies the system design procedures as it uses the reachability properties instead of validity properties. An algorithm is developed for computing the reachability set and for constructing the reachability graph. Based on these results, the procedure for the controller design and synthesis also does the verification. These results will prove to be useful for the users in the analysis, design, and synthesis of DESs. This paper is organized as follows. The temporal logic model (TLM) is defined for modeling of DESs in the next section. In Section 111, the relationship between reachability of states and validity of formulas is given by defining reachability and the properties of TLM; and then the algorithm for computing the reachability set and constructing the reachability graph is developed. By applying Hennessy’s process algebra, in Section IV, a TLM is formulated as a E-algebra and a E-homomorphism of TLMs is introduced to provide a composition operation for reachability synthesis of TLMs. This will lead naturally to, in Section V, a controller synthesis procedure using reachability properties to ensure that the closedloop system has the required behavior. An example of read-write processes is demonstrated throughout the paper to motivate and illustrate the discussions. These examples are treated using a temporal logic simulation language for DESs [16], proving in this way the validity of the theory on which they rely. Finally, conclusions are given.

11. TEMPORAL LOGIC MODELS FOR DESS Dynamical behavior specification of a DES consists of the tracing of occurrences of events. Presently there is a large number of models for representing systems which exhibit a discrete event behavior. Fundamental to all of these models is that the behavior of the system is described by a sequence of events. The temporal logic approach of discrete event processes concentrates on two primitive concepts: events and conditions. In the following, it is assumed that the events are simple and discrete for a given DES. Here we use that events are simple to imply that we do not worry about what kinds of events they are and that the events of interest to us come from a set E of events or more strictly event occurrences. Events are generally assumed to occur asynchronously and instantaneously, and their effects are immediately registered. A condition is one of the premises under which an event can occur. It is a predicate or logical description of the parts and/or the inputs of the system. In a temporal logic approach, a DES is characterized by a set of events and a set of temporal logic formulas describing the conditions under which events can occur. The language and the proof system of the temporal logic used in this paper are the same as those used by Thistle and Wonham

0018-9472/94$04.000 1994 IEEE

I

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS, VOL. 24, NO. 9, SEPTEMBER 1994

1398

[25] which have been adapted from Manna and Pnueli [18], [19] and have been extended to a generalized temporal logic by Lin and Ionescu [13], [15]. The temporal logic is an extension of the ordinary logic to include the notion of time, providing five modal operators: 0 (henceforth), o (eventually), 0(next), u (until) and p (precedes). Informally, for a sequence and a given state in that sequence, O w is true iff w is true in the next state in the sequence; Ow is true iff w is true in all future states of that sequence; ow is true iff w is true in some future state (Le. it is eventually true) in the sequence; wlUw2 is true iff w1 is true for all states until the first state where w2 is true; and w l P w z is true iff w1 is true for some states before any state where w2 is true. The language is a many-sorted one. Following Enderton [5], we assume that we have a non-empty set I, whose members are called sorts. There is a countable number of constant symbols, and also of variable symbols, of each sort i. For each n > 0 and each ( n 1)tuple of sorts (il,Zz, .. . ,&+I), there is a countable set of n-ary function letters said to be of sort (il,iz, .. . ,inti). Also, for each n > 0 and each n-tuple of sorts ( i l , i z , . . ,a,), there is a countable set of n-ary predicate letters said to be of sort (i 1, i z ,. . ,i n ) .

TABLE I EVENTSAND STATESOF THE EXAMPLE

+

.

.

Dejinition I : Let D , be the domain for sort a. A state is an assignment of an element of D , to each variable symbol of sort a. Let S denote the set of all states (state space). If the occurrence of e E E can change the system from state s E S to another state or a set of states, then we call this as that event e has an outcome on state s. Definition 2: An event is said to be enabled at state s if it has an outcome on s; otherwise it is said to be disabled at s. Let E, denote the set of events which are enabled in the state s and F be the set of temporal logic formulas describing the enable conditions for the events in E of the given DES. A temporal logic model for DESs is then defined as follows.

Definition 3: A temporal logic model (TLM) is dejned by a 6-tuple M = ( S ,E, F', f , 1, so) where S is the set of states; E is the set of events, each event can be viewed as a transition from a state to another state; F* is the set of all subsets of F; f is a mapping from E x S into S such that Vs E S, 'de E E,, f ( e ,s) is dejined 1 : E x S -+ F' is a labelingfunction, associating to every pair ( e ,s) the set of formulas that hold in (e, s); and so is an initial state. The above definition is a slight modification of Definition3 given by Lin and Ionescu [15]. Our temporal logic model is a slight modification of the computational model in [19]. Moreover, it emphasizes the dynamics of the model. The following result can be obtained easily from Definitions 1-3.

Proposition I : For any s E S, an event e E E, ifand only i f e is enabled, i.e. all preconditions of e are satisjied. If e is enabled, then the next state is s' = f ( e , s). Two sequences result from the execution of an event structure: the sequence of states ( S O , SI, S Z , . . . ,sn) and the sequence of events (el, e2, . . ,en), which were fired. These two sequences are related by the relationship f(ek+l, s k ) = S L + ~ for k = 0,1,2, . . . ,n - 1. Dejinition 4: An interpretation M specifies a domain D , for

.

each sort i, and assigns to each constant symbol of sort i an element of D , , to eachfunction letter of sort (il,i 2 , . . . ,in+l)a function f : D , , x D,,x ' . .x Dan Din+, and to each predicate x . . .xD,,. letterofsort(il,i 2 , . . . ,in) a relation P c D , , xD,, The formulas are evaluated with respect to the structure ( M , u ) .--)

where the model M defines an interpretation and u is a sequence of states with the initial state SO. A state formula is any well-formed first order formula constructed over the variables and propositions; and it can be evaluated over a single state to yield a truth value. A temporal formula is a formula constructed from state formulas to which we apply some temporal operators.

With the labeling function I , a TLM is described by a set of formulas. A temporal formula Z(e, s) has the following form: O[s(z) A

4.1

* Os'(z)I

(1)

where z is a local variable, s(z) stands for the predicate representing the state at the present time, e(.) for that representing the event about to occur, and os'(z) for that representing the state at the next time. Then the following theorem gives the enable rule for the TLM. Proposition 2: In a TLM M = (S, E, F * , f , 1 , so) for s E S ,

an event e E E, (e is enabled) if and only if 1 ( e ,s) having form (1) is in F*. The plant of a DES can be represented by a TLM plant which itself is composed of many TLMs with each TLM representing one of the plant processes. In each process, a state of a TLM corresponds to the execution of exactly one event. To reflect this fact, we systematically add to our specifications for each process in the TLM the following: O{[V~ sS-(R.ID) e6=(erqr 2)=e2 ---> s6=(WR,WR) e 7 = ( w q w 2)=e4 ---> s7=(WR,WW)

Fig. 1. The graph of process

2.

Dynamics

The root: s2=(ID,WR) e9-(erqr 1 ) - e l ---> s9-(WR,WR)=s6 elO=(erqw 1)=e3 -> slO=(WW,WR) e8=(estr 2 ) --> s8=(ID,R) The root: s3=(WW,ID) e l l - ( e s t w 1 ) --> s l l - ( W , I D ) s12-(WW,WR)-r ;lo e l & ( e r q r 2)-e2 --> e l 3-(erqw 2)-e4 ---> sl3=(WW,WW)

Formula (Pl) describes the effect of the request to read of process z: its state changes from ID(z) to WR(z),while the states of the other processes remain the same. (P2) - (P6) are similar to (Pl), describing the effects of the commencement of reading, the end of reading, the request to write, commencement of writing, and the end of writing, respectively, of process 2.

Initial condition

The root: elS-(erqr el6-(erqw el4=(estw

s4=(ID,WW) slS-(WR,WW)=s7 1)-el --> 1)-e3 ---> s16-(WW,WW)-s13 2) ---> sl4-(ID,W)

The root: e l 7=(endr el8=(erqr el9-(erqw

sS=(R.ID) 1) --> s17-(ID,ID)=sO 2 b e 2 ---> sl8-(R,WR) &e4 ---> s19-(R.WW)

The root: s6=(WR,WR) e20=(estr I)=e5 ---> s2O=(R,WR)=sl8 e21=(estr 2)-e8--> s2l-(WR,R) The root: s7=(WR,WW) e22=(estr 1)=e5 --> sZZ=(R,WW)=sl9 e 2 3 4 e s t w 2)-e14 ---> s23-(WR.W) The root: s8-(IO.R) e24=(erqr 1) = e l -> s24-(WR,R)=s21 e25=(erqw 1)=e3 ---> s254WW.R) e26=(endr 2 ) ---> s26=(ID.IO)=sO The root: slO-(WW,WR) e27=(estw 1 ) = e l 1 ---> s27=(W,WR) e28=(estr 2)=e8 ---> s28=(W,R)=s25

It means that initially all processes are idle. A graphical representation of a TLM is intuitive and useful. A TLM consists of transitions (events) and states (conditions). Corresponding to these, its graph has two types of nodes. A circle o represents a state; a bar 1 represents a transition. Directed arcs (or edges) connect the states and the transitions, with some arcs directed from states to transitions and other arcs directed from transitions to states. The graph of the example is shown in Fig. 1. The graph takes the advantages from both Petri nets and the state transition graphs of finite state machines.

The root: 51 l=(W,IO) e29=(endw 1) ---> s29=(ID,ID)-sO e30=(erqr 2)=e2 --> s30=(W,WR)=s27 e31=(erqw 2)=e4 ---> s31=(W,WW)

m e r o o t : s18-(R,WR) e37=(& 1)-e17 --> s37-(ID,WR)=s2 e38=(estr 2)-e8 -> s38-(R.R) The root: s l 9=(R,WW) e39-(endr 1)-e17 -+ s39-(ID,W)-s4

e4o=(estw Z)-e14 ---> s40-(R.W) The r w t : s2 1 -(WR.R) e41-(estr 1)-e5 -> s41-(R,Rk38 e42-(sndr & e 2 6 -> s4Z-(WR.D)-sl m e roof: s23-(WR.W) e43=(estr 1)-e5 -> s43-(R9W)-s40 e44-(endw 2)=e36 --> s44-(WR,ID)=sl The root: s25-(WW,R) e45-(estw 1 ) - e l l -> s45=(W,R) e 4 6 4 e n d r 2)-e26 --> s46-(WW,ID)-s3 The roof: s27-(W,WR) e 4 7 4 e n d w 1)-e29 -> s47-(1D,WR)-s2 e 4 8 4 e s t r 2)=e8 -> s48-(W,R)=s45 The root: s314W,WW) e49=(endw 1 )=e29 --> s49=(ID,WW)-s4 eSO=(estw 2)-e14 -> sSO-(W,W) The roof: s33=(WW,W) eSl-(estw l ) = e l l --> ~ 5 1 - ( W , W ) ~ s 5 0 e 5 2 4 e n d w 2)-e36 --> s52=(WW,ID)-s3 The root: s38=(R.R) e53=(endr 1)-e17 ---> s53=(ID.R)=s8 e54=(endr 2)-e26 --> sS4-(R,ID)-s5 The root: s40=(R.W) e55-(endr 1)-e17 ---> s55-(ID,W)-s14 e 5 6 4 e n d w 2)=e36 --> s56=(R,ID)-s5 The root: s45=(W,R) e57-(endw 1)=e29 -> s57=(ID.R)-s8 e58-(endr 2)=e26 ---> s58=(W,ID)-sll The root: sSO=(W,W) e 5 9 4 e n d w 1 )-e29 -> e60-(endw 2)-e36 -->

s59-(ID.W)-sl4 s6O-(W,ID)=sll

The root: s1 3-(WW.WW) e32=(estw l ) = e l l ---> s32=(W,WW)=s31 e33=(estw Z)-e14 ---> s33-(WW,W)

Fig. 2. The reachability computation of the example.

Dejinition 6: The mapping f is extended at state s for a sequence of events cr E E, and Ve E E such that cre E E, by

111. REACHABILITY ANALYSIS OF TLMS

Reachability analysis of DES was first mentioned for a temporal logic approach by Bochmann [ l ] where the definition of reachability was not given. A reachability definition for DES has been introduced by Ostroff [20], and some procedures for constructing reachability graphs have been also given for a special class of formulas in his language. In this section, we will define reachability to describe the dynamic behavior of the TLM introduced above, then find out the relationship between reachability of states and validity of formulas, and finally develop an algorithm for computing the reachability set and constructing the reachability graph. The result of firing an event in a state s is a new state s'. We say that s' is one step reachable from s; that is, the system can reach the state s' after firing an event from state s. The definition is as follows. Dejinition 5: For a TLM M = (S, E, F*, f , 1 , so), a state s' E S is one step reachable from s E S if there is an event e E E, such that s' = f ( e , s ) . It is convenient to extend the mapping f (next state function) to map a state and a sequence of events into a new state.

The rwt: sl4-(ID.W) e34=(erqr 1 ) - e l -> s34-(WR,W)-s23 e 3 5 4 e r q w 1)-e3 -> s35-(WW,W)-s33 e36-(endw 2 ) --> s36-(ID,ID)-sD

(3) where E is a null event. Eq. (3) means that the state of the system is unchanged if nothing happens. For a sequence of events e1e2 . . . e k , and state s, f ( e l e 2 . . . e k , s) is the result of enabling first e l , then e2, and so on, until e k is enabled. With this extended state mapping, we will extend Definition 5 to the definition of reachability (in general) as follows. Dejinition 7: For M = ( S , E, F*,f , 1, so), s E S is reachable

if s E R ( M ,so), the reachability set, which is the smallest set, defined by SO E R(M,so); If s E R ( M ,so) and t is one step reachable from s, then t E R(M,so). The smallest set is used to ensure that all elements of the set are reachable from so. In the following, when we say that s E S is reachable, it simply means that s E R ( M , so). Then reachability has the following properties. Proposition 3: The reachability relationship is transitive, i.e. if s' E S is reachable from s E S and s" E S is reachable from

~

1994

1400

Fig, 3. The reachability graph of the example.

s' E S, then s" E S is reachable from s E S . Theorem 1: In a TLM M = (S, E, F*,f,1 , so), s' is reachable from s if and only if the dynamical formula Z(e, s) E F* and has the form ( 1 ) . Proof: By Definition 5 , s' is reachable from s means that there exists e E E, such that s' = f ( e , s ) . By Proposition 2, this is equivalent to the dynamical formula Z(e, s) E F* which has the form (1). m Using Theorem 1, we can establish the relationship of transition mapping f and labeling function Z and it gives a relationship between the reachability of states and the validity of formulas in a TLM as follows.

Corollary I : For a given T U , the reachability of states is equivalent to the validity of the corresponding dynamical formulas. Prooj? By Theorem 1, s' is reachable from s if and only if Z(e,s), which has the form (1) belongs to F*. It follows from the definition of validity [13, 211 that l ( e , s) is valid. Hence we may use reachability properties of a TLM to verify the corresponding validity properties. Therefore, we may verify the specification of the plant by the reachability analysis. The verification of the specification given by a set of temporal logic formulas in a TLM is a procedure of proving validity of the formulas; and by Corollary 1, this can be converted to the reachability analysis of the TLM. As a computation algorithm for a TLM M , the procedure of computing the reachability set and constructing the reachability graph G M is as follows: Algorithm I: Step I : Given a temporal logic model A4 = (S,E, F*,f,SO, I ) . Then, node(GM) = {so}, edge(GM) = 4 where q5 is an empty set and SO is unmarked. Step 2: IF there is an unmarked node s in node(Gha), THEN MARK node s as a root and FIND the set E, using the following rule. OTHERWISE GOTO Step 4.

For each e E E, IF Z(e,s) is in F' THEN e E E,. Step 3: For every e E E,, DO edge(GM) := edge(GM) U {e} and FIND t = f ( e , s ) . IF t is unmarked, D O node(GM) := node(GM) U it}. GOTO Step 2. Step 4: END. Since F* is the set of all subsets of F, l ( e , s ) E F* is computationally decided by checking whether 1(e, s ) is a subset of F. This is used in the computation of the enable set E, according to Proposition 2. Thus, the reachability set is obtained as R ( M ,SO) = node(GM).It does not have duplicated elements; and this is ensured by the marking scheme used in the procedure such that no state is visited more than once. When a state is visited, it is marked as a root. Only those edges that are in the firing event set are added to the set of edges and only those states that have not previously been marked are marked as roots and added to the reachability set. At each state s, there are at most IE,J 5 [El events to be checked for successor states, where IEl is the number of events in E. Hence at most IEl . IR(M, SO)/ steps are needed to compute the reachability graph and the reachability set. The above algorithm was implemented in an object-oriented language (Objective-C) [17]. The state transitions of the given example are given in Fig. 2 for the case of N = 2 where N is the number of processes and the reachability graph is constructed in Fig. 3 which shows that the combinatorial explosion may occur in the construction of a reachability graph. The use of reachability as a specification of the DES system behavior will become clearer later when a relation on the reachability set of the system providing its entire dynamic behavior will be defined. IV. E-ALGEBRA AND COMPOSITION OF TLMS

As mentioned in Section 11, a DES may be composed of a number of TLMs with each TLM representing one of the DES processes. In this section, by applying Hennessy's process algebra [8], a TLM will be formulated as a E-algebra and a E-homomorphism of TLMs will be introduced to provide the composition operation and reachability

1401

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS, VOL. 24, NO. 9, SEPTEMBER 1994

synthesis for TLMs. In terms of Hennessy’s algebra, a E-algebra is defined as follows. Dejinition 8: [B] Given a set of formal functional symbols E, a

E-algebra is dejned by a pair ( A ,EA)in which A is a set, and E A is a set of functions { fA , f E E} such that, if the number of arguments o f f is n, then fa is afunction from A” A. -+

The mathematical significance of E-algebras resides in the use of E-homomorphisms which are defined in the following. Dejnition 9: IS] A E-homomorphism from a C-algebra (A, EA) to a E-algebra (B, E,) is defined by a function h satisfying for every fa in C A with k arguments there exists f~ in E, such that h(fA(a1,

... , U k ) )

= fB(h(Ul), . . . , h ( a k ) ) .

E-homomorphisms are simply functions which preserve the structures between E-algebras. By viewing our TLMs as E-algebras, this property can be used for the composition and reachability synthesis of TLMs. For this purpose, the following two results establish TLMs as E-algebras and the E-homomorphism between them. Theorem 2: ATLMisaE-algebra({S,E,F*},{f,l,so}) with the set { S , E, F*}, the binary operations f : E x S + S , and 1 : E x S +. F*, and the nullary operation so E S. Proof: By Definition 3, S, E, F’ are sets, and f , 1, are functional symbols with f : E x S -+ S, and 1 : E x S + F*. so can be viewed as a nullary operation over S. By Definition 8, ( { S , E, F*},{f,I , SO}) is a E-algebra. Corollary 2: Let M = ( { S ,E, F*},{f,I, so}) and M’ = ({S’,E‘,F*’}, { f ’ , l ’ , s & }betwo ) TLMs. Forany,threefunctions: h : S +. S’, g : E +. E’, and k : F* + F ’ , ifthey satisfy h ( s o ) = sb, and for all e E E , l ’ ( g ( e ) , h ( s ) ) = k(l(e,s)) and f‘(g(e), h ( s ) )= h ( f ( e ,s)), then [g, k , h] is a E-homomorphism

Fig. 4. Synchronization of two events.

particular, what effect the composition has on the dynamic behavior of the TLM and on the reachability set of the system. DejinitionIO: Let M = ( { S , E , F * } , { f , l , s o } ) and M’ =

({S‘,E‘,F*’},{~,l’,s~}) be two TLMs. The composition of M and M‘, denoted by MIIM’, is dejned by the concurrent operation of M and M’ in which selected events, e.g. e E E and e’ E E’, are synchronizedand fcm a synchronized event E = (e,e’). The event set of A4 is E =E {(e,e)le E E} U {(E,e’)le’ E E’} U {(e,e’)le E E , e ‘ E E’} where ( e , € ) and (€,e‘) denote events in M and M‘ respectively which are not synchronized with an event in the other T M . For all s E S and s’ E S‘ withs$f(s, s’), E E &only $e E E, ande’ E E,!. Thus, -

f ( e , s ) z ( f ( e , s), f‘(e‘, s’)), and t ( E , s ) z l ( e , s) n lr(e’,so. The synchronization of two events from M and M‘ is illustrated graphically in Fig. 4. Let 3 be the set of all B = (s,s‘). Then the composed model = MIIM‘ has the set of states 3 = S x S’, from M to M‘. the set F 2 F* U F’*,and the set of events E, the functions 7, Proof: Following Theorem 2, M and M’ are E-algebras. i, and the initial state 30 = (so, sb). The null event E is included Since h(so) = sb, and for all e E E,, g ( e ) E Eh(s). for null synchronization to make those unsynchronized events as the f ’ M e ) ,h ( s ) ) = W ( e ,s)), and Z’Me), h ( s ) ) = W ( e , s)), we events in the composite system. Particularly, 7 works with ( e ,E) in define [ h , g ,kl ( f ( e ,s ) ) e f h ( f ( e s,)), [h,9 , k ] ( I ( es, ) ) e f k ( I ( es,)), this way: 7 ( ( e ,e ) , (s, 5‘)) = (f(e, s), f ( ~ , = ( f ( e ,s), 0 .The and [h,9 , k ] (SO)%~~(SO).Then, [h,g , k ] ( f ( e s,)) = f ’ ( g ( e ) ,h ( s ) ) , processes involved in a synchronization remain in the same state for [ k g ,k I ( I ( e , s ) ) = I ‘ ( g ( e ) , h ( s ) ) , and [ h , g , k ] ( s o ) = sb. BY the null event E and have a transition f ( e , s ) for the event e # E . Definition 9, [h, g , k ] is a E-homomorphism from M to M’. Thus, the dynamic behavior of the composed TLM is now given in An important property of a E-homomorphism between TLMs is terms of the projection mappings from into M and M’. that it preserves the dynamic behavior and reachability of the TLMs -Theorem 4: Let [h,g, k ] and [h’,g‘, k’] be theprojectionsfrom as shown in the following theorem. M = MIJM‘ to M and M’ respectively, i.e. h : S -+ S, Theorem 3: Let [g, k , h] : M +. M‘ be a E-homomorphism g : E*-+ E, k : F* -+ F*, h’ : S +. 9’ : E +. E’, and

x

4)

s‘,

of TLMs. Then k‘ : F -+ F“. Then (a) Ift = f ( e , s ) is in M , itfollows that h ( t ) = f’(g(e), h ( s ) ) a) The prg’ection mapgngs are E-homomorphisms; is in M‘. b) Ifz = f ( E , s ) is in M , then both h(1) = f(g(E), h@))is in (b) I f t is a reachable state of M , then h ( t ) is a reachable M and h’(z) = f’(g‘(E), h‘(2))is in M’; and state of M‘. c) I f j is reachable in 2 = MIJM‘,then both h(z) and h’@) are reachable in M and M’ respectively. Proof: Proof: 1) Since [h,g, k ] : M -+ M‘ is a E-homomorphism, it follows from Corollary 2 that h ( f ( e ,s)) = f ‘ ( g ( e ) ,h ( s ) ) .Because of a) By the definitions of projections, h ( S ) = s, g(E) = e, t = f ( e , s ) E M , h ( t ) = h ( f ( e , s ) )= f ’ ( g ( e ) , h ( s ) ) Hence . k ( t ( E , s ) ) = Z(e,s), and h(T(F,B)) = f ( e , s ) . Hence, h ( t ) E M‘. z ( g ( z L h ( s ) ) = Z(e, s) = @ ( E m f ( g ( E ) ,h@)) = f ( e , s ) 2) Since t is a reachable state of M, there exist s E S and e E E, = h ( f ( E , S ) ) ,and h(20)= SO. By Definition 9 and Corollary such that t = f ( e , s) E M. It follows from (a) of this theorem 2, the result follows. that h ( t ) = f ’ ( g ( e ) , h ( s ) )E M‘ where g ( e ) E E q s ) and b) By (a) of this theorem, [h,g,k ] and [h’,g‘, k‘] are C h ( s ) E M’. By Definitions 5 and 6, h ( t ) is a reachable state homomorphisms. For -i = f ( F , B ) in R, it follows from of M’. (a) of Theorem 3 that h(E) = f ( g ( E ) , h ( B ) )is in M and h’(?) = f‘(g’(E),h’(3)) is in M ’ . The above results provide a possible composition operation to c) By (a) of this theorem, [ h , g , k ] and [h‘,g’,k’] are Ebuild a TLM from its component TLMs (say two TLMs), by putting together the TLMs, and synchronizing, selected events for homomorphisms. Because 5 in 3 = MIIM‘ is reachable, reachability synthesis, at the same time. In the following, we will define the composition operation and investigate its properties, in

it follows from (b) of Theorem 3 that both h(?) and h‘(?) are reachable in M and M’ respectively.

I

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS, VOL. 24, NO. 9, SEWEMBER 1994

1402

The state transitions of the diskfie are: The root: so=(iD.ID) el=(esbr 1) k-si=(BR,ID) e3=(esbw 1) -> s3=(BW,iD) ez=(esbr 2) --> sZ=(ID,BR) e4=( es bw 2) -> s4=( ID,B W) The root: s 1 =( BR ,ID) es=(enbr 1) --> s5=(1D,ID)=sO e6=(esbr 2)=e2 -> s6=(BR,BR) e7=(esbw 2)=84 -> s7=(BR,BW)

The root: sa=fBW.ID) , - , e 1 i=(enbw 1) --> s 1 l=(ID,ID)=so e iz=(esbr 2)=e2 -> s lz=(BW ,BR)=s 10 e i3=(esbw 2)=e4 -> s 13=(BW,BW) The root: s4=(iD,BW) e iS=(esbr i)=el -> s 15=(BR,BW)=s7 e 16=(esbw 1)=e3 -+ s 16=(BW,BW)=s 13 e 14=(enbw 2) -> s 14=(1D,ID)=sO

The root: sz=(ID,BR) e9=(esbr l)=e 1 -> s9=(BR,BR)=s6 e io=(esbw 1)=e3 -> s lo=(BW,BR) e8=(enbr 2) --> s8=(lD,ID)=sO Fig. 5. Reachability computation results of the disk model. TABLE I1 THEHOMOMORPHISM FROMTHE PROCESSOR TO THE DISKMODEL

\

/

\

Wd) Fig. 6. Composition of the disk and process models.

and the end of being read, and esbw(d) and enbw(d) represent the commencement and the end of being written, respectively, of the disk. Then, the specifications of the disk are as follows.

+ OBR(d)]

(MI)

O[enbr(d)A B R ( d ) + O I D ( d ) ] O[esbw(d)A I D ( d ) oBW(d)] O[enbw(d)A B W ( d ) + O I D ( d ) ]

(M2)

O[esbr(d)A I D ( d )

*

We use the given example to illustrate our composition procedure. Further consideration of this model shows that it is formed by the composition of two TLMs, one for processes and one for the disk. Events in each TLM are synchronized with one another in relation to the way in which the two subsystems interact such that these two TLMs are composed. For example, when a process goes from waiting for reading to reading, the disk goes from idle to being read. We can then combine the two synchronized events into a single event, and the two states, reading for the process model and being read for the disk model, into a single state. For the disk model in the given example, we give the following description. B R ( d ) ,BW(d), and ZD(d)will represent the three possible states of the disk d, those of being read, being written, and being idle. The event symbols esbr(d) and enbr(d) represent the commencement

(M3) (M4)

The reachability graph routines together with the enabled event sets of the disk model are given in Fig. 5. Now we can visualize all the components of the E-homomorphism [h,g, k ] from the twoprocessor model M to the disk model M' ( ' is added to e and s of Fig. 5) as shown in Table 11. The composition of the disk and process models is shown graphically in Fig. 6. This composition shows us that the composition operation could be used to build the closed-loop system from the plant and the controller; and it can be made by placing the controller in the place of the disk in the given example. This result provides a basis for a reachability synthesis procedure for constructing a controller which, when composed with the plant, will impose the required behavior on the composite system. V. CONTROLLER DESIGN AND SYNTHESIS PROCEDURE

The behavior of a DES plant (uncontrolled system) is usually unsatisfactory in some aspects; a description of the required plant

1403

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS, VOL. 24, NO. 9,S E m M B E R 1994

According t o t h e s p e c i f i c a t i o n s of t h e required behavior s40 should not been reached! So event e40 should s43=(R,W)=s40 So event e43 should be disabled at s45 should not been reached! So event e45 should s48=(W,R)=s45 So event e48 should be disabled at s50 should n o t been reached! So event e50 should s51=(W,W)=s50 So event e51 should be disabled at s40 may not be a r o o t ! s45 may not be a r o o t ! s50 may not be a r o o t !

be d i s a b l e d a t s t a t e s l 9 ! s t a t e s23 ! be d i s a b l e d a t s t a t e s25 ! s t a t e s27 ! be d i s a b l e d a t state s31 ! state s33 !

Then t h e s e t of states which should not be reached are: s40=(R ,W) s45=(W ,R) s50=(W,W) Fig. 7. List of warnings and suggestions given by the monitor.

The t r a n s i t i o n s i n t h e c o n t r o l l e r a r e : The r o o t : CO = ( O , O ) e l = ( e s t r 1) --- > e 2 = ( e s t r 2) ---> e3=(estw 1) --- > e4=(estw 2) --- > C l =(0,1) The r o o t : e5=(endr 1) --- > --- > e6=(endr 2) ei'=(estr 1) --- > e 8 = ( e s t r 2) --- > The r o o t : C 3 =(1,0) e9=(endw 1) --- > elO=(endw 2) --- > The r o o t : C7 = ( 0 , 2 ) e l l = ( e n d r 1) --- > el2=(endr 2) --- >

c1

=(0,1) c2 =(O,l) = C l c3 =(1,0) c4 = ( l , O ) = c3

c5 C6 c7 C8

=(O,O) = co =(O,O) = CO =(0,2) = ( 0 , 2 ) = C7

c 9 = ( O , O ) = co C l O = ( O , O ) = co

c11 = ( O , l ) = CI c12 = ( O , l ) = C l

Fig. 8. The state transitions of the controller.

behavior is then imposed. The description can be formulated in temporal logic formula specifications; and it usually is a restriction on the reachability set of the system such that the unsatisfactory states may not be reached. It is the task of the controller to ensure that the unsatisfactory behavior of the plant is eliminated. Let M denote the TLM of the plant and M , denote the TLM of the controller, as yet to be constructed according to the specifications of the required behavior. We propose that the plant operates concurrently with the controller such that the control action is achieved by the synchronization of the events in the controller with the same events in the plant. Hence, the behavior of the initially uncontrolled plant is restricted since certain selected events are prevented from occumng unless the controller is also in the state which allows the corresponding synchronized event to occur.

Fig. 9. Graph of the composite system of the example.

Let M = ({S,E,F*},{f,l,so}) and let Mc = ({Q,Ec,F:}, q o } ) with E, C E . Then the closed-loop system of the plant M and the controller M , is defined as follows. Definition 11: The closed-loop system of M and M,, written = MIJM,, is defned by replacing M' in Definition 10 by as M,; and in addition, for all s E S and q E Q with Z%f(s, q), e E & i f e E E, a n d e E Ep. Here the composite system consists of the plant M and the controller M , which will be designed according to the required behavior of the closed-loop system-the composite system, such that the undesired events will be prevented from occumng. The synchronization is performed by selecting the events from E n E, to achieve the required behavior. It is a special case of synchronization since two systems use the same event not a real synchronization of two events. By Definition 11, the closed-loop system = MIIM, has the set F* U Fr, the set of states = S x Q, and the set of events E = E. Denote the transition function in by 7, then e E & if both e E E, and e E E, where S = (s,q ) . Obviously, (SO,qo) is the initial state of The labeling function is t ( e , s ) = Z(e, s) n L ( e , q) in F*U Fr . Hence, we have = (S x Q, E, F* U Fr ,T, t, (SO,4 0 ) ) and the following result. Corollary 3: Let = MJIM, as stated above. Then a) ( s ' , 4') = T ( e , (s,q ) ) is in% ifand only ifborh s' = f ( e ,s ) in M and q' = f,(e, q ) is in M,Land b) If 7 = ( s ' , q') is reachable in M = MIIM,, then s' is

{f,,Z,

a

s

x.

x

w

reachable in M and q' is reachable in M,.

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS, VOL. 24, NO. 9, SEPTEMBER 1994

1404

Now the state t r a n s u o m of the m t r d l e d system are:

The root: 513 -(WW,WW,O.O) e32=(estw 1)-el 1 -> 532 =(W.WW.I,0)-531 e 3 3 4 e s t w +e14 --> 533 -(WW,W.l,O)

The root: SO =(ID.ID.O.O)

el-(wqr 1) ---> 5 1 -(WR.ID.O.O) e34erqw 1) -> 53 -(WW,ID,O,O) eZ=(erqr 2) ---> 5 2 -(ID.WR,O.O) e 4 4 e r q w 2) --> 54 -(ID,WW,O.O)

Theroot: 514 -(lD,W,l,O) e34-(aqr I)-el --> S34 -(WR,W,l,O)=S23 e 3 5 4 a q w 1)-e3 --> S35 -(WW.W,1.0)-533 e36-(mdw 2) --> 536 =(ID,ID.O,0)=50

The rWt: 51 -(WR,ID,O,O) e5=(estr 1) -> 55 =(R,lD,O,l) e6-(erqr 2 1 - d --> 56 -(WR,WR,O.O)

e7=(erqw +e4

-+

S7 =(WR.WW.O,O)

S l 8 -(R.WR,O.l) e 3 7 4 e n d r 1)=e17 -> 5 3 7 -(ID.WR,O,O)-SZ e3&(estr Z b e 8 -> S38 -(R.R,O.Z)

Themot:

The root: SZ -(ID.WR.O,O) e9-(wqr l ) = e l -> S9 =(WR.WR.O.O)=56 elO-(erqw l)-e3 -> S10 =(WW,WR.O.O) e8=(estr 2) --> 58 -(lD.R,D,l)

Themot: 519-(R,WW,O,I) e39-(mdr 1)-el 7 -> 5 3 9 -(ID,WW.O.D)-M

The root: 53 =(WW,lD.O.O) e l l = ( e s t w 1) -> S11 =(W.ID.l.O) e l 2 4 e r q r 2)-e2 --> 512 -(WW,WR,O.O)-510 el3=(erqw Z)=e4 ---> 513 =(WW,WW.O.O) The root: 54 =(ID,WW.O.O) elS-(erqr l ) = e l ---> 51 5 -(WR.WW.O.O)=S7 e l 6 4 e r q w 1)=e3 --> 5 1 6 =(WW,WW,O,O)=Sl3

elr=(estw 2)

---> S14 =(lD,W,l,O)

The r W t : 55 =(R,lD,O,l) el7-(endr 1) ---> 517 -(ID.ID.O.O)-SO e l 8 4 e r q r Z)=eZ --> 518 =(R.WR,O,l) el9=(erqw Z)=e4 -> 5 1 9 =(R,WW.O.l)

The root: 521 r(WR.R.0.I) e41-(estr l)=eS --> 541 =(R,R.0.2)=538 e42-(endr 2)=e26 -> S42 -(WR.ID.O.O)-Sl

The root: 523 -(WR.W,l .O) e444endw 2 h 3 6 ---> 544 -(WR.ID.O.O)=Sl The mot: 525 =(WW,R.O.l) e46-(endr +e26 -> 546 =(WW,ID,O,O)=S3

The root: 527 -(W.WR.l .O) e47-(mdw l ) s 2 9 --> 547 -(ID,WR,O,O)-S2

The root: 531 -(W,WW.l.O) e 4 9 4 m d w 1)-e29 -> S49 -(lD,Ww.O,0)=54

The root: 56 =(WR.WR.O.O) e 2 0 4 e s t r l)-eS --> SZO =(R,WR,O,l)=S18 e 2 1 4 e s t r 2 k e 8 --> 521 =(WR.R.O,l)

The root: 533 -(WW,W,l,O) eSZ4endw 2)-e36 --> 552 -(WW.lO.0.0)=53

The root: S7 =(WR,WW,O,O) eZZ=(estr 1)-e5 --> SZZ -(R,WW,O,l)-S19 e 2 3 4 e s t w 2)-e14 ---> 523 -(WR.W,l,O)

The root: 538 =(R,R.O.Z) e53=(mdr I ) = e l 7 --> 553 -(ID,R,O,l)-S8 e 5 4 4 e n d r +e26 -> 5 5 4 =(R.ID.O,l)-SS

The root: 58 =(ID.R,O,l) e244erqr l ) = e l ---> 524 =(WR.R.O.l)-SZl eZ54erqw 1)-e3 -.> 525 =(WW.R,O.l) e 2 6 4 m d r 2) ---> S26 =(ID.ID.O.O)-SO

The readability Set: 50 -1lD.lD.O.01 51 -1WR.ID.O.O) S2 =(ID.WR.O.O) 54 o.ww.oojss X i D , o . Y j 56-(WR,HR.O.O) 57-(WR.WW.O.O)S8-(D,R.O.I) 510 -(WW.NR.O.O)SI l-(W,ID.1.0)513-(VVW.WW.O.O) 914 =(ID.W.l.O) 518=(R,WR.O,1) Sl9-(R.WW,O.l) 921 =(WR,R,O.l)523 =(WR,W,l.O)S25-(WW,R,O.l) S27 =(W.WR.1,0) 531 -~W.WW.l.O)S33=~wW,W,l.O) 938 =(R.R,O,Z)

The root: 510 4WW.WR.O.O) e 2 7 4 e s t w l ) = e l l ---> 527 =(W,WR,l,O) e28=(estr 2)=& ---)S28 =(WW.R.O,l)=SZS

s3 -(&.m.o.oi

-i

Denote the set by R, and then find E, the set of events which lead to these states. iv) Find the event set E, = E fl 7 E U ,and then construct the controller M , by temporal logic formulas specifying the initial state qo and enabling rules for the events in E,. If verification is required, go to the next step; otherwise, go to Step (vi). Compute the reachability set R(M,, 4 0 ) of the controller. v) vi) Synchronize the events in E, of the controller Mc with the same events in EniE, of the plant M, and this synthesis will prevent those events in E, from occurring such that states in R, may not be reached; then compose M and Mc into the closed-loop system %. If verification is required, go to the next step; otherwise, go to Step (viii). vii) Compute the reachability set R ( Z ,(SO,4 0 ) ) . viii) End. From the computational analysis of Algorithm 1, at most IEl . IR(M,so)l, IEl. IR(MC,qo)l, and IEl. ~R(%,(so,~o))~ steps are needed to compute the reachability graphs for the plant, the controller, and the closed-loop system, respectively. Hence, at most IEl . (IR(M,so)( IR(Mc,qo)l ~ R ( = , ( S O , steps ~ O )are ) ~needed ) to complete the computations in Procedure 1. Theorem 5: Ifverification is required, Procedure I verifies that

+

+

the closed-loop system has the required behavior. Pro@ As Procedure 1 does the synthesis, by Corollary 3, R(%, (SO, Q O ) ) & R ( M , s o ) x R ( K ,40).It follows from Steps (iii), (iv) and (vi) that R(=, ( S O , Q O ) ) = ( R ( M ,S O ) - R,) x R ( M c ,4 0 ) . This

proves that the composite system model will have the required behavior given by Step (ii). By Corollary 1, it is equivalent to verify that the required behavior of the closed-loop system given by Step (ii) can be deduced from the specification of M given in Step (i) Fig. 10. The simulation results of the composite system. and the specification of the controller given in Step ( i v ) . Therefore, Procedure 1 also does the verification. Now Procedure 1 can be used to do the controller synthesis of Proof: DESs in the temporal logic approach; and at the same time it verifies a) Necessity. It follows from (b) of Theorem 4. that the controller ensures the required behavior of the system. Both Suficiency. Since both S’ = f ( e , s ) is in M and q‘ = f C ( e , q ) Algorithm 1 and Procedure 1 have been implemented in a simulation is in M,, it follows from Definition 11 that e E E(s,q). Hence environment for DESs (see [17]). (s’,q’) = J ( e , ( s , q ) ) is in M . To illustrate this procedure, we return to the given example. In the b) It follows from (c) of Theorem 4. 0 uncontrolled system, there is no restriction on the number of processes By Definition 6, the reachability set R ( g , (SO, 4 0 ) ) is the smallest which are allowed simultaneous access to the disk for either reading set defined by or writing. We need to impose some control on the system so that access is regulated according the following requirements: (SO, 40) E R(M, ( S O , 4 0 ) ) ; Any number of processes can read from the disk simultaneously; If (s, 4 ) E R(=, (so, 40)) and ( S I , 4’) = 7 ( e , ( s , q ) ) for some Only one process can write to the disk at any time; and e E E, n E,, then ( s ’ , Q ’ )E R(=, ( s o , q o ) ) . If a process is writing to the disk then no process may simultaIt follows from Corollary 3 that the reachability set of % is a neously read from the disk. subset of the Cartesian product of the reachable set of M and that Let E Q ( r ,y ) represent that z is identical to y. Following Proof M,. Here the states in are composed of the states of M and cedure 1, we first express the required behavior of the system as M, corresponding to the same events. Using the above results, for a given TLM of a DES plant M , for follows: designing a controller M , and reachability synthesis of M, with M, in order to achieve the required behavior of the closed loop system M , a procedure is developed in the following. Procedure 1 where is the negation. Give the specification of the plant M by temporal logic i) According to the specifications, it is found that R, = formulas describing rules of the state transitions and facts { s ~ oS, ~ S , S ~ Oand } E, = {e40, e43,e4s, e48) (eso = e40, es1 = e451 on the initial states and enable events, and then compute the as shown in Fig. 7. The next step in our procedure is to construct reachability set R ( M ,so). a controller to enable only the events in E, = E r) -E, such that ii) Specify the required behavior RB of the closed-loop system states s40, ~ 4 5 and , sso will not be reached in the closed-loop system. M by temporal logic formulas. The events to be controlled are those which result in a process iii) Check R(M,so) against RB to find out the set of states going from the waiting for reading state to the reading state and from which should not be reached by the closed-loop system. the waiting for writing state to the writing state. In order for the The root: 511 =(W,lD,l.O) e29=(endw 1) ---> 5 2 9 =(ID.ID.O.O)=SO e304erqr 2)=eZ ---> 530 =(W.WR.l.O)-527 e 3 1 4 e r q w 2 b e 4 ---> 531 =(W.WW.l.O)

z

-

I

1405

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS, VOL. 24, NO. 9, SEPTEMBER 1994

so

Fig. 11. The reachability graph of the composite system. controller to know when to permit a process to go from a waiting for reading state to a reading state, for example, it must also monitor the transition of processes out of the writing state and out of the reading state. Hence, the events to be selected and synchronized are those which result in processes entering and leaving the reading and writing states. We use additional local variable symbols u and v to represent the data stored by the controller. u is assigned values 1 and 0 representing if a process is writing to the disk or not; and we write them as predicates EQ(u,O) and E Q ( u , l ) . u is assigned non-negative integer values representing the number of processes which are reading from the disk. Let ADDl(u) stand for that u is increased by 1 and MlNl(u) for that u is decreased by 1. Then, the specifications of the controller are as follows. Dynamics of the Controller

By using Procedure 1, according to the required behavior of the system, a controller was designed and synthesized, and the behavior of the closed-loop system was obtained. From Figs. 2, 7 and 10 one can see that R ( a ,( s o ,q o ) ) = ( R ( M ,so) - R,) x R(M,, q o ) . This proves that the resulting composite system has the required behavior. By Procedure 1 and Theorem 5, we have also verified that the required behavior of the closed-loop system given by ( C L 1 ) - (CL2) can be deduced from the specifications of the read-write process given in ( P l ) - ( P 7 ) and the specifications of the controller given in ( C l ) - (C5). As we can see from these figures, the resulting composite system has the required behavior: the states s40, s45, s50 were eliminated by the controller. In this example, the controller synthesis procedure indeed does a formal verification. As this procedure takes the specification of the plant and synthesizes a controller according to the required behavior description, it proves that the required behavior description can be deduced from the specification of the plant and the controller design by using the reachability algorithm. The reachability properties verify the validity of the temporal logic formulas. VI. CONCLUSION

Initial Condition of the Controller

The state transitions of the controller are given in Fig. 8 to show its dynamic behavior. The controller synthesis procedure is illustrated graphically in Fig. 9 where ADDl(u) and MZNl(u) together with EQ(IJ,0) are used for counting the number of the processes which are reading from the disk, while EQ(u, 1) or EQ(u,0) together with EQ(u, 0) are used for representing if a process is writing to the disk or not. The dynamic behavior of the closed-loop system, which is composed of the plant and the controller, is shown in Fig. 10 and its reachability graph is constructed in Fig. 11.

A temporal logic model (TLM) has been defined by a set of states, a set of events, a mapping, a set of formulas, an initial state, and a labeling function. In reachability analysis of the DES, it has been shown that reachability of states is equivalent to validity of the corresponding logic formulas. Hence, we may use reachability properties to verify the corresponding validity properties. It is noticed that validity here is limited and relative to the logic specification provided by the user in applications; and therefore, it may be invalid if the user is erroneous. Nevertheless, this result theoretically simplifies the system design procedures as it is a bridge between reachability and validity. Based on this result, reachability properties may be used instead of validity properties. Hence, the reachability set has been defined and an algorithm for computing the reachability set and constructing the reachability graph has been developed.

I

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS, VOL. 24, NO. 9, SEFTEMBER 1994

1406

By applying Hennessy’s process algebra, TLMs have been viewed as E-algebras together with the E-homomorphisms between them, and a composition operator has been then defined to provide a basis for the composition of a number of TLMs. Control actions have been achieved by the composition of a controller with the plant. The controller has been designed through reachability synthesis and imposed by synchronization of events in the controller with the selected events in the plant. An example of read-write processes has been demonstrated throughout the paper to convey and motivate the theoretical discussions. Results of simulating this example have been given in Figs. 2, 5 and 10. The simulation was performed in a simulation environment [17] which implements procedures for computing the reachability set, for constructing the reachability graph, for designing a controller and reachability synthesis, and for temporal logic reasoning. As a comparison, our work, presented in this paper, is close to Denham’s work [4]. He uses the two-sorted algebra to do the composition of DESs in the Petri nets approach, while we use E algebra in the temporal logic approach. He uses invariants of the Petri nets to specify the system behavior, while we use reachability of TLMs. The disadvantage of his approach is that an additional language is needed to express the required behavior over a sequence of states. Our temporal logic language allows formal statements to be made which are interpreted over the sequence of states that constitute the dynamic behavior of the system. These can be seen by comparing the results of the read-write example in this paper with the results of the same example in [4]. Of course, there are parallel research efforts in DES formalisms in discrete event simulation area. For example, Operational Evaluation Modeling for context sensitive systems in [3] is claimed as far superior to Petri Nets. Based on the temporal logic framework, introduced and developed in this paper we also devised and implemented a visual programming environment for the simulation, analysis, and synthesis of DESs; and this will make the subject of another paper. Further comparing other related works, our work in Section I11 is close to the corresponding parts of Ostroff [20], [21]. Particularly, our Algorithm 1 is similar to his Procedure 7.1 [20]; but we have the set E, which is more convenient to use than his enable checking. The main difference between his work and ours is that he uses the extended state machine as the model for his real-time systems, while we use temporal logic model for DESs. Specifically, our usage of reachability and the reachability graphing are different from his. He used even more complicated reachability algorithms in his decision procedures for properties such as invariance and eventuality, but he did not claim that validity of logic formulas is equivalent to reachability of states in a system state-event graph as we did. Our contribution concerns the conversion of the verification procedure for validity of logic formulas into the reachability computation. Furthermore, we use this result to develop a controller design and synthesis procedure through the reachability properties such that the verification is carried out as soon as the procedure synthesizes the controller with the plant into the closed-loop system. ACKNOWLEDGMENT

The authors would like to thank all the reviewers for their helpful comments and suggestions. REFERENCES

[l] G. V. Bochmann, “Hardware specification with temporal logic: An example,” IEEE Tram. Computers, C-31, pp. 223-23 1, 1982.

E. M. Clarke, E. A. Emerson and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Trans. Programming Languages and Systems, 8, pp. 244-263, 1986. J. R. Clymer, D. J. Cheng and D. Hernandez, “Induction of decision making rules for context sensitive systems,” SIMULATION, vol. 59, pp. 198-207, Sept. 1992. M. J. Denham, “A Petri-net approach to the control of discrete-event systems,” In M. J. Denham and A. J. Laub (Ed.), Advanced Computing Concepts and Techniques in Control Engineering, NATO AS1 Series, vol. F47, Springer-Verlay, Berlin, pp. 191-214, 1988. H. A. Enderton, A Mathemafical Introduction to Logic Academic, Press, New York, 1972. A. Fusaoka, H. Seki and K. Takahashi, “A description and reasoning of plant controllers in temporal logic,” Proc. 8th Int. Joint Con$ on Artijicial Intelligence, pp. 405408, 1983. A. Galton, Temporal Logics and Their Applications, Academic Press, London, 1987. M. Hennessy, Algebraic Theory of Processes, The MIT press, Massachusetts, 1988. Y. C. Ho, X. R. Cao and C. G. Cassandras, “Infinitesimal and finite perturbation analysis for queueing networks,” Aufomafica,vol. 19, pp. 439445, 1983. K. Inan and P. Varaiya, “Finitely recursive process models for discrete event systems,” IEEE Trans. Automat. Contr., 33, pp. 626-639, 1988. J. F. Knight and K. M. Passino, “Decidability for a temporal logic used in discrete-event systemanalysis,” Int. J. Control, vol. 52, no. 6, pp. 1489-1506, 1990. F. Lin, “Analysis and synthesis of discrete event systems using temporal logic,” Proc. 1991 IEEE Int. Symposium on Intelligent Control., Arlington, Virginia, Aug. 13-15, 1991, pp. 140-145. J.-Y. Lin and D. Ionescu, “A generalized temporal logic approach for control problems of a class of nondeterministic discrete event systems,” Proc. 29th IEEE Con$ Decision & Control, Honolulu, Hawaii, Dec. 5-7, 1990, pp. 3440-3445. J.-Y. Lin and D. Ionescu, “A symptotic behavior of output feedback for a class of nondeterministic discrete event systems,” Int. J. Control, vol. 54, no. 4, pp. 903-920, 1991. J.-Y. Lin and D. Ionescu, “Verifying a class of nondeterministic discrete event systems in a generalized temporal logic framework,” IEEE Trans. Sys., Man and Cybern., vol. 22, no. 6, pp. 1461-1469, 1992. J.-Y. Lin and D. Ionescu, “A simulation language for discrete event systems in a temporal logic framework,” Proceedings of CCECE 92, Toronto, 13-16 Sept. 1992, pp. MM6.3.1-MM6.3.4. J.-Y. Lin, “A temporal logic approach to the analysis and synthesis of discrete event systems,” Ph.D. thesis, Dept. Electrical Engineering, University of Ottawa, 1993. Z. Manna and A. Pnueli, “Verification of concurrent programs: A temporal proof system,” Foundations of Computer Science N, Mathematical Centre Tracts 159, Mathematish Centrum, Amsterdam, pp. 163-255, 1983. Z. Manna and A. Pnueli, “Proving precedence properties: the temporal way,” Automata, Languages and Programming, Lecture Notes in Computer Science 154, pp. 491-512, 1983. J. S . Ostroff, Temporal Logic for Real-Time Sysfems. John Wiley, New York, 1989. J. S. Ostroff and W. M. Wonham, “A framework for real-time discrete event control,” IEEE Trans. Automat. Control, vol. 35, pp. 386-397, 1990. J. L. Peterson, Petri Net Theory and the Modeling of Systems. PrenticeHall, Englewood Cliffs, 1981. A. Pnueli, ‘The temporal semantics of concurrent programs,” Theoret. Comput. Sci., 13, pp. 45-60, 1981. P. J. Ramadge and W. M. Wonham, “Supervisory control of a class of discrete event process,” SIAM J. Contr. Optimiz., 25, pp. 20C230, 1987. J. G . Thistle and W. M. Wonham, “Control problems in a temporal logic framework,” Int. J. Control, 44, pp. 943-976, 1986. G . Winskel, “Event structures,” Petri Nets: Applications and Relationships to Other Models of Concurrency. ed. W. Brauer, W. Reisig and G. Rozenberg. Springer-Verlag, Berlin, pp. 325-392, 1987. W. M. Wonham, “A control theory for discrete-event systems,” Advanced Computing concepts and Techniques in Control Engineering. ed. M. J. Deham and A. J. Laub. Springer-Verlag, Berlin, pp. 129-169, 1988.

.