In this paper we present a procedure to automatically design and verify the local behavior of robots with highly limited cognition. All robots are: anonymous, homogeneous, non-communicating, memoryless, reactive, do not know their global position, do not have global state information, and operate by a local clock. They only know: (1) the relative location of their neighbors within a short range and (2) a common direction (North). We have developed a procedure to generate a local behavior that allows the robots to self-organize into a desired global pattern despite their individual limitations. This is done while also avoiding collisions and keeping the coherence of the swarm at all times. The generated local behavior is a probabilistic local state-action map. The robots follow this stochastic policy to select an action based on their current perception of their neighborhood (i.e., their local state). It is this stochasticity, in fact, that allows the global pattern to eventually emerge. For a generated local behavior, we present a formal proof procedure to verify whether the desired pattern will always eventually emerge from the local actions of the agents. The novelty of the proof procedure is that it is primarily local in nature and focuses on the local states of the robots and the global implications of their local actions. A local approach is of interest to reduce the computational effort as much as possible when verifying the emergence of larger patterns. Finally, we show how the behavior could be implemented on real robots and investigate this with extensive simulations on a realistic robot model. To the best of our knowledge, no other solutions exist for robots with such limited cognition to achieve this level of coordination with proof that the desired global property will emerge.

The autonomous maneuverable space net, which consists of a flexible net and several maneuverable units, is a promising solution for the active removal of space debris. A novel dynamics model and a corresponding controller are proposed in this paper to resolve the approach control problem. Given that the net tethers cannot be elongated, interval functions and corresponding constraint forces are exploited to model the unilaterally constrained tethers. The proposed approach dynamics model, which is based on the Hamilton principle, includes distinctive velocity jump phenomena. A dual-loop control scheme with double optimization pseudo-dynamics inversion and sliding mode control is also established. Simulation results validate the feasibility of the proposed control scheme. The net can fly along the expected trajectory without suffering unexpected net deformation or orbital radial movement.