TEMPER: a temporal programmer for time-sensitive control of discrete event systems

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS—PART A: SYSTEMS AND HUMANS, VOL. 31, NO. 6, NOVEMBER 2001

485

TEMPER: A Temporal Programmer for Time-Sensitive Control of Discrete Event Systems Abbas K. Zaidi, Member, IEEE, and Alexander H. Levis, Fellow, IEEE

Abstract—This paper is an extension of an earlier work on a methodology for modeling temporal aspects of discrete-event systems. The methodology incorporates point and interval descriptions of time, and offers both qualitative and quantitative calculus for time. A graph-based temporal programmer (TEMPER) is shown to implement the axiomatic system of the temporal formalism. The approach transforms the system specifications given by temporal statements into a graph structure, identifies errors (if present) in the system, infers new temporal relations among system intervals, and calculates delays among time points and their actual time of occurrence. Index Terms—Discrete event systems, Petri nets, point graphs, temporal inferencing, temporal logic.

I. INTRODUCTION

T

HIS PAPER presents an extension of earlier work [1] on a methodology for modeling time-sensitive aspects of discrete event systems (DESs). The approach models the temporal aspects—the time layer—of a DES separately from the functional and physical layers of the system. The idea is to decouple different aspects of a DES model and analyze each aspect using specialized analytical tools (e.g., Petri nets [2]–[4], colored Petri nets [5], IDEF, etc.) suitable for handling the requirements of that aspect. The resulting suite of analytical models can then be integrated into each other to help formulate an enhanced formal tool—a superstructure built upon all these models—to handle every aspect of DESs, which facilitates not only the analysis of a DES as a whole but the study of individual aspects of it. It was this objective that led us to differ from most of the existing temporal formalisms. However, in this respect, an approach we found similar to ours is that of Kahn and Gory’s time specialist [6]. The proposed temporal calculus, point interval temporal logic (PITL), is based on an extension of Allen’s ontology of time [7], [8], which looks at the modeling of temporal issues only and does not attempt to integrate it with the propositional or first-order predicate calculus. The temporal formalism presented in [1] extended Allen’s approach by incorporating explicit representation of time points (representing instantaneous events) together Manuscript received September 20, 1999; revised July 10, 2001. This work was supported by the Air Force Office of Scientific Research under Contract Number F4620-95-1-0134. This paper was recommended by Associate Editor B. Scherer. A. K. Zaidi is with the Department of Electrical Engineering and Computer Science, Mohammad Ali Jinnah University, Karachi, Pakistan (e-mail: [email protected]). A. H. Levis is with the C3I Center, George Mason University, Fairfax, VA 22030 USA (e-mail: [email protected]). Publisher Item Identifier S 1083-4427(01)09759-4.

with the interval description of time, and hence overcame an apparent weakness [9] in interval-based approaches. This paper extends the point-interval approach one step further by adding provisions for dates/clock times and time distances for points and intervals. Therefore, the approach sort of combines Dechter’s [10], Kahn and Gory’s [6], and Allen’s [7], [8] approaches into a single formalism. The major contribution of the paper is the formal tool, called TEMPER, which automates the inference mechanism of PITL. The tool is based on a graphical representation of the temporal inputs, which not only implements the axiomatic system of PITL, but also verifies system integrity before making inferences. Some of the recent approaches that try to combine the qualitative and quantitative aspects of time are due to Kautz and Ladkin [11], Meiri [12], and Yao [13]. A final note on TEMPER’s inference engine is that it infers temporal relationships among system intervals/points, calculates time distance among points, and identifies time stamps associated with points, without being engaged in a combinatorially expensive computation. Unlike the approaches of Allen, Kahn and Gory [6], [8], which make use of reference intervals to avoid memory problems, TEMPER manages to organize the temporal information with relatively no burden on available storage. The paper is organized as follows. Section II presents a brief account of PITL and its extension. Section III presents TEMPER, a formal tool based on PITL. The section presents an overall outline of the methodology of TEMPER and then takes the reader through the details of each module outlined. Section IV applies the result of the methodology to an example problem. Finally, Section V concludes the discussion by summarizing the contributions and identifying future extensions of the approach. II. POINT-INTERVAL TEMPORAL LOGIC (PITL) A. Topology of Temporal Systems The point interval formalism presented in this paper considers a system’s temporal specification on a single time line with a single future. The future of a system is determined by the set of events that culminates into the future, and the time sequence associated with the occurrence of these events—the definition is similar to the notion of a “chronicle” by McDermott [14]. A single timeline single future (STSF) system, therefore, has only one set of events with only one time sequence associated to it—a single chronicle. The time sequence may not be fully specified due to incompleteness in the system specification; there could be events with unspecified temporal relations

1083–4427/01$10.00 © 2001 IEEE

