Search

Markov decision processes (MDPs) are a standard model for sequential decision-making problems and are widely used across many scientific areas, including formal methods and artificial intelligence (AI). MDPs do, however, come with the restrictive assumption that the transition probabilities need to be precisely known. Robust MDPs (RMDPs) overcome this assumption by instead defining the transition probabilities to belong to some uncertainty set. We present a gentle survey on RMDPs, providing a tutorial covering their fundamentals. In particular, we discuss RMDP semantics and how to solve them by extending standard MDP methods such as value iteration and policy iteration. We also discuss how RMDPs relate to other models and how they are used in several contexts, including reinforcement learning and abstraction techniques. We conclude with some challenges for future work on RMDPs.

The kagome motif is a versatile platform for condensed matter physics, hosting rich interactions between magnetic, electronic, and structural degrees of freedom. In recent years, the discovery of a charge density wave (CDW) in the AV$_3$Sb$_5$ superconductors and structurally-derived bond density waves in FeGe and ScV$_6$Sn$_6$ have stoked the search for new kagome platforms broadly exhibiting density wave (DW) transitions. In this work, we evaluate the known AM$_6$X$_6$ chemistries and construct a stability diagram that summarizes the structural relationships between the $\approx$125 member family. Subsequently we introduce our discovery of the broader LnNb$_6$Sn$_6$ (Ln:Ce-Nd,Sm,Gd-Tm,Lu,Y) family of kagome metals and an analogous DW transition in LuNb$_6$Sn$_6$. Our X-ray scattering measurements clearly indicate a (1/3, 1/3, 1/3) ordering wave vector ($\sqrt{3}\times\sqrt{3}\times3$ superlattice) and diffuse scattering on half-integer $L$-planes. Our analysis of the structural data supports the ``rattling mode'' DW model proposed for ScV$_6$Sn$_6$ and paints a detailed picture of the steric interactions between the rare-earth filler element and the host Nb-Sn kagome scaffolding. We also provide a broad survey of the magnetic properties within the HfFe$_6$Ge$_6$-type LnNb$_6$Sn$_6$ members, revealing a number of complex antiferromagnetic and metamagnetic transitions throughout the family. This work integrates our new LnNb$_6$Sn$_6$ series of compounds into the broader AM$_6$X$_6$ family, providing new material platforms and forging a new route forward at the frontier of kagome metal research.

Game theory provides an effective way to model strategic interactions among rational agents. In the context of formal verification, these ideas can be used to produce guarantees on the correctness of multi-agent systems, with a diverse range of applications from computer security to autonomous driving. Psychological games (PGs) were developed as a way to model and analyse agents with belief-dependent motivations, opening up the possibility to model how human emotions can influence behaviour. In PGs, players' utilities depend not only on what actually happens (which strategies players choose to adopt), but also on what the players had expected to happen (their belief as to the strategies that would be played). Despite receiving much attention in fields such as economics and psychology, very little consideration has been given to their applicability to problems in computer science, nor to practical algorithms and tool support. In this paper, we start to bridge that gap, proposing methods to solve PGs and implementing them within PRISM-games, a formal verification tool for stochastic games. We discuss how to model these games, highlight specific challenges for their analysis and illustrate the usefulness of our approach on several case studies, including human behaviour in traffic scenarios.

We present a data-driven approach for producing policies that are provably robust across unknown stochastic environments. Existing approaches can learn models of a single environment as an interval Markov decision processes (IMDP) and produce a robust policy with a probably approximately correct (PAC) guarantee on its performance. However these are unable to reason about the impact of environmental parameters underlying the uncertainty. We propose a framework based on parametric Markov decision processes (MDPs) with unknown distributions over parameters. We learn and analyse IMDPs for a set of unknown sample environments induced by parameters. The key challenge is then to produce meaningful performance guarantees that combine the two layers of uncertainty: (1) multiple environments induced by parameters with an unknown distribution; (2) unknown induced environments which are approximated by IMDPs. We present a novel approach based on scenario optimisation that yields a single PAC guarantee quantifying the risk level for which a specified performance level can be assured in unseen environments, plus a means to trade-off risk and performance. We implement and evaluate our framework using multiple robust policy generation methods on a range of benchmarks. We show that our approach produces tight bounds on a policy's performance with high confidence.

