39 citations · 57 across the 17 of their papers we have counts for
11 papers · 1 filter
SafePILCO: a software tool for safe and data-efficient policy synthesis
Kyriakos Polymenakos, Nikitas Rontsis, Alessandro Abate +1
SafePILCO is a software tool for safe and data-efficient policy search with reinforcement learning. It extends the known PILCO algorithm, originally written in MATLAB, to support s…
Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
Daniele Ahmed, Andrea Peruffo, Alessandro Abate
In this paper we employ SMT solvers to soundly synthesise Lyapunov functions that assert the stability of a given dynamical model. The search for a Lyapunov function is framed as t…
Symbolic Reachability Analysis of High Dimensional Max-Plus Linear Systems
Muhammad Syifa'ul Mufid, Dieky Adzkiya, Alessandro Abate
This work discusses the reachability analysis (RA) of Max-Plus Linear (MPL) systems, a class of continuous-space, discrete-event models defined over the max-plus algebra. Given the…
Computation of the Transient in Max-Plus Linear Systems via SMT-Solving
Alessandro Abate, Alessandro Cimatti, Andrea Micheli +1
This paper proposes a new approach, grounded in Satisfiability Modulo Theories (SMT), to study the transient of a Max-Plus Linear (MPL) system, that is the number of steps leading…
Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-time Systems
Yulong Gao, Alessandro Abate, Frank J. Jiang +3
We propose algorithms for performing model checking and control synthesis for discrete-time uncertain systems under linear temporal logic (LTL) specifications. We construct tempora…
Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
Andrea Peruffo, Daniele Ahmed, Alessandro Abate
We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The…