Toni Mancini

Current AI-based Virtual Screening (VS) methods seek to manage ultra-large molecular libraries. To this end, they develop increasingly efficient heuristics

Realistic industrial systems typically need to be modeled as hybrid systems consisting of hundreds (easily thousands) of nonlinear differential algebraic equations (DAEs). The size of such models is one of the major obstacles to overcome when developing automated design methods for industrial control systems. In this article, we present a scenario-based approach that, by exploiting the synergies among simulation, black-box optimization, and statistical model checking, allows us to automate the design of quality-guaranteed industry-size control systems, i.e., control systems for which a user-specified statistical guarantee on correctness holds over the possible operational scenarios. We show the effectiveness of our approach through a Modelica model consisting of a hybrid nonlinear DAE system with 1276 equations, 492 of which are nontrivial, containing 152 continuous state variables and 38 discrete ones, plus 7 algorithm blocks. Our experiments show that within a few hours of computation on an off-the-shelf workstation, we can find quality-guaranteed solutions (with very tight quality guarantees) to our design problem. We also compute an entire discretized Pareto front for such a large system over two conflicting key performance indicators.

The increasing spreading of small commercial unmanned aerial vehicles (UAVs, also known as drones) presents serious threats for critical areas, such as airports, power plants, and governmental and military facilities. In fact, such UAVs can easily disturb or jam radio communications, collide with other flying objects, perform espionage activity, and carry offensive payloads, e.g., weapons or explosives. A central problem when designing surveillance solutions for the localization of unauthorized UAVs in critical areas is to decide how many triangulating sensors to use, and where to deploy them to optimize both coverage and cost effectiveness. In this article, we compute deployments of triangulating sensors for UAV localization, optimizing a given blend of metrics, namely: coverage under multiple sensing quality levels, cost-effectiveness, and fault-tolerance. We focus on large, complex three-dimensional (3-D) regions, which exhibit obstacles (e.g., buildings), varying terrain elevation, different coverage priorities, and constraints on possible sensors placement. Our novel approach relies on computational geometry and statistical model checking and enables the effective use of off-the-shelf AI-based black-box optimizers. Moreover, our method allows us to compute a closed-form, analytical representation of the region uncovered by a sensor deployment, which provides the means for rigorous, formal certification of the quality of the latter. We show the practical feasibility of our approach by computing optimal sensor deployments for UAV localization in two large, complex 3-D critical regions, the Rome Leonardo Da Vinci International Airport (FCO) and the Vienna International Center (VIC), using NOMAD as our state-of-the-art underlying optimization engine. Results show that we can compute optimal sensor deployments within a few hours on a standard workstation and within minutes on a small parallel infrastructure.

Cyber-Physical Systems (CPSs), i.e. , systems comprising both software and physical components, arise in many industry-relevant application domains and often mission- or safety-critical. System-Level Verification (SLV) of CPSs aims at certifying that given (e.g., safety or liveness) specifications are met, or at estimating the value of some Key Performance Indicators, when the system runs in its operational environment, that is in presence of inputs (from the user or other systems) and/or of additional, uncontrolled disturbances. In order to enable SLV of complex systems from the early design phases, the currently most adopted approach envisions the simulation of a system model under the (time bounded) operational scenarios deemed of interest. Unfortunately, simulation-based SLV can be computationally prohibitive (years of sequential simulation), since system model simulation is computationally intensive and the set of scenarios of interest can be extremely large. In this article, we present a technique that, given a collection of scenarios of interest (extracted from mass-storage databases or from symbolic structures like constraint-based scenario generators), computes parallel shortest simulation campaigns, which drive a possibly large number of system model simulators running in parallel in a HPC infrastructure through all (and only) those scenarios in the user-defined (possibly random) order, by wisely avoiding multiple simulations of repeated trajectories, and thus minimising the overall completion time, compatibly with the available simulator memory capacity. Our experiments on SLV of Modelica/FMU and Simulink case study models with up to almost 200 million scenarios show that our optimisation yields speedups as high as 8×. This, together with the enabled massive parallelisation, makes practically viable (a few weeks in a HPC infrastructure) verification tasks (both statistical and exhaustive, with respect to the given set of scenarios) which would otherwise take inconceivably long time.

Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints . Such constraints typically stem from requirements (or assumptions ) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding vacuity in their satisfaction. In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently enumerate (possibly in a uniformly random order) scenarios among those satisfying all the given constraints is a key enabler for the practical viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in general fail in extracting scenarios according to a given distribution (e.g., uniformly), and can be very inefficient to produce at all scenarios that are both legal (with respect to SUV assumptions) and of interest (with respect to the additional constraints). For example, in our case studies, up to 91% of the scenarios generated using such iterative approaches would need to be neglected. In this article, we show how, given a set of constraints on the input scenarios succinctly defined by multiple finite memory monitors , a data structure ( scenario generator ) can be synthesised, from which any-horizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables seamless support to virtually all simulation-based approaches to CPS verification , ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification, when a suitable bound on the horizon or an iterative horizon enlargement strategy is defined, as in the spirit of bounded model checking.

Within electrical distribution networks, substation constraint management requires that aggregated power demand from residential users is kept within suitable bounds. Efficiency of substation constraint management can be measured as the reduction of constraint violations w.r.t. unmanaged demand. Home batteries hold the promise of enabling efficient and user-oblivious substation constraint management. Centralized control of home batteries would achieve optimal efficiency. However, it is hardly acceptable by users, since service providers (e.g., utilities or aggregators) would directly control batteries at user premises. Unfortunately, devising efficient hierarchical control strategies, thus overcoming the above problem, is far from easy. In this article, we present a novel two-layer control strategy for home batteries that avoids direct control of home devices by the service provider and at the same time yields near-optimal substation constraint management efficiency. Our simulation results on field data from 62 households in Denmark show that the substation constraint management efficiency achieved with our approach is at least 82% of the one obtained with a theoretical optimal centralized strategy.