arXiv subjects

Alessandro Abate

Publications and source records attributed to Alessandro Abate.

At least 55 records · Page 3Linked to original sources

arXiv2025

Best-Effort Policies for Robust Markov Decision Processes

We study the common generalization of Markov decision processes (MDPs) with sets of transition probabilities, known as robust MDPs (RMDPs). A standard goal in RMDPs is to compute a policy that maximizes the expected return under an adversarial choice of the transition probabilities. If the uncertainty in the probabilities is independent between the states, known as s-rectangularity, such optimal robust policies can be computed efficiently using robust value iteration. However, there might still be multiple optimal robust policies, which, while equivalent with respect to the worst-case, reflect different expected returns under non-adversarial choices of the transition probabilities. Hence, we propose a refined policy selection criterion for RMDPs, drawing inspiration from the notions of dominance and best-effort in game theory. Instead of seeking a policy that only maximizes the worst-case expected return, we additionally require the policy to achieve a maximal expected return under different (i.e., not fully adversarial) transition probabilities. We call such a policy an optimal robust best-effort (ORBE) policy. We prove that ORBE policies always exist, characterize their structure, and present an algorithm to compute them with a manageable overhead compared to standard robust value iteration. ORBE policies offer a principled tie-breaker among optimal robust policies. Numerical experiments show the feasibility of our approach.

cs.AI↗

arXiv2025

Temporal-Difference Variational Continual Learning

Machine Learning models in real-world applications must continuously learn new tasks to adapt to shifts in the data-generating distribution. Yet, for Continual Learning (CL), models often struggle to balance learning new tasks (plasticity) with retaining previous knowledge (memory stability). Consequently, they are susceptible to Catastrophic Forgetting, which degrades performance and undermines the reliability of deployed systems. In the Bayesian CL literature, variational methods tackle this challenge by employing a learning objective that recursively updates the posterior distribution while constraining it to stay close to its previous estimate. Nonetheless, we argue that these methods may be ineffective due to compounding approximation errors over successive recursions. To mitigate this, we propose new learning objectives that integrate the regularization effects of multiple previous posterior estimations, preventing individual errors from dominating future posterior updates and compounding over time. We reveal insightful connections between these objectives and Temporal-Difference methods, a popular learning mechanism in Reinforcement Learning and Neuroscience. Experiments on challenging CL benchmarks show that our approach effectively mitigates Catastrophic Forgetting, outperforming strong Variational CL methods.

cs.LG↗

arXiv2025

Existence and Synthesis of Multi-Resolution Approximate Bisimulations for Continuous-State Dynamical Systems

We present a fully automatic framework for synthesising compact, finite-state deterministic abstractions of deterministic, continuous-state autonomous systems under locally specified resolution requirements. Our approach builds on multi-resolution approximate bisimulations, a generalisation of classical $ε$-approximate bisimulations, that support state-dependent error bounds and subsumes both variable- and uniform-resolution relations. We show that some systems admit multi-resolution bisimulations but no $ε$-approximate bisimulation. We prove the existence of multi-resolution approximately bisimilar abstractions for all incrementally uniformly bounded ($δ$-UB) systems, thereby broadening the applicability of symbolic verification to a larger class of dynamics; as a trivial special case, this result also covers incrementally globally asymptotically stable ($δ$-GAS) systems. The Multi-resolution Abstraction Synthesis Problem (MRASP) is solved via a scalable Counterexample-Guided Inductive Synthesis (CEGIS) loop, combining mesh refinement with counterexample-driven refinement. This ensures soundness for all $δ$-UB systems, and ensures termination in certain special cases. Experiments on linear and nonlinear benchmarks, including non-$δ$-GAS and non-differentiable cases, demonstrate that our algorithm yields abstractions up to 50\% smaller than Lyapunov-based grids while enforcing tighter, location-dependent error guarantees.

eess.SY↗

arXiv2025

PAC Apprenticeship Learning with Bayesian Active Inverse Reinforcement Learning

As AI systems become increasingly autonomous, reliably aligning their decision-making with human preferences is essential. Inverse reinforcement learning (IRL) offers a promising approach to infer preferences from demonstrations. These preferences can then be used to produce an apprentice policy that performs well on the demonstrated task. However, in domains like autonomous driving or robotics, where errors can have serious consequences, we need not just good average performance but reliable policies with formal guarantees -- yet obtaining sufficient human demonstrations for reliability guarantees can be costly. Active IRL addresses this challenge by strategically selecting the most informative scenarios for human demonstration. We introduce PAC-EIG, an information-theoretic acquisition function that directly targets probably-approximately-correct (PAC) guarantees for the learned policy -- providing the first such theoretical guarantee for active IRL with noisy expert demonstrations. Our method maximises information gain about the regret of the apprentice policy, efficiently identifying states requiring further demonstration. We also present Reward-EIG as an alternative when learning the reward itself is the primary objective. Focusing on finite state-action spaces, we prove convergence bounds, illustrate failure modes of prior heuristic methods, and demonstrate our method's advantages experimentally.