The field of spintronics has seen a surge of interest in altermagnetism due to novel predictions and many possible applications. MnTe is a leading altermagnetic candidate that is of significant interest across spintronics due to its layered antiferromagnetic structure, high Neel temperature (TN ~ 310 K) and semiconducting properties. We present results on molecular beam epitaxy (MBE) grown MnTe/InP(111) films. Here, it is found that the electronic and magnetic properties are driven by the natural stoichiometry of MnTe. Electronic transport and in situ angle-resolved photoemission spectroscopy show the films are natively metallic with the Fermi level in the valence band and the band structure is in good agreement with first principles calculations for altermagnetic spin-splitting. Neutron diffraction confirms that the film is antiferromagnetic with planar anisotropy and polarized neutron reflectometry indicates weak ferromagnetism, which is linked to a slight Mn-richness that is intrinsic to the MBE grown samples. When combined with the anomalous Hall effect, this work shows that the electronic response is strongly affected by the ferromagnetic moment. Altogether, this highlights potential mechanisms for controlling altermagnetic ordering for diverse spintronic applications., Comment: Accepted in Advanced Functional Materials

The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.

Here we present the discovery and characterization of the kagome metal TbTi$_3$Bi$_4$ in tandem with a new series of compounds, the Ln$_{2-x}$Ti$_{6+x}$Bi$_9$ (Ln: Tb-Lu) shurikagome metals. We previously reported on the growth of the LnTi$_3$Bi$_4$ (Ln: La-Gd$^{3+}$, Eu$^{2+}$, Yb$^{2+}$) family, a chemically diverse and exfoliable series of kagome metals with complex and highly anisotropic magnetism. However, unlike the La-Gd analogs, TbTi$_3$Bi$_4$ cannot be synthesized by our previous methodology due to phase competition with Ln$_{2-x}$Ti$_{6+x}$Bi$_9$ (x$\sim$1.7-1.2). Here we discuss the phase competition between the LnTi$_3$Bi$_4$ and Ln$_{2-x}$Ti$_{6+x}$Bi$_9$ families, helping to frame the difficulty in synthesizing LnTi$_3$Bi$_4$ compounds with small Ln species and providing a strategy to circumvent formation of Ln$_{2-x}$Ti$_{6+x}$Bi$_9$. Detailed characterization of the magnetic and electronic transport properties on single crystals of TbTi$_3$Bi$_4$ reveals a highly complex landscape of magnetic phases arising from an antiferromagnetic ground state. A series of metamagnetic transitions creates at least 5 unique magnetic phase pockets, including a 1/3 and 2/3 magnetization plateau. Further, the system exhibits an intimate connection between the magnetism and magnetotransport, exhibiting sharp switching from positive (+40%) to negative magnetoresistance (-50%). Like the LnTi$_3$Bi$_4$ kagome metals, the Ln$_{2-x}$Ti$_{6+x}$Bi$_9$ family exhibits quasi-2D networks of titanium and chains of rare-earth. We present the structures and some basic magnetic properties of the Ln$_{2-x}$Ti$_{6+x}$Bi$_9$ family alongside our characterization of the newly discovered TbTi$_3$Bi$_4$.

Online planning for partially observable Markov decision processes (POMDPs) provides efficient techniques for robot decision-making under uncertainty. However, existing methods fall short of preventing safety violations in dynamic environments. This work presents a novel safe POMDP online planning approach that maximizes expected returns while providing probabilistic safety guarantees amidst environments populated by multiple dynamic agents. Our approach utilizes data-driven trajectory prediction models of dynamic agents and applies Adaptive Conformal Prediction (ACP) to quantify the uncertainties in these predictions. Leveraging the obtained ACP-based trajectory predictions, our approach constructs safety shields on-the-fly to prevent unsafe actions within POMDP online planning. Through experimental evaluation in various dynamic environments using real-world pedestrian trajectory data, the proposed approach has been shown to effectively maintain probabilistic safety guarantees while accommodating up to hundreds of dynamic agents.

