arXiv subjects

David Parker

Publications and source records attributed to David Parker.

At least 55 records · Page 3Linked to original sources

arXiv2022

Symbolic Verification and Strategy Synthesis for Turn-based Stochastic Games

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.

cs.LO↗

arXiv2022

Partially-Observable Security Games for Automating Attack-Defense Analysis

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.

cs.CR↗

arXiv2022

Planning for Automated Vehicles with Human Trust

Recent work has considered personalized route planning based on user profiles, but none of it accounts for human trust. We argue that human trust is an important factor to consider when planning routes for automated vehicles. This paper presents a trust-based route planning approach for automated vehicles. We formalize the human-vehicle interaction as a partially observable Markov decision process (POMDP) and model trust as a partially observable state variable of the POMDP, representing the human's hidden mental state. We build data-driven models of human trust dynamics and takeover decisions, which are incorporated in the POMDP framework, using data collected from an online user study with 100 participants on the Amazon Mechanical Turk platform. We compute optimal routes for automated vehicles by solving optimal policies in the POMDP planning, and evaluate the resulting routes via human subject experiments with 22 participants on a driving simulator. The experimental results show that participants taking the trust-based route generally reported more positive responses in the after-driving survey than those taking the baseline (trust-free) route. In addition, we analyze the trade-offs between multiple planning objectives (e.g., trust, distance, energy consumption) via multi-objective optimization of the POMDP. We also identify a set of open issues and implications for real-world deployment of the proposed approach in automated vehicles.

cs.HC↗

arXiv2022

Probabilistic Model Checking for Strategic Equilibria-based Decision Making: Advances and Challenges

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.

cs.FL↗

arXiv2022

Finite-horizon Equilibria for Neuro-symbolic Concurrent Stochastic Games

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.

cs.GT↗

arXiv2022

Verified Probabilistic Policies for Deep Reinforcement Learning

Deep reinforcement learning is an increasingly popular technique for synthesising policies to control an agent's interaction with its environment. There is also growing interest in formally verifying that such policies are correct and execute safely. Progress has been made in this area by building on existing work for verification of deep neural networks and of continuous-state dynamical systems. In this paper, we tackle the problem of verifying probabilistic policies for deep reinforcement learning, which are used to, for example, tackle adversarial environments, break symmetries and manage trade-offs. We propose an abstraction approach, based on interval Markov decision processes, that yields probabilistic guarantees on a policy's execution, and present techniques to build and solve these models using abstract interpretation, mixed-integer linear programming, entropy-based refinement and probabilistic model checking. We implement our approach and illustrate its effectiveness on a selection of reinforcement learning benchmarks.

cs.AI↗

arXiv2022

Phonon Chirality Induced by Vibronic-Orbital Coupling

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 $δ$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.

cond-mat.mes-hall↗

arXiv2022

Multi-Objective Controller Synthesis with Uncertain Human Preferences

Complex real-world applications of cyber-physical systems give rise to the need for multi-objective controller synthesis, which concerns the problem of computing an optimal controller subject to multiple (possibly conflicting) criteria. The relative importance of objectives is often specified by human decision-makers. However, there is inherent uncertainty in human preferences (e.g., due to artifacts resulting from different preference elicitation methods). In this paper, we formalize the notion of uncertain human preferences and present a novel approach that accounts for this uncertainty in the context of multi-objective controller synthesis for Markov decision processes (MDPs). Our approach is based on mixed-integer linear programming and synthesizes an optimally permissive multi-strategy that satisfies uncertain human preferences with respect to a multi-objective property. Experimental results on a range of large case studies show that the proposed approach is feasible and scalable across varying MDP model sizes and uncertainty levels of human preferences. Evaluation via an online user study also demonstrates the quality and benefits of the synthesized controllers.

cs.AI↗

arXiv2022

Correlated Equilibria and Fairness in Concurrent Stochastic Games

Game-theoretic techniques and equilibria analysis facilitate the design and verification of competitive systems. While algorithmic complexity of equilibria computation has been extensively studied, practical implementation and application of game-theoretic methods is more recent. Tools such as PRISM-games support automated verification and synthesis of zero-sum and (epsilon-optimal subgame-perfect) social welfare Nash equilibria properties for concurrent stochastic games. However, these methods become inefficient as the number of agents grows and may also generate equilibria that yield significant variations in the outcomes for individual agents. Instead, we consider correlated equilibria, in which players can coordinate through public signals, and introduce an alternative optimality criterion of social fairness, which can be applied to both Nash and correlated equilibria. We show that correlated equilibria are easier to compute, are more equitable, and can also improve joint outcomes. We implement algorithms for both normal form games and the more complex case of multi-player concurrent stochastic games with temporal logic specifications.

