COCOLOG - A CONDITIONAL OBSERVER AND CONTROLLER LOGIC FOR FINITE MACHINES

The problem of observation and control for partially observed input-state-output machines is formulated in terms of a tree of first-order logical theories. A set of first-order languages for the description of the controlled evolution and state estimation of any given machine M is specified; further, extralogical conditional control rules are formulated so that closed loop control actions occur when extralogically specified past observation dependent conditions are fulfilled. In particular, conditional control rules may include commands that steer the system state from a current partially observed state (estimate) to a target state if such a sequence of controls can be proven to exist. Starting from a general theory of M at the initial instant, observations on the input-output behaviour of the system at each later instant are accepted by the system as new axioms; these are then used together with the previously generated theory to generate the current theory. The acronym COCOLOG is used to denote the family of first-order conditional observer and controller logics for any given input-state-output system. A semantics is supplied for each COCOLOG system in terms of interpretations of controlled transitions on a tree indexed by the possible sequences of input-output observations. Extralogical rules, including the conditional control rules, relating members of the family of theories of a COCOLOG system are presented in the form of a set of metalevel rules. Following the complete definition of a COCOLOG system, the consistency and completeness of the first-order theories in a COCOLOG system are established, decidability is obtained using a unique model property, and examples of the operation of a COCOLOG logic control system are given.