TY - JOUR
AB - Ageing, or senescence, is a decline in state at later ages that is manifested through a reduction in survival and fecundity. Ageing means that reproductive prospects and hence the life history options (trade-offs) open to the organism decline. Evolutionary theories of ageing suggest that it evolves in response to the level of externally imposed mortality and insults to fertility, either as part of life history optimization or as a result of mutation pressure. Several recent empirical and theoretical studies have produced apparently anomalous results. Some have suggested that the rate of ageing can decline at later ages, others that demographic evidence for ageing can appear in parallel with an improvement in state. All of these studies used measures of ageing that would not be expected to give an accurate reflection of changes in the state of the organism with age. We propose that Fisher's `reproductive value' is a natural measure of state at each age, which includes prospects for both survival and reproduction. If this measure is used, the apparently anomalous findings are not at variance with evolutionary theories of ageing.
AU - Partridge, Linda
AU - Nicholas Barton
ID - 4292
IS - 1375
JF - Proceedings of the Royal Society of London Series B Biological Sciences
TI - On measuring the rate of ageing
VL - 263
ER -
TY - CHAP
AU - Nicholas Barton
AU - Wilson, I
ID - 4294
T2 - New uses for new phylogenies
TI - Genealogies and geography
ER -
TY - GEN
AB - Genetic studies are beginning to provide insights into the evolutionary processes that reduce the fitness of hybrids between recently diverged species. However, the deleterious gene interactions responsible for this fitness reduction are still poorly understood.
AU - Nicholas Barton
ID - 4295
IS - 10
T2 - Current Biology
TI - Speciation: more than the sum of its parts
VL - 6
ER -
TY - THES
AU - Kopke, Peter
ID - 4419
TI - The Theory of Rectangular Hybrid Automata
ER -
TY - CHAP
AB - We use linear hybrid automata to define linear approximations of the phase portraits of nonlinear hybrid systems. The approximating automata can be analyzed automatically using the symbolic model checker HyTech. We demonstrate the technique through the study of predator-prey systems, where we compute population bounds for both species. We also identify a class of nonlinear hybrid automata for which linear phase-portrait approximations can be generated automatically.
AU - Thomas Henzinger
AU - Wong-Toi, Howard
ED - Alur, Rajeev
ED - Thomas Henzinger
ED - Sontag, Eduardo D
ID - 4426
T2 - Hybrid Systems III: Verification and Control
TI - Linear phase-portrait approximations for nonlinear hybrid systems
VL - 1066
ER -
TY - CHAP
AB - We model a steam-boiler control system using hybrid automata. We provide two abstracted linear models of the nonlinear behavior of the boiler. For each model, we define and verify a controller that maintains safe operation of the boiler. The less abstract model permits the design of a more efficient controller. We also demonstrate how the tool HyTech can be used to automatically synthesize control parameter constraints that guarantee safety of the boiler.
AU - Thomas Henzinger
AU - Wong-Toi, Howard
ID - 4427
T2 - Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control
TI - Using HyTech to synthesize control parameters for a steam boiler
VL - 1165
ER -
TY - CONF
AB - Three natural equivalence relations on the infinite state space of a hybrid automaton are language equivalence, simulation equivalence, and bisimulation equivalence. When one of these equivalence relations has a finite quotient, certain model checking and controller synthesis problems are decidable. When bounds on the number of equivalence classes are obtained, bounds on the running times of model checking and synthesis algorithms follow as corollaries.
We characterize the time-abstract versions of these equivalence relations on the state spaces of rectangular hybrid automata (RHA), in which each continuous variable is a clock with bounded drift. These automata are useful for modeling communications protocols with drifting local clocks, and for the conservative approximation of more complex hybrid systems. Of our two main results, one has positive implications for automatic verification, and the other has negative implications. On the positive side, we find that the (finite) language equivalence quotient for RHA is coarser than was previously known by a multiplicative exponential factor. On the negative side, we show that simulation equivalence for RHA is equality (which obviously has an infinite quotient).
Our main positive result is established by analyzing a subclass of timed automata, called one-sided timed automata (OTA), for which the language equivalence quotient is coarser than for the class of all timed automata. An exact characterization of language equivalence for OTA requires a distinction between synchronous and asynchronous definitions of (bi)simulation: if time actions are silent, then the induced quotient for OTA is coarser than if time actions (but not their durations) are visible.
AU - Thomas Henzinger
AU - Kopke, Peter W
ID - 4443
TI - State equivalences for rectangular hybrid automata
VL - 1119
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 main practical limitation of model checking is caused by the size of the state space of the program, which grows exponentially with the number of concurrent components. This problem, known as the state-explosion problem, becomes more difficult when we consider real-time model checking, where the program and the specification involve quantitative references to time. In particular, when use timed automata to describe real-time programs and we specify timed behaviors in the logic TCTL, a real-time extension of the temporal logic CTL with clock variables, then the state space under consideration grows exponentially not only with the number of concurrent components, but also with the number of clocks and the length of the clock constraints used in the program and the specification. Two powerful methods for coping with the state-explosion problem are on-the-fly and space-efficient model checking. In on-the-fly model checking, we explore only the portion of the state space of the program whose exploration is essential for determining the satisfaction of the specification. In space-efficient model checking, we store in memory the minimal information required, preferring to spend time on reconstructing information rather than spend space on storing it. In this work we develop an automata-theoretic approach to TCTL model checking that combines both methods. We suggest, for the first time, a PSPACE on-the-fly model-checking algorithm for TCTL.
AU - Thomas Henzinger
AU - Kupferman, Orna
AU - Vardi, Moshe Y
ID - 4495
TI - A space-efficient on-the-fly algorithm for real-time model checking
VL - 1119
ER -
TY - CONF
AB - We summarize several recent results about hybrid automata. Our goal is to demonstrate that concepts from the theory of discrete concurrent systems can give insights into partly continuous systems, and that methods for the verification of finite-state systems can be used to analyze certain systems with uncountable state spaces
AU - Thomas Henzinger
ID - 4519
TI - The theory of hybrid automata
ER -
TY - GEN
AU - Alur, Rajeev
AU - Thomas Henzinger
ID - 4585
T2 - CAV: Computer Aided Verification
TI - CAV: Computer Aided Verification
VL - 1102
ER -