---
_id: '4220'
abstract:
- lang: eng
text: In the zebrafish, Danio rerio, a caudal and pectoral fin fold develop during
embryogenesis. At larval stages the caudal fin fold is replaced by four different
fins, the unpaired anal, dorsal and tail fins. In addition the paired pelvic fins
are formed, We have identified a total of 118 mutations affecting larval fin formation,
Mutations in 11 genes lead to abnormal morphology or degeneration of both caudal
and pectoral fin folds, Most mutants survive to adulthood and form a surprisingly
normal complement of adult fins, Mutations in nine genes result in an increased
or reduced size of the pectoral fins, Interestingly, in mutants of one of these
genes, dackel (dak), pectoral fin buds form initially, but later the fin epithelium
fails to expand, Expression of sonic hedgehog mRNA in the posterior mesenchyme
of the pectoral fin bud is initiated in dak embryos, but not maintained, Mutations
in five other genes affect adult fin but not larval fin development, Two mutants,
longfin (lof) and another longfin (alf) have generally longer fins. Stein und
bein (sub) has reduced dorsal and pelvic fins, whereas finless (fls) and wanda
(wan) mutants affect all adult fins, Finally, mutations in four genes causing
defects in embryonic skin formation will be briefly reported.
article_processing_charge: No
article_type: original
author:
- first_name: Fredericus
full_name: Van Eeden, Fredericus
last_name: Van Eeden
- first_name: Michael
full_name: Granato, Michael
last_name: Granato
- first_name: Ursula
full_name: Schach, Ursula
last_name: Schach
- first_name: Michael
full_name: Brand, Michael
last_name: Brand
- first_name: Makoto
full_name: Furutani Seiki, Makoto
last_name: Furutani Seiki
- first_name: Pascal
full_name: Haffter, Pascal
last_name: Haffter
- first_name: Matthias
full_name: Hammerschmidt, Matthias
last_name: Hammerschmidt
- first_name: Carl-Philipp J
full_name: Heisenberg, Carl-Philipp J
id: 39427864-F248-11E8-B48F-1D18A9856A87
last_name: Heisenberg
orcid: 0000-0002-0912-4566
- first_name: Yunjin
full_name: Jiang, Yunjin
last_name: Jiang
- first_name: Donald
full_name: Kane, Donald
last_name: Kane
- first_name: Robert
full_name: Kelsh, Robert
last_name: Kelsh
- first_name: Mary
full_name: Mullins, Mary
last_name: Mullins
- first_name: Jörg
full_name: Odenthal, Jörg
last_name: Odenthal
- first_name: Rachel
full_name: Warga, Rachel
last_name: Warga
- first_name: Christiane
full_name: Nüsslein Volhard, Christiane
last_name: Nüsslein Volhard
citation:
ama: Van Eeden F, Granato M, Schach U, et al. Genetic analysis of fin formation
in the zebrafish, Danio rerio. Development. 1996;123(1):255-262. doi:10.1242/dev.123.1.255
apa: Van Eeden, F., Granato, M., Schach, U., Brand, M., Furutani Seiki, M., Haffter,
P., … Nüsslein Volhard, C. (1996). Genetic analysis of fin formation in the zebrafish,
Danio rerio. Development. Company of Biologists. https://doi.org/10.1242/dev.123.1.255
chicago: Van Eeden, Fredericus, Michael Granato, Ursula Schach, Michael Brand, Makoto
Furutani Seiki, Pascal Haffter, Matthias Hammerschmidt, et al. “Genetic Analysis
of Fin Formation in the Zebrafish, Danio Rerio.” Development. Company of
Biologists, 1996. https://doi.org/10.1242/dev.123.1.255
.
ieee: F. Van Eeden et al., “Genetic analysis of fin formation in the zebrafish,
Danio rerio,” Development, vol. 123, no. 1. Company of Biologists, pp.
255–262, 1996.
ista: Van Eeden F, Granato M, Schach U, Brand M, Furutani Seiki M, Haffter P, Hammerschmidt
M, Heisenberg C-PJ, Jiang Y, Kane D, Kelsh R, Mullins M, Odenthal J, Warga R,
Nüsslein Volhard C. 1996. Genetic analysis of fin formation in the zebrafish,
Danio rerio. Development. 123(1), 255–262.
mla: Van Eeden, Fredericus, et al. “Genetic Analysis of Fin Formation in the Zebrafish,
Danio Rerio.” Development, vol. 123, no. 1, Company of Biologists, 1996,
pp. 255–62, doi:10.1242/dev.123.1.255
.
short: F. Van Eeden, M. Granato, U. Schach, M. Brand, M. Furutani Seiki, P. Haffter,
M. Hammerschmidt, C.-P.J. Heisenberg, Y. Jiang, D. Kane, R. Kelsh, M. Mullins,
J. Odenthal, R. Warga, C. Nüsslein Volhard, Development 123 (1996) 255–262.
date_created: 2018-12-11T12:07:40Z
date_published: 1996-12-01T00:00:00Z
date_updated: 2022-08-04T10:01:17Z
day: '01'
doi: '10.1242/dev.123.1.255 '
extern: '1'
external_id:
pmid:
- '9007245 '
intvolume: ' 123'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://journals.biologists.com/dev/article/123/1/255/39327/Genetic-analysis-of-fin-formation-in-the-zebrafish
month: '12'
oa: 1
oa_version: Published Version
page: 255 - 262
pmid: 1
publication: Development
publication_identifier:
issn:
- 0950-1991
publication_status: published
publisher: Company of Biologists
publist_id: '1896'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Genetic analysis of fin formation in the zebrafish, Danio rerio
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 123
year: '1996'
...
---
_id: '4222'
abstract:
- lang: eng
text: Somitogenesis is the basis of segmentation of the mesoderm in the trunk and
tail of vertebrate embryos, Two groups of mutants with defects in this patterning
process have been isolated in our screen for zygotic mutations affecting the embryonic
development of the zebrafish (Danio rerio), In mutants of the first group, boundaries
between individual somites are invisible early on, although the paraxial mesoderm
is present, Later, irregular boundaries between somites are present, Mutations
infused somites (fss) and beamter (bea) affect all somites, whereas mutations
in deadly seven (des), after eight (aei) and white tail (wit) only affect the
more posterior somites, Mutants of all genes but wit are homozygous viable and
fertile, Skeletal stainings and the expression pattern of myoD and snail1 suggest
that anteroposterior patterning within individual somites is abnormal, In the
second group of mutants, formation of the horizontal myoseptum, which separates
the dorsal and ventral part of the myotome, is reduced, Six genes have been defined
in this group (you-type genes), yea-too mutants show the most severe phenotype;
in these the adaxial cells, muscle pioneers and the primary motoneurons are affected,
in addition to the horizontal myoseptum. The horizontal myoseptum is also missing
in mutants that lack a notochord. The similarity of the somite phenotype in mutants
lacking the notochord and in the you-type mutants suggests that the genes mutated
in these two groups are involved in a signaling pathway from the notochord, important
for patterning of the somites.
acknowledgement: We would like to thank P. Ingham and T. Whitfield for valuable comments
on the manuscript and cDNA probes, S. Schulte-Merker for the Ntl antibody and J.
Eisen and R. BreMiller for the znp-1 antibody.
article_processing_charge: No
article_type: original
author:
- first_name: Fredericus
full_name: Van Eeden, Fredericus
last_name: Van Eeden
- first_name: Michael
full_name: Granato, Michael
last_name: Granato
- first_name: Ursula
full_name: Schach, Ursula
last_name: Schach
- first_name: Michael
full_name: Brand, Michael
last_name: Brand
- first_name: Makoto
full_name: Furutani Seiki, Makoto
last_name: Furutani Seiki
- first_name: Pascal
full_name: Haffter, Pascal
last_name: Haffter
- first_name: Matthias
full_name: Hammerschmidt, Matthias
last_name: Hammerschmidt
- first_name: Carl-Philipp J
full_name: Heisenberg, Carl-Philipp J
id: 39427864-F248-11E8-B48F-1D18A9856A87
last_name: Heisenberg
orcid: 0000-0002-0912-4566
- first_name: Yunjin
full_name: Jiang, Yunjin
last_name: Jiang
- first_name: Donald
full_name: Kane, Donald
last_name: Kane
- first_name: Robert
full_name: Kelsh, Robert
last_name: Kelsh
- first_name: Mary
full_name: Mullins, Mary
last_name: Mullins
- first_name: Jörg
full_name: Odenthal, Jörg
last_name: Odenthal
- first_name: Rachel
full_name: Warga, Rachel
last_name: Warga
- first_name: Miguel
full_name: Allende, Miguel
last_name: Allende
- first_name: Eric
full_name: Weinberg, Eric
last_name: Weinberg
- first_name: Christiane
full_name: Nüsslein Volhard, Christiane
last_name: Nüsslein Volhard
citation:
ama: Van Eeden F, Granato M, Schach U, et al. Mutations affecting somite formation
and patterning in the zebrafish, Danio rerio. Development. 1996;123(1):153-164.
doi:10.1242/dev.123.1.153
apa: Van Eeden, F., Granato, M., Schach, U., Brand, M., Furutani Seiki, M., Haffter,
P., … Nüsslein Volhard, C. (1996). Mutations affecting somite formation and patterning
in the zebrafish, Danio rerio. Development. Company of Biologists. https://doi.org/10.1242/dev.123.1.153
chicago: Van Eeden, Fredericus, Michael Granato, Ursula Schach, Michael Brand, Makoto
Furutani Seiki, Pascal Haffter, Matthias Hammerschmidt, et al. “Mutations Affecting
Somite Formation and Patterning in the Zebrafish, Danio Rerio.” Development.
Company of Biologists, 1996. https://doi.org/10.1242/dev.123.1.153.
ieee: F. Van Eeden et al., “Mutations affecting somite formation and patterning
in the zebrafish, Danio rerio,” Development, vol. 123, no. 1. Company of
Biologists, pp. 153–164, 1996.
ista: Van Eeden F, Granato M, Schach U, Brand M, Furutani Seiki M, Haffter P, Hammerschmidt
M, Heisenberg C-PJ, Jiang Y, Kane D, Kelsh R, Mullins M, Odenthal J, Warga R,
Allende M, Weinberg E, Nüsslein Volhard C. 1996. Mutations affecting somite formation
and patterning in the zebrafish, Danio rerio. Development. 123(1), 153–164.
mla: Van Eeden, Fredericus, et al. “Mutations Affecting Somite Formation and Patterning
in the Zebrafish, Danio Rerio.” Development, vol. 123, no. 1, Company of
Biologists, 1996, pp. 153–64, doi:10.1242/dev.123.1.153.
short: F. Van Eeden, M. Granato, U. Schach, M. Brand, M. Furutani Seiki, P. Haffter,
M. Hammerschmidt, C.-P.J. Heisenberg, Y. Jiang, D. Kane, R. Kelsh, M. Mullins,
J. Odenthal, R. Warga, M. Allende, E. Weinberg, C. Nüsslein Volhard, Development
123 (1996) 153–164.
date_created: 2018-12-11T12:07:41Z
date_published: 1996-12-01T00:00:00Z
date_updated: 2022-08-04T09:29:56Z
day: '01'
doi: 10.1242/dev.123.1.153
extern: '1'
external_id:
pmid:
- '9007237 '
intvolume: ' 123'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://journals.biologists.com/dev/article/123/1/153/39329/Mutations-affecting-somite-formation-and
month: '12'
oa: 1
oa_version: Published Version
page: 153 - 164
pmid: 1
publication: Development
publication_identifier:
issn:
- 0950-1991
publication_status: published
publisher: Company of Biologists
publist_id: '1895'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Mutations affecting somite formation and patterning in the zebrafish, Danio
rerio
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 123
year: '1996'
...
---
_id: '4292'
abstract:
- lang: eng
text: Ageing, or senescence, is a decline in state at later ages that is manifested
through a reduction in survival and fecundity. Ageing means that reproductive
prospects and hence the life history options (trade-offs) open to the organism
decline. Evolutionary theories of ageing suggest that it evolves in response to
the level of externally imposed mortality and insults to fertility, either as
part of life history optimization or as a result of mutation pressure. Several
recent empirical and theoretical studies have produced apparently anomalous results.
Some have suggested that the rate of ageing can decline at later ages, others
that demographic evidence for ageing can appear in parallel with an improvement
in state. All of these studies used measures of ageing that would not be expected
to give an accurate reflection of changes in the state of the organism with age.
We propose that Fisher's `reproductive value' is a natural measure of state at
each age, which includes prospects for both survival and reproduction. If this
measure is used, the apparently anomalous findings are not at variance with evolutionary
theories of ageing.
article_processing_charge: No
author:
- first_name: Linda
full_name: Partridge, Linda
last_name: Partridge
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Partridge L, Barton NH. On measuring the rate of ageing. Proceedings of
the Royal Society of London Series B Biological Sciences. 1996;263(1375):1365-1371.
doi:10.1098/rspb.1996.0200
apa: Partridge, L., & Barton, N. H. (1996). On measuring the rate of ageing.
Proceedings of the Royal Society of London Series B Biological Sciences.
Royal Society of London. https://doi.org/10.1098/rspb.1996.0200
chicago: Partridge, Linda, and Nicholas H Barton. “On Measuring the Rate of Ageing.”
Proceedings of the Royal Society of London Series B Biological Sciences.
Royal Society of London, 1996. https://doi.org/10.1098/rspb.1996.0200.
ieee: L. Partridge and N. H. Barton, “On measuring the rate of ageing,” Proceedings
of the Royal Society of London Series B Biological Sciences, vol. 263, no.
1375. Royal Society of London, pp. 1365–1371, 1996.
ista: Partridge L, Barton NH. 1996. On measuring the rate of ageing. Proceedings
of the Royal Society of London Series B Biological Sciences. 263(1375), 1365–1371.
mla: Partridge, Linda, and Nicholas H. Barton. “On Measuring the Rate of Ageing.”
Proceedings of the Royal Society of London Series B Biological Sciences,
vol. 263, no. 1375, Royal Society of London, 1996, pp. 1365–71, doi:10.1098/rspb.1996.0200.
short: L. Partridge, N.H. Barton, Proceedings of the Royal Society of London Series
B Biological Sciences 263 (1996) 1365–1371.
date_created: 2018-12-11T12:08:05Z
date_published: 1996-10-22T00:00:00Z
date_updated: 2022-07-04T12:59:56Z
day: '22'
doi: 10.1098/rspb.1996.0200
extern: '1'
intvolume: ' 263'
issue: '1375'
language:
- iso: eng
main_file_link:
- url: https://royalsocietypublishing.org/doi/abs/10.1098/rspb.1996.0200
month: '10'
oa_version: None
page: 1365 - 1371
publication: Proceedings of the Royal Society of London Series B Biological Sciences
publication_identifier:
issn:
- 0950-1193
publication_status: published
publisher: Royal Society of London
publist_id: '1786'
quality_controlled: '1'
status: public
title: On measuring the rate of ageing
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 263
year: '1996'
...
---
_id: '4294'
abstract:
- lang: eng
text: 'Any sample of genes traces back to a single common ancestor. Each gene also
has other properties: its sequence, its geographic location and the phenotype
and fitness of the organism that carries it. With sexual reproduction, different
genes have different genealogies, which gives us much more information, but also
greatly complicates population genetic analysis. We review the close relation
between the distribution of genealogies and the classic theory of identity by
descent in spatially structured populations, and develop a simple diffusion approximation
to the distribution of coalescence times in a homogeneous two-dimensional habitat.
This shows that when neighbourhood size is large (as in most populations) only
a small fraction of pairs of genes are closely related, and only this fraction
gives information about current rates of gene flow. The increase of spatial dispersion
with lineage age is thus a poor estimator of gene flow. The bulk of the genealogy
depends on the long-term history of the population; we discuss ways of inferring
this history from the concordance between genealogies across loci.'
article_processing_charge: No
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
- first_name: Ian
full_name: Wilson, Ian
last_name: Wilson
citation:
ama: 'Barton NH, Wilson I. Genealogies and geography. In: New Uses for New Phylogenies.
Oxford University Press; 1996:23-56. doi:10.1098/rstb.1995.0090'
apa: Barton, N. H., & Wilson, I. (1996). Genealogies and geography. In New
uses for new phylogenies (pp. 23–56). Oxford University Press. https://doi.org/10.1098/rstb.1995.0090
chicago: Barton, Nicholas H, and Ian Wilson. “Genealogies and Geography.” In New
Uses for New Phylogenies, 23–56. Oxford University Press, 1996. https://doi.org/10.1098/rstb.1995.0090.
ieee: N. H. Barton and I. Wilson, “Genealogies and geography,” in New uses for
new phylogenies, Oxford University Press, 1996, pp. 23–56.
ista: 'Barton NH, Wilson I. 1996.Genealogies and geography. In: New uses for new
phylogenies. , 23–56.'
mla: Barton, Nicholas H., and Ian Wilson. “Genealogies and Geography.” New Uses
for New Phylogenies, Oxford University Press, 1996, pp. 23–56, doi:10.1098/rstb.1995.0090.
short: N.H. Barton, I. Wilson, in:, New Uses for New Phylogenies, Oxford University
Press, 1996, pp. 23–56.
date_created: 2018-12-11T12:08:05Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-08-04T08:59:18Z
day: '01'
doi: 10.1098/rstb.1995.0090
extern: '1'
external_id:
pmid:
- '8748019'
language:
- iso: eng
month: '01'
oa_version: None
page: 23 - 56
pmid: 1
publication: New uses for new phylogenies
publication_identifier:
isbn:
- 978-0198549840
publication_status: published
publisher: Oxford University Press
publist_id: '1783'
quality_controlled: '1'
status: public
title: Genealogies and geography
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1996'
...
---
_id: '4295'
abstract:
- lang: eng
text: Genetic studies are beginning to provide insights into the evolutionary processes
that reduce the fitness of hybrids between recently diverged species. However,
the deleterious gene interactions responsible for this fitness reduction are still
poorly understood.
acknowledgement: Thanks to Brian Charlesworth, Jerry Coyne, Allen Orr and Michael
Turelli for their comments on this note, and to the BBSRC and NERC for financial
support.
article_processing_charge: No
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: 'Barton NH. Speciation: more than the sum of its parts. In: Current Biology.
Vol 6. Cell Press; 1996:1244-1246. doi:10.1016/S0960-9822(02)70707-0'
apa: 'Barton, N. H. (1996). Speciation: more than the sum of its parts. In Current
Biology (Vol. 6, pp. 1244–1246). Cell Press. https://doi.org/10.1016/S0960-9822(02)70707-0'
chicago: 'Barton, Nicholas H. “Speciation: More than the Sum of Its Parts.” In Current
Biology, 6:1244–46. Cell Press, 1996. https://doi.org/10.1016/S0960-9822(02)70707-0.'
ieee: 'N. H. Barton, “Speciation: more than the sum of its parts,” in Current
Biology, vol. 6, Cell Press, 1996, pp. 1244–1246.'
ista: 'Barton NH. 1996.Speciation: more than the sum of its parts. In: Current Biology.
vol. 6, 1244–1246.'
mla: 'Barton, Nicholas H. “Speciation: More than the Sum of Its Parts.” Current
Biology, vol. 6, Cell Press, 1996, pp. 1244–46, doi:10.1016/S0960-9822(02)70707-0.'
short: N.H. Barton, in:, Current Biology, Cell Press, 1996, pp. 1244–1246.
date_created: 2018-12-11T12:08:06Z
date_published: 1996-10-01T00:00:00Z
date_updated: 2022-07-07T09:28:28Z
day: '01'
doi: 10.1016/S0960-9822(02)70707-0
extern: '1'
external_id:
pmid:
- '8939554'
intvolume: ' 6'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0960982202707070?via%3Dihub
month: '10'
oa: 1
oa_version: Published Version
page: 1244 - 1246
pmid: 1
publication: Current Biology
publication_identifier:
issn:
- 0960-9822
publication_status: published
publisher: Cell Press
publist_id: '1781'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Speciation: more than the sum of its parts'
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 6
year: '1996'
...
---
_id: '4419'
abstract:
- lang: eng
text: A {\em hybrid automaton\/} consists of a finite automaton interacting with
a dynamical system. Hybrid automata are used to model embedded controllers and
other systems that consist of interacting discrete and continuous components.
A hybrid automaton is {\em rectangular\/} if each of its continuous variables~x
satisfies a nondeterministic differential equation of the form a≤dxdt≤b, where
a and~b are rational constants. Rectangular hybrid automata are particularly useful
for the analysis of communication protocols in which local clocks have bounded
drift, and for the conservative approximation of systems with more complex continuous
behavior. We examine several verification problems on the class of rectangular
hybrid automata, including reachability, temporal logic model checking, and controller
synthesis. Both dense-time and discrete-time models are considered. We identify
subclasses of rectangular hybrid automata for which these problems are decidable
and give complexity analyses. An investigation of the structural properties of
rectangular hybrid automata is undertaken. One method for proving the decidability
of verification problems on infinite-state systems is to find finite quotient
systems on which analysis can proceed. Three state-space equivalence relations
with strong connections to temporal logic are bisimilarity, similarity, and language
equivalence. We characterize the quotient spaces of rectangular hybrid automata
with respect to these equivalence relations.
article_processing_charge: No
author:
- first_name: Peter
full_name: Kopke, Peter
last_name: Kopke
citation:
ama: Kopke P. The Theory of Rectangular Hybrid Automata. 1996.
apa: Kopke, P. (1996). The Theory of Rectangular Hybrid Automata. Cornell
University.
chicago: Kopke, Peter. “The Theory of Rectangular Hybrid Automata.” Cornell University,
1996.
ieee: P. Kopke, “The Theory of Rectangular Hybrid Automata,” Cornell University,
1996.
ista: Kopke P. 1996. The Theory of Rectangular Hybrid Automata. Cornell University.
mla: Kopke, Peter. The Theory of Rectangular Hybrid Automata. Cornell University,
1996.
short: P. Kopke, The Theory of Rectangular Hybrid Automata, Cornell University,
1996.
date_created: 2018-12-11T12:08:45Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-07-06T15:11:24Z
day: '01'
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
publication_status: published
publisher: Cornell University
publist_id: '312'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: The Theory of Rectangular Hybrid Automata
type: dissertation
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1996'
...
---
_id: '4426'
abstract:
- lang: eng
text: We use linear hybrid automata to define linear approximations of the phase
portraits of nonlinear hybrid systems. The approximating automata can be analyzed
automatically using the symbolic model checker HyTech. We demonstrate the technique
through the study of predator-prey systems, where we compute population bounds
for both species. We also identify a class of nonlinear hybrid automata for which
linear phase-portrait approximations can be generated automatically.
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grants CCR-9200794 and CCR-9504469,
by the AFOSR contract F49620-93-1-0056, and by the ARPA grant NAG2-892.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Howard
full_name: Wong Toi, Howard
last_name: Wong Toi
citation:
ama: 'Henzinger TA, Wong Toi H. Linear phase-portrait approximations for nonlinear
hybrid systems. In: Alur R, Henzinger TA, Sontag E, eds. Hybrid Systems III:
Verification and Control. Vol 1066. Springer; 1996:377-388. doi:10.1007/BFb0020961'
apa: 'Henzinger, T. A., & Wong Toi, H. (1996). Linear phase-portrait approximations
for nonlinear hybrid systems. In R. Alur, T. A. Henzinger, & E. Sontag (Eds.),
Hybrid Systems III: Verification and Control (Vol. 1066, pp. 377–388).
Springer. https://doi.org/10.1007/BFb0020961'
chicago: 'Henzinger, Thomas A, and Howard Wong Toi. “Linear Phase-Portrait Approximations
for Nonlinear Hybrid Systems.” In Hybrid Systems III: Verification and Control,
edited by Rajeev Alur, Thomas A Henzinger, and Eduardo Sontag, 1066:377–88. Springer,
1996. https://doi.org/10.1007/BFb0020961.'
ieee: 'T. A. Henzinger and H. Wong Toi, “Linear phase-portrait approximations for
nonlinear hybrid systems,” in Hybrid Systems III: Verification and Control,
1996, vol. 1066, pp. 377–388.'
ista: 'Henzinger TA, Wong Toi H. 1996. Linear phase-portrait approximations for
nonlinear hybrid systems. Hybrid Systems III: Verification and Control. , LNCS,
vol. 1066, 377–388.'
mla: 'Henzinger, Thomas A., and Howard Wong Toi. “Linear Phase-Portrait Approximations
for Nonlinear Hybrid Systems.” Hybrid Systems III: Verification and Control,
edited by Rajeev Alur et al., vol. 1066, Springer, 1996, pp. 377–88, doi:10.1007/BFb0020961.'
short: 'T.A. Henzinger, H. Wong Toi, in:, R. Alur, T.A. Henzinger, E. Sontag (Eds.),
Hybrid Systems III: Verification and Control, Springer, 1996, pp. 377–388.'
date_created: 2018-12-11T12:08:47Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-07-06T09:58:25Z
day: '01'
doi: 10.1007/BFb0020961
editor:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Thomas A
full_name: Henzinger, Thomas A
last_name: Henzinger
- first_name: Eduardo
full_name: Sontag, Eduardo
last_name: Sontag
extern: '1'
intvolume: ' 1066'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/BFb0020961
month: '01'
oa_version: None
page: 377 - 388
publication: 'Hybrid Systems III: Verification and Control'
publication_identifier:
isbn:
- '9783540611554'
publication_status: published
publisher: Springer
publist_id: '302'
quality_controlled: '1'
status: public
title: Linear phase-portrait approximations for nonlinear hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1066
year: '1996'
...
---
_id: '4427'
abstract:
- lang: eng
text: We model a steam-boiler control system using hybrid automata. We provide two
abstracted linear models of the nonlinear behavior of the boiler. For each model,
we define and verify a controller that maintains safe operation of the boiler.
The less abstract model permits the design of a more efficient controller. We
also demonstrate how the tool HyTech can be used to automatically synthesize control
parameter constraints that guarantee safety of the boiler.
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, and by the ARPA grant NAG2-892.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Howard
full_name: Wong Toi, Howard
last_name: Wong Toi
citation:
ama: 'Henzinger TA, Wong Toi H. Using HyTech to synthesize control parameters for
a steam boiler. In: Formal Methods for Industrial Applications: Specifying
and Programming the Steam Boiler Control. Vol 1165. Springer; 1996:265-282.
doi:10.1007/BFb0027241'
apa: 'Henzinger, T. A., & Wong Toi, H. (1996). Using HyTech to synthesize control
parameters for a steam boiler. In Formal Methods for Industrial Applications:
Specifying and Programming the Steam Boiler Control (Vol. 1165, pp. 265–282).
Springer. https://doi.org/10.1007/BFb0027241'
chicago: 'Henzinger, Thomas A, and Howard Wong Toi. “Using HyTech to Synthesize
Control Parameters for a Steam Boiler.” In Formal Methods for Industrial Applications:
Specifying and Programming the Steam Boiler Control, 1165:265–82. Springer,
1996. https://doi.org/10.1007/BFb0027241.'
ieee: 'T. A. Henzinger and H. Wong Toi, “Using HyTech to synthesize control parameters
for a steam boiler,” in Formal Methods for Industrial Applications: Specifying
and Programming the Steam Boiler Control, vol. 1165, Springer, 1996, pp. 265–282.'
ista: 'Henzinger TA, Wong Toi H. 1996.Using HyTech to synthesize control parameters
for a steam boiler. In: Formal Methods for Industrial Applications: Specifying
and Programming the Steam Boiler Control. LNCS, vol. 1165, 265–282.'
mla: 'Henzinger, Thomas A., and Howard Wong Toi. “Using HyTech to Synthesize Control
Parameters for a Steam Boiler.” Formal Methods for Industrial Applications:
Specifying and Programming the Steam Boiler Control, vol. 1165, Springer,
1996, pp. 265–82, doi:10.1007/BFb0027241.'
short: 'T.A. Henzinger, H. Wong Toi, in:, Formal Methods for Industrial Applications:
Specifying and Programming the Steam Boiler Control, Springer, 1996, pp. 265–282.'
date_created: 2018-12-11T12:08:48Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-07-06T10:06:19Z
day: '01'
doi: 10.1007/BFb0027241
extern: '1'
intvolume: ' 1165'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/BFb0027241
month: '01'
oa_version: None
page: 265 - 282
publication: 'Formal Methods for Industrial Applications: Specifying and Programming
the Steam Boiler Control'
publication_identifier:
isbn:
- '9783540495666'
publication_status: published
publisher: Springer
publist_id: '303'
quality_controlled: '1'
status: public
title: Using HyTech to synthesize control parameters for a steam boiler
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1165
year: '1996'
...
---
_id: '4443'
abstract:
- lang: eng
text: "Three natural equivalence relations on the infinite state space of a hybrid
automaton are language equivalence, simulation equivalence, and bisimulation equivalence.
When one of these equivalence relations has a finite quotient, certain model checking
and controller synthesis problems are decidable. When bounds on the number of
equivalence classes are obtained, bounds on the running times of model checking
and synthesis algorithms follow as corollaries.\r\nWe characterize the time-abstract
versions of these equivalence relations on the state spaces of rectangular hybrid
automata (RHA), in which each continuous variable is a clock with bounded drift.
These automata are useful for modeling communications protocols with drifting
local clocks, and for the conservative approximation of more complex hybrid systems.
Of our two main results, one has positive implications for automatic verification,
and the other has negative implications. On the positive side, we find that the
(finite) language equivalence quotient for RHA is coarser than was previously
known by a multiplicative exponential factor. On the negative side, we show that
simulation equivalence for RHA is equality (which obviously has an infinite quotient).\r\nOur
main positive result is established by analyzing a subclass of timed automata,
called one-sided timed automata (OTA), for which the language equivalence quotient
is coarser than for the class of all timed automata. An exact characterization
of language equivalence for OTA requires a distinction between synchronous and
asynchronous definitions of (bi)simulation: if time actions are silent, then the
induced quotient for OTA is coarser than if time actions (but not their durations)
are visible."
acknowledgement: This research was supported in part by ONR Young Investigator award
N00014-95-1-0520, by NSF CAREER award CCR-9501708, by NSF grant CCR-9504469, by
Air Force Office of Scientific Research contract F49620-93-1-0056, by ARPA grant
NAG2-892, and by the U.S. Army Research Office through the Mathematical Sciences
Institute of Cornell University, Contract Number DAAL03-91-C-0027.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Peter
full_name: Kopke, Peter
last_name: Kopke
citation:
ama: 'Henzinger TA, Kopke P. State equivalences for rectangular hybrid automata.
In: 7th International Conference on Concurrency Theory. Vol 1119. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 1996:530-545. doi:10.1007/3-540-61604-7_74'
apa: 'Henzinger, T. A., & Kopke, P. (1996). State equivalences for rectangular
hybrid automata. In 7th International Conference on Concurrency Theory
(Vol. 1119, pp. 530–545). Pisa, Italy: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.1007/3-540-61604-7_74'
chicago: Henzinger, Thomas A, and Peter Kopke. “State Equivalences for Rectangular
Hybrid Automata.” In 7th International Conference on Concurrency Theory,
1119:530–45. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1996. https://doi.org/10.1007/3-540-61604-7_74.
ieee: T. A. Henzinger and P. Kopke, “State equivalences for rectangular hybrid automata,”
in 7th International Conference on Concurrency Theory, Pisa, Italy, 1996,
vol. 1119, pp. 530–545.
ista: 'Henzinger TA, Kopke P. 1996. State equivalences for rectangular hybrid automata.
7th International Conference on Concurrency Theory. CONCUR: Concurrency Theory,
LNCS, vol. 1119, 530–545.'
mla: Henzinger, Thomas A., and Peter Kopke. “State Equivalences for Rectangular
Hybrid Automata.” 7th International Conference on Concurrency Theory, vol.
1119, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1996, pp. 530–45, doi:10.1007/3-540-61604-7_74.
short: T.A. Henzinger, P. Kopke, in:, 7th International Conference on Concurrency
Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1996, pp. 530–545.
conference:
end_date: 1996-08-29
location: Pisa, Italy
name: 'CONCUR: Concurrency Theory'
start_date: 1996-08-26
date_created: 2018-12-11T12:08:52Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-07-06T08:43:23Z
day: '01'
doi: 10.1007/3-540-61604-7_74
extern: '1'
intvolume: ' 1119'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-61604-7_74
month: '01'
oa_version: None
page: 530 - 545
publication: 7th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783540616047'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '288'
quality_controlled: '1'
status: public
title: State equivalences for rectangular hybrid automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1119
year: '1996'
...
---
_id: '4495'
abstract:
- lang: eng
text: In temporal-logic model checking, we verify the correctness of a program with
respect to a desired behavior by checking whether a structure that models the
program satisfies a temporal-logic formula that specifies the behavior. The main
practical limitation of model checking is caused by the size of the state space
of the program, which grows exponentially with the number of concurrent components.
This problem, known as the state-explosion problem, becomes more difficult when
we consider real-time model checking, where the program and the specification
involve quantitative references to time. In particular, when use timed automata
to describe real-time programs and we specify timed behaviors in the logic TCTL,
a real-time extension of the temporal logic CTL with clock variables, then the
state space under consideration grows exponentially not only with the number of
concurrent components, but also with the number of clocks and the length of the
clock constraints used in the program and the specification. Two powerful methods
for coping with the state-explosion problem are on-the-fly and space-efficient
model checking. In on-the-fly model checking, we explore only the portion of the
state space of the program whose exploration is essential for determining the
satisfaction of the specification. In space-efficient model checking, we store
in memory the minimal information required, preferring to spend time on reconstructing
information rather than spend space on storing it. In this work we develop an
automata-theoretic approach to TCTL model checking that combines both methods.
We suggest, for the first time, a PSPACE on-the-fly model-checking algorithm for
TCTL.
acknowledgement: Supported in part by the ONR YIP award N00014-95-1-0520, by the NSF
CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056,
and by the ARPA grant NAG2-892.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Moshe
full_name: Vardi, Moshe
last_name: Vardi
citation:
ama: 'Henzinger TA, Kupferman O, Vardi M. A space-efficient on-the-fly algorithm
for real-time model checking. In: 7th International Conference on Concurrency
Theory. Vol 1119. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1996:514-529.
doi:10.1007/3-540-61604-7_73'
apa: 'Henzinger, T. A., Kupferman, O., & Vardi, M. (1996). A space-efficient
on-the-fly algorithm for real-time model checking. In 7th International Conference
on Concurrency Theory (Vol. 1119, pp. 514–529). Pisa, Italy: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-61604-7_73'
chicago: Henzinger, Thomas A, Orna Kupferman, and Moshe Vardi. “A Space-Efficient
on-the-Fly Algorithm for Real-Time Model Checking.” In 7th International Conference
on Concurrency Theory, 1119:514–29. Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 1996. https://doi.org/10.1007/3-540-61604-7_73.
ieee: T. A. Henzinger, O. Kupferman, and M. Vardi, “A space-efficient on-the-fly
algorithm for real-time model checking,” in 7th International Conference on
Concurrency Theory, Pisa, Italy, 1996, vol. 1119, pp. 514–529.
ista: 'Henzinger TA, Kupferman O, Vardi M. 1996. A space-efficient on-the-fly algorithm
for real-time model checking. 7th International Conference on Concurrency Theory.
CONCUR: Concurrency Theory, LNCS, vol. 1119, 514–529.'
mla: Henzinger, Thomas A., et al. “A Space-Efficient on-the-Fly Algorithm for Real-Time
Model Checking.” 7th International Conference on Concurrency Theory, vol.
1119, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1996, pp. 514–29, doi:10.1007/3-540-61604-7_73.
short: T.A. Henzinger, O. Kupferman, M. Vardi, in:, 7th International Conference
on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1996,
pp. 514–529.
conference:
end_date: 1996-08-29
location: Pisa, Italy
name: 'CONCUR: Concurrency Theory'
start_date: 1996-08-26
date_created: 2018-12-11T12:09:08Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-07-06T08:21:20Z
day: '01'
doi: 10.1007/3-540-61604-7_73
extern: '1'
intvolume: ' 1119'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-61604-7_73
month: '01'
oa_version: None
page: 514 - 529
publication: 7th International Conference on Concurrency Theory
publication_identifier:
isbn:
- 978-3-540-70625-0
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '233'
quality_controlled: '1'
status: public
title: A space-efficient on-the-fly algorithm for real-time model checking
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1119
year: '1996'
...
---
_id: '4519'
abstract:
- lang: eng
text: We summarize several recent results about hybrid automata. Our goal is to
demonstrate that concepts from the theory of discrete concurrent systems can give
insights into partly continuous systems, and that methods for the verification
of finite-state systems can be used to analyze certain systems with uncountable
state spaces
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Henzinger TA. The theory of hybrid automata. In: Proceedings 11th Annual
IEEE Symposium on Logic in Computer Science. IEEE; 1996:278-292. doi:10.1109/LICS.1996.561342 '
apa: 'Henzinger, T. A. (1996). The theory of hybrid automata. In Proceedings
11th Annual IEEE Symposium on Logic in Computer Science (pp. 278–292). New
Brunswick, NJ, United States of America: IEEE. https://doi.org/10.1109/LICS.1996.561342 '
chicago: Henzinger, Thomas A. “The Theory of Hybrid Automata.” In Proceedings
11th Annual IEEE Symposium on Logic in Computer Science, 278–92. IEEE, 1996.
https://doi.org/10.1109/LICS.1996.561342
.
ieee: T. A. Henzinger, “The theory of hybrid automata,” in Proceedings 11th Annual
IEEE Symposium on Logic in Computer Science, New Brunswick, NJ, United States
of America, 1996, pp. 278–292.
ista: 'Henzinger TA. 1996. The theory of hybrid automata. Proceedings 11th Annual
IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science,
278–292.'
mla: Henzinger, Thomas A. “The Theory of Hybrid Automata.” Proceedings 11th Annual
IEEE Symposium on Logic in Computer Science, IEEE, 1996, pp. 278–92, doi:10.1109/LICS.1996.561342 .
short: T.A. Henzinger, in:, Proceedings 11th Annual IEEE Symposium on Logic in Computer
Science, IEEE, 1996, pp. 278–292.
conference:
end_date: 1996-07-30
location: New Brunswick, NJ, United States of America
name: 'LICS: Logic in Computer Science'
start_date: 1996-07-27
date_created: 2018-12-11T12:09:16Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-07-06T07:56:28Z
day: '01'
doi: '10.1109/LICS.1996.561342 '
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://ieeexplore.ieee.org/document/561342
month: '01'
oa_version: None
page: 278 - 292
publication: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science
publication_identifier:
issn:
- 1043-6871
publication_status: published
publisher: IEEE
publist_id: '213'
quality_controlled: '1'
status: public
title: The theory of hybrid automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1996'
...