cs.GT↗

arXiv2021

Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise

Controllers for autonomous systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modelled as process noise, 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 planning 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. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between 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 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 autonomous system. Realistic benchmarks show the practical applicability of our method, even when the iMDP has millions of states or transitions.

eess.SY↗

arXiv2021

Probabilistic Model Checking and Autonomy

Design and control of autonomous systems that operate in uncertain or adversarial environments can be facilitated by formal modelling and analysis. Probabilistic model checking is a technique to automatically verify, for a given temporal logic specification, that a system model satisfies the specification, as well as to synthesise an optimal strategy for its control. This method has recently been extended to multi-agent systems that exhibit competitive or cooperative behaviour modelled via stochastic games and synthesis of equilibria strategies. In this paper, we provide an overview of probabilistic model checking, focusing on models supported by the PRISM and PRISM-games model checkers. This includes fully observable and partially observable Markov decision processes, as well as turn-based and concurrent stochastic games, together with associated probabilistic temporal logics. We demonstrate the applicability of the framework through illustrative examples from autonomous systems. Finally, we highlight research challenges and suggest directions for future work in this area.

cs.LO↗

arXiv2021

Nearly-Resonant Crystalline-Phononic Coupling in Quantum Spin Liquid Candidate CsYbSe$_2$

CsYbSe$_2$, a recently identified quantum spin liquid (QSL) candidate, exhibits strong crystal electric field (CEF) excitations. Here, we identify phonon and CEF modes with Raman spectroscopy and observe strong CEF-phonon mixing resulting in a vibronic bound state. Complex, mesoscale interplay between phonon modes and CEF modes is observed in real space, and an unexpected nearly resonant condition is satisfied, yielding up to fifth-order combination modes, with a total of 17 modes identified in the spectra. This study paves the way to coherent control of possible QSL ground states with optically accessible CEF-phonon manifolds and mesoscale engineering of CEF-phonon interactions.

cond-mat.str-el↗

arXiv2021

Canted antiferromagnetic order and spin dynamics in the honeycomb-lattice Tb2Ir3Ga9

Single crystal neutron diffraction, inelastic neutron scattering, bulk magnetization measurements, and first-principles calculations are used to investigate the magnetic properties of the honeycomb lattice $\rm Tb_2Ir_3Ga_9$. While the $R\ln2$ magnetic contribution to the low-temperature entropy indicates a $\rm J_{eff}=1/2$ moment for the lowest-energy crystal-field doublet, the Tb$^{3+}$ ions form a canted antiferromagnetic structure below 12.5 K. Due to the Dzyalloshinskii-Moriya interactions, the Tb moments in the $ab$ plane are slightly canted towards $b$ by $6^\circ$ with a canted moment of 1.22 $μ_{\rm B} $ per formula unit. A minimal $xxz$ spin Hamiltonian is used to simultaneously fit the spin-wave frequencies along the high symmetry directions and the field dependence of the magnetization along the three crystallographic axes. Long-range magnetic interactions for both in-plane and out-of-plane couplings up to the second nearest neighbors are needed to account for the observed static and dynamic properties. The $z$ component of the exchange interactions between Tb moments are larger than the $x$ and $y$ components. This compound also exhibits bond-dependent exchange with negligible nearest exchange coupling between moments parallel and perpendicular to the 4$f$ orbitals. Despite the $J_{\rm eff}=1/2$ moments, the spin Hamiltonian is denominated by a large in-plane anisotropy $K_z \sim -1$ meV. DFT calculations confirm the antiferromagnetic ground state and the substantial inter-plane coupling at larger Tb-Tb distances.

cond-mat.str-el↗

arXiv2020

Automatic Verification of Concurrent Stochastic Systems

