TY - CONF
AB - 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.
AU - Herbert Edelsbrunner
ID - 4015
TI - Shape reconstruction with Delaunay complex
VL - 1380
ER -
TY - CONF
AB - 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.
AU - Herbert Edelsbrunner
AU - Facello, Michael A
AU - Fu, Ping
AU - Qian, Jiang
AU - Nekhayev, Dmitry V
ID - 4016
TI - Wrapping 3D scanning data
VL - 3313
ER -
TY - JOUR
AB - 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.
AU - Liang, Jie
AU - Herbert Edelsbrunner
AU - Woodward, Clare K
ID - 4017
IS - 9
JF - Protein Science
TI - Anatomy of protein pockets and cavities: Measurement of binding site geometry and implications for ligand design
VL - 7
ER -
TY - CONF
AB - 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.
AU - Cheng, Ho-Lun
AU - Herbert Edelsbrunner
AU - Fu, Ping
ID - 4019
TI - Shape space from deformation
ER -
TY - CHAP
AB - 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.
AU - Herbert Edelsbrunner
ID - 4020
T2 - Robotics: The Algorithmic Perspective
TI - Geometry for modeling biomolecules
ER -
TY - JOUR
AU - Ritchie, Mike
AU - Nicholas Barton
ID - 4280
IS - 7
JF - Trends in Ecology and Evolution
TI - Hybrids and hybrid zones: Reply from M.G. Ritchie and N.H. Barton
VL - 13
ER -
TY - JOUR
AB - 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.
AU - Barton, Nicholas H
AU - Charlesworth, Brian
ID - 4281
IS - 5385
JF - Science
TI - Why sex and recombination?
VL - 281
ER -
TY - GEN
AU - Nicholas Barton
ID - 4282
IS - 1
T2 - Genetical Research
TI - Genetics and analysis of quantitative traits
VL - 72
ER -
TY - GEN
AU - Nicholas Barton
ID - 4283
IS - 6704
T2 - Nature
TI - The geometry of adaptation
VL - 395
ER -
TY - CONF
AB - 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).
AU - Raskin, Jean-François
AU - Schobbens, Pierre Y
AU - Thomas Henzinger
ID - 4408
TI - Axioms for real-time logics
VL - 1466
ER -
TY - CONF
AB - 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’).
AU - Preußig, Jörg
AU - Kowalewski, Stefan
AU - Wong-Toi, Howard
AU - Thomas Henzinger
ID - 4410
TI - An algorithm for the approximative analysis of rectangular automata
VL - 1486
ER -
TY - CONF
AB - 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.
AU - Thomas Henzinger
AU - Rusu,Vlad
ID - 4429
TI - Reachability verification for hybrid automata
VL - 1386
ER -
TY - GEN
AU - Thomas Henzinger
AU - Sastry, Shankar
ID - 4430
T2 - HSCC: Hybrid Systems - Computation and Control
TI - HSCC: Hybrid Systems—Computation and Control
VL - 1386
ER -
TY - CONF
AB - 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
AU - Thomas Henzinger
AU - Qadeer,Shaz
AU - Rajamani, Sriram K
AU - Tasiran, Serdar
ID - 4486
TI - An assume-guarantee rule for checking simulation
VL - 1522
ER -
TY - CONF
AB - 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.
AU - Thomas Henzinger
AU - Qadeer,Shaz
AU - Rajamani, Sriram K
ID - 4488
TI - You assume, we guarantee: Methodology and case studies
VL - 1427
ER -
TY - CONF
AB - 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.
AU - Thomas Henzinger
AU - Kupferman, Orna
AU - Qadeer,Shaz
ID - 4489
TI - From pre-historic to post-modern symbolic model checking
VL - 1427
ER -
TY - CONF
AB - 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.
AU - Thomas Henzinger
AU - Raskin, Jean-François
AU - Schobbens, Pierre Y
ID - 4490
TI - The regular real-time languages
VL - 1443
ER -
TY - JOUR
AB - 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
AU - Thomas Henzinger
AU - Ho, Pei-Hsin
AU - Wong-Toi, Howard
ID - 4491
IS - 4
JF - IEEE Transactions on Automatic Control
TI - Algorithmic analysis of nonlinear hybrid systems
VL - 43
ER -
TY - JOUR
AB - 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.
AU - Thomas Henzinger
AU - Kopke, Peter W
AU - Puri, Anuj
AU - Varaiya,P.
ID - 4492
IS - 1
JF - Journal of Computer and System Sciences
TI - What's decidable about hybrid automata?
VL - 57
ER -
TY - CONF
AB - 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.
AU - Thomas Henzinger
ID - 4515
TI - It's about time: Real-time logics reviewed
VL - 1466
ER -
TY - JOUR
AB - 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.
AU - Peter Jonas
AU - Bischofberger, Joseph
AU - Sandkühler, Jürgen
ID - 3487
IS - 5375
JF - Science
TI - Corelease of two fast neurotransmitters at a central synapse
VL - 281
ER -
TY - JOUR
AB - 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.
AU - Martina, Marco
AU - Schultz, Jobst Hendrik
AU - Ehmke, Heimo
AU - Monyer, Hannah
AU - Peter Jonas
ID - 3488
IS - 20
JF - Journal of Neuroscience
TI - Functional and molecular differences between voltage-gated K+ channels of fast-spiking interneurons and pyramidal neurons of rat hippocampus
VL - 18
ER -
TY - GEN
AB - 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.
AU - Herbert Edelsbrunner
AU - Fu, Ping
ID - 3506
TI - Apparatus and method for geometric morphing
ER -
TY - JOUR
AB - 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.
AU - Jozsef Csicsvari
AU - Hirase, Hajima
AU - Czurkó, András
AU - Buzsáki, György
ID - 3521
IS - 1
JF - Neuron
TI - Reliability and state dependence of pyramidal cell-interneuron synapses in the hippocampus: an ensemble approach in the behaving rat
VL - 21
ER -
TY - JOUR
AU - Nádasdy, Zoltán
AU - Jozsef Csicsvari
AU - Hirase, Hajima
AU - Czurkó, András
AU - Buzsáki, György
ID - 3525
IS - Suppl. 10
JF - European Journal of Neuroscience
TI - Persistence and temporal compression of spike sequences during fast field oscillation in the hippocampus
VL - 10
ER -
TY - JOUR
AU - Jozsef Csicsvari
AU - Czurkó, András
AU - Hirase, Hajima
AU - Buzsáki, György
ID - 3527
IS - Suppl. 10
JF - European Journal of Neuroscience
TI - Monosynaptic interactions between CA1 Pyramidal cells and interneuron in the behaving rat
VL - 10
ER -
TY - JOUR
AU - Hirase, Hajima
AU - Czurkó, András
AU - Jozsef Csicsvari
AU - Buzsáki, György
ID - 3535
IS - Suppl. 10
JF - European Journal of Neuroscience
TI - Hippocampal pyramidal neutrons “space-clamped” in a running wheel task: Place cells or path integrators?
VL - 10
ER -
TY - CHAP
AB - 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.
AU - Axen, Ulrike
AU - Herbert Edelsbrunner
ID - 3570
T2 - Mathematical Visualization
TI - Auditory Morse analysis of triangulated manifolds
ER -
TY - JOUR
AB - 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.
AU - Nicholas Barton
ID - 3627
IS - 2
JF - Genetical Research
TI - The effect of hitch-hiking on neutral genealogies
VL - 72
ER -
TY - JOUR
AB - 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.
AU - West, Stuart A
AU - Peters, Andrew D
AU - Nicholas Barton
ID - 3628
IS - 1
JF - Genetics
TI - Testing for epistasis between deleterious mutations
VL - 149
ER -
TY - JOUR
AB - 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.
AU - MacCallum, Catriona J
AU - Nürnberger, Beate
AU - Nicholas Barton
AU - Szymura, Jacek M
ID - 3629
IS - 1
JF - Evolution
TI - Habitat preference in the Bombina hybrid zone in Croatia
VL - 52
ER -
TY - JOUR
AB - A specific antiserum against substance P receptor (SPR) labels nonprincipal neurons in the cerebral cortex of the rat (T. Kaneko et al. [1994], Neuroscience 60:199-211; Y. Nakaya et al. [1994], J. Comp. Neurol. 347:249-274). In the present study, we aimed to identify the types of SPR- immunoreactive neurons in the hippocampus according to their content of neurochemical markers, which label interneuron populations with distinct termination patterns. Markers for perisomatic inhibitory cells, parvalbumin and cholecystokinin (CCK), colocalized with SPR in pyramidallike basket cells in the dentate gyrus and in large multipolar or bitufted cells within all hippocampal subfields respectively. A dense meshwork of SPR-immunoreactive spiny dendrites in the hilus and stratum lucidum of the CA3 region belonged largely to inhibitory cells terminating in the distal dendritic region of granule cells, as indicated by the somatostatin and neuropeptide Y (NPY) content. In addition, SPR and NPY were colocalized in numerous multipolar interneurons with dendrites branching close to the soma. Twenty-five percent of the SPR-immunoreactive cells overlapped with calretinin-positive neurons in all hippocampal subfields, showing that interneurons specialized to contact other gamma-aminobutyric acid-ergic cells may also contain SPR. On the basis of the known termination pattern of the colocalized markers, we conclude that SPR-positive interneurons are functionally heterogeneous and participate in different inhibitory processes: (1) perisomatic inhibition of principal cells (CCK-containing cells, and parvalbumin-positive cells in the dentate gyrus), (2) feedback dendritic inhibition in the entorhinal termination zone (somatostatin and NPY-containing cells), and (3) innervation of other interneurons (calretinin-containing cells).
AU - Acsády, László
AU - Katona, István
AU - Gulyás, Attila I
AU - Ryuichi Shigemoto
AU - Freund, Tamás F
ID - 2493
IS - 3
JF - Journal of Comparative Neurology
TI - Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus
VL - 378
ER -
TY - JOUR
AB - It was examined electron microscopically in the rat if a metabotropic glutamate receptor, mGluR7, might be localized in axon terminals of nociceptive, primary afferent fibers in laminae I and II of the spinal dorsal horn. Nociceptive nature of axon terminals showing mGluR7-like immunoreactivity (mGluR7-LI) was indicated by binding to the isolectin I-B4 from Griffonia simplicifolia (I-B4), or by substance P-like immunoreactivity (SP-LI). Axon terminals labeled with immunogold particles indicating mGluR7-LI were usually filled with round synaptic vesicles and were in asymmetric synaptic contact with dendritic or somatic profiles; occasionally they contained pleomorphic vesicles and were in symmetric synaptic contact with somatic profiles in lamina II. The double-labeling studies revealed that most of axon terminals with I-B4 labeling as well as a small population of axon terminals with SP-LI, showed mGluR7-LI. About one-third or much smaller population of axon terminals with mGluR7-LI in laminae I and II were labeled, respectively, with I-B4 or SP-LI; these were in asymmetric synaptic contact with dendritic profiles.
AU - Li, He
AU - Ohishi, Hitoshi
AU - Kinoshita, Ayae
AU - Ryuichi Shigemoto
AU - Nomura, Sakashi
AU - Mizuno, Noboru
ID - 2575
IS - 3
JF - Neuroscience Letters
TI - Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat
VL - 223
ER -
TY - JOUR
AB - Primary afferent neurons containing substance P (SP) are apparently implicated in the transmission of noxious information from the periphery to the central nervous system, and SP released from primary afferent neurons acts on second-order neurons with the SP receptor (SPR). In the rat, nociceptive information reached the hypothalamus not only through indirect pathways but also directly through trigeminohypothalamic and spinohypothalamic pathways. Thus, in the present study, the distribution pattern of trigeminohypothalamic and spinohypothalamic tract neurons showing SPR-like immunoreactivity (SPR-LI) was examined in the rat by a retrograde tract-tracing method combined with immunofluorescence histochemistry for SPR. A substantial number of trigeminal and spinal neurons with SPR-LI were retrogradely labeled with Fluore-Gold (FG) injected into the hypothalamic regions. These neurons were distributed mainly in lamina I of the medullary and spinal dorsal horns, lateral spinal nucleus, regions around the central canal of the spinal cord, and the lateral aspect of the deep part of the spinal dorsal horn. A number of SPR-LI neurons in the spinal parasympathetic nucleus were labeled with FG injected into the area around the paraventricular hypothalamic nucleus. Some SPR-LI neurons in the lateral spinal nucleus and the lateral aspect of the deep part of the spinal dorsal horn were also labeled with FG injected into the septal region. On the basis of the distribution areas of SPR-LI trigeminal and spinal neurons projecting to the hypothalamic and septal regions, it is likely that these neurons are involved in the transmission of somatic and/or visceral noxious information.
AU - Li, Jin-Lian
AU - Kaneko, Takeshi
AU - Ryuichi Shigemoto
AU - Mizuno, Noboru
ID - 2576
IS - 4
JF - Journal of Comparative Neurology
TI - Distribution of trigeminohypothalamic and spinohypothalamic tract neurons displaying substance P receptor-like immunoreactivity in the rat
VL - 378
ER -
TY - JOUR
AB - The cloned cDNA for rat prostacyclin synthase was found to contain a 1503-bp open reading frame which encoded a 501-amino acid protein sharing 84% identity with the human enzyme. RNA blot analysis revealed that the rat prostacyclin synthase mRNA, as a single species of 2.1 kb, is expressed abundantly in the aorta and uterus. High levels of expression were also observed in the stomach, lung, heart, testis, liver, and skeletal muscle. Low but significant expression was also seen in the brain and kidney. Furthermore, the regional distribution and cellular localization of prostacyclin synthase mRNA were examined by in situ hybridization analysis of rat tissue sections. The definitive signals for the mRNA were localized in smooth muscle cells of the arteries, bronchi and uterus, and in the cells of the fibrous tunic surrounding the seminiferous tubules, which are characterized as smooth muscle cells. Besides smooth muscle cells, signal were also detected in the fibroblasts of the heart myocardium, lung parenchyma cells and kidney inner medulla tubules and interstitial cells.
AU - Tone, Yoshinori
AU - Inoue, Hiroyasu
AU - Hara, Shuntaro
AU - Yokoyama, Chieko
AU - Hatae, Toshihisa
AU - Oida, Hiroji
AU - Narumiya, Shuh
AU - Ryuichi Shigemoto
AU - Yukawa, Susumu
AU - Tanabe, Tadashi
ID - 2577
IS - 3
JF - European Journal of Cell Biology
TI - The regional distribution and cellular localization of mRNA encoding rat prostacyclin synthase
VL - 72
ER -
TY - JOUR
AB - The distribution of immunoreactivity to the neurokinin3 receptor (NK3R) was examined in segments C7, T11-12, L1-2, and L4-6 of the rat spinal cord. NK3R immunoreactivity was visualized by using two antisera generated against sequences of amino acids contained in the C-terminal region of the NK3R. NK3R-immunoreactive cells were numerous in the substantia gelatinosa of all spinal segments examined as well as the dorsal commissural nucleus of spinal segments L1-2. Isolated, immunoreactive cells were scattered throughout other regions of the spinal cord. The relationship of NK3R-immunoreactivity with neurons was demonstrated by colocalization with microtubule associated protein 2-immunoreactivity in individual cells. Within neurons, NK3R- immunoreactivity was associated predominately with the plasma membrane of cell bodies and dendrites. Within the substantia gelatinosa, 86% of nitric oxide synthase (NOS)-immunoreactive neurons were also NK3R-immunoreactive. Although NOS-immunoreactive neurons were found throughout all other regions of the spinal cord in the segments examined, these were not NK3R- immunoreactive. When preganglionic sympathetic neurons in spinal segments T11-12 and L1-2 were visualized by intraperitoneal injection of Fluorogold, less than 1% of the Fluorogold-labeled neurons were also immunoreactive for NK3R. The large number of NK3R-immunoreactive neurons in the substantia gelatinosa suggests that some effects of tachykinins an somatosensation may be mediated by NK3R.
AU - Seybold, Virginia S
AU - Grković, Ivica
AU - Portbury, Andrea L
AU - Ding, Yu-Qiang
AU - Ryuichi Shigemoto
AU - Mizuno, Noboru
AU - Furness, John B
AU - Southwell, Bridget R
ID - 2578
IS - 4
JF - Journal of Comparative Neurology
TI - Relationship of NK3 receptor-immunoreactivity to subpopulations of neurons in rat spinal cord
VL - 381
ER -
TY - JOUR
AB - The localisation of the neurokinin 3 receptor (NK3r) in the rat gastrointestinal tract has been studied by using a polyclonal antiserum against the C-terminal portion (amino acids 388-452) of the rat NK3r. In the oesophagus, immunoreactivity for the NK3r was found on smooth muscle cells of the muscularis mucosae. NK3r immunoreactivity was not present on muscle cells of other regions. Nerve cell bodies immunoreactive for NK3r were seen in the myenteric and submucous plexuses of the small and large intestine, but not in the stomach or oesophagus. Immunoreactivity was largely confined to nerve cell surfaces. The reaction product was on the cell soma and initial parts of axons. Reactivity was not seen on nerve terminals. Immunoreactive nerve cells had Dogiel Type II morphology. Patterns of co-localisation of NK3r and immunoreactivity for other markers were examined in the ileum, to provide a basis from which to deduce the functional identity of NK3r-immunoreactive nerve cells. Most of the NK3r-immunoreactive nerve cells were also immunoreactive for the calcium-binding proteins, calretinin and calbindin, and all were immunoreactive for the NK1 receptor (NK1r). Nerve cells that were immunoreactive for nitric oxide synthase were not immunoreactive for either NK3r or NK1r. The projections of the calbindin and calretinin neurons were determined by nerve lesion studies. Their morphology, projections to the mucosa and other ganglia and immunoreactivity for the calcium-binding proteins suggest that the NK3r-immunoreactive neurons are intrinsic sensory neurons.
AU - Mann, Patricia T
AU - Southwell, Bridget R
AU - Ding, Yu-Qiang
AU - Ryuichi Shigemoto
AU - Mizuno, Noboru
AU - Furness, John B
ID - 2579
IS - 1
JF - Cell and Tissue Research
TI - Localisation of neurokinin 3 (NK3) receptor immunoreactivity in the rat gastrointestinal tract
VL - 289
ER -
TY - JOUR
AB - Two group I metabotropic glutamate receptor subtypes, mGluR1 and mGluR5, have been reported to occur in highest concentration in an annulus surrounding the edge of the postsynaptic membrane specialisation. In order to determine whether such a distribution is uniform amongst postsynaptic mGluRs, their distribution was compared quantitatively by a pre-embedding silver-intensified immunogold technique at electron microscopic level in hippocampal pyramidal cells (mGluR5), cerebellar Purkinje cells (mGluR1α) and Golgi cells (mGluR2). The results show that mGluR1α, mGluR5 and mGluR2 each have a distinct distribution in relation to the glutamatergic synaptic junctions. On dendritic spines, mGluRlα and mGluR5 showed the highest receptor density in a perisynaptic annulus (defined as within 60 nm of the edge of the synapse) followed by a decreasing extrasynaptic (60-900 nm) receptor level, but the gradient of decrease and the proportion of the perisynaptic pool (mGluR1α, ~ 50%; vs mGluR5, ~ 25%) were different for the two receptors. The distributions of mGluRlα and mGluR5 also differed significantly from simulated random distributions. In contrast, mGluR2 was not closely associated with glutamatergic synapses in the dendritic plasma membrane of cerebellar Golgi cells and its distribution relative to synapses is not different from simulated random distribution in the membrane. The somatic membrane, the axon and the synaptic boutons of the GABAergic Golgi cells also contained immunoreactive mGluR2 that is not associated with synaptic specialisations. In the hippocampal CA1 area the distribution of immunoparticles for mGluR5 on individual spines was established using serial sections. The results indicate that dendritic spines of pyramidal cells are heterogeneous with respect to the ratio of perisynaptic to extrasynaptic mGluR5 pools and about half of the immunopositive spines lack the perisynaptic pool. The quantitative comparison of receptor distributions demonstrates that mGluRlα and mGluR5, but not mGluR2, are highly compartmentalised in different plasma membrane domains. The unique distribution of each mGluR subtype may reflect requirements for different transduction and effector mechanisms between cell types and different domains of the same cell, and suggests that the precise placement of receptors is a crucial factor contributing to neuronal communication.
AU - Luján, Rafael
AU - Roberts, John D
AU - Ryuichi Shigemoto
AU - Ohishi, Hitoshi
AU - Somogyi, Péter
ID - 2580
IS - 4
JF - Journal of Chemical Neuroanatomy
TI - Differential plasma membrane distribution of metabotropic glutamate receptors mGluR1α, mGluR2 and mGluR5, relative to neurotransmitter release sites
VL - 13
ER -
TY - JOUR
AB - It is well known that striatonigral neurons produce substance P (SP); however, no SP receptor (SPR) has so far been found in the substantia nigra. On the other hand, a previous study in the rat striatum indicated that SPR was expressed only in cholinergic or somatostatinergic intrinsic neurons (Kaneko et al. [1993] Brain Res. 631:297-303). Thus, it was assumed that SP produced by striatenigral neurons might be released through their intrastriatal axon collaterals to act upon intrinsic neurons in the striatum. To confirm this assumption, the distribution of axon collaterals of striatonigral neurons was examined in the striatum of the rat. The experiments were performed on brain slices by combining retrograde labeling with tetramethylrhodamine-dextran amine, electrophysiological recording, intracellular staining with biocytin, and immunocytochemistry for SPR. The distribution of axons of cholinergic striatal neurons (a group of SP-negative intrinsic striatal neurons) was also examined. It was observed that 16% of varicosities of intrastriatal axon collaterals of striatonigral neurons, as well as 6% of axonal varicosities of cholinergic neurons, were in close apposition to dendrites and cell bodies of SPB-immunoreactive striatal neurons. Since SPR-immunoreactive striatal neurons constituted only 2.7% of the total population of striatal neurons (Kaneko et al. [1993] Brain Res. 631:297-303), it appeared that axonal varicosities of striatonigral neurons were preferentially apposed to SPR-immunoreactive striatal neurons and that the varicosities in close apposition to SPR-immunoreactive neurons were derived more frequently from striatonigral neurons than from cholinergic interneurons. Confocal laser scanning microscopy indicated that axonal varicosities in close apposition to SPR-immunoreactive cells showed synaptophysin immunoreactivity, a marker of synaptic vesicles. In intrastriatal axons of striatonigral neurons, it was further revealed from electron microscopy that axonal varicosities in close apposition to SPR- immunoreactive dendrites, at least a part of them, made synapses of the symmetric type. Striatonigral neurons might release SP preferentially around cholinergic or somatostatinergic intrinsic neurons to regulate them through SP-SPR interactions.
AU - Lee, Teffy
AU - Kaneko, Takeshi
AU - Ryuichi Shigemoto
AU - Nomura, Sakashi
AU - Mizuno, Noboru
ID - 2581
IS - 2
JF - Journal of Comparative Neurology
TI - Collateral projections from striatonigral neurons to substance P receptor-expressing intrinsic neurons in the striatum of the rat
VL - 388
ER -
TY - JOUR
AB - Neurotransmission in the hippocampus is modulated variously through presynaptic metabotropic glutamate receptors (mGluRs). To establish the precise localization of presynaptic mGluRs in the rat hippocampus, we used subtype-specific antibodies for eight mGluRs (mGluR1-mGluR8) for immunohistochemistry combined with lesioning of the three major hippocampal pathways: the perforant path, mossy fiber, and Schaffer collateral. Immunoreactivity for group II (mGluR2) and group III (mGluR4a, mGluR7a, mGluR7b, and mGluR8) mGluRs was predominantly localized to presynaptic elements, whereas that for group I mGluRs (mGluR1 and mGluR5) was localized to postsynaptic elements. The medial perforant path was strongly immunoreactive for mGluR2 and mGluR7a throughout the hippocampus, and the lateral perforant path was prominently immunoreactive for mGluR8 in the dentate gyrus and CA3 area. The messy fiber was labeled for mGluR2, mGluR7a, and mGluR7b, whereas the Schaffer collateral was labeled only for mGluR7a. Electron microscopy further revealed the spatial segregation of group II and group III mGluRs within presynaptic elements. Immunolabeling for the group III receptors was predominantly observed in presynaptic active zones of asymmetrical and symmetrical synapses, whereas that for the group II receptor (mGluR2) was found in preterminal rather than terminal portions of axons. Target cell-specific segregation of receptors, first reported for mGluR7a (Shigemoto et al., 1996), was also apparent for the other group III mGluRs, suggesting that transmitter release is differentially regulated by 2-amino- 4-phosphonobutyrate-sensitive mGluRs in individual synapses on single axons according to the identity of postsynaptic neurons.
AU - Ryuichi Shigemoto
AU - Kinoshita, Ayae
AU - Wada, Eiki
AU - Nomura, Sakashi
AU - Ohishi, Hitoshi
AU - Takada, Masahiko
AU - Flor, Peter J
AU - Neki, Akio
AU - Abe, Takaaki
AU - Nakanishi, Shigetada
AU - Mizuno, Noboru
ID - 2582
IS - 19
JF - Journal of Neuroscience
TI - Differential presynaptic localization of metabotropic glutamate receptor subtypes in the rat hippocampus
VL - 17
ER -
TY - JOUR
AB - Diamagnetism of the magnetic Schrödinger operator and paramagnetism of the Pauli operator are rigorously proven for nonhomogeneous magnetic fields in the large field, in the large temperature and in the semiclassical asymptotic regimes. New counterexamples are presented which show that neither dia-nor paramagnetism is true in a robust sense (without asymptotics). In particular, we demonstrate that the recent diamagnetic comparison result by Loss and Thaller [M. Loss and B. Thaller, Commun. Math. Phys. (submitted)] is essentially the best one can hope for.
AU - László Erdös
ID - 2727
IS - 3
JF - Journal of Mathematical Physics
TI - Dia- and paramagnetism for nonhomogeneous magnetic fields
VL - 38
ER -
TY - JOUR
AB - We give the leading order semiclassical asymptotics for the sum of the negative eigenvalues of the Pauli operator (in dimension two and three) with a strong non-homogeneous magnetic field. As in [LSY-II] for homogeneous field, this result can be used to prove that the magnetic Thomas-Fermi theory gives the leading order ground state energy of large atoms. We develop a new localization scheme well suited to the anisotropic character of the strong magnetic field. We also use the basic Lieb-Thirring estimate obtained in our companion paper [ES-I].
AU - László Erdös
AU - Solovej, Jan P
ID - 2729
IS - 3
JF - Communications in Mathematical Physics
TI - Semiclassical eigenvalue estimates for the Pauli operator with strong non-homogeneous magnetic fields, II. Leading order asymptotic estimates
VL - 188
ER -
TY - JOUR
AB - We introduce a new potential-theoretic definition of the dimension spectrum of a probability measure for q > 1 and explain its relation to prior definitions. We apply this definition to prove that if and is a Borel probability measure with compact support in , then under almost every linear transformation from to , the q-dimension of the image of is ; in particular, the q-dimension of is preserved provided . We also present results on the preservation of information dimension and pointwise dimension. Finally, for and q > 2 we give examples for which is not preserved by any linear transformation into . All results for typical linear transformations are also proved for typical (in the sense of prevalence) continuously differentiable functions.
AU - Hunt, Brian R
AU - Kaloshin, Vadim
ID - 8527
IS - 5
JF - Nonlinearity
KW - Mathematical Physics
KW - General Physics and Astronomy
KW - Applied Mathematics
KW - Statistical and Nonlinear Physics
SN - 0951-7715
TI - How projections affect the dimension spectrum of fractal measures
VL - 10
ER -
TY - JOUR
AB - In the present paper, we give a definition of prevalent ("metrically prevalent" ) sets in nonlinear function
spaces. A subset of a Euclidean space is said to be metrically prevalent if its complement has measure zero.
There is no natural way to generalize the definition of a set of measure zero in a finite-dimensional space
to the infinite-dimensional case [6]. Therefore, it is necessary to give a special definition of a metrically
prevalent set (set of full measure) in an infinite-dimensional space. There are various ways to do so. We
suggest one of the possible ways to define the class of metrically prevalent sets in the space of smooth maps
of one smooth manifold into another. It is shown in this paper that the class of metrically prevalent sets
has natural properties; in particular, the intersection of finitely many metrically prevalent sets is metrically
prevalent. The main result of the paper is a prevalent version of Thorn's transversality theorem.
It is common practice in singularity theory and the theory of dynamical systems to say that a property
holds for "almost every" map (or flow) if it holds for a residual set, i.e., a set that contains a countable
intersection of open dense sets in the corresponding function space. However, even in finite-dimensional
spaces such a set can have arbitrarily small (say, zero) Lebesgue measure. We prove that Thorn's transversality theorem holds for an essentially "thicker" set than a residual set. It seems reasonable to revise from
the prevalent point of view the classical results of singularity theory and theory of dynamical systems,
including the multijet transversality theorem, Mather's stability theorem, Kupka-Smale's theorem for dynamical systems, etc. We shall do this elsewhere. The notion of prevalence in linear Banach spaces was
introduced and investigated in [8]. One of the possible ways to define a class of prevalent sets in the space
of smooth maps of manifolds, which essentially differs from that presented in this paper, is given in [7].
Definitions of typicalness based on the Lebesgue measure in a finite-dimensional space were suggested
by Kolmogorov [10] and Arnold [11]. These definitions were cited and discussed in [9]. Here we only point
out that the finite-dimensional analog of Arnold's definition allows prevalent sets to have arbitrarily small
measure, whereas the prevalent sets in the sense of the finite-dimensional analog of the definition given in
the present paper are necessarily of full measure. Our definition is a modification of that due to Arnold.
I wish to thank Yu. S. Illyashenko for constant attention to this work and useful discussions and
R. I. Bogdanov for help in the preparation of this paper.
AU - Kaloshin, Vadim
ID - 8528
IS - 2
JF - Functional Analysis and Its Applications
KW - Applied Mathematics
KW - Analysis
SN - 0016-2663
TI - Prevalence in the space of finitely smooth maps
VL - 31
ER -
TY - CONF
AB - A hybrid system is a dynamical system whose behavior exhibits both discrete and continuous change. A hybrid automaton is a mathematical model for hybrid systems, which combines, in a single formalism, automaton transitions for capturing discrete change with differential equations for capturing continuous change. In this survey, we demonstrate symbolic algorithms for the verification of and controller synthesis for linear hybrid automata, a subclass of hybrid automata that can be analyzed automatically
AU - Alur, Rajeev
AU - Thomas Henzinger
AU - Wong-Toi, Howard
ID - 4605
TI - Symbolic analysis of hybrid systems
ER -
TY - JOUR
AB - We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem.
AU - Alur, Rajeev
AU - Courcoubetis, Costas
AU - Thomas Henzinger
ID - 4607
IS - 2
JF - Formal Methods in System Design
TI - Computing accumulated delays in real-time systems
VL - 11
ER -
TY - CONF
AB - State space explosion is a fundamental obstacle in formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reductions and symbolic state space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.
AU - Alur, Rajeev
AU - Brayton, Robert K
AU - Thomas Henzinger
AU - Qadeer,Shaz
AU - Rajamani, Sriram K
ID - 4608
TI - Partial-order reduction in symbolic state-space exploration
VL - 1254
ER -
TY - CONF
AB - Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by system moves; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator “eventually” with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. Also the problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas
AU - Alur, Rajeev
AU - Thomas Henzinger
AU - Kupferman, Orna
ID - 4609
TI - Alternating-time temporal logic
ER -
TY - JOUR
AB - Given a subspace X subset of or equal to R-d and a finite set S subset of or equal to R-d, we introduce the Delaunay complex, D-X, restricted by X. Its simplices are spanned by subsets T subset of or equal to S for which the common intersection of Voronoi cells meets X in a non-empty set. By the nerve theorem, boolean OR D-X and X are homotopy equivalent if all such sets are contractible. This paper proves a sufficient condition for boolean OR D-X and X be homeomorphic.
AU - Herbert Edelsbrunner
AU - Shah, Nimish R
ID - 4018
IS - 4
JF - International Journal of Computational Geometry and Applications
TI - Triangulating topological spaces
VL - 7
ER -
TY - JOUR
AB - A homeomorphism from R-2 to itself distorts metric quantities, such as distance and area. We describe an algorithm that constructs homeomorphisms with prescribed area distortion. Such homeomorphisms can be used to generate cartograms, which are geographic maps purposely distorted so their area distributions reflects a variable different from area, as for example population density. The algorithm generates the homeomorphism through a sequence of local piecewise linear homeomorphic changes. Sample results produced by the preliminary implementation of the method are included.
AU - Herbert Edelsbrunner
AU - Waupotitsch, Roman
ID - 4021
IS - 5-6
JF - Computational Geometry: Theory and Applications
TI - A combinatorial approach to cartograms
VL - 7
ER -