# Probabilistic Temporal Logic for Motion Planning with Resource Threshold Constraints

@inproceedings{Yoo2012ProbabilisticTL, title={Probabilistic Temporal Logic for Motion Planning with Resource Threshold Constraints}, author={Chanyeol Yoo and Robert C. Fitch and Salah Sukkarieh}, booktitle={Robotics: Science and Systems}, year={2012} }

Temporal logic and model-checking are useful theoretical tools for specifying complex goals at the task level and formally verifying the performance of control policies. We are interested in tasks that involve constraints on real-valued energy resources. In particular, autonomous gliding aircraft gain energy in the form of altitude by exploiting wind currents and must maintain altitude within some range during motion planning. We propose an extension to probabilistic computation tree logic that… Expand

#### 12 Citations

Provably-correct stochastic motion planning with safety constraints

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

Novel algorithms for model checking and policy synthesis in PCTL are proposed that provide a quantitative measure of safety and completion time for a given policy, and synthesise policies that minimise completion time with respect to a given safety threshold. Expand

2 . 2 Probabilistic Signal Temporal Logic Probabilistic Signal Temporal

- 2016

Guaranteeing safety is a key problem that needs to be addressed in order to enable the real-world deployment of robots and autonomous cyber-physical systems (CPS). While there is a lot of interest in… Expand

Language-Guided Sampling-based Planning using Temporal Relaxation

- Computer Science
- WAFR
- 2016

This paper proposes a sampling-based algorithm and an associated language-guided biasing scheme that leverage the notion of temporal relaxation of time-window temporal logic formulae (TWTL) to reformulate the temporal logic synthesis problem into an optimization problem. Expand

Online Task Planning and Control for Aerial Robots with Fuel Constraints in Winds

- Engineering, Computer Science
- WAFR
- 2014

This paper presents an algorithm for automatically synthesizing a continuous non-linear flight controller given a complex temporal logic task specification that can include contingency planning rules and presents simulation examples of navigation in a wind field and surveillance with fuel constraints. Expand

Stochastic Path Planning for Autonomous Underwater Gliders with Safety Constraints

- Computer Science
- 2019 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)
- 2019

A set of recursive equations for state probability and expected travel cost conditional on safety are derived and used to implement a new stochastic variant of FMT in the context of two types of objective functions that allow a glider to reach a destination region with minimum cost or maximum probability of arrival given a safety threshold. Expand

Preallocation and Planning Under Stochastic Resource Constraints

- Computer Science
- AAAI
- 2018

It is shown how to factorize resource limit uncertainty and use this to develop novel algorithms to plan policies for stochastic constraints, and it is shown that plans taking into account all potential realizations of the constraint obtain significantly better utility than planning for the expectation, while causing fewer constraint violations. Expand

Hierarchical Planning in Time-Dependent Flow Fields for Marine Robots

- Computer Science
- 2020 IEEE International Conference on Robotics and Automation (ICRA)
- 2020

Results show that the algorithm performs efficiently in practice and can find paths that adapt to changing ocean currents, which are significant to marine robotics because they allow for efficient use of time-varying ocean predictions for motion planning. Expand

Signal Temporal Logic Synthesis as Probabilistic Inference

- Computer Science
- ArXiv
- 2021

The notion of random STL~(RSTL), which extends deterministic STL with random predicates is introduced, which leads to a synthesis-as-inference approach and allows for differentiable, gradient-based synthesis while extending the class of possible uncertain semantics. Expand

Energy-optimal kinodynamic planning for underwater gliders in flow fields

- Computer Science
- 2017

This work presents an asymptotically optimal planning framework for underwater gliders that will enable improved navigation capability for both commercial and defence applications and shows that, when internal control mechanics are taken into account, energy-efficient paths do not necessarily follow a regular up-and-down pattern. Expand

Streamlines for Motion Planning in Underwater Currents

- Computer Science
- 2019 International Conference on Robotics and Automation (ICRA)
- 2019

An efficient method to compute reachability and cost between sample points in sampling-based motion planning that supports long-range planning over hundreds of kilometres in complicated flows is presented. Expand

#### References

SHOWING 1-10 OF 25 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

LTL Control in Uncertain Environments with Probabilistic Satisfaction Guarantees

- Mathematics, Computer Science
- ArXiv
- 2011

The problem of generating a control policy for a Markov Decision Process (MDP) such that the probability of satisfying an LTL formula over its states is maximized can be reduced to the problem of creating a robot control strategy that maximizes the probability to accomplish a task. Expand

Probabilistic Analysis of Correctness of High-Level Robot Behavior with Sensor Error

- Computer Science
- Robotics: Science and Systems
- 2011

This paper considers robot controllers that are synthesized from a set of highlevel, temporal logic task specifications, such that the resulting robot behavior is guaranteed to satisfy these specifications when assuming perfect sensors and actuators. Expand

Automatic Deployment of Robotic Teams

- Engineering
- IEEE Robotics & Automation Magazine
- 2011

A major goal in robot motion planning and control is to be able to specify a task in a high-level, expressive language and have the robot(s) to automatically convert the specification into a set of… Expand

An online algorithm for constrained POMDPs

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

This work proposes a new online algorithm that explicitly ensures constraint feasibility while remaining computationally tractable and demonstrates that the online algorithm generates policies comparable to an offline constrained POMDP algorithm. Expand

Motion Planning with Complex Goals

- Computer Science
- IEEE Robotics & Automation Magazine
- 2011

This article describes approach for solving motion planning problems for mobile robots involving temporal goals and a wide variety of techniques have been pro posed over the last two decades to solve such problems. Expand

Stochastic Model Checking

- Computer Science
- SFM
- 2007

This tutorial presents an overview of model checking for both discrete and continuous-time Markov chains (DTMCs and CTMCs) by outlining the main features supported by PRISM and three real-world case studies: a probabilistic security protocol, dynamic power management and a biological pathway. Expand

Symbolic planning and control of robot motion [Grand Challenges of Robotics]

- Computer Science
- IEEE Robotics & Automation Magazine
- 2007

The aim of symbolic control as is envisioned in this article is to enable the usage of methods of formal logic, languages, and automata theory for solving effectively complex planning problems for robots and teams of robots. Expand

Controlling Wild Bodies Using Linear Temporal Logic

- Computer Science
- 2012

This paper proposes a methodology that creates low-level hybrid controllers that guarantee that a group of bodies execute a high-level specified task without dynamical system modeling, precise state estimation or state feedback. Expand

Reduction methods for probabilistic model checking

- Computer Science
- 2008

A conservative extension of the classical conditions which makes the ample set method work for Markov decision processes with respect to lineartime properties is shown and the new stronger conditions are equivalent to the classical ones, if they are applied to non-probabilistic (classical) systems. Expand