486

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS—PART A: SYSTEMS AND HUMANS, VOL. 31, NO. 6, NOVEMBER 2001

line: for any point on this time line there will exist only one future—an STSF system. (a)

D. Analytical Model for PITL Statements

(b) Fig. 1. Topology of temporal systems.

among them. An STSF system with a fully specified time sequence is shown in Fig. 1(a). A multiple timelines multiple futures (MTMF) system, on the other hand, is characterized either by a single set of events with associated multiple time lines each yielding a different future—type 1, or by multiple set of events with different single/multiple time sequences each representing a total world-history—type 2. Fig. 1(b) presents the two cases of MTMF systems. The treatment of MTMF systems by PITL is beyond the scope of this paper and is left for a future treatment of the subject. Readers who are interested in a detailed discussion on several other topological issues of time are referred to [15]. B. Lexicon The lexicon of PITL consists of the following primitive symbols. is represented as , Intervals: an interval where “ ” and “ ” denote the “start” and “end” of the interval. or simply Points: a point is represented as , i.e., an interval of zero length. (In the sequel, the term interval is used to refer to both intervals and points if not explicitly stated otherwise.) Temporal relations, : The set of temporal relations is given as

Before, Meets, Overlaps, Starts, During, Finishes, Equals

C. Syntactic and Semantic Structure of Statements The syntactic and semantic structure of the statements in PITL is shown in Fig. 2. The figure outlines three possible cases and the corresponding semantically relevant temporal relations that can exist between points and/or intervals, represented by generic symbols and . are mutually exclusive and exThe temporal relations haustive [1]. The well-formed temporal statements in PITL are all connected together with an implicit conjunction; therefore, they represent a system’s temporal description on a single time

A temporal relation between two intervals can be described with the help of algebraic inequalities, shown in Fig. 2, among points representing the start and end of these intervals. Two points, and , on a single time line can be related to each other by one of the following three relations: (greater/less than), (equal to), and “ ” (unknown). The “ ” is added to incorporate incomplete information. A temporal between two intervals and , denoted as relation ” can, therefore, be represented as a 4-digit string “ , where the made of elements from the alphabet and , first (left-most) digit represents the relation between and , the third digit represents the second digit between and , and the fourth between and the relation between . Fig. 3 shows this string representation for each temporal relation. E. Inference Mechanism The inference mechanism of PITL uses the analytical representation of temporal statements presented in the last section and point axioms [1] to infer unknown temporal relations among system intervals. be points defined on a 1) Point Axioms: Let , , and single time line. 1) 2) 3) 4) 5) (The symbol “_” is used to denote remaining combinations of , not covered by axioms 1–4.) the four relation, The inference mechanism of PITL constructs the analytical representation for the pairs of intervals with unknown temporal relations. The resulting string representation of the relation(s) is pattern matched with the string representations of Fig. 3 to infer possible temporal relation(s) between the intervals. An inference engine for PITL, therefore, requires an exhaustive enumeration of the result through all feasible combinations of available statements, provided no knowledge of the system’s correctness is available a priori [1]. However, an inference engine that outputs the result as soon as it finds the first feasible set of inputs can only be applied to a known consistent system of temporal statements. This, in turn, requires a front-end verification mechanism for the PITL statements. Zaidi [1] proposed a graph-based methodology, termed TL/PN methodology, to resolve this problem. A discussion on the TL/PN methodology is given in Section III. F. Extended PITL An extension to the formalism allows assignment of actual lengths to intervals, time distances between points, and time stamps to points representing the actual time of occurrences. The approach extends the lexicon of PITL by adding the following two functions to it.

ZAIDI AND LEVIS: TEMPER

Fig. 2.

487

Temporal statements in PITL.

Fig. 3. Analytical model of PITL statements.

Functions: Length: interval length function that assigns a positive in, where teger to a system interval, e.g., length Time: time stamp function that assigns an integer number to a system point, e.g., time A discussion on the inference mechanism for the extended PITL system is presented in Section III. III. TEMPER This section presents a tool, TEMPoral programmER (TEMPER), which implements the inference mechanism of PITL. TEMPER is built on a graph-based approach, termed Temporal logic/Petri net (TL/PN) formalism [1]. The TL/PN approach transforms the system’s specifications given by temporal statements into a graph structure. The approach then verifies the specifications for temporal inconsistencies and errors. Once the system is verified for correctness, the temporal inference engine (TIE) infers temporal relations

among system’s intervals, identifies the windows [1] of interest to the user, calculates lengths of intervals and windows, and infers actual time of occurrence of events. The TIE of the TL/PN methodology performs all these tasks by completely avoiding the combinatorial nature of the inference mechanism. An overview of the tool is shown in Fig. 4. The following sections present a detailed account of all the modules shown in the figure. A. Language The input to TEMPER is a set of statements in PITL. The folrepresents the lowing context-free grammar lexical and syntactical structure of the TEMPER inputs. Set of nonterminals; fV

