Tutorial: Software Tools for Hybrid Systems Verification, Transformation, and Synthesis: C2E2, HyST, and TuLiP (bibtex)

by Parasara Sridhar Duggirala, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, Sergiy Bogomolov, Taylor T. Johnson, Luan Viet Nguyen, Christian Schilling, Andrew Sogokon, Hoang-Dung Tran, Weiming Xiang

Reference:

Parasara Sridhar Duggirala, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, Sergiy Bogomolov, Taylor T. Johnson, Luan Viet Nguyen, Christian Schilling, Andrew Sogokon, Hoang-Dung Tran, Weiming Xiang, "Tutorial: Software Tools for Hybrid Systems Verification, Transformation, and Synthesis: C2E2, HyST, and TuLiP", In Proceedings of the IEEE Multi-Conference on Systems and Control (MSC 2016), Las Vegas, NV, USA, 2016, sep.

Bibtex Entry:

@inproceedings{duggirala2016msc, author = {Parasara Sridhar Duggirala and Chuchu Fan and Matthew Potok and Bolun Qi and Sayan Mitra and Mahesh Viswanathan and Stanley Bak and Sergiy Bogomolov and Taylor T. Johnson and Luan Viet Nguyen and Christian Schilling and Andrew Sogokon and Hoang-Dung Tran and Weiming Xiang}, title = {Tutorial: Software Tools for Hybrid Systems Verification, Transformation, and Synthesis: C2E2, HyST, and TuLiP}, year = {2016}, booktitle = {Proceedings of the IEEE Multi-Conference on Systems and Control (<a href="http://www.msc2016.org/">MSC 2016</a>)}, address = {Las Vegas, NV, USA}, month = sep, # pages = {2687--2692}, # gsid = {14666544104064248628}, # doi = {10.1109/CDC.2011.6161264}, # abstract = {A sufficient condition for stability of linear subsystems interconnected by digitized signals is presented. There is a digitizer for each linear subsystem that periodically samples an input signal and produces an output that is quantized and saturated. The output of the digitizer is then fed as an input (in the usual sense) to the linear subsystem. Due to digitization, each subsystem behaves as a switched affine system, where state-dependent switches are induced by the digitizer. For each quantization region, a storage function is computed for each subsystem by solving appropriate linear matrix inequalities (LMIs), and the sum of these storage functions is a Lyapunov function for the interconnected system. Finally, using a condition on the sampling period, we specify a subset of the unsaturated state space from which all executions of the interconnected system reach a neighborhood of the quantization region containing the origin. The sampling period proves to be pivotal---if it is too small, then a dwell-time argument cannot be used to establish convergence, while if it is too large, an unstable subsystem may not receive timely-enough inputs to avoid diverging.}, # issn = {0743-1546}, pdf = {http://www.taylortjohnson.com/research/duggirala2016msc.pdf}, }

Powered by bibtexbrowser