Cellular and subcellular distribution of substance P receptor immunoreactivity in the dorsal vagal complex of the rat and cat: A light and electron microscope study - Baude, Agnès; Shigemoto, Ryuichi (Journal of Comparative Neurology)
Immunoreactivity for the substance P receptor (NK1 receptor) has been investigated by light and electron microscopy in the dorsal vagal complexes of adult rats and cats. The general pattern of NK1 immunoreactivity was similar for both rat and cat. Numerous NK1-immunoreactive neurons were present in the area postrema, the nucleus of the solitary tract, and the dorsal motor nucleus of the vagus nerve. The density of labelled neurons differed between the subnuclei of the nucleus of the solitary tract. Overall, the efferent neurons of the dorsal motor nucleus of the vagus nerve highly expressed NK1 when compared to neurons in the nucleus of the solitary tract. The results are discussed with reference to the viscerotopic organisation of the dorsal vagal complex. Ultrastructural analysis demonstrated that NK1 immunoreactivity was present only at the membrane surface of somatic and dendritic profiles of neurons. No labelling was found in axon terminals, axons, or glial processes. NK1 immunoreactivity, as revealed by a preembedding immunogold technique in serial ultrathin sections; was preferentially located at nonsynaptic sites. A semiquantitative study suggested that the density of NK1 receptors is statistically higher at membrane sites free of any contact (synaptic or not) with axon terminals. The subcellular localisation of NK1 immunoreactivity was similar for neurons of both rat and cat. These results suggest that in the dorsal vagal complex, substance P might act on NK1 receptors through a process of volume transmission.

Linear Boltzmann equation as scaling limit of quantum Lorentz gas - Erdös, László; Yau, Horng (Advances in Differential Equations and Mathematical Physics)
We study a quantum particle in a random potential in two scaling limits: the low density limit (or Boltzman-Grad) and the weak coupling limit. The low density limit is the quantum analogue of the Lorentz gas. In both cases, the phase space density of the quantum evolution defined through the Wigner transform or the Husimi function converges weakly to a linear Boltz-mann equation with collision kernel given by the quantum scattering cross section.

Lifschitz tail in a magnetic field: The nonclassical regime - Erdös, László (Probability Theory and Related Fields)
We obtain the Lifschitz tail, i.e. the exact low energy asymptotics of the integrated density of states (IDS) of the two-dimensional magnetic Schrödinger operator with a uniform magnetic field and random Poissonian impurities. The single site potential is repulsive and it has a finite but nonzero range. We show that the IDS is a continuous function of the energy at the bottom of the spectrum. This result complements the earlier (nonrigorous) calculations by Brézin, Gross and Itzykson which predict that the IDS is discontinuous at the bottom of the spectrum for zero range (Dirac delta) impurities at low density. We also elucidate the reason behind this apparent controversy. Our methods involve magnetic localization techniques (both in space and energy) in addition to a modified version of the "enlargement of obstacles" method developed by A.-S. Sznitman.

Functional and molecular differences between voltage-gated K+ channels of fast-spiking interneurons and pyramidal neurons of rat hippocampus - Martina, Marco; Schultz, Jobst; Ehmke, Heimo; Monyer, Hannah; Jonas, Peter M (Journal of Neuroscience)
We have examined gating and pharmacological characteristics of somatic K+ channels in fast-spiking interneurons and regularly spiking principal neurons of hippocampal slices. In nucleated patches isolated from basket cells of the dentate gyrus, a fast delayed rectifier K+ current component that was highly sensitive to tetraethylammonium (TEA) and 4-aminopyridine (4- AP) (half-maximal inhibitory concentrations <0.1 mM) predominated, contributing an average of 58% to the total K+ current in these cells. By contrast, in pyramidal neurons of the CA1 region a rapidly inactivating A- type K+ current component that was TEA-resistant prevailed, contributing 61% to the total K+ current. Both types of neurons also showed small amounts of the K+ current component mainly found in the other type of neuron and, in addition, a slow delayed rectifier K+ current component with intermediate properties (sow inactivation, intermediate sensitivity to TEA). Single-cell RT-PCR analysis of mRNA revealed that Kv3 (Kv3.1, Kv3.2) subunit transcripts were expressed in almost all (89%) of the interneurons but only in 17% of the pyramidal neurons. In contrast, Kv4 (Kv4.2, Kv4.3) subunit mRNAs were present in 87% of pyramidal neurons but only in 55% of interneurons. Selective block of fast delayed rectifier K+ channels, presumably assembled from Kv3 subunits, by 4-AP reduced substantially the action potential frequency in interneurons. These results indicate that the differential expression of Kv3 and Kv4 subunits shapes the action potential phenotypes of principal neurons and interneurons in the cortex.