We consider a variant of continuous-state partially-observable stochastic games with neural perception mechanisms and an asymmetric information structure. One agent has partial information, with the observation function implemented as a neural network, while the other agent is assumed to have full knowledge of the state. We present, for the first time, an efficient online method to compute an $\varepsilon$-minimax strategy profile, which requires only one linear program to be solved for each agent at every stage, instead of a complex estimation of opponent counterfactual values. For the partially-informed agent, we propose a continual resolving approach which uses lower bounds, pre-computed offline with heuristic search value iteration (HSVI), instead of opponent counterfactual values. This inherits the soundness of continual resolving at the cost of pre-computing the bound. For the fully-informed agent, we propose an inferred-belief strategy, where the agent maintains an inferred belief about the belief of the partially-informed agent based on (offline) upper bounds from HSVI, guaranteeing $\varepsilon$-distance to the value of the game at the initial belief known to both agents., Comment: 12 pages, 2 figures

We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{\'{a}}zdil et al., significantly extending it as well as refining several details and fixing errors. The presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios. The first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.

Stochastic games are a well established model for multi-agent sequential decision making under uncertainty. In practical applications, though, agents often have only partial observability of their environment. Furthermore, agents increasingly perceive their environment using data-driven approaches such as neural networks trained on continuous data. We propose the model of neuro-symbolic partially-observable stochastic games (NS-POSGs), a variant of continuous-space concurrent stochastic games that explicitly incorporates neural perception mechanisms. We focus on a one-sided setting with a partially-informed agent using discrete, data-driven observations and another, fully-informed agent. We present a new method, called one-sided NS-HSVI, for approximate solution of one-sided NS-POSGs, which exploits the piecewise constant structure of the model. Using neural network pre-image analysis to construct finite polyhedral representations and particle-based representations for beliefs, we implement our approach and illustrate its practical applicability to the analysis of pedestrian-vehicle and pursuit-evasion scenarios., Comment: 42 pages, 6 figures. Extended version of paper to be published in FM 2024

Partially observable Markov decision processes (POMDPs) have been widely used in many robotic applications for sequential decision-making under uncertainty. POMDP online planning algorithms such as Partially Observable Monte-Carlo Planning (POMCP) can solve very large POMDPs with the goal of maximizing the expected return. But the resulting policies cannot provide safety guarantees which are imperative for real-world safety-critical tasks (e.g., autonomous driving). In this work, we consider safety requirements represented as almost-sure reach-avoid specifications (i.e., the probability to reach a set of goal states is one and the probability to reach a set of unsafe states is zero). We compute shields that restrict unsafe actions which would violate the almost-sure reach-avoid specifications. We then integrate these shields into the POMCP algorithm for safe POMDP online planning. We propose four distinct shielding methods, differing in how the shields are computed and integrated, including factored variants designed to improve scalability. Experimental results on a set of benchmark domains demonstrate that the proposed shielding methods successfully guarantee safety (unlike the baseline POMCP without shielding) on large POMDPs, with negligible impact on the runtime for online planning.

When deploying classifiers in the real world, users expect them to respond to inputs appropriately. However, traditional classifiers are not equipped to handle inputs which lie far from the distribution they were trained on. Malicious actors can exploit this defect by making adversarial perturbations designed to cause the classifier to give an incorrect output. Classification-with-rejection methods attempt to solve this problem by allowing networks to refuse to classify an input in which they have low confidence. This works well for strongly adversarial examples, but also leads to the rejection of weakly perturbed images, which intuitively could be correctly classified. To address these issues, we propose Reed-Muller Aggregation Networks (RMAggNet), a classifier inspired by Reed-Muller error-correction codes which can correct and reject inputs. This paper shows that RMAggNet can minimise incorrectness while maintaining good correctness over multiple adversarial attacks at different perturbation budgets by leveraging the ability to correct errors in the classification process. This provides an alternative classification-with-rejection method which can reduce the amount of additional processing in situations where a small number of incorrect classifications are permissible., Comment: 38 pages, 7 figures

Probabilistic model checking can provide formal guarantees on the behavior of stochastic models relating to a wide range of quantitative properties, such as runtime, energy consumption or cost. But decision making is typically with respect to the expected value of these quantities, which can mask important aspects of the full probability distribution such as the possibility of high-risk, low-probability events or multimodalities. We propose a distributional extension of probabilistic model checking, applicable to discrete-time Markov chains (DTMCs) and Markov decision processes (MDPs). We formulate distributional queries, which can reason about a variety of distributional measures, such as variance, value-at-risk or conditional value-at-risk, for the accumulation of reward until a co-safe linear temporal logic formula is satisfied. For DTMCs, we propose a method to compute the full distribution to an arbitrary level of precision, based on a graph analysis and forward analysis of the model. For MDPs, we approximate the optimal policy with respect to expected value or conditional value-at-risk using distributional value iteration. We implement our techniques and investigate their performance and scalability across a range of benchmark models. Experimental results demonstrate that our techniques can be successfully applied to check various distributional properties of large probabilistic models., Comment: 21 pages, 2 pages appendix, 4 figures. In proceedings Nasa Formal Methods Symposium 2024. For associated Github repository, see https://github.com/davexparker/prism/tree/ingy

Here we present the family of titanium-based kagome metals of the form LnTi$_3$Bi$_4$ (Ln: La...Gd$^{3+}$, Eu$^{2+}$, Yb$^{2+}$). Single crystal growth methods are presented alongside detailed magnetic and thermodynamic measurements. The orthorhombic (Fmmm) LnTi$_3$Bi$_4$ family of compounds exhibit slightly distorted titanium-based kagome nets interwoven with zig-zag lanthanide-based (Ln) chains. Crystals are easily exfoliated parallel to the kagome sheets and angular resolved photoemission (ARPES) measurements highlight the intricacy of the electronic structure in these compounds, with Dirac points existing at the Fermi level. The magnetic properties and the associated anisotropy emerge from the quasi-1D zig-zag chains of Ln, and impart a wide array of magnetic ground states ranging from anisotropic ferromagnetism to complex antiferromagnetism with a cascade of metamagnetic transitions. Kagome metals continue to provide a rich direction for the exploration of magnetic, topologic, and highly correlated behavior. Our work here introduces the LnTi$_3$Bi$_4$ compounds to augment the continuously expanding suite of complex and interesting kagome materials.

Probabilistic model checking is a technique for formal automated reasoning about software or hardware systems that operate in the context of uncertainty or stochasticity. It builds upon ideas and techniques from a diverse range of fields, from logic, automata and graph theory, to optimisation, numerical methods and control. In recent years, probabilistic model checking has also been extended to integrate ideas from game theory, notably using models such as stochastic games and solution concepts such as equilibria, to formally verify the interaction of multiple rational agents with distinct objectives. This provides a means to reason flexibly about agents acting in either an adversarial or a collaborative fashion, and opens up opportunities to tackle new problems within, for example, artificial intelligence, robotics and autonomous systems. In this paper, we summarise some of the advances in this area, and highlight applications for which they have already been used. We discuss how the strengths of probabilistic model checking apply, or have the potential to apply, to the multi-agent setting and outline some of the key challenges required to make further progress in this field.

The increasing trend to integrate neural networks and conventional software components in safety-critical settings calls for methodologies for their formal modelling, verification and correct-by-construction policy synthesis. We introduce neuro-symbolic partially observable Markov decision processes (NS-POMDPs), a variant of continuous-state POMDPs with discrete observations and actions, in which the agent perceives a continuous-state environment using a neural {\revise perception mechanism} and makes decisions symbolically. The perception mechanism classifies inputs such as images and sensor values into symbolic percepts, which are used in decision making. We study the problem of optimising discounted cumulative rewards for NS-POMDPs. Working directly with the continuous state space, we exploit the underlying structure of the model and the neural perception mechanism to propose a novel piecewise linear and convex representation (P-PWLC) in terms of polyhedra covering the state space and value vectors, and extend Bellman backups to this representation. We prove the convexity and continuity of value functions and present two value iteration algorithms that ensure finite representability. The first is a classical (exact) value iteration algorithm extending the $\alpha$-functions of Porta {\em et al} (2006) to the P-PWLC representation for continuous-state spaces. The second is a point-based (approximate) method called NS-HSVI, which uses the P-PWLC representation and belief-value induced functions to approximate value functions from below and above for two types of beliefs, particle-based and region-based. Using a prototype implementation, we show the practical applicability of our approach on two case studies that employ (trained) ReLU neural networks as perception functions, by synthesising (approximately) optimal strategies., Comment: 65 pages, 14 figures

The kagome lattice can host exotic magnetic phases arising from frustrated and competing magnetic interactions. However, relatively few insulating kagome materials exhibit incommensurate magnetic ordering. Here, we present a study of the magnetic structures and interactions of antiferromagnetic Na$_2$Mn$_3$Cl$_8$ with an undistorted Mn$^{2+}$ kagome network. Using neutron-diffraction and bulk magnetic measurements, we show that Na$_2$Mn$_3$Cl$_8$ hosts two different incommensurate magnetic states, which develop at $T_{N1} = 1.6$ K and $T_{N2} = 0.6$ K. Magnetic Rietveld refinements indicate magnetic propagation vectors of the form $\mathbf{q} = (q_{x},q_{y},\frac{3}{2})$, and our neutron-diffraction data can be well described by cycloidal magnetic structures. By optimizing exchange parameters against magnetic diffuse-scattering data, we show that the spin Hamiltonian contains ferromagnetic nearest-neighbor and antiferromagnetic third-neighbor Heisenberg interactions, with a significant contribution from long-ranged dipolar coupling. This experimentally-determined interaction model is compared with density-functional-theory simulations. Using classical Monte Carlo simulations, we show that these competing interactions explain the experimental observation of multiple incommensurate magnetic phases and may stabilize multi-$\mathbf{q}$ states. Our results expand the known range of magnetic behavior on the kagome lattice., Comment: 13 pages, 8 figures

Controllers for dynamical systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modeled as process noise in a dynamical system, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distribution. We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions. In particular, we address the problem of computing a controller that provides probabilistic guarantees on safely reaching a target, while also avoiding unsafe regions of the state space. First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states. As a key contribution, we adapt tools from the scenario approach to compute probably approximately correct (PAC) bounds on these transition probabilities, based on a finite number of samples of the noise. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP). This iMDP is, with a user-specified confidence probability, robust against uncertainty in the transition probabilities, and the tightness of the probability intervals can be controlled through the number of samples. We use state-of-the-art verification techniques to provide guarantees on the iMDP and compute a controller for which these guarantees carry over to the original control system. In addition, we develop a tailored computational scheme that reduces the complexity of the synthesis of these guarantees on the iMDP. Benchmarks on realistic control systems show the practical applicability of our method, even when the iMDP has hundreds of millions of transitions., Comment: To appear in the Journal of Artificial Intelligence Research (JAIR). arXiv admin note: text overlap with arXiv:2110.12662

