Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees
- 1 May 2010
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 3227-3232
- https://doi.org/10.1109/robot.2010.5509686
Abstract
We present a computational framework for automatic deployment of a robot from a temporal logic specification over a set of properties of interest satisfied at the regions of a partitioned environment. We assume that, during the motion of the robot in the environment, the current region can be precisely determined, while due to sensor and actuation noise, the outcome of a control action can only be predicted probabilistically. Under these assumptions, the deployment problem translates to generating a control strategy for a Markov Decision Process (MDP) from a temporal logic formula.We propose an algorithm inspired from probabilistic Computation Tree Logic (PCTL) model checking to find a control strategy that maximizes the probability of satisfying the specification. We illustrate our method with simulation and experimental results.Keywords
This publication has 11 references indexed in Scilit:
- Dealing with Nondeterminism in Symbolic ControlLecture Notes in Computer Science, 2008
- A Fully Automated Framework for Control of Linear Systems from Temporal Logic SpecificationsIEEE Transactions on Automatic Control, 2008
- Hybrid Controllers for Path Planning: A Temporal Logic ApproachPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2006
- Planning AlgorithmsPublished by Cambridge University Press (CUP) ,2006
- PRISM: A Tool for Automatic Verification of Probabilistic SystemsLecture Notes in Computer Science, 2006
- Probabilistic symbolic model checking with PRISM: a hybrid approachInternational Journal on Software Tools for Technology Transfer, 2004
- Multi-robot planning : a timed automata approachPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- Model-checking algorithms for continuous-time markov chainsIEEE Transactions on Software Engineering, 2003
- Speeding Up the Convergence of Value Iteration in Partially Observable Markov Decision ProcessesJournal of Artificial Intelligence Research, 2001
- The Complexity of Markov Decision ProcessesMathematics of Operations Research, 1987