An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms

An environment for specifying and model checking mobile robot algorithms on rings (or mobile ring robot algorithms) is proposed. We have developed the Maude Ring Specification Enviaude RSE), a specification environment that explicitly supports ring-shaped networks. Maude RSE is implemented on top of Maude, a rewriting logic-based specification language. The underlying key behind the tool is pattern matching between ring patterns and ring instances, called "ring pattern matching." Because rings are not commonly available data structures in any existing specification language, we encode ring patterns as sets of sequence patterns and simulate ring pattern matching by pattern matching between sets of sequence patterns and sequence instances, which is proven correct and transparent to Maude RSE users. The advantages of Maude RSE are demonstrated by case studies analyzing exploration and gathering algorithms.