Markovian Fragments of COCOLOG Theories

  • P. E. Caines
  • Y. J. Wei
Part of the The IMA Volumes in Mathematics and its Applications book series (IMA, volume 73)


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(Lk), 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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Cai88]
    P.E. Caines. Linear Stochastic Systems. John Wiley and Sons Inc. New York, 1988zbMATHGoogle Scholar
  2. [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
  3. [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
  4. [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
  5. [CL73]
    Chin-Liang Chang and R. Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.zbMATHGoogle Scholar
  6. [JO89]
    J.S.Ostroff. Real Time Temporal Logic. John Wiley, NYC, 1989Google Scholar
  7. [RG87]
    R.Goldblatt. Logics of Time and Computation. CSLI/Stanford, Stanford, CA, 1987.zbMATHGoogle Scholar
  8. [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
  9. [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 1713, INRIA-Sophia-Antipolis, 1992.Google Scholar
  10. [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
  11. [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
  12. [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

Copyright information

© Springer-Verlag New York, Inc. 1995

Authors and Affiliations

  • P. E. Caines
    • 1
    • 2
  • Y. J. Wei
    • 1
    • 2
  1. 1.Department of Electrical EngineeringMcGill UniversityMontreal, P.QCanada
  2. 2.Canadian Institute for Advanced ResearchCanada

Personalised recommendations