Knowledge-Based Systems

Knowledge-Based Systems

Jonathan Lee*

Department of Computer Science and Information Engineering, National Central University, Chungli, Taiwan

Recently, there has been an increasing interest in improving the reliability and quality of AI systems. As a result, a number of approaches to knowledge-based systems modeling have been proposed. However, these approaches are limited in formally verifying the intended functionality and behavior of a knowledge-based system. In this article, we proposed a formal treatment to task structures to formally specify and verify knowledge- based systems modeled using these structures. The specification of a knowledge-based system modeled using task structures has two components: a model specification that describes static properties of the system, and a process specification that characterizes dynamic properties of the system. The static properties of a system are described by two models: a model about domain objects (domain model), and a model about the problem- solving states (state model). The dynamic properties of the system are characterized by (1) using the notion of state transition to explicitly describe what the functionality of a task is, and (2) specifying the sequence of tasks and interactions between tasks (i.e., behavior of a system) using task state expressions (TSE). The task structure extended with the proposed formalism not only provides a basis for detailed functional decomposi- tion with procedure abstraction embedded in, but also facilitates the verification of the intended functionality and behavior of a knowledge-based system.1997 John Wiley &

Sons, Inc.

I. INTRODUCTION

Recently, there has been an increasing interest in improving the reliability and quality of AI systems.¹As a result, a number of approaches to knowledge- based systems modeling have been proposed in the Software Engineering and Artificial Intelligence literature, e.g., Refs. 2 to 8.

In particular, Tsai, Slagle, and their colleagues have conducted an empirical case study on requirements specifications of knowledge-based systems.^4,6These approaches are important in demonstrating the feasibility of developing specifi- cations for knowledge-based systems. Meanwhile, Chandrasekaran and several other researchers have advocated using task structures as a general modeling

*YJLEE@SE01.CSIE.NCU.EDU.TW

INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS, VOL. 12, 167–190 (1997)

1997 John Wiley & Sons, Inc. CCC 0884-8173/97/030167-24

approach to knowledge-based systems.^2,5,9,10The task structure is a tree of tasks, methods, and subtasks, which provides a framework for organizing knowledge in knowledge-based systems in a step-wise refinement fashion. However, these approaches are limited in formally verifying the intended functionality and behav- ior of a knowledge-based system.

Our emphasis in this article is to provide a formal treatment to task structures to formally specify and verify knowledge-based systems modeled using these structures. The specification of a knowledge-based system modeled using task structures has two components: a model specification that describes static proper- ties of the system, and a process specification that characterizes dynamic proper- ties of the system. The static properties of a system are described by two models:

a model about domain objects (domain model), and a model about the problem- solving states (state model). The dynamic properties of the system are character- ized by (1) using the notion of state transition to explicitly describe what the functionality of a task is, and (2) specifying the sequence of tasks and interactions between tasks (i.e., behavior of a system) using task state expressions (TSE).

TSE extends regular expressions with a task-based composition operator to combine expressions at different levels in a task structure, and a follow operator to describe a partial system behavior. TSE can be associated with a task to describe a global interaction or with a method to specify local task sequencing in the structure. Progression operators and frame axioms are adopted for con- structing the descriptions of a state through a TSE to an initial state description in the context of task structures. The task structure extended with the proposed formalism not only provides a basis for detailed functional decomposition with procedure abstraction embedded in, but also facilitates the verification of the intended functionality and behavior of a knowledge-based system.

In the sequel, we first describe some background work in task structures in the next section. The formal foundation of task structures is proposed in Section III. We discuss how to propagate state descriptions in the context of task struc- tures in Section IV. Verification of specifications modeled using the structures is presented in Section V. In Section VI, examples based on R1/SOAR¹¹are given to demonstrate the benefits of our approach. A discussion on the comparison of the proposed approach to related work is in Section VII. Finally, we summarize the proposed approach and outlined the plan for our future research.

II. BACKGROUND WORK IN TASK STRUCTURES

Variations of task structures have been proposed, e.g., Refs. 2, 5, and 12 (Fig. 1). Steels⁵[see Fig. 1(a)] has proposed work along lines that build on the notion of tasks and task structures. In his formulation, the task structure is intended to specify the task/subtask decomposition of a complex task. There is no explicit notion of alternate methods, that is, the method [M in Fig. 1(a)] is chosen implicitly in the analysis. The task sequencing relationship in a method cannot be specified.

In Ref. 2, Chandrasekaran has described a task structure in which we can explicitly identify alternative methods for each tasks in a task structure. A method

Figure 1. Variations of task structures.

can set up subtasks, which themselves can be accomplished by various methods.

Only search control knowledge can be described, for instance, the task sequencing relationship between subtasks B and C in Figure 1(b).

Hofsted et al.¹²has presented a task structure diagram, in which tasks can be recursively defined in terms of subtasks, and can be decomposed into a hierarchy of subtasks. Decisions are used if performing a task involves choices between subtasks [denoted as a circle in Fig. 1(c)]. In task structure diagrams, sequential execution, iteration, choice, parallelism, and synchronization can be expressed. For example, task sequencing relationship among subtasks B, C, D, and E is graphically documented in the task structure diagram, namely, task B is executed first, which is followed by the task C and decision d₁ in parallel fashion, and in turn is followed by the choice between task D or E. Similar to Steel’s approach, there is no explicit notion of alternative methods. The local task sequencing is expressed using the task structure diagram.

Problems with these approaches can be summarized below:

● cannot verify the consistency of system behaviors due to the lack of a formal foundation of task structures (and tasks);

● lack of a mechanism that can describe partial system behavior, and can fill in the missing detail as the information is available;

● unable to describe global interactions between tasks at different levels.

In the next section, we propose a formal treatment of task structures to formally specify functional specifications and dynamic behaviors of knowledge- based systems modeled using task structures.

