CaltechAUTHORS
  A Caltech Library Service

Evaluation and Benchmarking for Robot Motion Planning Problems Using TuLiP

Spooner, Nicholas (2012) Evaluation and Benchmarking for Robot Motion Planning Problems Using TuLiP. California Institute of Technology , Pasadena, CA. (Unpublished) http://resolver.caltech.edu/CaltechCDSTR:2012.007

[img]
Preview
PDF
See Usage Policy.

293Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCDSTR:2012.007

Abstract

Model checking is a technique commonly used in the verification of software and hardware. More recently, similar techniques have been employed to synthesize software that is correct by construction. TuLiP is a toolkit which interfaces with game solvers and model checkers to achieve this, producing a finite-state automaton representing a controller that satisfies the supplied specification. For motion planning in particular, a model checker may be employed in a deterministic scenario to produce a path satisfying a specification φ by checking against its negation ¬φ. If a counterexample is found, it will be a trace which satisfies φ. This was achieved in the TuLiP framework using the linear temporal logic (LTL) model checkers NuSMV and SPIN. A benchmark scenario based on a regular grid-world with obstacle and goal regions and reachability properties was devised, and extended to allow control of various complexity parameters, such as grid size, number of actors, specification type etc. Different measures of performance were explored, including CPU time, memory usage and path length, and the behavior of each checker with increasing problem complexity was analyzed using these metrics. The suitability of each checker for different classes and complexities of motion-planning problem was evaluated.


Item Type:Report or Paper (Technical Report)
Additional Information:With thanks to the Cambridge-Caltech Exchange (CamSURF) program, Lauren Stolper and Katherine Montgomery for their support, Caltech SFP for organizing the SURF program and the Caltech CDS group for accommodating me for the summer, in particular Necmiye Ozay, Ufuk Topcu, Pavithra Prabhakar and Richard Murray who gave excellent guidance and proofread this report. Thanks also to Mihai Florian for helping to resolve a stack-over flow problem in SPIN.
Group:Control and Dynamical Systems Technical Reports
Record Number:CaltechCDSTR:2012.007
Persistent URL:http://resolver.caltech.edu/CaltechCDSTR:2012.007
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:39299
Collection:CaltechCDSTR
Deposited By: Richard Murray
Deposited On:11 Jul 2013 22:26
Last Modified:11 Jul 2013 22:27

Repository Staff Only: item control page