TY - JOUR AB - We study Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) functions. We consider two different objectives, namely, expectation and satisfaction objectives. Given an MDP with κ limit-average functions, in the expectation objective the goal is to maximize the expected limit-average value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector. We show that under the expectation objective, in contrast to the case of one limit-average function, both randomization and memory are necessary for strategies even for ε-approximation, and that finite-memory randomized strategies are sufficient for achieving Pareto optimal values. Under the satisfaction objective, in contrast to the case of one limit-average function, infinite memory is necessary for strategies achieving a specific value (i.e. randomized finite-memory strategies are not sufficient), whereas memoryless randomized strategies are sufficient for ε-approximation, for all ε > 0. We further prove that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be ε-approximated in time polynomial in the size of the MDP and 1/ε, and exponential in the number of limit-average functions, for all ε > 0. Our analysis also reveals flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, corrects the flaws, and allows us to obtain improved results. AU - Brázdil, Tomáš AU - Brožek, Václav AU - Chatterjee, Krishnendu AU - Forejt, Vojtěch AU - Kučera, Antonín ID - 2234 IS - 1 JF - Logical Methods in Computer Science SN - 18605974 TI - Markov decision processes with multiple long-run average objectives VL - 10 ER - TY - JOUR AB - Muller games are played by two players moving a token along a graph; the winner is determined by the set of vertices that occur infinitely often. The central algorithmic problem is to compute the winning regions for the players. Different classes and representations of Muller games lead to problems of varying computational complexity. One such class are parity games; these are of particular significance in computational complexity, as they remain one of the few combinatorial problems known to be in NP ∩ co-NP but not known to be in P. We show that winning regions for a Muller game can be determined from the alternating structure of its traps. To every Muller game we then associate a natural number that we call its trap depth; this parameter measures how complicated the trap structure is. We present algorithms for parity games that run in polynomial time for graphs of bounded trap depth, and in general run in time exponential in the trap depth. AU - Grinshpun, Andrey AU - Phalitnonkiat, Pakawat AU - Rubin, Sasha AU - Tarfulea, Andrei ID - 2246 JF - Theoretical Computer Science SN - 03043975 TI - Alternating traps in Muller and parity games VL - 521 ER - TY - JOUR AB - Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω ω -regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on vector addition systems with states. Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts. AU - Chatterjee, Krishnendu AU - Randour, Mickael AU - Raskin, Jean ID - 2716 IS - 3-4 JF - Acta Informatica TI - Strategy synthesis for multi-dimensional quantitative objectives VL - 51 ER - TY - JOUR AB - The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a distance for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces, and how to synthesize an interface from incompatible requirements. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies. AU - Cerny, Pavol AU - Chmelik, Martin AU - Henzinger, Thomas A AU - Radhakrishna, Arjun ID - 1733 IS - 3 JF - Theoretical Computer Science TI - Interface simulation distances VL - 560 ER - TY - JOUR AB - The computation of the winning set for Büchi objectives in alternating games on graphs is a central problem in computer-aided verification with a large number of applications. The long-standing best known upper bound for solving the problem is Õ(n ⋅ m), where n is the number of vertices and m is the number of edges in the graph. We are the first to break the Õ(n ⋅ m) boundary by presenting a new technique that reduces the running time to O(n2). This bound also leads to O(n2)-time algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of Õ(n ⋅ m)), (2) in concurrent graph games with constant actions (improving an earlier bound of O(n3)), and (3) in Markov decision processes (improving for m>n4/3 an earlier bound of O(m ⋅ √m)). We then show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per operation. Our algorithms are the first dynamic algorithms for this problem. We then consider another core graph theoretic problem in verification of probabilistic systems, namely computing the maximal end-component decomposition of a graph. We present two improved static algorithms for the maximal end-component decomposition problem. Our first algorithm is an O(m ⋅ √m)-time algorithm, and our second algorithm is an O(n2)-time algorithm which is obtained using the same technique as for alternating Büchi games. Thus, we obtain an O(min &lcu;m ⋅ √m,n2})-time algorithm improving the long-standing O(n ⋅ m) time bound. Finally, we show how to maintain the maximal end-component decomposition of a graph under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per edge deletion, and O(m) worst-case time per edge insertion. Again, our algorithms are the first dynamic algorithms for this problem. AU - Chatterjee, Krishnendu AU - Henzinger, Monika H ID - 2141 IS - 3 JF - Journal of the ACM TI - Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition VL - 61 ER - TY - CONF AB - We study two-player concurrent games on finite-state graphs played for an infinite number of rounds, where in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. The objectives are ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respectively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). While the qualitative analysis problem for concurrent parity games with infinite-memory, infinite-precision randomized strategies was studied before, we study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision, or infinite-precision; and in terms of memory, strategies can be memoryless, finite-memory, or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as powerful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in (n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. Our symbolic algorithms are based on a characterization of the winning sets as μ-calculus formulas, however, our μ-calculus formulas are crucially different from the ones for concurrent parity games (without bounded rationality); and our memoryless witness strategy constructions are significantly different from the infinite-memory witness strategy constructions for concurrent parity games. AU - Chatterjee, Krishnendu ED - Baldan, Paolo ED - Gorla, Daniele ID - 2054 T2 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) TI - Qualitative concurrent parity games: Bounded rationality VL - 8704 ER - TY - CONF AB - First cycle games (FCG) are played on a finite graph by two players who push a token along the edges until a vertex is repeated, and a simple cycle is formed. The winner is determined by some fixed property Y of the sequence of labels of the edges (or nodes) forming this cycle. These games are traditionally of interest because of their connection with infinite-duration games such as parity and mean-payoff games. We study the memory requirements for winning strategies of FCGs and certain associated infinite duration games. We exhibit a simple FCG that is not memoryless determined (this corrects a mistake in Memoryless determinacy of parity and mean payoff games: a simple proof by Bj⋯orklund, Sandberg, Vorobyov (2004) that claims that FCGs for which Y is closed under cyclic permutations are memoryless determined). We show that θ (n)! memory (where n is the number of nodes in the graph), which is always sufficient, may be necessary to win some FCGs. On the other hand, we identify easy to check conditions on Y (i.e., Y is closed under cyclic permutations, and both Y and its complement are closed under concatenation) that are sufficient to ensure that the corresponding FCGs and their associated infinite duration games are memoryless determined. We demonstrate that many games considered in the literature, such as mean-payoff, parity, energy, etc., satisfy these conditions. On the complexity side, we show (for efficiently computable Y) that while solving FCGs is in PSPACE, solving some families of FCGs is PSPACE-hard. AU - Aminof, Benjamin AU - Rubin, Sasha ID - 475 T2 - Electronic Proceedings in Theoretical Computer Science, EPTCS TI - First cycle games VL - 146 ER - TY - CONF AB - We consider two-player zero-sum partial-observation stochastic games on graphs. Based on the information available to the players these games can be classified as follows: (a) general partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) perfect-observation (both players have complete view of the game). The one-sided partial-observation games subsumes the important special case of one-player partial-observation stochastic games (or partial-observation Markov decision processes (POMDPs)). Based on the randomization available for the strategies, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. We consider all these classes of games with reachability, and parity objectives that can express all ω-regular objectives. The analysis problems are classified into the qualitative analysis that asks for the existence of a strategy that ensures the objective with probability 1; and the quantitative analysis that asks for the existence of a strategy that ensures the objective with probability at least λ (0,1). In this talk we will cover a wide range of results: for perfect-observation games; for POMDPs; for one-sided partial-observation games; and for general partial-observation games. AU - Chatterjee, Krishnendu ID - 1903 IS - PART 1 TI - Partial-observation stochastic reachability and parity games VL - 8634 ER - TY - JOUR AB - In two-player finite-state stochastic games of partial observation on graphs, in every state of the graph, the players simultaneously choose an action, and their joint actions determine a probability distribution over the successor states. The game is played for infinitely many rounds and thus the players construct an infinite path in the graph. We consider reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1) or positively (i.e., with positive probability), no matter the strategy of the second player. We classify such games according to the information and to the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation (and the other player has perfect observation), or two-sided with (c) both players having partial observation. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Our main results for pure strategies are as follows: (1) For one-sided games with player 2 having perfect observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strategies are not sufficient, and we present an exponential upper bound on memory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete and present symbolic algorithms that avoid the explicit exponential construction. (2) For one-sided games with player 1 having perfect observation we show that nonelementarymemory is both necessary and sufficient for both almost-sure and positive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least nonelementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibit serious flaws in previous results of the literature: we show a nonelementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed. AU - Chatterjee, Krishnendu AU - Doyen, Laurent ID - 2211 IS - 2 JF - ACM Transactions on Computational Logic (TOCL) TI - Partial-observation stochastic games: How to win when belief fails VL - 15 ER - TY - JOUR AB - Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions. At the heart of quantitative objectives lies the accumulation of values along a computation. It is often the accumulated sum, as with energy objectives, or the accumulated average, as with mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point in time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire infinite computation. We study the border of decidability for such quantitative extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with both prefix-accumulation assertions, or extending LTL with both path-accumulation assertions, results in temporal logics whose model-checking problem is decidable. Moreover, the prefix-accumulation assertions may be generalized with "controlled accumulation," allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that this branching-time logic is, in a sense, the maximal logic with one or both of the prefix-accumulation assertions that permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL, makes the problem undecidable. AU - Boker, Udi AU - Chatterjee, Krishnendu AU - Henzinger, Thomas A AU - Kupferman, Orna ID - 2038 IS - 4 JF - ACM Transactions on Computational Logic (TOCL) TI - Temporal specifications with accumulative values VL - 15 ER - TY - CONF AB - We study two-player (zero-sum) concurrent mean-payoff games played on a finite-state graph. We focus on the important sub-class of ergodic games where all states are visited infinitely often with probability 1. The algorithmic study of ergodic games was initiated in a seminal work of Hoffman and Karp in 1966, but all basic complexity questions have remained unresolved. Our main results for ergodic games are as follows: We establish (1) an optimal exponential bound on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy); (2) the approximation problem lies in FNP; (3) the approximation problem is at least as hard as the decision problem for simple stochastic games (for which NP ∩ coNP is the long-standing best known bound). We present a variant of the strategy-iteration algorithm by Hoffman and Karp; show that both our algorithm and the classical value-iteration algorithm can approximate the value in exponential time; and identify a subclass where the value-iteration algorithm is a FPTAS. We also show that the exact value can be expressed in the existential theory of the reals, and establish square-root sum hardness for a related class of games. AU - Chatterjee, Krishnendu AU - Ibsen-Jensen, Rasmus ID - 2162 IS - Part 2 TI - The complexity of ergodic mean payoff games VL - 8573 ER - TY - CONF AB - We consider two-player partial-observation stochastic games on finitestate graphs where player 1 has partial observation and player 2 has perfect observation. The winning condition we study are ε-regular conditions specified as parity objectives. The qualitative-analysis problem given a partial-observation stochastic game and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). These qualitative-analysis problems are known to be undecidable. However in many applications the relevant question is the existence of finite-memory strategies, and the qualitative-analysis problems under finite-memory strategies was recently shown to be decidable in 2EXPTIME.We improve the complexity and show that the qualitative-analysis problems for partial-observation stochastic parity games under finite-memory strategies are EXPTIME-complete; and also establish optimal (exponential) memory bounds for finite-memory strategies required for qualitative analysis. AU - Chatterjee, Krishnendu AU - Doyen, Laurent AU - Nain, Sumit AU - Vardi, Moshe ID - 2213 TI - The complexity of partial-observation stochastic parity games with finite-memory strategies VL - 8412 ER - TY - CONF AB - The theory of graph games is the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic processes, we use 2 1/2-player games where some transitions of the game graph are controlled by two adversarial players, the System and the Environment, and the other transitions are determined probabilistically. We consider 2 1/2-player games where the objective of the System is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). We establish that the problem of deciding whether the System can ensure that the probability to satisfy the mean-payoff parity objective is at least a given threshold is in NP ∩ coNP, matching the best known bound in the special case of 2-player games (where all transitions are deterministic). We present an algorithm running in time O(d·n2d·MeanGame) to compute the set of almost-sure winning states from which the objective can be ensured with probability 1, where n is the number of states of the game, d the number of priorities of the parity objective, and MeanGame is the complexity to compute the set of almost-sure winning states in 2 1/2-player mean-payoff games. Our results are useful in the synthesis of stochastic reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective). AU - Chatterjee, Krishnendu AU - Doyen, Laurent AU - Gimbert, Hugo AU - Oualhadj, Youssouf ID - 2212 TI - Perfect-information stochastic mean-payoff parity games VL - 8412 ER - TY - CONF AB - The edit distance between two (untimed) traces is the minimum cost of a sequence of edit operations (insertion, deletion, or substitution) needed to transform one trace to the other. Edit distances have been extensively studied in the untimed setting, and form the basis for approximate matching of sequences in different domains such as coding theory, parsing, and speech recognition. In this paper, we lift the study of edit distances from untimed languages to the timed setting. We define an edit distance between timed words which incorporates both the edit distance between the untimed words and the absolute difference in time stamps. Our edit distance between two timed words is computable in polynomial time. Further, we show that the edit distance between a timed word and a timed language generated by a timed automaton, defined as the edit distance between the word and the closest word in the language, is PSPACE-complete. While computing the edit distance between two timed automata is undecidable, we show that the approximate version, where we decide if the edit distance between two timed automata is either less than a given parameter or more than δ away from the parameter, for δ > 0, can be solved in exponential space and is EXPSPACE-hard. Our definitions and techniques can be generalized to the setting of hybrid systems, and analogous decidability results hold for rectangular automata. AU - Chatterjee, Krishnendu AU - Ibsen-Jensen, Rasmus AU - Majumdar, Ritankar ID - 2216 TI - Edit distance for timed automata ER - TY - GEN AB - We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. AU - Chatterjee, Krishnendu AU - Daca, Przemyslaw AU - Chmelik, Martin ID - 5413 SN - 2664-1690 TI - CEGAR for qualitative analysis of probabilistic systems ER - TY - GEN AB - We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. AU - Chatterjee, Krishnendu AU - Daca, Przemyslaw AU - Chmelik, Martin ID - 5414 SN - 2664-1690 TI - CEGAR for qualitative analysis of probabilistic systems ER - TY - GEN AB - We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. AU - Chatterjee, Krishnendu AU - Daca, Przemyslaw AU - Chmelik, Martin ID - 5412 SN - 2664-1690 TI - CEGAR for qualitative analysis of probabilistic systems ER - TY - CONF AB - We consider multi-player graph games with partial-observation and parity objective. While the decision problem for three-player games with a coalition of the first and second players against the third player is undecidable in general, we present a decidability result for partial-observation games where the first and third player are in a coalition against the second player, thus where the second player is adversarial but weaker due to partial-observation. We establish tight complexity bounds in the case where player 1 is less informed than player 2, namely 2-EXPTIME-completeness for parity objectives. The symmetric case of player 1 more informed than player 2 is much more complicated, and we show that already in the case where player 1 has perfect observation, memory of size non-elementary is necessary in general for reachability objectives, and the problem is decidable for safety and reachability objectives. From our results we derive new complexity results for partial-observation stochastic games. AU - Chatterjee, Krishnendu AU - Doyen, Laurent ID - 2163 IS - Part 2 T2 - Lecture Notes in Computer Science TI - Games with a weak adversary VL - 8573 ER - TY - GEN AB - We consider the reachability and shortest path problems on low tree-width graphs, with n nodes, m edges, and tree-width t, on a standard RAM with wordsize W. We use O to hide polynomial factors of the inverse of the Ackermann function. Our main contributions are three fold: 1. For reachability, we present an algorithm that requires O(n·t2·log(n/t)) preprocessing time, O(n·(t·log(n/t))/W) space, and O(t/W) time for pair queries and O((n·t)/W) time for single-source queries. Note that for constant t our algorithm uses O(n·logn) time for preprocessing; and O(n/W) time for single-source queries, which is faster than depth first search/breath first search (after the preprocessing). 2. We present an algorithm for shortest path that requires O(n·t2) preprocessing time, O(n·t) space, and O(t2) time for pair queries and O(n·t) time single-source queries. 3. We give a space versus query time trade-off algorithm for shortest path that, given any constant >0, requires O(n·t2) preprocessing time, O(n·t2) space, and O(n1−·t2) time for pair queries. Our algorithms improve all existing results, and use very simple data structures. AU - Chatterjee, Krishnendu AU - Ibsen-Jensen, Rasmus AU - Pavlogiannis, Andreas ID - 5419 SN - 2664-1690 TI - Improved algorithms for reachability and shortest path on low tree-width graphs ER - TY - GEN AB - We consider multi-player graph games with partial-observation and parity objective. While the decision problem for three-player games with a coalition of the first and second players against the third player is undecidable, we present a decidability result for partial-observation games where the first and third player are in a coalition against the second player, thus where the second player is adversarial but weaker due to partial-observation. We establish tight complexity bounds in the case where player 1 is less informed than player 2, namely 2-EXPTIME-completeness for parity objectives. The symmetric case of player 1 more informed than player 2 is much more complicated, and we show that already in the case where player 1 has perfect observation, memory of size non-elementary is necessary in general for reachability objectives, and the problem is decidable for safety and reachability objectives. Our results have tight connections with partial-observation stochastic games for which we derive new complexity results. AU - Chatterjee, Krishnendu AU - Doyen, Laurent ID - 5418 SN - 2664-1690 TI - Games with a weak adversary ER - TY - GEN AB - We consider concurrent mean-payoff games, a very well-studied class of two-player (player 1 vs player 2) zero-sum games on finite-state graphs where every transition is assigned a reward between 0 and 1, and the payoff function is the long-run average of the rewards. The value is the maximal expected payoff that player 1 can guarantee against all strategies of player 2. We consider the computation of the set of states with value 1 under finite-memory strategies for player 1, and our main results for the problem are as follows: (1) we present a polynomial-time algorithm; (2) we show that whenever there is a finite-memory strategy, there is a stationary strategy that does not need memory at all; and (3) we present an optimal bound (which is double exponential) on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy). AU - Chatterjee, Krishnendu AU - Ibsen-Jensen, Rasmus ID - 5420 SN - 2664-1690 TI - The value 1 problem for concurrent mean-payoff games ER - TY - GEN AB - We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty. AU - Chatterjee, Krishnendu AU - Chmelik, Martin AU - Gupta, Raghav AU - Kanodia, Ayush ID - 5424 SN - 2664-1690 TI - Qualitative analysis of POMDPs with temporal logic specifications for robotics applications ER - TY - GEN AB - We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty. AU - Chatterjee, Krishnendu AU - Chmelik, Martin AU - Gupta, Raghav AU - Kanodia, Ayush ID - 5426 SN - 2664-1690 TI - Qualitative analysis of POMDPs with temporal logic specifications for robotics applications ER - TY - GEN AB - We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm- deadline real-time tasks based on multi-objective graphs: Given a taskset and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. a clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including D(over), that have been proposed in the past, for various tasksets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are tasksets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application. AU - Chatterjee, Krishnendu AU - Kössler, Alexander AU - Pavlogiannis, Andreas AU - Schmid, Ulrich ID - 5423 SN - 2664-1690 TI - A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks ER - TY - GEN AB - We consider graphs with n nodes together with their tree-decomposition that has b = O ( n ) bags and width t , on the standard RAM computational model with wordsize W = Θ (log n ) . Our contributions are two-fold: Our first contribution is an algorithm that given a graph and its tree-decomposition as input, computes a binary and balanced tree-decomposition of width at most 4 · t + 3 of the graph in O ( b ) time and space, improving a long-standing (from 1992) bound of O ( n · log n ) time for constant treewidth graphs. Our second contribution is on reachability queries for low treewidth graphs. We build on our tree-balancing algorithm and present a data-structure for graph reachability that requires O ( n · t 2 ) preprocessing time, O ( n · t ) space, and O ( d t/ log n e ) time for pair queries, and O ( n · t · log t/ log n ) time for single-source queries. For constant t our data-structure uses O ( n ) time for preprocessing, O (1) time for pair queries, and O ( n/ log n ) time for single-source queries. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries. AU - Chatterjee, Krishnendu AU - Ibsen-Jensen, Rasmus AU - Pavlogiannis, Andreas ID - 5427 SN - 2664-1690 TI - Optimal tree-decomposition balancing and reachability on low treewidth graphs ER - TY - GEN AB - Recently there has been a significant effort to add 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, several basic system properties such as average response time cannot be expressed with weighted automata. In this work, we introduce nested weighted automata as a new formalism for expressing important quantitative properties such as average response time. We establish an almost complete decidability picture for the basic decision problems for nested weighted automata, and illustrate its applicability in several domains. AU - Chatterjee, Krishnendu AU - Henzinger, Thomas A AU - Otop, Jan ID - 5415 SN - 2664-1690 TI - Nested weighted automata ER - TY - GEN AB - Evolution occurs in populations of reproducing individuals. The structure of the population affects the outcome of the evolutionary process. Evolutionary graph theory is a powerful approach to study this phenomenon. There are two graphs. The interaction graph specifies who interacts with whom in the context of evolution. The replacement graph specifies who competes with whom for reproduction. The vertices of the two graphs are the same, and each vertex corresponds to an individual. A key quantity is the fixation probability of a new mutant. It is defined as the probability that a newly introduced mutant (on a single vertex) generates a lineage of offspring which eventually takes over the entire population of resident individuals. The basic computational questions are as follows: (i) the qualitative question asks whether the fixation probability is positive; and (ii) the quantitative approximation question asks for an approximation of the fixation probability. Our main results are: (1) We show that the qualitative question is NP-complete and the quantitative approximation question is #P-hard in the special case when the interaction and the replacement graphs coincide and even with the restriction that the resident individuals do not reproduce (which corresponds to an invading population taking over an empty structure). (2) We show that in general the qualitative question is PSPACE-complete and the quantitative approximation question is PSPACE-hard and can be solved in exponential time. AU - Chatterjee, Krishnendu AU - Ibsen-Jensen, Rasmus AU - Nowak, Martin ID - 5421 SN - 2664-1690 TI - The complexity of evolution on graphs ER - TY - CONF AB - Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games. In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated. We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games.We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games. AU - Chatterjee, Krishnendu AU - Doyen, Laurent AU - Filiot, Emmanuel AU - Raskin, Jean-François ID - 10885 SN - 0302-9743 T2 - VMCAI 2014: Verification, Model Checking, and Abstract Interpretation TI - Doomsday equilibria for omega-regular games VL - 8318 ER - TY - JOUR AB - A fundamental question in biology is the following: what is the time scale that is needed for evolutionary innovations? There are many results that characterize single steps in terms of the fixation time of new mutants arising in populations of certain size and structure. But here we ask a different question, which is concerned with the much longer time scale of evolutionary trajectories: how long does it take for a population exploring a fitness landscape to find target sequences that encode new biological functions? Our key variable is the length, (Formula presented.) of the genetic sequence that undergoes adaptation. In computer science there is a crucial distinction between problems that require algorithms which take polynomial or exponential time. The latter are considered to be intractable. Here we develop a theoretical approach that allows us to estimate the time of evolution as function of (Formula presented.) We show that adaptation on many fitness landscapes takes time that is exponential in (Formula presented.) even if there are broad selection gradients and many targets uniformly distributed in sequence space. These negative results lead us to search for specific mechanisms that allow evolution to work on polynomial time scales. We study a regeneration process and show that it enables evolution to work in polynomial time. AU - Chatterjee, Krishnendu AU - Pavlogiannis, Andreas AU - Adlam, Ben AU - Nowak, Martin ID - 2039 IS - 9 JF - PLoS Computational Biology TI - The time scale of evolutionary innovation VL - 10 ER - TY - GEN AU - Chatterjee, Krishnendu AU - Pavlogiannis, Andreas AU - Adlam, Ben AU - Novak, Martin ID - 9739 TI - Detailed proofs for “The time scale of evolutionary innovation” ER - TY - JOUR AB - 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 NP∩co-NP, but are not known to be in 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 developing 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. AU - Chatterjee, Krishnendu AU - Henzinger, Monika H AU - Krinninger, Sebastian AU - Nanongkai, Danupon ID - 535 IS - 3 JF - Algorithmica TI - Polynomial-time algorithms for energy games with special weight structures VL - 70 ER - TY - CONF AB - We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation ofMDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.We present an automated technique for assume-guarantee style reasoning for compositional analysis ofMDPs with qualitative properties by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. AU - Chatterjee, Krishnendu AU - Chmelik, Martin AU - Daca, Przemyslaw ID - 2063 TI - CEGAR for qualitative analysis of probabilistic systems VL - 8559 ER - TY - GEN AB - Simulation is an attractive alternative for language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. For non-deterministic automata, while language inclusion is PSPACE-complete, simulation can be computed in polynomial time. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. Again, while fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable for mean-payoff automata and the decidability is open for discounted-sum automata, whereas the (quantitative) simulation reduce to mean-payoff games and discounted-sum games, which admit pseudo-polynomial time algorithms. In this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games. For example, whereas for mean-payoff and discounted-sum games, the players do not need memory to play optimally; we show in contrast that for simulation games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal strategies for both players require infinite memory in general, and (ii) for discounted-sum objectives, optimal strategies need not exist for both players. While the simulation games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory requirements for mean-payoff objectives) as compared to their counterpart without Büchi acceptance conditions, we still present pseudo-polynomial time algorithms to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff and weighted discounted-sum automata. AU - Chatterjee, Krishnendu AU - Henzinger, Thomas A AU - Otop, Jan AU - Velner, Yaron ID - 5428 SN - 2664-1690 TI - Quantitative fair simulation games ER - TY - CONF AB - We study two-player zero-sum games over infinite-state graphs equipped with ωB and finitary conditions. Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games. We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with ωB-conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete. AU - Chatterjee, Krishnendu AU - Fijalkow, Nathanaël ID - 1374 T2 - 22nd EACSL Annual Conference on Computer Science Logic TI - Infinite-state games with finitary conditions VL - 23 ER - TY - CONF AB - We study the problem of achieving a given value in Markov decision processes (MDPs) with several independent discounted reward objectives. We consider a generalised version of discounted reward objectives, in which the amount of discounting depends on the states visited and on the objective. This definition extends the usual definition of discounted reward, and allows to capture the systems in which the value of different commodities diminish at different and variable rates. We establish results for two prominent subclasses of the problem, namely state-discount models where the discount factors are only dependent on the state of the MDP (and independent of the objective), and reward-discount models where they are only dependent on the objective (but not on the state of the MDP). For the state-discount models we use a straightforward reduction to expected total reward and show that the problem whether a value is achievable can be solved in polynomial time. For the reward-discount model we show that memory and randomisation of the strategies are required, but nevertheless that the problem is decidable and it is sufficient to consider strategies which after a certain number of steps behave in a memoryless way. For the general case, we show that when restricted to graphs (i.e. MDPs with no randomisation), pure strategies and discount factors of the form 1/n where n is an integer, the problem is in PSPACE and finite memory suffices for achieving a given value. We also show that when the discount factors are not of the form 1/n, the memory required by a strategy can be infinite. AU - Chatterjee, Krishnendu AU - Forejt, Vojtěch AU - Wojtczak, Dominik ID - 2238 TI - Multi-objective discounted reward verification in graphs and MDPs VL - 8312 ER - TY - GEN AB - This book constitutes the thoroughly refereed conference proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science, MFCS 2013, held in Klosterneuburg, Austria, in August 2013. The 67 revised full papers presented together with six invited talks were carefully selected from 191 submissions. Topics covered include algorithmic game theory, algorithmic learning theory, algorithms and data structures, automata, formal languages, bioinformatics, complexity, computational geometry, computer-assisted reasoning, concurrency theory, databases and knowledge-based systems, foundations of computing, logic in computer science, models of computation, semantics and verification of programs, and theoretical issues in artificial intelligence. ED - Chatterjee, Krishnendu ED - Sgall, Jiri ID - 2292 SN - 978-3-642-40312-5 TI - Mathematical Foundations of Computer Science 2013 VL - 8087 ER - TY - JOUR AB - The standard hardware design flow involves: (a) design of an integrated circuit using a hardware description language, (b) extensive functional and formal verification, and (c) logical synthesis. However, the above-mentioned processes consume significant effort and time. An alternative approach is to use a formal specification language as a high-level hardware description language and synthesize hardware from formal specifications. Our work is a case study of the synthesis of the widely and industrially used AMBA AHB protocol from formal specifications. Bloem et al. presented the first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter circuit. However, in the first formal specification some important assumptions were missing. Our contributions are as follows: (a) We present detailed formal specifications for the AHB Arbiter incorporating the missing details, and obtain significant improvements in the synthesis results (both with respect to the number of gates in the synthesized circuit and with respect to the time taken to synthesize the circuit), and (b) we present formal specifications to generate compact circuits for the remaining two main components of AMBA AHB, namely, AHB Master and AHB Slave. Thus with systematic description we are able to automatically and completely synthesize an important and widely used industrial protocol. AU - Godhal, Yashdeep AU - Chatterjee, Krishnendu AU - Henzinger, Thomas A ID - 2299 IS - 5-6 JF - International Journal on Software Tools for Technology Transfer TI - Synthesis of AMBA AHB from formal specification: A case study VL - 15 ER - TY - CONF AB - The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements. AU - Chatterjee, Krishnendu AU - Gaiser, Andreas AU - Kretinsky, Jan ID - 2446 TI - Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis VL - 8044 ER - TY - CONF AB - We consider two core algorithmic problems for probabilistic verification: the maximal end-component decomposition and the almost-sure reachability set computation for Markov decision processes (MDPs). For MDPs with treewidth k, we present two improved static algorithms for both the problems that run in time O(n·k 2.38·2k ) and O(m·logn· k), respectively, where n is the number of states and m is the number of edges, significantly improving the previous known O(n·k·√n· k) bound for low treewidth. We also present decremental algorithms for both problems for MDPs with constant treewidth that run in amortized logarithmic time, which is a huge improvement over the previously known algorithms that require amortized linear time. AU - Chatterjee, Krishnendu AU - Ła̧Cki, Jakub ID - 2444 TI - Faster algorithms for Markov decision processes with low treewidth VL - 8044 ER - TY - JOUR AB - We study the problem of generating a test sequence that achieves maximal coverage for a reactive system under test. We formulate the problem as a repeated game between the tester and the system, where the system state space is partitioned according to some coverage criterion and the objective of the tester is to maximize the set of partitions (or coverage goals) visited during the game. We show the complexity of the maximal coverage problem for non-deterministic systems is PSPACE-complete, but is NP-complete for deterministic systems. For the special case of non-deterministic systems with a re-initializing "reset" action, which represent running a new test input on a re-initialized system, we show that the complexity is coNP-complete. Our proof technique for reset games uses randomized testing strategies that circumvent the exponentially large memory requirement of deterministic testing strategies. We also discuss the memory requirement for deterministic strategies and extensions of our results to other models, such as pushdown systems and timed systems. AU - Chatterjee, Krishnendu AU - Alfaro, Luca AU - Majumdar, Ritankar ID - 2814 IS - 2 JF - International Journal of Foundations of Computer Science TI - The complexity of coverage VL - 24 ER - TY - JOUR AB - The basic idea of evolutionary game theory is that payoff determines reproductive rate. Successful individuals have a higher payoff and produce more offspring. But in evolutionary and ecological situations there is not only reproductive rate but also carrying capacity. Individuals may differ in their exposure to density limiting effects. Here we explore an alternative approach to evolutionary game theory by assuming that the payoff from the game determines the carrying capacity of individual phenotypes. Successful strategies are less affected by density limitation (crowding) and reach higher equilibrium abundance. We demonstrate similarities and differences between our framework and the standard replicator equation. Our equation is defined on the positive orthant, instead of the simplex, but has the same equilibrium points as the replicator equation. Linear stability analysis produces the classical conditions for asymptotic stability of pure strategies, but the stability properties of internal equilibria can differ in the two frameworks. For example, in a two-strategy game with an internal equilibrium that is always stable under the replicator equation, the corresponding equilibrium can be unstable in the new framework resulting in a limit cycle. AU - Novak, Sebastian AU - Chatterjee, Krishnendu AU - Nowak, Martin ID - 2817 JF - Journal of Theoretical Biology TI - Density games VL - 334 ER - TY - CONF AB - We introduce quantatitive timed refinement metrics and quantitative timed simulation functions, incorporating zenoness checks, for timed systems. These functions assign positive real numbers between zero and infinity which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximum timing mismatch that can arise, (2) the "steady-state" maximum timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation functions to within any desired degree of accuracy. In order to compute the values of the quantitative simulation functions, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives for player 1, and then use these algorithms to compute the values of the quantitative timed simulation functions. AU - Chatterjee, Krishnendu AU - Prabhu, Vinayak ID - 2819 T2 - Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control TI - Quantitative timed simulation functions and refinement metrics for real-time systems VL - 1 ER - TY - JOUR AB - We study synthesis of controllers for real-time systems, where the objective is to stay in a given safe set. The problem is solved by obtaining winning strategies in the setting of concurrent two player timed automaton games with safety objectives. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a Zeno run. We construct winning strategies for the controller which require access only to (1) the system clocks (thus, controllers which require their own internal infinitely precise clocks are not necessary), and (2) a logarithmic (in the number of clocks) number of memory bits (i.e. a linear number of memory states). Precisely, we show that for safety objectives, a memory of size (3 + lg (| C | + 1)) bits suffices for winning controller strategies, where C is the set of clocks of the timed automaton game, significantly improving the previous known exponential memory states bound. We also settle the open question of whether winning region-based strategies require memory for safety objectives by showing with an example the necessity of memory for such strategies to win for safety objectives. Finally, we show that the decision problem of determining if there exists a receptive player-1 winning strategy for safety objectives is EXPTIME-complete over timed automaton games. AU - Chatterjee, Krishnendu AU - Prabhu, Vinayak ID - 2824 JF - Information and Computation TI - Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems VL - 228-229 ER - TY - JOUR AB - We study the automatic synthesis of fair non-repudiation protocols, a class of fair exchange protocols, used for digital contract signing. First, we show how to specify the objectives of the participating agents and the trusted third party as path formulas in linear temporal logic and prove that the satisfaction of these objectives imply fairness; a property required of fair exchange protocols. We then show that weak (co-operative) co-synthesis and classical (strictly competitive) co-synthesis fail, whereas assume-guarantee synthesis (AGS) succeeds. We demonstrate the success of AGS as follows: (a) any solution of AGS is attack-free; no subset of participants can violate the objectives of the other participants; (b) the Asokan-Shoup-Waidner certified mail protocol that has known vulnerabilities is not a solution of AGS; (c) the Kremer-Markowitch non-repudiation protocol is a solution of AGS; and (d) AGS presents a new and symmetric fair non-repudiation protocol that is attack-free. To our knowledge this is the first application of synthesis to fair non-repudiation protocols, and our results show how synthesis can both automatically discover vulnerabilities in protocols and generate correct protocols. The solution to AGS can be computed efficiently as the secure equilibrium solution of three-player graph games. AU - Chatterjee, Krishnendu AU - Raman, Vishwanath ID - 2836 IS - 4 JF - Formal Aspects of Computing TI - Assume-guarantee synthesis for digital contract signing VL - 26 ER - TY - JOUR AB - We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay forever in a given set of states, and its dual, the reachability objective to reach a given set of states. First, we present a simple proof of the fact that in concurrent reachability games, for all ε>0, memoryless ε-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an ε-optimal strategy achieves the objective with probability within ε of the value of the game. In contrast to previous proofs of this fact, our proof is more elementary and more combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives. Finally, we present a strategy-improvement algorithm for turn-based stochastic games (where each player selects moves in turns) with safety objectives. Our algorithms yield sequences of player-1 strategies which ensure probabilities of winning that converge monotonically (from below) to the value of the game. © 2012 Elsevier Inc. AU - Chatterjee, Krishnendu AU - De Alfaro, Luca AU - Henzinger, Thomas A ID - 2854 IS - 5 JF - Journal of Computer and System Sciences TI - Strategy improvement for concurrent reachability and turn based stochastic safety games VL - 79 ER - TY - CONF AB - We focus on the realizability problem of Message Sequence Graphs (MSG), i.e. the problem whether a given MSG specification is correctly distributable among parallel components communicating via messages. This fundamental problem of MSG is known to be undecidable. We introduce a well motivated restricted class of MSG, so called controllable-choice MSG, and show that all its models are realizable and moreover it is decidable whether a given MSG model is a member of this class. In more detail, this class of MSG specifications admits a deadlock-free realization by overloading existing messages with additional bounded control data. We also show that the presented class is the largest known subclass of MSG that allows for deadlock-free realization. AU - Chmelik, Martin AU - Řehák, Vojtěch ID - 2886 TI - Controllable-choice message sequence graphs VL - 7721 ER - TY - JOUR AB - Multithreaded programs coordinate their interaction through synchronization primitives like mutexes and semaphores, which are managed by an OS-provided resource manager. We propose algorithms for the automatic construction of code-aware resource managers for multithreaded embedded applications. Such managers use knowledge about the structure and resource usage (mutex and semaphore usage) of the threads to guarantee deadlock freedom and progress while managing resources in an efficient way. Our algorithms compute managers as winning strategies in certain infinite games, and produce a compact code description of these strategies. We have implemented the algorithms in the tool Cynthesis. Given a multithreaded program in C, the tool produces C code implementing a code-aware resource manager. We show in experiments that Cynthesis produces compact resource managers within a few minutes on a set of embedded benchmarks with up to 6 threads. © 2012 Springer Science+Business Media, LLC. AU - Chatterjee, Krishnendu AU - De Alfaro, Luca AU - Faella, Marco AU - Majumdar, Ritankar AU - Raman, Vishwanath ID - 3116 IS - 2 JF - Formal Methods in System Design TI - Code aware resource management VL - 42 ER - TY - JOUR AB - We consider Markov decision processes (MDPs) with Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almost-sure winning set for MDPs with Büchi objectives; our algorithm takes O(n · √ m) symbolic steps as compared to the previous known algorithm that takes O(n 2) symbolic steps, where n is the number of states and m is the number of edges of the MDP. In practice MDPs have constant out-degree, and then our symbolic algorithm takes O(n · √ n) symbolic steps, as compared to the previous known O(n 2) symbolic steps algorithm. Second, we present a new algorithm, namely win-lose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almost-sure winning set and its complement, as compared to all previous algorithms that discover the almost-sure winning set upon termination; and (b) requires O(n · √ K) symbolic steps, where K is the maximal number of edges of strongly connected components (scc's) of the MDP. The win-lose algorithm requires symbolic computation of scc's. Third, we improve the algorithm for symbolic scc computation; the previous known algorithm takes linear symbolic steps, and our new algorithm improves the constants associated with the linear number of steps. In the worst case the previous known algorithm takes 5×n symbolic steps, whereas our new algorithm takes 4×n symbolic steps. AU - Chatterjee, Krishnendu AU - Henzinger, Monika H AU - Joglekar, Manas AU - Shah, Nisarg ID - 2831 IS - 3 JF - Formal Methods in System Design TI - Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives VL - 42 ER - TY - CONF AB - We consider two-player games played on weighted directed graphs with mean-payoff and total-payoff objectives, two classical quantitative objectives. While for single-dimensional games the complexity and memory bounds for both objectives coincide, we show that in contrast to multi-dimensional mean-payoff games that are known to be coNP-complete, multi-dimensional total-payoff games are undecidable. We introduce conservative approximations of these objectives, where the payoff is considered over a local finite window sliding along a play, instead of the whole play. For single dimension, we show that (i) if the window size is polynomial, deciding the winner takes polynomial time, and (ii) the existence of a bounded window can be decided in NP ∩ coNP, and is at least as hard as solving mean-payoff games. For multiple dimensions, we show that (i) the problem with fixed window size is EXPTIME-complete, and (ii) there is no primitive-recursive algorithm to decide the existence of a bounded window. AU - Chatterjee, Krishnendu AU - Doyen, Laurent AU - Randour, Mickael AU - Raskin, Jean ID - 2279 TI - Looking at mean-payoff and total-payoff through windows VL - 8172 ER - TY - GEN AB - In this work we present a flexible tool for tumor progression, which simulates the evolutionary dynamics of cancer. Tumor progression implements a multi-type branching process where the key parameters are the fitness landscape, the mutation rate, and the average time of cell division. The fitness of a cancer cell depends on the mutations it has accumulated. The input to our tool could be any fitness landscape, mutation rate, and cell division time, and the tool produces the growth dynamics and all relevant statistics. AU - Reiter, Johannes AU - Bozic, Ivana AU - Chatterjee, Krishnendu AU - Nowak, Martin ID - 5399 SN - 2664-1690 TI - TTP: Tool for Tumor Progression ER -