Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs

EasyChair Preprint 1491

Abstract

Teleo-Reactive(TR) robotic agent programs comprise sequences of guarded action rules clustered into named parameterised procedures. Their ancestry goes back to the first cognitive robot, Shakey. Like Shakey, a TR programmed robotic agent has a deductive Belief Store comprising constantly changing predicate logic percept facts, and knowledge facts and rules for querying the percepts. In this paper we introduce TR programming using a simple example expressed in the teleo-reactive programming language TeleoR, which is a syntactic extension of QuLog, a typed logic programming language used for the agent’s Belief Store. The example is sufficient to illustrate key properties that a TR and a TeleoR program should have. We give formal definitions of the key properties, and an informal operational semantics of the evaluation of a TeleoR procedure call. We then formally express the key properties in LTL. Finally we show how their LTL formalisation can be used to prove key properties of TeleoR procedures by using the example TeleoR program.

Keyphrases: Teleo-reactive programs, temporal logic, verification

@booklet{EasyChair:1491,
  author    = {Keith Clark and Brijesh Dongol and Peter Robinson},
  title     = {Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs},
  howpublished = {EasyChair Preprint 1491},
  year      = {EasyChair, 2019}}