TY - GEN AB - Two-player games on graphs are central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this work we consider solving recursive game graphs (or pushdown game graphs) that can model the control flow of sequential programs with recursion. While pushdown games have been studied before with qualitative objectives, such as reachability and ω-regular objectives, in this work we study for the first time such games with the most well-studied quantitative objective, namely, mean-payoff objectives. In pushdown games two types of strategies are relevant: (1) global strategies, that depend on the entire global history; and (2) modular strategies, that have only local memory and thus do not depend on the context of invocation, but only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two- player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP- hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games; and memoryless modular strategies are sufficient in two- player pushdown games. Finally we also show that all the problems have the same complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded. AU - Chatterjee, Krishnendu AU - Velner, Yaron ID - 5377 SN - 2664-1690 TI - Mean-payoff pushdown games ER - TY - GEN AB - One central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n3 · m) time as compared to the previous known O(n6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m2)-time as compared to the previous known O((n · m)2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm. AU - Chatterjee, Krishnendu AU - Chaubal, Siddhesh AU - Kamath, Pritish ID - 5378 SN - 2664-1690 TI - Faster algorithms for alternating refinement relations ER - TY - CONF AB - We consider two-player stochastic games played on finite graphs with reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1), or positively (i.e., with positive probability), no matter the strategy of the second player. We classify such games according to the information and the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation (and the other player has perfect observation), or two-sided with (c) both players having partial observation. On the basis of randomization, the players (a) may not be allowed to use randomization (pure strategies), or (b) may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) may use full randomization. Our main results for pure strategies are as follows. (1) For one-sided games with player 1 having partial observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strategies are not sufficient, and we present an exponential upper bound on memory both for almostsure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete. (2) For one-sided games with player 2 having partial observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and positive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least non-elementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibits serious flaws in previous results of the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed. AU - Chatterjee, Krishnendu AU - Doyen, Laurent ID - 2955 T2 - Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science TI - Partial-observation stochastic games: How to win when belief fails ER - TY - CONF AB - We consider two-player stochastic games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine a probability distribution over the successor states. We also consider the important special case of turn-based stochastic games where players make moves in turns, rather than concurrently. We study concurrent games with \omega-regular winning conditions specified as parity objectives. The value for player 1 for a parity objective is the maximal probability with which the player can guarantee the satisfaction of the objective against all strategies of the opponent. We study the problem of continuity and robustness of the value function in concurrent and turn-based stochastic parity gameswith respect to imprecision in the transition probabilities. We present quantitative bounds on the difference of the value function (in terms of the imprecision of the transition probabilities) and show the value continuity for structurally equivalent concurrent games (two games are structurally equivalent if the support of the transition function is same and the probabilities differ). We also show robustness of optimal strategies for structurally equivalent turn-based stochastic parity games. Finally we show that the value continuity property breaks without the structurally equivalent assumption (even for Markov chains) and show that our quantitative bound is asymptotically optimal. Hence our results are tight (the assumption is both necessary and sufficient) and optimal (our quantitative bound is asymptotically optimal). AU - Chatterjee, Krishnendu ID - 3341 TI - Robustness of structurally equivalent concurrent parity games VL - 7213 ER - TY - CONF AB - We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether words are accepted with probability arbitrarily close to 1. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape (regular) words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions. For most decidable problems we show an optimal PSPACE-complete complexity bound. AU - Chatterjee, Krishnendu AU - Tracol, Mathieu ID - 2957 T2 - Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science TI - Decidable problems for probabilistic automata on infinite words ER - TY - JOUR AB - Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of "fit" or "desirability". We extend the simulation preorder to the quantitative setting by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes. AU - Cerny, Pavol AU - Henzinger, Thomas A AU - Radhakrishna, Arjun ID - 3249 IS - 1 JF - Theoretical Computer Science TI - Simulation distances VL - 413 ER - TY - CONF AB - We consider the problem of inference in a graphical model with binary variables. While in theory it is arguably preferable to compute marginal probabilities, in practice researchers often use MAP inference due to the availability of efficient discrete optimization algorithms. We bridge the gap between the two approaches by introducing the Discrete Marginals technique in which approximate marginals are obtained by minimizing an objective function with unary and pairwise terms over a discretized domain. This allows the use of techniques originally developed for MAP-MRF inference and learning. We explore two ways to set up the objective function - by discretizing the Bethe free energy and by learning it from training data. Experimental results show that for certain types of graphs a learned function can outperform the Bethe approximation. We also establish a link between the Bethe free energy and submodular functions. AU - Korc, Filip AU - Kolmogorov, Vladimir AU - Lampert, Christoph ID - 3124 TI - Approximating marginals using discrete energy minimization ER - TY - GEN AB - We consider the problem of inference in agraphical model with binary variables. While in theory it is arguably preferable to compute marginal probabilities, in practice researchers often use MAP inference due to the availability of efficient discrete optimization algorithms. We bridge the gap between the two approaches by introducing the Discrete Marginals technique in which approximate marginals are obtained by minimizing an objective function with unary and pair-wise terms over a discretized domain. This allows the use of techniques originally devel-oped for MAP-MRF inference and learning. We explore two ways to set up the objective function - by discretizing the Bethe free energy and by learning it from training data. Experimental results show that for certain types of graphs a learned function can out-perform the Bethe approximation. We also establish a link between the Bethe free energy and submodular functions. AU - Korc, Filip AU - Kolmogorov, Vladimir AU - Lampert, Christoph ID - 5396 SN - 2664-1690 TI - Approximating marginals using discrete energy minimization ER - TY - GEN AB - This document is created as a part of the project “Repository for Research Data on IST Austria”. It summarises the actual state of research data at IST Austria, based on survey results. It supports the choice of appropriate software, which would best fit the requirements of their users, the researchers. AU - Porsche, Jana ID - 5398 TI - Actual state of research data @ ISTAustria ER - TY - JOUR AB - Canny's edge detection algorithm is a classical and robust method for edge detection in gray-scale images. The two significant features of this method are introduction of NMS (Non-Maximum Suppression) and double thresholding of the gradient image. Due to poor illumination, the region boundaries in an image may become vague, creating uncertainties in the gradient image. In this paper, we have proposed an algorithm based on the concept of type-2 fuzzy sets to handle uncertainties that automatically selects the threshold values needed to segment the gradient image using classical Canny’s edge detection algorithm. The results show that our algorithm works significantly well on different benchmark images as well as medical images (hand radiography images). AU - Biswas, Ranita AU - Sil, Jaya ID - 5839 JF - Procedia Technology SN - 2212-0173 TI - An Improved Canny Edge Detection Algorithm Based on Type-2 Fuzzy Sets VL - 4 ER - TY - JOUR AB - The human Mediator complex controls RNA polymerase II (pol II) function in ways that remain incompletely understood. Activator-Mediator binding alters Mediator structure, and these activator-induced structural shifts appear to play key roles in regulating transcription. A recent cryo-electron microscopy (EM) analysis revealed that pol II adopted a stable orientation within a Mediator-pol II-TFIIF assembly in which Mediator was bound to the activation domain of viral protein 16 (VP16). Whereas TFIIF was shown to be important for orienting pol II within this assembly, the potential role of the activator was not assessed. To determine how activator binding might affect pol II orientation, we isolated human Mediator-pol II-TFIIF complexes in which Mediator was not bound to an activator. Cryo-EM analysis of this assembly, coupled with pol II crystal structure docking, revealed that pol II binds Mediator at the same general location; however, in contrast to VP16-bound Mediator, pol II does not appear to stably orient in the absence of an activator. Variability in pol II orientation might be important mechanistically, perhaps to enable sense and antisense transcription at human promoters. Because Mediator interacts extensively with pol II, these results suggest that Mediator structural shifts induced by activator binding help stably orient pol II prior to transcription initiation. AU - Bernecky, Carrie A AU - Taatjes, Dylan ID - 596 IS - 5 JF - Journal of Molecular Biology TI - Activator-mediator binding stabilizes RNA polymerase II orientation within the human mediator-RNA polymerase II-TFIIF assembly VL - 417 ER - TY - JOUR AB - Tonic receptors convey stimulus duration and intensity and are implicated in homeostatic control. However, how tonic homeostatic signals are generated and how they reconfigure neural circuits and modify animal behavior is poorly understood. Here we show that Caenorhabditis elegans O2-sensing neurons are tonic receptors that continuously signal ambient [O2] to set the animal's behavioral state. Sustained signaling relied on a Ca2+ relay involving L-type voltage-gated Ca2+ channels, the ryanodine and the inositol-1,4,5-trisphosphate receptors. Tonic activity evoked continuous neuropeptide release, which helps elicit the enduring behavioral state associated with high [O2]. Sustained O2 receptor signaling was propagated to downstream neural circuits, including the hub interneuron RMG. O2 receptors evoked similar locomotory states at particular O2 concentrations, regardless of previous d[O2]/dt. However, a phasic component of the URX receptors' response to high d[O2]/dt, as well as tonic-to-phasic transformations in downstream interneurons, enabled transient reorientation movements shaped by d[O2]/dt. Our results highlight how tonic homeostatic signals can generate both transient and enduring behavioral change. AU - Busch, Karl Emanuel AU - Laurent, Patrick AU - Soltesz, Zoltan AU - Murphy, Robin Joseph AU - Faivre, Olivier AU - Hedwig, Berthold AU - Thomas, Martin AU - Smith, Heather L AU - de Bono, Mario ID - 6136 IS - 4 JF - Nature Neuroscience SN - 1097-6256 TI - Tonic signaling from O2 sensors sets neural circuit activity and behavioral state VL - 15 ER - TY - CONF AB - This paper proposes a novel cooperative approach for two-hop amplify-and-forward (A&F) relaying that exploits both the signal forwarded by the relay and the one directly transmitted by the source in impulse-radio ultra-wideband (IR-UWB) systems. Specifically, we focus on a non-coherent setup employing a double-differential encoding scheme at the source node and a single differential demodulation at the relay and destination. The log-likelihood ratio based decision rule is derived at the destination node. A semi-analytical power allocation strategy is presented by evaluating a closed-form expression for the effective signal to noise ratio (SNR) at the destination, which is maximized by exhaustive search. Numerical simulations show that the proposed system outperforms both the direct transmission with single differential encoding and the non-cooperative multi-hop approach in different scenarios. AU - Mondelli, Marco AU - Zhou, Qi AU - Ma, Xiaoli AU - Lottici, Vincenzo ID - 6746 SN - 1520-6149 T2 - 2012 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP) TI - A cooperative approach for amplify-and-forward differential transmitted reference IR-UWB relay systems ER - TY - JOUR AB - The Seebeck coefficients, electrical resistivities, total thermal conductivities, and magnetization are reported for temperatures between 5 and 350 K for n-type Bi0.88Sb0.12 nano-composite alloys made by Ho-doping at the 0, 1, and 3 % atomic levels. The alloys were prepared using a dc hot-pressing method, and are shown to be single phase for both Ho contents with grain sizes on the average of 900 nm. We find the parent compound has a maximum of ZT = 0.28 at 231 K, while doping 1 % Ho increases the maximum ZT to 0.31 at 221 K and the 3 % doped sample suppresses the maximum ZT = 0.24 at a temperature of 260 K. AU - Lukas, K. C. AU - Joshi, G. AU - Modic, Kimberly A AU - Ren, Z. F. AU - Opeil, C. P. ID - 7074 IS - 15 JF - Journal of Materials Science SN - 0022-2461 TI - Thermoelectric properties of Ho-doped Bi0.88Sb0.12 VL - 47 ER - TY - JOUR AB - Carbon has been used widely as the basis of porous cathodes for nonaqueous Li–O2 cells. However, the stability of carbon and the effect of carbon on electrolyte decomposition in such cells are complex and depend on the hydrophobicity/hydrophilicity of the carbon surface. Analyzing carbon cathodes, cycled in Li–O2 cells between 2 and 4 V, using acid treatment and Fenton’s reagent, and combined with differential electrochemical mass spectrometry and FTIR, demonstrates the following: Carbon is relatively stable below 3.5 V (vs Li/Li+) on discharge or charge, especially so for hydrophobic carbon, but is unstable on charging above 3.5 V (in the presence of Li2O2), oxidatively decomposing to form Li2CO3. Direct chemical reaction with Li2O2 accounts for only a small proportion of the total carbon decomposition on cycling. Carbon promotes electrolyte decomposition during discharge and charge in a Li–O2 cell, giving rise to Li2CO3 and Li carboxylates (DMSO and tetraglyme electrolytes). The Li2CO3 and Li carboxylates present at the end of discharge and those that form on charge result in polarization on the subsequent charge. Li2CO3 (derived from carbon and from the electrolyte) as well as the Li carboxylates (derived from the electrolyte) decompose and form on charging. Oxidation of Li2CO3 on charging to ∼4 V is incomplete; Li2CO3 accumulates on cycling resulting in electrode passivation and capacity fading. Hydrophilic carbon is less stable and more catalytically active toward electrolyte decomposition than carbon with a hydrophobic surface. If the Li–O2 cell could be charged at or below 3.5 V, then carbon may be relatively stable, however, its ability to promote electrolyte decomposition, presenting problems for its use in a practical Li–O2 battery. The results emphasize that stable cycling of Li2O2 at the cathode in a Li–O2 cell depends on the synergy between electrolyte and electrode; the stability of the electrode and the electrolyte cannot be considered in isolation. AU - Ottakam Thotiyl, Muhammed M. AU - Freunberger, Stefan Alexander AU - Peng, Zhangquan AU - Bruce, Peter G. ID - 7308 IS - 1 JF - Journal of the American Chemical Society SN - 0002-7863 TI - The carbon electrode in nonaqueous Li–O2 cells VL - 135 ER - TY - JOUR AB - Energy‐storage technologies, including electrical double‐layer capacitors and rechargeable batteries, have attracted significant attention for applications in portable electronic devices, electric vehicles, bulk electricity storage at power stations, and “load leveling” of renewable sources, such as solar energy and wind power. Transforming lithium batteries and electric double‐layer capacitors requires a step change in the science underpinning these devices, including the discovery of new materials, new electrochemistry, and an increased understanding of the processes on which the devices depend. The Review will consider some of the current scientific issues underpinning lithium batteries and electric double‐layer capacitors. AU - Choi, Nam-Soon AU - Chen, Zonghai AU - Freunberger, Stefan Alexander AU - Ji, Xiulei AU - Sun, Yang-Kook AU - Amine, Khalil AU - Yushin, Gleb AU - Nazar, Linda F. AU - Cho, Jaephil AU - Bruce, Peter G. ID - 7309 IS - 40 JF - Angewandte Chemie International Edition SN - 1433-7851 TI - Challenges facing Lithium batteries and electrical double-layer capacitors VL - 51 ER - TY - JOUR AB - The rechargeable nonaqueous lithium-air (Li-O2) battery is receiving a great deal of interest because, theoretically, its specific energy far exceeds the best that can be achieved with lithium-ion cells. Operation of the rechargeable Li-O2 battery depends critically on repeated and highly reversible formation/decomposition of lithium peroxide (Li2O2) at the cathode upon cycling. Here, we show that this process is possible with the use of a dimethyl sulfoxide electrolyte and a porous gold electrode (95% capacity retention from cycles 1 to 100), whereas previously only partial Li2O2 formation/decomposition and limited cycling could occur. Furthermore, we present data indicating that the kinetics of Li2O2 oxidation on charge is approximately 10 times faster than on carbon electrodes. AU - Peng, Z. AU - Freunberger, Stefan Alexander AU - Chen, Y. AU - Bruce, P. G. ID - 7310 IS - 6094 JF - Science SN - 0036-8075 TI - A reversible and higher-rate Li-O2 battery VL - 337 ER - TY - JOUR AB - Stability of the electrolyte toward reduced oxygen species generated at the cathode is a crucial challenge for the rechargeable nonaqueous Li–O2 battery. Here, we investigate dimethylformamide as the basis of an electrolyte. Although reactions at the O2 cathode on the first discharge–charge cycle are dominated by reversible Li2O2 formation/decomposition, there is also electrolyte decomposition, which increases on cycling. The products of decomposition at the cathode on discharge are Li2O2, Li2CO3, HCO2Li, CH3CO2Li, NO, H2O, and CO2. Li2CO3 accumulates in the electrode with cycling. The stability of dimethylformamide toward reduced oxygen species is insufficient for its use in the rechargeable nonaqueous Li–O2 battery. AU - Chen, Yuhui AU - Freunberger, Stefan Alexander AU - Peng, Zhangquan AU - Bardé, Fanny AU - Bruce, Peter G. ID - 7311 IS - 18 JF - Journal of the American Chemical Society SN - 0002-7863 TI - Li–O2 battery with a dimethylformamide electrolyte VL - 134 ER - TY - CONF AB - Decades of research in distributed computing have led to a variety of perspectives on what it means for a concurrent algorithm to be efficient, depending on model assumptions, progress guarantees, and complexity metrics. It is therefore natural to ask whether one could compose algorithms that perform efficiently under different conditions, so that the composition preserves the performance of the original components when their conditions are met. In this paper, we evaluate the cost of composing shared-memory algorithms. First, we formally define the notion of safely composable algorithms and we show that every sequential type has a safely composable implementation, as long as enough state is transferred between modules. Since such generic implementations are inherently expensive, we present a more general light-weight specification that allows the designer to transfer very little state between modules, by taking advantage of the semantics of the implemented object. Using this framework, we implement a composed longlived test-and-set object, with the property that each of its modules is asymptotically optimal with respect to the progress condition it ensures, while the entire implementation only uses objects with consensus number at most two. Thus, we show that the overhead of composition can be negligible in the case of some important shared-memory abstractions. AU - Alistarh, Dan-Adrian AU - Guerraoui, Rachid AU - Kuznetsov, Petr AU - Losa, Giuliano ID - 762 TI - On the cost of composing shared-memory algorithms ER - TY - CONF AB - Renaming is a fundamental problem in distributed computing, in which a set of n processes need to pick unique names from a namespace of limited size. In this paper, we present the first early-deciding upper bounds for synchronous renaming, in which the running time adapts to the actual number of failures f in the execution. We show that, surprisingly, renaming can be solved in constant time if the number of failures f is limited to O(√n), while for general f ≤ n - 1 renaming can always be solved in O(log f) communication rounds. In the wait-free case, i.e. for f = n - 1, our upper bounds match the Ω(log n) lower bound of Chaudhuri et al. [13]. AU - Alistarh, Dan-Adrian AU - Attiya, Hagit AU - Guerraoui, Rachid AU - Travers, Corentin ID - 763 TI - Early deciding synchronous renaming in O(log f) rounds or less VL - 7355 LNCS ER -