This video shows the results of our paper titled "Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming". Given a mission captured by Linear Temporal Logic (LTL) along with the robots' dynamics, states, and inputs constraints, our tool synthesizes trajectories that are guaranteed to satisfy the mission. In this video, the mission is as follows:
1- INFINITELY OFTEN: each robot should visit its charging station (right top corner and bottom left corner).
2- EVENTUALLY ALWAYS: one robot must be patrolling the middle corridor
3- ALWAYS: avoid the obstacles and leave safety distance of 1 meter from each other

свернуть