# LTL Control in Uncertain Environments with Probabilistic Satisfaction Guarantees

@article{Ding2011LTLCI, title={LTL Control in Uncertain Environments with Probabilistic Satisfaction Guarantees}, author={Xu Chu Ding and Stephen L. Smith and Calin A. Belta and Daniela Rus}, journal={ArXiv}, year={2011}, volume={abs/1104.1159} }

We present a method to generate a robot control strategy that maximizes the probability to accomplish a task. The task is given as a Linear Temporal Logic (LTL) formula over a set of properties that can be satisfied at the regions of a partitioned environment. We assume that the probabilities with which the properties are satisfied at the regions are known, and the robot can determine the truth value of a proposition only at the current region. Motivated by several results on partitioned-based… Expand

#### Figures and Topics from this paper

#### 78 Citations

MDP Optimal Control under Temporal Logic Constraints-Technical Report -

- 2011

In this paper, we develop a method to automatically generate a control policy for a dynamical system modeled as a Markov Decision Process (MDP). The control specification is given as a Linear… Expand

MDP optimal control under temporal logic constraints

- Computer Science, Mathematics
- IEEE Conference on Decision and Control and European Control Conference
- 2011

A sufficient condition for a policy to be optimal is proposed, and a dynamic programming algorithm is developed that synthesizes a policy that is optimal under some conditions, and sub-optimal otherwise. Expand

Multi-agent persistent monitoring in stochastic environments with temporal logic constraints

- Computer Science
- 2012 IEEE 51st IEEE Conference on Decision and Control (CDC)
- 2012

An approximate dynamic programming framework that chooses a set of basis functions to approximate the optimal cost and finds the best parameters for these functions based on the least-square approximation and develops an approximate policy iteration algorithm to implement this framework. Expand

Optimal Control of Markov Decision Processes With Linear Temporal Logic Constraints

- Mathematics, Computer Science
- IEEE Transactions on Automatic Control
- 2014

A sufficient condition for a policy to be optimal is proposed, and a dynamic programming algorithm is developed that synthesizes a policy that is optimal for a set of LTL specifications. Expand

Temporal logic motion control using actor-critic methods

- Computer Science
- ICRA
- 2012

An approximate dynamic programming framework based on a least-square temporal difference learning method of the actor-critic type that operates on sample paths of the robot and optimizes a randomized control policy with respect to a small set of parameters. Expand

Optimal path planning for surveillance with temporal-logic constraints*

- Computer Science
- Int. J. Robotics Res.
- 2011

This paper utilizes Büchi automata to produce an automaton (which can be thought of as a graph) whose runs satisfy the temporal-logic specification, and presents a graph algorithm that computes a run corresponding to the optimal robot path. Expand

Optimal Control of Markov Decision Processes with Temporal Logic Constraints

- 2012

In this paper, we develop a method to automatically generate a control policy for a dynamical system modeled as a Markov Decision Process (MDP). The control specification is given as a Linear… Expand

Temporal logic robot control based on automata learning of environmental dynamics

- Computer Science
- Int. J. Robotics Res.
- 2013

A technique to automatically generate a control policy for a robot moving in an environment that includes elements with unknown, randomly changing behavior, and it is shown that the obtained control policy converges to an optimal one when the partially unknown behavior patterns are fully learned. Expand

Temporal logic motion control using actor–critic methods

- Computer Science, Mathematics
- 2012 IEEE International Conference on Robotics and Automation
- 2012

An approximate dynamic programming framework based on a least-squares temporal difference learning method of the actor–critic type is proposed that operates on sample paths of the robot and optimizes a randomized control policy with respect to a small set of parameters. Expand

LTL-Based Planning in Environments With Probabilistic Observations

- Computer Science
- IEEE Transactions on Automation Science and Engineering
- 2015

This research proposes a centralized method for planning and monitoring the motion of one or a few mobile robots in an environment where regions of interest appear and disappear based on exponential… Expand

#### References

SHOWING 1-10 OF 32 REFERENCES

Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees

- Computer Science
- 2010 IEEE International Conference on Robotics and Automation
- 2010

An algorithm inspired from probabilistic Computation Tree Logic (PCTL) model checking to find a control strategy that maximizes the probability of satisfying the specification is proposed. Expand

Where's Waldo? Sensor-Based Temporal Logic Motion Planning

- Engineering, Computer Science
- Proceedings 2007 IEEE International Conference on Robotics and Automation
- 2007

This paper provides a framework for automatically and verifiably composing controllers that satisfy high level task specifications expressed in suitable temporal logics that can express complex robot behaviors such as search and rescue, coverage, and collision avoidance. Expand

A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications

- Mathematics, Computer Science
- IEEE Transactions on Automatic Control
- 2008

The solution to the problem of finding a feedback control law with polyhedral bounds and a set of initial states so that all trajectories of the closed loop system satisfy the formula consists of three main steps. Expand

Receding horizon temporal logic planning for dynamical systems

- Computer Science
- Proceedings of the 48h IEEE Conference on Decision and Control (CDC) held jointly with 2009 28th Chinese Control Conference
- 2009

To address the computational difficulties in the synthesis of a discrete planner, this paper presents a receding horizon based scheme for executing finite state automata that essentially reduces the synthesis problem to a set of smaller problems. Expand

Controller Synthesis for Probabilistic Systems

- Computer Science
- IFIP TCS
- 2004

A model with probabilism and nondeterminism where the nondeterministic choices in some states are assumed to be controllable, while the others are under the control of an unpredictable environment is considered. Expand

Sampling-based motion planning with deterministic μ-calculus specifications

- Mathematics, Computer Science
- Proceedings of the 48h IEEE Conference on Decision and Control (CDC) held jointly with 2009 28th Chinese Control Conference
- 2009

Algorithms for the on-line computation of control programs for dynamical systems that provably satisfy a class of temporal logic specifications are proposed, generalizing state-of-the-art algorithms for point-to-point motion planning. Expand

High-level robot behavior control using POMDPs

- Computer Science
- 2002

A hierarchical variant of the POMDP model is presented which exploits structure in the problem domain to accelerate planning and successfully demonstrated that it could autonomously provide guidance and information to elderly residents with mild physical and cognitive disabilities. Expand

Automatic synthesis of multi-agent motion tasks based on LTL specifications

- Computer Science
- 2004 43rd IEEE Conference on Decision and Control (CDC) (IEEE Cat. No.04CH37601)
- 2004

A methodology for automatically synthesizing motion task controllers based on linear temporal logic (LTL) specifications that combines the continuous dynamics of the underlying system with the automatically synthesized switching logic that enforces the LTL specification. Expand

Bisimilar linear systems

- Mathematics, Computer Science
- Autom.
- 2003

It is shown that computing the coarsest bisimulation, which results in maximum complexity reduction, corresponds to computing the maximal controlled or reachability invariant subspace inside the kernel of the observations map. Expand

Probabilistic symbolic model checking with PRISM: a hybrid approach

- Computer Science
- International Journal on Software Tools for Technology Transfer
- 2004

A novel hybrid technique which combines aspects of symbolic and explicit approaches to overcome performance problems in probabilistic model checking, and achieves a dramatic improvement over the purely symbolic approach. Expand