  An autonomous navigation with proven collision avoidance in unknown and
dynamic environments is still a challenge, particularly when there are moving
obstacles. A popular approach to collision avoidance in the face of moving
obstacles is based on model predictive algorithms, which, however, may be
computationally expensive. Hence, we adopt a reactive potential field approach
here. At every cycle, the proposed approach requires only current robot states
relative to the closest obstacle point to find the potential field in the
current position; thus, it is more computationally efficient and more suitable
to scale up for multiple agent scenarios. Our main contribution here is to
write the reactive potential field based motion controller as a hybrid
automaton, and then formally verify its safety using differential dynamic
logic. In particular, we can guarantee a passive safety property, which means
that collisions cannot occur if the robot is to blame, namely a collision can
occur only if the robot is at rest. The proposed controller and verification
results are demonstrated via simulations and implementation on a Pioneer P3-AT
robot.
