arXiv subjects

David Parker

Publications and source records attributed to David Parker.

At least 19 recordsLinked to original sources

arXiv2026

Robust PAC Learning of Concurrent Stochastic Games

We introduce the first Probably Approximately Correct (PAC) learning framework for general-sum concurrent stochastic games (CSGs) with transition uncertainty, while addressing the challenge of Nash equilibrium (NE) existence. Our algorithm maintains data-driven $L^1$ confidence sets over transition kernels and solves a robust CSG to compute a social-welfare optimal $\varepsilon$-NE, using a robust MDP-based exploration mechanism to drive joint state-action coverage. Crucially, we introduce a Nash margin characterisation that enables principled reasoning about equilibrium existence: the framework either returns an $\varepsilon$-approximate NE whose social-welfare value is $\varepsilon$-close to optimal, or provides a sound certificate that no exact NE exists. Under a minimum reachability condition $p_{\mathrm{reach}}>0$ over relevant state-action pairs, the algorithm terminates after a polynomial number of trajectory samples, with sample complexity $\widetilde{O}\left( {R_{\max}^2 H^4 |S|^2 |A| / (p_{\mathrm{reach}} \varepsilon^2)} \right)$. Empirical results on benchmark CSGs demonstrate near-optimal performance, correct handling of equilibrium (non-)existence, and sample complexity consistent with theory.

cs.LG↗

arXiv2026

Property-driven Causal Abstractions for Markov Decision Processes

Markov Decision Processes (MDPs) are widely used as decision-making models, commonly specified over factored state spaces through state variables and their valuations. The exponential blowup in the number of states renders many reasoning tasks in MDPs challenging. Abstractions are promising techniques to reduce MDPs and thus mitigate scalability issues. In this work, we introduce a notion of causality on factored MDPs and a novel property-driven causal abstraction technique that retains many characteristics of the original MDP model. For this, we rely on causal relations over state variable predicates and identify those states that share the same reasons for fulfilling or violating a given abstraction property. We theoretically and empirically compare various causal MDP abstractions using different model types such as MDPs, interval MDPs, or stochastic games. Our evaluation demonstrates the potential of our approach: For several standard benchmarks, we obtain small abstractions that allow us to compute near-optimal policies for the original MDP. Furthermore, our causal abstractions often generalize to related large-scale MDP models.

cs.AI↗

arXiv2026

On the Continuity of the Probabilistic Bisimilarity Distance

The probabilistic bisimilarity distance provides a quantitative measure of behavioural difference for labelled Markov chains, but it may be discontinuous under perturbations of the transition probabilities. This lack of continuity undermines its applicability to empirically derived models, where transition probabilities are often approximations. Recently, we (CAV 2025) introduced robust probabilistic bisimilarity as a sufficient condition for continuity at distance zero. In this paper, we show that it is also a necessary condition, that is, two states are robustly probabilistic bisimilar if and only if their probabilistic bisimilarity distance is small for any small enough perturbation of the transition probabilities. We further extend robustness to non-bisimilar state pairs to establish a complete characterization for continuity of the probabilistic bisimilarity distance. Based on this characterization, we develop a polynomial time algorithm to decide continuity. Finally, we complement our theoretical contributions with an experimental evaluation demonstrating the proposed approach in practice. Our results show that the extra step of deciding continuity requires minimal additional cost when compared to computing the probabilistic bisimilarity distance.

cs.LO↗

arXiv2026

UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)

This paper presents the unified Markov binary (UMB) format, an efficient, extensible, and well-supported explicit-state file format for representing a wide range of probabilistic systems. UMB addresses the problem that, while probabilistic model checking tools often support common high-level modelling languages, there is no effective mechanism for exchanging low-level model representations. In practice, textual, tool-specific formats are used, hampering interoperability and resulting in large overheads in writing and reading model files. UMB provides a clean, unified, and efficient solution, based on a general underlying mathematical model, and encoded using a small set of bit-level primitive data structures. The format has already been adopted by prominent tools and comes with a convenient Python library for reading, manipulating, creating, and validating models, plus infrastructure for cross-tool installation and continuous validation. We report on both the efficiency of the file format and the new practical use cases that it facilitates.

cs.LO↗

arXiv2026

Symmetry-electronic fingerprints reveal competing magnetic phases in two-dimensional materials

