39 citations · 55 across the 11 of their papers we have counts for
7 papers · 1 filter
Data-driven memory-dependent abstractions of dynamical systems
Adrien Banse, Licio Romao, Alessandro Abate +1
We propose a sample-based, sequential method to abstract a (potentially black-box) dynamical system with a sequence of memory-dependent Markov chains of increasing size. We show th…
Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty
Thom Badings, Licio Romao, Alessandro Abate +1
Capturing uncertainty in models of complex dynamical systems is crucial to designing safe controllers. Stochastic noise causes aleatoric uncertainty, whereas imprecise knowledge of…
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…
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…