Knowledge Representation and Automated Task Planning for Intelligent Robots through Spatial Temporal Logic and Learning

Intelligent robots have emerged as a hot research topic in the interdisciplinary study of control theory, robotics, and computer science as it demonstrates huge potential in fundamentally benefiting our society. The development of intelligent robots with the ability to independently solve a new task is an important yet challenging research problem. This work devotes to proposing an integrated system for such intelligent robots through three major objectives.

First, we propose a new spatial temporal logic with a sound and complete deduction system for knowledge representation and reasoning in intelligent robots. The proposed logic achieves a balance between expressiveness and tractability for intelligent robots since the satisfiability of the proposed logic is decidable. We propose two specification mining algorithms to generate spatial temporal logic formulas from video and unstructured text data. The obtained formulas are used to construct a domain theory storing necessary knowledge for task planning.

Second, we develop automatic task planning with an interactive proposer and verifier for intelligent robots based on the domain theory in spatial temporal logic. The proposer is used to generate ordered actions through forward graph expansion and backward solution extraction, and the verifier is used to verify the results from the proposer and generate executable task plans. We further study the scenario where the domain theory for task planning is incomplete by integrating the task planning algorithm with machine learning systems. The proposed framework gives intelligent robots the ability to actively seeking knowledge online based on missing information.

Third, we study a motion planning problem for intelligent robots under formal specifications of the proposed spatial temporal logic. We develop a control synthesis algorithm for the formal specifications by proposing a two-layer MPC framework. The high-layer transfers the global formal specifications into a sequence of sub-formulas and the low-layer solves a distributed MPC using an MILP solver. We show that the proposed framework is sound and recursively feasible.