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

14 Citations (Scopus)

Abstract

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 publicationProceedings of the American Control Conference
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages2312-2317
Number of pages6
ISBN (Print)9781479932726
DOIs
StatePublished - 2014
Event2014 American Control Conference, ACC 2014 - Portland, OR, United States
Duration: Jun 4 2014Jun 6 2014

Other

Other2014 American Control Conference, ACC 2014
CountryUnited States
CityPortland, OR
Period6/4/146/6/14

Fingerprint

Temporal logic
Trajectories
Specifications
Nonlinear dynamical systems
Semantics
Concretes
Feedback

Keywords

  • Nonlinear systems
  • Optimal control
  • Optimization

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

Cite this

Abbas, H., Winn, A., Fainekos, G., & Julius, A. A. (2014). Functional gradient descent method for Metric Temporal Logic specifications. In Proceedings of the American Control Conference (pp. 2312-2317). [6859453] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ACC.2014.6859453

Functional gradient descent method for Metric Temporal Logic specifications. / Abbas, Houssam; Winn, Andrew; Fainekos, Georgios; Julius, A. Agung.

Proceedings of the American Control Conference. Institute of Electrical and Electronics Engineers Inc., 2014. p. 2312-2317 6859453.

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

Abbas, H, Winn, A, Fainekos, G & Julius, AA 2014, Functional gradient descent method for Metric Temporal Logic specifications. in Proceedings of the American Control Conference., 6859453, Institute of Electrical and Electronics Engineers Inc., pp. 2312-2317, 2014 American Control Conference, ACC 2014, Portland, OR, United States, 6/4/14. https://doi.org/10.1109/ACC.2014.6859453
Abbas H, Winn A, Fainekos G, Julius AA. Functional gradient descent method for Metric Temporal Logic specifications. In Proceedings of the American Control Conference. Institute of Electrical and Electronics Engineers Inc. 2014. p. 2312-2317. 6859453 https://doi.org/10.1109/ACC.2014.6859453
Abbas, Houssam ; Winn, Andrew ; Fainekos, Georgios ; Julius, A. Agung. / Functional gradient descent method for Metric Temporal Logic specifications. Proceedings of the American Control Conference. Institute of Electrical and Electronics Engineers Inc., 2014. pp. 2312-2317
@inproceedings{a1d2fa5d7a01476b8abed6d5d7d9eace,
title = "Functional gradient descent method for Metric Temporal Logic specifications",
abstract = "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.",
keywords = "Nonlinear systems, Optimal control, Optimization",
author = "Houssam Abbas and Andrew Winn and Georgios Fainekos and Julius, {A. Agung}",
year = "2014",
doi = "10.1109/ACC.2014.6859453",
language = "English (US)",
isbn = "9781479932726",
pages = "2312--2317",
booktitle = "Proceedings of the American Control Conference",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - GEN

T1 - Functional gradient descent method for Metric Temporal Logic specifications

AU - Abbas, Houssam

AU - Winn, Andrew

AU - Fainekos, Georgios

AU - Julius, A. Agung

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

KW - Nonlinear systems

KW - Optimal control

KW - Optimization

UR - http://www.scopus.com/inward/record.url?scp=84905693916&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84905693916&partnerID=8YFLogxK

U2 - 10.1109/ACC.2014.6859453

DO - 10.1109/ACC.2014.6859453

M3 - Conference contribution

SN - 9781479932726

SP - 2312

EP - 2317

BT - Proceedings of the American Control Conference

PB - Institute of Electrical and Electronics Engineers Inc.

ER -