Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics

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

24 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

Fingerprint

Hybrid Automata
Reachability Analysis
Clocks
Pipe Flow
Pipe flow
Reachability
Reachable Set
Communication Delay
Delay Time
Execution Time
Intersection
Control System
Benchmark
Sampling
Control systems
Invariant
Communication
Approximation
Model
Demonstrate

Keywords

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

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
El Hakim, Viktorio Semir ; Bekooij, Marco Jan Gerrit. / Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics. SCOPES '19 Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems. editor / Sander Stuijk. ACM Inc., 2019. pp. 27-36
@inproceedings{a87170d456a14690892a1893e1a9385e,
title = "Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics",
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.",
keywords = "reachability analysis, Hybrid Automata, Clocks, linear dynamical system (LDS), Distributed control, Control system analysis",
author = "{El Hakim}, {Viktorio Semir} and Bekooij, {Marco Jan Gerrit}",
year = "2019",
month = "5",
day = "27",
doi = "10.1145/3323439.3323980",
language = "English",
pages = "27--36",
editor = "Sander Stuijk",
booktitle = "SCOPES '19 Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems",
publisher = "ACM Inc.",

}

El Hakim, VS & Bekooij, MJG 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. ACM Inc., pp. 27-36, 22nd International Workshop on Software and Compilers for Embedded Systems, SCOPES 2019, Sankt Goar, Germany, 27/05/19. https://doi.org/10.1145/3323439.3323980

Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics. / El Hakim, Viktorio Semir; Bekooij, Marco Jan Gerrit.

SCOPES '19 Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems. ed. / Sander Stuijk. ACM Inc., 2019. p. 27-36.

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

TY - GEN

T1 - Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics

AU - El Hakim, Viktorio Semir

AU - Bekooij, Marco Jan Gerrit

PY - 2019/5/27

Y1 - 2019/5/27

N2 - 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.

AB - 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.

KW - reachability analysis

KW - Hybrid Automata

KW - Clocks

KW - linear dynamical system (LDS)

KW - Distributed control

KW - Control system analysis

U2 - 10.1145/3323439.3323980

DO - 10.1145/3323439.3323980

M3 - Conference contribution

SP - 27

EP - 36

BT - SCOPES '19 Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems

A2 - Stuijk, Sander

PB - ACM Inc.

ER -

El Hakim VS, Bekooij MJG. Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics. In Stuijk S, editor, SCOPES '19 Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems. ACM Inc. 2019. p. 27-36 https://doi.org/10.1145/3323439.3323980