The coverage problem is relevant to numerous real-life applications such as agriculture, search and rescue, and demining. The primary objective of this problem is to cover as many positions as possible in an unknown environment. Utilizing multiple robots can significantly reduce the total time required for coverage while enhancing overall efficiency. In this paper, we introduce a novel Distributed Coverage Algorithm (DCA) utilizing multiple robots which is also scalable. This algorithm can be used in various real life situations like for agricultural field work, for search and rescue, etc. We formally prove termination, no overlap, correctness and time complexity of the DCA algorithm. We have simulated the DCA algorithm using the Webots multi-robot simulator and compared its performance with existing approaches. The simulation results reveal that the DCA algorithm significantly outperforms the existing approaches. DCA algorithm achieves a maximum coverage time reduction of 31.51% to 70.73% while also offering enhanced coverage efficiency in all environmental conditions.

Team formation in an environment where some relevant parameters are not known in advance is a challenging problem. Communicating automata and distributed algorithms have been used to describe protocols for team formation. A high-level specification provides a mathematical description of a protocol or a program. TLA + is a formal specification language designed to provide high-level specifications of concurrent and distributed systems. The associated model checker known as TLC is capable of model checking the TLA + specifications. Recently formal specification of a team formation protocol is given using TLA + when there is a single initiator (an agent or a robot), that initiates the team formation. Using TLA +, we examine the formal specification for the multiple initiator situation and demonstrate that a composition technique can yield a single monolithic specification for the multiple initiator situation from the single initiator situation specification. We have used models of varying sizes, and the TLC model checker has confirmed that the protocol’s specifications meet certain desired characteristics in each case.