@article{4550, abstract = {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 = {Chatterjee, Krishnendu and Henzinger, Thomas A and Jurdziński, Marcin}, issn = {1879-2294}, journal = {Theoretical Computer Science}, number = {1-2}, pages = {67 -- 82}, publisher = {Elsevier}, title = {{Games with secure equilibria}}, doi = {10.1016/j.tcs.2006.07.032}, volume = {365}, year = {2006}, } @article{4451, abstract = {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.}, author = {Henzinger, Thomas A and Kupferman, Orna and Majumdar, Ritankar}, issn = {1879-2294}, journal = {Theoretical Computer Science}, number = {2}, pages = {173 -- 186}, publisher = {Elsevier}, title = {{On the universal and existential fragments of the mu-calculus}}, doi = {10.1016/j.tcs.2005.11.015}, volume = {354}, year = {2006}, } @article{4625, abstract = {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. We 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.}, author = {De Alfaro, Luca and Faella, Marco and Henzinger, Thomas A and Majumdar, Ritankar and Stoelinga, Mariëlle}, issn = {1879-2294}, journal = {Theoretical Computer Science}, number = {1}, pages = {139 -- 170}, publisher = {Elsevier}, title = {{Model checking discounted temporal properties}}, doi = {10.1016/j.tcs.2005.07.033}, volume = {345}, year = {2005}, } @article{4052, abstract = {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.}, author = {Chazelle, Bernard and Edelsbrunner, Herbert and Guibas, Leonidas and Sharir, Micha}, issn = {1879-2294}, journal = {Theoretical Computer Science}, number = {1}, pages = {77 -- 105}, publisher = {Elsevier}, title = {{A singly exponential stratification scheme for real semi-algebraic varieties and its applications}}, doi = {10.1016/0304-3975(91)90261-Y}, volume = {84}, year = {1991}, } @article{4084, abstract = {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. In 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.}, author = {Edelsbrunner, Herbert and Rote, Günter and Welzl, Emo}, issn = {1879-2294}, journal = {Theoretical Computer Science}, number = {2}, pages = {157 -- 180}, publisher = {Elsevier}, title = {{Testing the necklace condition for shortest tours and optimal factors in the plane}}, doi = {10.1016/0304-3975(89)90133-3}, volume = {66}, year = {1989}, }