BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

David Parker

David Parker appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
cond-mat.mtrl-sciLogic in Computer ScienceArtificial IntelligenceComputer Science and Game Theorycond-mat.supr-conquant-phcond-mat.str-elFormal Languages and Automata TheoryMachine Learningcond-mat.mes-hallcond-mat.otherhep-thHuman-Computer Interactionmath-phmath.MPMultiagent Systemsphysics.ins-detphysics.opticsSoftware EngineeringSystems and Control

Catalog footprint

What is connected

33works
20topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

33 published item(s)

preprint2026arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2026arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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/}].

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Acoustic impedance and interface phonon scattering in Bi$_2$Te$_3$ and other semiconducting materials

We present first principles calculations of the phonon dispersions of Bi2Te3 and discuss these in relation to the acoustic phonon interface scattering in ceramics. The phonon dispersions show agreement with what is known from neutron scattering for the optic modes. We find a difference between the generalized gradient approximation and local density results for the acoustic branches. This is a consequence of an artificial compression of the van der Waals bonded gaps in the Bi2Te3 structure when using the generalized gradient approximation. As a result local density approximation calculations provide a better description of the phonon dispersions in Bi$_{2}$Te$_{3}$. A key characteristic of the acoustic dispersions is the existence of a strong anisotropy in the velocities. We develop a model for interface scattering in ceramics with acoustic wave anisotropy and apply this to Bi2Te3 and compare with PbTe and diamond.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Observation of PT phase transition in a simple mechanical system

If a Hamiltonian is PT symmetric, there are two possibilities: Either the eigenvalues are entirely real, in which case the Hamiltonian is said to be in an unbroken-PT-symmetric phase, or else the eigenvalues are partly real and partly complex, in which case the Hamiltonian is said to be in a broken-PT-symmetric phase. As one varies the parameters of the Hamiltonian, one can pass through the phase transition that separates the unbroken and broken phases. This transition has recently been observed in a variety of laboratory experiments. This paper explains the phase transition in a simple and intuitive fashion and then describes an extremely elementary experiment in which the phase transition is easily observed.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Pareto Curves for Probabilistic Model Checking

Multi-objective probabilistic model checking provides a way to verify several, possibly conflicting, quantitative properties of a stochastic system. It has useful applications in controller synthesis and compositional probabilistic verification. However, existing methods are based on linear programming, which limits the scale of systems that can be analysed and makes verification of time-bounded properties very difficult. We present a novel approach that addresses both of these shortcomings, based on the generation of successive approximations of the Pareto curve for a multi-objective model checking problem. We illustrate dramatic improvements in efficiency on a large set of benchmarks and show how the ability to visualise Pareto curves significantly enhances the quality of results obtained from current probabilistic verification tools.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Thermoelectric properties of AgGaTe$_2$ and related chalcopyrite structure materials

We present an analysis of the potential thermoelectric performance of p-type AgGaTe$_{2}$, which has already shown a $ZT$ of 0.8 with partial optimization, and observe that the same band structure features, such as a mixture of light and heavy bands and isotropic transport, that lead to this good performance are present in certain other ternary chalcopyrite structure semiconductors. We find that optimal performance of AgGaTe$_2$ will be found for hole concentrations between 4 $\times 10^{19}$ and 2 $\times 10^{20}$cm$^{-3}$ at 900 K, and 2 $\times 10^{19}$ and 10$^{20}$ cm$^{-3}$ at 700 K, and that certain other chalcopyrite semiconductors might show good thermoelectric performance at similar doping ranges and temperatures if not for higher lattice thermal conductivity.

0 citations0 reviewsNo code linkedOpen access
preprint2009arXiv

Incommensurate spin resonance in URu2Si2

We focus on inelastic neutron scattering in $URu_2Si_2$ and argue that observed gap in the fermion spectrum naturally leads to the spin feature observed at energies $ω_{res} = 4-6 meV$ at momenta at $\bQ^* = (1\pm 0.4, 0,0)$. We discuss how spin features seen in $URu_2Si_2$ can indeed be thought of in terms of {\em spin resonance} that develops in HO state and is {\em not related} to superconducting transition at 1.5K. In our analysis we assume that the HO gap is due to a particle-hole condensate that connects nested parts of the Fermi surface with nesting vector $\bf{Q}^* $. Within this approach we can predicted the behavior of the spin susceptibility at $\bQ^*$ and find it to be is strikingly similar to the phenomenology of resonance peaks in high-T$_c$ and heavy fermion superconductors. The energy of the resonance peak scales with $T_{HO}$ $ω_{res} \simeq 4 k_BT_{HO}$. We discuss observable consequences spin resonance will have on neutron scattering and local density of states.

0 citations0 reviewsNo code linkedOpen access
preprint2009arXiv

Possible phase-sensitive tests of pairing symmetry in pnictide superconductors

The discovery of the new class of pnictide superconductors has engendered a controversy about their pairing symmetry, with proposals ranging from an extended s-wave or "s$_{\pm}$" symmetry to nodal or nodeless d-wave symmetry to still more exotic order parameters such as p-wave. In this paper, building on the earlier, similar work performed for the cuprates, we propose several phase-sensitive Josephson interferometry experiments, each of which may allow resolution of the issue.

0 citations0 reviewsNo code linkedOpen access
preprint2006arXiv

Small $T_1^{-1}$ coherence peak near $T_c$ in unconventional superconductors

It is usually believed that a coherence peak just below T$_{c}$ in the nuclear spin lattice relaxation rate T$_{1}^{-1}$ in superconducting materials is a signature of conventional s-wave pairing. In this paper we demonstrate that any unconventional superconductor obeying BCS pure-case weak-coupling theory should show a small T$_{1}^{-1}$ coherence peak near T$_{c}$, generally with a height between 3 and 15 percent greater than the normal state T$_{1}^{-1}$ at T$_{c}$. It is largely due to impurity effects that this peak has not commonly been observed.

0 citations0 reviewsNo code linkedOpen access