Macro control languages and decision procedures for COCOLOG

The control of a discrete event system is handled in the COCOLOG logic control system by use of an extra-logical representation of the control laws in terms of conditional control rules; these are condition-action pairs in which the conditions are mutually exclusive and exhaustive formulas in the language (L_k) at the instant k. Such formulas are tested for deducibility from Th_k, the current control theory, and once the unique deducible formula is found, the associated control action is applied to the system. The simplicity of L_k leads to even the most basic concepts having a complex expression as well formed formulas in L_k. Furthermore, the triggering of elementary control actions often depends upon complex nested sets of conditional control formulas expressed in L_k. In response to this set of problems, this article presents the foundations for: 1) a theory of the expression of complex predicates and functions in terms of simple macro language symbols which can be defined in an extended language L_k⁺; and 2) the construction of recursive systems of simple macro actions to express complex control actions