BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Alessandro Abate

Alessandro Abate contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer ScienceMachine Learningeess.SYSystems and ControlArtificial IntelligenceComputational Engineering, Finance, and ScienceMultiagent SystemsComputer Science and Game TheoryFormal Languages and Automata Theorymath.PRmath.RA

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
18works
0followers
11topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

18 published item(s)

preprint2026arXiv

Multi-Property Synthesis

We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude.

0 citations0 reviewsNo code linkedOpen access
preprint2026arXiv

Robust Parameter Learning for Uncertain MDPs

Learning-based approaches to verifying unknown Markov decision processes (MDPs) often employ uncertain MDPs. These models use, for example, confidence intervals to capture transition uncertainty and allow synthesis of policies that are robust to this uncertainty. However, this approach typically quantifies uncertainty independently for individual transition probabilities, ignoring dependencies due to shared latent quantities. We propose to learn such models using parametric MDPs (pMDPs), where transition probabilities are expressions over a set of parameters. We project statistical uncertainty from empirical transition frequencies onto the pMDP's parameter space, yielding a probably approximately correct (PAC) uncertainty model for the underlying MDP that respects the algebraic dependencies between transitions. The resulting models are algorithmically challenging to solve, so we propose a hierarchy of sound polytopic outer approximations of the induced confidence set. We implement and evaluate our approach, demonstrating substantially tighter uncertainty estimates than classical interval-based uncertain MDP learning techniques.

0 citations0 reviewsNo code linkedOpen access
preprint2023arXiv

Grid-Free Computation of Probabilistic Safety with Malliavin Calculus

This work concerns continuous-time, continuous-space stochastic dynamical systems described by stochastic differential equations (SDE). It presents a new approach to compute probabilistic safety regions, namely sets of initial conditions of the SDE associated to trajectories that are safe with a probability larger than a given threshold. The approach introduces a functional that is minimised at the border of the probabilistic safety region, then solves an optimisation problem using techniques from Malliavin Calculus, which computes such region. Unlike existing results in the literature, the new approach allows one to compute probabilistic safety regions without gridding the state space of the SDE.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey

Stochastic hybrid systems have received significant attentions as a relevant modelling framework describing many systems, from engineering to the life sciences: they enable the study of numerous applications, including transportation networks, biological systems and chemical reaction networks, smart energy and power grids, and beyond. Automated verification and policy synthesis for stochastic hybrid systems can be inherently challenging: this is due to the heterogeneity of their dynamics (presence of continuous and discrete components), the presence of uncertainty, and in some applications the large dimension of state and input sets. Over the past few years, a few hundred articles have investigated these models, and developed diverse and powerful approaches to mitigate difficulties encountered in the analysis and synthesis of such complex stochastic systems. In this survey, we overview the most recent results in the literature and discuss different approaches, including (in)finite abstractions, verification and synthesis for temporal logic specifications, stochastic similarity relations, (control) barrier certificates, compositional techniques, and a selection of results on continuous-time stochastic systems; we finally survey recently developed software tools that implement the discussed approaches. Throughout the manuscript we discuss a few open topics to be considered as potential future research directions: we hope that this survey will guide younger researchers through a comprehensive understanding of the various challenges, tools, and solutions in this enticing and rich scientific area.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Low Emission Building Control with Zero-Shot Reinforcement Learning

Heating and cooling systems in buildings account for 31\% of global energy use, much of which are regulated by Rule Based Controllers (RBCs) that neither maximise energy efficiency nor minimise emissions by interacting optimally with the grid. Control via Reinforcement Learning (RL) has been shown to significantly improve building energy efficiency, but existing solutions require access to building-specific simulators or data that cannot be expected for every building in the world. In response, we show it is possible to obtain emission-reducing policies without such knowledge a priori--a paradigm we call zero-shot building control. We combine ideas from system identification and model-based RL to create PEARL (Probabilistic Emission-Abating Reinforcement Learning) and show that a short period of active exploration is all that is required to build a performant model. In experiments across three varied building energy simulations, we show PEARL outperforms an existing RBC once, and popular RL baselines in all cases, reducing building emissions by as much as 31\% whilst maintaining thermal comfort. Our source code is available online via https://enjeeneer.io/projects/pearl .

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Modular Deep Reinforcement Learning for Continuous Motion Planning with Temporal Logic

This paper investigates the motion planning of autonomous dynamical systems modeled by Markov decision processes (MDP) with unknown transition probabilities over continuous state and action spaces. Linear temporal logic (LTL) is used to specify high-level tasks over infinite horizon, which can be converted into a limit deterministic generalized Büchi automaton (LDGBA) with several accepting sets. The novelty is to design an embedded product MDP (EP-MDP) between the LDGBA and the MDP by incorporating a synchronous tracking-frontier function to record unvisited accepting sets of the automaton, and to facilitate the satisfaction of the accepting conditions. The proposed LDGBA-based reward shaping and discounting schemes for the model-free reinforcement learning (RL) only depend on the EP-MDP states and can overcome the issues of sparse rewards. Rigorous analysis shows that any RL method that optimizes the expected discounted return is guaranteed to find an optimal policy whose traces maximize the satisfaction probability. A modular deep deterministic policy gradient (DDPG) is then developed to generate such policies over continuous state and action spaces. The performance of our framework is evaluated via an array of OpenAI gym environments.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning

