---
_id: '4549'
abstract:
- lang: eng
  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.
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.
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Luca
  full_name: de Alfaro, Luca
  last_name: De Alfaro
- first_name: Marco
  full_name: Faella, Marco
  last_name: Faella
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
- first_name: Mariëlle
  full_name: Stoelinga, Mariëlle
  last_name: Stoelinga
citation:
  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>'
  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>'
  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>.
  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.'
  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.'
  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.
conference:
  name: 'QEST: Quantitative Evaluation of Systems'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-09-01T00:00:00Z
date_updated: 2021-01-12T07:59:37Z
day: '01'
doi: 10.1109/QEST.2006.11
extern: 1
month: '09'
page: 179 - 188
publication_status: published
publisher: IEEE
publist_id: '163'
quality_controlled: 0
status: public
title: Compositional quantitative reasoning
type: conference
year: '2006'
...
---
_id: '4550'
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.'
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Marcin
  full_name: Jurdziński, Marcin
  last_name: Jurdziński
citation:
  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>
  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>
  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>.
  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.
  ista: Chatterjee K, Henzinger TA, Jurdziński M. 2006. Games with secure equilibria.
    Theoretical Computer Science. 365(1–2), 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>.
  short: K. Chatterjee, T.A. Henzinger, M. Jurdziński, Theoretical Computer Science
    365 (2006) 67–82.
date_created: 2018-12-11T12:09:26Z
date_published: 2006-08-07T00:00:00Z
date_updated: 2021-01-12T07:59:38Z
day: '07'
doi: 10.1016/j.tcs.2006.07.032
extern: 1
intvolume: '       365'
issue: 1-2
month: '08'
page: 67 - 82
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '164'
quality_controlled: 0
status: public
title: Games with secure equilibria
type: journal_article
volume: 365
year: '2006'
...
---
_id: '4551'
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. "
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.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  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>'
  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>'
  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>.
  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.'
  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.'
  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>.
  short: K. Chatterjee, R. Majumdar, T.A. Henzinger, in:, Springer, 2006, pp. 325–336.
conference:
  name: 'STACS: Theoretical Aspects of Computer Science'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-02-14T00:00:00Z
date_updated: 2021-01-12T07:59:38Z
day: '14'
doi: 10.1007/11672142_26
extern: 1
intvolume: '      3884'
month: '02'
page: 325 - 336
publication_status: published
publisher: Springer
publist_id: '161'
quality_controlled: 0
status: public
title: Markov decision processes with multiple objectives
type: conference
volume: 3884
year: '2006'
...
---
_id: '4552'
abstract:
- lang: eng
  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.'
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Luca
  full_name: de Alfaro, Luca
  last_name: De Alfaro
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
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.'
  ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2006. Strategy improvement for concurrent
    reachability games. QEST: Quantitative Evaluation of Systems, 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>.
  short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2006, pp. 291–300.
conference:
  name: 'QEST: Quantitative Evaluation of Systems'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:39Z
day: '01'
doi: 10.1109/QEST.2006.48
extern: 1
month: '01'
page: 291 - 300
publication_status: published
publisher: IEEE
publist_id: '162'
quality_controlled: 0
status: public
title: Strategy improvement for concurrent reachability games
type: conference
year: '2006'
...