---
_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.'
article_processing_charge: No
article_type: original
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  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: 2026-08-21T10:28:39Z
day: '07'
doi: 10.1016/j.tcs.2006.07.032
extern: '1'
fulldoi: https://doi.org/10.1016/j.tcs.2006.07.032
intvolume: '       365'
issue: 1-2
language:
- iso: eng
month: '08'
oa_version: None
page: 67 - 82
publication: Theoretical Computer Science
publication_identifier:
  eissn:
  - 1879-2294
  issn:
  - 0304-3975
publication_status: published
publisher: Elsevier
publist_id: '164'
status: public
title: Games with secure equilibria
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 365
year: '2006'
...
---
OA_type: closed access
_id: '4451'
abstract:
- lang: eng
  text: One source of complexity in the μ-calculus is its ability to specify an unbounded
    number of switches between universal (AX) and existential (EX) branching modes.
    We therefore study the problems of satisfiability, validity, model checking, and
    implication for the universal and existential fragments of the μ-calculus, in
    which only one branching mode is allowed. The universal fragment is rich enough
    to express most specifications of interest, and therefore improved algorithms
    are of practical importance. We show that while the satisfiability and validity
    problems become indeed simpler for the existential and universal fragments, this
    is, unfortunately, not the case for model checking and implication. We also show
    the corresponding results for the alternation-free fragment of the μ-calculus,
    where no alternations between least and greatest fixed points are allowed. Our
    results imply that efforts to find a polynomial-time model-checking algorithm
    for the μ-calculus can be replaced by efforts to find such an algorithm for the
    universal or existential fragment.
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  ama: Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments
    of the mu-calculus. <i>Theoretical Computer Science</i>. 2006;354(2):173-186.
    doi:<a href="https://doi.org/10.1016/j.tcs.2005.11.015">10.1016/j.tcs.2005.11.015</a>
  apa: Henzinger, T. A., Kupferman, O., &#38; Majumdar, R. (2006). On the universal
    and existential fragments of the mu-calculus. <i>Theoretical Computer Science</i>.
    Elsevier. <a href="https://doi.org/10.1016/j.tcs.2005.11.015">https://doi.org/10.1016/j.tcs.2005.11.015</a>
  chicago: Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal
    and Existential Fragments of the Mu-Calculus.” <i>Theoretical Computer Science</i>.
    Elsevier, 2006. <a href="https://doi.org/10.1016/j.tcs.2005.11.015">https://doi.org/10.1016/j.tcs.2005.11.015</a>.
  ieee: T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential
    fragments of the mu-calculus,” <i>Theoretical Computer Science</i>, vol. 354,
    no. 2. Elsevier, pp. 173–186, 2006.
  ista: Henzinger TA, Kupferman O, Majumdar R. 2006. On the universal and existential
    fragments of the mu-calculus. Theoretical Computer Science. 354(2), 173–186.
  mla: Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of
    the Mu-Calculus.” <i>Theoretical Computer Science</i>, vol. 354, no. 2, Elsevier,
    2006, pp. 173–86, doi:<a href="https://doi.org/10.1016/j.tcs.2005.11.015">10.1016/j.tcs.2005.11.015</a>.
  short: T.A. Henzinger, O. Kupferman, R. Majumdar, Theoretical Computer Science 354
    (2006) 173–186.
date_created: 2018-12-11T12:08:55Z
date_published: 2006-03-28T00:00:00Z
date_updated: 2026-08-21T10:58:07Z
day: '28'
doi: 10.1016/j.tcs.2005.11.015
extern: '1'
fulldoi: https://doi.org/10.1016/j.tcs.2005.11.015
intvolume: '       354'
issue: '2'
language:
- iso: eng
month: '03'
oa_version: None
page: 173 - 186
publication: Theoretical Computer Science
publication_identifier:
  eissn:
  - 1879-2294
  issn:
  - 0304-3975
