arXiv subjects

David Parker

Publications and source records attributed to David Parker.

At least 73 records · Page 4Linked to original sources

arXiv2019

Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games

Probabilistic model checking for stochastic games enables formal verification of systems that comprise competing or collaborating entities operating in a stochastic environment. Despite good progress in the area, existing approaches focus on zero-sum goals and cannot reason about scenarios where entities are endowed with different objectives. In this paper, we propose probabilistic model checking techniques for concurrent stochastic games based on Nash equilibria. We extend the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards) to allow reasoning about players with distinct quantitative goals, which capture either the probability of an event occurring or a reward measure. We present algorithms to synthesise strategies that are subgame perfect social welfare optimal Nash equilibria, i.e., where there is no incentive for any players to unilaterally change their strategy in any state of the game, whilst the combined probabilities or rewards are maximised. We implement our techniques in the PRISM-games tool and apply them to several case studies, including network protocols and robot navigation, showing the benefits compared to existing approaches.

cs.LO↗

arXiv2018

Simultaneous Task Allocation and Planning Under Uncertainty

We propose novel techniques for task allocation and planning in multi-robot systems operating in uncertain environments. Task allocation is performed simultaneously with planning, which provides more detailed information about individual robot behaviour, but also exploits independence between tasks to do so efficiently. We use Markov decision processes to model robot behaviour and linear temporal logic to specify tasks and safety constraints. Building upon techniques and tools from formal verification, we show how to generate a sequence of multi-robot policies, iteratively refining them to reallocate tasks if individual robots fail, and providing probabilistic guarantees on the performance (and safe operation) of the team of robots under the resulting policy. We implement our approach and evaluate it on a benchmark multi-robot example.

cs.AI↗

arXiv2018

Single Crystal Permanent Magnet: Extraordinary Magnetic Behavior in the ta, Cu and Fe Substituted CeCo5 System

To reduce material and processing costs of commercial permanent magnets and to attempt to fill the empty niche of energy products, 10 - 20 MGOe, between low-flux (ferrites, alnico) and high-flux (Nd2Fe14B- and SmCo5-type) magnets, we report synthesis, structure, magnetic properties and modeling of Ta, Cu and Fe substituted CeCo5. Using a self-flux technique, we grew single crystals of I - Ce15.1Ta1.0Co74.4Cu9.5, II - Ce16.3Ta0.6Co68.9Cu14.2, III - Ce15.7Ta0.6Co67.8Cu15.9, IV - Ce16.3Ta0.3Co61.7Cu21.7 and V - Ce14.3Ta1.0Co62.0Fe12.3Cu10.4. X-ray diffraction analysis (XRD) showed that these materials retain a CaCu5 substructure and incorporate small amounts of Ta in the form of \dumb-bells", filling the 2e crystallographic sites within the 1D hexagonal channel with the 1a Ce site, whereas Co, Cu and Fe are statistically distributed among the 2c and 3g crystallographic sites. Scanning electron microscopy, energy dispersive X-ray spectroscopy (SEM-EDS) and scanning transmission electron microscopy (STEM) examinations provided strong evidence of the single-phase nature of the as-grown crystals, even though they readily exhibited significant magnetic coercivitie of ~1.6 - ~1.8 kOe caused by Co-enriched, nano-sized, structural defects and faults that can serve as pinning sites. Formation of the "composite crystal" during the heat treatment creates a 3D array of extended defects within a primarily single grain single crystal, which greatly improves its magnetic characteristics. Possible causes of the formation of the "composite crystal" may be associated with Ta atoms leaving matrix interstices at lower temperatures and/or matrix degradation induced by decreased miscibility at lower temperatures. Fe strongly improves both the Curie temperature and magnetization of the system resulting in (BH)max:~13 MGOe at room temperature.

cond-mat.mtrl-sci↗

arXiv2017

Quantum Oscillations in the Anomalous Spin Density Wave State of FeAs

