@inproceedings{3888,
abstract = {A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with omega-regular winning conditions specified as Rabin or Streett objectives. These games are NP-complete and coNP-complete, respectively. The value of the game for a player at a state s given an objective Phi is the maximal probability with which the player can guarantee the satisfaction of Phi from s. We present a strategy-improvement algorithm to compute values in stochastic Rabin games, where an improvement step involves solving Markov decision processes (MDPs) and nonstochastic Rabin games. The algorithm also computes values for stochastic Streett games but does not directly yield an optimal strategy for Streett objectives. We then show how to obtain an optimal strategy for Streett objectives by solving certain nonstochastic Streett games.},
author = {Krishnendu Chatterjee and Thomas Henzinger},
pages = {375 -- 389},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Strategy improvement for stochastic Rabin and Streett games}},
doi = {10.1007/11817949_25},
volume = {4137},
year = {2006},
}
@inproceedings{3890,
abstract = {We consider two-player infinite games played on graphs. The games are concurrent, in that at each state the players choose their moves simultaneously and independently, and stochastic, in that the moves determine a probability distribution for the successor state. The value of a game is the maximal probability with which a player can guarantee the satisfaction of her objective. We show that the values of concurrent games with w-regular objectives expressed as parity conditions can be decided in NP boolean AND coNP. This result substantially improves the best known previous bound of 3EXPTIME. It also shows that the full class of concurrent parity games is no harder than the special case of turn-based stochastic reachability games, for which NP boolean AND coNP is the best known bound. While the previous, more restricted NP boolean AND coNP results for graph games relied on the existence of particularly simple (pure memoryless) optimal strategies, in concurrent games with parity objectives optimal strategies may not exist, and epsilon-optimal strategies (which achieve the value of the game within a parameter epsilon > 0) require in general both randomization and infinite memory. Hence our proof must rely on a more detailed analysis of strategies and, in addition to the main result, yields two results that are interesting on their own. First, we show that there exist epsilon-optimal strategies that in the limit coincide with memoryless strategies; this parallels the celebrated result of Mertens-Neyman for concurrent games with limit-average objectives. Second, we complete the characterization of the memory requirements for epsilon-optimal strategies for concurrent games with parity conditions, by showing that memoryless strategies suffice for epsilon-optimality for coBachi conditions.},
author = {Krishnendu Chatterjee and de Alfaro, Luca and Thomas Henzinger},
pages = {678 -- 687},
publisher = {SIAM},
title = {{The complexity of quantitative concurrent parity games}},
doi = {10.1145/1109557.1109631},
year = {2006},
}
@article{3934,
abstract = {T cells develop in the thymus in a highly specialized cellular and extracellular microenvironment. The basement membrane molecule, laminin-5 (LN-5), is predominantly found in the medulla of the human thymic lobules. Using high-resolution light microscopy, we show here that LN-5 is localized in a bi-membranous conduit-like structure, together with other typical basement membrane components including collagen type IV, nidogen and perlecan. Other interstitial matrix components, such as fibrillin-1 or -2, tenascin-C or fibrillar collagen types, were also associated with these structures. Three-dimensional (3D) confocal microscopy suggested a tubular structure, whereas immunoelectron and transmission electron microscopy showed that the core of these tubes contained fibrillar collagens enwrapped by the LN-5-containing membrane. These medullary conduits are surrounded by thymic epithelial cells, which in vitro were found to bind LN-5, but also fibrillin and tenascin-C. Dendritic cells were also detected in close vicinity to the conduits. Both of these stromal cell types express major histocompatibility complex (MHC) class II molecules capable of antigen presentation. The conduits are connected to blood vessels but, with an average diameter of 2 mum, they are too small to transport cells. However, evidence is provided that smaller molecules such as a 10 kDa dextran, but not large molecules (>500 kDa), can be transported in the conduits. These results clearly demonstrate that a conduit system, which is also known from secondary lymphatic organs such as lymph nodes and spleen, is present in the medulla of the human thymus, and that it might serve to transport small blood-borne molecules or chemokines to defined locations within the medulla.},
author = {Drumea-Mirancea, Mihaela and Wessels, Johannes T and Müller, Claudia A and Essl, Mike and Eble, Johannes A and Tolosa, Eva and Koch, Manuel and Reinhardt, Dieter P and Michael Sixt and Sorokin, Lydia and Stierhof, York-Dieter and Schwarz, Heinz and Klein, Gerd},
journal = {Journal of Cell Science},
number = {Pt 7},
pages = {1396 -- 1405},
publisher = {Company of Biologists},
title = {{Characterization of a conduit system containing laminin-5 in the human thymus: a potential transport system for small molecules}},
doi = {10.1242/jcs.02840},
volume = {119},
year = {2006},
}
@article{4184,
abstract = {Epithelial morphogenesis depends on coordinated changes in cell shape, a process that is still poorly understood. During zebrafish epiboly and Drosophila dorsal closure, cell-shape changes at the epithelial margin are of critical importance. Here evidence is provided for a conserved mechanism of local actin and myosin 2 recruitment during theses events. It was found that during epiboly of the zebrafish embryo, the movement of the outer epithelium (enveloping layer) over the yolk cell surface involves the constriction of marginal cells. This process depends on the recruitment of actin and myosin 2 within the yolk cytoplasm along the margin of the enveloping layer. Actin and myosin 2 recruitment within the yolk cytoplasm requires the Ste20-like kinase Msn1, an orthologue of Drosophila Misshapen. Similarly, in Drosophila, actin and myosin 2 localization and cell constriction at the margin of the epidermis mediate dorsal closure and are controlled by Misshapen. Thus, this study has characterized a conserved mechanism underlying coordinated cell-shape changes during epithelial morphogenesis.},
author = {Köppen, Mathias and Fernández, Beatriz García and Carvalho,Lara and Jacinto, António and Heisenberg, Carl-Philipp},
journal = {Development},
number = {14},
pages = {2671 -- 2681},
publisher = {Company of Biologists},
title = {{Coordinated cell-shape changes control epithelial movement in zebrafish and Drosophila}},
doi = {doi: 10.1242/dev.02439},
volume = {133},
year = {2006},
}
@article{4235,
author = {Harold Vladar and González,J. A},
journal = {Journal of Theoretical Biology},
pages = {91 -- 109},
publisher = {Elsevier},
title = {{Dynamic response of cancer under the influence of immunological activity and therapy}},
year = {2006},
}
@inproceedings{4374,
author = {Maler, Oded and Dejan Nickovic and Pnueli,Amir},
pages = {274 -- 289},
publisher = {Springer},
title = {{From MITL to Timed Automata}},
doi = {1570},
year = {2006},
}
@inproceedings{4406,
abstract = {We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization step implicit. Our algorithm computes the least fixed point of a monotone function on the lattice of antichains of state sets. We evaluate the performance of our algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard one by several orders of magnitude. We also show how variations of the antichain method can be used for solving the language-inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata.},
author = {De Wulf, Martin and Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François},
pages = {17 -- 30},
publisher = {Springer},
title = {{Antichains: A new algorithm for checking universality of finite automata}},
doi = {10.1007/11817963_5},
volume = {4144},
year = {2006},
}
@inproceedings{4432,
abstract = {We add freeze quantifiers to the game logic ATL in order to specify real-time objectives for games played on timed structures. We define the semantics of the resulting logic TATL by restricting the players to physically meaningful strategies, which do not prevent time from diverging. We show that TATL can be model checked over timed automaton games. We also specify timed optimization problems for physically meaningful strategies, and we show that for timed automaton games, the optimal answers can be approximated to within any degree of precision.},
author = {Thomas Henzinger and Prabhu, Vinayak S},
pages = {1 -- 17},
publisher = {Springer},
title = {{Timed alternating-time temporal logic}},
doi = {10.1007/11867340_1},
volume = {4202},
year = {2006},
}
@inproceedings{4437,
abstract = {The synthesis of reactive systems requires the solution of two-player games on graphs with ω-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Büchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Büchi automaton, an equivalent nondeterministic parity automaton that is good for solving games with objective . The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows an incremental search for winning strategies.},
author = {Thomas Henzinger and Piterman, Nir},
pages = {395 -- 410},
publisher = {Springer},
title = {{Solving games without determinization}},
doi = {10.1007/11874683_26},
volume = {4207},
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 = {Thomas Henzinger and Kupferman, Orna and Majumdar, Ritankar S},
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},
}