Reachability Analysis for High-Index Linear Differential Algebraic Equations

Hoang Dung Tran, Luan Viet Nguyen, Nathaniel Hamilton, Weiming Xiang, Taylor T. Johnson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Reachability analysis is a fundamental problem for safety verification and falsification of Cyber-Physical Systems (CPS) whose dynamics follow physical laws usually represented as differential equations. In the last two decades, numerous reachability analysis methods and tools have been proposed for a common class of dynamics in CPS known as ordinary differential equations (ODE). However, there is lack of methods dealing with differential algebraic equations (DAE), which is a more general class of dynamics that is widely used to describe a variety of problems from engineering and science, such as multibody mechanics, electrical circuit design, incompressible fluids, molecular dynamics, and chemical process control. Reachability analysis for DAE systems is more complex than ODE systems, especially for high-index DAEs because they contain both a differential part (i.e., ODE) and algebraic constraints (AC). In this paper, we propose a scalable reachability analysis for a class of high-index large linear DAEs. In our approach, a high-index linear DAE is first decoupled into one ODE and one or several AC subsystems based on the well-known Marz decoupling method utilizing admissible projectors. Then, the discrete reachable set of the DAE, represented as a list of star-sets, is computed using simulation. Unlike ODE reachability analysis where the initial condition is freely defined by a user, in DAE cases, the consistency of the initial condition is an essential requirement to guarantee a feasible solution. Therefore, a thorough check for the consistency is invoked before computing the discrete reachable set. Our approach successfully verifies (or falsifies) a wide range of practical, high-index linear DAE systems in which the number of state variables varies from several to thousands.

Original languageEnglish (US)
Title of host publicationFormal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings
EditorsÉtienne André, Mariëlle Stoelinga, Mariëlle Stoelinga
PublisherSpringer
Pages160-177
Number of pages18
ISBN (Print)9783030296612
DOIs
StatePublished - Jan 1 2019
Externally publishedYes
Event17th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2019 - Amsterdam, Netherlands
Duration: Aug 27 2019Aug 29 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11750 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference17th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2019
CountryNetherlands
CityAmsterdam
Period8/27/198/29/19

Fingerprint

Reachability Analysis
Algebraic Differential Equations
Differential equations
Ordinary differential equations
Ordinary differential equation
Reachable Set
Initial conditions
Electrical Circuits
Circuit Design
Chemical Processes
Dynamic Process
Projector
Process Control
Decoupling
Molecular Dynamics
System Dynamics
Incompressible Fluid
Mechanics
Star
Subsystem

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Tran, H. D., Nguyen, L. V., Hamilton, N., Xiang, W., & Johnson, T. T. (2019). Reachability Analysis for High-Index Linear Differential Algebraic Equations. In É. André, M. Stoelinga, & M. Stoelinga (Eds.), Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings (pp. 160-177). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11750 LNCS). Springer. https://doi.org/10.1007/978-3-030-29662-9_10

Reachability Analysis for High-Index Linear Differential Algebraic Equations. / Tran, Hoang Dung; Nguyen, Luan Viet; Hamilton, Nathaniel; Xiang, Weiming; Johnson, Taylor T.

Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings. ed. / Étienne André; Mariëlle Stoelinga; Mariëlle Stoelinga. Springer, 2019. p. 160-177 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11750 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Tran, HD, Nguyen, LV, Hamilton, N, Xiang, W & Johnson, TT 2019, Reachability Analysis for High-Index Linear Differential Algebraic Equations. in É André, M Stoelinga & M Stoelinga (eds), Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11750 LNCS, Springer, pp. 160-177, 17th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2019, Amsterdam, Netherlands, 8/27/19. https://doi.org/10.1007/978-3-030-29662-9_10
Tran HD, Nguyen LV, Hamilton N, Xiang W, Johnson TT. Reachability Analysis for High-Index Linear Differential Algebraic Equations. In André É, Stoelinga M, Stoelinga M, editors, Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings. Springer. 2019. p. 160-177. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-29662-9_10
Tran, Hoang Dung ; Nguyen, Luan Viet ; Hamilton, Nathaniel ; Xiang, Weiming ; Johnson, Taylor T. / Reachability Analysis for High-Index Linear Differential Algebraic Equations. Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings. editor / Étienne André ; Mariëlle Stoelinga ; Mariëlle Stoelinga. Springer, 2019. pp. 160-177 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{fe4cf83875344ab28f4b3c53f4a9a90d,
title = "Reachability Analysis for High-Index Linear Differential Algebraic Equations",
abstract = "Reachability analysis is a fundamental problem for safety verification and falsification of Cyber-Physical Systems (CPS) whose dynamics follow physical laws usually represented as differential equations. In the last two decades, numerous reachability analysis methods and tools have been proposed for a common class of dynamics in CPS known as ordinary differential equations (ODE). However, there is lack of methods dealing with differential algebraic equations (DAE), which is a more general class of dynamics that is widely used to describe a variety of problems from engineering and science, such as multibody mechanics, electrical circuit design, incompressible fluids, molecular dynamics, and chemical process control. Reachability analysis for DAE systems is more complex than ODE systems, especially for high-index DAEs because they contain both a differential part (i.e., ODE) and algebraic constraints (AC). In this paper, we propose a scalable reachability analysis for a class of high-index large linear DAEs. In our approach, a high-index linear DAE is first decoupled into one ODE and one or several AC subsystems based on the well-known Marz decoupling method utilizing admissible projectors. Then, the discrete reachable set of the DAE, represented as a list of star-sets, is computed using simulation. Unlike ODE reachability analysis where the initial condition is freely defined by a user, in DAE cases, the consistency of the initial condition is an essential requirement to guarantee a feasible solution. Therefore, a thorough check for the consistency is invoked before computing the discrete reachable set. Our approach successfully verifies (or falsifies) a wide range of practical, high-index linear DAE systems in which the number of state variables varies from several to thousands.",
author = "Tran, {Hoang Dung} and Nguyen, {Luan Viet} and Nathaniel Hamilton and Weiming Xiang and Johnson, {Taylor T.}",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-29662-9_10",
language = "English (US)",
isbn = "9783030296612",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "160--177",
editor = "{\'E}tienne Andr{\'e} and Mari{\"e}lle Stoelinga and Mari{\"e}lle Stoelinga",
booktitle = "Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings",

}

