How can we interact with physical systems, in particular robots, at a high level? How can we formalize high-level goals in a user-friendly way? How can we automatically create controllers for such systems and how can we guarantee these systems will behave correctly?