## Abstract

Partial differential equations (PDEs) mathematically describe a wide range of phenomena such as fluid dynamics, or quantum mechanics. Although great achievements have been accomplished in the field of numerical methods for solving PDEs, from a safety verification (or falsification) perspective, methods are still needed to verify (or falsify) a system whose dynamics is specified as a PDE that may depend not only on space, but also on time. As many cyber-physical systems (CPS) involve sensing and control of physical phenomena modeled as PDEs, reachability analysis of PDEs provides novel methods for safety verification and falsification. As a first step to address this challenging problem, we propose a reachability analysis approach leveraging the well-known Galerkin Finite Element Method (FEM) for a class of one-dimensional linear parabolic PDEs with fixed but uncertain inputs and initial conditions, which is a subclass of PDEs that is useful for modeling, for instance, heat flows. In particular, a continuous approximate reachable set of the parabolic PDE is computed using linear interpolation. Since a complete conservativeness is hardly achieved by using the approximate reachable set, to enhance the conservativeness, we investigate the error bound between the numerical solution and the exact analytically unsolvable solution to bloat the continuous approximate reachable set. This bloated reachable set is then used for safety verification and falsification. In the case that the safety specification is violated, our approach produces a numerical trace to prove that there exists an initial condition and input that lead the system to an unsafe state.

Original language | English (US) |
---|---|

Pages (from-to) | 133-138 |

Number of pages | 6 |

Journal | IFAC-PapersOnLine |

Volume | 51 |

Issue number | 16 |

DOIs | |

State | Published - Jan 1 2018 |

Externally published | Yes |

## Keywords

- Cyber-Physical Systems
- Partial Differential Equations
- Reachability Analysis

## ASJC Scopus subject areas

- Control and Systems Engineering

## Access to Document

## Other files and links

## Fingerprint

Dive into the research topics of 'Reachability Analysis for One Dimensional Linear Parabolic Equations'. Together they form a unique fingerprint.## Cite this

- APA
- Standard
- Harvard
- Vancouver
- Author
- BIBTEX
- RIS

*IFAC-PapersOnLine*,

*51*(16), 133-138. https://doi.org/10.1016/j.ifacol.2018.08.023

**Reachability Analysis for One Dimensional Linear Parabolic Equations.** / Tran, Hoang Dung; Xiang, Weiming; Bak, Stanley; Johnson, Taylor T.

Research output: Contribution to journal › Article › peer-review

*IFAC-PapersOnLine*, vol. 51, no. 16, pp. 133-138. https://doi.org/10.1016/j.ifacol.2018.08.023

**Reachability Analysis for One Dimensional Linear Parabolic Equations**. In: IFAC-PapersOnLine. 2018 ; Vol. 51, No. 16. pp. 133-138.

}

TY - JOUR

T1 - Reachability Analysis for One Dimensional Linear Parabolic Equations

AU - Tran, Hoang Dung

AU - Xiang, Weiming

AU - Bak, Stanley

AU - Johnson, Taylor T.

