# Markovian Fragments of COCOLOG Theories

## Abstract

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* _{0}, 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 AXM* ^{ obs }(*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.

## Preview

Unable to display preview. Download preview PDF.

## References

- [Cai88]P.E. Caines.
*Linear Stochastic Systems*. John Wiley and Sons Inc. New York, 1988zbMATHGoogle Scholar - [CW90]P.E. Caines and S. Wang. “COCOLOG: A Conditional Controller and Observer Logic for Finite Machines”,
*Proceeding of The 29th IEEE Conference on Decision and Control*, Hawaii, 1990. pp. 2845–2850. Complete version of research report, Department of Electrical Eng., McGill University, Montreal, Nov. 1991. To appear,*SIAM J. on Control and Optimization*,Google Scholar - [CW91]P.E. Caines and S.Wang, “On a Conditional Observer and Controller Logic (COCOLOG) For Finite Machines and its Automatic Reasoning Methodology”,
*Recent Advances in Mathematical Theory of Systems, Control, Networks and Signal Processing, II*, Eds. H Kimura, S.Kodama, Proceedings of MTNS-91, Kobe, Japan, June 1991, pp 49–54.Google Scholar - [CMW93]P.E. Caines, T. Mackling, Y.J Wei. “Logic Control via Automatic Theorem Proving: COCOLOG Fragments Implemented in Blitzensturm 5.0”,
*Proceedings of the American Control Conference*, San Francisco, 1993. pp. 1209–1213.Google Scholar - [CL73]Chin-Liang Chang and R. Char-Tung Lee.
*Symbolic Logic and Mechanical Theorem Proving*. Academic Press, New York, 1973.zbMATHGoogle Scholar - [JO89]J.S.Ostroff.
*Real Time Temporal Logic*. John Wiley, NYC, 1989Google Scholar - [RG87]R.Goldblatt.
*Logics of Time and Computation*. CSLI/Stanford, Stanford, CA, 1987.zbMATHGoogle Scholar - [W91]S. Wang.
*Classical and Logic Based Control Theory for Finite State Machines*Ph.D. Thesis McGill University, Montreal, P.Q., October, 1991.Google Scholar - [WC92]S.Wang and P.E. Caines. “Automated Reasoning with Function Evaluation for COCOLOG with Examples”
*The 31st IEEE Conference on Decision and Control*, Tucson, A.Z., 1992, pp. 3758–3763. Complete version: Research Report*N°*1713, INRIA-Sophia-Antipolis, 1992.Google Scholar - [WeC92]Y.J. Wei and P.E. Caines. “On Markovian Fragments of COCOLOG for Logic Control Systems”.
*Proceeding of The 31st IEEE Conference on Decision and Control*, Tucson, AZ, 1992, pp. 2967–2972.Google Scholar - [WeC94]Y.J. Wei, P.E. Caines, “Hierarchical COCOLOG for Finite Machines”,
*Lecture Notes in Control and Information Sciences, Volume 199, 11th International Conference on Analysis and Optimization of Systems*, Eds. G. Cohen, J-P Quadrat, Springer-Verlag, 1994, pp. 29–38.Google Scholar - [WR87]M.Wonham and P.J.Ramadge. “On the Supremal Controllable Sublanguage of a Given Language”,
*SIAM J. on Control and Optimization*, 25(3), May, 1987, pp 637–659.MathSciNetCrossRefGoogle Scholar