Robotics: Science and Systems VIII

Probabilistic Temporal Logic for Motion Planning with Resource Threshold Constraints

Chanyeol Yoo, Robert Fitch, Salah Sukkarieh


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.



    AUTHOR    = {Chanyeol Yoo AND Robert Fitch AND Salah Sukkarieh}, 
    TITLE     = {Probabilistic Temporal Logic for Motion Planning with Resource Threshold Constraints}, 
    BOOKTITLE = {Proceedings of Robotics: Science and Systems}, 
    YEAR      = {2012}, 
    ADDRESS   = {Sydney, Australia}, 
    MONTH     = {July},
    DOI       = {10.15607/RSS.2012.VIII.058}