Deadness and how to disprove liveness in hybrid dynamical systems

A simulation of the chaotic attractor of a hybrid automaton

Deadness and how to disprove liveness in hybrid dynamical systems

Authors: Eva M. Navarro-López, Rebekah Carter

Journal: Theoretical Computer Science

Publication Date: 23 August, 2016

In Abstract

On the mutual interdependence of life and death in novel theoretical computer science terms

Hybrid dynamical systems are systems that combine continuous and discrete, smooth and abrupt dynamics. They have been studied over the last twenty years as so-called ‘2-C science’ (meaning Computation-Control). Recently, they have evolved to cyber-physical systems and can now be regarded as 3-C science (Computation-Control-Communication).

Due to the discontinuous changes in states, hybrid systems entail complex behaviours not present in systems that are purely discrete or continuous. These ‘complex behaviours’ usually lead to faults. What if we designed a tool to automatically prove dynamical behaviours of these systems for which analytic proof is difficult or impossible to obtain? Such a tool would represent a significant advance in the understanding of complex systems. Computer Scientists at the University of Manchester have now achieved precisely this – a solution to the problem of automatically proving some dynamic properties of hybrid systems modelled as hybrid automata. For this, a computational reinterpretation of these dynamic properties is given, chiefly by defining for the first time the well-known properties in computer science of liveness and deadness for nonlinear hybrid automata.

This framework is general and applicable to a broad class of systems subject to different types of interactions with their environment: from neuronal networks to smart grids; from electromechanical systems to cybersecurity.

This work is informed by two insights: Cicero’s aphorism that “While there’s life, there’s hope” and, following the Mexican tradition, the mutual interdependence of life and death. An awareness of death only sharpens our appetite for life, and makes it more bearable. This paper formalises these insights in theoretical computer science terms, and advances the well-defined liveness properties used in computer science, but within the framework of hybrid dynamical systems.
What do you think is easier: to prove that ‘something bad will never happen’ or to prove that ‘something good will eventually happen’? Proving that ‘something good will eventually happen’ is difficult, and it is even harder to do so in an automated way. In computer science, this type of property is usually called ‘liveness’. This research led by a team of researchers from the School of Computer Science in The University of Manchester has found a shortcut for automatically proving ‘liveness’ properties in complex dynamical systems. If it is so hard to prove a liveness property, why don’t we disprove it? This is the concept of deadness, which captures the idea that there could exist another property which, if it is true, implies that the liveness property can never hold in the system: ‘if a system is dead it can never be live again’. This idea has important implications for the analysis of key properties of complex dynamical systems.
The process of checking in an automated way that a system behaves correctly is called ‘formal verification’ in the theory of computer science. This paper represents a paradigm shift in automated verification because a dynamically-driven verification method is proposed, by which it is meant that the way the method works is guided by properties of the dynamics of the hybrid automata. An automaton is a computational abstraction of the transitions of a system between discrete states or locations (on and off, for instance). A hybrid automaton, additionally, considers dynamical evolution in each location.

Click here to read the full article - DOI link: http://www.sciencedirect.com/science/article/pii/S0304397516302456

Links:

Project DYVERSE

Footnotes

This research 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.