Abstract
In this work, we introduce a framework for the statistical verification of Metric Interval Temporal Logic (MITL) formulas on continuous-time dynamical systems. By considering the continuous-time Markov process associated with the dynamical system, we apply the Mori-Zwanzig method to reduce the original system to a Continuous-Time Markov Chain (CTMC). Accordingly, the MITL formulas on the original system can be reduced to MITL formulas on the CTMC. Furthermore, we propose a statistical verification algorithm for checking the MITL formulas on the CTMCand show that the original MITL formulas on the original system can be checked by this procedure.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 267-273 |
| Number of pages | 7 |
| Journal | IFAC-PapersOnLine |
| Volume | 48 |
| Issue number | 27 |
| DOIs | |
| State | Published - 2015 |
ASJC Scopus subject areas
- Control and Systems Engineering
Fingerprint
Dive into the research topics of 'A Mori-Zwanzig and MITL Based Approach to Statistical Verification of Continuous-time Dynamical Systems'. Together they form a unique fingerprint.Cite this
- APA
- Standard
- Harvard
- Vancouver
- Author
- BIBTEX
- RIS
In: IFAC-PapersOnLine, Vol. 48, No. 27, 2015, p. 267-273.
Research output: Contribution to journal › Article › peer-review
}
TY - JOUR
T1 - A Mori-Zwanzig and MITL Based Approach to Statistical Verification of Continuous-time Dynamical Systems
AU - Wang, Yu
AU - Roohi, Nima
AU - West, Matthew
AU - Viswanathan, Mahesh
AU - Dullerud, Geir E.
N1 - Funding Information: Yu Wang ∗∗,∗∗∗∗∗∗ Nima Roohi∗∗ ∗∗ Matthew Wes∗t,∗∗∗∗∗∗ Mahesh Viswanathan∗∗ Geir E. Dullerud∗,∗∗∗ Mahesh Viswanathan Geir E. Dullerud Coordinated Science Laboratory, University of Illinois at ∗∗Coordinated SUcirebnacneaL-aCbhoarmatpoaryig,nU,nUivSeArsity of Illinois at ∗ Coordinated Science Laboratory, University of Illinois at Department ofUCrobmanpau-tCerhaSmcipeanicgen, ,UUnSivAersity of Illinois at ∗∗ Urbana-Champaign, USA ∗∗ Department ofUCrobmanpau-tCerhaSmcipeanicgen, ,UUnSivAersity of Illinois at ∗∗ Department of Computer Science, University of Illinois at Department of MeUchrabnanicaa-lCShcaiemnpcaeiagnnd, UEnSgAineering, University of ∗∗∗ Urbana-Champaign, USA ∗∗∗Department oIlfliMnoeicshaatnUicarlbaSncaie-nCcheaamnpdaEignng,iUneSeAring, University of Department of Mechanical Science and Engineering, University of {yuwang8, Irlolionhoi2is, amtwUersbta, nvam-Cahheasmh,pdauigllne,ruUdS}A@illinois.edu Illinois at Urbana-Champaign, USA {yuwang8, roohi2, mwest, vmahesh, dullerud}@illinois.edu {yuwang8, roohi2, mwest, vmahesh, dullerud}@illinois.edu Abstract: In this work, we introduce a framework for the statistical verification of Metric AInbtesrtvraacltT: eImn pthoirsalwLoorgki,c w(MeITinLt)rofdorumceulaasfroanmceownotirnkuofours-tthime estdaytinsatimcailcavlesryifsitceamtios.nBoyfcMonestirdic-Abstract: In this work, we introduce a framework for the statistical verification of Metric IenritnergvtahleTecmonptoinrualoLuos-gtiicm(eMMITaLrk) ofovrmpruolcaesssonascsoonctiiantuedouws-ittihmtehedydnyanmamicaiclaslyssytesmtems. ,Bwy ecoanpspidly-Interval Temporal Logic (MITL) formulas on continuous-time dynamical systems. By consid-ethrienMg othrie-Zcwonatninzuigoumse-ttihmode MtoarrekdouvceptrhoeceosrsigaisnsaolcsiaytsetdemwtiothatCheondtyinnuaomuisc-aTlimsyestMemar,kwove Caphpailny ering the continuous-time Markov process associated with the dynamical system, we apply t(hCeTMMoCr)i.-ZAwccaonrzdiigngmlye,ththoedMtoITreLdfuocremtuhleaosroigninthael soyrsigteinmaltosyastCeomntciannuobuesr-eTdimuceeMd taorkMovITCLhfaoirn-the Mori-Zwanzig method to reduce the original system to a Continuous-Time Markov Chain (mCuTlMasCo)n. AthcecoCrTdMinCgl.yF, uthrethMerImTLorfeo,rwmeuplarsopoonstehaesotraitgisintiaclalsyvsetreimficactainonbealrgeodruitchemd tfoorMchITeLckfionrg-(CTMC). Accordingly, the MITL formulas on the original system can be reduced to MITL for-mthuelMasIoTnLtfhoermCTuMlasCo. FnutrhtheeCrmTMorCe,awnde pshroopwostehatstthaetisotricigalinvaelriMficITatLiofnoramlguolraitshomnftohrechoericgkiinnagl mulas on the CTMC. Furthermore, we propose a statistical verification algorithm for checking tshyesteMmITcLanfobremcuhleacskeodn bthyethCisTpMrCocaenddurseh.ow that the original MITL formulas on the original the MITL formulas on the CTMCand show that the original MITL formulas on the original system can be checked by this procedure. systems©ys2t0e1m5, cancIFaAnCbeb e(Icheckedcnhteercnkateidonbybaly FthistehdiesraprptrioceduroonceodfuArue.et.omatic Control) Hosting by Elsevier Ltd. All rights reserved. system can be checked by this procedure. 1. INTRODUCTION ical systems governed by ordinary differential equations 1. INTRODUCTION tcoalcosnystitneumosugso-tvimereneMdabrykoovrdcihnaairnys d(CiffTeMreCnt)iaolredquynataimonics 1. INTRODUCTION ical systems governed by ordinary differential equations Fordecades,temporallogichasbeenapowerfultoolto toayceosnitainnunoeutws-otirmksebMy parakrotivtiocnhianignsth(eCsTtMateCs)poarcedaynndamapic-ForFoesrcdecades,driebceadthese, temporaltbeemhapvoiroarls,logiclosguicchhashas beenbseaefnetyaa powerfulpanowd elrivfuelntoolteosos,l ototof tiroonxsimbyastianetworksnmgpthliengtr.aTbynhsoipartitioningtuiognhpthriosbmabeitthelhitoydstatebwetowrspacekeesnfotrhandgeepnaeap-rrtai-lpraoycontinuous-timexeismiaantinnegtwthoerktrsabnMarkovysiptiaorntiptirochainsonbinabgitliht(CTMC)eysbteattwesepeoranctedynamichaenpdaartpi-- sdteastceritbraentshiteiobnehsyavstieomrss, s(Cuclahrkaes estafaelt.y, 1a9n8d6).livFoenr efsins,itoe-f proximating the transition probability between the parti- describestate transitionthethe behaviors,behaviors, suchsuch asas safetysafety andand liveness,liveness, ofof diyooximatingnnsambyicsaalmsyptheslitnegmtransition.sT,htohuergehiprtshiobabilitynsomdeethteordmbetweenwinoirsktiscfogtherugareparti-annetreael state systems, thseytsetmemposr(aCl lloargkicefeotrmalu.,la1s9c8a6n).bFeocrhfeicnkiteed-tions by sampling. Though this method works for general statestate transitiontransition systemssystems (Clarke(Clarke etet al.,al., 1986).1986). ForFor finite-finite-onynthamebyeicrsampling.arolrsiynsttreomdsuThough,ctehdeirnetithishsisnpomethodrdoceetedrumrworksein.isticforguaranteegeneral astuattoemsyastticeamllsy, tbhyeatelmibrpaorryalolfomgiocdfoelrmchuelcaksecrasn(Mbeanchneacaknedd dynamical systems, there is no deterministic guarantee statestate systems,systems, thethe temporaltemporal logiclogic formulasformulas cancan bebe checkedchecked dynamical systems, there is no deterministic guarantee state systems, the temporal logic formulas can be checked on the error introduced in this procedure. automatically by a library of model checkers (Manna and Inn tthhies ewrroorrki,nwtreodpurocepdosine tahfirsapmroecweodrukref.or defining and Pnueli, 1992). These model checkers are roughly divided vnertihfyisinwgoarkk, iwnde porfotpeomsepoarafrlalmogeiwc oornk tfhoresdeedfiynninagmaicnadl Pnueli,tinhteosttwatoi1992).stcilcaaslseThesems:etshyommodeldbs,olbicasacheckersenddosntastaismarticpealriln,oughlyginawndhidividedcshimounllay-In this work, we propose a framework for defining and into two classes: symbolic and statistical, in which only vyesrtifyminsg. Sapekcinifdicaolfly,tewmepocroanlsliodgeirc tohne tchoensteinduyonuasm-tiimcael ttihoen,staarteistaicbalel mtoethhaondds,lebasysesdtemons soafmapllianrggeanndumsibmeruloaf-verifying a kind of temporal logic on these dynamical the statistical methods, based on sampling and simula-Myastrekmovs.pSropceecsifsiecsalglye,newreatecdonbsyidaerdytnhaemciocnatlisnyusoteums-taimnde thestitoante,statisticalsa(rYeouabnleesmethods,atondhSanimdmlebasedosnyss,t2e0mon0s6)samplingo.f a largeandnumbersimula-of systems. Specifically, we consider the continuous-time tion, are able to handle systems of a large number of takaerkmvetprricocienstseersvgael nteermatpeodrably laogdiycna(MmIiTcaLl)sytostesmpeacnifdy tion, are able to handle systems of a large number of states (Younes and Simmons, 2006). Markov processes generated by a dynamical system and statesDuring(Ytheounpastes andseveralSimmons,years,2006).various kinds of temporal takeeir mbeehtraivcioirntoevrveraltitmeme.pTohraisl ilsogdiicffe(rMenITt Lfr)otmo csuprerceinfyt states (Yoouunneess and Simmons, 2006). take metric interval temporal logic (MITL) to specify During the past several years, various kinds of temporal rheseeirarbcehheasvoinorapopvreorxtiimmaet.inTghtihseisdydnifafmereicnatl sfryosmtemcusrwreitnht During the past several years, various kinds of temporal their behavior over time. This is different from current tloiognicohfadvyenaalmsoicbaelesnysatpepmlisedwhtoertheethseyyntahreesuisseadndtovsepriefcicifay- deissecarertceh-etismoen Mapaprrkooxvimchaatiinngs t(hSeouddyjnaanmi aicnadl sAysbtaetme,s2w01it3h) logic have also been applied to the synthesis and verifica-researches on approximating the dynamical systems with dtieosnigonf doybnjeacmtiviceasl. sHyesrtee,mthsewmhearientchheayllaerneguesiesdthtaotscpheeccikfy-discrete-timeMarkovchains(SoudjaniandAbate, 2013)researches onapproximatingthedynamicalsystemswith tiontion ofof dynamicaldynamical systemssystems wherwheree theythey araree usedused toto specifyspecify discrete-time Markov chains (Soudjani and Abate, 2013) tion of dynamical systems where they are used to specify and (Wang et al., 2015). design objectives. Here, the main challenge is that check-anedu(WseanthgeeMt aol.r,i2-Z01w5a).nzig method (Chorin et al., 2000; design objectives. Here, the main challenge is that check- ing temporal logic formulas on infinite-state systems di-Weeckuseet athl.,e2M00o9r)i-sZtewmamnziinggmfreotmhotdhe(Csthuodriynoeftmaol.,de2l00re0-; crehcetclykeirss.bOeynoendpotshseibcleomwpauytatotiocnirccuampavceitnyt othfitshpermoboldemel We use the Mori-Zwanzig method (Chorin et al., 2000; rectly is beyond the computation capacity of the model duccktioent aolf.,d2y0n0a9m) sicteaml smysintegmfsrotmo rtehdeucsteutdhye ionffimniotde-esltarete-icshetockreerdsu.cOentehepodsysnibalmeiwcaalysytostecmircsutmovfiennittethstisatpertorbalnesmi-Becketal.,2009)stemmingfromthestudyofmodelre-checkers. One possible way to circumvent this problem nounctliionneaorfddyynnaammiiccaall ssyysstteemmsintotoreCdTuMceCt.heNiontfiinngiteth-sattatiet checkers.tisiotnosryesdteumcOneestbhyepossibleadbysntraamctiiwaycoanl-bsyatossteecirdmmcumventsettohfoidnsite(thisTsatbautpreadtoblemraaannsid-ductionofdynamicalsystemstoreducetheinfinite-state is to reduce the dynamical systems to finite state transi-uosunalilnlyeanreeddysnaamlaircgael nsuymstebmer oinftdoisCcTreMteCs.taNteosttinogapthparot xi-t Ptiaopnpsayss,te2m00s6b; yKalobesttzraecrtiaonnd-bBaesletda,m20e0th8o; dWso(nTagbpuiraodmasaanrdn nonlinear dynamical system into CTMC. Noting that it tion systems by abstraction-based methods (Tabuada and imsuaatellya nceoendtisnauloaurgs ednoummaibne,rwofedaidscorpettethsteatsetsattiostaicpaplraopx--ePtaaplp.,a2s0,1200)0.6H;oKwloeevtezre,rfiannddinBgesltuac,h20a0n8a;bWstornacgtpioirnomisscaurrn-usuallyneedsalargenumberofdiscretestatestoapprox-Pappas, 2006; Kloetzer and Belta, 2008; Wongpiromsarn pmroaatechatococnhteicnkutohuesCdToMmCaind,erwiveeaddaonpdt pthreesestnattaisctiocnacl raepte-Pappas,reetnatll.y,2o0n12006;l0y).pHosoKloetzerswibelveefro,rfiandsnpdeicniBelta,gficsuclcahs2008;saensaobfWsdtoorynnancggatppimoiirrniomsarncaislcsyusr-imate a continuous domain, we adopt the statistical ap- et al., 2010). However, finding such an abstraction is cur-alrgooarcihthtmo cthoemckotdheelCchTeMckCMdeITriLvefdoramnudlpasr.esent a concrete treemntsly, sounclhyapsolisnseibalretfimores-pinevcaifriicacnltassysestseomfsdaynndampiieccaelwsyisse-proach to check the CTMC derived and present a concrete rently only possible for specific classes of dynamical sys-algorithm to model check MITL formulas. atefmfinse,ssuycshteamssli.neartime-invariantsystemsandpiecewise TlhgeorreitshtmofttohmepoadpeelrchiseockrgManIiTzLedfoarsmfoulllaosw. s.InSection2, tems, such as linear time-invariant systems and piecewise tems,affinesuchsystems.as linear time-invariant systems and piecewise thheeprersetliomfitnhaerpieaspaenr dis othrgeamniaztehdemasaftoicllaolwfos.rmInuSleactitoionno2f, Afnfiontehseyrsitdemeas.is to convert the dynamical systems into The rest of the paper is organized as follows. In Section 2, the pprroelbimleminaarriesgaivnedn.thIne mSeactthioenma3t,icthale fMoromriu-Zlawtioannzoigf pArnoobtahbeirlisidtiecafinisitetostcaotnevtrearnt stihtieondysynsatmemicsalbassyesdteomnssianmto-the preliminaries and the mathematical formulation of Another idea is to convert the dynamical systems into theethporodbilseumseadretogrievdeunc.eIntheSeMctaiorkno3v,ptrhoeceMssotroi-aZwCTanMzCig. Anotherpplrionbgabainlidsideatiscimfinuisiltaetotisotconvertnat.eIntra(nLsitheuitioetndynamicalasly.,st2e0m11s,b2asystems0s1ed2;oZnuslintoaiamn-i the problem are given. In Section 3, the Mori-Zwanzig probabilistic finite state transition systems based on sam-Acectohroddinisgulys,etdhetoMreIdTuLcfeotrhmeuMlaasrkoonvthperoocreisgsintoalaMCaTrMkoCv. preptliobabilisticanlg., 2a0n1d3;sZimufiniteluialantiistate,o2n0.1I4ntransition),(tLhieuauetthasystemsol.r,s2r0e1d1u,basedc2e0t1h2e;ondZyunsam-laiamn-i method is used to reduce the Markov process to a CTMC. plingandsimulation.In(Liuetal.,2011,2012;Zuliani Arcoccoersdsiensgalyre,trheeduMceITdLtofoMrmITuLlafosromnutlhaesoonrigthineaClTMMaCrk.oInv et al., 2013; Zuliani, 2014), the authors reduce the dynam-Accordingly, the MITL formulas on the original Markov e1tal.,2013;Zuliani,2014),theauthorsreducethedynam-adrodcietisosne,swaregreivdeucthedetbooMunIdTsLofofremrruolraisnotrnotdhuecCedTMbyC.thIne processes are reduced to MITL formulas on the CTMC. In 1et13T9h9e9a1u.thorsacknowledgesupportforthisworkfromNSFCPSgrantTaahlle..,,a22u00th11o33r;;sZZacuukllniioaawnniile,,d22g00e11s44u))p,,pthoretfaaouurttthhhioosrrwssorreekddfruuoccmeeNtthhSFeeCddPyySnngaarmman--taeddduitcitoionn,.wIneSgeivcteiotnhe4,bwouenpdressoenftearrsotratiinsttricoadluvceerdifibcyatitohne 1 addition, we give the bounds of error introduced by the 1 The authors acknowledge support for this work from NSF CPS grant addition, we give the bounds of error introduced by the 1329991. reduction. In Section 4, we present a statistical verification 1329991.1329991. reduction. In Section 4, we present a statistical verification Publisher Copyright: © 2015, IFAC (International Federation of Automatic Control) Hosting by Elsevier Ltd. All rights reserved.
PY - 2015
Y1 - 2015
N2 - In this work, we introduce a framework for the statistical verification of Metric Interval Temporal Logic (MITL) formulas on continuous-time dynamical systems. By considering the continuous-time Markov process associated with the dynamical system, we apply the Mori-Zwanzig method to reduce the original system to a Continuous-Time Markov Chain (CTMC). Accordingly, the MITL formulas on the original system can be reduced to MITL formulas on the CTMC. Furthermore, we propose a statistical verification algorithm for checking the MITL formulas on the CTMCand show that the original MITL formulas on the original system can be checked by this procedure.
AB - In this work, we introduce a framework for the statistical verification of Metric Interval Temporal Logic (MITL) formulas on continuous-time dynamical systems. By considering the continuous-time Markov process associated with the dynamical system, we apply the Mori-Zwanzig method to reduce the original system to a Continuous-Time Markov Chain (CTMC). Accordingly, the MITL formulas on the original system can be reduced to MITL formulas on the CTMC. Furthermore, we propose a statistical verification algorithm for checking the MITL formulas on the CTMCand show that the original MITL formulas on the original system can be checked by this procedure.
UR - http://www.scopus.com/inward/record.url?scp=84983115069&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84983115069&partnerID=8YFLogxK
U2 - 10.1016/j.ifacol.2015.11.186
DO - 10.1016/j.ifacol.2015.11.186
M3 - Article
AN - SCOPUS:84983115069
SN - 2405-8963
VL - 48
SP - 267
EP - 273
JO - IFAC-PapersOnLine
JF - IFAC-PapersOnLine
IS - 27
ER -