=<

temper-input

>; <

temporal statement >;< interval >; < temp relation > ; < point >;< temp relation 1 >; < temp relation 2 >;< temp relation 3 >;< letter >; < lower case letter >, < upper case letter >; < digit >; < sp ch >g

488

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS—PART A: SYSTEMS AND HUMANS, VOL. 31, NO. 6, NOVEMBER 2001

Fig. 4. TEMPER overview.

Set of terminals;

=

T

fBefore, Meets, Overlaps, Starts, During, Finishes, Equals, length, time [ ] ... . . . 0 1 2 .. . 9 ( ) ! @ $ % &g ; ; ;a; b;

; ;

;

;

;

;

;

Start Symbol;

; z;

A; B;

; Z;

;

;

;

;

;

S

=

temper-input

<

>

Set of Productions; P < temper-input > < temper-input temper-input > < temporal statement > temporal statement > < interval <

=

f

! !

j

temp relation >< interval > >< point < interval >< temp relation >< interval < point >< temp relation >< point > < point >< temp relation

><

><

This lexical structure of points and intervals allows the language processor of TEMPER to identify semantic errors in the input. A statement “process1 Overlaps process2” will result in an error, since the identifier “process1” represents a point and semantically a point (an interval with zero length) cannot overlap an interval. Similarly “length Event ” will be an erroneous statement because of the identifier “event” being defined as a point. However, “process1 Overlaps process2” and “length Event ” will be acceptable temporal statements. The input to TEMPER will consist of one or several such acceptable temporal statements connected together with an implicit conjunction. The following are two examples of an error-free input to TEMPER.

1 j 2 j 3 j jlength[ interval ] jtime[ point ] label ! ( letter j digit j sp ch ) 11 : event1 Starts process 1 12 : Overlaps time[pevent 1] = 1000 length [[ ]] = 10 label j3 length[process 1] = 10 length [[ ]] =8 interval ! upper case letter label event2 Finishes process1 Overlaps j[ point point ] event2 Starts process2 length [[ ]] = 5 point ! lower case letter label length [process2] = 20 length [[ ]] =8 j interval j interval temp relation ! Before jMeetsjOverlapsjStarts jDuringjFinishesjEquals B. Tl/PN Methodology temp relation 1 ! Before temp relation 2 ! The language processor of TEMPER performs the lexical and Before jStartsjDuringjFinishes syntactic/semantic analysis on the input statements and reports temp relation 3 ! BeforejEquals the errors, if any are found. Once the input is debugged, the lower case letter ! j j . . . j TL/PN approach takes each individual statement in the input and upper case letter ! j j . .. j transforms it into an equivalent graphical representation, called letter ! lower case letter j point graph (PG). The PG representation of a system’s temporal upper case letter aspects organizes the information contained in temporal statedigit ! 0j1j2j . . . j9 ments into a graphical structure. This section presents an analsp ch ! (j)j j!j@j$j%j&g ysis based on this graphical representation. The analysis applies <

>

>

<

> ;

>

<

>

<

>

<

>

<

>

X

<

>

<

>

<

><

>; <

<

>

<

sY ; eX

>

Z

> ;

<

><

>

s <

e <

>

sY ; eZ

>;

>

;

>

<

;

>

<

;

>

<

<

<

<

>

;

>

a b

>

A B

<

<

>

>

z;

Z;

>

>;

;

Y

sZ; sY

<

<

Y

sX; sY

<

ZAIDI AND LEVIS: TEMPER

489

Fig. 7.

Fig. 5. PG representation of a temporal situation.

Fig. 6.

Unified PG representation for statements in Fig. 6.

The PG representing the entire system of temporal statement is then constructed by unifying (Definition 2) individual PGs to a (possibly) single connected graph. Fig. 7 shows the unified PG for the temporal statements and PGs in Fig. 6. Note that the unifying process only looks at the labels of the nodes to identify equalities and does not take into consideration the arc lengths assigned to edges in the PGs. Definition 2: Unification: and , s.t. , a) For all to with construct a directed edge from node . length and be two b) Let nodes in a PG representation. If there exists a point such that and or then the two nodes are merged into ” such that a single composite node “

Temporal statement to PG translation.

