Control design for hybrid systems with TuLiP: The temporal logic planning toolbox

I. Filippidis, S. Dathathri, S. C. Livingston, N. Ozay and R. M. Murray
Proc. Multi-conference on Systems and Control (MSC) 2016.

This is a tutorial paper on TuLiP (tulip-control.org) that explains some of the underlying theory on game solving, BDDs, abstraction. It not only talks about some problems you can solve with TuLiP but also about some data structures available in TuLiP that can be used to develop new verification, synthesis or abstraction algorithms. It also points to some subtleties that could be of interest to experts. We took an “experimental” approach in exposition and tried to formalize some of the problems using TLA+.

Preprint