Two-dimensional magnets offer compelling platforms for spintronics and quantum technologies, yet predicting their magnetic ground states, moments, and anisotropy remains challenging. This limitation primarily arises because existing machine-learning representations encode chemical environments without capturing the symmetry or exchange physics that govern magnetism. In this work, we introduce the symmetry-electronic fingerprint (SEF), a physically interpretable representation that encodes crystallographic symmetry operations, Wyckoff-site geometry, together with site-resolved electronic structure. Combined with ensemble learning with random forests, the SEF accurately classifies magnetic ordering while regressing moments alongside anisotropy energies while simultaneously resolving the distinct regimes of itinerant Stoner ferromagnetism from localized superexchange. What sets the SEF-trained models apart is that regions of elevated model uncertainty are not a failure but a diagnostic, identifying materials where these mechanisms compete. First-principles calculations on Co- and Ni-based halides and oxides confirm that these regions correspond to genuine near-degenerate FM and AFM phases with magnetic frustration, suppressed anisotropy, and emergent non-collinear ordering. By encoding symmetry together with exchange physics directly into the representation unlike conventional descriptors, the SEF transforms model uncertainty into a compass pointing toward two-dimensional materials where small perturbations drive transitions between collinear, frustrated, or non-collinear magnetic phases.

cond-mat.mtrl-sci↗

arXiv2026

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.

cs.LG↗

arXiv2026

Synergistic doping and stabilization of magnetically tunable LnTi$_3$(Sb,Sn)$_4$ (Ln:Ce--Gd) kagome metals

Here we present our synthesis and characterization of the LnTi$_3$(Sb,Sn)$_4$ (Ln: Ce, Pr, Nd, Sm, Gd) family of cleavable kagome metals. While these materials are isostructural to the LnTi$_3$Bi$_4$ family, they only form as (Sb,Sn) solid-solutions with no corresponding LnTi$_3$Sb$_4$ or LnTi$_3$Sn$_4$ phases. We use a combination of first-principles density functional theory (DFT) and Crystal Orbital Hamilton Population (COHP) calculations to show that (Sb,Sn) alloying has a stabilizing effect on the structure by adjusting the Fermi level, filling bonding states, depopulating antibonding states, and adjusting the density-of-states (DOS) towards local minima, an effect we call ``synergistic doping.'' The tunable Fermi level also has a profound effect on the magnetism, which we demonstrate through a detailed characterization of the SmTi$_3$(Sb,Sn)$_4$ series. The series hosts multiple magnetic ground states resulting from competing magnetic interactions that are tunable by the (Sb,Sn) ratio. While the focus of this work is on SmTi$_3$(Sb,Sn)$_4$, we briefly comment on the (Sb,Sn) solubility range and the conferred magnetic tunability in the other rare-earths compounds (Ln: Ce, Pr, Nd, Gd) as well. Our work demonstrates how the (Sb,Sn) synergistic pair can be used to stabilize the LnTi$_3$(Sb,Sn)$_4$ structure while simultaneously providing a means to tune the magnetism, ultimately providing a potential route to develop new intermetallics with chemical, magnetic, and electronic tunability.

cond-mat.str-el↗

arXiv2026

Probabilistic Performance Guarantees for Multi-Task Reinforcement Learning

Multi-task reinforcement learning trains generalist policies that can execute multiple tasks. While recent years have seen significant progress, existing approaches rarely provide formal performance guarantees, which are indispensable when deploying policies in safety-critical settings. We present an approach for computing high-confidence guarantees on the performance of a multi-task policy on tasks not seen during training. Concretely, we introduce a new generalisation bound that composes (i) per-task lower confidence bounds from finitely many rollouts with (ii) task-level generalisation from finitely many sampled tasks, yielding a high-confidence guarantee for new tasks drawn from the same arbitrary and unknown distribution. Across state-of-the-art multi-task RL methods, we show that the guarantees are theoretically sound and informative at realistic sample sizes.

cs.LG↗

arXiv2026

Robust Verification of Concurrent Stochastic Games

Autonomous systems often operate in multi-agent settings and need to make concurrent, strategic decisions, typically in uncertain environments. Verification and control problems for these systems can be tackled with concurrent stochastic games (CSGs), but this model requires transition probabilities to be precisely specified - an unrealistic requirement in many real-world settings. We introduce *robust CSGs* and their subclass *interval CSGs* (ICSGs), which capture epistemic uncertainty about transition probabilities in CSGs. We propose a novel framework for *robust* verification of these models under worst-case assumptions about transition uncertainty. Specifically, we develop the underlying theoretical foundations and efficient algorithms, for finite- and infinite-horizon objectives in both zero-sum and nonzero-sum settings, the latter based on (social-welfare optimal) Nash equilibria. We build an implementation in the PRISM-games model checker and demonstrate the feasibility of robust verification of ICSGs across a selection of large benchmarks.