N1 - Funding Information: Reachability Analysis for One Dimensional Reachability Analysis for One Dimensional ReachabLiilniteyarAPnalarysiabsolfoicrEOnqueatDioinmsensional Linear Parabolic Equations Linear Pa∗rabolic Equ∗ations ∗∗ Hoang-Dung Tran ∗ Weiming Xiang ∗ Stanley fiaff ∗∗ Hoang-Dung Tran∗ Weiming Xiang∗∗ Stanley fiaff∗∗ Hoang-Dung TraTna∗ylWoreTim. iJnoghXnsioanng∗∗ Stanley fiaff∗∗ Hoang-DungTranTa∗ylorWeT.imiJohng Xiannsong∗∗ Stanley fiaff∗∗ Taylor T. Johnson∗ ∗∗ Vanderbilt University, TN 37023, USA. ∗∗Vanderbilt University, TN 37023, USA. ∗V∗aAnidreFrobirlcteURneisveearrscithy,LaTbNora3t7o0r2y3,,UUSSAA.. ∗∗∗Air Force Research Laboratory, USA. ∗∗Air Force Research Laboratory, USA. Air Force Research Laboratory, USA. Abstract: Partial differential equations (PDEs) mathematicallΩ describe a wide range oΣ Abstract: Partial differential equations (PDEs) mathematicallΩ describe a wide range oΣ pAhbesntormacent:a sPuacrhtiaals fdluififderdenΩtniaaml iecqsu, aotrioqnusan(tPuDmEms)ecmhatnhicesm. a∆tlitchaolluΩghdegsrceraibteacahiweviedme ernatnsgheavoeΣ Abstract: Partial differential equations (PDEs) mathematicallΩ describe a wide range oΣ been accomplished in the field oΣ numerical methods Σor solving PDEs, Σrom a saΣetΩ verification been accomplished in the field oΣ numerical methods Σor solving PDEs, Σrom a saΣetΩ verification dΩnamics is specified as a PDE that maΩ depend not onlΩ on space, but also on time. ∆s (or Σalsification) perspective, methods are still needed to veriΣΩ (or ΣalsiΣΩ) a sΩstem whose manΩ cΩber-phΩsical sΩstems (CPS) involve sensing and control oΣ phΩsical phenomena modeled amsanPΩDcEΩsb,err-epahcΩhsaibciallitsΩΩsatnemalsΩs(iCsPoSΣ)PinDvEolsvepsreonvsidinegs annodveclonmtreotlhooΣdpshΣΩosricsaalΣpethΩenvoemriefincatmioondealnedd manΩ cΩber-phΩsical sΩstems (CPS) involve sensing and control oΣ phΩsical phenomena modeled Σalsification. ∆s a first step to address this challenging problem, we propose a reachabilitΩ Σalsification. ∆s a first step to address this challenging problem, we propose a reachabilitΩ class oΣ one-dimensional linear parabolic PDEs with fixed but uncertain inputs and initial analΩsis approach leveraging the well-known Galerkin Finite Element Method (FEM) Σor a conditions, which is a subclass oΣ PDEs that is useΣul Σor modeling, Σor instance, heat flows. In class oΣ one-dimensional linear parabolic PDEs with fixed but uncertain inputs and initial particular, a continuous approximate reachable set oΣ the parabolic PDE is computed using linear particular, a continuous approximate reachable set oΣ the parabolic PDE is computed using linear reachable set, to enhance the conservativeness, we investigate the error bound between the interpolation. Since a complete conservativeness is hardlΩ achieved bΩ using the approximate numerical solution and the exact analΩticallΩ unsolvable solution to bloat the continuous reachable set, to enhance the conservativeness, we investigate the error bound between the approximate reachable set. This bloated reachable set is then used Σor saΣetΩ verification and approximate reachable set. This bloated reachable set is then used Σor saΣetΩ verification and numerical trace to prove that there exists an initial condition and input that lead the sΩstem numerical trace to prove that there exists an initial condition and input that lead the sΩstem numerical trace to prove that there exists an initial condition and input that lead the sΩstem to an unsaΣe state. © 2018, IFAC (International Federation of Automatic Control) Hosting by Elsevier Ltd. All rights reserved. Keywords: ReachabilitΩ ∆nalΩsis, CΩber-PhΩsical SΩstems, Partial Differential Equations Keywords: ReachabilitΩ ∆nalΩsis, CΩber-PhΩsical SΩstems, Partial Differential Equations Keywords: ReachabilitΩ ∆nalΩsis, CΩber-PhΩsical SΩstems, Partial Differential Equations 1. INTRODUCTION lenging problem in reachabilitΩ analΩsis named state space 1. INTRODUCTION lenging problem in reachabilitΩ analΩsis named state space 1. INTRODUCTION eexnpgloinsigopnr.oblem in reachabilitΩ analΩsis named state space explosion. ReachabilitΩanalΩs1.isIisNTtheROΣundaDUCTIOmentNal problem in saΣetΩ leexngplosingionpro. blem in reachabilitΩ analΩsis named state space ReachabilitΩ analΩsis is the Σundamental problem in saΣetΩ ∆lthough significant works in reachablitΩ analΩsis have vReeraifcihcaatbiiolintΩoaΣncaΩlbΩesirs-pishΩthsiecaΣulnsdΩasmteemnst.alOpvreorbltehmeilnasstaΣtewtΩo ex∆lthoplosugionh. significant works in reachablitΩ analΩsis have verification oΣ cΩber-phΩsical sΩstems. Over the last two belthnoduognhesΣiogrnicfiocnatnintuwouorskasnidnhrΩebarcihdabsΩlisttΩemansawlΩitshisOhDavEe ReachabilitΩ analΩsis is the Σundamental problem in saΣetΩ been done Σor continuous and hΩbrid sΩstems with ODE decades, numerous techniques and tools have been pro-bΩeennamdiocnse, lΣiotrtlecoantttinenutoiuosn ahnads hbΩebernidpsaΩidstetmo sthweitchlaOssDoEΣ verification oΣ cΩber-phΩsical sΩstems. Over the last two dΩnamics, little attention has been paid to the class oΣ posed Σor continuous and hΩbrid sΩstems whose dΩnamics sΩΩsntaemmiscsw,itlhittPleDaEttdeΩnntiaomnichsatshbateeanpppeaairdintomtahneΩcslcaisesncoeΣ decades, numerous techniques and tools have been pro-sΩstems with PDE dΩnamics that appear in manΩ science are described bΩ linear or nonlinear ordinarΩ differen-aΩnsdteemngsiwneitehrinPgDpErodbΩlnemamsiscuscthaatsaflpupideadrΩinnammaicnsΩcsocnietnrocle, posed Σor continuous and hΩbrid sΩstems whose dΩnamics and engineering problems such as fluid dΩnamics control, tial equations (ODEs). ReachabilitΩ analΩsis using zono-hneadteenqguianteieorninagnpdrqobulaenmtusmsumchecahsafnluicisd. dTΩhnisamioctsivcaotnetsrouls, are described bΩ linear or nonlinear ordinarΩ differen-heat equation and quantum mechanics. This motivates us topes/support Σunctions has been demonstrated to be the hoeactoenqduuacttiornesaenadrcqhuaontutmhismiencthearnesictisn. gThbiustmcohtaivllaetnegsinugs tial equations (ODEs). ReachabilitΩ analΩsis using zono-to conduct research on this interesting but challenging most efficient and scalable approach that can veriΣΩ linear porocbolenmdu.cIt srheoseualdrcbheonnottehdisthianttearetΩstpiincgalbpuatracbhoallilceneqguinag-topes/support Σunctions has been demonstrated to be the problem. It should be noted that a tΩpical parabolic equa-continuous and hΩbrid sΩstems with up to hundreds oΣ piroonbcleamlle.dIthsehaotuelqdubaetionnotheadstbheaetnautsΩepdicaaslapbaeranbchomlicarekquΣoar-most efficient and scalable approach that can veriΣΩ linear tion called heat equation has been used as a benchmark Σor state variables ??. For the nonlinear case, Flow* ? utilizing eivoanlucaatlilnedg htheaetsecqaulaabtilointΩhoaΣs abereenceunstedreaaschaabeinlictΩhmanaraklΩΣsoirs continuous and hΩbrid sΩstems with up to hundreds oΣ evaluating the scalabilitΩ oΣ a recent reachabilitΩ analΩsis TaΩlor model is well-known. RecentlΩ, the order-reduction avpaplruoaatcinhgdtehaelinsgcawlaibthililtaΩrgoeΣ sacarelecelintearerascΩhsatbemilistΩ?.anInaltΩhsis state variables ??. For the nonlinear case, Flow* ? utilizing approach dealing with large scale linear sΩstems ?. In this abstraction ?? and simulation-based reachabilitΩ analΩ-copnptreoxatc,hthdeeahlienagt weqituhatliaorngewsacsalteralninseΣoarrmsΩesdteinmtso ?a. cIonntthinis-sis ?? have exhibited an abilitΩ to tackle the most chal-context, the heat equation was transΣormed into a contin-sis ?? have exhibited an abilitΩ to tackle the most chal-context, the heat equation was transΣormed into a contin-★sisThe??materialhave epxhreibitesenteddinanthisabpapiliterΩistobasedtackupleonthewormoksuppst cortedhal- uosaΣusetΩODEspecimficatodeionl usoΣinginaterfiniteest wdiffas gierevencneΣormedithoscrdetaendmeshthe ★ The material presented in this paper is based upon work supported saΣetΩ specification oΣ interest was given Σor discrete mesh b★y the National Science Foundation (NSF) under grant numbers CNS saΣetΩ specification oΣ interest was given Σor discrete mesh by the National Science Foundation (NSF) under grant numbers CNS points. It is also worth noting that the input oΣ the heat 14T4h3e1m1,aCteNriSal1p7r1es3e2n5t3e,dSinHFthi1s5p2a7p3e9r8i,sabnadsedSHuFpon17w3o6r3k23s,upthpeorAteidr eqouinattsi.onItbiesnaclhsmo awrokrtwhasnoatsisnugmtehdatothbee aincpountstoaΣntthwe ihtheaat 1464311, CNS 1713253, SHF 1527398, and SHF 1736323, the Air 1464311, CNS 1713253, SHF 1527398, and SHF 1736323, the Air equation benchmark was assumed to be a constant with a Force Research Laboratory (AFRL) through the AFRLs Summer small time-invariant uncertainty while the initial states oΣ of 6I4n3n1o1v,atCioNnS(S17o1I)32P5r3o,gSraHmF u1n5d2e7r39c8o,ntarnadctSFHAF8615703-61322-33-,7t2h5e5 Aviiar equation benchmark was assumed to be a constant with a ofof IInnnnoovvaattiioonn (SoI(SoI)) PProgramrogram underunder ccoonnttrraacctt FFAA8650-12-38650-12-3-7255-7255 vviaia the mesh points was represented as a bounded box. FuobrceonRtreascetarncuhmLbaebroWraBtoSrCy(7A25F5RSLO)IthVrUoug0h001th,eanAdFtRhLesASirumFomrceer smalltime-invariantuncertaintywhiletheinitialstatesoΣ subcontract number WBSC 7255 SOI VU 0001, and the Air Force t∆hlthoe meshughptheointhes waatserquaepretiosenntedhasasbaeebnoudendmedonsbtraox.ted to subfffIicncoennotovrfaatcSitocnineun(tmSifobiIcer) RPWBSCersoegarracmh7255(uAndFeOSOIrScRo)nVtUtrharc0001,otuFgAh8andc6o5n0t-ther1a2c-t3A-7ni2ur5mF5bovrecriaes the mesh points was represented as a bounded box. FuAb9c5o5n0t-r1a5c-t1-n0u2m58b,erFAW9B55S0C-1762-15-502S4O6I, VanUd 0F0A019,55a0n-d18t-h1e-0A12ir2.FoTrhcee belthaouggohodthbeenhcehatmaerqkuaΣtoiornahccaesssbinegenthdeemsocnalsatbrailtietdΩ tooΣ FA9550-15-1-0258, FA9550-16-1-0246, and FA9550-18-1-0122. The be a good benchmark Σor accessing the scalabilitΩ oΣ FA.fSf9550-15-1-02i.cegoovferSncmieennt58,tifiics FaRAuet9550-sheoarriczh16-1-0246,ed(AtoFOreSpRro)andduthcreoFauAng955dh dc0-18-1-0122.iosntrtirbaucttenruemprbTheinetrss berifaicagtoiond tbeecnhcnhiqmuaersk, aΣordeaepcceersssitnugdΩthsehosucladlabielitdΩonoeΣ U.S. government is authorized to reproduce and distribute reprints verification techniques, a deeper studΩ should be done FoAr9G55o0v-e1r5n-m1-e0n2t5a8l,puFrAp9o5s5e0s-n16o-t1w-i0t2h4s6ta,nadnindgFaAn9y5c5o0p-1y8ri-g1h-0t1n2o2t.aTtiohne be a good benchmark Σor accessing the scalabilitΩ oΣ for Governmental purposes notwithstanding any copyright notation verification techniques, a deeper studΩ should be done forh.eSrG.eogonovv.eerAnrnmymeoenpntaitnliisopurpnasu,tfoseshinodriiznnegodst,wtaointdrhescptoarnoncddluiuncsgeioaannnsydorcdoriepsctyrorimibgumhtteennotationrdeaptriionntss ΣoΣoperrrificecttiwwfiaooctioarerteinoaanssootensnccosh..nncFirsFieqirrunsettellsdΩΩ,,,waitititdeisihsererapeeaarrsseoogsnanitudΩoanblebleintotshosouphhaaaldcvveeebanaessdaadoΣeΣneneottΩΩt thereon. Any opinions, findings, and conclusions or recommendations Σor two reasons. FirstlΩ, it is reasonable to have a saΣetΩ thereon. Any opinions, findings, and conclusions or recommendations specification concerned with a region in space and not foxrprGeossveedrnimnetnhtiaslppuubrpliocsaetsionnotawreiththstoasnedoinfgthaenyauctohpoyrrsigahntdnodtoatnioont specification concerned with a region in space and not expressed in this publication are those of the authors and do not spnelΩcicfiocnactieonntracotendceartnsepdecwifiitchmaesrhegpiointsin. Inspoatcheerawndorlndost, exheepressedcreesosanr.iAlyninryefothislpecintipublicationtohnes,vfiienwdisnogfsare,AaFndRthoseLco,nAcFlofuOsitheSoRns,orauthorsrNecSoFm.mandenddoationotns ononllΩΩ conconcceennttrratateded atat spspeciecifificc meshmesh ppoioinntts.s. InIn otothherer wwoorrlldds,s, expressed in this publication are those of the authors and do not specification concerned with a region in space and not necessarilyexpressed inreflectthis publicationthe views ofareAFRthoseL, AFofOtheSR,authorsor NSF.and do not onlΩ concentrated at specific mesh points. In other worlds, necessarily reflect the views of AFRL, AFOSR, or NSF. onlΩ concentrated at specific mesh points. In other worlds, 2405-8963 © 2018, IFAC (International Federation of Automatic Control) Hosting by Elsevier Ltd. All rights reserved. Copyright © 2018 IFAC 133 CCPooeppeyyr rrriieggvhhiett w©© u22n00d11e88r IIrFFeAAspCConsibility of International Federation of Automa1331t3ic3 Control. Copyright © 2018 IFAC 133 10.1016/j.ifacol.2018.08.023 Copyright © 2018 IFAC 133 we are interested in continuous-space and not discrete-space reachability analysis. Secondffi it is crflcial to have an affffroach that works for more general tyffes of inffflts and initial conditionsffi i.e.ffi an inffflt described by a nonlinear fflnction in both time and sffaceffi and an initial condition deΣned by a nonlinear sffatial fflnction. Publisher Copyright: © 2018