Corelease of two fast neurotransmitters at a central synapse - Jonas, Peter M; Bischofberger, Joseph; Sandkühler, Jürgen (Science)
It is widely accepted that individual neurons in the central nervous system release only a single fast transmitter. The possibility of corelease of fast neurotransmitters was examined by making paired recordings from synaptically connected neurons in spinal cord slices. Unitary inhibitory postsynaptic currents generated at interneuron-motoneuron synapses consisted of a strychnine-sensitive, glycine receptor-mediated component and a bicuculline-sensitive, γ-aminobutyric acid (GABA)(A) receptor-mediated component. These results indicate that spinal interneurons release both glycine and GABA to activate functionally distinct receptors in their postsynaptic target cells. A subset of miniature synaptic currents also showed both components, consistent with corelease from individual synaptic vesicles.

Apparatus and method for geometric morphing - Edelsbrunner, Herbert; Fu, Ping
A method of geometric morphing between a first object having a first shape and a second object having a second shape. The method includes the steps of generating a first Delaunay complex corresponding to the first shape and a second Delaunay complex corresponding to the second shape and generating a plurality of intermediary Delaunay complexes defined by a continuous family of mixed shapes corresponding to a mixing of the first shape and the second shape. The method further includes the steps of constructing a first skin corresponding to the first Delaunay complex and a second skin corresponding to the second Delaunay complex and constructing a plurality of intermediary skins corresponding to the plurality of intermediary Delaunay complexes. The first skin, second skin and plurality of intermediary skins may be visually displayed on an output device.

Reliability and state dependence of pyramidal cell-interneuron synapses in the hippocampus: an ensemble approach in the behaving rat - Csicsvari, Jozsef L; Hirase, Hajima; Czurkó, András; Buzsáki, György (Neuron)
Spike transmission probability between pyramidal cells and interneurons in the CA1 pyramidal layer was investigated in the behaving rat by the simultaneous recording of neuronal ensembles. Population synchrony was strongest during sharp wave (SPW) bursts. However, the increase was three times larger for pyramidal cells than for interneurons. The contribution of single pyramidal cells to the discharge of interneurons was often large (up to 0.6 probability), as assessed by the presence of significant (<3 ms) peaks in the cross-correlogram. Complex-spike bursts were more effective than single spikes. Single cell contribution was higher between SPW bursts than during SPWs or theta activity. Hence, single pyramidal cells can reliably discharge interneurons, and the probability of spike transmission is behavior dependent.

Hippocampal pyramidal neutrons “space-clamped” in a running wheel task: Place cells or path integrators? - Hirase, Hajima; Czurkó, András; Jozsef Csicsvari; Buzsáki, György (European Journal of Neuroscience)

Auditory Morse analysis of triangulated manifolds - Axen, Ulrike; Edelsbrunner, Herbert (Mathematical Visualization)
Visualization of high-dimensional or large geometric data sets is inherently difficult, so we experiment with the use of audio to display the shape and connectivity of these data sets. Sonification is used as both an addition to and a substitution for the visual display. We describe a new algorithm called wave traversal that provides a necessary intermediate step to sonification of the data; it produces an ordered sequence of subsets, called waves, that allows us to map the data to time. In this paper we focus in detail on the mathematics of wave traversal, in particular, how wave traversal can be used as a discrete Morse function.

Partitioning the components of sexual selection: attractiveness and agonistic behaviour in male wax moths, Achroia grisella (Lepidoptera, Pyralidae) - Cremer, Sylvia; Greenfield, Michael (Ethology)
Two components of sexual selection in the lesser wax moth, Achroia grisella, are clearly defined: females choose males based on characters of their ultrasonic advertisement signals, and males display agonistic behaviour patterns in contests over signalling stations. We conducted a series of laboratory trials to determine whether successes in these two sexual selection arenas were related. Our trials showed that winners in contests over signalling stations were characterized by earlier initiation of both signalling and aggression. These characteristics may indicate higher levels of ‘motivation,’ but it is unclear whether this level is a fixed trait. There was no relationship, however, between any measure of a male's attractiveness to females and his success in winning competition trials. Thus, inter- and intra-sexual selection may be acting on different, uncorrelated traits in A. grisella.

