Show simple item record

dc.contributor.authorLarocque, Luc
dc.date.accessioned2018-09-19 15:20:44 (GMT)
dc.date.available2018-09-19 15:20:44 (GMT)
dc.date.issued2018-09-19
dc.date.submitted2018-09-11
dc.identifier.urihttp://hdl.handle.net/10012/13818
dc.description.abstractMotion planning problems involve determining appropriate control inputs to guide a system towards a desired endpoint. Sampling-based motion planning was 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); thus far, mathematicians have yet to find analytic solutions to such problems in all but the simplest of 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 involving infinitely often reaching specified regions of state-space using only forward propagation of the system dynamics. 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.en
dc.language.isoenen
dc.publisherUniversity of Waterlooen
dc.subjectsamplingen
dc.subjectmotion planningen
dc.subjectkinodynamicen
dc.subjectmu-calculusen
dc.subjecttemporal logicen
dc.subjectquadrotoren
dc.subjectsteeringen
dc.subjectSSTen
dc.subjectFMTen
dc.subjectroboticsen
dc.subjectplanningen
dc.titleKinodynamic Planning with μ-Calculus Specificationsen
dc.typeMaster Thesisen
dc.pendingfalse
uws-etd.degree.departmentApplied Mathematicsen
uws-etd.degree.disciplineApplied Mathematicsen
uws-etd.degree.grantorUniversity of Waterlooen
uws-etd.degreeMaster of Mathematicsen
uws.contributor.advisorLiu, Jun
uws.contributor.affiliation1Faculty of Mathematicsen
uws.published.cityWaterlooen
uws.published.countryCanadaen
uws.published.provinceOntarioen
uws.typeOfResourceTexten
uws.peerReviewStatusUnrevieweden
uws.scholarLevelGraduateen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record


UWSpace

University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages