www.prismmodelchecker.org
[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.
Links: [Google] [Google Scholar]

Publications