III. A FORMAL FOUNDATION OF TASK STRUCTURES The specification of a knowledge-based system modeled using task structures has two components: a model specification that describes static properties of the system, and a process specification that characterizes dynamic properties of the system. The static properties of a system are described by two models: a model about domain objects (domain model), and a model about the problem-solving states (state model). The dynamic properties of the system are characterized by (1) using the notion of state transition to explicitly describe what the functionality of a task is, and (2) specifying the sequence of tasks and interactions between tasks (i.e., behaviors of a system) using task state expressions (TSE). In this article we will focus on aspects in the proposed framework that facilitate the process specification and verification of a knowledge-based system’s functional requirements. More detailed descriptions about model specifications can be found in Refs. 8 and 13. In this section, we first formulate the notion of tasks in task structures, provide a formalism, task state expressions, to describe the relation- ships among tasks, methods, and subtasks, and conclude with the specifications of tasks and methods.

A. Formal Semantics of Tasks in Task Structures

To explicitly specify what a task is in a task structure, a task is treated as (1) a state-transition which can take one state to another through a sequence of intermediate states, and (2) a functional unit that can be specified by using preconditions, protections, and postconditions, which are partial state descrip- tions about the state before, during, and after performing the task. State transition model is thus adopted for the purpose of formulating and analyzing the proposed specification methodology. In the general form of the model (e.g., Ref. 14), the world is viewed as being in one of a potentially infinite number of states. The effect of a task is to cause the world to make a transition from one state to another. Each task is therefore modeled by a set of triplekb, dˆ

, al where b and a are states, and dˆ

is a sequence of states, b being the ‘‘before state,’’ dˆ being the ‘‘during state,’’ and a being the ‘‘after state.’’

DEFINITION 1 (State Transition): A task T is defined as a set of tripleskb, dˆ , al, where b and a denote the state before and after an invocation of T, and dˆ

denotes the sequence of states during the invocation of T.

Formulas in first-order logic are used for state descriptions. The precondition of a task is a condition (i.e., a formula) that needs to be true for all states before the task. The rigid postcondition of a task is a condition that is true for all states after the task. The protection of a task is a condition that needs to be held before, during, and after the execution of the task. These are formally defined below.

DEFINITION2 (Functional Specification): Let a task T be a set of tripleskb, dˆ ,al.

1. A formulaw is a precondition of a task T, denoted as BT, if and only ifw is true in state b, for every triplekb, dˆ