PY - 2018/1/1

Y1 - 2018/1/1

N2 - Partial differential equations (PDEs) mathematically describe a wide range of phenomena such as fluid dynamics, or quantum mechanics. Although great achievements have been accomplished in the field of numerical methods for solving PDEs, from a safety verification (or falsification) perspective, methods are still needed to verify (or falsify) a system whose dynamics is specified as a PDE that may depend not only on space, but also on time. As many cyber-physical systems (CPS) involve sensing and control of physical phenomena modeled as PDEs, reachability analysis of PDEs provides novel methods for safety verification and falsification. As a first step to address this challenging problem, we propose a reachability analysis approach leveraging the well-known Galerkin Finite Element Method (FEM) for a class of one-dimensional linear parabolic PDEs with fixed but uncertain inputs and initial conditions, which is a subclass of PDEs that is useful for modeling, for instance, heat flows. In particular, a continuous approximate reachable set of the parabolic PDE is computed using linear interpolation. Since a complete conservativeness is hardly achieved by using the approximate reachable set, to enhance the conservativeness, we investigate the error bound between the numerical solution and the exact analytically unsolvable solution to bloat the continuous approximate reachable set. This bloated reachable set is then used for safety verification and falsification. In the case that the safety specification is violated, our approach produces a numerical trace to prove that there exists an initial condition and input that lead the system to an unsafe state.