This paper proposes DeepSynth, a method for effective training of deep Reinforcement Learning (RL) agents when the reward is sparse and non-Markovian, but at the same time progress towards the reward requires achieving an unknown sequence of high-level objectives. Our method employs a novel algorithm for synthesis of compact automata to uncover this sequential structure automatically. We synthesise a human-interpretable automaton from trace data collected by exploring the environment. The state space of the environment is then enriched with the synthesised automaton so that the generation of a control policy by deep RL is guided by the discovered structure encoded in the automaton. The proposed approach is able to cope with both high-dimensional, low-level features and unknown sparse non-Markovian rewards. We have evaluated DeepSynth's performance in a set of experiments that includes the Atari game Montezuma's Revenge. Compared to existing approaches, we obtain a reduction of two orders of magnitude in the number of iterations required for policy synthesis, and also a significant improvement in scalability.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Equilibrium Refinements for Multi-Agent Influence Diagrams: Theory and Practice

Multi-agent influence diagrams (MAIDs) are a popular form of graphical model that, for certain classes of games, have been shown to offer key complexity and explainability advantages over traditional extensive form game (EFG) representations. In this paper, we extend previous work on MAIDs by introducing the concept of a MAID subgame, as well as subgame perfect and trembling hand perfect equilibrium refinements. We then prove several equivalence results between MAIDs and EFGs. Finally, we describe an open source implementation for reasoning about MAIDs and computing their equilibria.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Multi-Agent Reinforcement Learning with Temporal Logic Specifications

In this paper, we study the problem of learning to satisfy temporal logic specifications with a group of agents in an unknown environment, which may exhibit probabilistic behaviour. From a learning perspective these specifications provide a rich formal language with which to capture tasks or objectives, while from a logic and automated verification perspective the introduction of learning capabilities allows for practical applications in large, stochastic, unknown environments. The existing work in this area is, however, limited. Of the frameworks that consider full linear temporal logic or have correctness guarantees, all methods thus far consider only the case of a single temporal logic specification and a single agent. In order to overcome this limitation, we develop the first multi-agent reinforcement learning technique for temporal logic specifications, which is also novel in its ability to handle multiple specifications. We provide correctness and convergence guarantees for our main algorithm - ALMANAC (Automaton/Logic Multi-Agent Natural Actor-Critic) - even when using function approximation. Alongside our theoretical results, we further demonstrate the applicability of our technique via a set of preliminary experiments.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers

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 the satisfiability of a second-order logical formula, asking whether there exists a function satisfying a desired specification (stability) for all possible initial conditions of the model. We synthesise Lyapunov functions for linear, non-linear (polynomial), and for parametric models. For non-linear models, the algorithm also determines a region of validity for the Lyapunov function. We exploit an inductive framework to synthesise Lyapunov functions, starting from parametric templates. The inductive framework comprises two elements: a learner proposes a Lyapunov function, and a verifier checks its validity - its lack is expressed via a counterexample (a point over the state space), for further use by the learner. Whilst the verifier uses the SMT solver Z3, thus ensuring the overall soundness of the procedure, we examine two alternatives for the learner: a numerical approach based on the optimisation tool Gurobi, and a sound approach based again on Z3. The overall technique is evaluated over a broad set of benchmarks, which shows that this methodology not only scales to 10-dimensional models within reasonable computational time, but also offers a novel soundness proof for the generated Lyapunov functions and their domains of validity.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Bayesian Verification of Chemical Reaction Networks

We present a data-driven verification approach that determines whether or not a given chemical reaction network (CRN) satisfies a given property, expressed as a formula in a modal logic. Our approach consists of three phases, integrating formal verification over models with learning from data. First, we consider a parametric set of possible models based on a known stoichiometry and classify them against the property of interest. Secondly, we utilise Bayesian inference to update a probability distribution of the parameters within a parametric model with data gathered from the underlying CRN. In the third and final stage, we combine the results of both steps to compute the probability that the underlying CRN satisfies the given property. We apply the new approach to a case study and compare it to Bayesian statistical model checking.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Cautious Reinforcement Learning with Logical Constraints

