Showing 201–250 of 362 results for author: Chatterjee, K

Faster Algorithms for Mean-Payoff Parity Games

Authors: Krishnendu Chatterjee, Monika Henzinger, Alexander Svozil

Abstract: Graph games provide the foundation for modeling and synthesis of reactive processes. Such games are played over graphs where the vertices are controlled by two adversarial players. We consider graph games where the objective of the first player is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). There… ▽ More Graph games provide the foundation for modeling and synthesis of reactive processes. Such games are played over graphs where the vertices are controlled by two adversarial players. We consider graph games where the objective of the first player is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). There are two variants of the problem, namely, the threshold problem where the quantitative goal is to ensure that the mean-payoff value is above a threshold, and the value problem where the quantitative goal is to ensure the optimal mean-payoff value; in both cases ensuring the qualitative parity objective. The previous best-known algorithms for game graphs with $n$ vertices, $m$ edges, parity objectives with $d$ priorities, and maximal absolute reward value $W$ for mean-payoff objectives, are as follows: $O(n^{d+1} \cdot m \cdot W)$ for the threshold problem, and $O(n^{d+2} \cdot m \cdot W)$ for the value problem. Our main contributions are faster algorithms, and the running times of our algorithms are as follows: $O(n^{d-1} \cdot m \cdot W)$ for the threshold problem, and $O(n^{d} \cdot m \cdot W \cdot \log (n\cdot W))$ for the value problem. For mean-payoff parity objectives with two priorities, our algorithms match the best-known bounds of the algorithms for mean-payoff games (without conjunction with parity objectives). Our results are relevant in synthesis of reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective). △ Less

Submitted 19 June, 2017; originally announced June 2017.

Improved Set-based Symbolic Algorithms for Parity Games

Authors: Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, Veronika Loitzenbauer

Abstract: Graph games with ω-regular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify ω-regular winning conditions. Graph games with parity conditions are equiva… ▽ More Graph games with ω-regular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify ω-regular winning conditions. Graph games with parity conditions are equivalent to μ-calculus model checking, and thus a very important algorithmic problem. Symbolic algorithms are of great significance because they provide scalable algorithms for the analysis of large finite-state systems, as well as algorithms for the analysis of infinite-state systems with finite quotient. A set-based symbolic algorithm uses the basic set operations and the one-step predecessor operators. We consider graph games with $n$ vertices and parity conditions with $c$ priorities. While many explicit algorithms exist for graph games with parity conditions, for set-based symbolic algorithms there are only two algorithms (notice that we use space to refer to the number of sets stored by a symbolic algorithm): (a) the basic algorithm that requires $O(n^c)$ symbolic operations and linear space; and (b) an improved algorithm that requires $O(n^{c/2+1})$ symbolic operations but also $O(n^{c/2+1})$ space (i.e., exponential space). In this work we present two set-based symbolic algorithms for parity games: (a) our first algorithm requires $O(n^{c/2+1})$ symbolic operations and only requires linear space; and (b) develo** on our first algorithm, we present an algorithm that requires $O(n^{c/3+1})$ symbolic operations and only linear space. We also present the first linear space set-based symbolic algorithm for parity games that requires at most a sub-exponential number of symbolic operations. △ Less

Submitted 15 June, 2017; originally announced June 2017.

Comments: An extended abstract has been accepted at CSL 2017

Value Iteration for Long-run Average Reward in Markov Decision Processes

Authors: Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Křetínský, Tobias Meggendorfer

Abstract: Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalism for expressing long term performance. Value iteration (VI) is one of the simplest and most efficient algorithmic approaches to MDPs with other properties, such as reachability objectives. Unfortunately, a naive extensi… ▽ More Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalism for expressing long term performance. Value iteration (VI) is one of the simplest and most efficient algorithmic approaches to MDPs with other properties, such as reachability objectives. Unfortunately, a naive extension of VI does not work for MDPs with long-run average rewards, as there is no known stop** criterion. In this work our contributions are threefold. (1) We refute a conjecture related to stop** criteria for MDPs with long-run average rewards. (2) We present two practical algorithms for MDPs with long-run average rewards based on VI. First, we show that a combination of applying VI locally for each maximal end-component (MEC) and VI for reachability objectives can provide approximation guarantees. Second, extending the above approach with a simulation-guided on-demand variant of VI, we present an anytime algorithm that is able to deal with very large models. (3) Finally, we present experimental results showing that our methods significantly outperform the standard approaches on several benchmarks. △ Less

Submitted 31 August, 2017; v1 submitted 5 May, 2017; originally announced May 2017.

Non-polynomial Worst-Case Analysis of Recursive Programs

Authors: Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady

Abstract: We study the problem of develo** efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of nonrecursive programs. First, we apply ranking functions to recursion, resulting in measure functions. We show that measure functions provide a sound and complete approach to prove wo… ▽ More We study the problem of develo** efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of nonrecursive programs. First, we apply ranking functions to recursion, resulting in measure functions. We show that measure functions provide a sound and complete approach to prove worst-case bounds of non-deterministic recursive programs. Our second contribution is the synthesis of measure functions in nonpolynomial forms. We show that non-polynomial measure functions with logarithm and exponentiation can be synthesized through abstraction of logarithmic or exponentiation terms, Farkas' Lemma, and Handelman's Theorem using linear programming. While previous methods obtain worst-case polynomial bounds, our approach can synthesize bounds of the form $\mathcal{O}(n\log n)$ as well as $\mathcal{O}(n^r)$ where $r$ is not an integer. We present experimental results to demonstrate that our approach can obtain efficiently worst-case bounds of classical recursive algorithms such as (i) Merge-Sort, the divide-and-conquer algorithm for the Closest-Pair problem, where we obtain $\mathcal{O}(n \log n)$ worst-case bound, and (ii) Karatsuba's algorithm for polynomial multiplication and Strassen's algorithm for matrix multiplication, where we obtain $\mathcal{O}(n^r)$ bound such that $r$ is not an integer and close to the best-known bounds for the respective algorithms. △ Less

Submitted 30 April, 2017; originally announced May 2017.

Comments: 54 Pages, Full Version to CAV 2017

Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds

Authors: Krishnendu Chatterjee, Hongfei Fu, Aniket Murhekar

Abstract: We consider the problem of develo** automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. Several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., QUICK-SORT), or completely ineffective (e.g., COUPON-COLLECTOR). Since the main focus of expecte… ▽ More We consider the problem of develo** automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. Several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., QUICK-SORT), or completely ineffective (e.g., COUPON-COLLECTOR). Since the main focus of expected-runtime analysis is to obtain efficient bounds, we consider bounds that are either logarithmic, linear, or almost-linear ($\mathcal{O}(\log n)$, $\mathcal{O}(n)$, $\mathcal{O}(n\cdot\log n)$, respectively, where n represents the input size). Our main contribution is an efficient (simple linear-time algorithm) sound approach for deriving such expected-runtime bounds for the analysis of recurrence relations induced by randomized algorithms. Our approach can infer the asymptotically optimal expected-runtime bounds for recurrences of classical randomized algorithms, including RANDOMIZED-SEARCH, QUICK-SORT, QUICK-SELECT, COUPONCOLLECTOR, where the worst-case bounds are either inefficient (such as linear as compared to logarithmic of expected-runtime, or quadratic as compared to linear or almost-linear of expected-runtime), or ineffective. We have implemented our approach, and the experimental results show that we obtain the bounds efficiently for the recurrences of various classical algorithms. △ Less