AB - Partial differential equations (PDEs) mathematically describe a wide range of phenomena such as fluid dynamics, or quantum mechanics. Although great achievements have been accomplished in the field of numerical methods for solving PDEs, from a safety verification (or falsification) perspective, methods are still needed to verify (or falsify) a system whose dynamics is specified as a PDE that may depend not only on space, but also on time. As many cyber-physical systems (CPS) involve sensing and control of physical phenomena modeled as PDEs, reachability analysis of PDEs provides novel methods for safety verification and falsification. As a first step to address this challenging problem, we propose a reachability analysis approach leveraging the well-known Galerkin Finite Element Method (FEM) for a class of one-dimensional linear parabolic PDEs with fixed but uncertain inputs and initial conditions, which is a subclass of PDEs that is useful for modeling, for instance, heat flows. In particular, a continuous approximate reachable set of the parabolic PDE is computed using linear interpolation. Since a complete conservativeness is hardly achieved by using the approximate reachable set, to enhance the conservativeness, we investigate the error bound between the numerical solution and the exact analytically unsolvable solution to bloat the continuous approximate reachable set. This bloated reachable set is then used for safety verification and falsification. In the case that the safety specification is violated, our approach produces a numerical trace to prove that there exists an initial condition and input that lead the system to an unsafe state.

KW - Cyber-Physical Systems

KW - Partial Differential Equations

KW - Reachability Analysis

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

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

U2 - 10.1016/j.ifacol.2018.08.023

DO - 10.1016/j.ifacol.2018.08.023

M3 - Article

AN - SCOPUS:85052613718

VL - 51

SP - 133

EP - 138

JO - IFAC-PapersOnLine

JF - IFAC-PapersOnLine

SN - 2405-8963

IS - 16

ER -