Analytical shape computation of macromolecules: I. molecular area and volume through alpha shape - Liang, Jie; Edelsbrunner, Herbert; Fu, Ping; Sudhakar, Pamidighantam; Subramaniam, Shankar (Proteins: Structure, Function and Bioinformatics)
The size and shape of macromolecules such as proteins and nucleic acids play an important role in their functions. Prior efforts to quantify these properties have been based on various discretization or tessellation procedures involving analytical or numerical computations. In this article, we present an analytically exact method for computing the metric properties of macromolecules based on the alpha shape theory. This method uses the duality between alpha complex and the weighted Voronoi decomposition of a molecule. We describe the intuitive ideas and concepts behind the alpha shape theory and the algorithm for computing areas and volumes of macromolecules. We apply our method to compute areas and volumes of a number of protein systems. We also discuss several difficulties commonly encountered in molecular shape computations and outline methods to overcome these problems. (C) 1998 Wiley-Liss, Inc.

Geometry for modeling biomolecules - Edelsbrunner, Herbert (Robotics: The Algorithmic Perspective)
Space Filing diagrams are geometric models of molecular conformations in three-dimensional space. Each atom is a location is space and a quantitative expression of influence on the immediate surrounding. This paper surveys the basic types of space filling diagrams with a focus on the dual alpha shape. Properties of those diagrams that relate to questions of connectivity, size, shape and symmetry, and metamorphosis are discussed.

Persistence and temporal compression of spike sequences during fast field oscillation in the hippocampus - Nádasdy, Zoltán; Jozsef Csicsvari; Hirase, Hajima; Czurkó, András; Buzsáki, György (European Journal of Neuroscience)

Monosynaptic interactions between CA1 Pyramidal cells and interneuron in the behaving rat - Jozsef Csicsvari; Czurkó, András; Hirase, Hajima; Buzsáki, György (European Journal of Neuroscience)

Habitat preference in the Bombina hybrid zone in Croatia - Maccallum, Catriona; Nürnberger, Beate; Barton, Nicholas H; Szymura, Jacek (Evolution)
This paper demonstrates the effect of habitat heterogeneity and a habitat preference on the genetic structure of a hybrid zone between the toads Bombina bombina and B. variegata (Anura: Discoglossidae); 1613 toads from 85 sites across a transect near Pešćenica, Croatia, were scored for five unlinked diagnostic allozyme markers. These were found to be largely concordant. Aside from minor systematic deviations, there was little variance in allele frequency among loci within sites. Yet the allele frequencies did not follow a smooth cline, but formed a mosaic in the center, such that neighboring sites could differ markedly in their enzyme score. A detailed ecological survey revealed a correlation between this pattern and habitat. In keeping with the typical breeding sites of the parental taxa, B. bombina-like hybrids were found more often in ponds, whereas B. variegata-like hybrids were more common in puddles. In addition, there was significant heterozygote deficit (FIS) and strong linkage disequilibrium (R), both of which were stronger on the B. bombina side of the transect, and stronger in puddles than ponds. Mark-recapture data showed: (1) that the animals disperse beyond the scale of the habitat pattern; (2) frequent turn-over of individuals within sites; and (3) nonrandom movement between two sites of different habitat type. We conclude that an active habitat preference must contribute to the observed association between marker alleles and habitat. As a consequence, there is incomplete mixing of the two gene pools, which could explain the high level of FIS and R. The asymmetry in these parameters may reflect asymmetry in the preference or in the distribution of habitats across the zone. We discuss the implications of habitat preference for the dynamics of hybrid zones.