Submitted 30 April, 2017; originally announced May 2017.

Comments: 41 pages, Full Version to CAV 2017

Zero range and finite range processes with asymmetric rate functions

Authors: Amit Kumar Chatterjee, P. K. Mohanty

Abstract: We introduce and solve exactly a class of interacting particle systems in one dimension where particles hop asymmetrically. In its simplest form, namely asymmetric zero range process (AZRP), particles hop on a one dimensional periodic lattice with asymmetric hop rates; the rates for both right and left moves depend only on the occupation at the departure site but their functional forms are differe… ▽ More We introduce and solve exactly a class of interacting particle systems in one dimension where particles hop asymmetrically. In its simplest form, namely asymmetric zero range process (AZRP), particles hop on a one dimensional periodic lattice with asymmetric hop rates; the rates for both right and left moves depend only on the occupation at the departure site but their functional forms are different. We show that AZRP leads to a factorized steady state (FSS) when its rate-functions satisfy certain constraints. We demonstrate with explicit examples that AZRP exhibits certain interesting features which were not possible in usual zero range process. Firstly, it can undergo a condensation transition depending on how often a particle makes a right move compared to a left one and secondly, the particle current in AZRP can reverse its direction as density is changed. We show that these features are common in other asymmetric models which have FSS, like the asymmetric misanthrope process where rate functions for right and left hops are different, and depend on occupation of both the departure and the arrival site. We also derive sufficient conditions for having cluster-factorized steady states for finite range process with such asymmetric rate functions and discuss possibility of condensation there. △ Less

Submitted 18 April, 2017; originally announced April 2017.

Comments: 21 pages, 2 eps figures

Journal ref: J. Stat. Mech. (2017) 093201

Study of acoustic emission due to vaporisation of superheated droplets at higher pressure

Authors: Rupa Sarkar, Prasanna Kumar Mondal, Barun Kumar Chatterjee

Abstract: The bubble nucleation in superheated liquid can be controlled by adjusting the ambient pressure and temperature. At higher pressure the threshold energy for bubble nucleation increases and we have observed that the amplitude of the acoustic emission during vaporisation of superheated droplet decreases with increase in pressure at any given temperature. Other acoustic parameters such as the primary… ▽ More The bubble nucleation in superheated liquid can be controlled by adjusting the ambient pressure and temperature. At higher pressure the threshold energy for bubble nucleation increases and we have observed that the amplitude of the acoustic emission during vaporisation of superheated droplet decreases with increase in pressure at any given temperature. Other acoustic parameters such as the primary harmonic frequency and the decay time constant of the acoustic signal also decrease with increase in pressure. It is independent of the type of superheated liquid. The decrease in signal amplitude limits the detection of bubble nucleation at higher pressure. This effect is explained by the microbubble growth dynamics in superheated liquid. △ Less

Submitted 28 March, 2017; originally announced March 2017.

Comments: 11 pages, 9 figures

On the estimation of population size from a post-stratified two sample capture-recapture data under dependence

Authors: Kiranmoy Chatterjee, Prajamitra Bhuyan

Abstract: Population size estimation based on two sample capture-recapture type experiment is an interesting problem in various fields including epidemiology, pubic health, population studies, etc. The Lincoln-Petersen estimate is popularly used under the assumption that capture and recapture status of each individual is independent. However, in many real life scenarios, there is an inherent dependency betw… ▽ More Population size estimation based on two sample capture-recapture type experiment is an interesting problem in various fields including epidemiology, pubic health, population studies, etc. The Lincoln-Petersen estimate is popularly used under the assumption that capture and recapture status of each individual is independent. However, in many real life scenarios, there is an inherent dependency between capture and recapture attempts which is not well-studied in the literature of the dual system or two sample capture-recapture method. In this article, we propose a novel model that successfully incorporates the possible causal dependency and provide corresponding estimation methodologies for the associated model parameters based on post-stratified two sample capture-recapture data. The superiority of the performance of the proposed model over the existing competitors is established through an extensive simulation study. The method is illustrated through analysis of some real data sets. △ Less

Submitted 17 January, 2019; v1 submitted 8 March, 2017; originally announced March 2017.

Comments: 26 Pages

Faster Algorithms for Weighted Recursive State Machines

Authors: Krishnendu Chatterjee, Bernhard Kragl, Samarth Mishra, Andreas Pavlogiannis

Abstract: Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled f… ▽ More Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the best-known complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project. △ Less

Submitted 17 January, 2017; originally announced January 2017.

Termination of Nondeterministic Recursive Probabilistic Programs

Authors: Krishnendu Chatterjee, Hongfei Fu

Abstract: We study the termination problem for nondeterministic recursive probabilistic programs. First, we show that a ranking-supermartingales-based approach is both sound and complete for bounded terminiation (i.e., bounded expected termination time over all schedulers). Our result also clarifies previous results which claimed that ranking supermartingales are not a complete approach even for nondetermin… ▽ More We study the termination problem for nondeterministic recursive probabilistic programs. First, we show that a ranking-supermartingales-based approach is both sound and complete for bounded terminiation (i.e., bounded expected termination time over all schedulers). Our result also clarifies previous results which claimed that ranking supermartingales are not a complete approach even for nondeterministic probabilistic programs without recursion. Second, we show that conditionally difference-bounded ranking supermartingales provide a sound approach for lower bounds of expected termination time. Finally, we show that supermartingales with lower bounds on conditional absolute difference provide a sound approach for almost-sure termination, along with explicit bounds on tail probabilities of nontermination within a given number of steps. We also present several illuminating counterexamples that establish the necessity of certain prerequisites (such as conditionally difference-bounded condition). △ Less

Submitted 11 January, 2017; originally announced January 2017.

Comments: 35 pages. Comments are welcome

Exploring Strategies for Classification of External Stimuli Using Statistical Features of the Plant Electrical Response

Authors: Shre Kumar Chatterjee, Saptarshi Das, Koushik Maharatna, Elisa Masi, Luisa Santopolo, Stefano Mancuso, Andrea Vitaletti

