[JKG13]Benjamin Johnson and Hadas Kress-Gazit.Analyzing and revising high-level robot behaviors under actuator error.In Proc. 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'13), pages 741-748.2013.
Notes:
Uses probabilistic model checking and PRISM for the synthesis of verifiable robot controllers.