Deadness and how to disprove liveness in hybrid dynamical systems
AbstractWhat 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.
CitationNavarro-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.
JournalTheoretical Computer Science
Description© 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.009
Series/Report no.discontinuous systems
SponsorsThis 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.
Except where otherwise noted, this item's license is described as https://creativecommons.org/licenses/by/4.0/