Quantum oscillations in the binary antiferromagnetic metal FeAs are presented and compared to theoretical predictions for the electronic band structure in the anomalous spin density wave state of this material. Demonstrating a new method for growing single crystals out of Bi flux, we utilize the highest quality FeAs to perform torque magnetometry experiments up to 35 T, using rotations of field angle in two planes to provide evidence for one electron and one hole band in the magnetically ordered state. The resulting picture agrees with previous experimental evidence for multiple carriers at low temperatures, but the exact Fermi surface shape differs from predictions, suggesting that correlations play a role in deviation from ab initio theory and cause up to a four-fold enhancement in the effective carrier mass.

cond-mat.str-el↗

arXiv2017

Focus on Imaging Methods in Granular Physics

Granular materials are complex multi-particle ensembles in which macroscopic properties are largely determined by inter-particle interactions between their numerous constituents. In order to understand and to predict their macroscopic physical behavior, it is necessary to analyze the composition and interactions at the level of individual contacts and grains. To do so requires the ability to image individual particles and their local configurations to high precision. A variety of competing and complementary imaging techniques have been developed for that task. In this introductory paper accompanying the Focus Issue, we provide an overview of these imaging methods and discuss their advantages and drawbacks, as well as their limits of application.

physics.ins-det↗

arXiv2015

Metallicity of Ca2Cu6P5 with Single and Double Copper-Pnictide Layers

We report thermodynamic and transport properties, and also theoretical calculations, for Cu-based compound Ca2Cu6P5 and compare with CaCu(2-x)P2. Both materials have layers of edge-sharing copper pnictide tetrahedral CuP4, similar to Fe-As and Fe-Se layers (with FeAs4, FeSe4) in the iron-based superconductors. Despite the presence of this similar transition-metal pnictide layer, we find that both Ca2Cu6P5 and CaCu(2-x)P2 have temperature-independent magnetic susceptibility and show metallic behavior with no evidence of either magnetic ordering or superconductivity down to 1.8 K. CaCu(2-x)P2 is slightly off-stoichiometric, with delta = 0.14. Theoretical calculations suggest that unlike Fe 3d-based magnetic materials with a large density of states (DOS) at the Fermi surface, Cu have comparatively low DOS, with the majority of the 3d spectral weight located well below Fermi level. The room-temperature resistivity value of Ca2Cu6P5 is only 9 micro ohm-cm, due to a substantial plasma frequency and an inferred electron-phonon coupling lambda of 0.073 (significantly smaller than that of metallic Cu). Also, microscopy result shows that Cu-Cu distance along the c-axis within the double layers can be very short (2.5 A), even shorter than metallic elemental copper bond (2.56 A). The value of dp over dT for CaCu(2-x)P2 at 300 K is approximately three times larger than in Ca2Cu6P5, which suggests the likelihood of stronger electron-phonon coupling. This study shows that the details of Cu-P layers and bonding are important for their transport characteristics. In addition, it emphasizes the remarkable character of the DOS of '122' iron-based materials, despite much structural similarities.

cond-mat.supr-con↗

arXiv2015

Permissive Controller Synthesis for Probabilistic Systems

We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty system components. Our aim is to generate robust controllers that are resilient to unexpected system changes at runtime, and flexible enough to be adapted if additional constraints need to be imposed. We develop a permissive controller synthesis framework, which generates multi-strategies for the controller, offering a choice of control actions to take at each time step. We formalise the notion of permissivity using penalties, which are incurred each time a possible control action is disallowed by a multi-strategy. Permissive controller synthesis aims to generate a multi-strategy that minimises these penalties, whilst guaranteeing the satisfaction of a specified system property. We establish several key results about the optimality of multi-strategies and the complexity of synthesising them. Then, we develop methods to perform permissive controller synthesis using mixed integer linear programming and illustrate their effectiveness on a selection of case studies.

cs.LO↗

arXiv2015

