Probabilistic temporal logic for motion planning with resource threshold constraints

Yoo, C; Fitch, R; Sukkarieh, S

Probabilistic temporal logic for motion planning with resource threshold constraints

Yoo, C

Fitch, R

Sukkarieh, S

Permalink

Publication Type:: Chapter
Citation:: 2013, 8 pp. 457 - 464
Issue Date:: 2013-01-01

Closed Access

	Filename	Description	Size
	p58.pdf	Published version	4.92 MB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Yoo, C https://orcid.org/0000-0002-2773-0527	en_US
dc.contributor.author	Fitch, R https://orcid.org/0000-0003-2215-5188	en_US
dc.contributor.author	Sukkarieh, S	en_US
dc.date.issued	2013-01-01	en_US
dc.identifier.citation	2013, 8 pp. 457 - 464	en_US
dc.identifier.isbn	9780262519687	en_US
dc.identifier.uri	http://hdl.handle.net/10453/121052
dc.description.abstract	© 2013 Massachusetts Institute of Technology. Temporal logic and model-checking are useful theoretical tools for specifying complex goals at the task level and formally verifying the performance of control policies. We are interested in tasks that involve constraints on real-valued energy resources. In particular, autonomous gliding aircraft gain energy in the form of altitude by exploiting wind currents and must maintain altitude within some range during motion planning. We propose an extension to probabilistic computation tree logic that expresses such real-valued resource threshold constraints, and present model-checking algorithms that evaluate a piecewise control policy with respect to a formal specification and hard or soft performance guarantees. We validate this approach through simulated examples of motion planning among obstacles for an autonomous thermal glider. Our results demonstrate probabilistic performance guarantees on the ability of the glider to complete its task, following a given piecewise control policy, without knowing the exact path of the glider in advance.	en_US
dc.rights	info:eu-repo/semantics/closedAccess
dc.title	Probabilistic temporal logic for motion planning with resource threshold constraints	en_US
dc.type	Chapter
utslib.citation.volume	8	en_US
utslib.for	080101 Adaptive Agents and Intelligent Robotics	en_US
utslib.for	091303 Autonomous Vehicles	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology/School of Mechanical and Mechatronic Engineering
pubs.organisational-group	/University of Technology Sydney/Strength - CAS - Centre for Autonomous Systems
utslib.copyright.status	closed_access	*
pubs.publication-status	Published	en_US
pubs.volume	8	en_US

Abstract:

© 2013 Massachusetts Institute of Technology. Temporal logic and model-checking are useful theoretical tools for specifying complex goals at the task level and formally verifying the performance of control policies. We are interested in tasks that involve constraints on real-valued energy resources. In particular, autonomous gliding aircraft gain energy in the form of altitude by exploiting wind currents and must maintain altitude within some range during motion planning. We propose an extension to probabilistic computation tree logic that expresses such real-valued resource threshold constraints, and present model-checking algorithms that evaluate a piecewise control policy with respect to a formal specification and hard or soft performance guarantees. We validate this approach through simulated examples of motion planning among obstacles for an autonomous thermal glider. Our results demonstrate probabilistic performance guarantees on the ability of the glider to complete its task, following a given piecewise control policy, without knowing the exact path of the glider in advance.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/121052