Search papers, labs, and topics across Lattice.
This paper introduces a new temporal logic, Logic of Fuzzy Paths (LFP), designed for motion planning that treats paths as first-class citizens, separating geometric and logical concerns. LFP builds upon Signal Temporal Logic (STL) but uses fuzzy, time-varying signal constraints to achieve simpler, more understandable formulae and a refined notion of satisfaction. The authors demonstrate LFP's usability for both human-specified verification and learning specifications from demonstrations in motion planning, showcasing its versatility and flexibility across various scenarios.
Separating geometry from logic with fuzzy path constraints yields motion planning specifications that are both more intuitive for humans and more amenable to learning from demonstrations.
We introduce a new family of temporal logics intended for specifications in motion planning (MP). It builds upon the signal temporal logic (STL), which is a linear-time logic over real-valued signals that possess quantitative semantics and thus became popular in the areas of cyber-physical systems, robotics, and specifically robot MP. However, in contrast to STL, the proposed logic works with paths as first-class citizens, separating the concerns of geometry and of logic. This in turn leads to simpler and more understandable formulae, and a more refined notion of satisfaction being able to reflect also preferences over behaviours. Technically, the logic is built on fuzzy, time-varying signal constraints. As a consequence of this expressivity, it is (i) more usable for human-given specifications in MP and (ii) more amenable to learning specifications from demonstrations than other logics. The former is important for the traditional style of verification in robot MP; the latter is becoming recognized as crucial for mining data-given tasks and controller synthesis in human-aware MP. We expose the advantages of our proposed logic on examples and show the versatility and flexibility of the framework on a number of scenarios. Finally, we give a learning algorithm with a prototype implementation and discuss the possibilities of model checking and monitoring.