Verification and Control of Partially Observable Probabilistic Real-Time Systems

We propose automated techniques for the verification and control of probabilistic real-time systems that are only partially observable. To formally model such systems, we define an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give a probabilistic temporal logic that can express a range of quantitative properties of these models, relating to the probability of an event's occurrence or the expected value of a reward measure. We then propose techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. Our approach is based on an integer discretisation of the model's dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however we show how both lower and upper bounds on numerical results can be generated. We illustrate the effectiveness of the approach by implementing it in the PRISM model checker and applying it to several case studies, from the domains of computer security and task scheduling.

cs.LO↗

arXiv2015

Benefits of Carrier Pocket Anisotropy to Thermoelectric Performance: The case of $p$-type AgBiSe$_2$

We study theoretically the effects of anisotropy on the thermoelectric performance of $p$-type AgBiSe$_2$. We present an apparent realization of the thermoelectric benefits of one-dimensional "plate-like" carrier pocket anisotropy in the valence band of this material. Based on first principles calculations we find a substantial anisotropy in the electronic structure, likely favorable for thermoelectric performance, in the valence bands of the hexagonal phase of the silver chalcogenide thermoelectric AgBiSe$_2$, while the conduction bands are more isotropic, and in our experiments do not attain high performance. AgBiSe$_2$ has already exhibited a $ZT$ value of 1.5 in a high-temperature disordered fcc phase, but room-temperature performance has not been demonstrated. We develop a theory for the ability of anisotropy to decouple the density-of-states and conductivity effective masses, pointing out the influence of this effect in the high performance thermoelectrics Bi$_2$Te$_3$ and PbTe. From our first principles and Boltzmann transport calculations we estimate the performance of $p$-type AgBiSe$_{2}$.

cond-mat.mtrl-sci↗

arXiv2015

Verification of Markov Decision Processes using Learning Algorithms

We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and 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, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model-checking for unbounded properties in MDPs. In contrast with other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular properties of the MDP. We also show how our techniques extend to LTL objectives. We present experimental results showing the performance of our framework on several examples.

cs.LO↗

arXiv2014

Connecting thermoelectric performance and topological-insulator behavior: Bi$_2$Te$_3$ and Bi$_{2}$Te$_{2}$Se from first principles

Thermoelectric performance is of interest for numerous applications such as waste heat recovery and solid state energy conversion, and will be seen to be closely connected to topological insulator behavior. In this context we here report first principles transport and defect calculations for Bi$_{2}$Te$_{2}$Se in relation to Bi$_{2}$Te$_{3}$. The two compounds are found to contain remarkably different electronic structures in spite of being isostructural and isoelectronic. We discuss these results in terms of the topological insulator characteristics of these compounds.

cond-mat.mtrl-sci↗

arXiv2013

Itinerant magnetism in doped semiconducting beta-FeSi2 and CrSi2

Novel or unusual magnetism is a subject of considerable interest, particularly in metals and degenerate semiconductors. In such materials the interplay of magnetism, transport and other Fermi liquid properties can lead to fascinating physical behavior. One example is in magnetic semiconductors, where spin polarized currents may be controlled and used. We report density functional calculations predicting magnetism in doped semiconducting beta-FeSi2 and CrSi2 at relatively low doping levels particularly for n-type. In this case, there is a rapid cross-over to a half-metallic state as a function of doping level. The results are discussed in relation to the electronic structure and other properties of these compounds.

cond-mat.mtrl-sci↗

arXiv2013

Importance of non-parabolic band effects in the thermoelectric properties of semiconductors

