MARC

 008250123s2024        us                              c    eng  d
■001000017161395
■00520250211151350
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798382830575
■035    ▼a(MiAaPQ)AAI31243131
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a621.3
■1001  ▼aCleaveland,  Matthew.
■24510▼aScalable  and  Risk-Aware  Verification  of  Learning  Enabled  Autonomous  Systems
■260    ▼a[Sl]▼bUniversity  of  Pennsylvania▼c2024
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2024
■300    ▼a235  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  85-12,  Section:  B.
■500    ▼aAdvisor:  Lee,  Insup;Pappas,  George  J.
■5021  ▼aThesis  (Ph.D.)--University  of  Pennsylvania,  2024.
■520    ▼aAs  autonomous  systems  become  more  prevalent,  ensuring  their  safety  will  become  more  and  more  important.  However,  deriving  guarantees  for  these  systems  is  becoming  increasingly  difficult  due  to  the  use  of  black  box,  learning  enabled  components  and  the  growing  range  of  operating  domains  in  which  they  are  deployed.  The  complexity  of  the  learning-enabled  components  greatly  increases  the  computational  complexity  of  the  verification  problem.  Additionally,  the  safety  predictions  from  verifying  these  systems  must  be  conservative.  This  thesis  explores  two  high-level  methods  for  verifying  autonomous  systems:  probabilistic  model  checking  and  statistical  model  checking.  Probabilistic  model  checking  methods  exhaustively  analyze  a  model  of  the  system  to  reason  about  its  properties.  These  methods  generally  suffer  from  scalability  issues,  but  if  the  abstraction  is  built  correctly  then  the  results  will  be  provably  conservative.  On  the  other  hand,  statistical  model  checking  methods  draw  traces  from  the  system  to  reason  about  its  properties.  These  methods  don't  suffer  the  scalability  drawback  of  probabilistic  model  checking,  but  their  guarantees  are  weaker  and  may  not  even  be  conservative.  This  thesis  introduces  methods  for  improving  the  scalability  of  verifying  autonomous  systems  with  probabilistic  model  checking  methods  and  incorporating  notions  of  conservatism  into  statistical  model  checking. On  the  probabilistic  model  checking  side,  this  thesis  first  explores  using  engineering  intuitions  about  systems  to  reduce  probabilistic  model  checking  complexity  while  preserving  conservatism.  Next,  standard  conservative  probabilistic  model  checking  techniques  are  used  to  synthesize  runtime  monitors  that  are  conservative  and  lightweight.  Finally,  this  thesis  presents  a  run-time  method  for  composing  monitors  of  verification  assumptions.  Verification  assumptions  are  critical  for  simplifying  verification  problems  so  that  they  become  computationally  feasible.For  statistical  model  checking,  this  thesis  first  leverages  a  method  called  conformal  prediction  to  bound  the  errors  of  trajectory  predictors,  which  enables  safe  (i.e.  conservative)  planning  in  dynamic  environments.  Additionally,  a  method  for  producing  less  conservative  conformal  prediction  regions  in  time  series  settings  is  developed.  Then  a  method  called  risk  verification  is  developed,  which  uses  statistical  methods  to  bound  risk  metrics  of  a  system's  performance.  Risk  metrics,  which  capture  tail  events  of  the  system's  performance,  offer  a  statistical  equivalent  of  worst  case  analysis.
■590    ▼aSchool  code:  0175.
■650  4▼aElectrical  engineering
■650  4▼aComputer  science
■650  4▼aComputer  engineering
■650  4▼aStatistics
■650  4▼aSystems  science
■653    ▼aAutonomous  systems  
■653    ▼aComputational  complexity
■653    ▼aScalability  issues
■653    ▼aProbabilistic  model  
■653    ▼aDynamic  environments
■690    ▼a0544
■690    ▼a0984
■690    ▼a0464
■690    ▼a0463
■690    ▼a0790
■71020▼aUniversity  of  Pennsylvania▼bElectrical  and  Systems  Engineering.
■7730  ▼tDissertations  Abstracts  International▼g85-12B.
■790    ▼a0175
■791    ▼aPh.D.
■792    ▼a2024
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17161395▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

미리보기

내보내기

chatGPT토론

Ai 추천 관련 도서