TY - GEN

T1 - Reachability Analysis for High-Index Linear Differential Algebraic Equations

AU - Tran, Hoang Dung

AU - Nguyen, Luan Viet

AU - Hamilton, Nathaniel

AU - Xiang, Weiming

AU - Johnson, Taylor T.

PY - 2019/1/1

Y1 - 2019/1/1

N2 - Reachability analysis is a fundamental problem for safety verification and falsification of Cyber-Physical Systems (CPS) whose dynamics follow physical laws usually represented as differential equations. In the last two decades, numerous reachability analysis methods and tools have been proposed for a common class of dynamics in CPS known as ordinary differential equations (ODE). However, there is lack of methods dealing with differential algebraic equations (DAE), which is a more general class of dynamics that is widely used to describe a variety of problems from engineering and science, such as multibody mechanics, electrical circuit design, incompressible fluids, molecular dynamics, and chemical process control. Reachability analysis for DAE systems is more complex than ODE systems, especially for high-index DAEs because they contain both a differential part (i.e., ODE) and algebraic constraints (AC). In this paper, we propose a scalable reachability analysis for a class of high-index large linear DAEs. In our approach, a high-index linear DAE is first decoupled into one ODE and one or several AC subsystems based on the well-known Marz decoupling method utilizing admissible projectors. Then, the discrete reachable set of the DAE, represented as a list of star-sets, is computed using simulation. Unlike ODE reachability analysis where the initial condition is freely defined by a user, in DAE cases, the consistency of the initial condition is an essential requirement to guarantee a feasible solution. Therefore, a thorough check for the consistency is invoked before computing the discrete reachable set. Our approach successfully verifies (or falsifies) a wide range of practical, high-index linear DAE systems in which the number of state variables varies from several to thousands.

AB - Reachability analysis is a fundamental problem for safety verification and falsification of Cyber-Physical Systems (CPS) whose dynamics follow physical laws usually represented as differential equations. In the last two decades, numerous reachability analysis methods and tools have been proposed for a common class of dynamics in CPS known as ordinary differential equations (ODE). However, there is lack of methods dealing with differential algebraic equations (DAE), which is a more general class of dynamics that is widely used to describe a variety of problems from engineering and science, such as multibody mechanics, electrical circuit design, incompressible fluids, molecular dynamics, and chemical process control. Reachability analysis for DAE systems is more complex than ODE systems, especially for high-index DAEs because they contain both a differential part (i.e., ODE) and algebraic constraints (AC). In this paper, we propose a scalable reachability analysis for a class of high-index large linear DAEs. In our approach, a high-index linear DAE is first decoupled into one ODE and one or several AC subsystems based on the well-known Marz decoupling method utilizing admissible projectors. Then, the discrete reachable set of the DAE, represented as a list of star-sets, is computed using simulation. Unlike ODE reachability analysis where the initial condition is freely defined by a user, in DAE cases, the consistency of the initial condition is an essential requirement to guarantee a feasible solution. Therefore, a thorough check for the consistency is invoked before computing the discrete reachable set. Our approach successfully verifies (or falsifies) a wide range of practical, high-index linear DAE systems in which the number of state variables varies from several to thousands.

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

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

U2 - 10.1007/978-3-030-29662-9_10

DO - 10.1007/978-3-030-29662-9_10

M3 - Conference contribution

AN - SCOPUS:85073150766

SN - 9783030296612

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 160

EP - 177

BT - Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Proceedings

A2 - André, Étienne

A2 - Stoelinga, Mariëlle

A2 - Stoelinga, Mariëlle

PB - Springer

ER -