certain graph–theoretic concepts on the structure of PGs, identifies their structural properties, and finally interprets the results obtained in terms of the temporal aspects of the systems under consideration. 1) Point Graph Representation: is a Definition 1: Point Graph (PG): A PG, PG directed graph with the following. Set of vertices with each node or vertex representing a point on a time line. Two points and are represented as a composite point if both are mapped to a single point on the time line. Set of edges with each edge , between two and , also denoted as , reprevertices senting a temporal relation “ ” between the two . vertices— Edge-length function (possibly partial): (set of positive integers) Vertex-time-stamp function (possibly partial): Fig. 5 presents a two-node PG with time stamps and arc length, and the corresponding temporal situation represented by the PG. The figure also presents a correspondence between the time stamps and edge lengths: a PG with only time stamps can be represented by an equivalent PG with edge length expressions and vice versa by using a reference time stamp for the conversion. between two intervals and A temporal relation can now be represented by an equivalent PG representation by translating the algebraic inequalities shown in Fig. 2 to corresponding PGs [1]. Fig. 6 presents the temporal-statement-to-PG translation process for the temporal system given in Section III-A.

where and represent the preset and postset of node

2) System Verification—Phase I: As mentioned in Section II, the inference engine of PITL requires a consistent system specification in order to infer temporal relations without enumerating all possible combinations of known temporal relations. Definition 3 identifies all possible cases of inconsistency in a PITL system. Definition 3: Inconsistency in PITL: A system’s description contains inconsistent information if the following occurs. and , a) For some intervals and both , or and (with the exception of ) hold true. b) For a point , the system calculates two different time stamps. and , , the system can c) For some points . determine two different lengths for the interval Some of the inconsistent cases, of the type defined in Definition 3b, are trivially detected during the unification process: whenever the system tries to merge two nodes with different time stamps into a single node, it signals an error. Once a unified PG representation is achieved, the graph is checked for other inconsistent cases defined by Definition 3a. Such inconsistent cases are characterized by the following proposition. Proposition 1: A set of temporal statements is inconsistent if the PG representation of the set contains self-loops and/or cycles. A necessary condition for a consistent set of temporal statements is, therefore, given as follows.

490

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS—PART A: SYSTEMS AND HUMANS, VOL. 31, NO. 6, NOVEMBER 2001

(a) Fig. 8.

Branch and join nodes in point graphs.

Proposition 2: A set of temporal statements is consistent only if the PG representation of the set is an acyclical graph. The TL/PN methodology identifies these inconsistent cases by applying the following result (Proposition 3), first presented in [1]. Proposition 3: A point graph contains cycles if and only if it has nonzero -invariants calculated for the connectivity matrix [1], [18] of the PG. Definition 4: -Invariant: Given the Connectivity Matrix of a PG, an -invariant is a non-negative integer vector of the kernel of , i.e.,

Once cycles are detected in a PG by calculating nonzero -invariants, the nodes responsible for these cycles can be easily identified. This will, in turn, identify intervals involved in these cycles. This information can be used to correct the system of temporal statements. 3) Folded PG Representation: Phase I of the verification process identifies temporal errors present in the system caused by the qualitative input to TEMPER. The unification process itself identifies some of the erroneous time stamps during the course of unifying individual PGs. This section presents an analysis, done on the unified PG, that looks at the edge (arc) length expressions and folds the unified PG into a folded PG. The folding process establishes new temporal relations among system intervals, inferred through the quantitative analysis of the known temporal relations specified by interval lengths and time stamps. The quantitative input provided to TEMPER may in turn have inconsistencies in it. Therefore, a second phase of system verification is carried out to ensure the correctness of the temporal system before the inference engine is invoked to process queries. A detailed account of the folding process is provided as follows. A correspondence between time stamps and edge length expressions has been presented earlier in Section II, therefore, the approach and results are illustrated with PGs with edge length expressions only. The results can be easily applied to graphs with time stamps using the equivalence. in a PG Definition 5: Branch (Join) Node: A vertex is termed a Branch (Join) node if it has multiple outgoing (incoming) edges connected to it. Fig. 8 shows a pictorial representation of a branch and a join node in PGs. is said Definition 6: Branch Folding: A branch node and in the post-set of to be folded if, for all a) with , the edge to , denoted as , is replaced from with by an edge

(b) Fig. 9.

Branch folding. (a) Unified PG. (b) PG after branch folding.

(a)

(b) Fig. 10.

Join folding. (a) Branch-folded PG. (b) PG after join folding.

, and the vertex removed from the postset. or , the two verand are merged into a single vertex with tices ’, and composite label ’ . The methodology applies the branch-folding process to all the original and newly created (formed during the folding process) branch nodes in the unified net. Fig. 9 illustrates the process by folding the unified PG of Fig. 7. The branch folding process, when applied to all the branch nodes of a graph, yields a partially folded PG having nodes with at most one outgoing edge with an edge length expression. Since all the edges in the PG may not have edge lengths associated with them, the branch folding may not result in a branch-node-free PG. A join folding process which applies a similar process to all the joins in the graph further treats the PG so obtained. is said to be Definition 7: Join Folding: A join node and in the preset of , with folded if, for all , the edge , • with is replaced by an edge , and the vertex removed from the preset. or , the two ver• and are merged into a single vertex with tices ,” and composite label “ . Fig. 10 illustrates the process on the PG of Fig. 9. b)