cs.LG↗

arXiv2025

Polymatroidal Representations of Aggregate EV Flexibility Considering Network Constraints

The increasing penetration of electric vehicles (EVs) introduces significant flexibility potential to power systems. However, uncoordinated or synchronous charging can lead to overloading of distribution networks. Extending recent approaches that utilize generalized polymatroids, a family of polytopes, to represent the aggregate flexibility of EV populations, we show how to integrate network constraints into this representation to obtain network-constrained aggregate flexibility sets. Furthermore, we demonstrate how to optimize over these network-constrained aggregate flexibility sets, and propose a disaggregation procedure that maps an aggregate load profile to individual EV dispatch instructions, while respecting both device-level and network constraints.

eess.SY↗

arXiv2025

Data-Driven Abstraction and Synthesis for Stochastic Systems with Unknown Dynamics

We study the automated abstraction-based synthesis of correct-by-construction control policies for stochastic dynamical systems with unknown dynamics. Our approach is to learn an abstraction from sampled data, which is represented in the form of a finite Markov decision process (MDP). In this paper, we present a data-driven technique for constructing finite-state interval MDP (IMDP) abstractions of stochastic systems with unknown nonlinear dynamics. As a distinguishing and novel feature, our technique only requires (1) noisy state-input-state observations and (2) an upper bound on the system's Lipschitz constant. Combined with standard model-checking techniques, our IMDP abstractions enable the synthesis of policies that satisfy probabilistic temporal properties (such as "reach-while-avoid") with a predefined confidence. Our experimental results show the effectiveness and robustness of our approach.

eess.SY↗

arXiv2025

Data-Driven Yet Formal Policy Synthesis for Stochastic Nonlinear Dynamical Systems

The automated synthesis of control policies for stochastic dynamical systems presents significant challenges. A standard approach is to construct a finite-state abstraction of the continuous system, typically represented as a Markov decision process (MDP). However, generating abstractions is challenging when (1) the system's dynamics are nonlinear, and/or (2) we do not have complete knowledge of the dynamics. In this work, we introduce a novel data-driven abstraction technique for nonlinear Lipschitz continuous dynamical systems with additive stochastic noise that addresses both of these issues. As a key step, we use samples of the dynamics to learn the enabled actions and transition probabilities of the abstraction. We represent abstractions as MDPs with intervals of transition probabilities, known as interval MDPs (IMDPs). These abstractions enable the synthesis of policies for the concrete nonlinear system, with probably approximately correct (PAC) guarantees on the probability of satisfying a specified control objective. Our numerical experiments illustrate the effectiveness and robustness of our approach in achieving reliable control under uncertainty.

eess.SY↗

arXiv2025

Data-Driven Certificate Synthesis

We investigate the problem of verifying different properties of discrete time dynamical systems, namely, reachability, safety and reach-while-avoid. To achieve this, we adopt a data driven perspective and, using past system trajectories as data, we aim at learning a specific function termed certificate for each property we wish to verify. We seek to minimize a loss function, designed to encompass conditions on the certificate to be learned that encode the satisfaction of the associated property. Besides learning a certificate, we quantify probabilistically its generalization properties, namely, how likely it is for a certificate to be valid (and hence for the associated property to be satisfied) when it comes to a new system trajectory not included in the training data set. We view this problem under the realm of probably approximately correct (PAC) learning under the notion of compression, and use recent advancements of the so-called scenario approach to obtain scalable generalization bounds on the learned certificates. To achieve this, we design a novel algorithm that minimizes the loss function and hence constructs a certificate, and at the same time determines a quantity termed compression, which is instrumental in obtaining meaningful probabilistic guarantees. This process is novel per se and provides a constructive mechanism for compression set calculation, thus opening the road for its use to more general non-convex optimization problems. We verify the efficacy of our methodology on several numerical case studies, and compare it (both theoretically and numerically) with closely related results on data-driven property verification.

eess.SY↗

arXiv2025

Continuous-time Data-driven Barrier Certificate Synthesis