We present an analysis of the thermoelectric properties of of $n$-type GeTe and SnTe in relation to the lead chalcogenides PbTe and PbSe. We find that the singly degenerate conduction bands of semiconducting GeTe and SnTe are highly non-ellipsoidal, even very close to the band edges. This leads to isoenergy surfaces with a strongly corrugated shape that is clearly evident at carrier concentrations well below 0.005 $e$ per formula unit (7 - 9 $\times$ 10$^{19}$cm$^{-3}$ depending on material) Analysis within Boltzmann theory suggests that this corrugation may be favorable for the thermoelectric transport. Our calculations also indicate that values of the power factor for these two materials may well exceed those of PbTe and PbSe. As a result these materials may exhibit $n$-type performance exceeding that of the lead chalcogenides.

cond-mat.mtrl-sci↗

arXiv2013

Proton irradiation robustness of dielectric mirrors for high-finesse Fabry-Pérot resonators in the near-infrared spectral range

We demonstrate that a proton irradiation with fluences of $3.6\times10^{10}$/cm$^{2}$ at low energy ($<$ 36 MeV) and $1.46 \times 10^{10}$/cm$^{2}$ at high energy (40 MeV and 90 MeV combined) on the dielectric mirrors of Fabry-Pérot cavities with a finesse of about 700 000 causes less than 5% change in the finesse. Furthermore, no influence on the coupling efficiency to the cavities was observed, the efficiency being approximately 70%. The irradiation was carried out with a spectrum approximating the proton energy spectrum of a highly elliptic Earth orbit with duration of 5 years, proposed for the Space-Time Explorer and Quantum Equivalence Space Test (STE-QUEST) mission [\url{http://sci.esa.int/ste-quest/}].

physics.optics↗

arXiv2013

Thermoelectric properties of $β$-FeSi$_{\text2}$

We investigate the thermoelectric properties of $β$-FeSi$_{\text2}$ using first principles electronic structure and Boltzmann transport calculations. We report a high thermopower for both \textit{p}- and \textit{n}-type $β$-FeSi$_{\text2}$ over a wide range of carrier concentration and in addition find the performance for \textit{n}-type to be higher than for the \textit{p}-type. Our results indicate that, depending upon temperature, a doping level of 3$\times10{^{20}}$ - 2$\times10{^{21}}$ cm${^{-3}}$ may optimize the thermoelectric performance.

cond-mat.mtrl-sci↗

arXiv2013

Strategic Analysis of Trust Models for User-Centric Networks

We present a strategic analysis of a trust model that has recently been proposed for promoting cooperative behaviour in user-centric networks. The mechanism for cooperation is based on a combination of reputation and virtual currency schemes in which service providers reward paying customers and punish non-paying ones by adjusting their reputation, and hence the price they pay for services. We model and analyse this system using PRISM-games, a tool that performs automated verification and strategy synthesis for stochastic multi-player games using the probabilistic alternating-time temporal logic with rewards (rPATL). We construct optimal strategies for both service users and providers, which expose potential risks of the cooperation mechanism and which we use to devise improvements that counteract these risks.

cs.GT↗

arXiv2013

Potential thermoelectric performance of hole-doped Cu2O

High thermoelectric performance in oxides requires stable conductive materials that have suitable band structures. Here we show based on an analysis of the thermopower and related properties using first-principles calculations and Boltzmann transport theory that hole doped Cu2O may be such a material. We find that hole-doped Cu2O has a high thermopower of above 200 microV/K even with doping levels as high as 5.5x10 20 cm-3 at 500 K, mainly attributed to the heavy valence bands of Cu2O. This is reminiscent of the cobaltate family of high performance oxide thermoelectrics and implies that hole-doped Cu2O could be an excellent thermoelectric material if suitably doped.

cond-mat.mtrl-sci↗

arXiv2012

High three dimensional thermoelectric performance from low dimensional bands

Reduced dimensionality has long been regarded as an important strategy for increasing thermoelectric performance, for example in superlattices and other engineered structures. Here we point out and illustrate by examples that three dimensional bulk materials can be made to behave as if they were two dimensional from the point of view of thermoelectric performance. Implications for the discovery of new practical thermoelectrics are discussed.

cond-mat.mtrl-sci↗