Show simple item record

dc.contributor.authorNavarro-López, EM
dc.contributor.authorCarter, R
dc.date.accessioned2021-02-17T10:31:20Z
dc.date.available2021-02-17T10:31:20Z
dc.date.issued2016-06-16
dc.identifier.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.en
dc.identifier.issn0304-3975en
dc.identifier.doi10.1016/j.tcs.2016.06.009en
dc.identifier.urihttp://hdl.handle.net/2436/623937
dc.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.009en
dc.description.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.en
dc.description.sponsorshipThis 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.en
dc.formatapplication/pdfen
dc.languageen
dc.language.isoenen
dc.publisherElsevieren
dc.relation.ispartofseriesdiscontinuous systemsen
dc.relation.urlhttps://www.sciencedirect.com/science/article/pii/S0304397516302456?via%3Dihub#!en
dc.subjecthybrid systemsen
dc.subjectlivenessen
dc.subjectstability analysisen
dc.subjecthybrid automataen
dc.titleDeadness and how to disprove liveness in hybrid dynamical systemsen
dc.typeJournal articleen
dc.identifier.journalTheoretical Computer Scienceen
dc.date.updated2021-02-15T16:15:49Z
dc.date.accepted2016-06-10
rioxxterms.funderEngineering and Physical Sciences Research Councilen
rioxxterms.identifier.projectEP/I001689/1en
rioxxterms.identifier.projectEP/E50048/1en
rioxxterms.versionVoRen
rioxxterms.licenseref.urihttps://creativecommons.org/licenses/by/4.0/en
rioxxterms.licenseref.startdate2021-02-17en
dc.source.volume642
dc.source.beginpage1
dc.source.endpage23
dc.description.versionPublished version
refterms.dateFCD2021-02-17T10:30:47Z
refterms.versionFCDVoR
refterms.dateFOA2021-02-17T10:31:21Z


Files in this item

Thumbnail
Name:
Publisher version
Thumbnail
Name:
Navarro-Lopez_Deadness_2016.pdf
Size:
1.937Mb
Format:
PDF

This item appears in the following Collection(s)

Show simple item record

https://creativecommons.org/licenses/by/4.0/
Except where otherwise noted, this item's license is described as https://creativecommons.org/licenses/by/4.0/