# Time window temporal logic

@article{Vasile2017TimeWT, title={Time window temporal logic}, author={Cristian Ioan Vasile and Derya Aksaray and Calin A. Belta}, journal={Theor. Comput. Sci.}, year={2017}, volume={691}, pages={27-54} }

This paper introduces time window temporal logic (TWTL), a rich expressivity language for describing various time bounded specifications. In particular, the syntax and semantics of TWTL enable the compact representation of serial tasks, which are typically seen in robotics and control applications. This paper also discusses the relaxation of TWTL formulae with respect to deadlines of tasks. Efficient automata-based frameworks to solve synthesis, verification and learning problems are also… Expand

#### 22 Citations

Automata-based Optimal Planning with Relaxed Specifications

- Computer Science
- ArXiv
- 2021

An automata-based framework for planning with relaxed specifications is introduced and a three-way product automaton construction method is proposed that allows us to compute minimal relaxation policies for the robots using standard shortest path algorithms. 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

Metrics for Signal Temporal Logic Formulae

- Computer Science
- 2018 IEEE Conference on Decision and Control (CDC)
- 2018

This paper shows that under mild assumptions, STL formulae admit a metric space, and proposes two metrics over this space based on i) the Pompeiu-Hausdorff distance and ii) the symmetric difference measure and presents algorithms to compute them. Expand

Continuous-time Signal Temporal Logic Planning with Control Barrier Functions

- Computer Science, Mathematics
- 2020 American Control Conference (ACC)
- 2020

An offline trajectory planner for linear cyber-physical systems with continuous dynamics, where controls are generated by digital computers in discrete time is proposed, based on a Mixed Integer Quadratic Programming (MIQP) formulation that utilizes CBFs to produce system trajectories that are valid in continuous time. Expand

Online Motion Planning with Soft Timed Temporal Logic in Dynamic and Unknown Environment

- Computer Science, Mathematics
- ArXiv
- 2021

This work proposes a control framework that considers hard constraints to enforce safety requirements and soft constraints to enable task relaxation, and employs the metric interval temporal logic specifications to deal with time constraints. Expand

Multi-robot routing and scheduling with temporal logic and synchronization constraints

- Computer Science
- 2019

Inspiring by model checking techniques, this work develops a solution able to satisfy both demands and synchronization rules of a fleet of robots involved in semiconductor manufacturing. Expand

Decentralized Safe Reactive Planning under TWTL Specifications

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

This work proposes a decentralized receding horizon algorithm for online planning of trajectories and shows that when the environment is sufficiently connected, the resulting agent trajectories are always safe (collision-free) and lead to the satisfaction of the TWTL specifications or their finite temporal relaxations. Expand

Sampling-based synthesis of maximally-satisfying controllers for temporal logic specifications

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

This work presents an incremental sampling-based algorithm that synthesizes a motion control policy satisfying a bounded Signal Temporal Logic formula over properties of a given environment using a quantitative measure of how well the best path in the current tree of samples satisfies the specification. Expand

Specifying User Preferences Using Weighted Signal Temporal Logic

- Computer Science, Engineering
- IEEE Control Systems Letters
- 2021

WSTL robustness can be defined as weighted generalizations of all known compatible robustness functionals that can take into account the weights in wSTL formulae, and is employed in an optimization framework to synthesize controllers that maximize satisfaction of a specification with user specified preferences. Expand

Probabilistically Guaranteed Satisfaction of Temporal Logic Constraints During Reinforcement Learning

- Computer Science, Engineering
- ArXiv
- 2021

An automata-theoretic approach is proposed to ensure probabilistic satisfaction of the constraint in each episode, which is different from penalizing violations to achieve constraint satisfaction after a sufficiently large number of episodes. Expand

#### References

SHOWING 1-10 OF 75 REFERENCES

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

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

Verification of concurrent programs, Part I: The temporal framework

- Computer Science
- 1981

The temporal formalism is introduced as a tool for reasoning about sequences of states and the set of interesting properties is classified into invariance (safety), eventuality (liveness, and precedence) properties. Expand

Querying Parametric Temporal Logic Properties on Embedded Systems

- Computer Science
- ICTSS
- 2012

This paper considers parametric specifications in Metric Temporal Logic (MTL), and using robust semantics for MTL, the parameter estimation problem can be converted into an optimization problem which can be solved by utilizing stochastic optimization methods. Expand

Specifying real-time properties with metric temporal logic

- Computer Science
- Real-Time Systems
- 2005

This paper characterize real-time systems by giving a classification of such quantitative temporal properties, and extends the usual models for temporal logic by including a distance function to measure time and analyzes what restrictions should be imposed on such a function. Expand

A Theory of Timed Automata

- Computer Science
- Theor. Comput. Sci.
- 1994

The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton, and it is proved that the universality problem and the language inclusion problem are solvable only for the deterministic automata. Expand

Receding horizon control for temporal logic specifications

- Mathematics, Computer Science
- HSCC '10
- 2010

A receding horizon framework that satisfies a class of linear temporal logic specifications sufficient to describe a wide range of properties including safety, stability, progress, obligation, response and guarantee is described. Expand

On the minimal revision problem of specification automata

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

This paper establishes that the latter problem, which is referred to as the minimal specification revision problem, is NP-complete and a heuristic algorithm is presented that can compute good approximations to the Minimal Revision Problem (MRP) in polynomial time. Expand

Temporal logic motion planning for dynamic robots

- Mathematics, Computer Science
- Autom.
- 2009

This paper designs a control law that enables the dynamic model to track a simpler kinematic model with a globally bounded error and builds a robust temporal logic specification that takes into account the tracking errors of the first step. Expand

Efficient Model Checking of Safety Properties

- Computer Science
- SPIN
- 2003

An algorithm for constructing finite automata recognising informative prefixes of LTL formulas based on [1] is presented and results indicate that the translation is competitive when compared to model checking with tools translating full LTL to Buchi automata. Expand