Functional gradient descent method for Metric Temporal Logic specifications

Houssam Abbas, Andrew Winn, Georgios Fainekos, A. Agung Julius

Research output: Chapter in Book/Report/Conference proceedingConference contribution

27 Scopus citations


Metric Temporal Logic (MTL) specifications can capture complex state and timing requirements. Given a nonlinear dynamical system and an MTL specification for that system, our goal is to find a trajectory that violates or satisfies the specification. This trajectory can be used as a concrete feedback to the system designer in the case of violation or as a trajectory to be tracked in the case of satisfaction. The search for such a trajectory is conducted over the space of initial conditions, system parameters and input signals. We convert the trajectory search problem into an optimization problem through MTL robust semantics. Robustness quantifies how close the trajectory is to violating or satisfying a specification. Starting from some arbitrary initial condition and parameter and given an input signal, we compute a descent direction in the search space, which leads to a trajectory that optimizes the MTL robustness. This process can be iterated to reach local optima (min or max). We demonstrate the method on examples from the literature.

Original languageEnglish (US)
Title of host publication2014 American Control Conference, ACC 2014
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages6
ISBN (Print)9781479932726
StatePublished - 2014
Event2014 American Control Conference, ACC 2014 - Portland, OR, United States
Duration: Jun 4 2014Jun 6 2014

Publication series

NameProceedings of the American Control Conference
ISSN (Print)0743-1619


Other2014 American Control Conference, ACC 2014
Country/TerritoryUnited States
CityPortland, OR


  • Nonlinear systems
  • Optimal control
  • Optimization

ASJC Scopus subject areas

  • Electrical and Electronic Engineering


Dive into the research topics of 'Functional gradient descent method for Metric Temporal Logic specifications'. Together they form a unique fingerprint.

Cite this