This paper presents the concept of an adaptive safe padding that forces Reinforcement Learning (RL) to synthesise optimal control policies while ensuring safety during the learning process. Policies are synthesised to satisfy a goal, expressed as a temporal logic formula, with maximal probability. Enforcing the RL agent to stay safe during learning might limit the exploration, however we show that the proposed architecture is able to automatically handle the trade-off between efficient progress in exploration (towards goal satisfaction) and ensuring safety. Theoretical guarantees are available on the optimality of the synthesised policies and on the convergence of the learning algorithm. Experimental results are provided to showcase the performance of the proposed method.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Computation of the Transient in Max-Plus Linear Systems via SMT-Solving

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 to its periodic regime. Differently from state-of-the-art techniques, our approach allows the analysis of periodic behaviors for subsets of initial states, as well as the characterization of sets of initial states exhibiting the same specific periodic behavior and transient. Our experiments show that the proposed technique dramatically outperforms state-of-the-art methods based on max-plus algebra computations for systems of large dimensions.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Formal Synthesis of Lyapunov Neural Networks

We propose an automatic and formally sound method for synthesising Lyapunov functions for the asymptotic stability of autonomous non-linear systems. Traditional methods are either analytical and require manual effort or are numerical but lack of formal soundness. Symbolic computational methods for Lyapunov functions, which are in between, give formal guarantees but are typically semi-automatic because they rely on the user to provide appropriate function templates. We propose a method that finds Lyapunov functions fully automatically$-$using machine learning$-$while also providing formal guarantees$-$using satisfiability modulo theories (SMT). We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks (LNNs). The learner trains a neural network that satisfies the Lyapunov criteria for asymptotic stability over a samples set; the verifier proves via SMT solving that the criteria are satisfied over the whole domain or augments the samples set with counterexamples. Our method supports neural networks with polynomial activation functions and multiple depth and width, which display wide learning capabilities. We demonstrate our method over several non-trivial benchmarks and compare it favourably against a numerical optimisation-based approach, a symbolic template-based approach, and a cognate LNN-based approach. Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

SafePILCO: a software tool for safe and data-efficient policy synthesis

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 safe learning. We provide a Python implementation and leverage existing libraries that allow the codebase to remain short and modular, which is appropriate for wider use by the verification, reinforcement learning, and control communities.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Safety Guarantees for Planning Based on Iterative Gaussian Processes

Gaussian Processes (GPs) are widely employed in control and learning because of their principled treatment of uncertainty. However, tracking uncertainty for iterative, multi-step predictions in general leads to an analytically intractable problem. While approximation methods exist, they do not come with guarantees, making it difficult to estimate their reliability and to trust their predictions. In this work, we derive formal probability error bounds for iterative prediction and planning with GPs. Building on GP properties, we bound the probability that random trajectories lie in specific regions around the predicted values. Namely, given a tolerance $ε> 0 $, we compute regions around the predicted trajectory values, such that GP trajectories are guaranteed to lie inside them with probability at least $1-ε$. We verify experimentally that our method tracks the predictive uncertainty correctly, even when current approximation techniques fail. Furthermore, we show how the proposed bounds can be employed within a safe reinforcement learning framework to verify the safety of candidate control policies, guiding the synthesis of provably safe controllers.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Symbolic Reachability Analysis of High Dimensional Max-Plus Linear Systems

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 initial and target sets, we develop algorithms to verify whether there exist trajectories of the MPL system that, starting from the initial set, eventually reach the target set. We show that RA can be solved symbolically by encoding the MPL system, as well as initial and target sets into difference logic, and then checking the satisfaction of the resulting logical formula via an off-the-shelf satisfiability modulo theories (SMT) solver. The performance and scalability of the developed SMT-based algorithms are shown to clearly outperform state-of-the-art RA algorithms for MPL systems, newly allowing to investigate RA of high-dimensional MPL systems: the verification of models with more than 100 continuous variables shows the applicability of these techniques to MPL systems of industrial relevance.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-time Systems

We propose algorithms for performing model checking and control synthesis for discrete-time uncertain systems under linear temporal logic (LTL) specifications. We construct temporal logic trees (TLT) from LTL formulae via reachability analysis. In contrast to automaton-based methods, the construction of the TLT is abstraction-free for infinite systems, that is, we do not construct discrete abstractions of the infinite systems. Moreover, for a given transition system and an LTL formula, we prove that there exist both a universal TLT and an existential TLT via minimal and maximal reachability analysis, respectively. We show that the universal TLT is an underapproximation for the LTL formula and the existential TLT is an overapproximation. We provide sufficient conditions and necessary conditions to verify whether a transition system satisfies an LTL formula by using the TLT approximations. As a major contribution of this work, for a controlled transition system and an LTL formula, we prove that a controlled TLT can be constructed from the LTL formula via control-dependent reachability analysis. Based on the controlled TLT, we design an online control synthesis algorithm, under which a set of feasible control inputs can be generated at each time step. We also prove that this algorithm is recursively feasible. We illustrate the proposed methods for both finite and infinite systems and highlight the generality and online scalability with two simulated examples.

0 citations0 reviewsNo code linkedOpen access