We consider the problem of verifying safety for continuous-time dynamical systems. Developing upon recent advancements in data-driven verification, we use only a finite number of sampled trajectories to learn a barrier certificate, namely a function which verifies safety. We train a safety-informed neural network to act as this certificate, with an appropriately designed loss function to encompass the safety conditions. In addition, we provide probabilistic generalisation guarantees from discrete samples of continuous trajectories, to unseen continuous ones. Numerical investigations demonstrate the efficacy of our approach and contrast it with related results in the literature.

eess.SY↗

arXiv2025

Probabilistic Alternating Simulations for Policy Synthesis in Uncertain Stochastic Dynamical Systems

A classical approach to formal policy synthesis in stochastic dynamical systems is to construct a finite-state abstraction, often represented as a Markov decision process (MDP). The correctness of these approaches hinges on a behavioural relation between the dynamical system and its abstraction, such as a probabilistic simulation relation. However, probabilistic simulation relations do not suffice when the system dynamics are, next to being stochastic, also subject to nondeterministic (i.e., set-valued) disturbances. In this work, we extend probabilistic simulation relations to systems with both stochastic and nondeterministic disturbances. Our relation, which is inspired by a notion of alternating simulation, generalises existing relations used for verification and policy synthesis used in several works. Intuitively, our relation allows reasoning probabilistically over stochastic uncertainty, while reasoning robustly (i.e., adversarially) over nondeterministic disturbances. We experimentally demonstrate the applicability of our relations for policy synthesis in a 4D-state Dubins vehicle.

eess.SY↗

arXiv2025

Studying Cross-cluster Modularity in Neural Networks

An approach to improve neural network interpretability is via clusterability, i.e., splitting a model into disjoint clusters that can be studied independently. We define a measure for clusterability and show that pre-trained models form highly enmeshed clusters via spectral graph clustering. We thus train models to be more modular using a "clusterability loss" function that encourages the formation of non-interacting clusters. We then investigate the emerging properties of these highly clustered models. We find our trained clustered models do not exhibit more task specialization, but do form smaller circuits. We investigate CNNs trained on MNIST and CIFAR, small transformers trained on modular addition, and GPT-2 and Pythia on the Wiki dataset, and Gemma on a Chemistry dataset. This investigation shows what to expect from clustered models.

cs.LG↗

arXiv2025

The Perils of Optimizing Learned Reward Functions: Low Training Error Does Not Guarantee Low Regret

In reinforcement learning, specifying reward functions that capture the intended task can be very challenging. Reward learning aims to address this issue by learning the reward function. However, a learned reward model may have a low error on the data distribution, and yet subsequently produce a policy with large regret. We say that such a reward model has an error-regret mismatch. The main source of an error-regret mismatch is the distributional shift that commonly occurs during policy optimization. In this paper, we mathematically show that a sufficiently low expected test error of the reward model guarantees low worst-case regret, but that for any fixed expected test error, there exist realistic data distributions that allow for error-regret mismatch to occur. We then show that similar problems persist even when using policy regularization techniques, commonly employed in methods such as RLHF. We hope our results stimulate the theoretical and empirical study of improved methods to learn reward models, and better ways to measure their quality reliably.

cs.LG↗

arXiv2025

SPoRt -- Safe Policy Ratio: Certified Training and Deployment of Task Policies in Model-Free RL

To apply reinforcement learning to safety-critical applications, we ought to provide safety guarantees during both policy training and deployment. In this work, we present theoretical results that place a bound on the probability of violating a safety property for a new task-specific policy in a model-free, episodic setting. This bound, based on a maximum policy ratio computed with respect to a 'safe' base policy, can also be applied to temporally-extended properties (beyond safety) and to robust control problems. To utilize these results, we introduce SPoRt, which provides a data-driven method for computing this bound for the base policy using the scenario approach, and includes Projected PPO, a new projection-based approach for training the task-specific policy while maintaining a user-specified bound on property violation. SPoRt thus enables users to trade off safety guarantees against task-specific performance. Complementing our theoretical results, we present experimental results demonstrating this trade-off and comparing the theoretical bound to posterior bounds derived from empirical violation rates.

cs.LG↗

arXiv2025

ARCH-COMP25 Category Report: Stochastic Models

This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year's edition of the competition. In particular, this report introduces three recently developed software tools, a new water distribution network benchmark, and a collection of simplified benchmarks intended to facilitate further comparisons among tools that were previously not directly comparable. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2025.

cs.LO↗