cs.LO↗

arXiv2026

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.

cs.AI↗

arXiv2025

About Time: Model-free Reinforcement Learning with Timed Reward Machines

Reward specification plays a central role in reinforcement learning (RL), guiding the agent's behavior. To express non-Markovian rewards, formalisms such as reward machines have been introduced to capture dependencies on histories. However, traditional reward machines lack the ability to model precise timing constraints, limiting their use in time-sensitive applications. In this paper, we propose timed reward machines (TRMs), which are an extension of reward machines that incorporate timing constraints into the reward structure. TRMs enable more expressive specifications with tunable reward logic, for example, imposing costs for delays and granting rewards for timely actions. We study model-free RL frameworks (i.e., tabular Q-learning) for learning optimal policies with TRMs under digital and real-time semantics. Our algorithms integrate the TRM into learning via abstractions of timed automata, and employ counterfactual-imagining heuristics that exploit the structure of the TRM to improve the search. Experimentally, we demonstrate that our algorithm learns policies that achieve high rewards while satisfying the timing constraints specified by the TRM on popular RL benchmarks. Moreover, we conduct comparative studies of performance under different TRM semantics, along with ablations that highlight the benefits of counterfactual-imagining.

cs.AI↗

arXiv2025

Optimization-Based Robust Permissive Synthesis for Interval MDPs

We present an optimization-based framework for robust permissive synthesis for Interval Markov Decision Processes (IMDPs), motivated by robotic decision-making under transition uncertainty. In many robotic systems, model inaccuracies and sensing noise lead to interval-valued transition probabilities. While robust IMDP synthesis typically yields a single policy and permissive synthesis assumes exact models, we show that robust permissive synthesis under interval uncertainty can be cast as a global mixed-integer linear program (MILP) that directly encodes robust Bellman constraints. The formulation maximizes a quantitative permissiveness metric (the number of enabled state-action pairs), while guaranteeing that every compliant strategy satisfies probabilistic reachability or expected reward specifications under all admissible transition realizations. To address the exponential complexity of vertex-based uncertainty representations, we derive a dualization-based encoding that eliminates explicit vertex enumeration and scales linearly with the number of successors. Experimental evaluation on four representative robotic benchmark domains demonstrates scalability to IMDPs with hundreds of thousands of states. The proposed framework provides a practical and general foundation for uncertainty-aware, flexibility-preserving controller synthesis in robotic systems.

cs.RO↗

arXiv2025

Probabilistic Model Checking: Applications and Trends

Probabilistic model checking is an approach to the formal modelling and analysis of stochastic systems. Over the past twenty five years, the number of different formalisms and techniques developed in this field has grown considerably, as has the range of problems to which it has been applied. In this paper, we identify the main application domains in which probabilistic model checking has proved valuable and discuss how these have evolved over time. We summarise the key strands of the underlying theory and technologies that have contributed to these advances, and highlight examples which illustrate the benefits that probabilistic model checking can bring. The aim is to inform potential users of these techniques and to guide future developments in the field.

cs.LO↗

arXiv2025

Insulating ground state and 2-k magnetic structure of candidate Weyl Hydrogen atom K$_2$Mn$_3$(AsO$_4$)$_3$

The ideal Weyl 'Hydrogen-atom' semi-metal exhibits only a single pair of Weyl nodes and no other trivial states at the Fermi energy. Such a material would be a panacea in the study of Weyl quasi particles allowing direct unambiguous observation of their topological properties. The alluaudite-like K$_2$Mn$_3$(AsO$_4$)$_3$ compound was recently proposed as such a material. Here we use comprehensive experimental work and first principle calculations to assess this prediction. We find K$_2$Mn$_3$(AsO$_4$)$_3$ crystallizes in the $C2/c$ symmetry with a quasi-1D Mn sublattice, growing as small needle-like crystals. Bulk properties measurements reveal magnetic transitions at $\approx$ 8 and $\approx$ 4 K which neutron scattering experiments show correspond to two distinct magnetic orders, first a partially ordered ferrimagnetic $\mathbf{k_1}$= (0, 0, 0) structure at 8 K and a second transition of $\mathbf{k_2}$= (1, 0, 0) at 4 K to a fully ordered state. Below the second transition, both ordering vectors are necessary to describe the complex magnetic structure with modulated spin magnitudes. Both of the best-fit magnetic structures in this work are found to break the symmetry necessary for the generation of the Weyl nodes, though one of the magnetic structures allowed by $\mathbf{k_1}$ does preserve this symmetry. However, the crystals are optically transparent and ellipsometry measurements reveal a large band-gap, undermining expectations of semi-metallic behavior. Density functional theory calculations predict an insulating antiferromagnetic ground state, in contrast to previous reports, and suggest potential frustration on the magnetic sublattice. Given the wide tunability of the alluaudite structure we consider ways to push the system closer to semi-metallic state.

