TY - GEN
AU - Nicholas Barton
ID - 4290
IS - 2
T2 - Genetical Research
TI - Natural hybridization and evolution
VL - 70
ER -
TY - GEN
AU - Nicholas Barton
ID - 4291
IS - 2
T2 - Genetical Research
TI - The ccological detective: Confronting models with data
VL - 70
ER -
TY - CHAP
AB - Natural populations differ from the simplest models in ways which can significantly affect their evolution. Real populations are rarely all of the same size; the rates of migration into and out of populations vary in space and time; some populations go extinct, and new ones are established, while all populations fluctuate in size. Furthermore, the genetic properties of real species are not like those assumed in simple models. Alleles are exposed to a wide variety of selection mutation rarely creates novel genotypes with each mutation event, generations overlap, and environments vary from place to place. Evolution in a metapopulation can be substantially different from the predictions of single-population models and, indeed, very different from the simplest models of subdivided species.
AU - Nicholas Barton
AU - Whitlock, Michael
ID - 4293
T2 - Metapopulation Biology
TI - The evolution of metapopulations
ER -
TY - CONF
AB - In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal-logic formula that specifies the behavior. The model-checking problem for the branching-time temporal logic CTL can be solved in linear running time, and model-checking tools for CTL are used successfully in industrial applications. The development of programs that must meet rigid real-time constraints has brought with it a need for real-time temporal logics that enable quantitative reference to time. Early research on real-time temporal logics uses the discrete domain of the integers to model time. Present research on real-time temporal logics focuses on continuous time and uses the dense domain of the reals to model time. There, model checking becomes significantly more complicated. For example, the model-checking problem for TCTL, a continuous-time extension of the logic CTL, is PSPACE-complete.
In this paper we suggest a reduction from TCTL model checking to CTL model checking. The contribution of such a reduction is twofold. Theoretically, while it has long been known that model-checking methods for untimed temporal logics can be extended quite easily to handle discrete time, it was not clear whether and how untimed methods can handle the reset quantifier of TCTL, which resets a realvalued clock. Practically, our reduction enables anyone who has a tool for CTL model checking to use it for TCTL model checking. The TCTL model-checking algorithm that follows from our reduction is in PSPACE, matching the known bound for this problem. In addition, it enjoys the wide distribution of CTL model-checking tools and the extensive and fruitful research efforts and heuristics that have been put into these tools.
AU - Thomas Henzinger
AU - Kupferman, Orna
ID - 4438
TI - From quantity to quality
VL - 1201
ER -
TY - CONF
AB - Rectangular hybrid automata model digital control programs of analog plant environments. We study rectangular hybrid automata where the plant state evolves continuously in real-numbered time, and the controller samples the plant state and changes the control state discretely, only at the integer points in time. We prove that rectangular hybrid automata have finite bisimilarity quotients when all control transitions happen at integer times, even if the constraints on the derivatives of the variables vary between control states. This is sharply in contrast with the conventional model where control transitions may happen at any real time, and already the reachability problem is undecidable. Based on the finite bisimilarity quotients, we give an exponential algorithm for the symbolic sampling-controller synthesis of rectangular automata. We show our algorithm to be optimal by proving the problem to be EXPTIME-hard. We also show that rectangular automata form a maximal class of systems for which the sampling-controller synthesis problem can be solved algorithmically.
AU - Thomas Henzinger
AU - Kopke, Peter W
ID - 4441
TI - Discrete-time control for rectangular hybrid automata
VL - 1256
ER -