Testing for epistasis between deleterious mutations - West, Stuart; Peters, Andrew; Barton, Nicholas H (Genetics)
Determining the way in which deleterious mutations interact in their effects on fitness is crucial to numerous areas in population genetics and evolutionary biology. For example, if each additional mutation leads to a greater decrease in log fitness than the last (synergistic epistasis), then the evolution of sex and recombination may be favored to facilitate the elimination of deleterious mutations. However, there is a severe shortage of relevant data. Three relatively simple experimental methods to test for epistasis between deleterious mutations in haploid species have recently been proposed. These methods involve crossing individuals and examining the mean and/or skew in log fitness of the offspring and parents. The main aim of this paper is to formalize these methods, and determine the most effective way in which tests for epistasis could be carried out. We show that only one of these methods is likely to give useful results: crossing individuals that have very different numbers of deleterious mutations, and comparing the mean log fitness of the parents with that of their offspring. We also reconsider experimental data collected on Chlamydomonas moewussi using two of the three methods. Finally, we suggest how the test could be applied to diploid species.

The effect of hitch-hiking on neutral genealogies - Barton, Nicholas H (Genetical Research)
When a favourable mutation sweeps to fixation, those genes initially linked to it increase in frequency; on average, this reduces diversity in the surrounding region of the genome. In the first analysis of this 'hitch-hiking' effect, Maynard-Smith and Haigh followed the increase of the neutral allele that chanced to be associated with the new mutation in the first generation, and assumed that the subsequent increase was deterministic. Later analyses, based on either coalescence arguments, or on diffusion equations for the mean and variance of allele frequency, have also made one or both of these assumptions. In the early generations, stochastic fluctuations in the frequency of the selected allele, and coalescence of neutral lineages, can be accounted for correctly by following relationships between genes conditional on the number of copies of the favourable allele. This analysis shows that the hitch-hiking effect is increased because an allele that is destined to fix tends to increase more rapidly than exponentially. However, the identity generated by the selective sweep has the same form as in previous work, h[r/s] (2 Ns)(-2r/s), where h[r/s] tends to 1 with tight linkage. This analysis is extended to samples of many genes; then, genes may trace back to several families of lineages, each related through a common ancestor early in the selective sweep. Simulations show that the number and sizes of these families can (in principle) be used to make separate estimates of r/s and Ns.

Anatomy of protein pockets and cavities: Measurement of binding site geometry and implications for ligand design - Liang, Jie; Edelsbrunner, Herbert; Woodward, Clare (Protein Science)
Identification and size characterization of surface pockets and occluded cavities are initial steps in protein structure-based ligand design. A new program, CAST, for automatically locating and measuring protein pockets and cavities, is based on precise computational geometry methods, including alpha shape and discrete flow theory. CAST identifies and measures pockets and pocket mouth openings, as well as cavities. The program specifies the atoms lining pockets, pocket openings. and buried cavities; the volume and area of pockets and cavities; and the area and circumference of mouth openings. CAST analysis of over 100 proteins has been carried out; proteins examined include a set of 51 monomeric enzyme-ligand structures, several elastase-inhibitor complexes, the FK506 binding protein, 30 HIV-1 protease-inhibitor complexes, and a number of small and large protein inhibitors, Medium-sized globular proteins typically have 10-20 pockets/cavities. Most often, binding sites are pockets with 1-2 mouth openings; much less frequently they are cavities. Ligand binding pockets vary widely in size, most within the range 10(2)-10(3) Angstrom(3). Statistical analysis reveals that the number of pockets and cavities is correlated with protein size, but there is no correlation between the size of the protein and the size of binding sites. Most frequently, the largest pocket/cavity is thp active site, but there are a number of instructive exceptions. Ligand volume and binding site volume are somewhat correlated when binding site volume is less than or equal to 700 Angstrom(3), but the ligand seldom occupies the entire site. Auxiliary pockets near the active site have been suggested as additional binding surface for designed ligands (Mattos C ct al., 1993, Nat Struct Biol 1:55-58). Analysis of elastase-inhibitor complexes suggests that CAST can identify ancillary pockets, suitable for recruitment in ligand design strategies. Analysis of the FK506 binding protein, and of compounds developed in SAR by NMR (Shuker SE et al.. 1996, Science 274:1531-1534), indicates that CAST pocket computation may provide a priori identification of target proteins for Linked-fragment design. CAST analysis of 30 HIV-1 protease-inhibitor complexes shows that the flexible active site pocket can vary over a range of 853-1,566 Angstrom(3), and that there are two pockets near or adjoining the active site that may be recruited for ligand design.

