@inbook{3576,
abstract = {ears of research in biology have established that all cellular functions are deeply connected to the shape and dynamics of their molec- ular actors. As a response, structural molecular biology has emerged as a new line of experimental research focused on revealing the structure of biomolecules. The analysis of these structures has led to the development of computational biology, whose aim is to predict from molecular simulation properties inaccessible to experimental probes.
Here we focus on the representation of biomolecules used in these sim- ulations, and in particular on the hard sphere models. We review how the geometry of the union of such spheres is used to model their interactions with their environment, and how it has been included in simulations of molecular dynamics.
In parallel, we review our own developments in mathematics and com- puter science on understanding the geometry of unions of balls, and their applications in molecular simulation.},
author = {Herbert Edelsbrunner and Koehl, Patrice},
booktitle = {Combinatorial and Computational Geometry},
pages = {243 -- 275},
publisher = {Cambridge University Press},
title = {{The geometry of biomolecular solvation}},
volume = {52},
year = {2005},
}
@inbook{3588,
author = {Castanon Ortega, Irinka and Heisenberg, Carl-Philipp J},
booktitle = {Cell Migration in Development and Disease},
editor = {Wedlich, Doris},
pages = {71 -- 105},
publisher = {Wiley-VCH},
title = {{Cell migration during zebrafish gastrulation}},
doi = {10.1002/3527604669},
year = {2005},
}
@inbook{3589,
abstract = {During zebrafish gastrulation, the interplay between patterning events and morphogenesis creates an embryo out of a seemingly unstructured blastula stage embryo, an embryo with distinct polarities along its anterior–posterior, dorsoventral and left–right axes at the end of gastrulation.},
author = {Köppen, Mathias and Heisenberg, Carl-Philipp J},
booktitle = {Encyclopedia of Life Sciences},
publisher = {Wiley-Blackwell},
title = {{Cleavage and gastrulation in zebrafish embryos}},
doi = {10.1038/npg.els.0001072},
year = {2005},
}
@misc{3590,
author = {Castanon Ortega, Irinka and Heisenberg, Carl-Philipp J},
booktitle = {Nature Cell Biology},
number = {1},
pages = {19 -- 19},
publisher = {Nature Publishing Group},
title = {{A stern view of gastrulation}},
doi = {10.1038/ncb0105-19},
volume = {7},
year = {2005},
}
@inproceedings{4541,
abstract = {Much recent research has focused on the applications of games with ω-regular objectives in the control and verification of reactive systems. However, many of the game-based models are ill-suited for these applications, because they assume that each player has complete information about the state of the system (they are “perfect-information” games). This is because in many situations, a controller does not see the private state of the plant. Such scenarios are naturally modeled by “partial-information” games. On the other hand, these games are intractable; for example, partial-information games with simple reachability objectives are 2EXPTIME-complete.
We study the intermediate case of “semiperfect-information” games, where one player has complete knowledge of the state, while the other player has only partial knowledge. This model is appropriate in control situations where a controller must cope with plant behavior that is as adversarial as possible, i.e., the controller has partial information while the plant has perfect information. As is customary, we assume that the controller and plant take turns to make moves. We show that these semiperfect-information turn-based games are equivalent to perfect-information concurrent games, where the two players choose their moves simultaneously and independently. Since the perfect-information concurrent games are well-understood, we obtain several results of how semiperfect-information turn-based games differ from perfect-information turn-based games on one hand, and from partial-information turn-based games on the other hand. In particular, semiperfect-information turn-based games can benefit from randomized strategies while the perfect-information variety cannot, and semiperfect-information turn-based games are in NP ∩ coNP for all parity objectives.
},
author = {Krishnendu Chatterjee and Thomas Henzinger},
pages = {1 -- 18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Semiperfect-information games}},
doi = {10.1007/11590156_1},
volume = {3821},
year = {2005},
}
@inproceedings{4553,
abstract = {The theory of graph games with ω-regular winning conditions is the foundation for modeling and synthesizing reactive processes. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider two problems for stochastic graph games: the qualitative problem asks for the set of states from which a player can win with probability 1 (almost-sure winning); the quantitative problem asks for the maximal probability of winning (optimal winning) from each state. We show that for Rabin winning conditions, both problems are in NP. As these problems were known to be NP-hard, it follows that they are NP-complete for Rabin conditions, and dually, coNP-complete for Streett conditions. The proof proceeds by showing that pure memoryless strategies suffice for qualitatively and quantitatively winning stochastic graph games with Rabin conditions. This insight is of interest in its own right, as it implies that controllers for Rabin objectives have simple implementations. We also prove that for every ω-regular condition, optimal winning strategies are no more complex than almost-sure winning strategies.},
author = {Krishnendu Chatterjee and de Alfaro, Luca and Thomas Henzinger},
pages = {878 -- 890},
publisher = {Springer},
title = {{The complexity of stochastic Rabin and Streett games}},
doi = {10.1007/11523468_71},
volume = {3580},
year = {2005},
}
@inproceedings{4554,
abstract = {Games played on graphs may have qualitative objectives, such as the satisfaction of an ω-regular property, or quantitative objectives, such as the optimization of a real-valued reward. When games are used to model reactive systems with both fairness assumptions and quantitative (e.g., resource) constraints, then the corresponding objective combines both a qualitative and a quantitative component. In a general case of interest, the qualitative component is a parity condition and the quantitative component is a mean-payoff reward. We study and solve such mean-payoff parity games. We also prove some interesting facts about mean-payoff parity games which distinguish them both from mean-payoff and from parity games. In particular, we show that optimal strategies exist in mean-payoff parity games, but they may require infinite memory.},
author = {Krishnendu Chatterjee and Thomas Henzinger and Jurdziński, Marcin},
pages = {178 -- 187},
publisher = {IEEE},
title = {{Mean-payoff parity games}},
doi = {10.1109/LICS.2005.26},
year = {2005},
}
@inproceedings{4557,
abstract = {Planning in adversarial and uncertain environments can be modeled as the problem of devising strategies in stochastic perfect information games. These games are generalizations of Markov decision processes (MDPs): there are two (adversarial) players, and a source of randomness. The main practical obstacle to computing winning strategies in such games is the size of the state space. In practice therefore, one typically works with abstractions of the model. The diffculty is to come up with an abstraction that is neither too coarse to remove all winning strategies (plans), nor too fine to be intractable. In verification, the paradigm of counterexample-guided abstraction refinement has been successful to construct useful but parsimonious abstractions automatically. We extend this paradigm to probabilistic models (namely, perfect information games and, as a special case, MDPs). This allows us to apply the counterexample-guided abstraction paradigm to the AI planning problem. As special cases, we get planning algorithms for MDPs and deterministic systems that automatically construct system abstractions.},
author = {Krishnendu Chatterjee and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S},
pages = {104 -- 111},
publisher = {AUAI Press},
title = {{Counterexample-guided planning}},
year = {2005},
}
@inproceedings{4560,
abstract = {We define and study a quantitative generalization of the traditional boolean framework of model-based specification and verification. In our setting, propositions have integer values at states, and properties have integer values on traces. For example, the value of a quantitative proposition at a state may represent power consumed at the state, and the value of a quantitative property on a trace may represent energy used along the trace. The value of a quantitative property at a state, then, is the maximum (or minimum) value achievable over all possible traces from the state. In this framework, model checking can be used to compute, for example, the minimum battery capacity necessary for achieving a given objective, or the maximal achievable lifetime of a system with a given initial battery capacity. In the case of open systems, these problems require the solution of games with integer values.
Quantitative model checking and game solving is undecidable, except if bounds on the computation can be found. Indeed, many interesting quantitative properties, like minimal necessary battery capacity and maximal achievable lifetime, can be naturally specified by quantitative-bound automata, which are finite automata with integer registers whose analysis is constrained by a bound function f that maps each system K to an integer f(K). Along with the linear-time, automaton-based view of quantitative verification, we present a corresponding branching-time view based on a quantitative-bound μ-calculus, and we study the relationship, expressive power, and complexity of both views.
},
author = {Chakrabarti, Arindam and Krishnendu Chatterjee and Thomas Henzinger and Kupferman, Orna and Majumdar, Ritankar S},
pages = {50 -- 64},
publisher = {Springer},
title = {{Verifying quantitative properties using bound functions}},
doi = {10.1007/11560548_7},
volume = {3725},
year = {2005},
}
@inproceedings{4624,
abstract = {Surveying results from [5] and [6], we motivate and introduce the theory behind formalizing rich interfaces for software and hardware components. Rich interfaces specify the protocol aspects of component interaction. Their formalization, called interface automata, permits a compiler to check the compatibility of component interaction protocols. Interface automata support incremental design and independent implementability. Incremental design means that the compatibility checking of interfaces can proceed for partial system descriptions, without knowing the interfaces of all components. Independent implementability means that compatible interfaces can be refined separately, while still maintaining compatibility.},
author = {de Alfaro, Luca and Thomas Henzinger},
pages = {83 -- 104},
publisher = {Springer},
title = {{Interface-based design}},
doi = {10.1007/1-4020-3532-2_3},
volume = {195},
year = {2005},
}