• DocumentCode
    490287
  • Title

    Logic Control via Automatic Theorem Proving: COCOLOG Fragments Implemented in Blitzensturm 5.0

  • Author

    Caines, P.E. ; Mackling, T. ; Wei, Y.J.

  • Author_Institution
    The Canadian Institute for Advanced Research, Canada; Department of Electrical Engineering, McGill University 3480 University Street, Montreal, P.Q., Canada H3A 2A7 Tel.(514)-398-7129, em: peterc@moe.mcrcim.mcgill.edu
  • fYear
    1993
  • fDate
    2-4 June 1993
  • Firstpage
    1209
  • Lastpage
    1213
  • Abstract
    The COCOLOG sstem is a partially ordered family of first order logical theories that describe the controlled evolution of the state of a given partially observered finite machine M. Following the review of the general theory of COCOLOG, the notion of Markovian fragments MThk,k ¿ 1, of full COCOLOG theories Thk, is presented. These fragments enjoy the property of having axiom set of fixed size over time. MThk and Thk, have the virtually same state estimation and control power. Next, a newly developed automatic theorem proving software called Blitzenstrum is described and some applications Blitzenstrnm 5.0 to the logic control of a stylized elevator problem are presented.
  • Keywords
    Application software; Automatic control; Automatic logic units; Control systems; Elevators; Software testing; State estimation;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    American Control Conference, 1993
  • Conference_Location
    San Francisco, CA, USA
  • Print_ISBN
    0-7803-0860-3
  • Type

    conf

  • Filename
    4793060
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=490287