Identifying and characterizing new magnetic systems with Co2+ ions can enhance our understanding of quantum behavior since Co2+ can host a pseudospin-1/2 magnetic ground state. Understanding the magnetic ground state and the phase diagrams of such systems are central to the development of new theoretical models to described emergent quantum properties of complex magnetic systems. The sawtooth chain compound, CsCo2MoO4_2OH, is one such complex magnetic system and here, we present a comprehensive series of magnetic and neutron scattering measurements to determine its magnetic phase diagram. The magnetic properties of CsCo2MoO4_2OH exhibit a strong coupling to the crystal lattice and its magnetic ground state can be easily manipulated by applied magnetic fields. There are two unique Co2+ ions, base and vertex, with Jbb and Jbv magnetic exchange. The magnetism is highly anisotropic with the b-axis (chain) along the easy axis and the material orders antiferromagnetically at TN = 5 K. The zero field antiferromagnetic phase contains vertex magnetic vectors Co1 aligned parallel to the b-axis, while the base vectors Co2 are canted by 34 and aligned in an opposite direction to the vertex vectors. The spins in parallel adjacent chains align in opposite directions, creating an overall antiferromagnetic structure. At a 3 kOe applied magnetic field, adjacent chains flip by 180{\deg} to generate a ferrimagnetic phase. An increase in field gradually induces the Co(1) moment to rotate along the b-axis and align in the same direction with Co2 generating a ferromagnetic structure. Our results demonstrate that the CsCo2MoO4_2OH is a promising candidate to study new physics associated with sawtooth chain magnetism.