ZAIDI AND LEVIS: TEMPER

491

length[process1]= 3 length [process2] = 3 length[[pevent1, pevent2]] = 1 length[[eprocess2, pevent3]]= 3 Fig. 11.

Inconsistent case during folding process.

A single application of join folding after a single application of branch folding is all that is required to fully fold the graph. Proposition 4 ensures the fact that single applications of branch folding followed by join folding are enough to fold the graph completely (the term “completely” is used relative to the quantitative information available in the PG.) Proposition 4: Let a PG be folded by branch folding. A subsequent application of join folding does not create any new branch nodes that can be folded by the branch folding process. Proof: The branch folding process results in a PG having nodes with at most one outgoing edge of specified length. The join folding process does not add any new edges to the nodes with length expressions. The join folding might result in a new and , branch node only when it merges the two vertices, .” This merging, in turn, into a single composite vertex “ takes place along the outgoing edges of the original vertices and with edge lengths. The process (Definition 7) reand by a single edge places the two edges having the same edge length as that of the replaced ones, leaving the newly created vertex with only one outgoing edge of specified length. A similar result can be obtained for the branch folding process in terms of join nodes if the TL/PN methodology applies the join folding before branch folding. 4) System Verification—Phase II: As mentioned earlier, the folding process establishes new temporal relations, among system intervals, inferred through the quantitative analysis of the known temporal relations specified by interval lengths and time stamps. The possible inconsistencies present in the quantitative input to TEMPER may hinder the folding process or result in erroneous structures in the folded graph. Definition 3 identifies the set of possible inconsistencies that might find their way into the temporal system modeled by PITL. The type of inconsistency defined by Definition 3b may reveal itself during the folding process: If, during folding, a PG the process finds multiple edges between a branch(join) node and a vertex in its postset and preset, where these edges have different lengths associated with them, then the process halts and reports an error. A pictorial representation of such an erroneous case is presented in Fig. 11. During Phase I of the verification process, the unified PG is checked for acyclicity. The inconsistency, however, can result in creation of new cycles in the graph during the folding process. The following example illustrates the issue. Example 1: Let a temporal system be described by the following set of TEMPER statements. event1 Starts process1 process1 Meets process2 event1 Before event2 process2 Before event2 process2 Before event3

The corresponding unified PG is given in Fig. 12(a). The graph has an acyclical structure and, therefore, contains no inconsistent cases that can be identified at the first phase of the verification process. The branch node labeled “ pevent1;sProcess1?” has two outgoing edges with edge lengths and it can be folded by the branch folding procedure. The resulting folded graph, with a cycle, is given in Fig. 12(b). The folded graph in the previous example cannot be folded further; an approach similar to the one in Proposition 3 can be applied to identify the cycles present in the folded PG. The TL/PN methodology, therefore, constructs a Connectivity Matrix of the folded PG and calculates the -invariants of the graph. The resulting nonzero -invariants identify the cycles (inconsistencies) in the temporal system (Proposition 3). The creation of cycles during the folding process can have serious effects on the graph. Once a cycle is created during the folding process, it tends to attract the remaining vertices in the PG toward itself. And, if the PG has edge lengths on all its edges, the folding process ends up with a folded PG which has a single cycle with all its vertices collapsed into it. The phenomenon is termed “black hole effect” for the obvious reason. Example 2 illustrates the effect. Example 2: Black Hole Effect: Let the temporal system presented in Example 1 be augmented with an additional statement eprocess2, pevent2 The PG with this added information is given in Fig. 13(a). The methodology now finds a branch node “eprocess2” with two outgoing edges that can be folded. The graph after folding the node is shown in Fig. 13(b). The branch folding proceeds with folding the other branch node “pevent2.” The resulting branchfolded PG is given in Fig. 13(c). In the previous two iterations of the branch folding procedure, readers must have noticed the fact that the cycle present in the original PG has caused the vertex labeled as “pevent3” to wrap around the cycle—the black hole—until it becomes a part of it. A final application of join folding will have a similar effect; the node labeled as “pevent;sprocess1” will collapse into the black hole and become a part of it. The intensive computational effort required to fold a PG and the possible loss of this effort due to the black hole effect, demand an earlier detection of cycles during the folding process itself. The folding procedure is, therefore, tailored to identify cycles by assigning dummy time stamps to vertices being folded: reassignment of a time stamp to an already marked vertex prompts the presence of a cycle. The folding process folds in a PG all the vertices that are connected together through quantitative temporal relations. A PG and/or vertex-time-stamps function with a total edge-length will be folded into a PG having each vertex with at most one incoming and outgoing edge connected to it; the folding process will remove all the branch and join nodes. However, for

