arXiv subjects

David Parker

Publications and source records attributed to David Parker.

At least 19 recordsLinked to original sources

arXiv2026

Perturbation equivalence in labelled Markov chains

Behavioural equivalences, such as language equivalence and probabilistic bisimilarity, are fundamental techniques for reducing the size of probabilistic models. However, these equivalences are sensitive to the precise values of transition probabilities, making them unsuitable in applications where probabilities are subject to approximation. Motivated by settings in which the support graph of a labelled Markov chain is known but the transition probabilities are uncertain, we study robust variants of these equivalences. We introduce universal (perturbation) equivalence, which captures a variant of equivalence that is resilient to all perturbations of transition probabilities: two states or distributions are universally equivalent if they remain equivalent under every assignment of transition probabilities consistent with the support graph. We also consider the dual notion of existential (perturbation) equivalence, which holds whenever there exists an assignment of transition probabilities that yields equivalence. We establish that, for states, universal language equivalence coincides with universal probabilistic bisimilarity and develop a characterisation that yields a polynomial-time partition refinement algorithm. We implement the algorithm and demonstrate experimentally that it is effective as a technique for robust model reduction. We further show that universal language equivalence for distributions is closely related to the state case, and prove NL-completeness of deciding universal equivalence for both states and distributions. We prove that, for states, existential language equivalence coincides with existential probabilistic bisimilarity and deterministic witness transition functions always suffice, leading to an NP-completeness result. In contrast, we show that existential language equivalence for distributions is complete for the existential theory of the reals.

cs.LO↗

arXiv2026

Optimization-Based Robust Permissive Synthesis for Interval MDPs

We present an optimization-based framework for robust permissive synthesis for Interval Markov Decision Processes (IMDPs). While robust IMDP controller synthesis typically yields a single policy and most permissive-synthesis methods assume exact transition models, we synthesize multi-strategies that retain multiple actions while guaranteeing satisfaction of probabilistic reachability or expected-reward specifications under all admissible transition probabilities. We formulate the problem as a mixed-integer linear program (MILP) that maximizes the number of enabled state--action pairs subject to robust Bellman constraints. We develop two encodings: a direct vertex-enumeration formulation and a dualization-based formulation that avoids explicit enumeration of uncertainty-polytope vertices and has size linear in the number of successor transitions. Experiments on four benchmark domains show that both encodings achieve the same optimal permissiveness and scale to IMDPs with hundreds of thousands of states. Compared with standard robust single-policy synthesis, the resulting multi-strategies retain substantially more action choices.

cs.RO↗

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

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↗

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

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

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↗

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

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

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

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

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↗