First-Order Logic Models for Real-Time, Discrete-Event Systems Arch Naylor Universityof Michigan May, 1993 Abstract A methodology based on first-order logic for modeling discrete-event systems is introduced. Time is the real line, and systems are allowed to have an infinite number states. Applications of the modeling methodology are presented. 1. Introduction Our purpose is to introduce a dodeling tnefhdology foi;discrete-event systems [1, 2, 3, 4] and to demonstrate its use. Th' ^ietho4b i'i. "e first-order logic [5]. We use logic because most discrete-event syst`ps "zei'a e zed by logical conditions and quantities, and we choose first-ordr lo heci's1itslsby far the most widely known and developed version of logic. And, first;ec,ea p will show, expressive enough to model the phenomena of interest. In par tcifhrWt'tan have real time, simultaneous events, and infinite state sets, yet still obtain classes of tractable models. However, even though first-order logic is the best known version of logic, few know more than introductory concepts, and setting up our modeling methodology requires more. Fortunately, using the methodology does not. Here we will cover the background technical issues but in a largely segregated manner. Thus, a reader willing to accept things on faith can skip over their discussion. Another possibility would have been to do everything semantically in terms of sets, ignoring syntax and the connections to logic. However, we would still have to reason about these sets, and that would mean we were back to logic, but in an informal, somewhat disorganized, manner. We believe an orderly theoretical foundation is better. It allows us to use known facts of first-order logic. For example, Beth's theorem [6, page 87] is very useful. 1

