[University home]

School of Computer Science

DYVERSE framework


DYVERSE represents a fresh perspective within the theory of hybrid systems and dynamical systems in general, and provides new insights into the modelling, analysis and control of systems with switching dynamics and complex behaviours.

DYVERSE is a computational dynamical framework for the modelling, analysis and control of complex control systems.

DYVERSE is the DYnamical-driven VERification of Systems with Energy considerations. By energy, we refer to abstract energy which may not have a physical interpretation. The formalization of the abstract energy of dynamical systems is achieved by means of dissipativity theory, which analyses dynamical systems behaviour by means of the exchange of energy with the environment.

DYVERSE goes beyond the control and verification of discontinuous and switched systems. It is a long-term research to extend the results on analysis and control of hybrid systems to complex networks and distributed systems. What it is more important, DYVERSE integrates our vision of Science.

Which framework?

DYVERSE is presented under the framework of the EPSRC-funded project DYVERSE: A New Kind of Control for Hybrid Systems. I am the principal investigator of DYVERSE. This project naturally arises from my previous work and falls within the boundaries of control engineering, computer science and dynamical systems theory.

DYVERSE is to be combined with the work in automated formal verification headed by Prof. Lawrence Paulson from the Computer Laboratory in Cambridge in the EPSRC-funded project Automatic Proof Procedures for Polynomials and Special Functions.


We are a group of enthusiastic, energetic and dynamic people, with literally diverse backgrounds:

e-mail message


It might be as simple as jumping on a trampoline, or as sophisticated as the docking of vehicles in outer space; as trivial as playing billiards, or as crucial as maintaining the stability of an airplane during landing; as random as the flow of information in a communication network, or as synchronised as a school of fish swimming in the sea. These are examples of systems that combine continuous and discrete, smooth and abrupt dynamics. In dynamical systems theory, this is called discontinuity or switching behaviour. The systems exhibiting it are called discontinuous, switched, non-smooth or discrete-event systems. Their combined dynamics can be seen as a hybrid dynamical system.

What makes the behaviour of hybrid systems so complex? Where does the unpredictable behaviour of these systems come from: from the system itself, or from its environment? Every mathematical model is an approximation of the real world, and is full of limitations. However, some models are better than others at describing the evolution of certain physical and engineering systems. DYVERSE proposes a fresh perspective within the hybrid systems framework, and will provide new insights into the modelling, analysis and control of systems with switching dynamics.

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 or dynamics degrading performance. Chaos or mechanical vibrations are examples of these kinds of negative dynamics. Complex behaviours usually have their origin in what in mathematical terms is known as a bifurcation. That is, the point which marks a change. The challenge is to ensure through design that devices behave correctly, eliminating all negative behaviour.

The process of checking in an automated way that a system behaves correctly is called 'formal verification' in the theory of computer science; the elimination of negative behaviours falls into the field of control engineering. DYVERSE brings together computer science formal methods, dynamical systems analysis and control engineering methodologies. The research mixes theory and practice and crosses different application domains, which is why the project is quite literally diverse.

There has been great success in applying formal verification methods to validate dynamical properties in particular classes of discontinuous systems. However, it is still a challenge to give satisfactory solutions for the verification of complex dynamical behaviours of discontinuous systems, as DYVERSE proposes. One of the main obstacles has been the difficulty of obtaining a computational representation of these complex dynamical properties. Consideration of the changes of the energy of the system is the answer to this problem. But DYVERSE is not only about formal verification: DYVERSE will use the verification results to modify and improve the system behaviour. Furthermore, it will bring new theory into practice.

An integral part of the project is that the theoretical results will be experimentally validated in an electromechanical prototype: a system with impacts and friction. A system with impacts and friction is a discontinuous system because it evolves smoothly until an event (impact/friction) triggers changes in the velocities or position.

Would you like to work with us in DYVERSE?

If you think that we have common interests and can learn together, please, contact me.