Projects

Expand All

This research concerns quantitative model checking of complex probabilistic models encompassing continuous/discrete dynamics, nondeterminism, and control inputs. Such models are often categorised within a class known as Stochastic Hybrid Systems (SHS), which is recognised as the theoretical underpinning for applications in the Cyber-Physical Systems (CPS) domain. This research works towards formally bridging Verification, Control Theory, and Stochastic Processes.    

The computation of quantitative properties and the synthesis of related control architectures optimising properties of interest, is attained via the development of abstraction techniques based on quantitative approximations. This abstraction approach employs methods and concepts from the formal verification area, such as that of (approximate probabilistic) bisimulation, over models and problems known in the field of systems and control. Theory is complemented by algorithms, all packaged software tools that are freely available to users. 

Themes: Stochastic Hybrid Systems, Automated Verification, Probabilistic Model Checking

People: Licio Romao, Francesco Cosentino, Yulong Gao, Nathalie Cauchi, Sofie Haesaert, Sadegh Soudjani, Alessandro Abate

Software:  StocHy, FAUST2

Recent Publications:

Reinforcement Learning (RL) is a known architecture for synthesising policies for Markov Decision Processes (MDP). We work on extending this paradigm to the synthesis of ‘safe policies’, or more general of policies such that a linear time property is satisfied. We convert the property into an automaton, then construct a product MDP between the automaton and the original MDP. A reward function is then assigned to the states of the product automaton, according to accepting conditions of the automaton. With this reward function, RL synthesises a policy that satisfies the property: as such, the policy synthesis procedure is `constrained' by the given specification. Additionally, we show that the RL procedure sets up an online value iteration method to calculate the maximum probability of satisfying the given property, at any given state of the MDP. We evaluate the performance of the algorithm on numerous numerical examples.

 

Themes:  Learning and Verification

People:  Licio Romao, Lewis Hammond, Joar Skalse, Hosein Hasanbeig, Kyriakos Polymenakos, Alessandro Abate

 

Publications:

Max-PlusLinear (MPL) models are a class of discrete-event systems used to characterize the dynamics of the timing related to successive events that synchronize autonomously. Nonautonomous versions of MPL models embed within their dynamics nondeterminism, namely a signal choice that is usually regarded as an exogenous control or schedule.

 

Abstractions of MPL models are characterized as finite-state Labeled Transition Systems (LTS). LTS are obtained first by partitioning the state space (and, for the nonautonomous model, by covering the input space) of the MPL model and by associating states of the LTS to the introduced partitions, then by defining relations among the states of the LTS based on dynamical transitions between the corresponding partitions of the MPL state space, and finally by labeling the LTS edges according to the one-step timing properties of the events of the original MPL model.

Themes:  Max-plus Linear Systems

People:  Muhammad Syifa'ul Mufid, Alessandro Abate

Software:  VeriSiMPL

Publications:

We are interested in applications of and algorithmic improvements to CounterExample Guided Inductive Synthesis (CEGIS). We are exploring and developing the use of different learning and verification techniques within the CEGIS architecture, and have an upcoming paper at CAV 2018 on CEGIS(T), a CEGIS algorithm that incorporates theory solvers for improved synthesis of constants.We are also interested in the application of the CEGIS paradigm to a broad range of applications, and have several recent works focusing on the application of CEGIS to the synthesis of safe controllers for Linear-Time-Invariant systems.

 

Themes:  Program Synthesis

People:  Alec Edwards, Mirco Giacobbe, Andrea Peruffo, Elizabeth Polgreen, Dario Cattaruzza, Alessandro Abate

Software: FOSSIL, DSSynth

 

Publications:

Complex engineering systems, such as autonomous vehicles, are often safety-critical and demand high guarantees of correctness. Given a complete model of the system of interest, these guarantees can be obtained through formal methods, such as model checking, though the outcomes of these formal proofs are bound to the model of the system of interest. Obtaining a complete model is not possible for systems with uncertain stochastic dynamics, but we can capture these dynamics with parameterised Markov chains. Model checking now produces a result dependent on knowledge of the value of parameters within the model.

In this work we integrate the use of model checking techniques (for parameter synthesis over the model) with data-based approaches (for parametric Bayesian inference) in order to compute a confidence, based on observed data collected from the system, that the system satisfies a given specification.

Themes:  Bayesian Learning and Verification

People:  Viraj Wijesuriya, Gareth Molyneux, Alessandro Abate

Publications:

The future is smart: smart meters, smart buildings, smart cities. Digital technologies integrated into everyday life will give us and our descendants an environmentally sustainable and comfortable life. Automation is key: devices capable of self-diagnosing faults and send reports to the maintenance team; offices able to decide the best environment needed for your work; cities that manage the power demand to allow only clean energy use.  

Our research focuses on multi-layered aspects of energy systems and networks: industrial building automation systems (a.k.a. Smart Buildings) and smart home metering, optimisation and reliability of smart grids, and renewables (solar panels) integration over the power grid.  

 

  • Building Automation Systems aim to deliver useful building services that are cost-effective, reliable and ensure occupant comfort and productivity (thermal quality, air comfort). Our aim is to develop and design a library of models using the knowledge garnered from data collected within the Smart Buildings Laboratory at the Department of Computer Science. From these models, we are developing a tool which controls the building automation system's performance, pro-actively detects faults and performs predictive maintenance actions in order to increase the life-span of the system. 

 

  a

 

 

  • Decarbonisation of Homes using Probabilistic Models and Smart Meter Data. Residential homes represent approximately 22% of global energy use and a large proportion of this is due to space heating. The thermal efficiency of a building is typically evaluated manually via surveys, or via intrusive measurements requiring homes to be vacated for prolonged periods, which is inconvenient and expensive. We develop non-intrusive methods to infer the thermal efficiency of a home: they can identify where interventions, such as installing insulation, will have the greatest impact in reducing heating energy usage and carbon emissions. We blend techniques from data-driven learning and model-based synthesis. 

 

  • Solar panels are spreading worldwide, millions are installed on the European roofs. When the energy is not self-consumed, it is injected into the electric grid. Even if the contribution of a single panel is negligible, a large population can and will make the difference. Our objective is to build a model for the aggregation of devices in a network that spans the whole Europe and to design a control solution to ensure a reliable power network, avoid black-outs and provide guarantees of efficiency.  

 

Themes:  Automated Verification, Stochastic Hybrid Systems, Bayesian Learning 

People:  Karan Mukhi, Yongchao Huang, Nathalie Cauchi, Andrea Peruffo, Joe Brown, Alessandro Abate

Software:  FAUST2, Benchmarks for BAS

Publications:

Reachability analysis of continuous and discrete time models is a hard problem that has seen much progress in the last decades.  In many cases the problem has been reduced to bisimulations with a number of limitations in the nature of the dynamics, soundness, or time horizon. 

In this research we focus on sound safety verification of Unbounded-Time Linear Time-Invariant (LTI) models with inputs, over both continuous and discrete time, using reachability analysis.  We achieve this using Abstract Acceleration: this over-approximates the reach tube of a model over unbounded time by using abstraction.  The technique is applied to a number of discrete- and continuous-time models and the results show good performance when compared to state-of-the-art tools.  

Themes: Automated Verification

People: Dario Cattaruzza, Alessandro Abate

Software:  Axelerator

Publications: