The COCODEF approach to COCOLOG logic control

In this paper, we present the application of Macro COCOLOG definition expressions to COCOLOG control theories themselves. In particular, the reachability relation on systems which can be modeled in COCOLOG is shown to have a definition in a subset of the basic axiom set of COCOLOG. The definition of the reachability predicate is then explored in the light of possible extensions to the arithmetic system in COCOLOG. Given the fact that reachability is a fundamental system-theoretic concept, the definition expression describing this predicate is given the special status of a definitional axiom. The application of definability theory to COCOLOG control theories then gives rise to COCO^DEF, in which the original COCOLOG framework is shown to have an equivalent definitional framework. Furthermore, Macro actions themselves are shown to have a definitional expression equivalent to them. A couple of examples used elsewhere in the Macro COCOLOG framework are then reformulated to show the application of this approach