The modeling formalism yields models that are systems of what we call pseudodifferential-difference equationsl. They are analogous to systems of ordinary differential difference equations, and they are used in the same way. That is, one tries to find closedform solutions where they exist; one deduces properties of solutions from the form of the system of equations; one uses approximations such as linearization, and one exercises the system of equations in simulations. 2. Dynamic and Static Quantities We view a discrete-event system as being made up of dynamic and static quantities. The dynamic quantities are predicate-valued and function-valued functions of time. Example 1 Time is the real line R?. Vehicles are in a set V of ten vehicles. There are twenty locations in a set L. The predicate Loc.(r,v,~), that is, some subset of the Cartesian product Rt x V x L, keeps track of vehicle location. We view Loc_(r,v,~) as a mapping of t into VXL, the power set of V x L. That is, we view it as a predicate-valued function of time. For example, if < 1, V, e7 > and < 1, V3, e2 > are the only ordered triples in Loc. with r = 1, then the value of Loc- at time 1 is the predicate {< vI, 7 >, < v3, 2 >}. Vehicle 1 is at location 7, vehicle 3 is at location 2, and no othet vehicle is at a location; that is, they are between locations. Example 2 In Example 1 the predicate Loc-(r, v, ~) might contain both < 1,v,e~ > and < 1,v, 12 >, that is, it might specify that vehicle 1 is at two' different locations at the same time. In some systems this might notbe physically possible, and the model would presumably have to reflect this constraint. One way to reflect it is to reqi're that the sentenuce (Vtr)(r) = (Vtr)(Vv)(V)(V') [Loc4r, v, l) A Loc(T, v,') -- (~ =')] (1) be satisfied, that is, if v is at I and I' at time r, then I and I' have to be the same. Using this approach would require that we would have to show that ib was satisfied initially and that no subsequent event causes (Tr) not to be satisfied. This is a reasonable approach, and there are many situations in which this technique is used. Indeed, it is a simple example of supervisory control which we discuss later. Example 3 Another approach to the problem addressed in Example 2 is to replace the predicate Loc_(r, v, I) by a function Loc_(r, v), that is, by a mapping of Rt x V into L. Loc_(r,v) can be viewed as a function-valued function of time; in particular, at any fixed 1A related approach is presented in [7]. 2

time r, Loc-(r,v) yields a mapping of V into L. This mapping assigns a unique location to each vehicle at time r. Since Loc- is a function, we do not need sentence 1. On the other hand, since Loc- is defined on all of? x V, a vehicle is always at some location, that is, a vehicle cannot be between locations. We will organize dynamic quantities into dynamic predicate families and dynamic function families. A dynamic predicate family is an ordered pair of predicates {P-(r, xl,...xn), 6P (r, x1,..., xa)}. We call this a family because, as we will explain below, 6P is supposed to be what we call the pseudo-derivative of P_. We say "supposed to be" because it is not always the case for technical reasons which we will also explain below. Similarly, a dynamic function family is an ordered pair {F.(r, x1,..., xn), 6F(r, xl,..., n, y)}, where F_ is a function and 6F is a predicate. 6F is supposed to be the pseudo-derivative of the predicate defined by (y = F. (r, 1,..., Xn)). Quantities that have no occurrence of time are said to be static. Further, and a bit inconsistently, some quantities with occurrences of time are still classified as static. For example, addition of two times certainly has occurrences of times, but we say that this addition is static. Dynamic quantities are really things that are dynamic in the discreteevent system being modeled. Each dynamic family is classified as either endogenous or exogenous. The endogenous families are inside the system and the exogenous ones are inputs. 3. C, Language Each model of a discrete-event system is expressed in terms of a first-order language L [5, page 67] that is appropriate for the system being modeled. Such a language has variable and constant symbols, predicate and function symbols, and logic symbols. There are the usual syntactic rules for combining these symbols into well-formed formulas [5, page 73] and sentences [5, page 75]. The language is "appropriate" in the sense that its constant, predicate, and function symbols are associated with entities and concepts of interest in the system being modeled. Each model of a discrete- event system is a collection of sentences over a language C. Remark 1 Logic has a syntactic and a semantic side. An example of the syntactic side is a predicate symbol Loc, and an example of the semantic side is a predicate that provides a meaning or interpretation for the symbol Loc-. Predicates P1i(r, v, 1) and P2_(r, v, I) might be two different interpretations. Thus, there are predicate symbols and predicates. Often authors will use different notations for these two concepts, for example, Loc- for the symbol and Loc_ for a predicate. Here, however, we will risk a bit of confusion by using the same notation for both concepts. 3

Remark 2 An interpretation for a first-order language is a collection of interpretations of the constant, predicate, and function symbols over one or more universes of discourse. This is usually called a structure [5, page 79] for the language. There are many structures for any first-order language. A structure is said to satisfy [5, page 81] a first-order sentence a if a is a true statement about the structure. It satisfies a set of first-order sentences if it satisfies each sentence in the set. We will denote a model of a discrete-event system by E. The sentences in E are subdivided into the following subsets: * ET, the sentences defining time * EPD, the sentences defining pseudo-differentation * EDEB, the sentences defining discrete-event behavior * ERS, the sentences defining the right sides of the pseudo-differential- difference equations * Zs, the sentences defining other static quantities * Z,, sentences added to support universal quantification over time Initial conditions and inputs are specified by a set of sentences ZIC&E:. A set of sentences ZH connects initial conditions to the original dynamic quantities. We will denote E U IC&E U EH by Et. Remark 3 The subsets ET, ZPD, 2DEB and Ew are essentially common to all models. They will differ only because the underlying first-order languages differ. In a sense, this part of j defines the mathematical environment of a model. Logical models are peculiar in that they contain everything that may be needed. In models using ordinary differential equations, one need not include a definition of differentiation as part of the model: it is implicit. In contrast EPD C E- Of course, as long as F is going to be worked with only "by hand", much of it can be made implicit, too. However, any automated use of E will have to include everything in one way or another. Remark 4 In the basic version of first-order logic, all the symbols in a structure are interpreted with respect to one universe. Thus, time and parts and vehicles and locations are mized together into a common universe of discourse. This is sometimes awkward, so different categories are sometimes interpreted with their own separate universes of discourse. Thus, there would be a universe for times, another one for parts, another for vehicles, another for locations, and so on. To do this, one uses what is called a many-sorted first-order language [5, page 277]. For example Loc (r, v, I) could be many sorted with r a symbol of the sort time, v of the 4

sort vehicle, and I of the sort location. A structure then requires a set T for times, a set V for vehicles, a set L for locations, and Loc. is a subset of? x V x L. If, instead, we did not use a many-sorted language, a structure would have a common universe U, and Loc. would be a subset of U x U x U. But we would need additional predicates to say what subsets of U were times, vehicles, and locations, respectively. For example, T(x), V(y) and L(z) would define times, locations, and vehicles, respectively. Then we would need sentences saying that the defined sets were pairwise disjoint, for example, (Vx)(-n(T(x) A V(x))). And so on. In summary, then, many-sorted languages simplify things, so our models will use them. However, to simplify things even further, we usually let the many-sortedness be implicit. Example 4 A transport system has one vehicle which moves from one location to the next when a move command is given. The route is a fixed loop. There are two sorts: time and locations. The endogenous dynamic families are {W-(r, 1), bW(r, 1)}, and {S-(r, 1, Ta), 6S(r, 1, Ta)}. W. models "Where is the vehicle stopped now?" Its value at any time is either the empty set or a set containing a single location. The value of 6 W is empty at all time except those where a move starts or finishes. S models an ongoing move with r denoting the current time, I denoting the destination location, and Ta denoting the scheduled arrival times. If there is no move currently in progress, the value of S. will be the empty set. The value of 6S at any time is empty except at the start and finish of moves. The single exogenous dynamic family is {MA(r), 6M(r)}, which models move requests. This model has an infinite state set because Ta can be any real number. 4. ET, Time Time is the real line t. Remark 5 However, there is a technical issue. Our modeling methodology is developed within first-order logic, but we want time to be the real line. Unfortunately, we cannot have both. If we insist on defining time as exactly the real line, then we have to go beyond first-order logic, and if we insist on staying within first-order logic, then we cannot define exactly the real line. Let us see why. First-order logic allows predicates, functions, and quantification of only variables which refer to elements of the universe of discourse, for example, (ix) and (3x). Secondorder logic allows predicate and function variables, and it allows quantification of these variables, for example, (VX), (3X), (VF), and (3F). That is, we can make statements such as "there exists a set..." and "there exists a function...". Higher-order logics allow us to talk about sets of sets, sets of sets of sets, and so on. If one looks at a serious definition of the real line in any graduate analysis book, one discovers, once the definition has been translated into an appropriate logical formulation, that the definition uses some higher-order constructs, and, it turns out, that they are unavoidable. 5

Indeed, let rz be the set of all first-order sentences that are true statements about the real line. rR is obviously consistent because 3R satisfies it. Since any first-order sentence a is either satisfied by the real line or not satisfied, rR is complete [5, page 145]. Complete means that for any first-order sentence a either a E rR or a 0 rz and not both. In other words, as long as "first-order questions" are posed, rT contains all the answers, However, if we ask a second- or higher-order question, r3 may not allow us to determine the answer. Suppose that (3 is a higher-order sentence saying something true about the real line. For example, let 3 be (VX) [{(y)(Vz) (X(z) - (z < y)) A (z)X(z) - {(3y)(Vy') ((Vz)(X(z) (z < y')) - (y < y')}] (2) where X is a unary predicate variable symbol. This second-order sentence says that any bounded nonempty set has a least upper bound. /3 is certainly a true statement about the real line, but it does not follow from rR, that is, there are structures that satisfy rR U {a/} (e.g., R) and other structures that satisfy rt U {-i/3}. This means that neither t3 nor -1 can be deduced 2 from rt. /3 is an important property of the real line, then, that cannot be expressed in first-order logic. Consequently, our first-order version of time will not be able to talk about least upper bounds, among other things. Since there are structures satisfying ra U {1-n/} and 3t does not satisfy rR U {n-o/}, there are structures satisfying ra that are not isomorphic to R3. Such a structure is usually referred to as a nonstandard model3 of the real line. The point is that there are structures which satisfy rat that do not "look like" AR. Since we cannot add any first-order sentence 7 to rR because the resulting set of sentences would be inconsistent (i.e., 7 and -my would both be present), we cannot do anything within first-order logic to remove the nonstandard models. But the existence of nonstandard models is really a side effect; the real issue is that there are important things that cannot be expressed in first-order logic. The obvious question, then, is: why not use some higher-order logic? Our reasons for not doing so are, as we have said, (1) there are fundamental technical problems with higher-order logics, (2) first-order logic is well developed, and (3) higher-order logics are familiar to only a relatively few experts. But if we cannot formulate a workable modeling methodology these three reasons are irrelevant. Consequently, we have to show that we can get a good modeling methodology within first-order logic in spite of its limitations. That this is possible is a major result of this presentation. In passing, we note that we will use the existence of nonstandard models to show that certain deductions are not possible. To show that E V a, we will describe a structure 2A technical weakness of higher-order logics is that "not all things that are true" can be deduced. However, this is not the point here.,B is just not a true statement about all structures that satisfy ra. 3The word "model" is used here in two ways. First, there is a model of a discrete-event system. This is a set of first-order sentences A. Second, there is the use of "model" in first-order logic. In that case, a model is the same thing as a structure. That is, it is a semantic interpretation of the first-order language. A nonstandard model of the real line is this latter ind of model. 6

which satisfies E U {-fa}. The first such use occurs in this section. Given, then, that we want a first-order theory of time, what should it be? rR is inappropriate because we do not have a practical way to specify it. Instead, we choose to characterize time with the axioms, denoted here by ET, for ordered real closed fields [6, page 41]. The language is {(, +,, 0,1}, where 0 and 1 are constant symbols. The field axioms are: (V, y,z) [x+(y+z) = (x+y)+z] (VX) [(x + 0 = x) A (0 + x = x)] (Vx)(3y) [(x + y = O) A (y + x = 0)] (Vx,y) [x+y= y+x] (Vx) [lx = xl = 2] (Vx, y, z) [x(yz) = (xy)z] (Vx, y) [xy = yx] (Vx, y, z) [x(y + z) = (xy) + (xz)] (Vx,y) [xy = 0 (x = 0 V y = 0)] 0#1 (Vx) [(x + 0) (3y)(yx = 1)] The order axioms are (Vx) [x < x] (VX, y, z) [(x < y) A (y < z) - (x < z)] (Va y) [(x < y)A (y < x)- ( = y)] (Vx,y,z) [(x < y) - (x+z < y+z)] 0<1 In addition, there is the axiom (Vx)(3y) [(y= ) A (y + x = 0)] (3) and the two infinite sets of axioms, for each n > 0 (Vo, 1,..., an) [(xoX2 xz1 +..+ + = 0) ((xo = 0) A... A (Xn = 0))] (4) and for each odd n > 0 (VXzzo,... Xn)(3y) [(zyn + _ yn +... + x y + xo = 0) V (xn = 0)] (5) The latter two are called axiom schema in that they each describe an infinite set of axioms. 7

The theory of ET, Th(ZT), is the set of all first-order sentences over the language {<, +,), 0, 1} that can be deduced from ET. This theory is complete, that is, if a is a firstorder sentence over {<, +, 7, 0,1), then either a E Th (ZT) or -1a ~ Th (ZT) but not both. However, there are other first-order sentences that are true of the real line. For example, if we add a predicate symbol to describe exponentiation, y", there will be new first-order sentences that cannot be expressed in terms of the language {<, +,', 0, 1}. These sentences will be in Pr but not in Th(ZT). The point is that we are using part of the first-order theory of the real line: Th(ZT) is a proper subset of ra. There are really two models recognized as standard models for ET. The first, (?, <, +,, 0,1), is ordered real closed field in the real line. This is our intended model of time. The other is (4, <, +,.,0,1), where A is the set of all algebraic numbers in the real line. The former is an uncountable model and the latter is countably infinite, so they are not isomorphic. We note in passing that the model (A,<,+,.,0,1) plays a special role in the theory of ordered real closed fields in that it can be isomorphically embedded into any ordered real closed field. Though (?, <,+,.,0,1) is our intended model of time (A4, <, +,, 0, 1) is sometimes referred to for technical reasons. In any event, there is no first-order way to say we mean (3?, <,+, -,0, 1) and not (AI, <, +, *,0, O1). Moreover, there are nonstandard models that are not isomorphic to either of these models. If p is sentence ( 2) about least upper bounds, then any structure satisfying ET U {fP} is isomorphic to (3t,,7+,7,0,). That is, if we add /r, we get precisely the ordered real closed field in?. However, adding even just this one second-order sentence introduces the problems associated with higher-order logics, so we do not add it. 5. EPD, Pseudo-differentiation Consider a dynamic predicate family {P.(r, x1,..., xn), 6P(r, x1,..., xn)}. Our intention is that P- should be left-piecewise constant, 6P should be impulsive, and 6P should be the pseudo-derivative of P. We define these terms in this section. Definition 1 A predicate P(Tr, xl,..., xn) is left-piecewise constant at time r if the following first-order well-formed formula is satisfied by P. at time r. (3rT)(3r,) [[re < r < ru] A (Vr1)(Vr2) [((re < r, T2 < r) V (r < T1, r2 < r,)) (V (Ai,,) P 1,..., Xn) {P(r+,, P.(T2, 1, X, X.,)}]] (6) Remark 6 Our convention is to use a "-" subscript to denote dynamic predicates and functions that are normally left-piecewise constant. Those that are right-piecewise constant will have a U+'f subscript. 8

Remark 7 In a nonstandard model of ZT it is possible that (r, - r7) could be a so-called infinitesimal [5, page 164] even though it is greater than zero, that is, it could be smaller than each algebraic number. Or (7r - 7T) might be greater than each algebraic number, that is, it might be an infinite number. Either case is a technical curiosity because any firstorder statements we deduce will be correct statements about all possible models of time, in particular, about the real line which is the one that we care about. Definition 2 A predicate 6P(r, xl,..., xn) is said to be impulsive at time r if the following first-order well-formed formula is satisfied by 6P at time r. (3re)(3Tu) [[ir < r < ru] A (Vr') [((T < r < r) V (r < r < ru)) - (V17,..., n)(-6P(-r1,,,Xn))]] (7) That is, 6P is empty for time sufficiently close to r, and it may or may not be empty at exactly r. If it is nonempty, we say that there is an impulse at 7. Remark 8 Remark 7 about nonstandard models applies here also. Remark 9 We will usually use a "6" prefix as in "6P" to denote dynamic predicates that are normally impulsive. Rather than define the pseudo-derivative at one time, we have to define it in a neighborhood of a time; otherwise, we do not capture the intuitive idea of 6P being the step change in P_. Definition 3 A predicate 6P(r, xi,..., an) is the left pseudo-derivative of a predicate P-(r, xi,..., xn) in a neighborhood of a time r if the following first-order well-formed formula is satisfied by 6P and P_ at time r. (3r-)(3ru) [rt < r < ruJ A [(Vr')(re < r < r) -) [(3r)(3ru') [r <'r < r < r < r] A [(vri)(Vr2) ((r; < r < r)A (r < r2 < r)) - (VXi,..., n) {P(r' xi,..., n) (P-(1i, i,...,,n) + P-(r2, X,..., xn))}]]] (8) where "+" denotes symmetric difference. TI and ru establish an open neighborhood of r in which 6P is the pseudo-derivative of P_. In particular, for each r' in this open neighborhood there is an open neighborhood of r defined by r\ and rT. Then for any 1r and r2 in this latter neighborhood with Tl ~ r and rt < r2 we have that 6P(r', x,..., Xn) is the symmetric difference of P-(ri,x1,,..., n) and P-(r2,xi,..., Xn). The following lemma shows that the above definition captures the intuitive idea of pseudo-derivative. 9

Lemma 1 If 6P is the left pseudo-derivative of P. in a neighborhood of time r, then 6P is impulsive and P_ is left-piecewise constant at time r. Proof: Let r = r. We know that there are rt and T% such that 6P(-r, l,...,xn) P-(r1,x1,...,zn) + P-(r2,x1,...,xn) for all (rt < 71 < r) A (r < r2 < ru). From this we conclude that P-(r3, x,..., n) is constant for rt < T3 < r and for r < T3 < r which shows that P. is left-piecewise constant at time r. Let r4 satisfy r< < r4 <7. Since 6P is the left pseudo-derivative at P., we have 6P(r4,x1,..., xn) - P-(75, x,..., xn) + P-(T6, x1,..., n) for all r5 and r6 is an open neighborhood of r4 contained in the interval (rt,r. Since it is constant in this neighborhood of 74, ~-P(r4,x,..., n) is satisfied. Therefore, 6P is impulsive at time r. Henceforth, we will drop "left" from "left pseudo-derivative". Remark 10 Note that had we defined pseudo-derivative at a point rather than in a neighborhood, the above lemma would not be true. So far we have said that "6P is supposed to be the pseudo-derivative of P_". We formalize this idea with a first-order sentence that says that if 6P is impulsive at time 7r, then it is the pseudo-derivative of P. in a neighborhood of time r. That is, for each dynamic family we require that the following sentence be satisfied. (Vr) [{Formula 7} -* {Formula 8}] (9) These sentences are part of ZPD. The rest of ZPD is required for technical reasons. The additional sentences say that if 6P is empty over any time interval, then P. is constant over that interval. These sentences are (Vru)(Vr<) [{(Vr) ((rt < r < rU) D (VXI,..Xn) (-6P( x1t x...,Xn)))} {(V1r)(Vr2)((rt < T1,T2 < Tu) -- (VX1,...,aXn)(P-(T1,1,...,Xn) (-. P4-(2, l,..,aXn)))}] (10) (VrT) [{(Vr) ((rt < r) -^ (Vaxl,.., ) (IP(r, xi..n)))} {(V71)(VT2) ((r< < 71 T2) (V21,..., an) (P-(ri, 21 i... an) ++ P-(72, xI,..., X)))}] (11) (Vru) [{(Vr') ((r < ru) -- (VXI..,XAn) ('6P(r,ZX,...,)))} {(Vr1)(Vr2)((71,T2,< TU) -) (VXa,1,Xn)(P-(71,x1,... an) < — P-(72,a21,xi...,n)))}] (12) Remark 11 We need the second set of sentences in >PD because it is not implied by the first set. The reason is, once again, that there are nonstandard models of time. 10

6. EDEB, Discrete-event Behavior 6P. Remark 12 There is no first-order formula which defines a finite time interval and none that defines a finite set, so we have to get at discrete-event behavior indirectly. We do so as follows. Definition 4 A predicate family {6P, P-} is said to have discrete-event behavior if the following sentences are satisfied. (Vr,)(Vru) [(re < r,) -- (3e)(0 < e) A (Vri)(V72) {((r < 1, 72 < 7u) A (1 + 2)^ (3ax,..., xn)xP(, x,..., 2n) ^ (3xi,..., xn)P(r2, xi,..., ) -+ (E < |I - T21)}] (13) (Vr) [(3rf)(r < f ) A (31,..., xn)6P(rf 1,i,...,n) X - (3rn)(r < rn) A (3x1i,.., n)P(rn, 1,...Xn) A(V7) {(T < b < rn) - (V1,...,xn) (-P(7b, 2,..., ))}] (14) (Vr) [(37f)(rf < r) A (3x,..., xn)6P(rf, xi,..., Xn) -* (3rp)(rp < r) A (3x1,..., xn)P(rp, x1 i, Xn) A(Vr) {(rp < re < r) -) (wV1,..., xn)(-nP(r,, x,...,))}] (15) The above sentences for each dynamic family are the set EDEB. The first sentence says that in each interval defined by rt and rT, there is a lower bound e on the spacing between impulses of 6P. The second sentence says that if there is an impulse after time r, then there is a next impulse after r at time r7. The third sentence says the same thing about predecessors. Remark 13 We need all three sentences (IS), (14), and (15); for example, ET U {first sentence} does not imply the second sentence. That is, there are structures satisfying ET U {first sentence) which do not satisfy the second. For example, let T be a nonstandard model of time with the real line aR embedded in it and with positive infinite times. Let 6P be nonempty at 0 and empty everywhere else in R. Further, let there be a doubly infinite sequence {k)}, k =..., -1, 0, 1,..., of positive infinite times (i.e. xk is greater than every real number ) such that Xk+l = Xk +1 for all k. For times in T-R, let 6P be nonempty at exactly these times. This 6P will satisfy the first sentence but not the second. In particular, there is no next impulse after time 0 even though there are impulses after time 0. 11

Remark 14 A variation on the Definition (4) replaces the first sentence by one that treats only intervals of length one. This definition is implied by Definition (4) but not vice versa. However, this is another technical curiosity because they are equivalent when restricted to the real line. Remark 15 Yet another technical curiosity is that for a nonstandard model of time a predicate 6P can have discrete-event behavior with the bound E being an infinitesimal, that is e is greater than zero but less than every algebraic number. So we might have 6P satisfying Definition (4) with an infinite number of pulses between 0 and 1. Again, we do not care about this possibility because every first-order sentence applied to the real line will have a standard and familiar meaning. 7. ZRS, Pseudo-differential-difference Equations Consider a simple ordinary differential-difference equation dx/dr = f(x(r), x(r - 1)). The right side f gives a function of time, the left side says that if f is the derivative of something, then one of them is x. We use this two part view as a model for our pseudo- differentialdifference equations. EPD covers one part. A set of first-order sentences ZRS - "RS" for "right sides" - covers the other part. For each endogenous dynamic predicate symbol family we have a sentence in ERS defining 6P for times greater than or equal to the initial time To. Example 5 Continuing the transport system example, the pseudo-differential-difference equations for the two endogenous families are (Vr) [(Tro r) -- (tl) {W(r, 1) I. ((tM(r) A W(r, I)) + ((r = r,) A S-(r,, ra)))}] (16) (Vr) [(o < r) -. (Vl)(VrT) {6S(r,, 1,) T (17) ((6M(r) A [W(Tr, PL(I)) A (ra = r + 1)]) + ((r = ra) A S-(T, 1, ra)))}] (18) that is, 6W and 6S have impulses when moves start or finish, and a move takes one second. PL is a function symbol denoting the "predecessor location" in the fixed loop. PL is an example of a static symbol. We refer to the subformula to the right of "" as the "right side". Remark 16 We will usually drop the outer (Vr) and the leading (r0 < r) -+ and consider them implicit. The sentences in ERS are the heart of a model because they specify when events occur and what the events are. Right sides are usually causal in the sense that their current value is independent of the future. Our models allow "parallelism" in the sense that pseudodifferential-difference equations can easily model more than one event occurring at a time. 12

8. Es, Static Quantities These sentences define static quantities other than those defined in ET. ZS has no particular form; it depends on each particular case. 9. EH, Histories Histories are convenient for specifying initial conditions. The histories H_ and 6H with respect to a time rh of P_ and 6P, respectively, are defined by (Vr)(VXi,..., X)(Vrh) [H_(r, X1,..., X,, Th) ( (r < rh) A P-(r, X1,..., n) +(h < r) A P-(rh,...,,X)] (19) and (Vr)(V1,, Xn)(VVa) [(H(r, x1,...[, X, 7h) ( (r < rh) A 6P(6, 1,..., X,)] (20) That is, the history of P. with respect to 7h agrees with P. up to and including 7h and is constant for times greater than or equal to rh. The history of 6P with respect to 7h agrees with 6P for times less than rh and is empty for times greater than or equal to 7rh. There is a pair of such sentences for each endogenous4 dynamic family. The set of these sentences is denoted EH. Each {H, 6H} is a new dynamic symbol family that is included in the language C, and like all dynamic families it is required to satisfy EPD10. EIC&Ez, Initial Conditions and Inputs Initial conditions are conditions on histories with respect to the initial time To. The set of inputs are, again, the exogeneous dynamic families. The set of sentences ICjC E3: characterizes both. It always says that each H. is constant for ro, r and that each 6H is empty for ro < r. It also says that each family {H._, 6H} has discrete-event behavior. Often the needed initial conditions are conditions on the history H_ at only r = To, that is, conditions on H(ro, xi,..., xXn, T). This is usually the case with pseudo-differential equations. In such cases we will additionally require that H_ be constant for r < To and SH be empty for r < ro. We could have truncated time to [ro, oo), but it is more convenient to have time be? in all cases. So we accept the minor cost of having to be concerned with the histories for all times, even when most of these times are irrelevant as far as the solution of interest is concerned. 4We do not bother with histories of exogenous dynamic families in E because they do not have initial conditions, at least not in A. 13

At one extreme each history and each input can be explicitly defined by a first-order formula that uses only static symbols. For example, H_(r, x,y, To) - (x = c1) A (y = C2) (21) where cl and c2 are constant symbols in L. Here H_ is constant for all time. 6H(r,x,y, ro) -1 (22) that is, 6H is empty for all times (I is false), and 6I(r) - ( = = 10) V (r = 32) (23) that is, there is an impulse at times 1, 10, and 32. The problem with the above explicit way of characterizing initial conditions and inputs is that it is too limited. We need implicit characterizations. For example, a periodic input might be characterized. 61(0), (Vr) [6I(r) 6I(r + 1)], (Vr)(VT1)(Vr2) [(r < r1, 2 < r + 1) A 6(T1) A 6I(r2) ( - (r1 = -2)] (24) The first sentence says that there is an impulse at 0, the second says that 61 is periodic, and the third says that any open interval of length 1 contains at most one impulse. This is an example of a 61 that cannot be defined explicitly as we did above. Remark 17 Denote the union of ET and the sentences (24) by 2sI. We make a distinction between E6I being an implicit characterization of 61 and,6I being an implicit definition of 61. The phrase "implicit characterization" is not formal, any set of sentences can be one. On the other hand, "implicit definition" has a precise meaning. Definition 5 FSI defines 61 implicitly [6, page 87] if E i,(I U ) U (2) (Vr) [61I(r) 62(r)] (25) where 61I and 612 are new symbols, and 2s61(6I) s 2,61 with each occurrence of 61 replaced by 61i, i = 1,2. The above definition says that there is only one I6 over a given model of time. Beth's theorem says that 2,6 defines 61 implicitly if and only if 61 has an explicit definition. 61 has an explicit first-order definition if there is a first-order formula 4f with no occurrence of 61 such that (Vt) [6(T) -,(T)] (26) 14

is implied by 6jI. However, it is not difficult to find two different 61's over the same model of time. For example, let T be a nonstandard model of time that contains R? as a proper subset and with infinitesimal and infinite times. Let 6I and 612 agree on R but be shifted by 1/2 with respect to one another on the rest of T. Both satisfy Zuj but are different. Therefore, ZSI is not an implicit definition of 61. Consequently, 61 cannot be defined explicitly. The point, then, is that EIC&Ex need not be made up of explicit definitions of histories and inputs. Remark 18 However, it is always possible that the first-order theory of the histories and inputs will be complete. That is, Th(SB U ZIC&E.) is complete, where EB is the mathematical background needed to support CIC&E,. Typically, ZB contains ET and Es plus the parts of EPD, EDEB, and E pertaining to historics and inputs. It also usually contains the part of EPD referring to historics and inputs. ZB will also contain the part of joo referring to historics and inputs. The point is that Th(EB U YIC&E.) can be complete even if there is not an implicit definition. Remark 19 We refer to complete theories and completions of theories in a number of places. It should be appreciated that it is impractical to try to determine if an arbitrary set of sentences has a complete theory. Complete theories and completions have a mainly theoretical interest. In fact, even if we have not given a complete first-order description of the histories and inputs, it can easily be that what is missing is merely a technical curiosity. For example, the sentences (24) together with EB do not have a complete theory. Nevertheless, the standard model is uniquely defined (but not in first-order logic). The point is that we have enough information to characterize the things of practical importance. 11. Solutions A solution for given initial conditions and input is any standard structure that satisfies Et = E U CIC&Ex U LHY We also call a solution a trajectory. EH is needed to connect EIC&Ex and I. Remark 20 "Standard structure" is not a technical phrase, and it is, of course, not definable within first-order logic. It does, however, say what our actual intention is. Remark 21 Two structures are said to be elementarily equivalent [6, page 32] if they both satisfy exactly the same set of first-order sentences. Complete first-order theories and elementary equivalence classes of structures go together. Given a complete first-order theory, 15

the class of all structures satisfying this theory is, by definition, an elementary equivalence class. Given an elementary equivalence class, each structure satisfies the same complete theory. The point is that technically we work with elementary equivalence classes or, equivalently, complete theories whether we say "standard structure" or not. 12. Existence of a Solution Most ordinary differential equations have a solution for a given input and set of initial conditions. Those that do not are usually of limited interest for systems applications. This is not the case for pseudo-differential-difference equations. A solution can easily fail to exist in an important way because we require that solutions have discrete-event behavior. This is illustrated in the next example. Example 6 The system being modeled has two entities which alternate between being in a predicate; as soon as one is in the predicate it is immediately replaced by the other one. Obviously, there will be an infinite number of alternations within any finite interval. In those cases, where neither or both entities are in the predicate, the system does nothing. The model has one endogenous family {C4r, x), SC(r, x)} and two constant symbols "a" and "b". There is no exogeneous family. The initial time is 0. The only static condition, other than those in ET, is a sentence saying that a and b are different. The pseudodifferential equation is SC(r, x) 4- [{C-(r, a) + C_(r, b)} A ((x = a) V (x = b))] (27) That is, a and b alternate whenever just one of them is in C_. There are two cases to consider, depending on the choice of initial conditions. First, suppose that only one of the entities denoted by a and b is in C- at time 0. In that case SC(0,x) is not empty. This means that a and b are interchanged at time 0. If {C-, 6C} has discrete-event behavior, there is supposed to be a time interval of nonzero length over which C_ is constant and EC is empty. But immediately after time 0, SC is again nonempty, which is a contradiction. In other words, for these initial conditions, E U EIC&Ez U 2H is an inconsistent set of sentences. On the other hand, it is not difficult to construct a structure satisfying A U FIC)EJ U EH - EDEB. For example, let C. contain a on the rational numbers and b on the irrational numbers. The resulting S C is not impulsive anywhere, so it does not have to be the pseudo-derivative of C_. That is, if we drop EDEB we obtain a consistent set of sentences. The point is that for these initial conditions the system is attempting to alternate too fast to have discrete-event behavior. Second, suppose that both a and b or neither is in C. at time 0. In this case it is easy to see that there is a solution with C- constant and 6C empty for all time. Here, then, 16

E U ZIC'&Ex U EH is a consistent set of sentences. And, of course, (Z U EIC&Ex U ZH) - EDEB is also consistent. Further, any structure with discrete-event behavior satisfying E U ZIC&Ez U iH will satisfy (E U ZIC&E U'H) - EDEB However, there are also structures without discrete-event behavior satisfying this latter set of sentences and not the former. The point is that the existence of bizarre structures satisfying (I U ZIC&Ex U HE)EDEB is physically significant only when I U EIC&EI U EH is inconsistent. From one point of view there is a solution if E U SIC&ES U EH is a consistent set of sentences. However, we are not interested in any solution; we want "standard solutions". Each sort has a standard interpretation (e.g., the real line for time, the natural numbers for counting and arithmetic, etc.), and we are concerned with the existence of solutions based on these standard interpretations. The usual way to proceed is to construct a structure that (1) satisfies E U ZIc&EI U EH and (2) uses the standard interpretations. That is, one shows the existence of a solution by constructing one. And, when doing so one may use any part of mathematics that helps with carrying out the construction, that is, we are not limited by first-order logic in our search for a structure satisfying U EIC&Er U fH' Assuming that there are no inconsistencies in ( U ZIC&EZ U ZH) - EDEB, the construction will hinge on showing that the impulses in 6C's will have to be separated from one another in time. Usually, this is not a major problem. Remark 22 The above argument is vague. Ideally, we would like to be able to say that there is a standard solution if and only if M U EIC&Ez U EH is consistent. However, the author does not have a way to guarantee that this is the case. However, even if the author had such a guarantee, showing consistency would still reduce to constructing a solution as sketched above. In summary, existence is not a crucial practical problem for ordinary differential equations, but it may be for our equations. Thus, the question cannot be completely ignored. We have to be assured that we have discrete-event behavior. 13. Explicit Solutions As in the case of ordinary differential-difference equations, some, but definitely not all, pseudo-differential-difference equations have "closed form" or explicit solutions. Let bP(r,...) +-+(P-,H)(r,...) (28) be some pseudo-differential equation, and let Tr be the defined initial time. An explicit solution is a pair of first-order formulas -(r,...e) and 6b(r,...) with no occurrence of P. or 17

6P such that (Vr)[( < 70) - (V...) (, H(..., T) )} (Vr) [(r < r) (- (V...) {6(r,...) -+ (r,..., ) }] (V7) [(7 < 70) > (V@@). 6.(T. *.) t- b(7,.-,TO) }] (Vr)[(r0 < r) - (V...) {P(7,...) - (7,...) }] can be deduced from ct. Showing that the first and third sentences can be deduced is usually trivial because the histories of -, and 64, with respect to r0 will always be defined to be H-(,..., 70) and 6H(r,..., To). The challenge is to find the rest of -b and 64. Example 7 Consider 6P(r, x) + 61(r) A (x = c) A P-_(, X) (29) where c is a constant symbol and T, = 0. In this case the following is the 4, part of an explicit solution -(r, x) Z [(r < 0) + {(O < r) A [(x i c) + (x = c) A (Vr') ((0 <' < r) -+ JI(r'))]}] A H_(r, X,0) (30) where, recall, H_(r,X, O) is constant for 0 < r. Thus, for r < 0 _, is the history, and for (0 < r) 4-, is constant until the first impulse of 61, if there is one. Then the element denoted by c is deleted from the value of H- if it is present; otherwise, nothing happens. Subsequent impulses have no effect. If the first impulse occurs at 0, then c, if present, is deleted at time 0. Remark 23 Having an explicit solution is a fairly strong property. It says that for every structure that satisfies Et the solution is represented by the formulas {4,-, 64}. In particular, this is the case even when nonstandard models of time are used. In any event, there are many applicable t's that do not have an explicit solution. Remark 24 If we have an explicit solution, then the solution is, in an important way, unique. Indeed, suppose the {P1_, 6P1} and {P2, 6P2} are two solutions with the same histories and inputs. Then both satisfy the above four sentences and are, consequently, equal because {(_, 64} and {H(_, 6H} do not involve {PI, P2} and {P2_, 6P2} Remark 25 Since 64, can be determined from 4, we will often call 4, by itself the explicit solution. 14. Unique Solutions In the case of ordinary differential equations initial conditions and inputs usually determine a unique trajectory (solution). This is essentially the case with pseudo-differential-difference 18

equations, and from a practical point of view uniqueness, or lack thereof, is usually obvious. For example, if E contains a system of n pseudo-differential equations, and if EIC&Erx defines all histories and inputs explicitly, then Et will almost always have a unique solution. However, this is informal, and if one needs to go further, there are several technical issues. Remark 26 There are four reasonable ways to define uniqueness. 1. There is a unique standard structure (up to isomorphism) satisfying Et. 2. Et has an explicit solution. 3. 1t is an implicit definition of a solution. 4. The theory of E is complete, where the theory of t, denoted Th(Ct), is the set of all first-order sentences that can be deduced from Et. The first definition is the one that we really care about, but it cannot be expressed in firstorder logic. The others are, in contrast, first-order conditions. The second has already been discussed in section 13. The point made there is that many useful t's do not have an explicit solution; consequently, the second definition would be too strong. Consider the third definition. To simplify things, assume for a moment that Et has just one endogenous dynamic family {P_, 6P}. Let {P1_, 6P1} and {P2_, P2} be two dynamic families of the same type as {P, 6P}. Let Ft(P-_) and it(P2-) denote Et with {P_,P} replaced by {P1_,6P1} and {P2_,6P), respectively. An obvious definition of uniqueness is Et(P1) U Et(P2.) F (Vr)(V...) [P1._(r,...) P2.(r,... )] A (Vr)(V...) [SP1(r,...) P2(r,...)] (31) that is, when any two trajectories have the same histories, inputs, and static quantities, then they are the same. St is said to be an implicit definition of the solution if the deduction 31 is possible. This concept of uniqueness is essentially the one used for ordinary differential equations. Unfortunately, it is too strong. In fact, Beth's theorem says that definitions 2 and 3 are equivalent. The fourth definition is the first-order definition which is generally applicable, but there are problems. First, suppose that ET U YPD U XDEB U 2S U ZIC&E.E has a complete theory. This says that we have a complete first-order definition of histories, inputs, and static quantities. ET U EPD U EDEB U As are included to provide the mathematical foundation for XIC&Ex. If, then, Et is an implicit definition of the solution, then the theory of Et will be complete. However, as we had said,, need not be an implicit definition; moreover, the theory of Et need not be complete even when the first definition is satisfied. 19

Suppose that Th(5t) is not complete but that Th(ZT U EPD U EDEB U ES U EIC&Ex) is complete. Further, suppose that there is a unique standard structure satisfying the latter theory, that is, EIC&Ex uniquely describes some real histories and inputs. Assuming that Et is consistent, as we usually do, Th(Ct) will have a completion. This means that we can add sentences to obtain a complete theory, in fact there will be many possible completions. So to get a unique solution according to definition 4 we have to select one of these completions, that is, we have to add more first- order sentences to our model. The question is: which ones? In a sense, the selection is easy. Suppose that definition 1 is satisfied and let S be the standard structure. The theory of S, denoted Th(S), is the set of all first-order sentences satisfied by S. Th(S) is always complete, and since S satisfies Et, we have Th(Ct) C Th(S). Since we have assumed Th(3t) not complete, this is a proper containment. The point is that the natural completion of Th(Yt) is Th(S), so it is the one to pick from all the possible completions of Th(2t). Ideally, we would like to find a set of sentences Zadd to add to S so that whenever Th(ST U EPD U EDEB U ES U EIC&Ex) was complete, Th(t U Zadd) would be complete and have a unique standard structure satisfying it. That is, Zadd is in a sense a missing part of the model E. We discuss this in the next section. 15. E,, Universal Quantification Over Time If some formula lb((r) is satisfied over each interval (-00,r1], where r1 is finite, then we conclude that (Vz)iL(r) is satisfied. Example 8 Consider the pseudo-differential equation 6C(r, x) - 6Ia() A (x = a) + 6Ib(r) A (x = b) (32) where a and b are constant symbols. The initial conditions are (VT) [(r < 0) - -If-(T, c, 0)] and (Vr) [(r < 0) -+ (Vx) (-n6H(r, a, 0))], where c is another constant. There are sentences in Es which say that a, b, and c are distinct and that any x is one of them. The input 61a causes a to be added to C. if it is absent and to be deleted if it is present. The analogous statement holds for b. The initial conditions say that c is not initially in C. Since the pseudo-differential equation does not change the status of c, can we conclude that c is never in C.. The answer is no. At least it is no, if we we do not include the set of sentences,, being discussed in this section. To see why, suppose that,,, is not present. Then let time T be a nonstandard model with infinite times that contains R as a subset. It is easy to construct a solution such that C- does not contain c on t but does 20

contain c for some infinite times. Intuitively, T has more than one part, one of them is R?, the initial conditions determine the solution on R, but not on the other parts. The point is that having c in C. does not make practical sense, so we want to remove this possibility. That is the purpose of,,. Remark 27 Since there is no first-order way to define a finite number, the statement opening the section must be modified to fit into first-order logic. There are several ways to do this, and we allow any one of them. For example, if we know that +(r) is satisfied over every interval of the form (oo,a], where a is an algebraic number, we then conclude that (Vr)b(Tr) is satisfied. Strictly speaking, this introduces an infinite deduction rule because the deduction of (VrT)'(r) requires an infinite number of conditions - one for each algebraic number - therefore this is not really a first-order solution. Another approach is to show (1) that ) is satisfied and that (ro) sa e a () + 6(r) is satisfied for all. This might seem like begging the question because we are again confronted with universal quantification over time. However, in most applications either (Vr) [+L(r) -+ (rT) + 6b(r)] or its negation is implied by T, U Y IC&Ez U ZH The reason is that o U ZIC&EX U ZH is usually a firstorder characterization of what is going to happen over the next instant of time. Yet another way to proceed would be to (1) show that e(ro) is satisfied and then show that if () is satisfied at an arbitrary time, this fact implies that is satisfied immediately after the next event, if there is one. From these facts we would again conclude (V7r)g(Tr). There are other imaginable approaches. We allow any one of them. All of them together are the set,,, which is a subset of Eadd discussed in remark 26. In fact, it is usually the only part of Zadd, that we make explicit. Remark 28 The problem arises only if the theory of A U EIC&Ez U EH is not complete. Indeed, if this theory is complete, then for any (Vr)a(r) either it or its negation, but not both, must be in theory. However, if the theory E U YIC&Ex U H is not complete and neither (Vr)o/(r) nor -n(Vr)1b(r) is in this theory, then there is a completion containing ~ U EIC&Ex U EH U {(Vr)b(r)}) and another completion containing A, U,ICc&E. U LH U {'n(V'r)b(r)}. However, only one of them makes practical sense. It is the one that agrees with Th(S), where S, again, is the standard structure satisfying A U ^ic&Eg U ZH. The various techniques for deciding whether (Vr)/1(r) is satisfied are really techniques based on things that are true in the standard structure. That is, the sentences in E, will allow us to proceed without knowing S explicitly. Remark 29 The last two remarks beat about the bush because the author does not know of a better way to select the "natural" completion. This has no practical fall out, but it would be nice to tie things up better. Remark 30 There is a subtle trap to be avoided. It is connected with Beth's theorem. Suppose that Zt(P') and.t(P2) are two version of t with two different sets of endogenous 21

dynamic families substituted for the original endogenous dynamic families. If we let (r) = (V...) [Pi_(r,...) P2-(,...)], it will usually be the case that we can show that,(To) A (Vr) [+(r) - b(P+)(r)] (33) where 3b(P+) is, with P replaced by P+, is satisfied, so we conclude that (Vr)b(r) is always satisfied. One might then conclude - erroneously - that by adding a sentence to a we have made it an implicit definition of the solution; therefore, we have an explicit definition of a solution. This is erroneous because we have not added a sentence about P to A, we have added a sentence about P1_ and P2_ to Z(Pi) U Z(P2), and that is not what Beth's theorem is about. In other words, we do not magically force an explicit solution into existence. Remark 31 If more than one time variable is present or if the natural numbers are used, the sentences in,, will have to be augmented to handle these cases. Remark 32 Something analogous to,, is built into most temporal logics [8, 9, 10, 11] in one way or another. 16. Supervising We present a brief overview of using our modeling methodology in the supervision of discrete-event systems. By "supervision" we mean constraining the inputs to a discreteevent system in such a way that some condition is satisfied. The problem is usually that some inputs cannot be constrained. Such inputs are said to be uncontrollable; the others are controllable inputs. To simplify the discussion we assume for a moment that our first-order language has one endogeneous dynamic family {P., 6P} and two exogeneous dynamic families {u_, 6u} and {c_, 6c}, where the first is uncontrollable and the second is controllable. Since we will never use them, we suppress u- and c. We assume discrete-event behavior for all dynamic entities. Assume that we want a sentence b(P,, 6u, bc) to be satisfied because it characterizes some kind of desirable behavior. From a practical point of view the set of standard structures satisfying Ob is the set of acceptable trajectories. This set can be thought of as a generalization of the event languages used with finite-state automaton models of discreteevent systems. The examples presented in this section are relatively simple. However, it often happens that even in big discrete-event systems that the condition S will refer explicitly to only a small part of the system. This means that, with luck, one has a chance of attacking 22

a supervision problem even in an enormous system. In any event, some of the examples in this section have infinite state sets, and, yet, the solution of the supervision problem is trivial. Example 9 Suppose that the sentence b is - = (Vr)(V1) [P1i_(, T1, a3) -- (7T 71 < + 1)] = (V7T)_(r) (34) where a3 is a constant symbol; that is, the times 71 recorded in P are always in the interval [r,r+ 1). Now apply Ob to the discrete-event system characterized by 6P(7r, 71, 7) (r = 71) A (x = a3) A Pi.(7, 71, a3) + 6c(7) A (x = a3) A (71 = r + 1) (35) When there is an impulse in 8c, the subformula 6c(7) A (x = a3) A (71 = r + 1) adds the ordered-pair < r + 1, a3 > to P1 if it is not already present and deletes if otherwise. The subformula (7 = 7T) A (x = a3) A P1 _(, 71, a3) deletes an ordered-pair < 71, a3 > from P1_ when T = 71. So if Sc adds < 7 + 1, a3 > to P1_, it is automatically removed one second later. Let 0 be the initial time and assume 5.(O) is satisfied. Since 6u does not occur in this example, we will assume that tc is uncontrollable here. Since we are assuming discrete-event behavior, +_(() has a pseudo- derivative given by 6+(r) V (Vr1)[P_(r, r1,, 3) (T < 7 < T + 1)] + (Vr) [(Pi.r, r1, a3) + P,(r, r;, a3)) -. (r < r < r + 1)] (36) that is, 4_(r) + ++(r), where, informally, <+(r) is q_(r+), that is, q_ at a slightly later time. Assuming that q.(r) is satisfied, we want the second subformula on the right of sentence (36) to be satisfied. Substitution of 6P1 yields (Vr';) [((r j r;) A P._(r,;, a3) + 6c(r) A (r7 = r + 1)) - (r < r; < r + 1)] (37) for this subformula, and it is implied by +_(r). Indeed, < T, T > satisfies the subformula to the left of "-A" by either satisfying (r # Tr) A P1._(7, r, a3) or with r1 = r +1, and in either case (r < r; < r + 1) is satisfied. Thus, for any 6c the sentence b is satisfied. This is a trivial analysis even though this is an infinite state system. Trying to model this situation with a finite-state model could easily result in a very large state set and lengthy analysis. 23

Example 10 Consider the following sentence 4 = (Vr) [(Vri) {Pi(r, ri, a3) - (3r2)(r1 < r2) A P2_(r, 2, b2)}] = (Vr) (Tr) (38) that is, any time there is a pair < rT, a3 > in the value of P1 there must be a pair < r2, b2 > in the value of P2_ with r1 < T2. Assuming, as in the previous example, discrete-event behavior, the pseudo-derivative of q_(r) is o(r) + _(r) + (VTi) {(Pi_(T, r1, a3) + Pi (r, 71, a3)) - (3r2)(r1 < r2) A (P2-(r, r2, b2) + P2(r, r2, b2))} Now suppose that we apply the above condition to the discrete-event system characterized by 6Pi(r, 1, x) (T = T) A (x = a3) A Pi_(r, i, a3) + 6c(T) A (x a3) A (T = T + 1) eP2(r, r2, y) - (= 2) A (y = b2) A P2_(., r2, b2) + eu(r) A (y b2)A(T2 = T + 2) where 6c is controllable and 6u is uncontrollable, a3 and b2 are constant symbols, and the initial time is 0. Substituting the definitions of 6P1 and 6P2 into 6q yields 6(Tr) + 0(r) + [(Vn1) {(r n1) A P1.(r, r, a3) + 6c(r) A (r1 = r + 1)} - (3r2) {(T1 < T2) A ((rT r2) A P2(r, T2, b2) + u(r) A (r2 = r + 2))}] Since q_ is satisfied, 6{(r) -.L corresponds to the second subformula on the right being satisfied. We also assume (see the previous example) that (Vr)(Vt1) [Pi_(r, r, a3) -, (r < i < r + 1)] (39) and (Vr)(Vr2) [P2.((r,, 2,2) -- (T < T2 < r + 2)] (40) are satisfied. It follows from (39) that (Tl r) A Pl_(r, Tl, a3) and 5c(r) A (Tr = r + 1) (41) 24

are mutually exclusive. Likewise (r1 < Tr2) A (r $ r2) A P2-((r, 72, b2) and (r, < r2) A 6u(r) A (r2 = r + 2) (42) are mutually exclusive because of (40). If (r1 5 r) A P1_(,ri, a3) is satisfied, then by 5_(r) and (39) it follows that (372)(71 < r2) A (7 r72) A P2_(7,72, b2) is satisfied. If 6C(r) A (71 = r + 1) is satisfied, then either (3r2)(r1 < r2) A (7 $ T72) A P2_(7, 72, b2) or (3r2) ((r1 < T2) A 6U(r) A (r2 = r + 2)) have to be satisfied. After further simplification, we get 6c(r) -- 6u(r) V (3r2) ((r + 1 < r2) A P2_(r, 72, b2)) (43) that is, there can be an impulse in 6c if there is one in 6u or if there is a pair < r2, b2 > already in P2_ with r + 1 < T2. This assumes that 6c can depend on 6u. If this is not possible, then we have 6c(r) -, (3r2) ((r + 1 < r2) A P2 (r, r2, b2)) (44) That is, 6C(r) cannot depend on 6u(r) because, for example, there is a significant delay between sensing the existence of an impulse 6u(r) and creating an impulse 6c(r). Example 11 This is an extension of the preceding example. Suppose that in addition to satisfying j/, we want to select 6c so that Pi_(10, 10.5, a3) is satisfied. That is, we want to have a pair < 10.5, a3 > in the value of PI_ at time r = 10. Assuming discrete-event behavior, this is equivalent to 6P1_(9.5,10.5, a3) A -'P _(9.5, 10.5, a3) (45) being satisfied. But by (39) -nP1i(9.5, 10.5, a3) is satisfied. By the definition of 6P1, 6P1(9.5, 10.5, a3) - c(9.5) (46) But from the preceding example 6c(9.5) -, u(9.5) V (3r2)(10.5 < r) A P2-(9.5, r2, b2) (47) Since 6u is arbitrary, 6u(9.5) need not be satisfied, so we need (3T2)(10.5 < r2)AP2(9-5, T2, b2) 25

to be satisfied. But if there is no appropriate impulse in 6u before 9.5, the value of P2_ will be empty at r = 9.5. Thus the sentence A Pi.(10, 10.5, a3) (48) is not controllable. In general, we want to be able to select 6c in such a way that b is satisfied for any 6u. This means that allowable ec's will be determined by 6u. In fact, 6c has to be causally related to 6u. Remark 33 The foregoing approach can be formalized; however, the formalization requires higher- order logic. It is useful for stating the above condition precisely, but it is of very limited value for computational purposes. For example, one part of a formalization might be ET U Es U En - (Vu) [(6u DEB) -> (36c)(3 {P., 6P}) (_(P, 6P, 6u, 66c) A EPD A EDEB}] (49) ET and Zs are, as before, the definitions of time and static quantities. En is a modification of E,. In particular, if a (A,B, C) is a sentence in E,, where A, B, and C are predicate symbols, then a is replaced by (VX)(VY)(VZ)a(X,Y, Z) where X, Y, and Z are predicate variable symbols. The idea is that the first-order sentence a (A,B,C) which is a condition on specific predicates is replaced by the general condition (VX)(VY)(VZ)a(X, Y, Z) on all predicates. It is reasonable to do this because,, is already a set of general statements about behavior as r -> oo. The infinite set ETU s U En, in effect, sets up the mathematical environment. The deduction says that in this environment the second-order sentence on the right is satisfied. This sentence says that for every uncontrolled input bu with discrete-event behavior, (V6u) [(6uDEB) —, there exists a controlled input 6c and a dynamic family {P, 6P} with discrete-event behavior and with 6P the pseudo-derivative of P such that,b is satisfied, (36c)(3 {P. P}) (P, 6P, 6u, 6c)} A EPD A EDEB- It is a sentence because EPD and ZDEB are finite and their conjunctions can be formed. It is second-order because we are treating 6u, 6c, P., and SP as predicate variable symbols and quantifying over them. The above formal condition says that there is a structure satisfying'b for every 6u. It does not say, however, that this structure is a trajectory of the discrete-event system satisfying the initial conditions or any further conditions on the inputs. To include the discrete-event system we add finite sets RS and ZIC&Ez to the sentence on the right of a -". The result is ET U ES U En - ( Vu) [(6uDEB) -+ (36c)(3{P, 6P}) {((P, 6P, 6u, 6c) A EPD A EDEB A ERS A ZIC&EA}] (50) 26

where, recall, ERS is the set of right sides for the pseudo-differential-difference equations. However, the above condition does not say that 6c is causally related to 6u. This idea is captured by the following deduction. ET U ES U En I- (P-, 6P, 6u, 6c) A ZRS A EIC&Ex (Vr) [(wu')(VO) {(O < r) - (6u(O) 6u'())} (3{P.6P})(36c)( {(() (( ) P())) A ((6 < r) -+ ((6P(O) 6P'(0)) A (6c(0) - 6c'(O)))} A EPD A EPD A EDEB A EDEB A ERS A EZRS A EIC&Ex A E'IC&E AA (P, 6P'1, 6', u C') ] (51) that is, whenever we have a trajectory for the system satisfying b and for any time r, if the 6u' is a new uncontrolled input that agrees with the old one 6u in the past, then we can always find a new trajectory using 6u' that agrees with the old one in the past and still satisfies the condition 0. EPD is EPD applied to the new trajectory, and so forth. Example 12 LetC = {<, +,., 0, 1}U{Pl, 6P1, P2_, 6P2, 6u,, c, al, a2, a, b, b2}, where al, a2, a3, b, b2 are constant symbols denoting different entities. Let b(r) = (VTr)O_(r), and q_(r) = 1_-(r) V 62_(r), where 01-(r) = (Vtr1)(-iPi.(r7, a3)) and 82-(r) = (Vt2)(iP2(-r, r2, b2)). Suppose that the discrete-event system is modeled by P1(Tr, I, X) 6U(Tr) A (x = a) A(r= 1 -1) - - add al +(r = 1r) A ( = al) A P1_(r,, Tal) - - remove a, +(r = i - 1) A (X = a2) A P1-(T,, - 1, a,) - - add a2 +(r = r1) A (x = a2) A P1_.(, r, a2) - - remove a2 +(r = r - 1)A (x = a3) A Pl_(r, rI - 1,a2) - - add a3 +(r = r1) A (X = a3) A P1_(r, T1, a3) - - remove a3 and 6P2(r2, T2, ) 4 )c(r) A (x = bl) A (r = r2 - 2) - - add bl +( = T2) A (X = bl) A P2-(r, 72, bl) - - remove b +( = T2 - 2) A (a = b2) A P2_(, 2 - 2, bl) - - add b2 +(r = r2) A (a = b2) A P2-(,r 72, b2) - - remove b2 where the initial time is 0, and P1. and P2_ are empty for r <~ 0. In each equation an input impulse sets off a chain of events. For example, an impulse of 6u at time r causes the ordered pair < r + 1, al > to be added to P1_ (assuming it is not already present). The time (r + 1) recorded in this 27

pair is the time when this pair is scheduled for removal. At the same time the ordered pair < r + 2, a2> is added to P1i. Then at time r + 2, the pair < r + 2, a2> is removed, and the pair < r + 3, a3> is added. At time r + 3 the pair < r + 3, a3> is removed. One can view al, a2, a3 as denoting three different activities which are carried out in sequence and each of which takes one second. The sentence b says that activities a3 and b2 cannot both be in progress at the same time. Since we are assuming discrete-event behavior, +_(r) has a pseudo- derivative, and 6+(T) = (e1_(T) V 02_(T)) + ((e._(T) + 61i(T)) V ((e2_(T) + 062(T))) (52) Further, 6O1(r) = 81_(r) + (Vri) (6Pl(r, 71, a3) - P.((r, 71, a3)) (53) 602(r) = 2_(r) + (VT2) (bP2(T, 72, b2)' P2(Tr, T2, b2)) (54) Substitution into 6> yields 6+(r)= _(r) + {(Vri)(eP1('r,r1,a3) Pi.(r,7r,a3))V (55) ((Vr2) (eP2(r, T2, b2) + P2-(r, T2, b2)) (56) Assuming that +_(r) is satisfied, then 6({r) +~L is satisfied if and only if the subformula... * } is satisfied. There are three ways that q_(r) can be satisfied: neither a3 or b2 present; a3 present and b2 not present; b2 present and a3 not present. The subformula {. * *} describes 0_ immediately after time r, that is, it is ++(r). If (Vr1)(6Pl(r, ri, a3) ) P_(r, r1, a3)) is satisfied, then a3 is not present just after time r because Pi+(r, T1,a3) a - P1 (r, T1, a3)+6l(r, 1, a3) = Pl-(r, -1, a3)+Pl-(T, ri, a3) -+~. Similarly, if (Vr2)(SP2(r, r2, b2) - P2(T, 72, b2)) is satisfied, b2 is not present just after r. Consequently, the disjunction of these two formulas says that not both as and b2 are present. Next substitute in the definitions of 6P1 and 6P2 from the pseudo- differential equations. This yields after minor rearrangement the condition (Vr1) [{(r = r1 - 1) A Pl_(r,rl - 1, a2)} + {(r1: r) A P_.(r,, r, a3)}] V (Vr2) [{(r = T2 - 2) A P2_.(, r2 - 2, b1)}) {(r2 $ r) A P2.(r, r2, b2)}] (57) But we see that we do not have, yet, an explicit condition on 6c or 6u, and we need such a condition. Furthermore, it will not help to take the pseudo-derivative of the above formula. It, after all, is merely ++(r), and its pseudo-derivative is the same as that of #_(r). Consequently, we need another approach, and one possibility is shown in the next example. 28

Example 13 This is a continuation of the previous ezample. To finish the previous example we construct a partial solution of the pseudo-differential equations. In particular, we analyze the quantities P1_(, 71, a3) and P _(r, 71- 1, a2) that appear in condition (57). From the definition of 6P1 we obtain 6P1i(T, r, a3) + (P = T1 - 1)APi_(-, 1a) + (7 = 1) A Pi_(r, T, a3) (58) and P1(T, 71- 1, a2) +- (r = 71 - 2) A P1-(, 71 - 2, a) + (r = 71 - 1) A P1_(, T71 - 1, a2) (59) Since P1_(r, 1 - 2, al) occurs on the right of the second equation, we also need 6P1(r,71 - 2, ai) - (7 = T7 -2) A Pi_(.r, 7 - 2, ai) + U(r) A (r = 71 -3) (60) The above three equations form the following system Pi(r, ri, a3) (T= T1) ( 71 - 1) ~ Pi_(T, T71,a3) P1(r, 1r- 1, a2) + ~ (7 = T1 -1) (r = 1 -2) PI_(T, 71- 1, a2) Pi(r,r71- 2, a) J L 1 (r = 1- 2) P.(r, 71 - 2,al) J + (7 = 71 - 3) A tu(r) (61) where the obvious matrix manipulations are intended. This is a particularly simple system of equations to solve. The solution is P1i(r, r1, a3) ~ P1i_(, 1 - 1, a2) ((71 - 3) < r < (r - 2)) A P1i-(r, ri - 2, ai) 6u(r71 - 3) + ((1 - 2) <7 < ( - 1)) A 6u(7 - 3) 6U(nr - 3) + ((ri -1) < r < Ti) A ~ (62) where empty initial conditions have been assumed. More details of this solution method are presented in a later example. Similarly, 29

[P2(7, ) (( 2- b4) < (12-2))A ] +((~-llc~r~)n[ bC(72- 4) + ((r2-2) <r < ) A [( - ] Substituting into condition (57) we get (Vr1) [{(r = r1 - 1) A u(r7 - 3) + (r = 1) A 6(T1 - 3)} +- {((T1 - 1) < r < nr) A 6u(r1 - 3)}] V (V2) [{(r = 2 - 2) A 6(r2 - 4) + (r = r2) A 6c(2- 4)} {((r2 - 2) < r < 72) A 6(r2 -4)}] This is equivalent to (Vt1) [((r - 3) < 1 < (- - 2)) - 6u(nT)] V (V2) [((r-4) < r2 < (- 2))- -6c(r2)] The first sentence says that there is no impulse 6u at an earlier time that could cause a3 to be present at time r. The second sentence says the same thing about b2. The last condition can be rearranged to yield [6c(r) -- (V) {(r < r' < r + 1) - -6u(r')}] (63) that is, a controlled input 6c at time r requires that there be no uncontrolled input 6u in the future interval (r < rT < r + 1), but the latter condition means that 6c be selected on the basis of the future of 6u. Since the future of 6u is unknown at r, the only choice for 6c is (Vr)(-6c(r)). In principle, then, it is possible to control the system to satisfy the original ib; however, it is probably not attractive to say that no controlled input is ever allowed. The problem with the above system is, of course, that the delay of the uncontrolled inputs is 3 while that of the controlled inputs is 4. If this were reversed, we could have more interesting 6c's. 17. Additional Examples and Techniques The following examples illustrate various aspects of the modeling methodology. 30

Example 14 The following is a simple example from a class of models that is quite tractable. In particular, this class contains large models that can be attacked effectively with the method presented here. Let E contain the single pseudo-differential equation. 6P(r, x, x2) - 6el(r,, xX2) A P(7r, i,X2) + 6e2(r, Xi, X2) A P (r, x2, x) (64) where 6el and 6e2 are formulas with no occurrence of P_ or 6P. If one takes the informal view that x1 and x2 are "indices" over some index set, then for a fixed x1 and X2 5P(7, xl, x2) can be viewed as a Boolean-valued function of time. It depends on P for the indices < 1l,X2 > and for the indices < x2, x >. Thus, we also need a pseudo-differential equation to keep track of P. at < x2, x >, that is, we need P(r, x2, X1) - 6e2(r, X, x1) A P (r, 1, X2) + el(r, X2, x1) A P _(, X2, Xi) (65) Combining these two equations in a matrix format yields E 6P(r, x1, X2) 1 f e1(r, 1, X2) 6e2(r, x, 2) P (, X1, 2) 1 (66) P(r,x2,X1) J 6e2(r,X2,X1) e1l(r,x2,X1) [ P (r,2,x1) (6 This, then, characterizes the behavior of P_ at < x1,X2 > and < x2, x >, and it is very simple to solve. However, there may be an infinite number of different sets {x1,x2}, so it would appear that this approach yields an infinite number of Boolean systems. In fact, it does, but, fortunately, things can usually be simplified. We will discuss the simplification, but first we discuss the solution of one of the Boolean systems. It follows from P+ - P + 6P that P+(rXl' 22, ) {6poO + 6plWX + 6p2W2 + 6p3W3 + 6p4W4 + p5W5 + nel [ P_(r, ZX ]2) (67) where 6po = 6el(r, x1, x2) A el(r,X2, 1) pl = 6el(r, Xl, x2) A -16el(r, x2, xl) 6p2 = 6e (rx1, x2) ^A e1(r, x2, x) 6p3 = e2(r, 1, x2) A e2(r, x2, 1) 6p4 = 6e2(r, xi, x2) A -6e2(r, x2, x) ep5 = -e2(r, x1, x2) A e2(r, x2, xl) ne = none of the above (68) 31

6Po 6pl 6P2 aP3 6p4 5p5 I 0 W W2 w 3 W4 W5 WI 0 Wi 0 w4 W4 0 W2 0 WM W Ws 0 Ws w3 0 W5 W4 I W2 W1 W40 0 W4 WI 0 Wi Ws5 0 W5s 0 W2 W2 0 0 O O O O O 0 Table 1: The finite-state automaton and 0 [1 1 = W [ 1, W2 = 1 (69) 3 [ 1]' [1 ]'5[ T 1 ]I T (70) So if the interval r2 - rl contains a finite number of events, then [ P(r2, X1,x2) ] M[ P-(rl, IZ1, 2) (71) P_(72, XI, 2) P_(71, X2, XI) where M is a product of the above matrices, and the product is determined by the sequence of the events 6p. Initially M=I. After the first event M will be either 0, Wi, W2, W2, W3, W4, or W5, depending on which 6p occurred. It happens that this set of matrices is closed under matrix multiplication, so M is always one of them, and one can model the progression of M's with a finite-state machine described in Table 1. Thus we see that * There is a finite-state machine associated with each pair < xl, x2 >, < 2, xl >. * Since each machine has seven states, the set of all finite strings of 6p events associated with < X1, X2 >, < x2, X1 > is partitioned into seven languages Lo(zl, x2), L1(xz,2),..., L5(X1, X2), LI(x1, X2) The matrix M is determined by the language that the string of events up to the current time belongs to. It turns out that we can represent each of these languages with a second-order formula, and if the language is star free we get a first-order formula. 32

Definition 6 A language W C A*, where A is an alphabet, is star free [12] if it can be generated from finite sets of strings by repeated application of the Boolean operations (union, intersection, and complementation) and concatenation. Below we show how to represent star free languages with first-order formulas. The languages are strings made up of events that occur between times r1 and r2. Empty language: L(r1, r2) = Some contradiction in 6p's (72) Language containing just the empty string: LA(1, r2) = (V[) [(r1 < < 2 < ) -+ no event at 0] (73) Language containing just the string w = wl...wn: L(T71, 2) = (3!162e...9n)[(n7 < 1 <... < On < 2) A 6p(O1) = wi A... A fp(On) = wn A no other events] (74) Union: L1(rl,r2) V L2(r1, r2) (75) Intersection: Li(ri, T2) A L2(1, 72) (76) Complement: -L(1r, r2) A Discrete-event behavior (77) Remark 34 -L(r1, r2) contains bp's that do not have discrete-event behavior, and these have to be removed. Concatenation: (36)L1(ri, 6) A L2(6, r2) (78) Remark 35 Needless to say, nonstandard models will exists for many of these languages. If the language is regular but not star free, we have to allow the star operation. It can be characterized with the following second-order formula 33

L*(71, 2) = (3X) [X(r1) A X(r2) A (VO) (X(O) -- (71 < 0 < T2)) A (Xhas discrete-event behavior) A (N(81, 02) -- L(01, 02))] (79) where N(01, 02) is the formula N(81, 02) = X(01) A X(02) A {(V@) ((81 < 0 < 02) - — X(0))} (80) that is, 81 and 82 are neighboring points in X. The above formula is monadic second-order because of the existential quantification of the unary predicate variable symbol X. The purpose of X is to partition the interval [Ti1, 2]. The formula says that over each piece of this partition we have a string in L(1, 02). If we denote the formulas for the seven languages in this example by Lo(X, x2, r, To), L1(xi, X2, 7,7o)..., L5(xi,, 2 T7, o), LI(xi, x2 r, To), where To is the initial time and is defined in terms of static quantities, for example, 7T = 0, then we can represent the solution by [P (r, xl, x2) ] {oL(,0(x2,, 7, ro)O + L(Z1, X2, r, To)WI +... [ P-(r'' X2) ] + L5(xi, 2,r,,r)W5 + LI(xi, 2,rro)I} [P (,21), ] (81) If each of the seven languages is star free, the above is a first-order explicit solution. Otherwise, it is a second-order explicit solution. Note that even though we said that we were considering a fixed x1 and x2, we have, in fact, obtained a formula that works for arbitrary x1 and x2. Finally, it is really more important that we found finite-state automata than that we found first and/or second-order formulas. The automata are usually the means by which we can do something practical. Remark 36,,, allows us to conclude that the above solution is unique. Although we have an explicit solution, there are some limits to its usefulness. In particular, there are still an infinite number of finite-state automata implicit in the explicit solution, and sometimes we cannot ignore this fact. One way to go further is to assume some convenient form for 6el and 5e2. For example, ie(Tr,x1,X2) = 61i(r) A D1(x1,2) 6e2(T, X21,2) = I12(r) A D2(X1, 2) (82) 34

occurs fairly often in practice. It follows that 6po(r, X1,X2) = 1(r) A Di(xi, 2) A Di(x2,Xi) bP1(-, 1,x2) = 61(r) A Di(x1, 2) A-i D(x2,x1) bP2(-r,1,2) = 62(r) A= -D((x1,) A2A D1(x2, 1) p3(r, Xi, 2) = 612(r) A D2(x1,x2) A D2(x2, x) ep4(T, x1, x2) = 512(r) A D2(x1, X2) A -D2(x2, x1) bp5(T,, X2, 2 = 6() =A -nD2(x1, 2) A D2(x2, X1) ne(r,xi,x2) = no event. (83) A simplification results because the D's partition the set of all possible x1,x2s into a finite set of blocks (at most 16), and one finite-state automaton can be assigned to each block. This means that at most 16 finite-state automata will characterize a solution. The common inputs to all automata are 6I1 and 612. Example 15 Kitting Station: Consider a kitting station5 at which three types of kits are assembled: the first has one part of type A, the second has one part of type B, and the third has a part of type A and one of type B. Custom pallets for the kits arrive at the station on a conveyor one after another at irregular times, and there is a bound on the number of pallets that can be passing through the station at a time. There are sensors that sense arrival times and kit type. The conveyor is such that there is a minimum time interval, m, between pallet arrivals. The appropriate parts are placed on a pallet while it is passing through the station. It is assumed that loading parts takes zero time and that after the pallet arrives there is a A-second interval during which the pallet may be loaded. The pallet must be loaded strictly after the beginning and strictly before the end of this A-interval. There are two infinite capacity bins at the station, one contains A parts and the other B parts. New parts are added to these bins at irregular times, and the bins may become empty. If two parts must be loaded, both must be loaded simultaneously. If a pallet cannot be loaded because of a lack of parts, it passes through the station. The above is an infinite state system because the bins have infinite capacity, and the leaving times can be any positive real number. The sorts in the model are * time * parts 5A station where parts are combined into kits. 35

* kit types * pallet load status for parts of type A * pallet load status for parts of type B The sentences ET characterize time, and there are sentences defining A and m. There are three constant symbols of the sort kit type, kA, kB, kAB, and there are sentences saying that these symbols denote all the kit types, and each denotes a different kit type. There are two constant symbols, PA, aA, of the sort pallet load status for parts of type A that are used to denote that a part of type A is'p"resent or "a"bsent from the pallet. Similarly, there are constant symbols PB and aB of the sort pallet load status for parts of type B. Model for the conveyor-pallet subsystem: In the dynamic predicate symbol family {C(7(r, Y, T7, U, v), 6C(r, y, ri, u, v)}, the predicate symbol C_ denotes pallets passing through the station. The symbol r denotes the current time, y denotes the kit type, and rT denotes the time at which the pallet will leave the station. Since only one pallet leaves the station at a time, rl indirectly identifies a pallet. The variable symbols u and v denote whether or not parts of type A and B, respectively, are present or absent on the pallet. The initial time is zero. We assume that C_ is constant-valued for all times less than or equal to zero; therefore, the history of C_ with respect to zero is determined by its value at time zero, C_(O, y, rl, U, v). The intuitive idea is that this latter predicate is a set of pallets at the station at time zero. The predicate shows the type, leaving time, and load status for each of these initial pallets. The leaving time for one of these pallets must be nonnegative, so we require that 0 < 7r be satisfied. It takes A seconds to traverse the station, so these initial leaving times must satisfy r1 < A, and equality is not allowed because that would correspond to a pallet arriving at time zero, and such pallets are not initial pallets. Thus, the following sentence must be satisfied. (VrT)(Vy)(VU)(V)[C_(o0, yT, U, V) - (0 < n < A)] This sentence is an initial condition. The pallets are supposed to arrive unloaded at the station, but we allow the initial pallets to be loaded, that is, the pallets may have arrived and been loaded before time zero. Similarly, we allow any pallet type. Thus the following sentences must be satisfied. (Vri)(Vu)(Vv)[CO(0,, A, UT, v) - {((u = PA) A (v = aB)) V ((U = aA) A (v = aB))}] (VrT)(Vu)(Vv)[C_(O, kB, TB, Tu, v ) - {((u = aA) A (v = PB)) V ((u = aA) A (v = aB))}] (VTi)(Vu)(Vv)[C_(0, kAB, 7T, u, v) {((U = PA) A (v = PB)) V ((u = aA) A (v = aB))}] 36

That is, we assume that an initial pallet is either empty or properly loaded. There are other initial conditions. We restrict even further. Since there is a bound on the number of pallets that can be passing through the station at one time, we require that the difference in leaving times for two different initial pallets be greater than or equal to the known minimum m. That is, the following sentence is satisfied. (V1r)(Vy()(VU1)(Vv1)(VT1)(Vy22)(VU2)(VV2)[C —(O, Y, Ul ) C(, y2,, "2, u2,, v) -.V (((n1 = T12) A (yi = Y2) A (u1 = u2) A (vl = v2)) V (m < J7r1 - Tr2)] That is, they are either the same pallet or their leaving times differ by at least m, that is, they are different pallets. This is another initial condition. The following pseudo-differential equation models arrivals of pallets, their loading, and their departure. Each subformula is explained below. 6C(r,') (-, eo(r, X) + ei (r,') A D (X) A C_ (r, fi()) + +e4(r,) A {D41(x) A C_(r, f41(Y)) + D42(x) A C-(r, f42(X)) + D43(X) A C-(r, f43(X))} where x is an abreviation for y, rI, u, v, the ei's are subformulas characterizing events, and the f's and the fki are formulas characterizing vector-valued functions. eo(r, ) = [K(r, y) A (r: = r + A) A (u = aA) A (v = aB)] e1(,(,) = (r = r), Di(x) = T, fi() = (y,'r, u, v) that is, fi is the identity function. e2(r,x) = [6A(r, l) A (-n6B(r, n)) A (r < rT < r + A)] D2(7) = ((u = aA) + (U = PA)), f2(7) = (y,, aA,v) that is, f2 maps u into aA. e3(r, X) = [6B(r, r) A (-n6A(r,r )) A (r < n < T + A)] D3(7) = ((v = aB) + (v = PB)), f3() = (y, 7, u, aB) e4((7, X) = [6A(r, ri) A 6B(r, rl) A (r < rT < r + A) D41(X) = [((u = PA) A (v = PB)) + ((u = aA) A (v = aB))], f41(') = (y, Tl, aA, aB) D42(') = [(u = PA) A (v = PB) + (u = aA) A (v = PB)], f42(X) = (y,, aA,pB) D43(X) = [(u = PA) A (v = PB) + (u = PA) A (v = aB)], f43(') = (Y, TI,PA, aB) Consider the subformula eo(r, -) = [6K(T, y) A (7 = r + A) A (u = aA) A (v = aA)]. The symbol 6K(r, y) denotes the arrivals of pallets at the station, T the arrival time and y 37

the type. If < r, y,,r, 1u, v > is a tuple satisfying eo(r, ), then the value of the predicate C_ switches at time r. Thus, if the value of C_ does not contain the tuple < y, r, u, v > just before time r, then it will just afterwards and vice versa. 6K is an exogenous quantity, and it is uncontrollable in the sense that it is not determined at the station. However, there are sentences which say that only one pallet arrives at a time and that arrivals are spaced by at least m. Next consider the subformula e1(r, x) A C_(r, fi(7)) = [(Tr = r) A C(r, y, 71, U, v)]. It says that whenever the current time, r, equals the leaving time, T7, of a pallet, remove that pallet from the station. That is, at the end of the A-interval the pallet exits the station. The subformula e2(r, ) A C_(r, f2(7)) = [6A(r,ri) A (-ibB(r,rI)) A (r < 7r < r + A) A ((u = aA) + (u = PA)) A C_ (r, y, 77,aA, V)] loads parts of type A onto a pallet. The load command is denoted by 6A(T, Ti), where r denotes the time of the command and Tl denotes the pallet, that is, the pallet with that leaving time. The -n6B says that a part of type B is not simultaneously being loaded. If there is no pallet with this leaving time, nothing happens. If there is, then there is a corresponding tuple in the predicate C_, and if u in this tuple is not aA, then nothing happens. Otherwise, a part of type A is loaded onto the pallet. 6A denotes an exogenous quantity, but it is assumed to be controllable by the station, that is, a controller at the station can give this load command. Analogous remarks hold for the subformula e3(r, ) A D3(7) A C_(r, f3(x)) = [6B(r, rT) A (-inA(r, rl)) A (r < r7 < r + A) A ((v = aB) + (v = PB)) A C_(r, y,, r, u, aB)] Note that the previous paragraph assumes that the bins are never empty. We will return to this assumption in a moment. The subformula e4(r,') A {D41i()) A C_(r, f4l(x)) + D42(') A C_(r, f42(')) + D43(') A C_(r, f43(a))} is similar to the previous two. It handles simultaneous loading of both types of parts. The e;'s are mutually exclusive. There are few useful facts that are listed below. Their proofs are not presented. The following sentence says that the initial condition on the identity and spacing of pallets is true for all times. (Vr)(V7ll)(Vy)(Vu)(Vv)( 2)(2)()(V712)(2)(VU2)(Vv2)[C-(r, Yi1, ul, v1) A C-(r, Y12, 7'2, v 2) (((Tl1 = 712) A (Y1 = Y2) A (ul = u2) A (vi = v2)) V (m < 1TI1 - T121))] The next sentence says that if there is a pallet present, then it arrived at the time denoted by rT - A or it is one of the initial pallets. (VW)(Vy)(V7T)[(3u)(3v)C_(T, Y, Ty, u, V), ) 38

{(6K(r - A, y) A (r < T1 < T + A)) V (C_(0, y, 7, U, v) A (0 < r < A))}] Bin Subsystems We model a bin with the following pseudo-differential equation6 eB(-r, n) +-+ (r) A (-inR(r))A {[(n = 0) A (B_(r) = 0)] + [(n 7 O) A ((B_(r) = n) + (B_(r) = n - 1))]} + 6R(r) A (-i6(T))A {[(n = 0) A (B_(r) = 1)] + [(n $ 0) A ((B_(r) = n) + (B_(r) = n + 1))]} Es contains first-order sentences describing enough of the natural numbers to allow addition and subtraction, that is, n - 1 and n + 1 are defined. B_ is a function whose value is the current contents of the bin. 61 denotes the insertion of a part into the bin, and 6R denotes removal. Simultaneous impulses in 61 and 6R have no effect. Suppose that B_(r) = 10 and there is an impulse in 61. Then the value of the first subformula on the right will be the set {10, 11}, and that of the second subformula will be empty. The effect will be to delete 10 from and add 11 to B_. That is, one part is added to the bin. Next suppose that B_?(r) = 10 and there is an impulse in 6R. Then the value of the first subformula is empty, and that of the second is 9, 10}. The effect will be to remove a part from the bin. Suppose that B() = 0 and there is an impulse in e 61. Then the value of the first subformula is {, 1}, and this causes a part to be added. Similarly, if B_(r) = 0 and there is an impulse in 6R, the value of the right side is empty, so nothing happens. If B_-(r) = 1 and there is an impulse in 61, the value is {1, 2}, and a part is added. Finally, if B_(r) = 1 and there is an impulse in 6R, the value is {0, 1}, and the bin becomes empty. The two pseudo-differential equations developed above are linear in the sense that their right sides have a linear form with respect to exclusive-or + ". This is useful because simple solution methods are available for some linear equations. We will discuss this below. Unfortunately, when we combine these two pseudo-differential equations the result is not linear. Interconnection of the subsystems The model for the interconnection of the two subsystems is (Vr)(Vr7)[6A(r, 7r) + 6A'(r, r) A (BA(T) $ 0)] 6Note that the symbol A+" is used in two ways: + for exclusive or and + for addition of natural numbers. 39

where 6A' is a new predicate symbol, and (Vr)[bRA(7) (3i7)6A'(r, 71)1 The first sentence in effect replaces 6A by 6A' A (BA $ 0) in the first pseudo-differential equation, and the presence of (BA(T) 4 0) destroys the linearity of this equation. The new loading command 6A' causes loading only when the bin is not empty. The second sentence says that the new loading command and a removal command must occur simultaneously. A similar pair of sentences applies to B parts. Note that if we assume that the bins are never empty (as we did while developing the first pseudo-differential equation), then we get a kind of linearization. In particular, 6A and 6A' become equivalent, and the source of nonlinearity disappears. 17.1. A General Solution Method: We present a general solution method for linear pseudo-differential equations of the following form: 6P(r, X) eO(, X)+ el(r,a ) A {Dl(x) A P_(r, fil(Y)) + * * + Dlkl(Y) A P-(r, fik,1())} + +en(T, ) A {Dn (x) A P_(r, fnl(z)) + -* * + Dnkn(2) A P_(r, fnkn(x))} where x is an abreviation for xl,..., xl, the ei's are formulas, and each of the fij, i = 1,..., n, j = 1,..., ki, is a set of I formulas defining a mapping of I-tuples to I-tuples7 These mappings are distinct. The ei ADij,'s represent events and are formulas with no occurrence of P_ or 6P. The ei's are assumed to have discrete-event behavior. We also assume that the ei's are pairwise mutually exclusive in the sense that (Vr)(Vli)(Vx2)[-n(ei(r, 7l)Aei(r, x2))] is satisfied. Thus, events associated with different ei's cannot occur simultaneously; however, events associate with a common ei, for example, el A Dll and el A D12, can be simultaneous. Example 16 The pseudo-differential equation for the dynamic function symbol family {C_, 6C) in Example (15) is an example of such a pseudo-differential equation. The pseudo-differential equation for the dynamic function symbol family {B_, SB) is also in this form. Our solution method is based on creating a system of linear pseudo-differential equations. The basic idea is to add a new equation for each subformula of the form P_(r, fij(7)) appearing on the right side of the original pseudo-differential equation. However, the right sides of these new equations will contain subformulas such as P_-(r, fk(fij())), and we need a pseudo-differential equation for the pseudo-derivative of this subformula. It can 7Since we are allowing a many-sorted language, these mappings will have to respect the sort of each argument of the predicate symbols P_ and 6P. 40

happen that the composition fka(fij) is equal to a function for which we already have a pseudo-differential equation. If it is not, then another equation will have to be added. It in turn may have subformulas on its right side which require yet more equations. If the process terminates, the result is a finite system of equations, and this is the case of practical interest. Example 17 This is a continuation of Example 15. For the family {C_, 6C}, we have flf = fl flf2 = f2 flf3 = f3 flf41 = f41 f1f42 = f42 f1f43 = f43 f2fl = f2 f2f2 = f2 f2f3 = f41 f2f41 = f41 f2f42 = f42 f2f43 = f41 f3fl = f3 f3f2 = f41 f3f3 = f3 f3f41 = f41 f3f42 = f41 f3f43 = f43 f4lfl = f41 f41f2 = f41 f41f3 = f41 f41f41 = f41 f41f42 = f41 f41f43 = f41 f42f1 = f42 f42f2 = f42 f42f3 = f42 f42f41 = f42 f42f42 = f42 f42f43 = f42 f = 43 4 3f2 = f43 f43f3 = f43 f43f41 = f43 f43f42 = f43 f43f43 = f43 where, recall, some of the f's have a single subscript in the equation for {C-, IC). The significant point is that in this example the f-functions are closed under composition. In other situations this may not be true. That is, certain compositions of f functions may not be equal to any f function, and new pseudo-differential equations will have to be added. But one still hopes that only a finite number of equations need be added; however, this also need not be the case. For example, it is not the case for the pseudo-differential equation for the family {B_, SB} because of the n - 1 and n + 1 terms, so an infinite number of equations would have to be added. Let G be the set of all functions that can be characterized by compositions of the fij-functions. We assume that G is finite, and let G = {gl,..., gv}. Our convention is that g9 is the identity function. The fij's will be in G. The system of pseudo-differential equations will be P(r, gp(()) eo(r,g p())+ ei(r, gp()) A {2Dl(gp()) A P- (r, fil(gp(Y))) + * * * + Dlnl(g9p()) A P- (r, finl (gp()))} + * * +en(r, gp()) A {Dnl(gp()) A P-(r, fnl((gp(9))) + * +Dnk (9p(X)) A P (r, fnkn(g9p()))} where p = 1,..., N. By our assumption that G is finite, each of the compositions of a fij and a gp in the above formula will be equivalent to some g function. In other words, we will have a closed system of equations. Example 18 In Example 15 this system of equations for the family {C-, 6C} is SCo(T f) Eo(, f )+ {e(r, X NAW +e2(r, A^ W2+ e3(, ) A W3+e4(T,1 ) W4} ^ C, f 41

where c(, fi(z)) eo(r, fi()) T I I I bC(7,f2()) eo(r, f2(Y)) I T I 6C(i-, f)= | C(rf3( )) Eo(, f)= w eo(rf =) T C((r, f4i(5)) eo(r,/ f41()) lI-TII 6C(T, f42(o)) I I I ~ I T I 1(,/42()) 1 1 ~ ~ ~ T T 1 I T I 1 1. 1 I T I I LTII T II IITIIIJL W2 = -W3 =|T 1T 11~ T IL 1~ T1~ 1 1 L T 1 T 1 1T 1 i T~ ~1 J_ ~ D41(fl(Y)) D42(f/1()) D43(f/1()) - C_(Tr,f1()) I ~ I ID41(f2()) D42(f2(z)) I C_(r,f f()) W4 ~ ) 1 D41(f3(y)) | D43(f3(')) C I I 1 T I C_-(, f42(y)) 1I T T J L C_(T, f43(y)) _~ I ~ T _ T.. I-(r,f43(c)) Example 19 Since C+,- C_ + 5C, in Example 18 we get c+(r,/i(5)) eo(r,f()) - I ~ I I I - C+(T, fi(x)) eO(T fM(Y)) C+(,/ f2()) eo(, f2(~)) I I~ I I I C+(r3(5) eo(rf3(Y)) ((-,, ~ 1 111 C+(r,/f41()) +el(A ~. 1 1 C+(r, f42()) - ~ ~ ~ I ~ L C+(r, f43()). L ~ ~ ~ I I T T J J L IT 1~ T 1 J 1 1 1 I 1 I T I T I 1 JI. ITTJ _.L 1. J-i i _L1 +e2(r,-), ) T T ^ +e3(r,)A A ^ 1 1 1 1 1 1 1 111 1 I T 1 1 1 1 ~~i 1~ T I I D41(fl(x)) D42(fi(x)) D43(fi(x)) C_-(r,i(X)) I T ~ D41(f2(()) D42(f2(3)) 1 C_(r, f2(~)) +rr I I T D41(f3(/)) ~ D4(f3()) r A C{-,()) +e4(r,a )A T D41(3()) +ne(r, ) I}A C_(r f31()) I 1 1 1 1L C_-(T, f42(y)) I 1 T ~ L C-(r, f43(y)). where ne(r, ) denotes no event. 42

The discrete-event operation of the system will then be characterized as a product of the above matrices. However, there will only be a finite number of such products, and there will be a corresponding finite-state automaton that specifies the product that applies between r0 and r. 18. Final Remarks Remark 37 The modeling methodology presented here is extremely flexible in that it can model a vast range of discrete-event systems. Unfortunately, many of the resulting models will be intractable in that it will be difficult to use them to solve practical problems. This is analogous to ordinary differential equations: most of them are intractable, too. Still, models based on ordinary differential equations are of enormous importance. One focuses on special cases, special techniques, and approximations. This approach applies to pseudo-differential equations as well. For example, we showed that linear pseudo-differential equations are a useful concept. We presented a useful solution technique, and we presented an example of linearization of a system of nonlinear pseudo-differential equations. And there are other useful classes of equations that are tractable. The point is, then, that a general approach to all possible models is impractical but specific ones are. Remark 38 Although the models of discrete-event systems based on finite-state systems do have general solution methods, they quickly become impractical because of state-set explosion. This means that techniques to handle models with enormous state sets are needed. But this just means that one has to consider special classes of models, special techniques, and approximation. In other words, the finite-state models really have to be approached in the same ad hoc manner as our models. Arguably, our models are better for ad hoc approaches in that they make more of the system's structure and operation visible. For example, it was trivial for us to treat some infinite state systems. Remark 39 Temporal logic has also been used for modeling discrete-event systems. The typical approach considers a special class of discrete-event systems and a restricted class of logical questions about system operation. Then an analysis algorithm is presented for this combination of systems and questions. So far we have been able to model each class of discrete-event system that is modeled by temporal logic and adapt its analysis algorithm to our framework. Thus, one can think of our modeling methodology as including temporal logic approaches as special cases. However, this is a mixed blessing since temporal logic analysis algorithms are applicable to only small systems. Typically, each version of temporal logic is shown to be complete in some sense. Here we know that we may not get completeness. That is, even if we have a complete description of initial conditions and inputs, there may be a first-order sentence a such that neither a 43

nor -a can be deduced. Roughly speaking, temporal logic avoids this by restricting the class of sentences that is considered and tailoring the logic to the temporal framework. Since we allow all possible first-order sentences and insist on remaining within standard first-order logic, we may miss completeness. However, anything that can be proved in temporal logic can be proved within our framework. The point is that we may be able to prove more. Remark 40 Rule-based models are another approach to modeling discrete-event systems. There one has rules of the form a p 3, where a and / are first-order sentences. The idea is that if a is currently satisfied and the rule "fires", then /3 will be satisfied afterwards. If a is not satisfied, the rule cannot fire. The firing of a rule can be thought of as an event. The trouble with rule-based models is that they are ambiguous. Suppose that A is a structure modeling the current state of a discrete-event system and that A satisfies a. Further, suppose that the rule a - f3 fires. The new state will be a structure B that satisfies /3. Unfortunately, knowing that B satisfies /3, is not enough information to specify B, and this is the sense in which rule-based models are ambiguous. To remove this ambiguity one needs to select a structure from among all those that satisfy /. The usual approach is to argue that B should be as close to as possile, where saying what "close to" means becomes the key issue. One can view our modeling system as an unambiguous alternative to rule-based models. In fact, it grew out of an earlier effort to use rule-based models [13]. References [1] P J. G. Ramadge and W. M. Wonham, "The control of discrete event systems," Proceedings of the IEEE, vol. 77, no. 1, pp. 81-98, January 1989. [2] P. Varaiya and A. B. Kurzhanski, editors, Lecture Notes in Control and Information Sciences, Discrete Event Systems and Applications, number 103, Springer-Verlag, August 1987. [3] Y. C. Ho, editor, Proceedings of the IEEE, Special Issue on Dynamics of Discrete Event Systems, volume 77, January 1989. [4] C. G. Cassandras and P. J. Ramadge, "Special section on discrete event systems," IEEE Control Systems Magazine, pp. 66-112, June 1990. [5] H. Enderton, A Mathematical Introduction to Logic, Academic Press, 1972. [6] C. C. Chang and H. J. Keisler, Model Theory, North-Holland, 1973. [7] R. Scheuring and H. Wehlan, "On the design of discrete event dynamic systems by means of the boolean differential calculus," in IFAC Symposium, Zurich (Design Methods of Control Systems, pp. 4-6, September 1991. 44

[8] A. Pnueli, "Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends," in Lecture Notes in Computer Science, Current Trends in Concurrency, J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, number 224, pp. 510-584, Springer-Verlag, 1986. [9] J. S. Ostroff, "A logic for real-time discrete event processes," IEEE Control Systems Magazine, pp. 95-102, June 1990. [10] R. Alur, C. Courcoubetis, and D. Dill, "Model-checking for real-time systems," in Proceedings Fifth Annual IEEE Symposium on Login in Computer Science, pp. 414425, June 1990. [11] E. Harel, 0. Lichtenstein, and A. Pnueli, "Explicit clock temporal logic," in Proceedings Fifth Annual IEEE Symposium on Login in Computer Science, pp. 402-413, June 1990. [12] W. Thomas, "Automata on infinite objects," in Handbook of Theoretical Computer Science, J. van Leeuwen, editor, chapter 4, pp. 134-187, Elsevier Science Publishers B.V., 1990. [13] A. Naylor and R. Volz, "Design of integrated manufacturing system control software," IEEE Transactions on Systems, Man, and Cybernetics, vol. SMC-17, no. 6, pp. 881897, November/December 1987. 45