Abstract: Plants sense their environment by producing electrical signals which in essence represent changes in underlying physiological processes. These electrical signals, when monitored, show both stochastic and deterministic dynamics. In this paper, we compute 11 statistical features from the raw non-stationary plant electrical signal time series to classify the stimulus applied (causing the electrical s… ▽ More Plants sense their environment by producing electrical signals which in essence represent changes in underlying physiological processes. These electrical signals, when monitored, show both stochastic and deterministic dynamics. In this paper, we compute 11 statistical features from the raw non-stationary plant electrical signal time series to classify the stimulus applied (causing the electrical signal). By using different discriminant analysis based classification techniques, we successfully establish that there is enough information in the raw electrical signal to classify the stimuli. In the process, we also propose two standard features which consistently give good classification results for three types of stimuli - Sodium Chloride (NaCl), Sulphuric Acid (H2SO4) and Ozone (O3). This may facilitate reduction in the complexity involved in computing all the features for online classification of similar external stimuli in future. △ Less

Submitted 29 November, 2016; originally announced November 2016.

Comments: 22 pages, 7 figures, 9 tables

Journal ref: Journal of the Royal Society Interface, vol. 12, no. 104, pp. 20141225, March 2015

Drift Removal in Plant Electrical Signals via IIR Filtering Using Wavelet Energy

Authors: Saptarshi Das, Barry Juans Ajiwibawa, Shre Kumar Chatterjee, Sanmitra Ghosh, Koushik Maharatna, Srinandan Dasmahapatra, Andrea Vitaletti, Elisa Masi, Stefano Mancuso

Abstract: Plant electrical signals often contains low frequency drifts with or without the application of external stimuli. Quantification of the randomness in plant signals in a stimulus-specific way is hindered because the knowledge of vital frequency information in the actual biological response is not known yet. Here we design an optimum Infinite Impulse Response (IIR) filter which removes the low frequ… ▽ More Plant electrical signals often contains low frequency drifts with or without the application of external stimuli. Quantification of the randomness in plant signals in a stimulus-specific way is hindered because the knowledge of vital frequency information in the actual biological response is not known yet. Here we design an optimum Infinite Impulse Response (IIR) filter which removes the low frequency drifts and preserves the frequency spectrum corresponding to the random component of the unstimulated plant signals by bringing the bias due to unknown artifacts and drifts to a minimum. We use energy criteria of wavelet packet transform (WPT) for optimization based tuning of the IIR filter parameters. Such an optimum filter enforces that the energy distribution of the pre-stimulus parts in different experiments are almost overlapped but under different stimuli the distributions of the energy get changed. The reported research may popularize plant signal processing, as a separate field, besides other conventional bioelectrical signal processing paradigms. △ Less

Submitted 29 November, 2016; originally announced November 2016.

Comments: 12 pages, 9 figures, 1 table

Journal ref: Computers and Electronics in Agriculture, Volume 118, October 2015, Pages 15-23

Optimizing Expectation with Guarantees in POMDPs (Technical Report)

Authors: Krishnendu Chatterjee, Petr Novotný, Guillermo A. Pérez, Jean-François Raskin, Đorđe Žikelić

Abstract: A standard objective in partially-observable Markov decision processes (POMDPs) is to find a policy that maximizes the expected discounted-sum payoff. However, such policies may still permit unlikely but highly undesirable outcomes, which is problematic especially in safety-critical applications. Recently, there has been a surge of interest in POMDPs where the goal is to maximize the probability t… ▽ More A standard objective in partially-observable Markov decision processes (POMDPs) is to find a policy that maximizes the expected discounted-sum payoff. However, such policies may still permit unlikely but highly undesirable outcomes, which is problematic especially in safety-critical applications. Recently, there has been a surge of interest in POMDPs where the goal is to maximize the probability to ensure that the payoff is at least a given threshold, but these approaches do not consider any optimization beyond satisfying this threshold constraint. In this work we go beyond both the "expectation" and "threshold" approaches and consider a "guaranteed payoff optimization (GPO)" problem for POMDPs, where we are given a threshold $t$ and the objective is to find a policy $σ$ such that a) each possible outcome of $σ$ yields a discounted-sum payoff of at least $t$, and b) the expected discounted-sum payoff of $σ$ is optimal (or near-optimal) among all policies satisfying a). We present a practical approach to tackle the GPO problem and evaluate it on standard POMDP benchmarks. △ Less

Submitted 29 January, 2017; v1 submitted 26 November, 2016; originally announced November 2016.

Stochastic Invariants for Probabilistic Termination

Authors: Krishnendu Chatterjee, Petr Novotný, Đorđe Žikelić

Abstract: Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability~1 (almost-sure termination). A powerful approach for this qualitative problem is the notion of ranking supermartingales with respect to a give… ▽ More Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability~1 (almost-sure termination). A powerful approach for this qualitative problem is the notion of ranking supermartingales with respect to a given set of invariants. The quantitative problem (probabilistic termination) asks for bounds on the termination probability. A fundamental and conceptual drawback of the existing approaches to address probabilistic termination is that even though the supermartingales consider the probabilistic behavior of the programs, the invariants are obtained completely ignoring the probabilistic aspect. In this work we address the probabilistic termination problem for linear-arithmetic probabilistic programs with nondeterminism. We define the notion of {\em stochastic invariants}, which are constraints along with a probability bound that the constraints hold. We introduce a concept of {\em repulsing supermartingales}. First, we show that repulsing supermartingales can be used to obtain bounds on the probability of the stochastic invariants. Second, we show the effectiveness of repulsing supermartingales in the following three ways: (1)~With a combination of ranking and repulsing supermartingales we can compute lower bounds on the probability of termination; (2)~repulsing supermartingales provide witnesses for refutation of almost-sure termination; and (3)~with a combination of ranking and repulsing supermartingales we can establish persistence properties of probabilistic programs. We also present results on related computational problems and an experimental evaluation of our approach on academic examples. △ Less

Submitted 16 November, 2016; v1 submitted 3 November, 2016; originally announced November 2016.

Comments: Full version of a paper published at POPL 2017. 20 pages

Data-centric Dynamic Partial Order Reduction

Authors: Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, Kapil Vaidya

Abstract: We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully u… ▽ More We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class. We introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence. For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence. For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence. △ Less

Submitted 25 January, 2019; v1 submitted 4 October, 2016; originally announced October 2016.

Conditionally Optimal Algorithms for Generalized Büchi Games

Authors: Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, Veronika Loitzenbauer

Abstract: Games on graphs provide the appropriate framework to study several central problems in computer science, such as the verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized Büchi objective… ▽ More Games on graphs provide the appropriate framework to study several central problems in computer science, such as the verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized Büchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized Büchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification. We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider graph games with $n$ vertices, $m$ edges, and generalized Büchi objectives with $k$ conjunctions. First, we present an algorithm with running time $O(k \cdot n^2)$, improving the previously known $O(k \cdot n \cdot m)$ and $O(k^2 \cdot n^2)$ worst-case bounds. Our algorithm is optimal for dense graphs under (A1). Second, we show that the basic algorithm for the problem is optimal for sparse graphs when the target sets have constant size under (A2). Finally, we consider GR(1) objectives, with $k_1$ conjunctions in the antecedent and $k_2$ conjunctions in the consequent, and present an $O(k_1 \cdot k_2 \cdot n^{2.5})$-time algorithm, improving the previously known $O(k_1 \cdot k_2 \cdot n \cdot m)$-time algorithm for $m > n^{1.5}$. △ Less

