The logical control of an elevator

This paper presents a detailed example of the design of a logical feedback controller for finite state machines. In this approach, the control objectives and associated control actions are formulated as a set of axioms each of the form X implies Y, where X asserts that (i) the current state satisfies a set of conditions and (ii) the control action y will steer the current state towards a given target state; Y asserts that the next control input will take the value y. An automatic theorem prover establishes which of the assertions X is true, and then the corresponding control y is applied. The main advantages of this system are its flexibility (changing the control law is accomplished through changing only the axioms) and the fact that, by the design of the system, control actions will provably achieve the control objectives. The illustrative design problem presented in this paper is that of the logical specification and logical feedback control of an elevator