Computing descent direction of MTL robustness for non-linear systems

Houssam Abbas, Georgios Fainekos

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

15 Citations (Scopus)

Abstract

The automatic analysis of transient properties of nonlinear dynamical systems is a challenging problem. The problem is even more challenging when complex state-space and timing requirements must be satisfied by the system. Such complex requirements can be captured by Metric Temporal Logic (MTL) specifications. The problem of finding system behaviors that do not satisfy an MTL specification is referred to as MTL falsification. This paper presents an approach for improving stochastic MTL falsification methods by performing local search in the set of initial conditions. In particular, MTL robustness quantifies how correct or wrong is a system trajectory with respect to an MTL specification. Positive values indicate satisfaction of the property while negative values indicate falsification. A stochastic falsification method attempts to minimize the system's robustness with respect to the MTL property. Given some arbitrary initial state, this paper presents a method to compute a descent direction in the set of initial conditions, such that the new system trajectory gets closer to the unsafe set of behaviors. This technique can be iterated in order to converge to a local minimum of the robustness landscape. The paper demonstrates the applicability of the method on some challenging nonlinear systems from the literature.

Original languageEnglish (US)
Title of host publicationProceedings of the American Control Conference
Pages4405-4410
Number of pages6
StatePublished - 2013
Event2013 1st American Control Conference, ACC 2013 - Washington, DC, United States
Duration: Jun 17 2013Jun 19 2013

Other

Other2013 1st American Control Conference, ACC 2013
CountryUnited States
CityWashington, DC
Period6/17/136/19/13

Fingerprint

Temporal logic
Nonlinear systems
Specifications
Trajectories
Nonlinear dynamical systems

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

Cite this

Abbas, H., & Fainekos, G. (2013). Computing descent direction of MTL robustness for non-linear systems. In Proceedings of the American Control Conference (pp. 4405-4410). [6580518]

Computing descent direction of MTL robustness for non-linear systems. / Abbas, Houssam; Fainekos, Georgios.

Proceedings of the American Control Conference. 2013. p. 4405-4410 6580518.

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

Abbas, H & Fainekos, G 2013, Computing descent direction of MTL robustness for non-linear systems. in Proceedings of the American Control Conference., 6580518, pp. 4405-4410, 2013 1st American Control Conference, ACC 2013, Washington, DC, United States, 6/17/13.
Abbas H, Fainekos G. Computing descent direction of MTL robustness for non-linear systems. In Proceedings of the American Control Conference. 2013. p. 4405-4410. 6580518
Abbas, Houssam ; Fainekos, Georgios. / Computing descent direction of MTL robustness for non-linear systems. Proceedings of the American Control Conference. 2013. pp. 4405-4410
@inproceedings{35f55dc4c1c44293b7c09a22acc2fef0,
title = "Computing descent direction of MTL robustness for non-linear systems",
abstract = "The automatic analysis of transient properties of nonlinear dynamical systems is a challenging problem. The problem is even more challenging when complex state-space and timing requirements must be satisfied by the system. Such complex requirements can be captured by Metric Temporal Logic (MTL) specifications. The problem of finding system behaviors that do not satisfy an MTL specification is referred to as MTL falsification. This paper presents an approach for improving stochastic MTL falsification methods by performing local search in the set of initial conditions. In particular, MTL robustness quantifies how correct or wrong is a system trajectory with respect to an MTL specification. Positive values indicate satisfaction of the property while negative values indicate falsification. A stochastic falsification method attempts to minimize the system's robustness with respect to the MTL property. Given some arbitrary initial state, this paper presents a method to compute a descent direction in the set of initial conditions, such that the new system trajectory gets closer to the unsafe set of behaviors. This technique can be iterated in order to converge to a local minimum of the robustness landscape. The paper demonstrates the applicability of the method on some challenging nonlinear systems from the literature.",
author = "Houssam Abbas and Georgios Fainekos",
year = "2013",
language = "English (US)",
isbn = "9781479901777",
pages = "4405--4410",
booktitle = "Proceedings of the American Control Conference",

}

TY - GEN

T1 - Computing descent direction of MTL robustness for non-linear systems

AU - Abbas, Houssam

AU - Fainekos, Georgios

PY - 2013

Y1 - 2013

N2 - The automatic analysis of transient properties of nonlinear dynamical systems is a challenging problem. The problem is even more challenging when complex state-space and timing requirements must be satisfied by the system. Such complex requirements can be captured by Metric Temporal Logic (MTL) specifications. The problem of finding system behaviors that do not satisfy an MTL specification is referred to as MTL falsification. This paper presents an approach for improving stochastic MTL falsification methods by performing local search in the set of initial conditions. In particular, MTL robustness quantifies how correct or wrong is a system trajectory with respect to an MTL specification. Positive values indicate satisfaction of the property while negative values indicate falsification. A stochastic falsification method attempts to minimize the system's robustness with respect to the MTL property. Given some arbitrary initial state, this paper presents a method to compute a descent direction in the set of initial conditions, such that the new system trajectory gets closer to the unsafe set of behaviors. This technique can be iterated in order to converge to a local minimum of the robustness landscape. The paper demonstrates the applicability of the method on some challenging nonlinear systems from the literature.

AB - The automatic analysis of transient properties of nonlinear dynamical systems is a challenging problem. The problem is even more challenging when complex state-space and timing requirements must be satisfied by the system. Such complex requirements can be captured by Metric Temporal Logic (MTL) specifications. The problem of finding system behaviors that do not satisfy an MTL specification is referred to as MTL falsification. This paper presents an approach for improving stochastic MTL falsification methods by performing local search in the set of initial conditions. In particular, MTL robustness quantifies how correct or wrong is a system trajectory with respect to an MTL specification. Positive values indicate satisfaction of the property while negative values indicate falsification. A stochastic falsification method attempts to minimize the system's robustness with respect to the MTL property. Given some arbitrary initial state, this paper presents a method to compute a descent direction in the set of initial conditions, such that the new system trajectory gets closer to the unsafe set of behaviors. This technique can be iterated in order to converge to a local minimum of the robustness landscape. The paper demonstrates the applicability of the method on some challenging nonlinear systems from the literature.

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

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

M3 - Conference contribution

SN - 9781479901777

SP - 4405

EP - 4410

BT - Proceedings of the American Control Conference

ER -