This is part of a joint project between the Planning and Diagnosis group at ANU & NICTA, and the Model-Based Embedded Robotics Systems group at MIT. We are interested in automated planning and execution for autonomous systems such as autonomous air vehicles, Mars rovers, and energy management systems to cite but a few. Because the environment is uncertain, robust plans for such systems will never be a simple sequence of fixed instructions -- there will always be an element of dynamism, with some decisions deferred to the on-line plan execution phase. Moreover, In almost any realistic environment, constraints cannot be guaranteed with certainty, and no goals can be achieved without taking some risk. To allow for this, we consider chance constraints: constraints that are satisfied with (at least) a given probability Î¸, based on a probabilistic model of environment uncertainties. This class of problems can be modelled as chance-constrained Markov decision processes (cc-MDPs). These are expressive probabilistic models for optimal planning and decision-making under uncertainty, subject to chance constraints on the evolution of the controlled environment. A solution for a cc-MDP is a policy mapping the history of states of the environment to the action to be taken by the autonomous system at execution, and which guarantees that the execution risk is bounded as specified by the chance constraints.
Whilst cc-MDPs are the right model for our problem, policy generation algorithms for cc-MDPs are still in their infancy and lack efficiency and generality. In this project, you will design and implement efficient algorithms cc-MDPs, for which the chance constraints are specified in a probabilistic temporal logic like pCTL, pLTL, or pCTL*. This will require combining model-checking algorithms for these logics with new algorithms for MDPs. You will also apply these algorithms to significant case studies in robotics or energy systems (see videos below).
This project is best suited to a strong student with a computer science or software engineering background, with a keen interest in artificial intelligence, logic, and algorithms, and good programming skills.
(None of this is required reading before commencing the project) Books on Markov decision processes in AI: Planning with Markov Decision Processes: An AI Perspective Mausam and Andrey Kolobov, Morgan Claypool, 2013. Available free from your institutional virtual library (e.g virtual.anu.edu.au) http://www.morganclaypool.com/doi/pdf/10.2200/S00426ED1V01Y201206AIM017 Olivier Sigaud and Olivier Buffet (eds). Markov Processes in Artificial Intelligence, Wiley-ISTE, 2010. http://au.wiley.com/WileyCDA/WileyTitle/productCd-1848211678.html Papers on model-checking and controler synthesis for probabilistic temporal logics: M. Kwiatkowska and D. Parker. Automated Verification and Strategy Synthesis for Probabilistic Systems. In Proc. 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), volume 8172 of LNCS, pages 5-22, Springer. October 2013. http://qav.comlab.ox.ac.uk/bibitem.php?key=KP13 M. Kwiatkowska, G. Norman and D. Parker. Stochastic Model Checking. In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of Lecture Notes in Computer Science (Tutorial Volume), pages 220-270, Springer. June 2007. http://qav.comlab.ox.ac.uk/bibitem.php?key=KNP07a Papers on chance constrained MDPs: Florent Teichteil-KÃ¶nigsbuch: Path-Constrained Markov Decision Processes: bridging the gap between probabilistic model-checking and decision-theoretic planning. ECAI 2012: 744-749 http://dx.doi.org/10.3233/978-1-61499-098-7-744 Jonathan Sprauel, Andrey Kolobov, Florent Teichteil-KÃ¶nigsbuch: Saturated Path-Constrained MDP: Planning under Uncertainty and Deterministic Model-Checking Constraints. AAAI 2014: 2367-2373 http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8533
The student will gain a solid, world class grounding in sequential decision making, AI planning, and model-checking for probabilistic temporal logics. This topic is ideal for a honours student interested in pursuing a PhD in artificial intelligence, formal methods, or cognitive robotics, or to a PhD student in one of these areas. Moreover, the student would have the possibility of interacting with partners at MIT.