Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics

Viktorio Semir El Hakim*, Marco Jan Gerrit Bekooij

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)
    93 Downloads (Pure)

    Abstract

    Disributed control systems often exhibit aperiodic sampling behavior due to varying communication delays and execution times. In such cases traditional analysis methods fall short because the functional and temporal behaviors need to be analyzed simultaneously. Therefore such systems are often modeled by Hybrid Automata (HA) with clock and non-clock variables, and verified using reachability analysis. However, modern reachability tools introduce a large overapproximation error because non-clock variables, as well as clock variables, are equally treated by the algorithm.

    In this paper we present a reachability algorithm which exploits the explicit separation of clock and non-clock variables in the Hybrid Automata with Clocked Linear Dynamics (HA-CLD) subclass, as well as restricting that guard and invariant constraints can only be specified in the HA-CLD model for clock variables. These properties of HA-CLD allow independent computation of tight reachable set over-approximations, in the form of flow-pipes, of clock and non-clock variables. A computationaly efficient and tight intersection operation is obtained by relating segments of the clock flow-pipe with segments of the non-clock flow-pipe.

    We demonstrate the effectiveness of our approach using two benchmarks, in the context of verifying stability. From the results it can be concluded that our reachability approach obtains significantly tighter results with an up-to 65 times smaller run-time compared to the start-of-the-art model checker SpaceEx.
    Original languageEnglish
    Title of host publicationSCOPES '19 Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems
    EditorsSander Stuijk
    PublisherACM Inc.
    Pages27-36
    Number of pages10
    ISBN (Electronic)978-1-4503-6762-2
    DOIs
    Publication statusPublished - 27 May 2019
    Event22nd International Workshop on Software and Compilers for Embedded Systems, SCOPES 2019 - Sankt Goar, Germany
    Duration: 27 May 201928 May 2019
    Conference number: 22
    https://scopesconf.org/scopes-19/

    Workshop

    Workshop22nd International Workshop on Software and Compilers for Embedded Systems, SCOPES 2019
    Abbreviated titleSCOPES 2019
    CountryGermany
    CitySankt Goar
    Period27/05/1928/05/19
    Internet address

    Keywords

    • reachability analysis
    • Hybrid Automata
    • Clocks
    • linear dynamical system (LDS)
    • Distributed control
    • Control system analysis

    Fingerprint Dive into the research topics of 'Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics'. Together they form a unique fingerprint.

  • Cite this

    El Hakim, V. S., & Bekooij, M. J. G. (2019). Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics. In S. Stuijk (Ed.), SCOPES '19 Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems (pp. 27-36). ACM Inc.. https://doi.org/10.1145/3323439.3323980