next up previous
Next: Composition rules and KL-structures Up: KL-components Previous: Lift definitions

Decomposition methods

specify how a task is achieved through the execution of a set of subtasks, and regulate the data and control flows between such subtasks. Task decomposition methods are formally specified through QDL meta-theories, whose tex2html_wrap_inline1191 predicate meta-variables describe the task decomposition they introduce. The number and syntactical structure of the arguments in each atomic formula tex2html_wrap_inline1193 describe the requirements on methods imposed by tex2html_wrap_inline1191 . The axioms and program parts respectively specify the data and control flow the method establishes among its subtasks. The description of the data flow a decomposition method establishes among its subtasks is done through the definition of input axioms, which specify how the contents of the state variables of some subtasks are used by other subtasks. The control flow among its subtasks is described by a QDL program tex2html_wrap_inline1071 , that specifies which tex2html_wrap_inline1191 should be invoked in each state of execution. The execution state of a decomposition method is described by the values of the state variables of all its subtasks tex2html_wrap_inline1201 .

sorts sort tree
constants (constantsymbol +: sortsymbol) *
functions (functionsymbol +: sortsymb tex2html_wrap_inline977 sortsymbol) *
predicates (predicatesymbol +: sortsymbol *) *
variables (variablesymbol +: sortsymbol) *
metavariables (varsymbol +: metatype) *
tex2html_wrap_inline1217 : predicate
axioms (input axiom) *
program tex2html_wrap_inline1091
a QDL program made from tex2html_wrap_inline1223
conditions and programs on tex2html_wrap_inline1225

The following example shows the formal description of a decomposition method.

predicates sequentialexecution
variables tex2html_wrap_inline1229
metavariables tex2html_wrap_inline1231
axioms tex2html_wrap_inline1233
program tex2html_wrap_inline1235