Analytical shape computation of macromolecules: II. Inaccessible cavities in proteins - Liang, Jie; Edelsbrunner, Herbert; Fu, Ping; Sudhakar, Pamidighantam; Subramaniam, Shankar (Proteins: Structure, Function and Bioinformatics)
The structures of proteins are well-packed, yet they contain numerous cavities which play key roles in accommodating small molecules, or enabling conformational changes. From high-resolution structures it is possible to identify these cavities. We have developed a precise algorithm based on alpha shapes for measuring space-filling-based molecular models (such as van der Waals, solvent accessible, and molecular surface descriptions). We applied this method for accurate computation of the surface area and volume of cavities in several proteins. In addition, all of the atoms/residues Lining the cavities are identified, We use this method to study the structure and the stability of proteins, as well as to locate cavities that could contain structural water molecules in the proton transport pathway in the membrane protein bacteriorhodopsin.

On the definition and the construction of pockets in macromolecules - Edelsbrunner, Herbert; Facello, Michael; Liang, Jie (Discrete Applied Mathematics)
The shape of a protein is important for its functions, This includes the location and size of identifiable regions in its complement space. We formally define pockets as regions in the complement with limited accessibility from the outside. Pockets can be efficiently constructed by an algorithm based on alpha complexes. The algorithm is implemented and applied to proteins with known three-dimensional conformations. 1998 Published by Elsevier Science B.V. All rights reserved.

Shape reconstruction with Delaunay complex - Edelsbrunner, Herbert (Proceedingsof the 3rd Latin American Symposium on Theoretical Informatics)
The reconstruction of a shape or surface from a finite set of points is a practically significant and theoretically challenging problem. This paper presents a unified view of algorithmic solutions proposed in the computer science literature that are based on the Delaunay complex of the points.

Shape space from deformation - Cheng, Ho; Edelsbrunner, Herbert; Fu, Ping (Proceedings of the 6th Pacific Conference on Computer Graphics and Applications)
The construction of shape spaces is studied from a mathematical and a computational viewpoint. A program is outlined reducing the problem to four tasks: the representation of geometry, the canonical deformation of geometry, the measuring of distance in shape space, and the selection of base shapes. The technical part of this paper focuses on the second task: the specification of a deformation mixing two or more shapes in continuously, changing proportions.

Wrapping 3D scanning data - Edelsbrunner, Herbert; Facello, Michael; Fu, Ping; Qian, Jiang; Nekhayev, Dmitry
Geomagic Wrap™ is a commercially available software for reconstructing shapes and surfaces from 3D scanning data. The data can be any arbitrary finite point set in 3D, and there are no requirements on local density or organization in slices etc. The software contains components for surface reconstruction, improvement, and analysis, and it supports a variety of input and output formats that make it compatible with scanning hardware and CAD and graphics software.

Why sex and recombination? - Barton, Nicholas H; Charlesworth, Brian (Science)
Most higher organisms reproduce sexually, despite the automatic reproductive advantage experienced by asexual variants. This implies the operation of selective forces that confer an advantage to sexuality and genetic recombination, at either the population or individual level. The effect of sex and recombination in breaking down negative correlations between favorable variants at different genetic loci, which increases the efficiency of natural selection, is likely to be a major factor favoring their evolution and maintenance. Various processes that can cause such an effect have been studied theoretically. It has, however, so far proved hard to discriminate among them empirically.

Hybrids and hybrid zones: Reply from M.G. Ritchie and N.H. Barton - Ritchie, Mike; Barton, Nicholas H (Trends in Ecology and Evolution)

The geometry of adaptation - Barton, Nicholas H (Nature)

Genetics and analysis of quantitative traits - Barton, Nicholas H (Genetical Research)

An algorithm for the approximative analysis of rectangular automata - Preußig, Jörg; Kowalewski, Stefan; Wong Toi, Howard; Henzinger, Thomas A (Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems)
Rectangular automata are well suited for approximate modeling of continuous-discrete systems. The exact analysis of these automata is feasible for small examples but can encounter severe numerical problems for even medium-sized systems. This paper presents an analysis algorithm that uses conservative overapproximation to avoid these numerical problems. The algorithm is demonstrated on a simple benchmark system consisting of two connected tanks. Supported by the German Research Council (DFG) under grant Ko1430/3 in the special program KONDISK (‘Continuous-discrete dynamics of technical systems’).