cond-mat.str-el↗

arXiv2025

Efficient Solution and Learning of Robust Factored MDPs

Robust Markov decision processes (r-MDPs) extend MDPs by explicitly modelling epistemic uncertainty about transition dynamics. Learning r-MDPs from interactions with an unknown environment enables the synthesis of robust policies with provable (PAC) guarantees on performance, but this can require a large number of sample interactions. We propose novel methods for solving and learning r-MDPs based on factored state-space representations that leverage the independence between model uncertainty across system components. Although policy synthesis for factored r-MDPs leads to hard, non-convex optimisation problems, we show how to reformulate these into tractable linear programs. Building on these, we also propose methods to learn factored model representations directly. Our experimental results show that exploiting factored structure can yield dimensional gains in sample efficiency, producing more effective robust policies with tighter performance guarantees than state-of-the-art methods.

cs.LG↗

arXiv2025

Robust Probabilistic Bisimilarity for Labelled Markov Chains

Despite its prevalence, probabilistic bisimilarity suffers from a lack of robustness under minuscule perturbations of the transition probabilities. This can lead to discontinuities in the probabilistic bisimilarity distance function, undermining its reliability in practical applications where transition probabilities are often approximations derived from experimental data. Motivated by this limitation, we introduce the notion of robust probabilistic bisimilarity for labelled Markov chains, which ensures the continuity of the probabilistic bisimilarity distance function. We also propose an efficient algorithm for computing robust probabilistic bisimilarity and show that it performs well in practice, as evidenced by our experimental results.

cs.LO↗

arXiv2025

Learning Probabilistic Temporal Logic Specifications for Stochastic Systems

There has been substantial progress in the inference of formal behavioural specifications from sample trajectories, for example, using Linear Temporal Logic (LTL). However, these techniques cannot handle specifications that correctly characterise systems with stochastic behaviour, which occur commonly in reinforcement learning and formal verification. We consider the passive learning problem of inferring a Boolean combination of probabilistic LTL (PLTL) formulas from a set of Markov chains, classified as either positive or negative. We propose a novel learning algorithm that infers concise PLTL specifications, leveraging grammar-based enumeration, search heuristics, probabilistic model checking and Boolean set-cover procedures. We demonstrate the effectiveness of our algorithm in two use cases: learning from policies induced by RL algorithms and learning from variants of a probabilistic model. In both cases, our method automatically and efficiently extracts PLTL specifications that succinctly characterise the temporal differences between the policies or model variants.

cs.LO↗

arXiv2025

Planning with Linear Temporal Logic Specifications: Handling Quantifiable and Unquantifiable Uncertainty

This work studies the planning problem for robotic systems under both quantifiable and unquantifiable uncertainty. The objective is to enable the robotic systems to optimally fulfill high-level tasks specified by Linear Temporal Logic (LTL) formulas. To capture both types of uncertainty in a unified modelling framework, we utilise Markov Decision Processes with Set-valued Transitions (MDPSTs). We introduce a novel solution technique for the optimal robust strategy synthesis of MDPSTs with LTL specifications. To improve efficiency, our work leverages limit-deterministic B\"uchi automata (LDBAs) as the automaton representation for LTL to take advantage of their efficient constructions. To tackle the inherent nondeterminism in MDPSTs, which presents a significant challenge for reducing the LTL planning problem to a reachability problem, we introduce the concept of a Winning Region (WR) for MDPSTs. Additionally, we propose an algorithm for computing the WR over the product of the MDPST and the LDBA. Finally, a robust value iteration algorithm is invoked to solve the reachability problem. We validate the effectiveness of our approach through a case study involving a mobile robot operating in the hexagonal world, demonstrating promising efficiency gains.

cs.RO↗