492

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS—PART A: SYSTEMS AND HUMANS, VOL. 31, NO. 6, NOVEMBER 2001

(a)

(b) Fig. 12.

Example 1 graph. (a) Acyclical graph. (b) Folded graph with cycle.

(a)

(b)

(c) Fig. 13.

Example 2 graph. (a) Original point graph. (b) Folding node [eprocess2]. (c) Folding node [pevent2].

a PG with partial and functions, the folded graph might still have branch and join nodes. The folding process reveals all the quantitative inconsistency in the system; however, some of the inconsistent cases might still be hiding due to the lack of specified edge lengths and/or time stamps on some of the edges and vertices of the graph. A folded PG with leftover branch and join nodes should be checked for multiple directed paths from any branch node to any other join node. The length expressions corresponding to each such path are equated to each other and the resulting set of equations is checked for feasibility. A set of infeasible equations signals an inconsistent case present in the system. The following example illustrates the issue. Example 3: Let a temporal system contains the following TEMPER statements as part of its system specification

Fig. 14.

PG with an inconsistent case.

The PG representing the system is shown in Fig. 14. The obvious inconsistency present in the statements neither reveals itself as a cycle nor gets identified during the folding process. However, the error is detected by equating the length expressions corresponding to the two directed paths from vertex “ ” (branch node) to “ ” (join node).

ZAIDI AND LEVIS: TEMPER

493

TABLE I QUERIES FOR CALCULATING TEMPORAL RELATIONS

The TL/PN methodology employs the following steps to carry out this analysis on a folded PG. The approach makes use of two search procedures, the FPSI and FPSO [1], [16] algorithms, which are variants of an earlier FindPath algorithm algorithm, when applied to an edge in [17]. The a PG, collects all the nodes that have directed paths to . The algorithm, on the other hand, collects all the nodes to which has a directed path. The steps of the methodology are given as follows. , the set of all branch nodes in the PG. Se1) Construct and calculate by applying lect a node . Remove from all the branch nodes present . in , the set of all join nodes in . Select 2) Construct and calculate by applying a node . Remove from all the branch nodes . present in into a single node, and calculate -in3) Merge and variants for the Connectivity Matrix of the modified . The calculated -invariants correspond to all dito . Equate the lengths correrected paths from sponding to the calculated -invariants and check the equations for feasibility. If found infeasible, report the error, else iterate through step 2 until there are no ele. ments left in the set . 4) Go to step 1 until there are no elements left in the set The analysis of the equations constructed as a result of the approach helps bound some of the unknown edge lengths in terms of lower and/or upper limits to their values. The calculated -invariants can also be used to remove nonconnected chains in the folded PG [1].

C. Temporal Inference Engine (TIE) The output of the TL/PN methodology is a consistent (error free) description of the temporal system represented in terms of a PG structure. The temporal inference engine (TIE) implements the inference mechanism of PITL to infer the temporal relations among system intervals, time distances among points, length of user-specified intervals, and time stamps associated with points, through a simple search in the PG. TIE infers temporal relations between two intervals and by constructing the string representation of the temporal relation (Fig. 3) between the two intervals by searching for the directed paths between the vertices representing the intervals in the PG representation. The search for the directed path between two vertices in a PG uses a depth-first search with arc lengths as the heuristic measure; the depth-first search engine first explores the outgoing edge of the current vertex with a length expression. The search, therefore, finds the path between two vertices that has (possibly) all its constituent edges with length expressions. The sum of all these lengths gives the total distance between the two vertices (points). Similarly, if the time stamp of one of these points is known, the time stamp of the other can be calculated by adding or subtracting the distance (path length) between the two. The advantage of the TL/PN formalism is that it not only verifies system correctness prior to any inference making, but also overcomes the combinatorial problem, discussed in Section II, associated with inferring new temporal relations; TIE’s search engine stops as soon as it finds the first directed path between two vertices under consideration and does not explore all paths between the two vertices to ensure consistency. TEMPER’s inference engine takes user queries, interprets them, and by invoking the search engine calculates the answers

494

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS—PART A: SYSTEMS AND HUMANS, VOL. 31, NO. 6, NOVEMBER 2001

TABLE II MISSION REQUIREMENTS

TABLE III INPUT STATEMENTS

Fig. 15. Mission net. Length expression for path 1: d1 + 30 + 30 + 15 + 45 + d2, where d1, d2 > 0. Length expression for path 2: 240. Equating the two: d1 + 120 + d2 = 240 with d1 + d2 = 120; d1, d2 , 120.

