SMC-LTL: SMC-based LTL Multi-Robot Motion Planner

Satisﬁability Modulo Convex programming (SMC)-based Linear Temporal Logic (LTL) Multi-Robot Motion Planner.

See Wiki for instructions and the following papers for technical details:

Yasser Shoukry, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, and Paulo Tabuada, “SMC: Satisﬁability Modulo Convex programming,” Proceedings of the IEEE, vol. 106, no. 9, pp. 1655-1679, September 2018.
Yasser Shoukry, Pierluigi Nuzzo, Indranil Saha, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, and Paulo Tabuada, "Scalable lazy SMT-based motion planning," in Proceedings of the 55th IEEE Conference on Decision and Control (IEEE CDC), Las Vegas, NV, December 2016, pp. 6683-6688.
Yasser Shoukry, Pierluigi Nuzzo, Ayca Balkan, Indranil Saha, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, and Paulo Tabuada, "Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming," in Proceedings of the 56th IEEE Conference on Decision and Control (IEEE CDC), Melbourne, Australia, December 2017, pp. 1132-1137.

Simulations and experiments showing the performance of the SMC-LTL motion planner can be found here: https://www.youtube.com/watch?v=4vybbqXsPaM

License

The code is released under MIT License.