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
U2 - 10.1109/acc.2013.6580518
DO - 10.1109/acc.2013.6580518
M3 - Conference contribution
AN - SCOPUS:84883502317
SN - 9781479901777
T3 - Proceedings of the American Control Conference
SP - 4405
EP - 4410
BT - 2013 American Control Conference, ACC 2013
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2013 1st American Control Conference, ACC 2013
Y2 - 17 June 2013 through 19 June 2013
ER -