Deadness and how to disprove liveness in hybrid dynamical systems
Name:
Publisher version
View Source
Access full-text PDFOpen Access
View Source
Check access options
Check access options
Abstract
What if we designed a tool to automatically prove the dynamical properties of systems for which analytic proof is difficult or impossible to obtain? Such a tool would represent a significant advance in the understanding of complex dynamical systems with nonlinearities. This is precisely what this paper offers: a solution to the problem of automatically proving some dynamic stability properties of complex systems with multiple discontinuities and modes of operation modelled as hybrid dynamical systems. For this purpose, we propose a reinterpretation of some stability properties from a computational viewpoint, chiefly by using the computer science concepts of safety and liveness. However, these concepts need to be redefined within the framework of hybrid dynamical systems. In computer science terms, here, we consider the problem of automatically disproving the liveness properties of nonlinear hybrid dynamical systems. For this purpose, we define a new property, which we call deadness. This is a dynamically-aware property of a hybrid system which, if true, disproves the liveness property by means of a finite execution. We formally define this property, and give an algorithm which can derive deadness properties automatically for a type of liveness property called inevitability. We show how this algorithm works for three different examples that represent three classes of hybrid systems with complex behaviours.Citation
Navarro-López, E.M. and Carter, R. (2016) Deadness and how to disprove liveness in hybrid dynamical systems. Theoretical Computer Science, 642, pp. 1-23.Publisher
ElsevierJournal
Theoretical Computer ScienceType
Journal articleLanguage
enDescription
© 2016 The Authors. Published by Elsevier. This is an open access article available under a Creative Commons licence. The published version can be accessed at the following link on the publisher’s website: https://doi.org/10.1016/j.tcs.2016.06.009Series/Report no.
discontinuous systemsISSN
0304-3975Sponsors
This work has been supported by the Engineering and Physical Sciences Research Council (EPSRC) of the UK under the framework of the project DYVERSE: A New Kind of Control for Hybrid Systems (EP/I001689/1). The first author also acknowledges the support of the Research Councils UK under the grant EP/E50048/1.ae974a485f413a2113503eed53cd6c53
10.1016/j.tcs.2016.06.009
Scopus Count
Collections
Except where otherwise noted, this item's license is described as https://creativecommons.org/licenses/by/4.0/