Stochastic games are a convenient formalism for modelling systems that comprise rational agents competing or collaborating within uncertain environments. Probabilistic model checking techniques for this class of models allow us to formally specify quantitative specifications of either collective or individual behaviour and then automatically synthesise strategies for the agents under which these specifications are guaranteed to be satisfied. Although good progress has been made on algorithms and tool support, efficiency and scalability remain a challenge. In this paper, we investigate a symbolic implementation based on multi-terminal binary decision diagrams. We describe how to build and verify turn-based stochastic games against either zero-sum or Nash equilibrium based temporal logic specifications. We collate a set of benchmarks for this class of games, and evaluate the performance of our approach, showing that it is superior in a number of cases and that strategies synthesised in a symbolic fashion can be considerably more compact.

Network systems often contain vulnerabilities that remain unfixed in a network for various reasons, such as the lack of a patch or knowledge to fix them. With the presence of such residual vulnerabilities, the network administrator should properly react to the malicious activities or proactively prevent them, by applying suitable countermeasures that minimize the likelihood of an attack by the attacker. In this paper, we propose a stochastic game-theoretic approach for analyzing network security and synthesizing defense strategies to protect a network. To support analysis under partial observation, where some of the attacker's activities are unobservable or undetectable by the defender, we construct a one-sided partially observable security game and transform it into a perfect game for further analysis. We prove that this transformation is sound for a sub-class of security games and a subset of properties specified in the logic rPATL. We implement a prototype that fully automates our approach, and evaluate it by conducting experiments on a real-life network.

