Towards reasoning about teleo-reactive programs for robust real-time systems

Abstract

The teleo-reactive programming approach was developed by Nilsson for application in domains like robotics. It has a high-level programming model that allows real-time control programs to be written in a manner that allows them to react robustly to changes in the environment. In this paper we give a formalisation of the semantics of teleo-reactive programs and provide rely/guarantee rules for reasoning about them. The semantics are given in a form that partitions the behaviour of the system into its behaviour over a sequence of time intervals.