@article{2836, abstract = {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. }, author = {Chatterjee, Krishnendu and Raman, Vishwanath}, journal = {Formal Aspects of Computing}, number = {4}, pages = {825 -- 859}, publisher = {Springer}, title = {{Assume-guarantee synthesis for digital contract signing}}, doi = {10.1007/s00165-013-0283-6}, volume = {26}, year = {2013}, } @article{2854, abstract = {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.}, author = {Chatterjee, Krishnendu and De Alfaro, Luca and Henzinger, Thomas A}, journal = {Journal of Computer and System Sciences}, number = {5}, pages = {640 -- 657}, publisher = {Elsevier}, title = {{Strategy improvement for concurrent reachability and turn based stochastic safety games}}, doi = {10.1016/j.jcss.2012.12.001}, volume = {79}, year = {2013}, } @inproceedings{2886, abstract = {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.}, author = {Chmelik, Martin and Řehák, Vojtěch}, location = {Znojmo, Czech Republic}, pages = {118 -- 130}, publisher = {Springer}, title = {{Controllable-choice message sequence graphs}}, doi = {10.1007/978-3-642-36046-6_12}, volume = {7721}, year = {2013}, } @article{3116, abstract = {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.}, author = {Chatterjee, Krishnendu and De Alfaro, Luca and Faella, Marco and Majumdar, Ritankar and Raman, Vishwanath}, journal = {Formal Methods in System Design}, number = {2}, pages = {142 -- 174}, publisher = {Springer}, title = {{Code aware resource management}}, doi = {10.1007/s10703-012-0170-4}, volume = {42}, year = {2013}, } @article{2831, abstract = {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.}, author = {Chatterjee, Krishnendu and Henzinger, Monika H and Joglekar, Manas and Shah, Nisarg}, journal = {Formal Methods in System Design}, number = {3}, pages = {301 -- 327}, publisher = {Springer}, title = {{Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives}}, doi = {10.1007/s10703-012-0180-2}, volume = {42}, year = {2013}, }