We propose svMorph, a framework for interactive virtual sculpting of patient-specific vascular anatomic models. Our framework includes three tools for the creation of tortuosity, aneurysms, and stenoses in tubular vascular geometries. These shape edits are performed via geometric operations on the surface mesh and vessel centerline curves of the input model. The tortuosity tool also uses the physics-based Oriented Particles method, coupled with linear blend skinning, to achieve smooth, elastic-like deformations. Our tools can be applied separately or in combination to produce simulation-suitable morphed models. They are also compatible with popular vascular modeling software, such as SimVascular. To illustrate our tools, we morph several image-based, patient-specific models to create a range of shape changes and simulate the resulting hemodynamics via three-dimensional, computational fluid dynamics. We also demonstrate the ability to quickly estimate the hemodynamic effects of the shape changes via automated generation of associated zero-dimensional lumped-parameter models.

While certain magnetic sublattices have long been known theoretically to give rise to emergent physics via competing magnetic interactions and quantum effects, finding such configurations in real materials is often deeply challenging. Here we report the synthesis and characterization of a new such material, NaCo2(SeO3)2(OH) which crystallizes with a highly frustrated sublattice of sawtooth Co2+ chains. Single crystals of NaCo2(SeO3)2(OH) were synthesized using a low-temperature hydrothermal method. X-ray single crystal structure analysis reveals that the material crystallizes in orthorhombic space group of Pnma (no. 62). Its crystal structure exhibits one-dimensional chains of corner-sharing isosceles triangles that are made of two crystallographically distinct 3d7 Co2+ sites (Co(1) and Co(2)). The chains run along the b-axis and are interconnected via [SeO3] groups to form a three-dimensional structure mediating super-exchange interactions. The temperature dependent magnetization data show a ferromagnetic-like (FM) transition at 11 K (T1) followed by an antiferromagnetic (AFM) transition at about 6 K (T2). Neutron-powder diffraction measurements reveal that at T1 = 11 K only Co(2) site orders magnetically, forming ferromagnetic zigzag chains along the b-axis. Below T2 = 6 K, both Co(1) and Co(2) sites order in an nearly orthogonal configuration, with Co(1) moments lying inside the plane of the sawtooth chain while Co(2) moments cant out of the plane. The canting of the magnetic moments leads to a net ferromagnetic component along b-axis, parallel to the chain direction. The ordered moments are fully compensated in the ac-plane., Comment: N/A

