Synthesis for Robotics
We consider two types of synthesis. The first is reactive synthesis, where the system (robot) and environment (human) choose their actions. We formulate this as a game where the robot and human play against each other. This provides strong guarantees, as the robot must deal with worst-case human behaviors. On the other hand, the worst-case is frequently too pessimistic. Efficient Symbolic Reactive Synthesis for Finite-Horizon Tasks
In the second type, we consider probabilistic synthesis. Here the system (robot) makes choices while the environment (human) is stochastic. This allows us to deal with expected-case behaviors, but leads to challenges modeling the human. LTLf Synthesis on Probabilistic Systems
We present probabilistic synthesis for robotic manipulation domains on Probabilistic Manipulation with LTLf The key improvement compared to reactive synthesis is the ability to deal with the expected case rather than being limited to the worst case. This can enable more efficient human-robot collaboration.