Will the Robot Do the Right Thing?

ID
TR-92-31
Authors
Ying Zhang and Alan K. Mackworth
Publishing date
November 1992
Length
20 pages
Abstract
Constraint Nets have been developed as an algebraic on-line computational model of robotic systems. A robotic system consists of a robot and its environment. A robot consists of a plant and a controller. A constraint net is used to model the dynamics of each component and the complete system. The overall behavior of the system emerges from the coupling of each of its components. The question posed in the title is decomposed into two questions: first, what is the right thing? second, how does one guarantee the robot will do it? We answer these questions by establishing a formal approach to the specification and verification of robotic behaviors. In particular, we develop a real-time temporal logic for the specification of behaviors and a new verification method, based on timed forall-automata, for showing that the constraint net model of a robotic system satisfies the specification of a desired global behavior of the system. Since the constraint net model of the controller can also serve as the on-line controller of the real plant, this is a practical way of building well-behaved robots. Running examples of a coordinator for a two-handed robot performing an assembly task and a reactive maze traveler illustrate the approach.