Game-theoretic concepts have been extensively studied in economics to provide insight into competitive behaviour and strategic decision making. As computing systems increasingly involve concurrently acting autonomous agents, game-theoretic approaches are becoming widespread in computer science as a faithful modelling abstraction. These techniques can be used to reason about the competitive or collaborative behaviour of multiple rational agents with distinct goals or objectives. This paper provides an overview of recent advances in developing a modelling, verification and strategy synthesis framework for concurrent stochastic games implemented in the probabilistic model checker PRISM-games. This is based on a temporal logic that supports finite- and infinite-horizon temporal properties in both a zero-sum and nonzero-sum setting, the latter using Nash and correlated equilibria with respect to two optimality criteria, social welfare and social fairness. We summarise the key concepts, logics and algorithms and the currently available tool support. Future challenges and recent progress in adapting the framework and algorithmic solutions to continuous environments and neural networks are also outlined., Comment: 22 pages, 7 figures

Markov decision processes (MDPs) are formal models commonly used in sequential decision-making. MDPs capture the stochasticity that may arise, for instance, from imprecise actuators via probabilities in the transition function. However, in data-driven applications, deriving precise probabilities from (limited) data introduces statistical errors that may lead to unexpected or undesirable outcomes. Uncertain MDPs (uMDPs) do not require precise probabilities but instead use so-called uncertainty sets in the transitions, accounting for such limited data. Tools from the formal verification community efficiently compute robust policies that provably adhere to formal specifications, like safety constraints, under the worst-case instance in the uncertainty set. We continuously learn the transition probabilities of an MDP in a robust anytime-learning approach that combines a dedicated Bayesian inference scheme with the computation of robust policies. In particular, our method (1) approximates probabilities as intervals, (2) adapts to new data that may be inconsistent with an intermediate model, and (3) may be stopped at any time to compute a robust policy on the uMDP that faithfully captures the data so far. Furthermore, our method is capable of adapting to changes in the environment. We show the effectiveness of our approach and compare it to robust policies computed on uMDPs learned by the UCRL2 reinforcement learning algorithm in an experimental evaluation on several benchmarks., Comment: Accepted at NeurIPS 2022

We present novel techniques for neuro-symbolic concurrent stochastic games, a recently proposed modelling formalism to represent a set of probabilistic agents operating in a continuous-space environment using a combination of neural network based perception mechanisms and traditional symbolic methods. To date, only zero-sum variants of the model were studied, which is too restrictive when agents have distinct objectives. We formalise notions of equilibria for these models and present algorithms to synthesise them. Focusing on the finite-horizon setting, and (global) social welfare subgame-perfect optimality, we consider two distinct types: Nash equilibria and correlated equilibria. We first show that an exact solution based on backward induction may yield arbitrarily bad equilibria. We then propose an approximation algorithm called frozen subgame improvement, which proceeds through iterative solution of nonlinear programs. We develop a prototype implementation and demonstrate the benefits of our approach on two case studies: an automated car-parking system and an aircraft collision avoidance system., Comment: 14 pages, 7 figures

The notion that phonons can carry pseudo-angular momentum has become popular in the last decade, with recent research efforts highlighting phonon chirality, Berry curvature of phonon band structure, and the phonon Hall effect. When a phonon is resonantly coupled to a crystal electric field excitation, a so-called vibronic bound state forms. Here, we observe angular momentum transfer of $\delta$Jz = $\pm$1$\hbar$ between phonons and an orbital state in a vibronic bound state of a candidate quantum spin liquid. This observation has profound implications for the engineering of phonon band structure topology through chiral quasiparticle interactions., Comment: 29 pages, 10 figures