Submitted 20 July, 2016; originally announced July 2016.

Suppression of Superfluid Density and the Pseudogap State in the Cuprates by Impurities

Authors: Unurbat Erdenemunkh, Brian Koopman, Ling Fu, Kamalesh Chatterjee, W. D. Wise, G. D. Gu, E. W. Hudson, Michael C. Boyer

Abstract: We use scanning tunneling microscopy (STM) to study magnetic Fe impurities intentionally doped into the high-temperature superconductor Bi$_{2}$Sr$_{2}$Ca$_{2}$CuO$_{8+δ}$. Our spectroscopic measurements reveal that Fe impurities introduce low-lying resonances in the density of states at Ω$_{1}$ $\approx$ 4meV and Ω$_{2}$ $\approx$ 15 meV allowing us to determine that, despite having a large magne… ▽ More We use scanning tunneling microscopy (STM) to study magnetic Fe impurities intentionally doped into the high-temperature superconductor Bi$_{2}$Sr$_{2}$Ca$_{2}$CuO$_{8+δ}$. Our spectroscopic measurements reveal that Fe impurities introduce low-lying resonances in the density of states at Ω$_{1}$ $\approx$ 4meV and Ω$_{2}$ $\approx$ 15 meV allowing us to determine that, despite having a large magnetic moment, potential scattering of quasiparticles by Fe impurities dominates magnetic scattering. In addition, using high-resolution spatial characterizations of the local density of states near and away from Fe impurities, we detail the spatial extent of impurity affected regions as well as provide a local view of impurity-induced effects on the superconducting and pseudogap states. Our studies of Fe impurities, when combined with a reinterpretation of earlier STM work in the context of a two-gap scenario, allow us to present a unified view of the atomic-scale effects of elemental impurities on the pseudogap and superconducting states in hole-doped cuprates; this may help resolve a previously assumed dichotomy between the effects of magnetic and non-magnetic impurities in these materials. △ Less

Submitted 18 July, 2016; originally announced July 2016.

Journal ref: Phys. Rev. Lett. 117, 257003 (2016)

Evaluation and selection of Medical Tourism sites: A rough AHP based MABAC approach

Authors: Jagannath Roy, Kajal Chatterjee, Abhirup Bandhopadhyay, Samarjit Kar

Abstract: In this paper, a novel multiple criteria decision making (MCDM) methodology is presented for assessing and prioritizing medical tourism destinations in uncertain environment. A systematic evaluation and assessment method is proposed by integrating rough number based AHP (Analytic Hierarchy Process) and rough number based MABAC (Multi-Attributive Border Approximation area Comparison). Rough number… ▽ More In this paper, a novel multiple criteria decision making (MCDM) methodology is presented for assessing and prioritizing medical tourism destinations in uncertain environment. A systematic evaluation and assessment method is proposed by integrating rough number based AHP (Analytic Hierarchy Process) and rough number based MABAC (Multi-Attributive Border Approximation area Comparison). Rough number is used to aggregate individual judgments and preferences to deal with vagueness in decision making due to limited data. Rough AHP analyzes the relative importance of criteria based on their preferences given by experts. Rough MABAC evaluates the alternative sites based on the criteria weights. The proposed methodology is explained through a case study considering different cities for healthcare service in India. The validity of the obtained ranking for the given decision making problem is established by testing criteria proposed by Wang and Triantaphyllou (2008) along with further analysis and discussion. △ Less

Submitted 25 August, 2016; v1 submitted 29 June, 2016; originally announced June 2016.

Comments: 25 pages

Report number: 14450977

Nested Weighted Limit-Average Automata of Bounded Width

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop

Abstract: While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weight… ▽ More While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlap** requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness. △ Less

Submitted 11 June, 2016; originally announced June 2016.

Comments: A conference version will appear in MFCS 2016. arXiv admin note: text overlap with arXiv:1604.06764

Phase coexistence and spatial correlations in reconstituting k-mer models

Authors: Amit Kumar Chatterjee, Bijoy Daga, P. K. Mohanty

Abstract: In reconstituting k-mer models, extended objects which occupy several sites on a one dimensional lattice, undergo directed or undirected diffusion, and reconstitute -when in contact- by transferring a single monomer unit from one k-mer to the other; the rates depend on the size of participating k-mers. This polydispersed system has two conserved quantities, the number of k-mers and the packing fra… ▽ More In reconstituting k-mer models, extended objects which occupy several sites on a one dimensional lattice, undergo directed or undirected diffusion, and reconstitute -when in contact- by transferring a single monomer unit from one k-mer to the other; the rates depend on the size of participating k-mers. This polydispersed system has two conserved quantities, the number of k-mers and the packing fraction. We provide a matrix product method to write the steady state of this model and to calculate the spatial correlation functions analytically. We show that for a constant reconstitution rate, the spatial correlation exhibits damped oscillations in some density regions separated, from other regions with exponential decay, by a disorder surface. In a specific limit, this constant-rate reconstitution model is equivalent to a single dimer model and exhibits a phase coexistence similar to the one observed earlier in totally asymmetric simple exclusion process on a ring with a defect. △ Less

Submitted 1 August, 2016; v1 submitted 12 May, 2016; originally announced May 2016.

Comments: 9 pages, 5 eps figures

Journal ref: Phys. Rev. E 94, 012121 (2016)

Polynomial-Time Algorithms for Energy Games with Special Weight Structures

Authors: Krishnendu Chatterjee, Monika Henzinger, Sebastian Krinninger, Danupon Nanongkai

Abstract: Energy games belong to a class of turn-based two-player infinite-duration games}played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in ${\sf NP} \cap {\sf co\mbox{-}NP}$, but are not known to be in ${\sf P}$. The existence of polynomial-time algorithms has been a major open problem for decades and apart from pseudopolynomial algorithms there is… ▽ More Energy games belong to a class of turn-based two-player infinite-duration games}played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in ${\sf NP} \cap {\sf co\mbox{-}NP}$, but are not known to be in ${\sf P}$. The existence of polynomial-time algorithms has been a major open problem for decades and apart from pseudopolynomial algorithms there is no algorithm that solves any non-trivial subclass in polynomial time. In this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several worst-case instances on which previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is develo** the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting the graph structure does not necessarily help. △ Less

Submitted 29 April, 2016; v1 submitted 27 April, 2016; originally announced April 2016.

Comments: This paper appeared in the ESA 2012 special issue of Algorithmica. A preliminary version was presented at the 20th Annual European Symposium on Algorithms (ESA 2012)

Journal ref: Algorithmica 70(3): 457-492 (2014)

Termination Analysis of Probabilistic Programs through Positivstellensatz's

Authors: Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady

