@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},
}
@inproceedings{4526,
abstract = {We designed and implemented a new programming language called Hierarchical Timing Language (HTL) for hard realtime systems. Critical timing constraints are specified within the language,and ensured by the compiler. Programs in HTL are extensible in two dimensions without changing their timing behavior: new program modules can be added, and individual program tasks can be refined. The mechanism supporting time invariance under parallel composition is that different program modules communicate at specified instances of time. Time invariance under refinement is achieved by conservative scheduling of the top level. HTL is a coordination language, in that individual tasks can be implemented in "foreign" languages. As a case study, we present a distributed HTL implementation of an automotive steer-by-wire controller.},
author = {Ghosal, Arkadeb and Thomas Henzinger and Iercan, Daniel and Kirsch, Christoph M and Sangiovanni-Vincentelli, Alberto},
pages = {132 -- 141},
publisher = {ACM},
title = {{A hierarchical coordination language for interacting real-time tasks}},
doi = {10.1145/1176887.1176907},
year = {2006},
}
@inproceedings{4552,
abstract = {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 > 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 = {Krishnendu Chatterjee and de Alfaro, Luca and Thomas Henzinger},
pages = {291 -- 300},
publisher = {IEEE},
title = {{Strategy improvement for concurrent reachability games}},
doi = {10.1109/QEST.2006.48},
year = {2006},
}
@inproceedings{4401,
author = {Alur, Rajeev and Pavol Cerny and Zdancewic,Steve},
pages = {107 -- 118},
publisher = {Springer},
title = {{Preserving Secrecy Under Refinement}},
doi = {1543},
year = {2006},
}
@inproceedings{4538,
abstract = {A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with ω-regular winning conditions specified as parity objectives. These games lie in NP ∩ coNP. We present a strategy improvement algorithm for stochastic parity games; this is the first non-brute-force algorithm for solving these games. From the strategy improvement algorithm we obtain a randomized subexponential-time algorithm to solve such games.},
author = {Krishnendu Chatterjee and Thomas Henzinger},
pages = {512 -- 523},
publisher = {Springer},
title = {{Strategy improvement and randomized subexponential algorithms for stochastic parity games}},
doi = {10.1007/11672142_42},
volume = {3884},
year = {2006},
}
@inproceedings{578,
abstract = {A source of single photons allows secure quantum key distribution, in addition, to being a critical resource for linear optics quantum computing. We describe our progress on deterministically creating single photons from spontaneous parametric downconversion, an extension of the Pittman, Jacobs and Franson scheme [Phys. Rev A, v66, 042303 (2002)]. Their idea was to conditionally prepare single photons by measuring one member of a spontaneously emitted photon pair and storing the remaining conditionally prepared photon until a predetermined time, when it would be "deterministically" released from storage. Our approach attempts to improve upon this by recycling the pump pulse in order to decrease the possibility of multiple-pair generation, while maintaining a high probability of producing a single pair. Many of the challenges we discuss are central to other quantum information technologies, including the need for low-loss optical storage, switching and detection, and fast feed-forward control.},
author = {Peters, Nicholas A and Arnold, Keith J and VanDevender, Aaron P and Jeffrey, Evan R and Rangarajan, Radhika and Onur Hosten and Barreiro, Julio T and Altepeter, Joseph B and Kwiat, Paul G},
publisher = {SPIE},
title = {{Towards a quasi-deterministic single-photon source}},
doi = {10.1117/12.684702},
volume = {6305},
year = {2006},
}
@article{573,
abstract = {Mitchison and Jozsa recently suggested that the "chained-Zeno" counterfactual computation protocol recently proposed by Hosten et al. is counterfactual for only one output of the computer. This claim was based on the existing abstract algebraic definition of counterfactual computation, and indeed according to this definition, their argument is correct. However, a more general definition (physically adequate) for counterfactual computation is implicitly assumed by Hosten et. al. Here we explain in detail why the protocol is counterfactual and how the "history tracking" method of the existing description inadequately represents the physics underlying the protocol. Consequently, we propose a modified definition of counterfactual computation. Finally, we comment on one of the most interesting aspects of the error-correcting protocol. },
author = {Onur Hosten and Rakher, Matthew T and Barreiro, Julio T and Peters, Nicholas A and Kwiat, Paul G},
journal = {Quantum Physics},
publisher = {ArXiv},
title = {{Counterfactual computation revisited}},
year = {2006},
}
@article{903,
abstract = {Background: Carcinogenesis typically involves multiple somatic mutations in caretaker (DNA repair) and gatekeeper (tumor suppressors and oncogenes) genes. Analysis of mutation spectra of the tumor suppressor that is most commonly mutated in human cancers, p53, unexpectedly suggested that somatic evolution of the p53 gene during tumorigenesis is dominated by positive selection for gain of function. This conclusion is supported by accumulating experimental evidence of evolution of new functions of p53 in tumors. These findings prompted a genome-wide analysis of possible positive selection during tumor evolution. Methods: A comprehensive analysis of probable somatic mutations in the sequences of Expressed Sequence Tags (ESTs) from malignant tumors and normal tissues was performed in order to access the prevalence of positive selection in cancer evolution. For each EST, the numbers of synonymous and non-synonymous substitutions were calculated. In order to identify genes with a signature of positive selection in cancers, these numbers were compared to: i) expected numbers and ii) the numbers for the respective genes in the ESTs from normal tissues. Results: We identified 112 genes with a signature of positive selection in cancers, i.e., a significantly elevated ratio of non-synonymous to synonymous substitutions, in tumors as compared to 37 such genes in an approximately equal-sized EST collection from normal tissues. A substantial fraction of the tumor-specific positive-selection candidates have experimentally demonstrated or strongly predicted links to cancer. Conclusion: The results of EST analysis should be interpreted with extreme caution given the noise introduced by sequencing errors and undetected polymorphisms. Furthermore, an inherent limitation of EST analysis is that multiple mutations amenable to statistical analysis can be detected only in relatively highly expressed genes. Nevertheless, the present results suggest that positive selection might affect a substantial number of genes during tumorigenic somatic evolution.},
author = {Babenko, Vladimir N and Basu, Malay K and Fyodor Kondrashov and Rogozin, Igor B and Koonin, Eugene V},
journal = {BMC Cancer},
publisher = {BioMed Central},
title = {{Signs of positive selection of somatic mutations in human cancers detected by EST sequence analysis}},
doi = {10.1186/1471-2407-6-36},
volume = {6},
year = {2006},
}
@article{869,
abstract = {The impact of synonymous nucleotide substitutions on fitness in mammals remains controversial. Despite some indications of selective constraint, synonymous sites are often assumed to be neutral, and the rate of their evolution is used as a proxy for mutation rate. We subdivide all sites into four classes in terms of the mutable CpG context, nonCpG, postC, preG, and postCpreG, and compare four-fold synonymous sites and intron sites residing outside transposable elements. The distribution of the rate of evolution across all synonymous sites is trimodal. Rate of evolution at nonCpG synonymous sites, not preceded by C and not followed by G, is ∼10% below that at such intron sites. In contrast, rate of evolution at postCpreG synonymous sites is ∼30% above that at such intron sites. Finally, synonymous and intron postC and preG sites evolve at similar rates. The relationship between the levels of polymorphism at the corresponding synonymous and intron sites is very similar to that between their rates of evolution. Within every class, synonymous sites are occupied by G or C much more often than intron sites, whose nucleotide composition is consistent with neutral mutation-drift equilibrium. These patterns suggest that synonymous sites are under weak selection in favor of G and C, with the average coefficient s∼0.25/Ne∼10-5, where Ne is the effective population size. Such selection decelerates evolution and reduces variability at sites with symmetric mutation, but has the opposite effects at sites where the favored nucleotides are more mutable. The amino-acid composition of proteins dictates that many synonymous sites are CpGprone, which causes them, on average, to evolve faster and to be more polymorphic than intron sites. An average genotype carries ∼107 suboptimal nucleotides at synonymous sites, implying synergistic epistasis in selection against them.},
author = {Fyodor Kondrashov and Ogurtsov, Aleksey Yu and Kondrashov, Alexey S},
journal = {Journal of Theoretical Biology},
number = {4},
pages = {616 -- 626},
publisher = {Elsevier},
title = {{Selection in favor of nucleotides G and C diversifies evolution rates and levels of polymorphism at mammalian synonymous sites}},
doi = {10.1016/j.jtbi.2005.10.020},
volume = {240},
year = {2006},
}
@article{3009,
author = {Paciorek, Tomasz and Friml, Jirí},
journal = {Journal of Cell Science},
number = {7},
pages = {1199 -- 1202},
publisher = {Company of Biologists},
title = {{Auxin signaling}},
doi = {10.1242/jcs.02910},
volume = {119},
year = {2006},
}
@article{3908,
abstract = {It is commonly believed that both the average length and the frequency of microsatellites correlate with genome size. We have estimated the frequency and the average length for 69 perfect dinucleotide microsatellites in an insect with an exceptionally large genome: Chorthippus biguttulus (Orthoptera, Acrididae). Dinucleotide microsatellites are not more frequent in C. biguttulus, but repeat arrays are 1.4 to 2 times longer than in other insect species. The average repeat number in C. biguttulus lies in the range of higher vertebrates. Natural populations are highly variable. At least 30 alleles per locus were found and the expected heterozygosity is above 0.95 at all three loci studied. In contrast, the observed heterozygosity is much lower (≤0.51), which could be caused by long null alleles.},
author = {Ustinova, Jana and Achmann, Roland and Cremer, Sylvia and Mayer, Frieder},
journal = {Journal of Molecular Evolution},
number = {2},
pages = {158 -- 167},
publisher = {Springer},
title = {{Long repeats in a huge gemome: microsatellite loci in the grasshopper Chorthippus biguttulus}},
doi = {10.1007/s00239-005-0022-6},
volume = {62},
year = {2006},
}