Markovian Fragments of COCOLOG Theories

The COCOLOG (Conditional Observer and Controller Logic) system is a partially ordered family of first order logical theories expressed in the typed first order languages {L _k ;k ≥ 0z describing the controlled evolution of the state of a given partially observed finite machine M The initial theory of the system, denoted Th₀, gives the theory of M. without data being given on the initial state. Later theories, $$\{ Th(o_1^k);k \ge 1\}$$ , depend upon the (partially ordered lists of) observed input-output trajectories, where new data is accepted in the form of the new axioms AXMobs(L _k ),k ≥ 1. A feedback control input U(k) is determined via the solution of control problems posed in the form of a set of conditional control rules, denoted CCR(L_k), which is paired with the theory $$Th(o_1^k)$$. The disadvantage of this formulation is that the accumulation of observation axioms may handicap the speed of reasoning. In this paper, by use of a restricted subset, $$L_k^m$$, of each language L _k , k ≥ 1, we introduce a restricted version of COCOLOG; this is called a system of Markovian fragments of COCOLOG and it is designed so that a smaller amount of information than in the full COCOLOG system is communicated from one theory to the next. Systems of Markovian fragments are associated with a restricted set of candidate control problems, denoted $$ CCR(L_k^m)$$k ≥ 1. It is shown that, under certain conditions, a Markovian fragment theory $$MTh(o_1^k)$$ contains a large subset of $$Th(o_1^k)$$ which includes, in particular, the state estimation theorems of the corresponding full COCOLOG system, and, for the set of control rules $$CCR(L_k^m)$$, possesses what may be informally termed the same control reasoning power. In formal terms, this means that $$MTh(o_1^k)$$ with respect to the well formed formulas in $$L_k^m$$. Hence a theoretical basis is supplied for the increased theorem proving efficiency of the fragment systems versus the full COCOLOG systems. Finally some computer generated examples are given illustrating these results.