publication_status: published
publisher: Elsevier
publist_id: '276'
status: public
title: On the universal and existential fragments of the mu-calculus
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 354
year: '2006'
...
---
OA_type: closed access
_id: '4625'
abstract:
- lang: eng
  text: "Temporal logic is two-valued: formulas are interpreted as either true or
    false. When applied to the analysis of stochastic systems, or systems with imprecise
    formal models, temporal logic is therefore fragile: even small changes in the
    model can lead to opposite truth values for a specification. We present a generalization
    of the branching-time logic CTL which achieves robustness with respect to model
    perturbations by giving a quantitative interpretation to predicates and logical
    operators, and by discounting the importance of events according to how late they
    occur. In every state, the value of a formula is a real number in the interval
    [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators
    and and or are replaced by min and max, the path quantifiers ∃ and ∀ determine
    sup and inf over all paths from a given state, and the temporal operators ⋄ and
    □ specify sup and inf over a given path; a new operator averages all values along
    a path. Furthermore, all path operators are discounted by a parameter that can
    be chosen to give more weight to states that are closer to the beginning of the
    path.\r\n\r\nWe interpret the resulting logic DCTL over transition systems, Markov
    chains, and Markov decision processes. We present two semantics for DCTL: a path
    semantics, inspired by the standard interpretation of state and path formulas
    in CTL, and a fixpoint semantics, inspired by the μ-calculus evaluation of CTL
    formulas. We show that, while these semantics coincide for CTL, they differ for
    DCTL, and we provide model-checking algorithms for both semantics."
article_processing_charge: No
article_type: original
author:
- 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: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Mariëlle
  full_name: Stoelinga, Mariëlle
  last_name: Stoelinga
citation:
  ama: De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. Model checking
    discounted temporal properties. <i>Theoretical Computer Science</i>. 2005;345(1):139-170.
    doi:<a href="https://doi.org/10.1016/j.tcs.2005.07.033">10.1016/j.tcs.2005.07.033</a>
  apa: De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., &#38; Stoelinga,
    M. (2005). Model checking discounted temporal properties. <i>Theoretical Computer
    Science</i>. Elsevier. <a href="https://doi.org/10.1016/j.tcs.2005.07.033">https://doi.org/10.1016/j.tcs.2005.07.033</a>
  chicago: De Alfaro, Luca, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and
    Mariëlle Stoelinga. “Model Checking Discounted Temporal Properties.” <i>Theoretical
    Computer Science</i>. Elsevier, 2005. <a href="https://doi.org/10.1016/j.tcs.2005.07.033">https://doi.org/10.1016/j.tcs.2005.07.033</a>.
  ieee: L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, “Model
    checking discounted temporal properties,” <i>Theoretical Computer Science</i>,
    vol. 345, no. 1. Elsevier, pp. 139–170, 2005.
  ista: De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2005. Model
    checking discounted temporal properties. Theoretical Computer Science. 345(1),
    139–170.
  mla: De Alfaro, Luca, et al. “Model Checking Discounted Temporal Properties.” <i>Theoretical
    Computer Science</i>, vol. 345, no. 1, Elsevier, 2005, pp. 139–70, doi:<a href="https://doi.org/10.1016/j.tcs.2005.07.033">10.1016/j.tcs.2005.07.033</a>.
  short: L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, Theoretical
    Computer Science 345 (2005) 139–170.
date_created: 2018-12-11T12:09:49Z
date_published: 2005-11-21T00:00:00Z
date_updated: 2026-09-30T14:03:08Z
day: '21'
doi: 10.1016/j.tcs.2005.07.033
extern: '1'
fulldoi: https://doi.org/10.1016/j.tcs.2005.07.033
intvolume: '       345'
issue: '1'
language:
- iso: eng
month: '11'
oa_version: None
page: 139 - 170
publication: Theoretical Computer Science
publication_identifier:
  eissn:
  - 1879-2294
  issn:
  - 0304-3975
publication_status: published
publisher: Elsevier
publist_id: '80'
status: public
title: Model checking discounted temporal properties
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 345
year: '2005'
...
---
_id: '4052'
abstract:
- lang: eng
  text: This paper describes an effective procedure for stratifying a real semi-algebraic
    set into cells of constant description size. The attractive feature of our method
    is that the number of cells produced is singly exponential in the number of input
    variables. This compares favorably with the doubly exponential size of Collins'
    decomposition. Unlike Collins' construction, however, our scheme does not produce
    a cell complex but only a smooth stratification. Nevertheless, we are able to
    apply our results in interesting ways to problems of point location and geometric
    optimization.
acknowledgement: The authors wish to thank DEC/Systems Research Center and DEC/Paris
  Research Laboratory, where part of this research was conducted. For individual support,
  Bernard Chazelle acknowledges the National Science Foundation for supporting this
  research in part under Grant CCR-8700917. Herbert Edelsbrunner acknowledges the
  support of the National Science Foundation under Grant CCR-8714565. Micha Sharir
  acknowledges the Office of Naval Research under Grant N00014-87-K-0129, the National
  Science Foundation under Grant No. NSF-DCR-83-20085, grants from the Digital Equipment
  Corporation and the IBM Corporation, and a research grant from the US-Israeli Binational
  Science Foundation.
article_processing_charge: No
article_type: original
author:
- first_name: Bernard
  full_name: Chazelle, Bernard
  last_name: Chazelle
- first_name: Herbert
  full_name: Edelsbrunner, Herbert
  id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
  last_name: Edelsbrunner
  orcid: 0000-0002-9823-6833
- first_name: Leonidas
  full_name: Guibas, Leonidas
  last_name: Guibas
- first_name: Micha
  full_name: Sharir, Micha
  last_name: Sharir
citation:
  ama: Chazelle B, Edelsbrunner H, Guibas L, Sharir M. A singly exponential stratification
    scheme for real semi-algebraic varieties and its applications. <i>Theoretical
    Computer Science</i>. 1991;84(1):77-105. doi:<a href="https://doi.org/10.1016/0304-3975(91)90261-Y">10.1016/0304-3975(91)90261-Y</a>
  apa: Chazelle, B., Edelsbrunner, H., Guibas, L., &#38; Sharir, M. (1991). A singly
    exponential stratification scheme for real semi-algebraic varieties and its applications.
    <i>Theoretical Computer Science</i>. Elsevier. <a href="https://doi.org/10.1016/0304-3975(91)90261-Y">https://doi.org/10.1016/0304-3975(91)90261-Y</a>
  chicago: Chazelle, Bernard, Herbert Edelsbrunner, Leonidas Guibas, and Micha Sharir.
    “A Singly Exponential Stratification Scheme for Real Semi-Algebraic Varieties
    and Its Applications.” <i>Theoretical Computer Science</i>. Elsevier, 1991. <a
    href="https://doi.org/10.1016/0304-3975(91)90261-Y">https://doi.org/10.1016/0304-3975(91)90261-Y</a>.
  ieee: B. Chazelle, H. Edelsbrunner, L. Guibas, and M. Sharir, “A singly exponential
    stratification scheme for real semi-algebraic varieties and its applications,”
    <i>Theoretical Computer Science</i>, vol. 84, no. 1. Elsevier, pp. 77–105, 1991.
  ista: Chazelle B, Edelsbrunner H, Guibas L, Sharir M. 1991. A singly exponential
    stratification scheme for real semi-algebraic varieties and its applications.
    Theoretical Computer Science. 84(1), 77–105.
  mla: Chazelle, Bernard, et al. “A Singly Exponential Stratification Scheme for Real
    Semi-Algebraic Varieties and Its Applications.” <i>Theoretical Computer Science</i>,
    vol. 84, no. 1, Elsevier, 1991, pp. 77–105, doi:<a href="https://doi.org/10.1016/0304-3975(91)90261-Y">10.1016/0304-3975(91)90261-Y</a>.
  short: B. Chazelle, H. Edelsbrunner, L. Guibas, M. Sharir, Theoretical Computer
    Science 84 (1991) 77–105.
date_created: 2018-12-11T12:06:39Z
date_published: 1991-07-22T00:00:00Z
date_updated: 2022-03-02T10:23:58Z
day: '22'
doi: 10.1016/0304-3975(91)90261-Y
extern: '1'
fulldoi: https://doi.org/10.1016/0304-3975(91)90261-Y
intvolume: '        84'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.sciencedirect.com/science/article/pii/030439759190261Y?via%3Dihub
month: '07'
oa: 1
oa_version: Published Version
page: 77 - 105
publication: Theoretical Computer Science
publication_identifier:
  eissn:
  - 1879-2294
  issn:
  - 0304-3975
publication_status: published
publisher: Elsevier
publist_id: '2073'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A singly exponential stratification scheme for real semi-algebraic varieties
  and its applications
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 84
year: '1991'
...
---
_id: '4084'
abstract:
- lang: eng
  text: "A tour  of a finite set P of points is a necklace-tour if there are disks
    with the points in P as centers such that two disks intersect if and only if their
    centers are adjacent in . It has been observed by Sanders that a necklace-tour
    is an optimal traveling salesman tour.\r\n\r\nIn this paper, we present an algorithm
    that either reports that no necklace-tour exists or outputs a necklace-tour of
    a given set of n points in O(n2 log n) time. If a tour is given, then we can test
    in O(n2) time whether or not this tour is a necklace-tour. Both algorithms can
    be generalized to ƒ-factors of point sets in the plane. The complexity results
    rely on a combinatorial analysis of certain intersection graphs of disks defined
    for finite sets of points in the plane."
article_processing_charge: No
article_type: original
author:
- first_name: Herbert
  full_name: Edelsbrunner, Herbert
  id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
  last_name: Edelsbrunner
  orcid: 0000-0002-9823-6833
- first_name: Günter
  full_name: Rote, Günter
  last_name: Rote
- first_name: Emo
  full_name: Welzl, Emo
  last_name: Welzl
citation:
  ama: Edelsbrunner H, Rote G, Welzl E. Testing the necklace condition for shortest
    tours and optimal factors in the plane. <i>Theoretical Computer Science</i>. 1989;66(2):157-180.
    doi:<a href="https://doi.org/10.1016/0304-3975(89)90133-3">10.1016/0304-3975(89)90133-3</a>
  apa: Edelsbrunner, H., Rote, G., &#38; Welzl, E. (1989). Testing the necklace condition
    for shortest tours and optimal factors in the plane. <i>Theoretical Computer Science</i>.
    Elsevier. <a href="https://doi.org/10.1016/0304-3975(89)90133-3">https://doi.org/10.1016/0304-3975(89)90133-3</a>
  chicago: Edelsbrunner, Herbert, Günter Rote, and Emo Welzl. “Testing the Necklace
    Condition for Shortest Tours and Optimal Factors in the Plane.” <i>Theoretical
    Computer Science</i>. Elsevier, 1989. <a href="https://doi.org/10.1016/0304-3975(89)90133-3">https://doi.org/10.1016/0304-3975(89)90133-3</a>.
  ieee: H. Edelsbrunner, G. Rote, and E. Welzl, “Testing the necklace condition for
    shortest tours and optimal factors in the plane,” <i>Theoretical Computer Science</i>,
    vol. 66, no. 2. Elsevier, pp. 157–180, 1989.
  ista: Edelsbrunner H, Rote G, Welzl E. 1989. Testing the necklace condition for
    shortest tours and optimal factors in the plane. Theoretical Computer Science.
    66(2), 157–180.
  mla: Edelsbrunner, Herbert, et al. “Testing the Necklace Condition for Shortest
    Tours and Optimal Factors in the Plane.” <i>Theoretical Computer Science</i>,
    vol. 66, no. 2, Elsevier, 1989, pp. 157–80, doi:<a href="https://doi.org/10.1016/0304-3975(89)90133-3">10.1016/0304-3975(89)90133-3</a>.
  short: H. Edelsbrunner, G. Rote, E. Welzl, Theoretical Computer Science 66 (1989)
    157–180.
date_created: 2018-12-11T12:06:51Z
date_published: 1989-08-01T00:00:00Z
date_updated: 2022-02-11T11:15:43Z
day: '01'
doi: 10.1016/0304-3975(89)90133-3
extern: '1'
fulldoi: https://doi.org/10.1016/0304-3975(89)90133-3
intvolume: '        66'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.sciencedirect.com/science/article/pii/0304397589901333?via%3Dihub
month: '08'
oa: 1
oa_version: Published Version
page: 157 - 180
publication: Theoretical Computer Science
publication_identifier:
  eissn:
  - 1879-2294
  issn:
  - 0304-3975
publication_status: published
publisher: Elsevier
publist_id: '2041'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Testing the necklace condition for shortest tours and optimal factors in the
  plane
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 66
year: '1989'
...