**Contact Info**

Department of Applied Mathematics

University of Waterloo

Waterloo, Ontario

Canada N2L 3G1

Phone: 519-888-4567, ext. 32700

Fax: 519-746-4319

PDF files require Adobe Acrobat Reader

Friday, August 10, 2018 10:00 AM EDT

MC 5417

Luc Larocque | Applied Math, University of Waterloo

Kinodynamic Planning with mu-Calculus Specifications

Motion planning problems involve determining appropriate control inputs to guide a system towards a desired endpoint. Sampling-based motion planning was then developed as a technique for discretizing the state space of systems with complex environments. This makes the sampling-based method especially useful in robotics, where robots are expected to perform tasks in unknown, changing, or cluttered environments. On the other hand, temporal logic presents a means of prescribing the desired behaviour of a system. In the area of formal methods, researchers seek to solve problems in such a way that synthesized solutions provably satisfy a given temporal logic specification. In this thesis, we investigate combining the flexibility of sampling-based planning with the ability to specify the high-level behaviour of an autonomous system with the temporal logic known as mu-calculus.

While using temporal logic specifications with motion planning has been heavily researched, reliance on an available steering function is often impractical and suited only to basic problems with linear dynamics. This is because a steering function is a solution to an optimal two-point boundary value problem (OBVP); to our knowledge, it is nearly impossible to find an analytic solution to such problems in many cases. Addressing this issue, we have developed a means of using the motion planning algorithm SST* in combination with a local model checking procedure to solve kinodynamic planning problems with deterministic mu-calculus specifications without using a steering function. The procedure involves combining only the most pertinent information from multiple Kripke structures in order to create one abstracted Kripke structure storing the best paths to all possible proposition regions of the state-space. A linear-quadratic regulator (LQR) feedback control policy is then used to track these best paths, effectively connecting the trajectories found from multiple Kripke structures. Simulations demonstrate that it is possible to satisfy a complex liveness specification for infinitely often reaching specified regions of state-space using only forward propagation.

We proceed to repurpose this tool for real-time quadrotor motion planning with temporal logic specifications. The dynamical system is derived, and a real-time planning framework is presented based on a variant of the FMT* planning algorithm. Despite requiring a steering function, an argument is presented which allows finding OBVP solutions only for an approximation of the full dynamics. The notion of an abstracted Kripke structure is then applied in the context of quadrotor kinodynamic planning, allowing for rapid model checking and ensuring high-quality feasible solutions satisfying a given deterministic mu-calculus specification.

**Contact Info**

Department of Applied Mathematics

University of Waterloo

Waterloo, Ontario

Canada N2L 3G1

Phone: 519-888-4567, ext. 32700

Fax: 519-746-4319

PDF files require Adobe Acrobat Reader

University of Waterloo

University of Waterloo

43.471468

-80.544205

200 University Avenue West

Waterloo,
ON,
Canada
N2L 3G1

The University of Waterloo acknowledges that much of our work takes place on the traditional territory of the Neutral, Anishinaabeg and Haudenosaunee peoples. Our main campus is situated on the Haldimand Tract, the land granted to the Six Nations that includes six miles on each side of the Grand River. Our active work toward reconciliation takes place across our campuses through research, learning, teaching, and community building, and is co-ordinated within the Office of Indigenous Relations.