Abstract: We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic probabilistic programs with polynomial guards and assignments. Our approach is through synthesis of polynomial ranking supermartingales, that on one hand significantly generalizes linear ranking supermartingales and on t… ▽ More We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic probabilistic programs with polynomial guards and assignments. Our approach is through synthesis of polynomial ranking supermartingales, that on one hand significantly generalizes linear ranking supermartingales and on the other hand is a counterpart of polynomial ranking-functions for proving termination of nonprobabilistic programs. The approach synthesizes polynomial ranking-supermartingales through Positivstellensatz's, yielding an efficient method which is not only sound, but also semi-complete over a large subclass of programs. We show experimental results to demonstrate that our approach can handle several classical programs with complex polynomial guards and assignments, and can synthesize efficient quadratic ranking-supermartingales when a linear one does not exist even for simple affine programs. △ Less

Submitted 25 April, 2016; originally announced April 2016.

Comments: A conference version will appear in CAV 2016

Quantitative Automata under Probabilistic Semantics

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop

Abstract: Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative autom… ▽ More Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. △ Less

Submitted 10 August, 2019; v1 submitted 22 April, 2016; originally announced April 2016.

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 3 (August 13, 2019) lmcs:4512

Computation Tree Logic for Synchronization Properties

Authors: Krishnendu Chatterjee, Laurent Doyen

Abstract: We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that… ▽ More We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking. △ Less

Submitted 24 May, 2016; v1 submitted 21 April, 2016; originally announced April 2016.

Comments: A conference version will appear in ICALP 2016

Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives

Authors: Krishnendu Chatterjee, Laurent Doyen

Abstract: Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjuncti… ▽ More Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is 1. Previous results presented a semi-decision procedure for epsilon-approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements. △ Less

Submitted 21 April, 2016; originally announced April 2016.

Comments: A conference version will appear in LICS 2016

Robust Draws in Balanced Knockout Tournaments

Authors: Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Josef Tkadlec

Abstract: Balanced knockout tournaments are ubiquitous in sports competitions and are also used in decision-making and elections. The traditional computational question, that asks to compute a draw (optimal draw) that maximizes the winning probability for a distinguished player, has received a lot of attention. Previous works consider the problem where the pairwise winning probabilities are known precisely,… ▽ More Balanced knockout tournaments are ubiquitous in sports competitions and are also used in decision-making and elections. The traditional computational question, that asks to compute a draw (optimal draw) that maximizes the winning probability for a distinguished player, has received a lot of attention. Previous works consider the problem where the pairwise winning probabilities are known precisely, while we study how robust is the winning probability with respect to small errors in the pairwise winning probabilities. First, we present several illuminating examples to establish: (a)~there exist deterministic tournaments (where the pairwise winning probabilities are~0 or~1) where one optimal draw is much more robust than the other; and (b)~in general, there exist tournaments with slightly suboptimal draws that are more robust than all the optimal draws. The above examples motivate the study of the computational problem of robust draws that guarantee a specified winning probability. Second, we present a polynomial-time algorithm for approximating the robustness of a draw for sufficiently small errors in pairwise winning probabilities, and obtain that the stated computational problem is NP-complete. We also show that two natural cases of deterministic tournaments where the optimal draw could be computed in polynomial time also admit polynomial-time algorithms to compute robust optimal draws. △ Less

Submitted 18 April, 2016; originally announced April 2016.

Removal of angular momentum by strong magnetic field stresses in advective accretion flows around black holes

Authors: Banibrata Mukhopadhyay, Koushik Chatterjee

Abstract: We show that the removal of angular momentum is possible in the presence of large scale magnetic stresses, arisen by fields much stronger than that required for magnetorotational instability, in geometrically thick, advective, sub-Keplerian accretion flows around black holes in steady-state, in the complete absence of alpha-viscosity. The efficiency of such angular momentum transfer via Maxwell st… ▽ More We show that the removal of angular momentum is possible in the presence of large scale magnetic stresses, arisen by fields much stronger than that required for magnetorotational instability, in geometrically thick, advective, sub-Keplerian accretion flows around black holes in steady-state, in the complete absence of alpha-viscosity. The efficiency of such angular momentum transfer via Maxwell stress, with the field well below its equipartition value, could be equivalent to that of alpha-viscosity, arisen via Reynolds stress, with $α=0.01-0.08$. We find in our simpler vertically averaged advective disk model that stronger the magnetic field and/or larger the vertical-gradient of azimuthal component of magnetic field, stronger the rate of angular momentum transfer is, which in turn may lead to a faster rate of outflowing matter, which has important implications to describe the hard spectral states of black hole sources. When the generic origin of alpha-viscosity is still being explored, mechanism of efficient angular momentum transfer via magnetic stresses alone is very interesting. △ Less

Submitted 29 February, 2016; originally announced March 2016.

Comments: 6 pages including 2 figures; to appear in the Proceedings of 14th Marcel Grossman Meeting (MG14), Rome, Italy, 12-18 July 2015; based on the talk given in the meeting in the session AC2

Stochastic Shortest Path with Energy Constraints in POMDPs

Authors: Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelík, Anchit Gupta, Petr Novotný

Abstract: We consider partially observable Markov decision processes (POMDPs) with a set of target states and positive integer costs associated with every transition. The traditional optimization objective (stochastic shortest path) asks to minimize the expected total cost until the target set is reached. We extend the traditional framework of POMDPs to model energy consumption, which represents a hard cons… ▽ More We consider partially observable Markov decision processes (POMDPs) with a set of target states and positive integer costs associated with every transition. The traditional optimization objective (stochastic shortest path) asks to minimize the expected total cost until the target set is reached. We extend the traditional framework of POMDPs to model energy consumption, which represents a hard constraint. The energy levels may increase and decrease with transitions, and the hard constraint requires that the energy level must remain positive in all steps till the target is reached. First, we present a novel algorithm for solving POMDPs with energy levels, develo** on existing POMDP solvers and using RTDP as its main method. Our second contribution is related to policy representation. For larger POMDP instances the policies computed by existing solvers are too large to be understandable. We present an automated procedure based on machine learning techniques that automatically extracts important decisions of the policy allowing us to compute succinct human readable policies. Finally, we show experimentally that our algorithm performs well and computes succinct policies on a number of POMDP instances from the literature that were naturally enhanced with energy levels. △ Less

Submitted 11 May, 2016; v1 submitted 24 February, 2016; originally announced February 2016.

Comments: Technical report accompanying a paper published in proceedings of AAMAS 2016

Restricted deterministic Watson-Crick automata

Authors: Kingshuk Chatterjee, Kumar Sankar Ray

