[{"acknowledgement":"Supported in part by the NSF grants CCR-0234690, CCR-0208875, and CCR-0225610; by the NSF grant CCR-0132780 and ARP grant SC20051123.","status":"public","extern":1,"year":"2006","citation":{"apa":"Chatterjee, K., De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., &#38; Stoelinga, M. (2006). Compositional quantitative reasoning (pp. 179–188). Presented at the QEST: Quantitative Evaluation of Systems, IEEE. <a href=\"https://doi.org/10.1109/QEST.2006.11\">https://doi.org/10.1109/QEST.2006.11</a>","ama":"Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. Compositional quantitative reasoning. In: IEEE; 2006:179-188. doi:<a href=\"https://doi.org/10.1109/QEST.2006.11\">10.1109/QEST.2006.11</a>","ieee":"K. Chatterjee, L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, “Compositional quantitative reasoning,” presented at the QEST: Quantitative Evaluation of Systems, 2006, pp. 179–188.","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and Mariëlle Stoelinga. “Compositional Quantitative Reasoning,” 179–88. IEEE, 2006. <a href=\"https://doi.org/10.1109/QEST.2006.11\">https://doi.org/10.1109/QEST.2006.11</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Compositional Quantitative Reasoning</i>. IEEE, 2006, pp. 179–88, doi:<a href=\"https://doi.org/10.1109/QEST.2006.11\">10.1109/QEST.2006.11</a>.","short":"K. Chatterjee, L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, in:, IEEE, 2006, pp. 179–188.","ista":"Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2006. Compositional quantitative reasoning. QEST: Quantitative Evaluation of Systems, 179–188."},"date_updated":"2021-01-12T07:59:37Z","type":"conference","date_published":"2006-09-01T00:00:00Z","day":"01","doi":"10.1109/QEST.2006.11","publist_id":"163","abstract":[{"text":"We present a compositional theory of system verification, where specifications assign real-numbered costs to systems. These costs can express a wide variety of quantitative system properties, such as resource consumption, price, or a measure of how well a system satisfies its specification. The theory supports the composition of systems and specifications, and the hiding of variables. Boolean refinement relations are replaced by real-numbered distances between descriptions of a system at different levels of detail. We show that the classical Boolean rules for compositional reasoning have quantitative counterparts in our setting. While our general theory allows costs to be specified by arbitrary cost functions, we also consider a class of linear cost functions, which give rise to an instance of our framework where all operations are computable in polynomial time.","lang":"eng"}],"quality_controlled":0,"page":"179 - 188","publisher":"IEEE","conference":{"name":"QEST: Quantitative Evaluation of Systems"},"_id":"4549","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Krishnendu Chatterjee"},{"full_name":"de Alfaro, Luca","last_name":"De Alfaro","first_name":"Luca"},{"first_name":"Marco","last_name":"Faella","full_name":"Faella, Marco"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar S"},{"last_name":"Stoelinga","first_name":"Mariëlle","full_name":"Stoelinga, Mariëlle"}],"date_created":"2018-12-11T12:09:26Z","publication_status":"published","title":"Compositional quantitative reasoning","month":"09"},{"volume":365,"extern":1,"status":"public","date_updated":"2021-01-12T07:59:38Z","year":"2006","citation":{"ista":"Chatterjee K, Henzinger TA, Jurdziński M. 2006. Games with secure equilibria. Theoretical Computer Science. 365(1–2), 67–82.","short":"K. Chatterjee, T.A. Henzinger, M. Jurdziński, Theoretical Computer Science 365 (2006) 67–82.","mla":"Chatterjee, Krishnendu, et al. “Games with Secure Equilibria.” <i>Theoretical Computer Science</i>, vol. 365, no. 1–2, Elsevier, 2006, pp. 67–82, doi:<a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">10.1016/j.tcs.2006.07.032</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and M. Jurdziński, “Games with secure equilibria,” <i>Theoretical Computer Science</i>, vol. 365, no. 1–2. Elsevier, pp. 67–82, 2006.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Marcin Jurdziński. “Games with Secure Equilibria.” <i>Theoretical Computer Science</i>. Elsevier, 2006. <a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">https://doi.org/10.1016/j.tcs.2006.07.032</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Jurdziński, M. (2006). Games with secure equilibria. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">https://doi.org/10.1016/j.tcs.2006.07.032</a>","ama":"Chatterjee K, Henzinger TA, Jurdziński M. Games with secure equilibria. <i>Theoretical Computer Science</i>. 2006;365(1-2):67-82. doi:<a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">10.1016/j.tcs.2006.07.032</a>"},"date_published":"2006-08-07T00:00:00Z","type":"journal_article","doi":"10.1016/j.tcs.2006.07.032","day":"07","abstract":[{"lang":"eng","text":"In 2-player non-zero-sum games, Nash equilibria capture the options for rational behavior if each player attempts to maximize her payoff. In contrast to classical game theory, we consider lexicographic objectives: first, each player tries to maximize her own payoff, and then, the player tries to minimize the opponent's payoff. Such objectives arise naturally in the verification of systems with multiple components. There, instead of proving that each component satisfies its specification no matter how the other components behave, it sometimes suffices to prove that each component satisfies its specification provided that the other components satisfy their specifications. We say that a Nash equilibrium is secure if it is an equilibrium with respect to the lexicographic objectives of both players. We prove that in graph games with Borel winning conditions, which include the games that arise in verification, there may be several Nash equilibria, but there is always a unique maximal payoff profile of a secure equilibrium. We show how this equilibrium can be computed in the case of ω-regular winning conditions, and we characterize the memory requirements of strategies that achieve the equilibrium."}],"publist_id":"164","page":"67 - 82","quality_controlled":0,"publisher":"Elsevier","publication":"Theoretical Computer Science","_id":"4550","author":[{"full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jurdziński, Marcin","last_name":"Jurdziński","first_name":"Marcin"}],"issue":"1-2","publication_status":"published","date_created":"2018-12-11T12:09:26Z","title":"Games with secure equilibria","month":"08","intvolume":"       365"},{"extern":1,"status":"public","acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202.","volume":3884,"date_published":"2006-02-14T00:00:00Z","type":"conference","date_updated":"2021-01-12T07:59:38Z","citation":{"ieee":"K. Chatterjee, R. Majumdar, and T. A. Henzinger, “Markov decision processes with multiple objectives,” presented at the STACS: Theoretical Aspects of Computer Science, 2006, vol. 3884, pp. 325–336.","chicago":"Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Markov Decision Processes with Multiple Objectives,” 3884:325–36. Springer, 2006. <a href=\"https://doi.org/10.1007/11672142_26\">https://doi.org/10.1007/11672142_26</a>.","apa":"Chatterjee, K., Majumdar, R., &#38; Henzinger, T. A. (2006). Markov decision processes with multiple objectives (Vol. 3884, pp. 325–336). Presented at the STACS: Theoretical Aspects of Computer Science, Springer. <a href=\"https://doi.org/10.1007/11672142_26\">https://doi.org/10.1007/11672142_26</a>","ama":"Chatterjee K, Majumdar R, Henzinger TA. Markov decision processes with multiple objectives. In: Vol 3884. Springer; 2006:325-336. doi:<a href=\"https://doi.org/10.1007/11672142_26\">10.1007/11672142_26</a>","ista":"Chatterjee K, Majumdar R, Henzinger TA. 2006. Markov decision processes with multiple objectives. STACS: Theoretical Aspects of Computer Science, LNCS, vol. 3884, 325–336.","short":"K. Chatterjee, R. Majumdar, T.A. Henzinger, in:, Springer, 2006, pp. 325–336.","mla":"Chatterjee, Krishnendu, et al. <i>Markov Decision Processes with Multiple Objectives</i>. Vol. 3884, Springer, 2006, pp. 325–36, doi:<a href=\"https://doi.org/10.1007/11672142_26\">10.1007/11672142_26</a>."},"year":"2006","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple discounted reward objectives. Such MDPs occur in design problems where one wishes to simultaneously optimize several criteria, for example, latency and power. The possible trade-offs between the different objectives are characterized by the Pareto curve. We show that every Pareto-optimal point can be achieved by a memoryless strategy; however, unlike in the single-objective case, the memoryless strategy may require randomization. Moreover, we show that the Pareto curve can be approximated in polynomial time in the size of the MDP. Additionally, we study the problem if a given value vector is realizable by any strategy, and show that it can be decided in polynomial time; but the question whether it is realizable by a deterministic memoryless strategy is NP-complete. These results provide efficient algorithms for design exploration in MDP models with multiple objectives.\nThis research was supported in part by the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202. "}],"publist_id":"161","doi":"10.1007/11672142_26","day":"14","page":"325 - 336","quality_controlled":0,"conference":{"name":"STACS: Theoretical Aspects of Computer Science"},"publisher":"Springer","author":[{"full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar S"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"4551","title":"Markov decision processes with multiple objectives","month":"02","alternative_title":["LNCS"],"intvolume":"      3884","publication_status":"published","date_created":"2018-12-11T12:09:26Z"},{"extern":1,"status":"public","date_updated":"2021-01-12T07:59:39Z","citation":{"ama":"Chatterjee K, De Alfaro L, Henzinger TA. Strategy improvement for concurrent reachability games. In: IEEE; 2006:291-300. doi:<a href=\"https://doi.org/10.1109/QEST.2006.48\">10.1109/QEST.2006.48</a>","apa":"Chatterjee, K., De Alfaro, L., &#38; Henzinger, T. A. (2006). Strategy improvement for concurrent reachability games (pp. 291–300). Presented at the QEST: Quantitative Evaluation of Systems, IEEE. <a href=\"https://doi.org/10.1109/QEST.2006.48\">https://doi.org/10.1109/QEST.2006.48</a>","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Strategy Improvement for Concurrent Reachability Games,” 291–300. IEEE, 2006. <a href=\"https://doi.org/10.1109/QEST.2006.48\">https://doi.org/10.1109/QEST.2006.48</a>.","ieee":"K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Strategy improvement for concurrent reachability games,” presented at the QEST: Quantitative Evaluation of Systems, 2006, pp. 291–300.","short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2006, pp. 291–300.","mla":"Chatterjee, Krishnendu, et al. <i>Strategy Improvement for Concurrent Reachability Games</i>. IEEE, 2006, pp. 291–300, doi:<a href=\"https://doi.org/10.1109/QEST.2006.48\">10.1109/QEST.2006.48</a>.","ista":"Chatterjee K, De Alfaro L, Henzinger TA. 2006. Strategy improvement for concurrent reachability games. QEST: Quantitative Evaluation of Systems, 291–300."},"year":"2006","date_published":"2006-01-01T00:00:00Z","type":"conference","doi":"10.1109/QEST.2006.48","day":"01","abstract":[{"text":"A concurrent reachability game is a two-player game played on a graph: at each state, the players simultaneously and independently select moves; the two moves determine jointly a probability distribution over the successor states. The objective for player 1 consists in reaching a set of target states; the objective for player 2 is to prevent this, so that the game is zero-sum. Our contributions are two-fold. First, we present a simple proof of the fact that in concurrent reachability games, for all epsilon &gt; 0, memoryless epsilon-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an epsilon-optimal strategy achieves the objective with probability within epsilon of the value of the game. In contrast to previous proofs of this fact, which rely on the limit behavior of discounted games using advanced Puisieux series analysis, our proof is elementary and combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives.","lang":"eng"}],"publist_id":"162","page":"291 - 300","quality_controlled":0,"publisher":"IEEE","conference":{"name":"QEST: Quantitative Evaluation of Systems"},"_id":"4552","author":[{"orcid":"0000-0002-4561-241X","full_name":"Krishnendu Chatterjee","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"de Alfaro, Luca","first_name":"Luca","last_name":"De Alfaro"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger"}],"publication_status":"published","date_created":"2018-12-11T12:09:26Z","month":"01","title":"Strategy improvement for concurrent reachability games"}]