Formal methods for controlling networked systems

Summary form only given. The goal in robot motion planning and control is to be able to specify a motion task in a rich, high level language and have the robot(s) automatically convert this specification into a set of low level primitives, such as feedback controllers and communication protocols, to accomplish the task. In most of the existing works, the motion planning problem is simply specified as "go from A to B while avoiding obstacles". However, there are many situations in which this is not enough to capture the nature of the task. Consider, for example, the miniature Robotic Urban-Like Environment (RULE) shown in Fig. 1, where a robot might be required to "Visit Road R1 or Road R2 without crossing Intersection I3, and then park in an available parking space," while at same time obeying the traffic rules. Such a "rich" specification cannot be trivially converted to a sequence of "go from A to B" primitives. When several robots are available, the problem becomes even more interesting and challenging. Assume that several service requests occur at different locations in the city, and they need to be serviced subject to some temporal and logical constraints. Some of these requests can be serviced by one (possibly specific) robot, while others require the collaboration of two or more (possibly specific) robots. For example, assume that the task is to first gather two pieces of data, one of which is available at P3 only, and the other at either P4 or P5, and and then fuse and transmit the data at one of the transmission locations P1 or P2. Assume that two robotic cars C1and C2 are available; only C1 can read the data at P4, and both cars are necessary to fuse and transmit the data. It has been recently advocated that temporal logics, such as Linear Temporal Logic (LTL) and Computation Tree Logic (CTL), can be used as "rich" specification languages in mobile robotics. Most existing works suggest that the corresponding formal verification (model checking) algorithms can be adapted for motion planning and controller synthesis from such specifications. Some related works show that such techniques can be extended to multi-agent systems through the use of parallel composition. However, such bottom-up approaches are expensive and can lead to state-space explosion even for relatively simple problems. As a result, one of the main challenges in the area of motion planning and control of distributed teams based on formal verification is to create provably-correct, top-down approaches in which a global, "rich" specification can be decomposed into local (individual) specifications, which can then be used to automatically synthesize robot control and communication strategies. In such a framework, the construction of the parallel composition of the individual motions is not necessary, and therefore the state-space explosion problem is avoided. In [1], we draw inspiration from the area of distributed formal synthesis to develop such a top-down approach. We consider a team of robots that can move among the regions of a partitioned environment, and which have known capabilities of servicing a set of requests that can occur in the regions of the partition. Some of these requests can be serviced by a robot individually, while some require the cooperation of groups of robots. We present an algorithm that allows for the fully automatic synthesis of robot control and communication strategies from a task specification given as a regular expression over the set of requests. For simplicity of presentation, we model the (partitioned) environment as a graph and the robots as agents that can move between adjacent vertices and can communicate only when at particular vertices. This framework is quite general and can be used in conjunction with cell decomposition motion planning techniques. In particular, by using feedback controllers for facet reachability in polytopes, this scenario can be extended to robots with continuous dynamics moving in environments