Axioms for real-time logics - Raskin, Jean; Schobbens, Pierre; Henzinger, Thomas A (Proceedings of the 9th Interantional Conference on Concurrency Theory)
This paper presents a complete axiomatization of fully decidable propositional real-time linear temporal logics with past: the Event Clock Logic (ECL) and the Metric Interval Temporal Logic with past (MITL). The completeness proof consists of an effective proof building procedure for ECL. From this result we obtain a complete axiomatization of MITL by providing axioms translating MITL formulae into ECL formulae, the two logics being equally expressive. Our proof is structured to yield a similar axiomatization and procedure for interesting fragments of these logics, such as the linear temporal logic of the real numbers (LTR).

Reachability verification for hybrid automata - Henzinger, Thomas A; Rusu, Vlad (Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control)
We study the reachability problem for hybrid automata. Automatic approaches, which attempt to construct the reachable region by symbolic execution, often do not terminate. In these cases, we require the user to guess the reachable region, and we use a theorem prover (Pvs) to verify the guess. We classify hybrid automata according to the theory in which their reachable region can be defined finitely. This is the theory in which the prover needs to operate in order to verify the guess. The approach is interesting, because an appropriate guess can often be deduced by extrapolating from the first few steps of symbolic execution.

HSCC: Hybrid Systems—Computation and Control

An assume-guarantee rule for checking simulation - Henzinger, Thomas A; Qadeer, Shaz; Rajamani, Sriram; Tasiran, Serdar (Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design)
The simulation preorder on state transition systems is widely accepted as a useful notion of refinement, both in its own right and as an efficiently checkable sufficient condition for trace containment. For composite systems, due to the exponential explosion of the state space, there is a need for decomposing a simulation check of the form P< s Q into simpler simulation checks on the components of P and Q. We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q, we provide a procedure for constructing a witness relation for P< s Q. We also extend our assume-guarantee rule to account for fairness assumptions on transition systems

The regular real-time languages - Henzinger, Thomas A; Raskin, Jean; Schobbens, Pierre (Proceedings of the 25th International Colloqium on Automata, Languages and Programming)
A specification formalism for reactive systems defines a class of Ω-languages. We call a specification formalism fully decidable if it is constructively closed under boolean operations and has a decidable satisfiability (nonemptiness) problem. There are two important, robust classes of Ω-languages that are definable by fully decidable formalisms. The Ω -reqular languages are definable by finite automata, or equivalcntly, by the Sequential Calculus. The counter-free Ω-regular languages are definable by temporal logic, or equivalcntly, by the first-order fragment of the Sequential Calculus. The gap between both classes can be closed by finite counting (using automata connectives), or equivalently, by projection (existential second-order quantification over letters). A specification formalism for real-time systems defines a class of timed Ω-langnages, whose letters have real-numbered time stamps. Two popular ways of specifying timing constraints rely on the use of clocks, and on the use of time bounds for temporal operators. However, temporal logics with clocks or time bounds have undecidable satisfiability problems, and finite automata with clocks (so-called timed automata) are not closed under complement. Therefore, two fully decidable restrictions of these formalisms have been proposed. In the first case, clocks are restricted to event clocks, which measure distances to immediately preceding or succeeding events only. In the second case, time bounds are restricted to nonsingular intervals, which cannot specify the exact punctuality of events. We show that the resulting classes of timed Ω-languages are robust, and we explain their relationship. First, we show that temporal logic with event clocks defines the same class of timed Ω-languages as temporal logic with nonsingular time bounds, and we identify a first-order monadic theory that also defines this class. Second, we show that if the ability of finite counting is added to these formalisms, we obtain the class of timed Ω-languages that are definable by finite automata with event clocks, or equivalently, by a restricted second-order extension of the monadic theory. Third, we show that if projection is added, we obtain the class of timed Ω-languages that are definable by timed automata, or equivalently, by a richer second-order extension of the monadic theory. These results identify three robust classes of timed Ω-languages, of which the third, while popular, is not definable by a, fully decidable formalism. By contrast, the first two classes are definable by fully decidable formalisms from temporal logic, from automata theory, and from monadic logic. Since the gap between these two classes can be closed by finite counting, we dub them the timed Ω-regular languages and the timed counter-free Ω-rcgular languages, respectively.

