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

Shakiba Yaghoubi, Georgios Fainekos

    Research output: Contribution to journalArticle

    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 -