Automated verification techniques for stochastic games allow formal reasoning about systems that feature competitive or collaborative behaviour among rational agents in uncertain or probabilistic settings. Existing tools and techniques focus on turn-based games, where each state of the game is controlled by a single player, and on zero-sum properties, where two players or coalitions have directly opposing objectives. In this paper, we present automated verification techniques for concurrent stochastic games (CSGs), which provide a more natural model of concurrent decision making and interaction. We also consider (social welfare) Nash equilibria, to formally identify scenarios where two players or coalitions with distinct goals can collaborate to optimise their joint performance. We propose an extension of the temporal logic rPATL for specifying quantitative properties in this setting and present corresponding algorithms for verification and strategy synthesis for a variant of stopping games. For finite-horizon properties the computation is exact, while for infinite-horizon it is approximate using value iteration. For zero-sum properties it requires solving matrix games via linear programming, and for equilibria-based properties we find social welfare or social cost Nash equilibria of bimatrix games via the method of labelled polytopes through an SMT encoding. We implement this approach in PRISM-games, which required extending the tool's modelling language for CSGs, and apply it to case studies from domains including robotics, computer security and computer networks, explicitly demonstrating the benefits of both CSGs and equilibria-based properties.

cs.LO↗

arXiv2020

Multi-player Equilibria Verification for Concurrent Stochastic Games

Concurrent stochastic games (CSGs) are an ideal formalism for modelling probabilistic systems that feature multiple players or components with distinct objectives making concurrent, rational decisions. Examples include communication or security protocols and multi-robot navigation. Verification methods for CSGs exist but are limited to scenarios where agents or players are grouped into two coalitions, with those in the same coalition sharing an identical objective. In this paper, we propose multi-coalitional verification techniques for CSGs. We use subgame-perfect social welfare (or social cost) optimal Nash equilibria, which are strategies where there is no incentive for any coalition to unilaterally change its strategy in any game state, and where the total combined objectives are maximised (or minimised). We present an extension of the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards) to specify equilibria-based properties for any number of distinct coalitions, and a corresponding model checking algorithm for a variant of stopping games. We implement our techniques in the PRISM-games tool and apply them to several case studies, including a secret sharing protocol and a public good game.

cs.LO↗

arXiv2020

Failure Mode Reasoning in Model Based Safety Analysis

Failure Mode Reasoning (FMR) is a novel approach for analyzing failure in a Safety Instrumented System (SIS). The method uses an automatic analysis of an SIS program to calculate potential failures in parts of the SIS. In this paper we use a case study from the power industry to demonstrate how FMR can be utilized in conjunction with other model-based safety analysis methods, such as HiP-HOPS and CFT, in order to achieve a comprehensive safety analysis of SIS. In this case study, FMR covers the analysis of SIS inputs while HiP-HOPS/CFT models the faults of logic solver and final elements. The SIS program is analyzed by FMR and the results are exported to HiP-HOPS/CFT via automated interfaces. The final outcome is the collective list of SIS failure modes along with their reliability measures. We present and review the results from both qualitative and quantitative perspectives.

cs.SE↗

arXiv2020

Probabilistic Guarantees for Safe Deep Reinforcement Learning

Deep reinforcement learning has been successfully applied to many control tasks, but the application of such agents in safety-critical scenarios has been limited due to safety concerns. Rigorous testing of these controllers is challenging, particularly when they operate in probabilistic environments due to, for example, hardware faults or noisy sensors. We propose MOSAIC, an algorithm for measuring the safety of deep reinforcement learning agents in stochastic settings. Our approach is based on the iterative construction of a formal abstraction of a controller's execution in an environment, and leverages probabilistic model checking of Markov decision processes to produce probabilistic guarantees on safe behaviour over a finite time horizon. It produces bounds on the probability of safe operation of the controller for different initial configurations and identifies regions where correct behaviour can be guaranteed. We implement and evaluate our approach on agents trained for several benchmark control problems.

cs.AI↗

arXiv2019

Verification and Control of Turn-Based Probabilistic Real-Time Games

Quantitative verification techniques have been developed for the formal analysis of a variety of probabilistic models, such as Markov chains, Markov decision process and their variants. They can be used to produce guarantees on quantitative aspects of system behaviour, for example safety, reliability and performance, or to help synthesise controllers that ensure such guarantees are met. We propose the model of turn-based probabilistic timed multi-player games, which incorporates probabilistic choice, real-time clocks and nondeterministic behaviour across multiple players. Building on the digital clocks approach for the simpler model of probabilistic timed automata, we show how to compute the key measures that underlie quantitative verification, namely the probability and expected cumulative price to reach a target. We illustrate this on case studies from computer security and task scheduling.

cs.LO↗