arXiv2025

Exact Characterization of Aggregate Flexibility via Generalized Polymatroids

It is well established that the aggregate flexibility inherent in populations of distributed energy resources (DERs) can be leveraged to mitigate the intermittency and uncertainty associated with renewable generation, while also providing ancillary grid services. To enable this, aggregators must effectively represent the flexibility in the populations they control to the market or system operator. A key challenge is accurately computing the aggregate flexibility of a population, which can be formally expressed as the Minkowski sum of a collection of polytopes, a problem that is generally computationally intractable. However, the flexibility polytopes of many DERs exhibit structural symmetries that can be exploited for computational efficiency. To this end, we introduce generalized polymatroids, a family of polytopes, into the flexibility aggregation literature. We demonstrate that individual flexibility sets belong to this family, enabling efficient computation of their exact Minkowski sum. For homogeneous populations of DERs we further derive simplifications that yield more succinct representations of aggregate flexibility. Additionally, we develop an efficient optimization framework over these sets and propose a vertex-based disaggregation method, to allocate aggregate flexibility among individual DERs. Finally, we validate the optimality and computational efficiency of our approach through comparisons with existing methods.

eess.SY↗

arXiv2025

Goal Kernel Planning: Linearly-Solvable Non-Markovian Policies for Logical Tasks with Goal-Conditioned Options

In the domain of hierarchical planning, compositionality, abstraction, and task transfer are crucial for designing algorithms that can efficiently solve a variety of problems with maximal representational reuse. Many real-world problems require non-Markovian policies to handle complex structured tasks with logical conditions, often leading to prohibitively large state representations; this requires efficient methods for breaking these problems down and reusing structure between tasks. To this end, we introduce a compositional framework called Linearly-Solvable Goal Kernel Dynamic Programming (LS-GKDP) to address the complexity of solving non-Markovian Boolean sub-goal tasks with ordering constraints. LS-GKDP combines the Linearly-Solvable Markov Decision Process (LMDP) formalism with the Options Framework of Reinforcement Learning. LMDPs can be efficiently solved as a principal eigenvector problem, and options are policies with termination conditions used as temporally extended actions; with LS-GKDP we expand LMDPs to control over options for logical tasks. This involves decomposing a high-dimensional problem down into a set of goal-condition options for each goal and constructing a goal kernel, which is an abstract transition kernel that jumps from an option's initial-states to its termination-states along with an update of the higher-level task-state. We show how an LMDP with a goal kernel enables the efficient optimization of meta-policies in a lower-dimensional subspace defined by the task grounding. Options can also be remapped to new problems within a super-exponential space of tasks without significant recomputation, and we identify cases where the solution is invariant to the task grounding, permitting zero-shot task transfer.

cs.AI↗

arXiv2025

LLM-Enhanced Symbolic Control for Safety-Critical Applications

Motivated by Smart Manufacturing and Industry 4.0, we introduce a framework for synthesizing Abstraction-Based Controller Design (ABCD) for reach-avoid problems from Natural Language (NL) specifications using Large Language Models (LLMs). A Code Agent interprets an NL description of the control problem and translates it into a formal language interpretable by state-of-the-art symbolic control software, while a Checker Agent verifies the correctness of the generated code and enhances safety by identifying specification mismatches. Evaluations show that the system handles linguistic variability and improves robustness over direct planning with LLMs. The proposed approach lowers the barrier to formal control synthesis by enabling intuitive, NL-based task definition while maintaining safety guarantees through automated validation.

eess.SY↗

arXiv2025

Branching Bisimulation Learning

We introduce a bisimulation learning algorithm for non-deterministic transition systems. We generalise bisimulation learning to systems with bounded branching and extend its applicability to model checking branching-time temporal logic, while previously it was limited to deterministic systems and model checking linear-time properties. Our method computes a finite stutter-insensitive bisimulation quotient of the system under analysis, represented as a decision tree. We adapt the proof rule for well-founded bisimulations to an iterative procedure that trains candidate decision trees from sample transitions of the system, and checks their validity over the entire transition relation using SMT solving. This results in a new technology for model checking CTL* without the next-time operator. Our technique is sound, entirely automated, and yields abstractions that are succinct and effective for formal verification and system diagnostics. We demonstrate the efficacy of our method on diverse benchmarks comprising concurrent software, communication protocols and robotic scenarios. Our method performs comparably to mature tools in the special case of LTL model checking, and outperforms the state of the art in CTL and CTL* model checking for systems with very large and countably infinite state space.

cs.LO↗