to the input queries. A list of different types of queries that can be processed by TIE is given in Table I. The variables have the same definitions provided in Section III-A. IV. APPLICATION Consider a mission requiring three resources of types Bomber (R1), Fighter (R2), and Tanker (R3) each. Each resource has to go through a sequence of four consecutive stages, prepare(T1), ingress(T2), service(T3), and egress(T4), during the mission. Each stage requires a specified time period to complete. Table II gives the delays associated with each of the resources. In addition to the delays required of each resource, the following constraints also apply to the mission under consideration. 1) T3 of R1 should start right after T3 of R2. In TEMPER syntax the requirement is translated as T3(R2) Meets T3(R1) 2) T4 of R2 should occur during T3 of R3. In TEMPER we will have T4(R2) During T3(R3)

3) T2 of R1 should occur during T3 of R3. In TEMPER we will have T2(R1) During T3(R3) The entire set of mission requirements is now translated into TEMPER statements. The set of input statements to TEMPER is shown in Table III. The unified PG representing the mission requirements is constructed and checked for errors. Since no errors are found, the PG is folded. The folded PG is shown in Fig. 15. The term “Mission net” will be used to refer to this PG from now on. The second round of verification checks for cycles in the net and calculates the expressions for lengths between every pair of a branch and a join node. In the Mission net of Fig. 15, there exists a situation, shown with bold lines on the net, where there exist two paths between the two marked nodes with corresponding expressions for length. The two expressions, when equated together, give additional information regarding the upper bounds and for values of each of the two unknown time distances, . The PG in Fig. 15 is error-free, and the inference engine can now be invoked to process queries. Let us assume that we

ZAIDI AND LEVIS: TEMPER

495

need to know the temporal relation between the times when resources R1 and R2 should be made available. The following set of queries and their return values provide the answer(s):

-R(sR1, sR2) TIE returns: sR1 Before sR2 -length[[sR1, sR2]] TIE returns: 30

The output of the query processing can be interpreted as follows: The Fighter, R2, should be available 30 time units after the availability of the Bomber, R1. Similarly the following queries result in

-R(eR1, eR2) TIE returns: eR2 Before eR1 -length[[eR1, eR2]] TIE returns: 15

The result can be interpreted as follows: The Bomber, R1, should remain available 15 time units after the Fighter, R2, has finished its assigned task. This type of information is essential for planning and scheduling purposes.

V. CONCLUSION The paper presented a temporal reasoning tool, TEMPER, based on a point-interval logic, PITL, which incorporates both qualitative and quantitative temporal aspects associated with points and intervals defined on a single time line with a single future. The system takes input in PITL language, interprets it, and transforms the temporal statements into an equivalent graphical structure. The structure of the graphical representation reveals temporal inconsistency present in the system and then an inference engine, TIE, uses the corrected graphical representation to answer user-defined queries. The system TEMPER is intended for modeling time-only aspects of discrete-event systems (DES) and therefore is not capable of addressing or programming other qualitative, physical, and/or functional aspects of the system under consideration. In this respect, it differs from some of existing temporal logic based programming languages like Tempura [19] and Tokio [20], [21]. (The two mentioned tools are both based on a modal interval temporal logic (ITL) [9].) The presented methodology can be used as a verification tool for verifying consistency in a temporal system. It can also be used for temporal constraint generation and validation tool for optimization and planning problems. The present implementation of TEMPER handles only STSF systems. A future extension to this approach considers issues for modeling MTMF system by an enhanced version of TEMPER.

REFERENCES [1] A. K. Zaidi, “On temporal logic programming using Petri nets,” IEEE Trans. Syst., Man, Cybern. A, vol. 29, pp. 245–254, May 1999.

