Synthesis of an Asynchronous Communication Protocol for Search and Rescue Robots

We present a protocol for reliable communication between search and rescue robots, which is synthesized from a high-level temporal logic specification. The protocol ensures provably correct data transmission on an asynchronous point-to-point link in the presence of an adverse environment. We synthesize the protocol into correct-by-construction transceiver controllers that can be included as building blocks in a larger design. The viability of our approach of synthesizing controllers with clearly defined interfaces and the validity of our protocol is demonstrated by implementing controllers for robots searching cooperatively for a moving target.