# Projects

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, FAUST^{2}

**Recent Publications:**

- Tkachev I, Mereacre A, Katoen J-P, Abate A. 2017. Quantitative model-checking of controlled discrete-time Markov processes. Inf. Comput.. 253:1–35.
- Haesaert S, Soudjani SEsmaeil Za, Abate A. 2016. Verification of general Markov decision processes by approximate similarity relations and policy refinement. CoRR. abs/1605.09557
- Soudjani SEsmaeil Za, Adzkiya D, Abate A. 2016. Formal Verification of Stochastic Max-Plus-Linear Systems. {IEEE} Trans. Automat. Contr.. 61:2861–2876.

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:**

- Hasanbeig M, Abate A, Kroening D. 2018. Logically-Constrained Reinforcement Learning. CoRR. abs/1801.08099

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:**

- Soudjani SEsmaeil Za, Adzkiya D, Abate A. 2016. Formal Verification of Stochastic Max-Plus-Linear Systems. {IEEE} Trans. Automat. Contr.. 61:2861–2876.
- Adzkiya D, Zhang Y, Abate A. 2016. VeriSiMPL 2: An open-source software for the verification of max-plus-linear systems. Discrete Event Dynamic Systems. 26:109–145.
- Adzkiya D, De Schutter B, Abate A. 2015. Computational techniques for reachability analysis of Max-Plus-Linear systems. Automatica. 53:293–302.

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:**

- CounterExample Guided Inductive Synthesis Modulo Theories - Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, CAV 2018
- Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants - Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, CAV 2017
- Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants - Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, HSCC 2017
- DSSynth: an automated digital controller synthesis tool for physical plants - Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lennon Chaves, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, ASE 2017

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:**

- Polgreen E, Wijesuriya VB, Haesaert S, Abate A. 2017. Automated Experiment Design for Data-Efficient Verification of Parametric Markov Decision Processes. Quantitative Evaluation of Systems - 14th International Conference, {QEST} 2017, Berlin, Germany, September 5-7, 2017, Proceedings. :259–274.
- Polgreen E, Wijesuriya VB, Haesaert S, Abate A. 2016. Data-Efficient Bayesian Verification of Parametric Markov Chains. Quantitative Evaluation of Systems - 13th International Conference, {QEST} 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings. :35–51.

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.

- 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: ** FAUST^{2}, Benchmarks for BAS

**Publications:**

- Cauchi N, Abate A. 2018. Benchmarks for cyber-physical systems: A modular model library for buildings automation. IFAC Conference on Analysis and Design of Hybrid Systems.
- Cauchi N, Hoque Anuarul, Abate A, Stoelinga M. 2017. Efficient Probabilistic Model Checking of Smart Building Maintenance using Fault Maintenance Trees. In Proceedings of the 4th International Conference on Systems for Energy-Efficient Built Environments.
- Peruffo A, Guiu E, Panciatici P, Abate A. 2017. Aggregated Markov Models of a Heterogeneous Population of Photovoltaic Panels. Quantitative Evaluation of Systems - 14th International Conference, {QEST} 2017, Berlin, Germany, September 5-7, 2017, Proceedings. :72–87.
- Haesaert S, Cauchi N, Abate A. 2017. Certified policy synthesis for general Markov decision processes: An application in building automation systems. Perform. Eval.. 117:75–103.
- Macek K, Endel P, Cauchi N, Abate A. 2017. Long-Term Predictive Maintenance: A Study of Optimal Cleaning of Biomass Boilers. Energy and Buildings.
- Cauchi N, Macek K, Abate A. 2017. Model-based predictive maintenance in building automation systems with user discomfort. Energy. 138:306-315.
- Holub O, Zamani M, Abate A. 2016. Efficient {HVAC} controls: {A} symbolic approach. 2016 European Control Conference, {ECC} 2016, Aalborg, Denmark, June 29 - July 1, 2016. :1159–1164.
- Abate A. 2016. Verification of Networks of Smart Energy Systems over the Cloud. Numerical Software Verification - 9th International Workshop, {NSV} 2016, Toronto, ON, Canada, July 17-18, 2016, [collocated with {CAV} 2016], Revised Selected Papers. :1–14.

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:**

- Cattaruzza D, Abate A, Schrammel P, Kroening D. 2017. Sound Numerical Computations in Abstract Acceleration. Numerical Software Verification - 10th International Workshop, {NSV} 2017, Heidelberg, Germany, July 22-23, 2017, Proceedings [collocated with {CAV} 2017]. :38–60.
- Cattaruzza D, Abate A, Schrammel P, Kroening D. 2015. Unbounded-Time Analysis of Guarded {LTI} Systems with Inputs by Abstract Acceleration. Static Analysis - 22nd International Symposium, {SAS} 2015, Saint-Malo, France, September 9-11, 2015, Proceedings.