Optimal Control of Markov Decision Processes with Temporal Logic Constraints
Xu Chu (Dennis) Ding, Stephen L. Smith, Calin Belta, and Daniela Rus
Hybrid and Networked Systems Laboratory, Boston University {xcding(at)bu.edu, cbelta(at)bu.edu}
Department of Electrical and Computer Engineering, University of Waterloo {stephen.smith@uwaterloo.ca}
Distributed Robotics Laboratory, Massachusetts Institute of Technology {rus@csail.mit.edu}
This toolbox automatically generates an optimal control policy for a Markov Decision Process (MDP) that maximizes the probability of satisfying a Linear Temporal Logic (LTL) formula and minimize the expected cost in between satisfaction of a given proposition.
For more detail of the algorithm that produces the policy, please see [1]. This software calls open source software [2] and [3].
Requirements
– Mac OS X 10.6, Linux and Windows (Linux and Windows should work, but let me know if there is any issue)
– MATLAB 2010b or later with Bioinformatics toolbox (for SCC computation)
Download
How to use
Download the software package: Optimal_Control-LTL package and run ACPCLTL.m
References
[1] Xu Chu (Dennis) Ding, Stephen L. Smith, Calin Belta, and Daniela. “Optimal Control of Markov Decision Processes with Temporal Logic Constraints”, submitted to Transactions on Automatic Control.
[2] “LTL2DSTAR”, http://www.ltl2dstar.de/.
[3] “LTL2BA,” http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php.