Abstract: In this paper, we introduce a new model of deterministic Watson-Crick automaton namely restricted deterministic Watson- Crick automaton which is a deterministic Watson-Crick automaton where the complementarity string in the lower strand is restricted to a language L. We examine the computational power of the restricted model with respect to L being in different language classes such as regular, un… ▽ More In this paper, we introduce a new model of deterministic Watson-Crick automaton namely restricted deterministic Watson- Crick automaton which is a deterministic Watson-Crick automaton where the complementarity string in the lower strand is restricted to a language L. We examine the computational power of the restricted model with respect to L being in different language classes such as regular, unary regular, finite, context free and context sensitive. We also show that computational power of restricted deterministic Watson- Crick automata with L in regular languages is same as that of deterministic Watson-Crick automata and that the set of all languages accepted by restricted deterministic Watson-Crick automata with L in unary regular languages is a proper subset of context free languages. △ Less

Submitted 18 February, 2016; originally announced February 2016.

Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction

Authors: Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, Veronika Loitzenbauer

Abstract: Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental $ω$-regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, y… ▽ More Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental $ω$-regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as reachability/safety (for disjunctive questions) and Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical $ω$-regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives. △ Less

Submitted 8 February, 2016; originally announced February 2016.

Searching for X-ray sources in nearby late-type galaxies with low star formation rates

Authors: K. Chatterjee, P. Kaaret, M. Brorby, J. J. E. Kajava, F. Grise, S. Farrell, J. Poutanen

Abstract: Late type non-starburst galaxies have been shown to contain X-ray emitting objects, some being ultraluminous X-ray sources. We report on XMM-Newton observations of 11 nearby, late-type galaxies previously observed with the Hubble Space Telescope (HST) in order to find such objects. We found 18 X-ray sources in or near the optical extent of the galaxies, most being point-like. If associated with th… ▽ More Late type non-starburst galaxies have been shown to contain X-ray emitting objects, some being ultraluminous X-ray sources. We report on XMM-Newton observations of 11 nearby, late-type galaxies previously observed with the Hubble Space Telescope (HST) in order to find such objects. We found 18 X-ray sources in or near the optical extent of the galaxies, most being point-like. If associated with the corresponding galaxies, the source luminosities range from $2 \times 10^{37}$ erg s$^{-1}$ to $6 \times 10^{39}$ erg s$^{-1}$. We found one ultraluminous X-ray source, which is in the galaxy IC 5052, and one source coincident with the galaxy IC 4662 with a blackbody temperature of $0.166 \pm 0.015$ keV that could be a quasi-soft source or a quiescent neutron star X-ray binary in the Milky Way. One X-ray source, XMMU J205206.0$-$691316, is extended and coincident with a galaxy cluster visible on an HST image. The X-ray spectrum of the cluster reveals a redshift of $z = 0.25 \pm 0.02$ and a temperature of 3.6$\pm$0.4 keV. The redshift was mainly determined by a cluster of Fe XXIV lines between the observed energy range $0.8-1.0$ keV. △ Less

Submitted 18 December, 2015; originally announced December 2015.

Comments: 8 pages, to appear in MNRAS

A Symbolic SAT-based Algorithm for Almost-sure Reachability with Small Strategies in POMDPs

Authors: Krishnendu Chatterjee, Martin Chmelik, Jessica Davies

Abstract: POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIME-complete, in many practic… ▽ More POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIME-complete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. △ Less

Submitted 26 November, 2015; originally announced November 2015.

Comments: Full version of "A Symbolic SAT-based Algorithm for Almost-sure Reachability with Small Strategies in POMDPs" AAAI 2016

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs

Authors: Krishnendu Chatterjee, Hongfei Fu, Petr Novotny, Rouzbeh Hasheminezhad

