This paper proposes a deductive approach towards controller synthesis. The system to be controlled and the environment are modeled as phase transition systems and the specification of the entire system is expressed by a hybrid temporal logic formula. Verification rules are used to determine whether the system in conjunction with a control strategy meets the specification. The control strategy is refined until it meets the given specification.
In 1995 IEEE International Symposium on Intelligent Control, Monterey, CA, 1995, pp. 35--41.
Postscript, PDF. © 1995, IEEE Press.