, al [ T.

2. A formulaw is a protection of a task T, denoted as PT, if and only if for every triplekb, dˆ

, al [ T,w is true in state b, w is true in state sequence dˆ

, andw is true in state a.

3. A formulaw is a rigid postcondition of a task T, denoted as RT, if and only if for everykb, dˆ

, al [ T,w is true in state a.

4. A formulaw is a soft postcondition of a task T, denoted as ST, if and only if for everykb, dˆ

, al [ T, the degree to whichw is true in state a is a real number [ [0, 1].

B. Task State Expression

Task state expression (TSE), based on regular expressions, is to describe the dynamic behavior of a system modeled using task structures. Regular expression has been used in AI planning to represent the procedural knowledge (e.g., Ref.

15) and in software engineering to describe the behavior of a software system (e.g., Ref. 16). A TSE is an expression that defines (1) the desirable sequence of tasks that are expected to have processed before a given task, and (2) interactions between tasks at different levels. The notion of conditional expression is also adopted in TSE. We formally define TSE below.

DEFINITION3 (Task State Expression). The task state expression, E , over a set of tasks, I 5 hT1, T2, . . . , Tnj, is defined as follows:

1. « is a task state expression, where « stands for null.

2. For each task T[ T , (T) is a task state expression.

3. If Eiand Ejare task state expressions, then (Ei,Ej) is a task state expressions, where

‘‘,’’ denotes immediately follow.

4. For each expression E , bE is a task state expression, where b is a well-formed formula to be attached to a TSE, E , to represent the conditional branching. For a TSE, E , ‘‘b1E1~ b1E2. . .~ bnEn’’ means ‘‘Ifb1then E1else ifb2then E2. . . else ifbnthen En’’ where~ denotes selection, and b1,b2, . . . ,bnare mutually exclusive.

5. For each expression E , [E ] is a task state expression and is a short hand notation for (« ~ E), where ‘‘[ ]’’ denotes optional.

6. If Eiand Ej are task state expressions, then (bEi)* and (Ei, bEj)* are task state expressions, where ‘‘*’’ denotes iteration and ‘‘b’’ is an iteration condition.

7. If Eiand Ejare task state expressions, then (Ei; Ej) are task state expressions, where

‘‘i’’ denotes follow.

Graphical notations of TSE operators in a task structure diagram are shown in Figure 2. The relationship between subtasks B and C of method M1 is a sequential relationship [that is, (B, C)]. Selectional relationship is illustrated using the relationship between the subtasks of method M₂, denoted by conditions b1,b2, and a ‘‘n’’ within a rectangle [e.g., (b1D ~ b2E)]. As for iteration, there are two cases: (1) the iteration condition is associated with the whole expression (namely,b3(F, G)]; and (2) the iteration condition is associated with a subtask of its method [e.g., (F,b4G)]. We call the relationship between task F and B a global interaction (denoted using a dotted line), because the interaction is be- tween tasks at different levels. This kind of relationship can be expressed using a follow operator [e.g., (F; B)].

Figure 2. Dynamic behaviors in a task structure.

A TSE represents a collection of possible sequences of task invocations, referred to as task sequences. More formally, the semantics of a TSE over T is defined by a mapping to S , which is the set of all possible task sequences for tasks in T . The convention of viewing a conditional test as a task is also adopted,¹⁷ denoted asb?. b? is a special control flow task that is invoked only when b is tested to be true. Similarly, ¬b? is another special control flow task that is invoked only when ¬b is tested to be true. The mapping function between a TSE and its corresponding task sequences is defined as follows:

DEFINITION4. Let E1, E2be TSEs over T , T[ T and b be a well-formed formula.

G is a function that maps a TSE to a subset of S such that 1. G(«) 5 hhj, where h denotes the empty task sequence.

2. G(T) 5 hktlj, where t denotes an invocation of T and k l denotes a task sequence.

3. G(E1, E2)5 hs1n s2us1[ G(E1)` s2[ G(E2)j, where n stands for concatenation.

4. G([E1])5 hhj < G[(E1)].

5. G(b1E1~ b2E2)5 G(b1?, E1)< G(b2?, E2).

6. G((bE1)*)5 G((b?, E1)*, (¬b?, «))

5 hs n¬b? n hus [ G((b?, E1)*)j,

whereG((b?, E1)*)5 <^yi51Gⁱ(b?, E1), andGⁱ(b?, E1)5 hs1n s2n . . . n siusj[ G(b?, E1), 1# j # ij

7. G(E1; E2)5 hs1n s3n s2us1[ G(E1)` s2[ G(E2)` s3[ S ].

A TSE can be described at either the task level (a global TSE) or at the method level (a local TSE). In Figure 2, EF5 (F; B) and EM₂5 (b1D ~ b2E) are examples of global and local TSEs, respectively. A TSE at the task level is used to document global interactions between the current task and tasks at different levels that require special attentions in implementing and testing the system. A TSE at the method level documents the local control flow between subtasks of the method. To specify a global interaction, a global TSE often uses the ‘‘follow’’ operator (‘‘;’’) to describe a set of partial task sequences. In contrast, a local TSE, which typically does not contain the ‘‘follow’’ operator, completely describes the control flow among the method’s subtasks. A TSE that does not contain the ‘‘follow’’ operator is called a complete TSE; otherwise, it is called a partial TSE.

There is another important difference between the semantics of the global TSE and the local TSE. A global TSE describes expected system behavior when the associated task is invoked. This property plays an important role in combining TSE’s at different levels. The current task to which a global TSE is associated is denoted by ‘‘1’’. The semantics of the global TSE implies that it is meaningless to use optional, conditional, and selection operators for a task to which the task level TSE is associated, and therefore TSEs such as ([1]), (b1), and (1 ~ Ti) are invalid TSEs at the task level.

C. Composition Operators

Multiple TSEs often need to be combined to obtain a global view of the system’s behavior from pieces of local behavior specifications. To achieve this, a composition operator is developed for combining two TSEs with a designated task T (called task-based composition operator), denoted as%T. The semantics of composing two TSEs is defined through the corresponding set of task se- quences. To compose two task sequences on a designated task invocation, de- noted as (s1 %t s2), is defined by examining the relationship between the two sequences. We have identified three types of relationship between any two task sequences.

(a) Two task sequences may share a common subsequence containing an invocation of a designated task T [see Fig. 3(a)].

(b) Two task sequences are irrelevant w.r.t. a designated task T, if at least one task sequence does not contain an invocation of T [see Fig. 3(b)].

(c) Two task sequences, s1and s2, are said to have a conflicting subsequence w.r.t.

a designated task T, if (1) the task sequences contain the invocation of T, (2) there exists a predecessor (or successor) of T in s1that is different from that in s2(which is called a conflicting predecessor or successor), and (3) the conflicting

Figure 3. Relationships between any two task sequences.

predecessor (or successor) is not mapped to by a ‘‘follow’’ operator. Note that condition (3) is necessary in that, based on the definition of the follow operator, we can always find a conflicting predecessor (or successor) when composing a complete TSE with a partial one [see Fig. 3(c)].

DEFINITION5 (Composing Two Task Sequences). Suppose s₁and s₂are two task sequences. The composition of s₁and s₂on an invocation of a designated task T, denoted as (s₁%t s₂), is defined as follows:

● If s1and s2are sharing a common subsequence on an invocation of T, then if s15 s91n a and s25 a n s92then s1%ts25 s91n a n s92

else if s15 s91n as01and s25 a then s1%ts25 s91n a n s02

● If s1and s2are irrelevant, then s1%ts25 s1<s2.

● If s1and s2have a conflicting subsequence containing an invocation of T, then s1

%ts25 h.

The semantics of composing two TSEs conditioned on a designated task T, is defined through its corresponding set of task sequences,G(E1%TE2). That is, we can take a task sequence from E1and compose it with all task sequences in

E2by taking the union, and repeat the same process until all task sequences in E1are considered. This is formally defined below.

DEFINITION 6 (Composing Two TSEs). Let E1 and E2 be two TSEs over T . Suppose T is a task in T . The semantics of composing E1and E2conditioned on the designated task T, denoted as E1%TE2, is defined as follows:

G(E1%TE2)5;s₁[G(

<

(s1%ts2)

It is trivial, from Definition 6, to show that the composition operator has the following properties:

● commutative: E1%TE25 E2%TE1.

● associative: (E1%TE2)%TE35 E1%T(E2%TE3).

However, not all TSEs in task structures are eligible for composition. There are two factors that affect the composability of TSEs: the conflicting task sequence and the follow operator. Intuitively, if there exists a conflicting task sequence in the to-be-composed TSEs, then we should not compose the TSEs. However, to compose a partial TSE with a complete TSE, we need to ensure that there does not exist a task sequence in the complete TSE that is conflicting with every possible task sequences of the partial TSE. A formal definition of composability is described below.

DEFINITION7 (Composability). Two TSEs, E1and E2, are not composable condi- tioned on a designated task T, iff's1 [ G(E1),;s2[ G(E2), such that s1and s2

are conflicting w.r.t. T.

The following theorems for composing TSEs follow from Definition 4 and 6.†

THEOREM1. Let E and ETbe two TSEs over T , and T be a task in T . If E does not contain any invocation of T inG(ET), then E %TET5 E ~ ET.

THEOREM2. Let E1, E2, and ETbe three TSEs over T . ETdenotes a TSE in which T appears. (E1~ E2)%TET5 (E1%T)~ (E2%TET).

THEOREM 3. Let E1 and E2 be two TSEs over T , E1 5 (a, T, b(c1, c2)), and E25 (T, b(c1;g)), where a, c1,c2andg are TSEs, and b is a condition. E1%T

E25 (a, T, b(c1,c2;g)).

To summarize, there are two important characteristics of the task-based composition operator. First, to prevent any arbitrary composition, the composi- tion is conditioned on a designated task to focus the attention on tasks that are

†All proofs of theorems can be found in Appendix A.

Task: Model:

. Model Specification: . Parent Task:

- Domain Model: . Guard Conditions:

- State Model: . Subtasks:

. Process Specification: . TSE:

- TSE:

- Precondition:

- Postcondition:

Figure 4. Task and method specification templates.

related to or interacted with the designated task. Second, combining a complete TSE with a partial one will help to fill in some of the missing details by fusing multiple pieces of behavioral specification.

As an illustration of the composition of TSEs, let us consider the following example. Suppose EM5 (T1, [T3]), and ET₃5 (1; T4).

EM%T₃ET₃5 ((T1)~ (T1, T3))%T₃(T3; T4) (1) 5 (((T1)%T₃(T₃; T₄))~ ((T1, T₃)%T₃(T₃; T₄))) (2) 5 ((T1)~ (T3; T₄)~ (T1, T₃; T₄)) (3)

In this example, the global TSE is associated with T3. However, T3 is an optional task in its parent method. To compose EMand ET₃, from Definition 4, we can transform EMinto an equivalent TSE that has two components: one that always invokes T3, the other that does not invoke T3at all. Based on Theorem 2, we can derive Eq. (2). Equation (3) follows directly from Theorem 1 and Definition 6.

Templates for tasks and methods specifications are shown in Figure 4. A task can be described using the triplekprecondition, protection, postconditionl, and the relationship between the task and tasks at different levels is captured by a global TSE. A task in a task structure can be refined into a set of methods that can accomplish the task. Each method can be further refined by specifying subtasks involved and sequencing relationship between subtasks using a local TSE. The specifications of tasks and methods are defined below.

DEFINITION8 (Task Specification). A specification of a task T is a tuplekCT, ETl, where CTis a triplekBT, PT, RT~ (RT` ST)l, and ETis a task state expression involving tasks which have global interaction with T.

DEFINITION 9 (Method Specification). A method specification of a task T is a quadruplekT, g, ST, EMl, where g is a formula describing the guard condition under which the method is applicable, S T is a collection of subtasks, and EMis a TSE involving subtasks in S T.

IV. COMPUTING STATE DESCRIPTIONS IN TASK STRUCTURES In software specifications, it is desirable to compute the description of a state after the application of a transition.¹⁸Similarly, researchers in AI planning are concerned about synthesizing a plan (that is, a sequence of actions) which involves constructing a state description after executing an action. Both software specifications and AI planning share a similar problem: How to keep track of what has not been changed? (This is the so-called frame problem¹⁹.) The frame problem and its partial solutions are introduced in the next section. Section B elaborates on the proposed approach to the frame problem in the context of task structures.

A. Frame Problem in Software Specifications

In AI planning, frame axioms have been used to describe what has not been changed after the performance of an action. However, the problem arises when the number of frame axioms increases rapidly with the complexity of the applica- tion. Several partial solutions have been proposed. Fikes and Nilsson used the notion of differences, as well as ideas from the situation calculus to make the assumption that the initial world model would only be changed by a set of additions to, and deletions from, the statements modeling the world state—every- thing else remained unchanged.²⁰ This assumption is sometimes called the STRIPS assumption. Hayes proposed using causal connections as a frame rule to the frame problem.¹⁹The assumption is that if a term (or a nonlogical symbol) is not connected to an action, then any change to the action does not affect the term.

In software specifications, it is sometimes necessary to express explicitly the fact that certain variables do not change value (or state) due to the performance of a task.^21,22ASLAN²¹provides four procedural operators: NoChange, ALTerna- tive, Conditional, and Become, to explicitly specify unmentioned variables which are assumed not to have changed; meanwhile, the notationQ in Z has been used to denote that any variable followed by theQ will not change value, and J is used to indicate that any state space followed byJ will not change. Four types of solutions to the frame problem are identified below:‡

● Domain-independent approaches: the solution is designed to be applicable to a wide variety of domains, for example, STRIPS assumption and the causal connec- tion frame rule.

● Domain-independent, if-needed-basis approaches: a frame axiom is generated by the system on a if-needed-basis. A typical example of this approach is the NoChange operator in ASLAN, which is generated if the correctness of a specification cannot be proved due to the missing of values for variables.

● Application-specific approaches: frame axioms are tightly related to the application, and therefore, it is necessary for users to explicitly specify what will remain unal- tered, for instance, the notion of invariant in software specifications such as Z.²²

● Operator-specific approaches: the solution is tied to a specific implementation of

‡A similar classification scheme can be found in Ref. 23.

a specification language, and is only applicable to that particular language. The procedural operators in ASLAN are examples of this category.

To compute the description of a state involves not only the propagation of what has not been changed, but also the progression of what has been changed.

Rosenschein’s progression operator²⁴and Waldinger’s regression operator²⁵are two similar approaches to only specifying what has been changed using a tuple kprecondition, postconditionl in the state before and after an action. A progres- sion operator is a function that maps conditions that are true immediately before a task (called before-state description) to conditions that are true immediately after the task (called after-state description), which is formally defined below.

DEFINITION10 (Progression Operator). A progression operator, denoted as /; for T is a function mapping from formulas to formulas, such that for every triplekb, dˆ

, al [ T, ifwis true in state b, thenw/T is true in state a.

;kb, dˆ

, al [ T, b u5w^⇒au5 w^/T

In the proposed framework, for the purpose of verification, it is desirable to compute the description of a state that is obtained through a TSE to an initial state description, which is addressed in the next section.

B. Computing State Descriptions

As was noted by Borgida et al.²³ that the frame problem is still an open issue and that it is likely no single general solution exists. In this section, the notions of progression operator, default rule, and frame axioms are introduced to address this problem in the context of task structures.

To extend the progression operator in the context of task structures, we first assume the description of a state is in a disjunctive normal form. An assump- tion about the forms of the precondition and the postcondition of a task is also made, that is, the precondition is a conjunction of literals; while the postcondition assumes a disjunctive normal form.

Second, the notion of default rule proposed by Reiter²⁶ and frame axioms advocated by Hayes¹⁹ are incorporated into the semantics of the progression operator to specify state descriptions that remain unchanged after performing a task. The default rule and frame axioms are used to describe state descriptions that remain unaltered after performing a task. In default logic, unless there is knowledge to the contrary, we assume what is assumed to be true in the before state is also assumed to be true in the after state. Thus, the default rule is formulated as: a literal in the description of a state will remain intact if the literal is not contradictory to the postcondition of the task. This is formally defined below.

DEFINITION 11. Let the state descriptionwito a task T in a specification be in a disjunctive normal form:w5 (w1~w2~ ? ? ? ~wn), wherewiinwis a conjunction of literals:wi5 (l1` l2` . . . ` ln), andwiR BT,wi/T5 RT`wj, wherewjis a conjunction of literals and liinwisuch that liis not contradictory to RT.

Several features in the proposed framework facilitate the formulation of frame axioms: domain model, state model, and protections. Both the value of a variable and the state of an object in the model specification of a task can be changed after performing the task, which is analogous to the value of a variable (or a state variable) in conventional software specifications. Most software speci- fications methods use a variable with a prime (that is,9) to represent the old value of the variable and a variable without the prime for new value of the variable, which is a convention adopted in the proposed framework. The same approach is used for representing the change of status for a state variable in conventional software specifications. However, in the proposed framework, the notion of state objects in the state model, represented using either a proposition or a predicate, is used to reflect the change of status for an object. Therefore, predicates in the domain model of a task should never be changed after the task.

From the definition of protections in the functional specification of a task, the predicates in the protection should remain intact after the execution of the task.

Based on the above discussion, the following lemma can be derived.

LEMMA1. Let D be the domain model of a specification and the state description wito a task T in the specification be in a disjunctive normal form:w5 (w1~w2

~ . . . ~wn), wherewiin w is a conjunction of literals:wi5 (l1 ` l2` . . . ` ln), andwiR BT,wi/T5 RT`wj, wherewjis a conjunction of literals and liin wiin wisuch that lisatisfies any of the following:

1. liis a domain model predicate.

2. liis a predicate in the protection of T.

Third, since the proposed framework adopts the notion of task structures for functional decomposition, the progression is only performed within each task (that is, the task, its methods, subtasks of the methods, and tasks related through global interactions). In another word, the initial state description is the conjunct of the precondition of the task and the guard condition of the task’s method, and the state descriptions are progressed through the composed TSE of the task’s method TSE and the TSE of any high level task that has global interactions with any task in the method.§ For example, in Figure 2, to propagate through the task D is to progress through the composed TSE: EM₃ %F EB with BD ` bM₃as the initial state description.

To progress a state description through an immediate follow operator (‘‘,’’) in a TSE, there are two conditions which need to be satisfied: (1) the state description is in a disjunctive normal form, and (2) the precondition of a task T that immediately follows the operator can be derived from every disjunct in the state description. The result of the progression through the immediately follow operator will be equivalent to the disjunction of applying the progression operator

§To make it consistent in the presentation, ‘‘/’’ is used to represent both the progres- sion operator through a task and a TSE.

to each individual disjunct over the task T. This is formally described using the following theorem.

THEOREM4. Suppose the initial state descriptionwto a TSE E is in a disjunctive normal form:w5 (w1~w2~ . . . ~wn), wherewiinwis a conjunction of literals.

If E 5 («, T) and ;iwiR BT, then (w1,~ . . . ~wn)/E 5w1/T~ . . . wn/T.

To progress a state description through a selection operator (‘‘~’’) in a TSE, several conditions need to be satisfied: (1) the state description is in a disjunctive normal form, (2) at least one disjunct in the state description can deduce the precondition of the task T (i.e., BT) that is used with the selection operator.

The result of the progression is a disjunction of applying the progression operator over T to those disjuncts that can derive BT, and applying the progression operator to those disjunctions that cannot derive BT.

THEOREM5. Suppose the initial state descriptionwto a TSE E is in a disjunctive normal form:w5 (w1~w2~ . . . ~wn), wherewiinwis a conjunction of literals.

E 5 (T1~ T2)

If w 5 w9 ~ w0 wherew9 and w0 are in disjunctive normal form, such that

;wiinw9,wiR BT₁, and;wjinw0,wjR BT2, then (w9 ~w0)/ E 5w9/T1~ (w0)/T2. Based on the above discussion, the following algorithm will compute the state description through a TSE E to an initial state descriptionw. A specification is said to be weakly inconsistent if a consistency condition cannot be proved;

meanwhile, if a consistency condition can be disproved, then the specification is said to be strongly inconsistent (the detail of levels of inconsistency is described in the next section).

ALGORITHM1 (Progression Algorithm for a TSE). Assume that the initial state descriptionwto a TSE E is in disjunctive normal form:w5 (w1 ~w2~ . . . ~ wn), wherewiinwis a conjunction of literals. Domain model predicates are denoted aswD.

1. E 5 («, T)

Case 1: If;iwiR BT, then (w1~ . . . ~wn)/E5w1/T~ . . . ~wn/T.

Case 2: If'wisuch thatwiRy BT, then weakly inconsistent.

Case 3: If'wisuch thatwiR¬BT, then strongly inconsistent.

2. E 5 (T1~ T2)

Case 1: Ifw5w9 ~w0 wherew9 andw0 are in disjunctive normal form, such that ;wi in w9,wiR BT1, and ;wjin d0,wj R BT₂, then (w9 ~ w0)/E 5w9/T1~w0/T2.

Case 2: if'ywiinw^{such that}wiR BT₁orwiR BT₂, then weakly incon- sistent.

Case 3: If'wiinw^{such that}wiR¬BT₁andwiR BT₂, then strongly incon- sistent.

3. E 5 («; T)

w/E 5 RT`wD` PT`w9, wherew9 is the state description constructed by the expression performed immediately before T.

4. E 5 (bT)*

w/E 5¬b `wD` PT`w9, wherew9 is the state description propagated immediately before exiting the iteration.

V. VERIFICATION OF SPECIFICATIONS

The verification of a specification is important because it helps early detec- tion of errors in the software life cycle to produce an adequate specification, thus eliminating possible design failures and reducing product costs. The proposed framework provides two levels of inconsistency checking in a single layer: strong and weak inconsistency. A system specification is weakly inconsistent if its consis- tency cannot be proved. On the other hand, a system specification is strongly inconsistent if its consistency can be disproved. The proposed framework also checks for if a refinement is consistent by comparing the specificity of conditions at the high layer to that of the low layer. Types of faults that could result in an inconsistent process specification include protection violation, precondition violation, postcondition violation, and incorrect TSEs. Missing methods will result in incompleteness in the specification.

A specification of a task or a method of a system is consistent if (1) the precondition of a task in the TSE of a task or a method can be deduced from the state description before performing the task; (2) the postcondition of the task can be deduced from the description of the state after performing the task;

and (3) the protection of T can be deduced from state descriptions before, after, and during performing the task.

Thus, a method specification of a task is weakly inconsistent if (1) the precondition of a task in the TSE of the method cannot always be deduced to be true from the state description after the task: (2) the postcondition of the task cannot always be deduced to be true from the state description before the task; and (3) the protection of the task cannot always be deduced to be true from the state description before, after, or during the task. In contrast, a method specification of a task is strongly inconsistent if (1) the precondition of a task in the TSE of the method can sometimes be proved to be false from the state description after the task; (2) the postcondition of the task can sometimes be proved to be false from the state description before the task; and (3) the protection of the task can sometimes be proved to be false from the state description before, after, or during the task.

The consistent refinement checking is performed between adjacent levels of a task and its methods. The mechanism for verifying the consistency is to check for if a refinement is consistent by comparing the specificity of conditions at the high level to that of the low one.

DEFINITION 12 (Specificity of Conditions). A condition C₁ is exclusively more specific, denoted asa, than condition C2if and only if for all states s, if s satisfies C₁, then s satisfies C₂, but not vice versa (i.e., they are not equivalent).

C1a C2⇔(;s, s u5 C1⇒su5 C2)` ¬(;s, s u5 C2⇒su5 C1)

DEFINITION 13 (Consistent Refinement). A refinement of a task T is consistent with T’s specification, if and only if the collection of state transitionkb, dˆ

, al of T’s methods is a subset of the collection of T’s state transitionkb, dˆ

, al [ T.

THEOREM6 (Inconsistent Refinement). LetkCT, ETl be a task specification of T, andkT, g, S T, EMl a method specification M of T. M is an inconsistent refinement of T, if one of the following holds:

1. BTsy BM. 2. PTsy PM. 3. RTsy RM.

4. RT` STsy RM` SM.

THEOREM 7 (Protection Violation). A refinement of T is inconsistent, if w ^is protected during task T, there exists a subtask T9 of a method M in T’s refinement such that the rigid postconditions of T9 can deduce¬w^.

DEFINITION14 (Complete Refinement). A refinement of a task T is complete with T’s specification, if and only if the collection of the before states of T’s method specifications is equivalent to the collection of the before states of T.

The verification of the process specification starts from the highest level task, and focuses one task at a time.

ALGORITHM2. To verify a task, there are two major steps involved:

1. The specification of a task T is compared with the method that contains T (called T’s parent method) and other subtasks in the method to prove or disprove T’s precondition using the resolution algorithm.

2. The specification of a task T is compared with those methods (and their subtasks) that accomplish T (i.e., T’s child methods) for consistency and completeness checking.

(a) The specification of a T’s method is consistent with T if

i. the description of the state prior to executing the method, referred to as the before state description, is semantically more specific than T’s precondition,

ii. the description of the state after executing the method, referred to as the after state description, is more specific than T’s rigid postcondition, iii. the protection of T is not violated by any subtasks of T.

(b) The specification of T’s methods is considered complete if the union of their before state descriptions is equivalent to T’s precondition.

Task: configure modules

● Model Specification:

— Domain Model: (omitted)

— State Model:

* A moduled backplane is a backplane that 1) has as many modules as possible been placed in, and 2) satisfies the constraint of maintaining the optimal ordering of modules configured into the backplane.

● Process Specification:

— Precondition: There exists a current backplane, and a sequence of modules.

— Protection: The optimal ordering of modules should be maintained (inherited).

— Postcondition:

* (rigid) The chosen backplane is a moduled backplane.

Figure 5. Configure modules.

VI. AN EXAMPLE

Based on an original implementation and documentation of R1/SOAR, the reimplementation of a major portion of the well-known computer configuration expert system R1,¹¹ we have constructed, in a reverse engineering fashion, a specification for R1/SOAR to evaluate the proposed framework.

R1/SOAR focuses on the unibus configuration task of the entire configura- tion task of R1. The problem is given a customer’s order, place the modules on the order into backplanes, and the backplanes into boxes on the correct unibus.

The backplanes need to be cabled together, and the panel space allocated when required by the modules. If the containers on order are not sufficient to hold the modules, additional containers must be ordered.

The following example is from a subset of the task-based specifications of R1/SOAR. Two major tasks of concern in this example are configure modules and configure a module. The functionality of the task configure modules is to configure as many modules as possible into the current backplane while main- taining the optimal ordering. This is achieved by iterating between two subtasks:

(1) configure a module, which attempts to configure the current module into the current backplane, and (2) obtain the next module, which gets an ordered module that follows the current module in the optimal ordering.

One of the errors that a knowledge engineer is likely to make is about the situation when the current module fails to be configured into the current back- plane. A correct specification should indicate that obtain the next module should be skipped under the situation, since we have not finished configuring the current module yet. It is also desirable to indicate that if the current module cannot be configured into the current backplane, the system should later find a backplane suitable for the current module before configuring the next module. The specifi- cations for the tasks and methods relevant to this example are shown in Figures 5, 6, and 7. We discuss the state model, functional specification, and behavioral specification relevant to the example below, and show how the common error mentioned above can be detected by the verification algorithm.

Functional specification: An example of protections in R1/SOAR is that the optimal ordering in which modules are configured should be maintained in the

Method:

● Parent Task: Configure Modules

● Guard Condition: TRUE

● Subtasks:

— T1: configure a module.

— T2: obtain the next module.

● TSE: (T1, [T2])*

Figure 6. A method of the task configure modules.

task unassigned backplane. Consequently, both tasks inherit the protection from the parent task unassigned backplane. The postcondition of the subtask configure a module is a conjunction of two conditions, corresponding to the two possible outcomes that the task succeeds or fails in configuring the current module into the current backplane.

Behavioral specification: The rational underlying TSEs in this example is that if the current module and current backplane are incompatible, then we should latter find a backplane suitable for the current module and not to try to configure another module using the current backplane, because doing so will violate the protection to maintain the optimal ordering of modules. From the local TSE of the method, EM5 (T1, [T2])*, and the global TSE of T1, ET₁5 (1;

[T3]) (see Fig. 7), the result of the composition can be derived as follows:

EM%T₁ET₁5 ((T1, [T₂])*%T₁(T₁; [T₃]) (4) 5 ((T1, [T₂])*; [T₃]) (5)

Task: configure a module

● Model Specification:

— Domain Model: (omitted)

— State Model:

* A current module is said to be compatible with the current backplane if 1. The current module’s unibus load is less or equal to the univus load left.

2. The current module’s pin type is the same as the current backplane’s pin type.

3. The current module is a kmc11 and the backplane is either 4-slot or 9-slot.

4. Modules’ power drawn for some type of power is less or equal to the available power of that type.

5. There is enough room for the current module in the backplane.

● Process Specification:

— TSE: (1;[T3: find a backplane suitable for current module])

— Precondition: There exists a current module, and a current backplane.

— Protection: The optimal ordering of module should be maintained (inherited).

— Postconditions (disjunctive):

* (rigid)

1. The current module is compatible with the current backplane and is configured into the current backplane. Or,

2. The current module is not compatible with the current backplane and the current backplane is a moduled backplane.

Figure 7. Configure a module.

Verification: If the TSE of the method were (T1, T2)*, a strong inconsistency will be detected by the verification algorithm because the postcondition of con- figure a module can be formally expressed using the following logic formula:

configured(current2 module)

~ incompatible(current 2 module, current 2 backplane) Invoking the sequence, (. . . T2, T1. . .), when the current module is incompati- ble with the current backplane leads to configuring the next module before configuring the current one. Hence, two strong inconsistencies can be detected:

(1) the precondition of the task obtain the next module, which states that the current module should have been configured, can be violated, and (2) the protec- tion that the optimal ordering of modules should be maintained can also be vio- lated.

VII. RELATED WORK

We briefly compare our methodology with major alternative specification methodologies for knowledge-based systems below.

● Zualkernan and Tsai have developed two specification methodologies for expert systems: an object-oriented methodology, and a knowledge-model methodology.⁶ The object-oriented methodology first establishes the object class for specifying instances of each of the expert activity involved, which is followed by the definition of the methods for each class, and then the instantiation of class instances. The knowledge-model methodology describes the concept structures and the goal struc- tures that are required to solve the problem. Both methodologies provide a top–

down approach and have been demonstrated for a heuristic classification system.

Verification and validation are performed through the interaction with experts.

Compared to our approach, both methodologies offer two benefits: (1) the specifi- cation is executable, and (2) the methodologies are easier to be applied to the heuristic classification type expert systems.

● Slagle has used conceptual graphs for specifying a heuristic classification expert system.⁴His approach begins with type definitions, identifies the high-level lines of reasoning focused on a few concepts, construct implications, facts, type lattice, and canonical graphs. Like Zualkernan and Tsai’s work, Slagle’s methodology is suitable for heuristic classification type systems, whose knowledge can be specified by constructing an inference network that relates pieces of evidence to hypotheses.

● A problem space approach to expert system specification has been proposed by Yost and Newell.²⁷The approach is designed specifically for the SOAR architecture.

It is difficult to see how the methodology can be applied to other AI architectures.

Furthermore, verification of the specification has not been demonstrated.

The proposed approach offers two important advantages: (1) It provides a solid automatic verification capability. (2) It provides a detailed functional decomposi- tion technique.

VIII. CONCLUSION

In this article, the formal foundation for task structures has been proposed to formulate two major features in process specification: state-transition and process refinement. The general form of state-transition model^24,28is thus adopted

for the purpose of formulating and analyzing the notion of tasks in the structures.

The notion of task structure (i.e., task/method/subtask) is formalized for the analysis of task process refinement. Task state expressions, based on regular expressions, are used to describe expected behavior specifications. Progression operators and frame axioms are adopted for constructing the description of a state through a TSE to an initial state description. Levels of inconsistency: strong and weak, have been identified. The formalism provided by the framework facilitates the verification of specifications. Verification for consistency and com- pleteness is performed for pieces of the specification within one abstraction level or between multiple levels based upon their formal semantics.

Our approach offers several important benefits for specifying knowledge- based systems. First, the incorporation of task structures provides a detailed functional decomposition technique for organizing and refining functional and behavioral specifications of a knowledge-based system. Second, the use of TSEs can assist not only in documenting the expected control flow and module interac- tions, but also in verifying that the behavioral specification is consistent with the system’s functional specification. Third, the verification algorithm is based on its well-defined formal foundation, and is achieved by centering around one func- tional unit at a time. Finally, the distinction between soft and rigid conditions makes it possible to specify conflicting functional requirements.

Future research will consider the following directions: (1) to enhance the verification capability by an extension of the proposed framework which can be facilitated using a principled knowledge representation language (e.g., conceptual graphs²⁹); and (2) to perform a trade-offs analysis for informal requirements.

This research is partially supported by National Science Council (Taiwan, R.O.C.) under Grant NSC 86-2213-E-008-006. The author would like to thank Professor John Yen for his invaluable comments on an early draft of this article.

IX. APPENDIX: PROOFS

THEOREM1. Let E and ETbe two TSEs over T , and T be a task in T . If E does not contain any invocation of T inG(ET), then E %TET5 E ~ ET.

Proof. Since G(E) does not contain any task invocation of T in G(ET), it follows from Definition 6 that

G(E %TET)5 G(E) < G(ET) (6) From Definition 4, we have

G(E ~ ET)5 G(E) < G(ET) (7) Combining Eqs. (6) and (7), we getG(E %TET)5 G(E ~ ET). Therefore, it is proved that

E %TET5 E ~ ET. j

THEOREM2. Let E1, E2, and ETbe three TSEs over T . ETdenotes a TSE in which T appears. (E1~ E2)%TET5 (E1%TET)~ (E2%TET).

Proof. The theorem can be trivially proved based on the Definintion 6 and Definition 4. Based on Definition 6, we have

G((E1%TE2))5;s₁[G(

<

(s1%ts2)

From Definition 4, we know thatG(E1~ E2)5 G(E1)< G(E2). Therefore, G(E1~ E2)%TET)5 G(E1%TET)> G(E2%TET) j THEOREM 3. Let E1 and E2 be two TSEs over T , E1 5 (a, T, b(c1, c2)), and E25 (T, b(c1;g)), where a, c1,c2andg are TSEs, and b is a condition. E1%T

E25 (a, T, b(c1,c2;g)).

Proof. From Definition 4, we know that G(a, T, b(c1,c2))

5 hs91n t n b? n s92n s93us91[ G(a) ` t is an invocation of T ` b? is a task for testingb ` s92[ G(c1)` s93[ G(c2)j

< hs1n t n¬b? n hus91[ G(a) ` t is an invocation of T ` b? is a task for testingb ` h an empty task sequencej

G(T, b(c1;g))

5 ht n b? n s92n s94n s95u t is an invocation of T ` b? is a task for testingb ` s92[ G(c1)` s94[ S ` s95[ G(g)j

< ht n¬b? n hu t is an invocation of T `¬b? is a task for testing¬b ` h is an empty task sequencej

and that (1) for any sequencekt n b? n s92n s4n s95l [ G(T, b(c1;g)), we know that there always exists a sequence kt n b? n s92n s93l such that kt n b? n s92n s93l is a subsequence ofkt n b? n s92n s94l (i.e., kt n b? n s92n s94l 5 kt n b? n s92n s93n s04l, where s04 [ S ), and (2) for any sequence kt n¬b? n hl [ G(T, b(c1;g)), it is obvious thatkt n¬b? n hl is a subsequence of ks91n t n¬b? n hl [ G(a, T, b(c1,c2)).

Based on Definition 6, the result of composition is G(E1%TE2)

5 hs91n t n b? n s92n s93n s04n s95us91[ G(a) ` t is an invocation of T ` b? is a testing task forb ` s92[ G(c1)` s93[ G(c2)` s04[ S ` s5[ G(g)j

< hs91n t n¬b? n hus91[ G(a) ` t is an invocation of T `¬b? is a task for testingb ` h is an empty task sequencej

Based on Definition 4, we have G(a, T, b(c1,c2;g))

5 hs91n t n b? n s93n s04n s95us91[ G(a) ` t is an invocation of T ` b? is a testing task forb ` s92[ G(c1)` s93[ G(c2)` s04[ S ` s95[ G(g)j

< hs91n t n¬b? n hus91[ G(a) s t is an invocation of T `¬b? is a task for testingb ` h is an empty task sequencej

Hence, the theorem (E1%TE2)5 (a, T, b(c1,c2;g)) is proved. j THEOREM4. Suppose the initial state descriptionwto a TSE E is in a disjunctive normal form:w5 (w1~w2~ . . .w wn), wherewiinwis a conjunction of literals.

If E 5 («, T) and ;iwi R BT, then (w1 ~ . . . ~wn)/E 5 w1/T~ . . . ~ wn/T.

Proof. The proof of this theorem is outlined below: Since bu5w1 ~ . . . ~wn

⇔bu5w1~ . . . ~ b u5wn, we can derive that au5 (w1~ . . . ~wn)/T⇔au5 w1/T~ . . . ~wn/T. Given the precondition of the task can be deduced from everywi, we know that everyw/T is valid. Thus, the theorem is proved. j THEOREM 5. Suppose the initial state descriptionw to a TSE E is a disjunctive normal form:w5 (w1~w2~ . . . ~wn), wherewiinwis a conjunction of literals.

E 5 (T1~ T2)

If w 5 w9 ~ w0 wherew9 and w0 are in disjunctive normal form, such that

;wiinw9,wiR BT₁, and;wjinw0,wjR BT₂, then (w9 ~w0)/E 5w9/T1~ (w0)/T2. Proof. This theorem can be trivially proved by showing that since w0 can not deduce the precondition of T,w0/T1is not defined. Similarly,w9/T2is not defined

either. j

THEOREM6. (Inconsistent Refinement). LetkCT, ETl be a task specification of T, andkT, g, S T, EMl a method specification M of T. M is an inconsistent refinement of T, one of the following holds:

1. BTsy BM. 2. PTsy PM. 3. RTsy RM.

4. RT` STsy RM` SM.

Proof. This theorem can be trivially proved by following directly from Definition

12 and 13. j