Reasoning about real-time teleo-reactive programs
Brijesh Dongol, Ian J. Hayes, Peter J. Robinson · 2009
Abstract. The teleo-reactive programming model is a high-level approach to im-plementing real-time control programs that react dynamically to changes in their environment. Teleo-reactive programs are particularly useful for implementing controllers in autonomous agents. In this paper we present formal techniques for reasoning about robust teleo-reactive programs. We develop a temporal logic over continuous intervals, which we use to formalise the semantics of teleo-reactive programs. To facilitate compositional reasoning about a program and its environ-ment, we use rely/guarantee style specications. We also present several theo-rems for simplifying proofs of teleo-reactive programs that control goal-directed agents. 1