Title:Towards an LTL Semantics for Teleo-Reactive Programs for Robotic Agents
Date: November 22, 2018 (Thursday)
Time: 3:00 pm - 4:00 pm
Venue: Room 121, 1/F, Ho Sin-hang Engineering Building, The Chinese University of Hong Kong, Shatin, N.T.
Speaker: Prof. Keith L. Clark
Emeritus Professor
Imperial College London


A TR Program comprises a set of parameterised procedures each of which comprises a sequence of guarded action rules of the form:  G ~> A   Here G is a deductive query to the agent's dynamic Belief Store (BS) of percept and told facts, ,and A is a tuple of robotic actions or a TR proc. call, including a recursive call. Some or all of the robotic actions may be durative - continuing until stopped. The purpose of some proc call C is to be bring about a state of the robotic environment which can be recognised as having been achieved by a successful evaluation of the guard of the procedure's C partially instantiate first rule. The guards of later rules represent detectable sub-goal states. When C is called its guards are (optimistically) tested in before/after order until one is found with a guard query that succeeds, typically further instantiating the rule’s action. This rule instance is fired and its action started. It continues whilst the rule’s instantiated guard query continues to be inferable, no earlier guard instance becomes inferable, and the procedure call action remains active. The purpose of the continuing execution of the action is to bring about a detectable super-goal of the rule’s guard, and to eventually achieve the guard of the first rule. This is the procedure’s regression property. In this informal talk a small example use of TR language will be given, and the rule firing and regression semantics precisely but informally defined. However, the use of words such as “eventually” suggests that the semantics of a particular TR procedure may be expressible in Linear Temporal Logic. Preliminary ideas of how this may be done will be given for which constructive criticism is welcome. The long term goal is to be able to use an LTL specification of the behaviour of primitive robotic actions, and of existing TR procedures, to systematically derive the sequence of rules of a new TR procedure given its LTL specification.



Keith Clark has Bachelor degrees in both maths and philosophy and a PhD in Computational Logic. He is one of the founders of Logic Programming.  His early research was primarily in the theory and practice of LP. His paper: “Negation as Failure” (1978), giving a semantics to Prolog’s negation operator, has over 3000 citations.  

In 1981, inspired by Hoare’s CSP, with a PhD student Steve Gregory, he introduced the concepts of committed choice non-determinism and stream communicating and-parallel sub-proofs into logic programming.   This restriction of the LP concept was then adopted by the Japanese Fifth Generation Project.  This had the goal of building multi-processor knowledge using computers. Unfortunately, the restrictions men it is not a natural tool for building KP applications, and the FGP project failed.  Since 1990 his research emphasis has been on the design, implementation and application of multi-threaded rule based programming languages, with a strong declarative component, for multi-agent and cognitive robotic applications.

He has had visiting positions at Stanford University, UC Santa Cruz, Syracuse University and Uppsala University amongst others. He is currently an Emeritus Professor at Imperial, and an Honorary Professor at University of Queensland and the University of New Soul Wales.  He has consulted for the Japanese Fifth Generation Project, Hewlett Packard, IBM,  Fujitsu and two start-ups. With colleague Frank McCabe, he foundedthe company Logic Programming Associates in 1980. This produced and marketed Prolog systems for micro-computers, offering training and consultancy on their use. The star product was MacProlog,  with primitives for exploiting the Mac GUI for AI applications.


Enquiries: Ms. Crystal Tam at tel. 3943 8439

For more information, please refer to http://www.cse.cuhk.edu.hk/en/events