Falsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time

Shakiba Yaghoubi, Georgios Fainekos

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

We study the problem of computing input signals that produce system behaviors that falsify requirements written in temporal logic. We provide a method to automatically search for falsifying time varying uncertain inputs for nonlinear and possibly hybrid systems. The input to the system is parametrized using piecewise constant signals with varying switch times. By applying small perturbations to the system input in space and time, and by using gradient descent approach, we try to converge to the worst local system behavior. The experimental results on non-trivial benchmarks demonstrate that this local search can significantly improve the rate of finding falsifying counterexamples.

Original languageEnglish (US)
Pages (from-to)103-108
Number of pages6
JournalIFAC-PapersOnLine
Volume51
Issue number16
DOIs
StatePublished - Jan 1 2018

Fingerprint

Time switches
Temporal logic
Hybrid systems

Keywords

  • Cyber-physical systems
  • Gradient Descent
  • Optimization
  • Temporal Logic
  • Testing

ASJC Scopus subject areas

  • Control and Systems Engineering

Cite this

Falsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time. / Yaghoubi, Shakiba; Fainekos, Georgios.

In: IFAC-PapersOnLine, Vol. 51, No. 16, 01.01.2018, p. 103-108.

Research output: Contribution to journalArticle

@article{8dbccb121dc14b36b019442bd556616a,
title = "Falsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time",
abstract = "We study the problem of computing input signals that produce system behaviors that falsify requirements written in temporal logic. We provide a method to automatically search for falsifying time varying uncertain inputs for nonlinear and possibly hybrid systems. The input to the system is parametrized using piecewise constant signals with varying switch times. By applying small perturbations to the system input in space and time, and by using gradient descent approach, we try to converge to the worst local system behavior. The experimental results on non-trivial benchmarks demonstrate that this local search can significantly improve the rate of finding falsifying counterexamples.",
keywords = "Cyber-physical systems, Gradient Descent, Optimization, Temporal Logic, Testing",
author = "Shakiba Yaghoubi and Georgios Fainekos",
year = "2018",
month = "1",
day = "1",
doi = "10.1016/j.ifacol.2018.08.018",
language = "English (US)",
volume = "51",
pages = "103--108",
journal = "IFAC-PapersOnLine",
issn = "2405-8963",
publisher = "IFAC Secretariat",
number = "16",

}

TY - JOUR

T1 - Falsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time

AU - Yaghoubi, Shakiba

AU - Fainekos, Georgios

PY - 2018/1/1

Y1 - 2018/1/1

N2 - We study the problem of computing input signals that produce system behaviors that falsify requirements written in temporal logic. We provide a method to automatically search for falsifying time varying uncertain inputs for nonlinear and possibly hybrid systems. The input to the system is parametrized using piecewise constant signals with varying switch times. By applying small perturbations to the system input in space and time, and by using gradient descent approach, we try to converge to the worst local system behavior. The experimental results on non-trivial benchmarks demonstrate that this local search can significantly improve the rate of finding falsifying counterexamples.

AB - We study the problem of computing input signals that produce system behaviors that falsify requirements written in temporal logic. We provide a method to automatically search for falsifying time varying uncertain inputs for nonlinear and possibly hybrid systems. The input to the system is parametrized using piecewise constant signals with varying switch times. By applying small perturbations to the system input in space and time, and by using gradient descent approach, we try to converge to the worst local system behavior. The experimental results on non-trivial benchmarks demonstrate that this local search can significantly improve the rate of finding falsifying counterexamples.

KW - Cyber-physical systems

KW - Gradient Descent

KW - Optimization

KW - Temporal Logic

KW - Testing

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

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

U2 - 10.1016/j.ifacol.2018.08.018

DO - 10.1016/j.ifacol.2018.08.018

M3 - Article

VL - 51

SP - 103

EP - 108

JO - IFAC-PapersOnLine

JF - IFAC-PapersOnLine

SN - 2405-8963

IS - 16

ER -