COCOLOG is implemented through a combination of automated deduction (first order theorem-proving) and model verification techniques. This is achieved in software created by T. Mackling which, in one current version, utilises a ``semantic attachment facility''. In this system, the user can specify or define predicate and functional symbols by a formula in the language of first order logic providing that each predicate symbol and (possibly recursively specified) functional symbol occurring in the definitional part is ``semantically attached". Semantic evaluation (as part of the model verification) of a first order logical expression involves the dynamical syntactical reduction of expressions (and hence their subexpressions) as they are evaluated. This process of ``quantifier pushing'' makes the model verification of defined predicates viable. The software was recently tested in a real-time simulation of the COCOLOG control of two elevators in a forty floor building. A second project under this heading involves the re-expression of the tree of nested first order logical theories of a COCOLOG system in terms of Branching Time, or Computation Tree, Logic (CTL). Here, branching time logic modal operators are adjoined to the basic Markovian fragment COCOLOG language. The feasibility of verifying safety, liveness and correctness of COCOLOG control laws in this framework is being evaluated and to this end, amongst others, a CTL tableau based formula verification scheme has been formulated.

T. Mackling, P.E. Caines

Mon Nov 13 10:43:02 EST 1995