@inproceedings{3865,
abstract = {We introduce a technique for debugging multi-threaded C programs and analyzing the impact of source code changes, and its implementation in the prototype tool DIRECT. Our approach uses a combination of source code instrumentation and runtime management. The source code along with a test harness is instrumented to monitor Operating System (OS) and user defined function calls. DIRECT tracks all concurrency control primitives and, optionally, data from the program. DIRECT maintains an abstract global state that combines information from every thread, including the sequence of function calls and concurrency primitives executed. The runtime manager can insert delays, provoking thread inter-leavings that may exhibit bugs that are difficult to reach otherwise. The runtime manager collects an approximation of the reachable state space and uses this approximation to assess the impact of change in a new version of the program.},
author = {Chatterjee, Krishnendu and De Alfaro, Luca and Raman, Vishwanath and Sánchez, César},
editor = {Rosenblum, David and Taenzer, Gabriele},
location = {Paphos, Cyprus},
pages = {293 -- 307},
publisher = {Springer},
title = {{Analyzing the impact of change in multi-threaded programs}},
doi = {10.1007/978-3-642-12029-9_21},
volume = {6013},
year = {2010},
}
@inproceedings{3866,
abstract = {Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which prescribes, for any number of environment assumptions that are violated, a minimal number of system guarantees that must still be fulfilled. This notion of robustness can be formulated and realized using a Generalized Reactivity formula. We present an algorithm for synthesizing robust systems from such formulas. For the important special case of Generalized Reactivity formulas of rank 1, our algorithm improves the complexity of [PPS06] for large specifications with a small number of assumptions and guarantees.},
author = {Bloem, Roderick and Chatterjee, Krishnendu and Greimel, Karin and Henzinger, Thomas A and Jobstmann, Barbara},
editor = {Touili, Tayssir and Cook, Byron and Jackson, Paul},
location = {Edinburgh, UK},
pages = {410 -- 424},
publisher = {Springer},
title = {{Robustness in the presence of liveness}},
doi = {10.1007/978-3-642-14295-6_36},
volume = {6174},
year = {2010},
}
@article{3868,
abstract = {Simulation and bisimulation metrics for stochastic systems provide a quantitative generalization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative mu-calculus and related probabilistic logics. We first show that the metrics provide a bound for the difference in long-run average and discounted average behavior across states, indicating that the metrics can be used both in system verification, and in performance evaluation. For turn-based games and MDPs, we provide a polynomial-time algorithm for the computation of the one-step metric distance between states. The algorithm is based on linear programming; it improves on the previous known exponential-time algorithm based on a reduction to the theory of reals. We then present PSPACE algorithms for both the decision problem and the problem of approximating the metric distance between two states, matching the best known algorithms for Markov chains. For the bisimulation kernel of the metric our algorithm works in time O(n(4)) for both turn-based games and MDPs; improving the previously best known O(n(9).log(n)) time algorithm for MDPs. For a concurrent game G, we show that computing the exact distance be tween states is at least as hard as computing the value of concurrent reachability games and the square-root-sum problem in computational geometry. We show that checking whether the metric distance is bounded by a rational r, can be done via a reduction to the theory of real closed fields, involving a formula with three quantifier alternations, yielding O(vertical bar G vertical bar(O(vertical bar G vertical bar 5))) time complexity, improving the previously known reduction, which yielded O(vertical bar G vertical bar(O(vertical bar G vertical bar 7))) time complexity. These algorithms can be iterated to approximate the metrics using binary search},
author = {Chatterjee, Krishnendu and De Alfaro, Luca and Majumdar, Ritankar and Raman, Vishwanath},
journal = {Logical Methods in Computer Science},
number = {3},
pages = {1 -- 27},
publisher = {International Federation of Computational Logic},
title = {{Algorithms for game metrics}},
doi = {10.2168/LMCS-6(3:13)2010},
volume = {6},
year = {2010},
}
@article{3863,
abstract = {We consider two-player parity games with imperfect information in which strategies rely on observations that provide imperfect information about the history of a play. To solve such games, i.e., to determine the winning regions of players and corresponding winning strategies, one can use the subset construction to build an equivalent perfect-information game. Recently, an algorithm that avoids the inefficient subset construction has been proposed. The algorithm performs a fixed-point computation in a lattice of antichains, thus maintaining a succinct representation of state sets. However, this representation does not allow to recover winning strategies. In this paper, we build on the antichain approach to develop an algorithm for constructing the winning strategies in parity games of imperfect information. One major obstacle in adapting the classical procedure is that the complementation of attractor sets would break the invariant of downward-closedness on which the antichain representation relies. We overcome this difficulty by decomposing problem instances recursively into games with a combination of reachability, safety, and simpler parity conditions. We also report on an experimental implementation of our algorithm: to our knowledge, this is the first implementation of a procedure for solving imperfect-information parity games on graphs.},
author = {Berwanger, Dietmar and Chatterjee, Krishnendu and De Wulf, Martin and Doyen, Laurent and Henzinger, Thomas A},
journal = {Information and Computation},
number = {10},
pages = {1206 -- 1220},
publisher = {Elsevier},
title = {{Strategy construction for parity games with imperfect information}},
doi = {10.1016/j.ic.2009.09.006},
volume = {208},
year = {2010},
}
@article{3861,
abstract = {We introduce strategy logic, a logic that treats strategies in two-player games as explicit first-order objects. The explicit treatment of strategies allows us to specify properties of nonzero-sum games in a simple and natural way. We show that the one-alternation fragment of strategy logic is strong enough to express the existence of Nash equilibria and secure equilibria, and subsumes other logics that were introduced to reason about games, such as ATL, ATL*, and game logic. We show that strategy logic is decidable, by constructing tree automata that recognize sets of strategies. While for the general logic, our decision procedure is nonelementary, for the simple fragment that is used above we show that the complexity is polynomial in the size of the game graph and optimal in the size of the formula (ranging from polynomial to 2EXPTIME depending on the form of the formula).},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Piterman, Nir},
journal = {Information and Computation},
number = {6},
pages = {677 -- 693},
publisher = {Elsevier},
title = {{Strategy logic}},
doi = {10.1016/j.ic.2009.07.004},
volume = {208},
year = {2010},
}
@inproceedings{489,
abstract = {Graph games of infinite length are a natural model for open reactive processes: one player represents the controller, trying to ensure a given specification, and the other represents a hostile environment. The evolution of the system depends on the decisions of both players, supplemented by chance. In this work, we focus on the notion of randomised strategy. More specifically, we show that three natural definitions may lead to very different results: in the most general cases, an almost-surely winning situation may become almost-surely losing if the player is only allowed to use a weaker notion of strategy. In more reasonable settings, translations exist, but they require infinite memory, even in simple cases. Finally, some traditional problems becomes undecidable for the strongest type of strategies.},
author = {Cristau, Julien and David, Claire and Horn, Florian},
booktitle = {Proceedings of GandALF 2010},
location = {Minori, Amalfi Coast, Italy},
pages = {30 -- 39},
publisher = {Open Publishing Association},
title = {{How do we remember the past in randomised strategies? }},
doi = {10.4204/EPTCS.25.7},
volume = {25},
year = {2010},
}
@misc{5390,
abstract = {The class of ω regular languages provide a robust specification language in verification. Every ω-regular condition can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens “eventually.” Two main strengths of the classical, infinite-limit formulation of liveness are robustness (independence from the granularity of transitions) and simplicity (abstraction of complicated time bounds). However, the classical liveness formulation suffers from the drawback that the time until something good happens may be unbounded. A stronger formulation of liveness, so-called finitary liveness, overcomes this drawback, while still retaining robustness and simplicity. Finitary liveness requires that there exists an unknown, fixed bound b such that something good happens within b transitions. In this work we consider the finitary parity and Streett (fairness) conditions. We present the topological, automata-theoretic and logical characterization of finitary languages defined by finitary parity and Streett conditions. We (a) show that the finitary parity and Streett languages are Σ2-complete; (b) present a complete characterization of the expressive power of various classes of automata with finitary and infinitary conditions (in particular we show that non-deterministic finitary parity and Streett automata cannot be determinized to deterministic finitary parity or Streett automata); and (c) show that the languages defined by non-deterministic finitary parity automata exactly characterize the star-free fragment of ωB-regular languages.},
author = {Chatterjee, Krishnendu and Fijalkow, Nathanaël},
issn = {2664-1690},
pages = {21},
publisher = {IST Austria},
title = {{Topological, automata-theoretic and logical characterization of finitary languages}},
doi = {10.15479/AT:IST-2010-0002},
year = {2010},
}
@misc{5388,
abstract = {We present an algorithmic method for the synthesis of concurrent programs that are optimal with respect to quantitative performance measures. The input consists of a sequential sketch, that is, a program that does not contain synchronization constructs, and of a parametric performance model that assigns costs to actions such as locking, context switching, and idling. The quantitative synthesis problem is to automatically introduce synchronization constructs into the sequential sketch so that both correctness is guaranteed and worst-case (or average-case) performance is optimized. Correctness is formalized as race freedom or linearizability.
We show that for worst-case performance, the problem can be modeled
as a 2-player graph game with quantitative (limit-average) objectives, and
for average-case performance, as a 2 1/2 -player graph game (with probabilistic transitions). In both cases, the optimal correct program is derived from an optimal strategy in the corresponding quantitative game. We prove that the respective game problems are computationally expensive (NP-complete), and present several techniques that overcome the theoretical difficulty in cases of concurrent programs of practical interest.
We have implemented a prototype tool and used it for the automatic syn- thesis of programs that access a concurrent list. For certain parameter val- ues, our method automatically synthesizes various classical synchronization schemes for implementing a concurrent list, such as fine-grained locking or a lazy algorithm. For other parameter values, a new, hybrid synchronization style is synthesized, which uses both the lazy approach and coarse-grained locks (instead of standard fine-grained locks). The trade-off occurs because while fine-grained locking tends to decrease the cost that is due to waiting for locks, it increases cache size requirements.},
author = {Chatterjee, Krishnendu and Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun and Singh, Rohit},
issn = {2664-1690},
pages = {17},
publisher = {IST Austria},
title = {{Quantitative synthesis for concurrent programs}},
doi = {10.15479/AT:IST-2010-0004},
year = {2010},
}
@inproceedings{3855,
abstract = {We study observation-based strategies for partially-observable Markov decision processes (POMDPs) with parity objectives. An observation-based strategy relies on partial information about the history of a play, namely, on the past sequence of observations. We consider qualitative analysis problems: given a POMDP with a parity objective, decide whether there exists an observation-based strategy to achieve the objective with probability 1 (almost-sure winning), or with positive probability (positive winning). Our main results are twofold. First, we present a complete picture of the computational complexity of the qualitative analysis problem for POMDPs with parity objectives and its subclasses: safety, reachability, Büchi, and coBüchi objectives. We establish several upper and lower bounds that were not known in the literature. Second, we give optimal bounds (matching upper and lower bounds) for the memory required by pure and randomized observation-based strategies for each class of objectives.},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A},
location = {Brno, Czech Republic},
pages = {258 -- 269},
publisher = {Springer},
title = {{Qualitative analysis of partially-observable Markov Decision Processes}},
doi = {10.1007/978-3-642-15155-2_24},
volume = {6281},
year = {2010},
}
@inproceedings{4388,
abstract = {GIST is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Jobstmann, Barbara and Radhakrishna, Arjun},
location = {Edinburgh, UK},
pages = {665 -- 669},
publisher = {Springer},
title = {{GIST: A solver for probabilistic games}},
doi = {10.1007/978-3-642-14295-6_57},
volume = {6174},
year = {2010},
}