Abstraction refinement for stability

Parasara Sridhar Duggirala, Sayan Mitra

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

Abstract

The paper presents a CEGAR-based procedure for verifying stability (region stabillity) of CPS modeled as hybrid automata. It relies a characterization of the blocking property of hybrid automata in terms of well-foundedness of a relation that combines the discrete transitions and continuous trajectories and a key assumption about the switching speed of the system in terms of average dwell time, but does not require the individual modes to be stable. This characterization enables the adaptation of program analysis techniques in the domain of hybrid systems. It is shown that the procedure is complete for rectangular initialized hybrid automata. Several illustrative examples are verified using a prototype tool that implements the methodology.

Original languageEnglish (US)
Title of host publicationProceedings - 2011 IEEE/ACM 2nd International Conference on Cyber-Physical Systems, ICCPS 2011
Pages22-31
Number of pages10
DOIs
StatePublished - Aug 10 2011
Event2011 IEEE/ACM 2nd International Conference on Cyber-Physical Systems, ICCPS 2011 - Chicago, IL, United States
Duration: Apr 12 2011Apr 14 2011

Publication series

NameProceedings - 2011 IEEE/ACM 2nd International Conference on Cyber-Physical Systems, ICCPS 2011

Other

Other2011 IEEE/ACM 2nd International Conference on Cyber-Physical Systems, ICCPS 2011
CountryUnited States
CityChicago, IL
Period4/12/114/14/11

Keywords

  • Cyber-Physical Systems
  • Hybrid Systems
  • Region Stability
  • Stability
  • Termination
  • Well-Founded Relations

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Abstraction refinement for stability'. Together they form a unique fingerprint.

Cite this