**Authors: **[tex2html_wrap4412]*P.E. Caines, D. Dyck, T. Mackling, C. Mascarua, Y-J. Wei*

**Investigator username:** peterc

**Category: ** systems and control theory

**Subcategory:**

The acronym COCOLOG stands for (*families of first order*) *conditional observer and controller logical theories*. In the
foundational work with S. Wang, problems of observation and control for
partially observed input-state-output machines were formulated in terms
of COCOLOG trees of first order logical theories. Subsequent work with
Y-J. Wei has resulted in the definition of the so-called Markovian
fragment systems of full COCOLOG theories; these have the property that
they have virtually the same control decision making power as full
COCOLOG theories but their axiom sets are of constant size over
time. This is important for automatic theorem proving (ATP)
implementations.

Current work is focusing on
hierarchies of COCOLOG control theories which express and perform the
control of complex systems via their formulation as *hierarchical
control lattices*. These notions form a foundation for work with
C. Mascarua in which COCOLOG is being extended to give expression and
solution to certain geometric control problems such as those arising in
robotics.

Implementation work has involved the creation by T. Mackling of the Blitzensturm series of efficient ATP programs; these are being applied to logic control problems in work with D. Dyck, T. Mackling, and Y-J. Wei.

baron@cim.mcgill.ca