From pre-historic to post-modern symbolic model checking - Henzinger, Thomas A; Kupferman, Orna; Qadeer, Shaz (Proceedings of the 10th International Conference on Computer Aided Verification)
Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating with expressions that represent state sets. Traditionally, symbolic model-checking tools arc based on backward state traversal; their basic operation is the function pre, which given a set of states, returns the set of all predecessor states. This is because specifiers usally employ formalisms with future-time modalities. which are naturally evaluated by iterating applications of pre. It has been recently shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only those parts of the state space are explored which are reachable from an initial state and relevant for satisfaction or violation of the specification; that is, errors can be detected as soon as possible. In this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two -calculi. The pre- calculus is based on the pre operation; the post- calculus, on the post operation. These two -calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all -regular (linear-time) specifications can be expressed as post- queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way.

You assume, we guarantee: Methodology and case studies - Henzinger, Thomas A; Qadeer, Shaz; Rajamani, Sriram (Proceedings of the 10th International Conference on Computer Aided Verification)
Assume-guarantee reasoning has long been advertised as an important method for decomposing proof obligations in system verification. Refinement mappings (homomorphisms) have long been advertised as an important method for solving the language-inclusion problem in practice. When confronted with large verification problems, we therefore attempted to make use of both techniques. We soon found that rather than offering instant solutions, the success of assume-guarantee reasoning depends critically on the construction of suitable abstraction modules, and the success of refinement checking depends critically on the construction of suitable witness modules. Moreover, as abstractions need to be witnessed, and witnesses abstracted, the process must be iterated. We present here the main lessons we learned from our experiments, in limn of a systematic and structured discipline for the compositional verification of reactive modules. An infrastructure to support this discipline, and automate parts of the verification, has been implemented in the tool Mocha.

Algorithmic analysis of nonlinear hybrid systems - Henzinger, Thomas A; Ho, Pei; Wong Toi, Howard (IEEE Transactions on Automatic Control)
We present two methods for translating nonlinear hybrid systems into linear hybrid automata. Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated linear hybrid automata. The first method, called clock translation, replaces constraints on nonlinear variables by constraints on clock variables. The second method, called linear phase-portrait approximation, conservatively overapproximates the phase portrait of a hybrid automaton using piecewise-constant polyhedral differential inclusions. Both methods are sound for safety properties. We illustrate both methods by using HYTECH, a symbolic model checker for linear hybrid automata, to automatically check properties of a nonlinear temperature controller and of a predator-prey ecology

What's decidable about hybrid automata? - Henzinger, Thomas A; Kopke, Peter; Puri, Anuj; Varaiya, P. (Journal of Computer and System Sciences)
Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify a boundary between decidability and undecidability for the reachability problem of hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow independent trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves theω-languages of initialized rectangular automata with bounded nondeterminism. On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch.

It's about time: Real-time logics reviewed - Henzinger, Thomas A (Proceedings of the 9th Interantional Conference on Concurrency Theory)
We summarize and reorganize some of the last decade's research on real-time extensions of temporal logic. Our main focus is on tableau constructions for model checking linear temporal formulas with timing constraints. In particular, we find that a great deal of real-time verification can be performed in polynomial space, but also that considerable care must be exercised in order to keep the real-time verification problem in polynomial space, or even decidable.

Symbolic exploration of transition hierarchies - Alur, Rajeev; Henzinger, Thomas A; Rajamani, Sriram (Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems)
In formal design verification, successful model checking is typically preceded by a laborious manual process of constructing design abstractions. We present a methodology for partially—and in some cases, fully—bypassing the abstraction process. For this purpose, we provide to the designer abstraction operators which, if used judiciously in the description of a design, structure the corresponding state space hierarchically. This structure can then be exploited by verification tools, and makes possible the automatic and exhaustive exploration of state spaces that would otherwise be out of scope for existing model checkers. Specifically, we present the following contributions: - A temporal abstraction operator that aggregates transitions and hides intermediate steps. Mathematically, our abstraction operator is a function that maps a flat transition system into a two-level hierarchy where each atomic upper-level transition expands into an entire lower-level transition system. For example, an arithmetic operation may expand into a sequence of bit operations. - A BDD-based algorithm for the symbolic exploration of multi-level hierarchies of transition systems. The algorithm traverses a level-n transition by expanding the corresponding level-(n − 1) transition system on-the-fly. The level-n successors of a state are determined by computing a level-(n − 1) reach set, which is then immediately released from memory. In this fashion, we can exhaustively explore hierarchically structured state spaces whose flat counterparts cause memory overflows. - We experimentally demonstrate the efficiency of our method with three examples—a multiplier, a cache coherence protocol, and a multiprocessor system. In the first two examples, we obtain significant improvements in run times and peak BDD sizes over traditional state-space search. The third example cannot be model checked at all using conventional methods (without manual abstractions), but can be analyzed fully automatically using transition hierarchies.

