Learning Linear Temporal Properties for Autonomous Robotic Systems

The problem of passive learning of linear temporal logic formulae consists in finding the best explanation for how two sets of execution traces differ, in the form of the shortest formula that separates the two sets. We approach the problem by implementing an exhaustive search algorithm optimized for execution speed. We apply it to the use-case of a robot moving in an unstructured environment as its battery discharges, both in simulation and in the real world. The results of our experiments confirm that our approach can learn temporal formulas explaining task failures in a case of practical interest.