Abstract: In this paper, we consider termination of probabilistic programs with real-valued variables. The questions concerned are: 1. qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); 2. quantitative ones that ask (i) to approximate the expected termination time (expectat… ▽ More In this paper, we consider termination of probabilistic programs with real-valued variables. The questions concerned are: 1. qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); 2. quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound B such that the probability to terminate after B steps decreases exponentially (concentration problem). To solve these questions, we utilize the notion of ranking supermartingales which is a powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic programs (APP's) with both angelic and demonic non-determinism. An important subclass of APP's is LRAPP which is defined as the class of all APP's over which a linear ranking-supermartingale exists. Our main contributions are as follows. Firstly, we show that the membership problem of LRAPP (i) can be decided in polynomial time for APP's with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for APP's with angelic non-determinism; moreover, the NP-hardness result holds already for APP's without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRAPP can be solved in the same complexity as for the membership problem of LRAPP. Finally, we show that the expectation problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP's without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to answer the qualitative and quantitative questions over APP's with at most demonic non-determinism. △ Less

Submitted 28 October, 2015; originally announced October 2015.

Comments: 24 pages, full version to the conference paper on POPL 2016

ACM Class: D.2.4

Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components

Authors: Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis

Abstract: We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is… ▽ More We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure, which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms. △ Less

Submitted 26 October, 2015; originally announced October 2015.

ACM Class: F.3.2

Multi-head Watson-Crick automata

Authors: Kingshuk Chatterjee, Kumar Sankar Ray

Abstract: Inspired by multi-head finite automata and Watson-Crick automata in this paper, we introduce new structure namely multi-head Watson-Crick automata where we replace the single tape of multi-head finite automaton by a DNA double strand. The content of the second tape is determined using a complementarity relation similar to Watson-Crick complementarity relation. We establish the superiority of our m… ▽ More Inspired by multi-head finite automata and Watson-Crick automata in this paper, we introduce new structure namely multi-head Watson-Crick automata where we replace the single tape of multi-head finite automaton by a DNA double strand. The content of the second tape is determined using a complementarity relation similar to Watson-Crick complementarity relation. We establish the superiority of our model over multi-head finite automata and also show that both the deterministic and non-deterministic variant of the model can accept non-regular unary languages. We also compare our model with parallel communicating Watson-Crick automata systems and prove that both of them have the same computational power. △ Less

Submitted 9 December, 2015; v1 submitted 14 October, 2015; originally announced October 2015.

Comments: arXiv admin note: text overlap with arXiv:1507.05284, arXiv:1510.02070

Non-regular unary language and parallel communicating Watson-Crick automata systems

Authors: Kingshuk Chatterjee, Kumar Sankar Ray

Abstract: In 2006, Czeizler et.al. introduced parallel communicating Watson-Crick automata system. They showed that parallel communicating Watson-Crick automata system can accept the non-regular unary language L={a^(n^2 ),where n>1} using non-injective complementarity relation and three components. In this paper, we improve on Czeizler et.al. work by showing that parallel communicating Watson-Crick automata… ▽ More In 2006, Czeizler et.al. introduced parallel communicating Watson-Crick automata system. They showed that parallel communicating Watson-Crick automata system can accept the non-regular unary language L={a^(n^2 ),where n>1} using non-injective complementarity relation and three components. In this paper, we improve on Czeizler et.al. work by showing that parallel communicating Watson-Crick automata system can accept the same language L using just two components. △ Less

Submitted 7 October, 2015; originally announced October 2015.

Comments: arXiv admin note: text overlap with arXiv:1507.05284

Deterministic parallel communicating Watson-Crick automata systems

Authors: Kingshuk Chatterjee, Kumar Sankar Ray

Abstract: In this paper, we have introduced the deterministic variant of parallel communicating Watson-Crick automata systems. We show that similar to the non-deterministic version, the deterministic version can also recognise some non-regular uniletter languages. We further establish that strongly deterministic Watson-Crick automata systems and deterministic Watson-Crick automata system are incomparable in… ▽ More In this paper, we have introduced the deterministic variant of parallel communicating Watson-Crick automata systems. We show that similar to the non-deterministic version, the deterministic version can also recognise some non-regular uniletter languages. We further establish that strongly deterministic Watson-Crick automata systems and deterministic Watson-Crick automata system are incomparable in terms of their computational ability. We have also compared the computational ability of our system with multihead finite automata and parallel communicating finite automata systems. △ Less

Submitted 19 July, 2015; originally announced July 2015.

Reversible Watson-Crick Automata

Authors: Kingshuk Chatterjee, Kumar Sankar Ray

Abstract: Watson-Crick automata are finite automata working on double strands. Extensive research work has already been done on non-deterministic Watson-Crick automata and on deterministic Watson-Crick automata. In this paper, we introduce a new model of Watson-Crick automata which is reversible in nature named reversible Watson-Crick automata and explore its computational power. We show even though the mod… ▽ More Watson-Crick automata are finite automata working on double strands. Extensive research work has already been done on non-deterministic Watson-Crick automata and on deterministic Watson-Crick automata. In this paper, we introduce a new model of Watson-Crick automata which is reversible in nature named reversible Watson-Crick automata and explore its computational power. We show even though the model is reversible and one way it accepts all regular languages and also analyze the state complexity of the above stated model with respect to non-deterministic block automata and non-deterministic finite automata and establish its superiority. We further explore the relation of the reversible model with twin-shuffle language and recursively enumerable languages. △ Less

Submitted 9 December, 2015; v1 submitted 19 July, 2015; originally announced July 2015.

Comments: arXiv admin note: text overlap with arXiv:1507.05282

Watson-Crick Quantum Finite Automata

Authors: Kingshuk Chatterjee, Kumar Sankar Ray

Abstract: 1-way quantum finite automata are deterministic and reversible in nature, which greatly reduces its accepting property. In fact the set of languages accepted by 1-way quantum finite automata is a proper subset of regular languages. In this paper we replace the tape head of 1-way quantum finite automata with DNA double strand and name the model Watson-Crick quantum finite automata. The non-injectiv… ▽ More 1-way quantum finite automata are deterministic and reversible in nature, which greatly reduces its accepting property. In fact the set of languages accepted by 1-way quantum finite automata is a proper subset of regular languages. In this paper we replace the tape head of 1-way quantum finite automata with DNA double strand and name the model Watson-Crick quantum finite automata. The non-injective complementarity relation of Watson-Crick automata introduces non-determinism in the quantum model. We show that this introduction of non-determinism increases the computational power of 1-way Quantum finite automata significantly. We establish that Watson-Crick quantum finite automata can accept all regular languages and that it also accepts some languages not accepted by any multihead deterministic finite automata. Exploiting the superposition property of quantum finite automata we show that Watson-Crick quantum finite automata accept the language L=ww where w belongs to {a,b}*. △ Less

Submitted 9 December, 2015; v1 submitted 19 July, 2015; originally announced July 2015.

Strategy Complexity of Concurrent Stochastic Games with Safety and Reachability Objectives

Authors: Krishnendu Chatterjee, Kristoffer Arnsfelt Hansen, Rasmus Ibsen-Jensen

Abstract: We consider finite-state concurrent stochastic games, played by k>=2 players for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. We consider reachability objectives that given a target… ▽ More We consider finite-state concurrent stochastic games, played by k>=2 players for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. We consider reachability objectives that given a target set of states require that some state in the target is visited, and the dual safety objectives that given a target set require that only states in the target set are visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest nonzero probability employed. Our main results are as follows: We show that in two-player zero-sum concurrent stochastic games (with reachability objective for one player and the complementary safety objective for the other player): (i) the optimal bound on the patience of optimal and epsilon-optimal strategies, for both players is doubly exponential; and (ii) even in games with a single nonabsorbing state exponential (in the number of actions) patience is necessary. In general we study the class of non-zero-sum games admitting stationary epsilon-Nash equilibria. We show that if there is at least one player with reachability objective, then doubly-exponential patience may be needed for epsilon-Nash equilibrium strategies, whereas in contrast if all players have safety objectives, the optimal bound on patience for epsilon-Nash equilibrium strategies is only exponential. △ Less

Submitted 8 June, 2015; originally announced June 2015.

Hydromagnetics of advective accretion flows around black holes: Removal of angular momentum by large scale magnetic stresses

Authors: Banibrata Mukhopadhyay, Koushik Chatterjee

Abstract: We show that the removal of angular momentum is possible in the presence of large scale magnetic stresses in geometrically thick, advective, sub-Keplerian accretion flows around black holes in steady-state, in the complete absence of alpha-viscosity. The efficiency of such an angular momentum transfer could be equivalent to that of alpha-viscosity with alpha=0.01-0.08. Nevertheless, required field… ▽ More We show that the removal of angular momentum is possible in the presence of large scale magnetic stresses in geometrically thick, advective, sub-Keplerian accretion flows around black holes in steady-state, in the complete absence of alpha-viscosity. The efficiency of such an angular momentum transfer could be equivalent to that of alpha-viscosity with alpha=0.01-0.08. Nevertheless, required field is well below its equipartition value, leading to a magnetically stable disk flow. This is essentially important in order to describe the hard spectral state of the sources, when the flow is non/sub-Keplerian. We show in our simpler 1.5-dimensional, vertically averaged disk model that larger the vertical-gradient of azimuthal component of magnetic field, stronger the rate of angular momentum transfer is, which in turn may lead to a faster rate of outflowing matter. Finding efficient angular momentum transfer, in black hole disks, via magnetic stresses alone is very interesting, when the generic origin of alpha-viscosity is still being explored. △ Less

Submitted 6 May, 2015; originally announced May 2015.

Comments: 14 pages including 8 figures; accepted for publication in The Astrophysical Journal

Journal ref: ApJ 807 (2015) 43

Edit Distance for Pushdown Automata

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, Rasmus Ibsen-Jensen, Jan Otop

Abstract: The edit distance between two words $w_1, w_2$ is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform $w_1$ to $w_2$. The edit distance generalizes to languages $\mathcal{L}_1, \mathcal{L}_2$, where the edit distance from $\mathcal{L}_1$ to $\mathcal{L}_2$ is the minimal number $k$ such that for every word from $\mathcal{L}_1$ there exists… ▽ More The edit distance between two words $w_1, w_2$ is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform $w_1$ to $w_2$. The edit distance generalizes to languages $\mathcal{L}_1, \mathcal{L}_2$, where the edit distance from $\mathcal{L}_1$ to $\mathcal{L}_2$ is the minimal number $k$ such that for every word from $\mathcal{L}_1$ there exists a word in $\mathcal{L}_2$ with edit distance at most $k$. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1)~deciding whether, for a given threshold $k$, the edit distance from a pushdown automaton to a finite automaton is at most $k$, and (2)~deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. △ Less

