文件名称：A Formal Model of a Multi-Robot Control and Communication Task
文件大小：153KB
文件格式：PDF
更新时间：2017-08-23 13:49:15
Robot Control
We introduce the Computation and Control Language (CCL), a guarded-command language for expressing systems wherein control and computation are inter- twined. A CCL program consists of a set of guarded commands that may update continuous or discrete vari- ables and that can be reasoned about using a simple temporal logic. In this paper, a detailed case study of a robot capture-the- ag system, called the \RoboFlag Drill", is encoded in CCL and certain properties of it are veried. The example consists of a self-stabilizing communications protocol whose behavior depends on the actions taken by the robots in their environment. The paper concludes with a brief overview of our initial implementation of the formal semantics of CCL as a practical programming language.