A computation and control language for multi-vehicle systems

We introduce the Computation and Control Language (CCL), a guarded-command formalism for expressing systems wherein control and computation are intertwined. A CCL program consists of a set of guarded commands that update continuous or discrete variables. CCL programs are used to specify systems and program them. Their properties can be analyzed using temporal logic. In this paper, a robot capture-the-flag system, called the "RoboFlag Drill", is encoded in CCL and certain desirable properties of it are verified. 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.