Submitted 22 September, 2017; v1 submitted 30 April, 2015; originally announced April 2015.

Comments: An extended version of a paper accepted to ICALP 2015 with the same title. The paper has been accepted to the LMCS journal

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 3 (September 13, 2017) lmcs:3927

Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs

Authors: Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis

Abstract: We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the g… ▽ More We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let $n$ denote the number of nodes of a graph, $m$ the number of edges (for constant treewidth graphs $m=O(n)$) and $W$ the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of $ε$ in time $O(n \cdot \log (n/ε))$ and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time $O(n \cdot \log (|a\cdot b|))=O(n\cdot\log (n\cdot W))$, when the output is $\frac{a}{b}$, as compared to the previously best known algorithm with running time $O(n^2 \cdot \log (n\cdot W))$. Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in $O(n^2\cdot m)$ time and the associated decision problem can be solved in $O(n\cdot m)$ time, improving the previous known $O(n^3\cdot m\cdot \log (n\cdot W))$ and $O(n^2 \cdot m)$ bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires $O(n\cdot \log n)$ time, improving the previous known $O(n^4 \cdot \log (n \cdot W))$ bound. △ Less

Submitted 28 April, 2015; originally announced April 2015.

ACM Class: G.2.2

Nested Weighted Automata

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop

Abstract: Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know dec… ▽ More Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties. △ Less

Submitted 23 April, 2015; originally announced April 2015.

Comments: The full version of the paper "Nested Weighted Automata" accepted to LICS 2015

ACM Class: F.1.1; D.2.4

On the Population Size Estimation from Dual-record System: Profile-Likelihood Approaches

Authors: Kiranmoy Chatterjee, Diganta Mukherjee

Abstract: Motivated by various applications, we consider the problem of homogeneous human population size (N) estimation from Dual-record system (DRS) (equivalently, two-sample capture-recapture experiment). The likelihood estimate from the independent capture-recapture model Mt is widely used in this context though appropriateness of the behavioral dependence model Mtb is unanimously acknowledged. Our prim… ▽ More Motivated by various applications, we consider the problem of homogeneous human population size (N) estimation from Dual-record system (DRS) (equivalently, two-sample capture-recapture experiment). The likelihood estimate from the independent capture-recapture model Mt is widely used in this context though appropriateness of the behavioral dependence model Mtb is unanimously acknowledged. Our primary aim is to investigate the use of several relevant pseudo-likelihood methods profiling N, explicitly for model Mtb. An adjustment over profile likelihood is proposed. Simulation studies are carried out to evaluate the performance of the proposed method compared with Bayes estimate suggested for general capture-recapture experiment by Lee et al. (Statistica Sinica, 2003, vol. 13). We also analyse the effect of possible model mis-specification, due to the use of model Mt, in terms of efficiency and robustness. Finally two real life examples with different characteristics are presented for illustration of the methodologies discussed. △ Less

Submitted 5 April, 2015; originally announced April 2015.

Comments: 24 Pages, 4 Figures

The Complexity of Synthesis from Probabilistic Components

Authors: Krishnendu Chatterjee, Laurent Doyen, Moshe Y. Vardi

Abstract: The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is "constructed from scratch" rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced dataflow… ▽ More The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is "constructed from scratch" rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced dataflow and controlflow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while controlflow synthesis is decidable. The problem of controlflow synthesis from libraries of probabilistic components was considered by Nain, Lustig and Vardi, and was shown to be decidable for qualitative analysis (that asks that the specification be satisfied with probability 1). Our main contributions for controlflow synthesis from probabilistic components are to establish better complexity bounds for the qualitative analysis problem, and to show that the more general quantitative problem is undecidable. For the qualitative analysis, we show that the problem (i) is EXPTIME-complete when the specification is given as a deterministic parity word automaton, improving the previously known 2EXPTIME upper bound; and (ii) belongs to UP $\cap$ coUP and is parity-games hard, when the specification is given directly as a parity condition on the components, improving the previously known EXPTIME upper bound. △ Less

Submitted 17 February, 2015; originally announced February 2015.

Counterexample Explanation by Learning Small Strategies in Markov Decision Processes

Authors: Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelík, Andreas Fellner, Jan Křetínský

Abstract: While for deterministic systems, a counterexample to a property can simply be an error trace, counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the c… ▽ More While for deterministic systems, a counterexample to a property can simply be an error trace, counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy - which can be a counterexample to violation of or a witness of satisfaction of a property - itself, and extract the most important decisions it makes, and present its succinct representation. The key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour. △ Less

Submitted 10 February, 2015; originally announced February 2015.

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

Authors: Krishnendu Chatterjee, Zuzana Křetínská, Jan Křetínský

Abstract: We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optim… ▽ More We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. △ Less

Submitted 29 June, 2017; v1 submitted 2 February, 2015; originally announced February 2015.

Comments: Extended journal version of the LICS'15 paper

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 2 (July 3, 2017) lmcs:3757

Nucleation and Growth Mechanism of a Covalent Material: Magic Clusters and Chemical Reactions

Authors: Yi-Hsien Lee, Kuntal Chatterjee, Chung-Kai Fang, Shih-Hsin Chang, I-Po Hong, Tien-Chih Chang, Ing-Shouh Hwang

Abstract: With scanning tunneling microscopy, we study the very early stage of Si deposition on a Pb monolayer covered Si(111) surface. We find a special type of Si magic clusters which are highly mobile on the defect-free surface but may be trapped temporarily at certain boundary or defect sites. They may also aggregate and a special aggregate arrangement is found to be stable for one to two days at room t… ▽ More With scanning tunneling microscopy, we study the very early stage of Si deposition on a Pb monolayer covered Si(111) surface. We find a special type of Si magic clusters which are highly mobile on the defect-free surface but may be trapped temporarily at certain boundary or defect sites. They may also aggregate and a special aggregate arrangement is found to be stable for one to two days at room temperature. Adding more Si on the cluster aggregate can transform it into a metastable structure. A scenario based on magic clusters and their chemical reactions is proposed to describe the nucleation and growth processes of covalent materials. △ Less

Submitted 16 January, 2015; originally announced January 2015.

MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives

Authors: Tomáš Brázdil, Krishnendu Chatterjee, Vojtěch Forejt, Antonín Kučera

Abstract: We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i)~generating strategies and exploring them for… ▽ More We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i)~generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii)~generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies. △ Less

Submitted 13 January, 2015; originally announced January 2015.

Comments: Extended version for a TACAS 2015 tool demo paper