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)

See Usage Policy.


Use this Persistent URL to link to this item:


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:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:39299
Deposited By: Richard Murray
Deposited On:11 Jul 2013 22:26
Last Modified:03 Oct 2019 05:05

Repository Staff Only: item control page