Alternating refinement relations - Alur, Rajeev; Henzinger, Thomas A; Kupferman, Orna; Vardi, Moshe (Proceedings of the 9th Interantional Conference on Concurrency Theory)
Alternating transition systems are a general model for composite systems which allow the study of collaborative as well as adversarial relationships between individual system components. Unlike in labeled transition systems, where each transition corresponds to a possible step of the system (which may involve some or all components), in alternating transition systems, each transition corresponds to a possible move in a game between the components. In this paper, we study refinement relations between alternating transition systems, such as “Does the implementation refine the set A of specification components without constraining the components not in A?” In particular, we generalize the definitions of the simulation and trace containment preorders from labeled transition systems to alternating transition systems. The generalizations are called alternating simulation and alternating trace containment. Unlike existing refinement relations, they allow the refinement of individual components within the context of a composite system description. We show that, like ordinary simulation, alternating simulation can be checked in polynomial time using a fixpoint computation algorithm. While ordinary trace containment is PSPACE-complete, we establish alternating trace containment to be EXPTIME-complete. Finally, we present logical characterizations for the two preorders in terms of ATL, a temporal logic capable of referring to games between system components.

Mocha: Modularity in model checking - Alur, Rajeev; Henzinger, Thomas A; Mang, Freddy; Qadeer, Shaz; Rajamani, Sriram; Tasiran, Serdar (Proceedings of the 10th International Conference on Computer Aided Verification)

Concurrent reachability games - De Alfaro, Luca; Henzinger, Thomas A; Kupferman, Orna (Proceedings 39th Annual Symposium on Foundations of Computer Science)
An open system can be modeled as a two-player game between the system and its environment. At each round of the game, player 1 (the system) and player 2 (the environment) independently and simultaneously choose moves, and the two choices determine the next state of the game. Properties of open systems can be modeled as objectives of these two-player games. For the basic objective of reachability-can player 1 force the game to a given set of target states?-there are three types of winning states, according to the degree of certainty with which player 1 can reach the target. From type-1 states, player 1 has a deterministic strategy to always reach the target. From type-2 states, player 1 has a randomized strategy to reach the target with probability 1. From type-3 states, player 1 has for every real ε>0 a randomized strategy to reach the target with probability greater than 1-ε. We show that for finite state spaces, all three sets of winning states can be computed in polynomial time: type-1 states in linear time, and type-2 and type-3 states in quadratic time. The algorithms to compute the three sets of winning states also enable the construction of the winning and spoiling strategies. Finally, we apply our results by introducing a temporal logic in which all three kinds of winning conditions can be specified, and which can be model checked in polynomial time. This logic, called Randomized ATL, is suitable for reasoning about randomized behavior in open (two-agent) as well as multi-agent systems

Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans - de Bono, Mario; Bargmann, Cornelia I (Cell)
Natural isolates of C. elegans exhibit either solitary or social feeding behavior. Solitary foragers move slowly on a bacterial lawn and disperse across it, while social foragers move rapidly on bacteria and aggregate together. A loss-of-function mutation in the npr-1 gene, which encodes a predicted G protein–coupled receptor similar to neuropeptide Y receptors, causes a solitary strain to take on social behavior. Two isoforms of NPR-1 that differ at a single residue occur in the wild. One isoform, NPR-1 215F, is found exclusively in social strains, while the other isoform, NPR-1 215V, is found exclusively in solitary strains. An NPR-1 215V transgene can induce solitary feeding behavior in a wild social strain. Thus, isoforms of a putative neuropeptide receptor generate natural variation in C. elegans feeding behavior.