[2] J. L. Peterson, Petri Net Theory and Modeling of Systems. Englewood Cliffs, NJ: Prentice-Hall, 1981. [3] W. Reisig, Petri Nets, New York: Springer-Verlag, 1991. [4] G. Rozenberg, “Advances in Petri nets,” in Lecture Notes in Computer Science, New York: Springer-Verlag, 1991, vol. 524. [5] K. Jensen, Colored Petri Nets: Basic Concepts, Analysis Methods and Practical Use. New York: Springer-Verlag, 1992. [6] K. Kahn and G. Gory, “Mechanizing temporal knowledge,” Artif. Intell., vol. 9, pp. 87–108, 1977. [7] J. F. Allen, “Maintaining knowledge about temporal intervals,” Commun. ACM, vol. 26, no. 11, pp. 832–843, Nov. 1983. , “Toward a general theory of action and time,” Artif. Intell., vol. [8] 23, no. 2, pp. 123–154, 1984. [9] A. Galton, Temporal Logics and Their Applications. New York: Academic, 1987. [10] R. Dechter, I. Meiri, and J. Pearl, “Temporal constraint network,” Artif. Intell., vol. 49, pp. 61–95, 1991. [11] H. Kautz and P. Ladkin, “Integrating metric and qualitative temporal reasoning,” in Proc. AAAI, Anaheim, CA, 1991, pp. 241–246. [12] I. Meiri, “Combining qualitative and quantitative constraints in temporal reasoning,” in Proc. AAAI, Anaheim, CA, 1991, pp. 260–267. [13] Y. Yao, “A Petri net model for temporal knowledge representation and reasoning,” IEEE Trans Syst., Man, Cybern., vol. 24, pp. 1374–1382, Sept. 1994. [14] D. McDermott, “A temporal logic for reasoning about processes and plans,” Cogn. Sci., vol. 6, pp. 101–155, 1982. [15] W. H. Newton-Smith, The Structure of Time. London, U.K.: Routledge & Kegan, 1980. [16] A. K. Zaidi and A. H. Levis, “Validation and verification of decision making rules,” Automatica, vol. 33, no. 2, pp. 155–169, 1997. [17] V. Y. Jin, “Delays for distributed decisionmaking organizations,” Lab. Inform. Decision Syst., Mass. Inst. Technol., Cambridge, Tech. Rep. LIDS-TH-1459, 1986. [18] A. K. Zaidi and A. H. Levis, “On verifying inferences in an influence diagram,” in Proc. First Int. Symp. Command Contr. Res. Technol., Washington, D.C., June 19–23, 1995, pp. 443–451. [19] B. Moszkowski, Executing Temporal Logic Programs. New York: Cambridge Univ. Press, 1986. [20] T. Aoyagi, M. Fujita, and T. Moto-Oka, “Temporal logic programming language Tokio: Programming in Tokio,” in Logic Programming. New York: Springer, 1985, vol. 221, Lecture Notes in Computer Science, pp. 128–137. [21] M. Fujita, S. Kono, H. Tanaka, and T. Moto-Oka, “Tokio: Logic programming language based on temporal logic and its compilation to prolog,” in Proc. 3rd Int. Conf. Logic Programming, vol. 225, Lecture Notes in Computer Science, 1986, pp. 695–709.

Abbas K. Zaidi (M’90) received the B.E. degree in electrical engineering from NED University of Engineering and Technology, Karachi, Pakistan, and the M.S. degree in electrical and computer engineering and the Ph.D. degree in information technology and engineering from George Mason University (GMU), Fairfax, VA, in 1991, 1989, and 1994, respectively. Currently, he is an Associate Professor in the Department of Electrical Engineering and Computer Science, Mohammad Ali Jinnah University, Karachi. Since 1990, he has been with the System Architectures Laboratory, School of Information Technology and Engineering, GMU, first as a Graduate Research Assistant and now as Affiliate Research Faculty. He sits on the Statutory Academic Committees of the Karachi Institute of Information Technology and National University. He has taught at NED University, FAST Institute of Computer Science, Karachi, and the University of Karachi. His current research interests include distributed intelligence systems, temporal control of discrete event systems, validation and verification of rule-based systems, colored Petri nets, and IT education. Dr. Zaidi is currently a member of the Information Technology Accreditation Council (ITAC), Ministry of Science and Technology, Government of Pakistan.

496

IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS—PART A: SYSTEMS AND HUMANS, VOL. 31, NO. 6, NOVEMBER 2001

Alexander H. Levis (F’87) received the A.B. degree in mathematics and physics from Ripon College, Ripon, WI, in 1963. He also received the B.S., M.S., M.E., and Sc.D. degrees in mechanical engineering, with control systems as his area of specialization, all from the Massachusetts Institute of Technology (MIT), Cambridge, in 1965, 1967, and 1968, respectively. Currently, he is University Professor of Electrical, Computer, and Systems Engineering, George Mason University (GMU), Fairfax, VA. He is associated with the C3I Center, where he heads the System Architectures Laboratory. From 1992 to 1994, he served as Chair of the Systems Engineering Department. He held the same position from 1992 to 1994 and again from 1996 to 1997. From 1968 to 1973, he taught systems and control theory at the Polytechnic Institute of Brooklyn, Brooklyn, NY. From 1974 to 1980, he was with Systems Control, Inc., Palo Alto, CA, where he was Manager of the Systems Research Department. From 1979 to 1990, he was a Senior Research Scientist at the MIT Laboratory for Information and Decision Systems. He joined GMU and the C3I Center in 1990. His research interests for the last 15 years include architectures for command and control, organization theory and design, human decision making, and distributed intelligence systems. He has published over 150 papers and many book chapters and has co-edited three volumes of The Science of Command and Control (Fairfax, VA: AFCEA, 1994). He has served as Editor or Associate Editor of several professional journals. Dr. Levis is Past President of the IEEE Control Systems Society. He is also a Fellow of the American Association for the Advancement of Science (AAAS), a senior member of AIAA, and a member of AFCEA and INCOSE.