Cyber-physical systems (CPS) are systems of collaborating computational elements controlling physical entities. Composition of continuous and discrete models is essential for capturing the behaviour of such systems. Verification and synthesis of CPS are algorithmically studied using abstraction techniques and model checking tools. The goal of this research is to focus on formal verification and controller synthesis of CPS models by addressing robustness and scalability of the algorithms, while taking uncertainty into account, utilising available data from the system and synthesising optimal controllers.
Qualitative modelling techniques have become increasingly important in biology as the basis for developing formal techniques and tools for modelling, analysing and synthesizing biological systems. Multi-valued networks are a widely used qualitative approach based on representing the state of each entity using a range of discrete values. They have been successfully applied in the literature to model and analyse complex biological systems such as gene regulatory networks. However, their application is limited by the well-known state space explosion which means that modelling and analysing large-scale, realistic regulatory systems is challenging.
Group theory interacts with computation in a variety of ways. In this project, we describe two related strands within this theme: equations in groups; and automatic groups and their generalizations.
When G= < X > is a finitely generated group, the word problem is soluble for G if an algorithm exists that, given any product w of elements of X and their inverses, can determine whether or not w represents the identity element.
Graphs (composed of vertices and edges) are ubiquitous not only in Computer Science and Mathematics but across the whole spectrum of Science and Engineering. They are used to abstractly model many diverse real-world systems, where vertices and edges represent elementary system units and some kind of interactions between them, respectively. However, in modern systems this modeling paradigm using static graphs may be restrictive or oversimplifying, as the interactions among entities usually change over time in a highly dynamic manner.
Positive semidefinite matrices play in important role in semidefinite programming for optimisation problems. An aspect of their study concerns the completion of a matrix, whose only partially entries are known, to a positive one by using undirected finite graphs. A fundamental question involves the characterisation of all such graphs which give rise to a positive completion. Related research includes studying positive completion problems that correspond to Hankel and Toeplitz structure with a number of rich applications on orthogonal polynomials, moment problems and Schur analysis.
With the increasing deployment of smart grid infrastructures, power systems operations and electricity markets are changing. Instead of electricity supply following demand, portions of demand can be manipulated to fit the current supply levels. Such demand-side elasticity is facilitated via demand response (DR) programs, in which the electricity usage by end-use customers changes from their normal consumption patterns in response to the variations in the price of electricity over time.
How curvy is Facebook? When we think of curvature, we usually think of smooth objects like Riemannian manifolds. Recently, however, discrete optimal transport theory has been used to introduce a notion of Ricci curvature for graphs and Markov chains. This new curvature notion, called Ollivier-Ricci curvature, has been used to model the internet, wireless networks, and financial markets. Just like for Riemannian manifolds, a positive lower bound on the Ollivier-Ricci curvature of a graph gives an upper bound on the diameter of the graph (Bonnet-Myers Theorem), which means that local curvature information can be used to estimate the global size of a network.
Random walks are fundamental models in probability theory that exhibit deep mathematical properties and enjoy broad application across the sciences and beyond. By executing a series of random steps, the random walker describes a trajectory in space. Of interest are the geometrical characteristics of this trajectory, such as its convex hull (the smallest convex set enclosing the trajectory), or the centre of mass of the trajectory. The object of this project is to study such objects in the limit as the number of steps of the walk tends to infinity.
Major scientific advances can be made from the synergy between Dynamical Systems, Combinatorics, Operator Algebras and Topology. Dynamical systems, which originated in Newtonian Mechanics, has evolved to a much wider context, and is ideally placed to study systems in which information is processed via one or more “time” dependencies.
Current research has shown there are natural representations of such processes as topological (“moduli” or “state”) spaces, as operator algebras and as combinatorial or “symbolic”
Phylogenetic trees represent evolutionary relationships between organisms, and they are fundamental to many applications in molecular biology. Phylogenies are usually inferred by analysing DNA sequence data. Typically, each analysis can produce many different plausible trees, and these will vary between different analyses. Understanding the structure of such samples of trees, and evaluating underlying assumptions and biases in bioinformatic methods, requires techniques for assessing similarities and differences between trees.
While several measures of similarity between trees exist, these are somewhat arbitrary in nature.