Loading...
Deadness and how to disprove liveness in hybrid dynamical systems
Carter, R
Carter, R
Authors
Editors
Other contributors
Affiliation
Epub Date
Issue Date
2016-06-16
Submitted date
Files
Alternative
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
Journal
Research Unit
PubMed ID
PubMed Central ID
Embedded videos
Type
Journal article
Language
en
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
ISSN
0304-3975
EISSN
ISBN
ISMN
Gov't Doc #
Sponsors
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.