@inproceedings{82fc94e42e574242be606094016e34af,
title = "Abstraction refinement for stability",
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.",
keywords = "Cyber-Physical Systems, Hybrid Systems, Region Stability, Stability, Termination, Well-Founded Relations",
author = "Duggirala, {Parasara Sridhar} and Sayan Mitra",
year = "2011",
doi = "10.1109/ICCPS.2011.24",
language = "English (US)",
isbn = "9780769543611",
series = "Proceedings - 2011 IEEE/ACM 2nd International Conference on Cyber-Physical Systems, ICCPS 2011",
pages = "22--31",
booktitle = "Proceedings - 2011 IEEE/ACM 2nd International Conference on Cyber-Physical Systems, ICCPS 2011",
note = "2011 IEEE/ACM 2nd International Conference on Cyber-Physical Systems, ICCPS 2011 ; Conference date: 12-04-2011 Through 14-04-2011",
}