---
_id: '4248'
abstract:
- lang: eng
text: 'In finite populations, genetic drift generates interference between selected
loci, causing advantageous alleles to be found more often on different chromosomes
than on the same chromosome, which reduces the rate of adaptation. This “Hill–Robertson
effect” generates indirect selection to increase recombination rates. We present
a new method to quantify the strength of this selection. Our model represents
a new beneficial allele (A) entering a population as a single copy, while another
beneficial allele (B) is sweeping at another locus. A third locus affects the
recombination rate between selected loci. Using a branching process model, we
calculate the probability distribution of the number of copies of A on the different
genetic backgrounds, after it is established but while it is still rare. Then,
we use a deterministic model to express the change in frequency of the recombination
modifier, due to hitchhiking, as A goes to fixation. We show that this method
can give good estimates of selection for recombination. Moreover, it shows that
recombination is selected through two different effects: it increases the fixation
probability of new alleles, and it accelerates selective sweeps. The relative
importance of these two effects depends on the relative times of occurrence of
the beneficial alleles.'
author:
- first_name: Denis
full_name: Roze, Denis
last_name: Roze
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Roze D, Barton NH. The Hill-Robertson effect and the evolution of recombination.
Genetics. 2006;173(3):1793-1811. doi:10.1534/genetics.106.058586
apa: Roze, D., & Barton, N. H. (2006). The Hill-Robertson effect and the evolution
of recombination. Genetics. Genetics Society of America. https://doi.org/10.1534/genetics.106.058586
chicago: Roze, Denis, and Nicholas H Barton. “The Hill-Robertson Effect and the
Evolution of Recombination.” Genetics. Genetics Society of America, 2006.
https://doi.org/10.1534/genetics.106.058586
.
ieee: D. Roze and N. H. Barton, “The Hill-Robertson effect and the evolution of
recombination,” Genetics, vol. 173, no. 3. Genetics Society of America,
pp. 1793–1811, 2006.
ista: Roze D, Barton NH. 2006. The Hill-Robertson effect and the evolution of recombination.
Genetics. 173(3), 1793–1811.
mla: Roze, Denis, and Nicholas H. Barton. “The Hill-Robertson Effect and the Evolution
of Recombination.” Genetics, vol. 173, no. 3, Genetics Society of America,
2006, pp. 1793–811, doi:10.1534/genetics.106.058586
.
short: D. Roze, N.H. Barton, Genetics 173 (2006) 1793–1811.
date_created: 2018-12-11T12:07:50Z
date_published: 2006-07-01T00:00:00Z
date_updated: 2021-01-12T07:55:36Z
day: '01'
doi: '10.1534/genetics.106.058586 '
extern: 1
intvolume: ' 173'
issue: '3'
month: '07'
page: 1793 - 1811
publication: Genetics
publication_status: published
publisher: Genetics Society of America
publist_id: '1854'
quality_controlled: 0
status: public
title: The Hill-Robertson effect and the evolution of recombination
type: journal_article
volume: 173
year: '2006'
...
---
_id: '4250'
abstract:
- lang: eng
text: A recent analysis has shown that divergence between human and chimpanzee varies
greatly across the genome. Although this is consistent with ‘hybridisation’ between
the diverging human and chimp lineages, such observations can be explained more
simply by the null model of allopatric speciation.
author:
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: 'Barton NH. Evolutionary Biology: How did the human species form? Current
Biology. 2006;16(16):647-650. doi:10.1016/j.cub.2006.07.032'
apa: 'Barton, N. H. (2006). Evolutionary Biology: How did the human species form?
Current Biology. Cell Press. https://doi.org/10.1016/j.cub.2006.07.032'
chicago: 'Barton, Nicholas H. “Evolutionary Biology: How Did the Human Species Form?”
Current Biology. Cell Press, 2006. https://doi.org/10.1016/j.cub.2006.07.032.'
ieee: 'N. H. Barton, “Evolutionary Biology: How did the human species form?,” Current
Biology, vol. 16, no. 16. Cell Press, pp. 647–650, 2006.'
ista: 'Barton NH. 2006. Evolutionary Biology: How did the human species form? Current
Biology. 16(16), 647–650.'
mla: 'Barton, Nicholas H. “Evolutionary Biology: How Did the Human Species Form?”
Current Biology, vol. 16, no. 16, Cell Press, 2006, pp. 647–50, doi:10.1016/j.cub.2006.07.032.'
short: N.H. Barton, Current Biology 16 (2006) 647–650.
date_created: 2018-12-11T12:07:51Z
date_published: 2006-08-22T00:00:00Z
date_updated: 2019-04-26T07:22:41Z
day: '22'
doi: 10.1016/j.cub.2006.07.032
extern: 1
intvolume: ' 16'
issue: '16'
month: '08'
page: 647 - 650
publication: Current Biology
publication_status: published
publisher: Cell Press
publist_id: '1850'
quality_controlled: 0
status: public
title: 'Evolutionary Biology: How did the human species form?'
type: review
volume: 16
year: '2006'
...
---
_id: '4345'
abstract:
- lang: eng
text: Der Artikel beschäftigt sich mit dem Konzept der Bibliothek 2.0 (bzw. Library
2.0). Er skizziert anhand einiger Beispiele die Entwicklung zum Web 2.0 und beschreibt,
wie Web 2.0-Technologien und -Anwendungen in Bibliotheken eingesetzt werden. Im
Mittelpunkt stehen Social-Tagging-Systeme, benutzerorientierte Erweiterungen von
Bibliothekskatalogen und Dokumentenservern sowie der Einsatz von Weblogs an Bibliotheken.
Ferner werden neue Anforderungen an Bibliothekare diskutiert.
author:
- first_name: Patrick
full_name: Patrick Danowski
id: 2EBD1598-F248-11E8-B48F-1D18A9856A87
last_name: Danowski
orcid: 0000-0002-6026-4409
- first_name: Lambert
full_name: Heller,Lambert
last_name: Heller
citation:
ama: Danowski P, Heller L. Bibliothek 2.0 - Die Bibliothek der Zukunft? Bibliotheksdienst.
2006;40(11):1250-1271. doi:424
apa: Danowski, P., & Heller, L. (2006). Bibliothek 2.0 - Die Bibliothek der
Zukunft? Bibliotheksdienst. Zentral- und Landesbibliothek Berlin. https://doi.org/424
chicago: Danowski, Patrick, and Lambert Heller. “Bibliothek 2.0 - Die Bibliothek
Der Zukunft?” Bibliotheksdienst. Zentral- und Landesbibliothek Berlin,
2006. https://doi.org/424.
ieee: P. Danowski and L. Heller, “Bibliothek 2.0 - Die Bibliothek der Zukunft?,”
Bibliotheksdienst, vol. 40, no. 11. Zentral- und Landesbibliothek Berlin,
pp. 1250–1271, 2006.
ista: Danowski P, Heller L. 2006. Bibliothek 2.0 - Die Bibliothek der Zukunft? Bibliotheksdienst.
40(11), 1250–1271.
mla: Danowski, Patrick, and Lambert Heller. “Bibliothek 2.0 - Die Bibliothek Der
Zukunft?” Bibliotheksdienst, vol. 40, no. 11, Zentral- und Landesbibliothek
Berlin, 2006, pp. 1250–71, doi:424.
short: P. Danowski, L. Heller, Bibliotheksdienst 40 (2006) 1250–1271.
date_created: 2018-12-11T12:08:23Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:17Z
day: '01'
doi: '424'
extern: 1
intvolume: ' 40'
issue: '11'
main_file_link:
- open_access: '0'
url: http://www.zlb.de/aktivitaeten/bd_neu/heftinhalte2006/DigitaleBib011106.pdf
month: '01'
page: 1250 - 1271
publication: Bibliotheksdienst
publication_status: published
publisher: Zentral- und Landesbibliothek Berlin
publist_id: '1229'
quality_controlled: 0
status: public
title: Bibliothek 2.0 - Die Bibliothek der Zukunft?
type: journal_article
volume: 40
year: '2006'
...
---
_id: '4351'
abstract:
- lang: eng
text: 'BACKGROUND: Character mapping on phylogenies has played an important, if
not critical role, in our understanding of molecular, morphological, and behavioral
evolution. Until very recently we have relied on parsimony to infer character
changes. Parsimony has a number of serious limitations that are drawbacks to our
understanding. Recent statistical methods have been developed that free us from
these limitations enabling us to overcome the problems of parsimony by accommodating
uncertainty in evolutionary time, ancestral states, and the phylogeny. RESULTS:
SIMMAP has been developed to implement stochastic character mapping that is useful
to both molecular evolutionists, systematists, and bioinformaticians. Researchers
can address questions about positive selection, patterns of amino acid substitution,
character association, and patterns of morphological evolution. CONCLUSION: Stochastic
character mapping, as implemented in the SIMMAP software, enables users to address
questions that require mapping characters onto phylogenies using a probabilistic
approach that does not rely on parsimony. Analyses can be performed using a fully
Bayesian approach that is not reliant on considering a single topology, set of
substitution model parameters, or reconstruction of ancestral states. Uncertainty
in these quantities is accommodated by using MCMC samples from their respective
posterior distributions.'
author:
- first_name: Jonathan P
full_name: Jonathan Bollback
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
citation:
ama: 'Bollback JP. SIMMAP: stochastic character mapping of discrete traits on phylogenies.
BMC Bioinformatics. 2006;7. doi:10.1186/1471-2105-7-88'
apa: 'Bollback, J. P. (2006). SIMMAP: stochastic character mapping of discrete traits
on phylogenies. BMC Bioinformatics. BioMed Central. https://doi.org/10.1186/1471-2105-7-88'
chicago: 'Bollback, Jonathan P. “SIMMAP: Stochastic Character Mapping of Discrete
Traits on Phylogenies.” BMC Bioinformatics. BioMed Central, 2006. https://doi.org/10.1186/1471-2105-7-88.'
ieee: 'J. P. Bollback, “SIMMAP: stochastic character mapping of discrete traits
on phylogenies,” BMC Bioinformatics, vol. 7. BioMed Central, 2006.'
ista: 'Bollback JP. 2006. SIMMAP: stochastic character mapping of discrete traits
on phylogenies. BMC Bioinformatics. 7.'
mla: 'Bollback, Jonathan P. “SIMMAP: Stochastic Character Mapping of Discrete Traits
on Phylogenies.” BMC Bioinformatics, vol. 7, BioMed Central, 2006, doi:10.1186/1471-2105-7-88.'
short: J.P. Bollback, BMC Bioinformatics 7 (2006).
date_created: 2018-12-11T12:08:25Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:20Z
day: '01'
doi: 10.1186/1471-2105-7-88
extern: 1
intvolume: ' 7'
month: '01'
publication: BMC Bioinformatics
publication_status: published
publisher: BioMed Central
publist_id: '1109'
quality_controlled: 0
status: public
title: 'SIMMAP: stochastic character mapping of discrete traits on phylogenies'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
volume: 7
year: '2006'
...
---
_id: '4352'
abstract:
- lang: eng
text: 'Anopheles darlingi is the primary malaria vector in Latin America, and is
especially important in Amazonian Brazil. Historically, control efforts have been
focused on indoor house spraying using a variety of insecticides, but since the
mid-1990s there has been a shift to patient treatment and focal insecticide fogging.
Anopheles darlingi was believed to have been significantly reduced in a gold-mining
community, Peixoto de Azevedo (in Mato Grosso State), in the early 1990s by insecticide
use during a severe malaria epidemic. In contrast, although An. darlingi was eradicated
from some districts of the city of Belem (the capital of Para State) in 1968 to
reduce malaria, populations around the water protection area in the eastern district
were treated only briefly. To investigate the population structure of An. darlingi
including evidence for a population bottleneck in Peixoto, we analyzed eight microsatellite
loci of 256 individuals from seven locations in Brazil: three in Amapa State,
three in Para State, and one in Mato Grosso State. Allelic diversity and mean
expected heterozygosity were high for all populations (mean number alleles/locus
and H(E) were 13.5 and 0.834, respectively) and did not differ significantly between
locations. Significant heterozygote deficits were associated with linkage disequilibrium,
most likely due to either the Wahlund effect or selection. We found no evidence
for a population bottleneck in Peixoto, possibly because the reduction was not
extreme enough to be detected. Overall estimates of long-term N(e) varied from
92.4 individuals under the linkage disequilibrium model to infinity under the
heterozygote excess model. Fixation indices and analysis of molecular variance
demonstrated significant differentiation between locations north and south of
the Amazon River, suggesting a degree of genetic isolation between them, attributed
to isolation by distance.'
author:
- first_name: Jan
full_name: Conn, Jan E
last_name: Conn
- first_name: Joseph
full_name: Vineis, Joseph H
last_name: Vineis
- first_name: Jonathan P
full_name: Jonathan Bollback
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
- first_name: David
full_name: Onyabe, David Y
last_name: Onyabe
- first_name: Richard
full_name: Wilkerson, Richard C
last_name: Wilkerson
- first_name: Marinete
full_name: Povoa, Marinete M
last_name: Povoa
citation:
ama: Conn J, Vineis J, Bollback JP, Onyabe D, Wilkerson R, Povoa M. Population structure
of the malaria vector Anopheles darlingi in a malaria-endemic region of eastern
Amazonian Brazil. The American Journal of Tropical Medicine and Hygiene.
2006;74(5):798-806.
apa: Conn, J., Vineis, J., Bollback, J. P., Onyabe, D., Wilkerson, R., & Povoa,
M. (2006). Population structure of the malaria vector Anopheles darlingi in a
malaria-endemic region of eastern Amazonian Brazil. The American Journal of
Tropical Medicine and Hygiene. American Society of Tropical Medicine and Hygiene.
chicago: Conn, Jan, Joseph Vineis, Jonathan P Bollback, David Onyabe, Richard Wilkerson,
and Marinete Povoa. “Population Structure of the Malaria Vector Anopheles Darlingi
in a Malaria-Endemic Region of Eastern Amazonian Brazil.” The American Journal
of Tropical Medicine and Hygiene. American Society of Tropical Medicine and
Hygiene, 2006.
ieee: J. Conn, J. Vineis, J. P. Bollback, D. Onyabe, R. Wilkerson, and M. Povoa,
“Population structure of the malaria vector Anopheles darlingi in a malaria-endemic
region of eastern Amazonian Brazil,” The American Journal of Tropical Medicine
and Hygiene, vol. 74, no. 5. American Society of Tropical Medicine and Hygiene,
pp. 798–806, 2006.
ista: Conn J, Vineis J, Bollback JP, Onyabe D, Wilkerson R, Povoa M. 2006. Population
structure of the malaria vector Anopheles darlingi in a malaria-endemic region
of eastern Amazonian Brazil. The American Journal of Tropical Medicine and Hygiene.
74(5), 798–806.
mla: Conn, Jan, et al. “Population Structure of the Malaria Vector Anopheles Darlingi
in a Malaria-Endemic Region of Eastern Amazonian Brazil.” The American Journal
of Tropical Medicine and Hygiene, vol. 74, no. 5, American Society of Tropical
Medicine and Hygiene, 2006, pp. 798–806.
short: J. Conn, J. Vineis, J.P. Bollback, D. Onyabe, R. Wilkerson, M. Povoa, The
American Journal of Tropical Medicine and Hygiene 74 (2006) 798–806.
date_created: 2018-12-11T12:08:25Z
date_published: 2006-05-01T00:00:00Z
date_updated: 2021-01-12T07:56:20Z
day: '01'
extern: 1
intvolume: ' 74'
issue: '5'
main_file_link:
- open_access: '0'
url: http://www.ajtmh.org/content/74/5/798.full
month: '05'
page: 798 - 806
publication: The American Journal of Tropical Medicine and Hygiene
publication_status: published
publisher: American Society of Tropical Medicine and Hygiene
publist_id: '1108'
quality_controlled: 0
status: public
title: Population structure of the malaria vector Anopheles darlingi in a malaria-endemic
region of eastern Amazonian Brazil
type: journal_article
volume: 74
year: '2006'
...
---
_id: '4359'
alternative_title:
- LNCS 3855
author:
- first_name: Thomas
full_name: Thomas Wies
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
- first_name: Patrick
full_name: Lam,Patrick
last_name: Lam
- first_name: Andreas
full_name: Podelski,Andreas
last_name: Podelski
- first_name: Martin
full_name: Rinard,Martin
last_name: Rinard
citation:
ama: 'Wies T, Kuncak V, Lam P, Podelski A, Rinard M. Field Constraint Analysis.
In: Springer; 2006:157-173. doi:1551'
apa: 'Wies, T., Kuncak, V., Lam, P., Podelski, A., & Rinard, M. (2006). Field
Constraint Analysis (pp. 157–173). Presented at the VMCAI: Verification, Model
Checking and Abstract Interpretation, Springer. https://doi.org/1551'
chicago: Wies, Thomas, Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin
Rinard. “Field Constraint Analysis,” 157–73. Springer, 2006. https://doi.org/1551.
ieee: 'T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard, “Field Constraint
Analysis,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
2006, pp. 157–173.'
ista: 'Wies T, Kuncak V, Lam P, Podelski A, Rinard M. 2006. Field Constraint Analysis.
VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS 3855, ,
157–173.'
mla: Wies, Thomas, et al. Field Constraint Analysis. Springer, 2006, pp.
157–73, doi:1551.
short: T. Wies, V. Kuncak, P. Lam, A. Podelski, M. Rinard, in:, Springer, 2006,
pp. 157–173.
conference:
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
date_created: 2018-12-11T12:08:27Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:23Z
day: '01'
doi: '1551'
extern: 1
month: '01'
page: 157 - 173
publication_status: published
publisher: Springer
publist_id: '1097'
quality_controlled: 0
status: public
title: Field Constraint Analysis
type: conference
year: '2006'
...
---
_id: '4373'
alternative_title:
- LNCS
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Dejan Nickovic
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli,Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. Real Time Temporal Logic: Past, Present, Future.
In: Springer; 2006:2-16. doi:1571'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2006). Real Time Temporal Logic:
Past, Present, Future (pp. 2–16). Presented at the FORMATS: Formal Modeling and
Analysis of Timed Systems, Springer. https://doi.org/1571'
chicago: 'Maler, Oded, Dejan Nickovic, and Amir Pnueli. “Real Time Temporal Logic:
Past, Present, Future,” 2–16. Springer, 2006. https://doi.org/1571.'
ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “Real Time Temporal Logic: Past, Present,
Future,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems,
2006, pp. 2–16.'
ista: 'Maler O, Nickovic D, Pnueli A. 2006. Real Time Temporal Logic: Past, Present,
Future. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 2–16.'
mla: 'Maler, Oded, et al. Real Time Temporal Logic: Past, Present, Future.
Springer, 2006, pp. 2–16, doi:1571.'
short: O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2006, pp. 2–16.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:31Z
date_published: 2006-01-23T00:00:00Z
date_updated: 2021-01-12T07:56:29Z
day: '23'
doi: '1571'
extern: 1
month: '01'
page: 2 - 16
publication_status: published
publisher: Springer
publist_id: '1084'
quality_controlled: 0
status: public
title: 'Real Time Temporal Logic: Past, Present, Future'
type: conference
year: '2006'
...
---
_id: '4374'
alternative_title:
- LNCS
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Dejan Nickovic
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli,Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. From MITL to Timed Automata. In: Springer;
2006:274-289. doi:1570'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2006). From MITL to Timed Automata
(pp. 274–289). Presented at the FORMATS: Formal Modeling and Analysis of Timed
Systems, Springer. https://doi.org/1570'
chicago: Maler, Oded, Dejan Nickovic, and Amir Pnueli. “From MITL to Timed Automata,”
274–89. Springer, 2006. https://doi.org/1570.
ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “From MITL to Timed Automata,” presented
at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2006, pp. 274–289.'
ista: 'Maler O, Nickovic D, Pnueli A. 2006. From MITL to Timed Automata. FORMATS:
Formal Modeling and Analysis of Timed Systems, LNCS, , 274–289.'
mla: Maler, Oded, et al. From MITL to Timed Automata. Springer, 2006, pp.
274–89, doi:1570.
short: O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2006, pp. 274–289.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:31Z
date_published: 2006-10-19T00:00:00Z
date_updated: 2021-01-12T07:56:30Z
day: '19'
doi: '1570'
extern: 1
month: '10'
page: 274 - 289
publication_status: published
publisher: Springer
publist_id: '1085'
quality_controlled: 0
status: public
title: From MITL to Timed Automata
type: conference
year: '2006'
...
---
_id: '4401'
alternative_title:
- LNCS
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Pavol
full_name: Pavol Cerny
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Steve
full_name: Zdancewic,Steve
last_name: Zdancewic
citation:
ama: 'Alur R, Cerny P, Zdancewic S. Preserving Secrecy Under Refinement. In: Springer;
2006:107-118. doi:1543'
apa: 'Alur, R., Cerny, P., & Zdancewic, S. (2006). Preserving Secrecy Under
Refinement (pp. 107–118). Presented at the ICALP: Automata, Languages and Programming,
Springer. https://doi.org/1543'
chicago: Alur, Rajeev, Pavol Cerny, and Steve Zdancewic. “Preserving Secrecy Under
Refinement,” 107–18. Springer, 2006. https://doi.org/1543.
ieee: 'R. Alur, P. Cerny, and S. Zdancewic, “Preserving Secrecy Under Refinement,”
presented at the ICALP: Automata, Languages and Programming, 2006, pp. 107–118.'
ista: 'Alur R, Cerny P, Zdancewic S. 2006. Preserving Secrecy Under Refinement.
ICALP: Automata, Languages and Programming, LNCS, , 107–118.'
mla: Alur, Rajeev, et al. Preserving Secrecy Under Refinement. Springer,
2006, pp. 107–18, doi:1543.
short: R. Alur, P. Cerny, S. Zdancewic, in:, Springer, 2006, pp. 107–118.
conference:
name: 'ICALP: Automata, Languages and Programming'
date_created: 2018-12-11T12:08:40Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:42Z
day: '01'
doi: '1543'
extern: 1
month: '01'
page: 107 - 118
publication_status: published
publisher: Springer
publist_id: '1054'
quality_controlled: 0
status: public
title: Preserving Secrecy Under Refinement
type: conference
year: '2006'
...
---
_id: '4406'
abstract:
- lang: eng
text: We propose and evaluate a new algorithm for checking the universality of nondeterministic
finite automata. In contrast to the standard algorithm, which uses the subset
construction to explicitly determinize the automaton, we keep the determinization
step implicit. Our algorithm computes the least fixed point of a monotone function
on the lattice of antichains of state sets. We evaluate the performance of our
algorithm experimentally using the random automaton model recently proposed by
Tabakov and Vardi. We show that on the difficult instances of this probabilistic
model, the antichain algorithm outperforms the standard one by several orders
of magnitude. We also show how variations of the antichain method can be used
for solving the language-inclusion problem for nondeterministic finite automata,
and the emptiness problem for alternating finite automata.
acknowledgement: This research was supported in part by the NSF grants CCR-0234690
and CCR-0225610, and the Belgian FNRS grant 2.4530.02 of the FRFC project “Centre
Fédéré en Vérification.”
alternative_title:
- LNCS
author:
- first_name: Martin
full_name: De Wulf, Martin
last_name: De Wulf
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jean
full_name: Raskin, Jean-François
last_name: Raskin
citation:
ama: 'De Wulf M, Doyen L, Henzinger TA, Raskin J. Antichains: A new algorithm for
checking universality of finite automata. In: Vol 4144. Springer; 2006:17-30.
doi:10.1007/11817963_5'
apa: 'De Wulf, M., Doyen, L., Henzinger, T. A., & Raskin, J. (2006). Antichains:
A new algorithm for checking universality of finite automata (Vol. 4144, pp. 17–30).
Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/11817963_5'
chicago: 'De Wulf, Martin, Laurent Doyen, Thomas A Henzinger, and Jean Raskin. “Antichains:
A New Algorithm for Checking Universality of Finite Automata,” 4144:17–30. Springer,
2006. https://doi.org/10.1007/11817963_5.'
ieee: 'M. De Wulf, L. Doyen, T. A. Henzinger, and J. Raskin, “Antichains: A new
algorithm for checking universality of finite automata,” presented at the CAV:
Computer Aided Verification, 2006, vol. 4144, pp. 17–30.'
ista: 'De Wulf M, Doyen L, Henzinger TA, Raskin J. 2006. Antichains: A new algorithm
for checking universality of finite automata. CAV: Computer Aided Verification,
LNCS, vol. 4144, 17–30.'
mla: 'De Wulf, Martin, et al. Antichains: A New Algorithm for Checking Universality
of Finite Automata. Vol. 4144, Springer, 2006, pp. 17–30, doi:10.1007/11817963_5.'
short: M. De Wulf, L. Doyen, T.A. Henzinger, J. Raskin, in:, Springer, 2006, pp.
17–30.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:41Z
date_published: 2006-08-08T00:00:00Z
date_updated: 2021-01-12T07:56:45Z
day: '08'
doi: 10.1007/11817963_5
extern: 1
intvolume: ' 4144'
month: '08'
page: 17 - 30
publication_status: published
publisher: Springer
publist_id: '326'
quality_controlled: 0
status: public
title: 'Antichains: A new algorithm for checking universality of finite automata'
type: conference
volume: 4144
year: '2006'
...
---
_id: '4431'
abstract:
- lang: eng
text: 'We summarize some current trends in embedded systems design and point out
some of their characteristics, such as the chasm between analytical and computational
models, and the gap between safety-critical and best-effort engineering practices.
We call for a coherent scientific foundation for embedded systems design, and
we discuss a few key demands on such a foundation: the need for encompassing several
manifestations of heterogeneity, and the need for constructivity in design. We
believe that the development of a satisfactory Embedded Systems Design Science
provides a timely challenge and opportunity for reinvigorating computer science.'
acknowledgement: Supported in part by the ARTIST2 European Network of Excellence on
Embedded Systems Design, by the NSF ITR Center on Hybrid and Embedded Software Systems
(CHESS), and by the SNSF NCCR on Mobile Information and Communication Systems (MICS).
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Joseph
full_name: Sifakis, Joseph
last_name: Sifakis
citation:
ama: 'Henzinger TA, Sifakis J. The embedded systems design challenge. In: Vol 4085.
Springer; 2006:1-15. doi:10.1007/11813040_1'
apa: 'Henzinger, T. A., & Sifakis, J. (2006). The embedded systems design challenge
(Vol. 4085, pp. 1–15). Presented at the FM: Formal Methods, Springer. https://doi.org/10.1007/11813040_1'
chicago: Henzinger, Thomas A, and Joseph Sifakis. “The Embedded Systems Design Challenge,”
4085:1–15. Springer, 2006. https://doi.org/10.1007/11813040_1.
ieee: 'T. A. Henzinger and J. Sifakis, “The embedded systems design challenge,”
presented at the FM: Formal Methods, 2006, vol. 4085, pp. 1–15.'
ista: 'Henzinger TA, Sifakis J. 2006. The embedded systems design challenge. FM:
Formal Methods, LNCS, vol. 4085, 1–15.'
mla: Henzinger, Thomas A., and Joseph Sifakis. The Embedded Systems Design Challenge.
Vol. 4085, Springer, 2006, pp. 1–15, doi:10.1007/11813040_1.
short: T.A. Henzinger, J. Sifakis, in:, Springer, 2006, pp. 1–15.
conference:
name: 'FM: Formal Methods'
date_created: 2018-12-11T12:08:49Z
date_published: 2006-08-10T00:00:00Z
date_updated: 2021-01-12T07:56:55Z
day: '10'
doi: 10.1007/11813040_1
extern: 1
intvolume: ' 4085'
month: '08'
page: 1 - 15
publication_status: published
publisher: Springer
publist_id: '301'
quality_controlled: 0
status: public
title: The embedded systems design challenge
type: conference
volume: 4085
year: '2006'
...
---
_id: '4432'
abstract:
- lang: eng
text: We add freeze quantifiers to the game logic ATL in order to specify real-time
objectives for games played on timed structures. We define the semantics of the
resulting logic TATL by restricting the players to physically meaningful strategies,
which do not prevent time from diverging. We show that TATL can be model checked
over timed automaton games. We also specify timed optimization problems for physically
meaningful strategies, and we show that for timed automaton games, the optimal
answers can be approximated to within any degree of precision.
acknowledgement: This research was supported in part by the NSF grants CCR-0208875,
CCR-0225610, and CCR-0234690.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Vinayak
full_name: Prabhu, Vinayak S
last_name: Prabhu
citation:
ama: 'Henzinger TA, Prabhu V. Timed alternating-time temporal logic. In: Vol 4202.
Springer; 2006:1-17. doi:10.1007/11867340_1'
apa: 'Henzinger, T. A., & Prabhu, V. (2006). Timed alternating-time temporal
logic (Vol. 4202, pp. 1–17). Presented at the FORMATS: Formal Modeling and Analysis
of Timed Systems, Springer. https://doi.org/10.1007/11867340_1'
chicago: Henzinger, Thomas A, and Vinayak Prabhu. “Timed Alternating-Time Temporal
Logic,” 4202:1–17. Springer, 2006. https://doi.org/10.1007/11867340_1.
ieee: 'T. A. Henzinger and V. Prabhu, “Timed alternating-time temporal logic,” presented
at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2006, vol. 4202,
pp. 1–17.'
ista: 'Henzinger TA, Prabhu V. 2006. Timed alternating-time temporal logic. FORMATS:
Formal Modeling and Analysis of Timed Systems, LNCS, vol. 4202, 1–17.'
mla: Henzinger, Thomas A., and Vinayak Prabhu. Timed Alternating-Time Temporal
Logic. Vol. 4202, Springer, 2006, pp. 1–17, doi:10.1007/11867340_1.
short: T.A. Henzinger, V. Prabhu, in:, Springer, 2006, pp. 1–17.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:49Z
date_published: 2006-09-19T00:00:00Z
date_updated: 2021-01-12T07:56:56Z
day: '19'
doi: 10.1007/11867340_1
extern: 1
intvolume: ' 4202'
month: '09'
page: 1 - 17
publication_status: published
publisher: Springer
publist_id: '296'
quality_controlled: 0
status: public
title: Timed alternating-time temporal logic
type: conference
volume: 4202
year: '2006'
...
---
_id: '4436'
abstract:
- lang: eng
text: We present an assume-guarantee interface algebra for real-time components.
In our formalism a component implements a set of task sequences that share a resource.
A component interface consists of an arrival rate function and a latency for each
task sequence, and a capacity function for the shared resource. The interface
specifies that the component guarantees certain task latencies depending on assumptions
about task arrival rates and allocated resource capacities. Our algebra defines
compatibility and refinement relations on interfaces. Interface compatibility
can be checked on partial designs, even when some component interfaces are yet
unknown. In this case interface composition computes as new assumptions the weakest
constraints on the unknown components that are necessary to satisfy the specified
guarantees. Interface refinement is defined in a way that ensures that compatible
interfaces can be refined and implemented independently. Our algebra thus formalizes
an interface-based design methodology that supports both the incremental addition
of new components and the independent stepwise refinement of existing components.
We demonstrate the flexibility and efficiency of the framework through simulation
experiments.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: 'Henzinger TA, Matic S. An interface algebra for real-time components. In:
IEEE; 2006:253-266. doi:10.1109/RTAS.2006.11'
apa: 'Henzinger, T. A., & Matic, S. (2006). An interface algebra for real-time
components (pp. 253–266). Presented at the RTAS: Real-time and Embedded Technology
and Applications Symposium, IEEE. https://doi.org/10.1109/RTAS.2006.11'
chicago: Henzinger, Thomas A, and Slobodan Matic. “An Interface Algebra for Real-Time
Components,” 253–66. IEEE, 2006. https://doi.org/10.1109/RTAS.2006.11.
ieee: 'T. A. Henzinger and S. Matic, “An interface algebra for real-time components,”
presented at the RTAS: Real-time and Embedded Technology and Applications Symposium,
2006, pp. 253–266.'
ista: 'Henzinger TA, Matic S. 2006. An interface algebra for real-time components.
RTAS: Real-time and Embedded Technology and Applications Symposium, 253–266.'
mla: Henzinger, Thomas A., and Slobodan Matic. An Interface Algebra for Real-Time
Components. IEEE, 2006, pp. 253–66, doi:10.1109/RTAS.2006.11.
short: T.A. Henzinger, S. Matic, in:, IEEE, 2006, pp. 253–266.
conference:
name: 'RTAS: Real-time and Embedded Technology and Applications Symposium'
date_created: 2018-12-11T12:08:50Z
date_published: 2006-04-24T00:00:00Z
date_updated: 2021-01-12T07:56:57Z
day: '24'
doi: 10.1109/RTAS.2006.11
extern: 1
month: '04'
page: 253 - 266
publication_status: published
publisher: IEEE
publist_id: '294'
quality_controlled: 0
status: public
title: An interface algebra for real-time components
type: conference
year: '2006'
...
---
_id: '4437'
abstract:
- lang: eng
text: The synthesis of reactive systems requires the solution of two-player games
on graphs with ω-regular objectives. When the objective is specified by a linear
temporal logic formula or nondeterministic Büchi automaton, then previous algorithms
for solving the game require the construction of an equivalent deterministic automaton.
However, determinization for automata on infinite words is extremely complicated,
and current implementations fail to produce deterministic automata even for relatively
small inputs. We show how to construct, from a given nondeterministic Büchi automaton,
an equivalent nondeterministic parity automaton that is good for solving games
with objective . The main insight is that a nondeterministic automaton is good
for solving games if it fairly simulates the equivalent deterministic automaton.
In this way, we omit the determinization step in game solving and reactive synthesis.
The fact that our automata are nondeterministic makes them surprisingly simple,
amenable to symbolic implementation, and allows an incremental search for winning
strategies.
acknowledgement: This research was supported in part by the Swiss National Science
Foundation.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Henzinger TA, Piterman N. Solving games without determinization. In: Vol 4207.
Springer; 2006:395-410. doi:10.1007/11874683_26'
apa: 'Henzinger, T. A., & Piterman, N. (2006). Solving games without determinization
(Vol. 4207, pp. 395–410). Presented at the CSL: Computer Science Logic, Springer.
https://doi.org/10.1007/11874683_26'
chicago: Henzinger, Thomas A, and Nir Piterman. “Solving Games without Determinization,”
4207:395–410. Springer, 2006. https://doi.org/10.1007/11874683_26.
ieee: 'T. A. Henzinger and N. Piterman, “Solving games without determinization,”
presented at the CSL: Computer Science Logic, 2006, vol. 4207, pp. 395–410.'
ista: 'Henzinger TA, Piterman N. 2006. Solving games without determinization. CSL:
Computer Science Logic, LNCS, vol. 4207, 395–410.'
mla: Henzinger, Thomas A., and Nir Piterman. Solving Games without Determinization.
Vol. 4207, Springer, 2006, pp. 395–410, doi:10.1007/11874683_26.
short: T.A. Henzinger, N. Piterman, in:, Springer, 2006, pp. 395–410.
conference:
name: 'CSL: Computer Science Logic'
date_created: 2018-12-11T12:08:51Z
date_published: 2006-09-20T00:00:00Z
date_updated: 2021-01-12T07:56:58Z
day: '20'
doi: 10.1007/11874683_26
extern: 1
intvolume: ' 4207'
month: '09'
page: 395 - 410
publication_status: published
publisher: Springer
publist_id: '295'
quality_controlled: 0
status: public
title: Solving games without determinization
type: conference
volume: 4207
year: '2006'
...
---
_id: '4451'
abstract:
- lang: eng
text: One source of complexity in the μ-calculus is its ability to specify an unbounded
number of switches between universal (AX) and existential (EX) branching modes.
We therefore study the problems of satisfiability, validity, model checking, and
implication for the universal and existential fragments of the μ-calculus, in
which only one branching mode is allowed. The universal fragment is rich enough
to express most specifications of interest, and therefore improved algorithms
are of practical importance. We show that while the satisfiability and validity
problems become indeed simpler for the existential and universal fragments, this
is, unfortunately, not the case for model checking and implication. We also show
the corresponding results for the alternation-free fragment of the μ-calculus,
where no alternations between least and greatest fixed points are allowed. Our
results imply that efforts to find a polynomial-time model-checking algorithm
for the μ-calculus can be replaced by efforts to find such an algorithm for the
universal or existential fragment.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
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: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments
of the mu-calculus. Theoretical Computer Science. 2006;354(2):173-186.
doi:10.1016/j.tcs.2005.11.015
apa: Henzinger, T. A., Kupferman, O., & Majumdar, R. (2006). On the universal
and existential fragments of the mu-calculus. Theoretical Computer Science.
Elsevier. https://doi.org/10.1016/j.tcs.2005.11.015
chicago: Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal
and Existential Fragments of the Mu-Calculus.” Theoretical Computer Science.
Elsevier, 2006. https://doi.org/10.1016/j.tcs.2005.11.015.
ieee: T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential
fragments of the mu-calculus,” Theoretical Computer Science, vol. 354,
no. 2. Elsevier, pp. 173–186, 2006.
ista: Henzinger TA, Kupferman O, Majumdar R. 2006. On the universal and existential
fragments of the mu-calculus. Theoretical Computer Science. 354(2), 173–186.
mla: Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of
the Mu-Calculus.” Theoretical Computer Science, vol. 354, no. 2, Elsevier,
2006, pp. 173–86, doi:10.1016/j.tcs.2005.11.015.
short: T.A. Henzinger, O. Kupferman, R. Majumdar, Theoretical Computer Science 354
(2006) 173–186.
date_created: 2018-12-11T12:08:55Z
date_published: 2006-03-28T00:00:00Z
date_updated: 2021-01-12T07:57:04Z
day: '28'
doi: 10.1016/j.tcs.2005.11.015
extern: 1
intvolume: ' 354'
issue: '2'
month: '03'
page: 173 - 186
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '276'
quality_controlled: 0
status: public
title: On the universal and existential fragments of the mu-calculus
type: journal_article
volume: 354
year: '2006'
...
---
_id: '4523'
abstract:
- lang: eng
text: We consider the problem if a given program satisfies a specified safety property.
Interesting programs have infinite state spaces, with inputs ranging over infinite
domains, and for these programs the property checking problem is undecidable.
Two broad approaches to property checking are testing and verification. Testing
tries to find inputs and executions which demonstrate violations of the property.
Verification tries to construct a formal proof which shows that all executions
of the program satisfy the property. Testing works best when errors are easy to
find, but it is often difficult to achieve sufficient coverage for correct programs.
On the other hand, verification methods are most successful when proofs are easy
to find, but they are often inefficient at discovering errors. We propose a new
algorithm, Synergy, which combines testing and verification. Synergy unifies several
ideas from the literature, including counterexample-guided model checking, directed
testing, and partition refinement.This paper presents a description of the Synergy
algorithm, its theoretical properties, a comparison with related algorithms, and
a prototype implementation called Yogi.
author:
- first_name: Bhargav
full_name: Gulavani, Bhargav S
last_name: Gulavani
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Yamini
full_name: Kannan, Yamini
last_name: Kannan
- first_name: Aditya
full_name: Nori, Aditya V
last_name: Nori
- first_name: Sriram
full_name: Rajamani, Sriram K
last_name: Rajamani
citation:
ama: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. Synergy: A new algorithm
for property checking. In: ACM; 2006:117-127. doi:10.1145/1181775.1181790'
apa: 'Gulavani, B., Henzinger, T. A., Kannan, Y., Nori, A., & Rajamani, S. (2006).
Synergy: A new algorithm for property checking (pp. 117–127). Presented at the
FSE: Foundations of Software Engineering, ACM. https://doi.org/10.1145/1181775.1181790'
chicago: 'Gulavani, Bhargav, Thomas A Henzinger, Yamini Kannan, Aditya Nori, and
Sriram Rajamani. “Synergy: A New Algorithm for Property Checking,” 117–27. ACM,
2006. https://doi.org/10.1145/1181775.1181790.'
ieee: 'B. Gulavani, T. A. Henzinger, Y. Kannan, A. Nori, and S. Rajamani, “Synergy:
A new algorithm for property checking,” presented at the FSE: Foundations of Software
Engineering, 2006, pp. 117–127.'
ista: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. 2006. Synergy: A
new algorithm for property checking. FSE: Foundations of Software Engineering,
117–127.'
mla: 'Gulavani, Bhargav, et al. Synergy: A New Algorithm for Property Checking.
ACM, 2006, pp. 117–27, doi:10.1145/1181775.1181790.'
short: B. Gulavani, T.A. Henzinger, Y. Kannan, A. Nori, S. Rajamani, in:, ACM, 2006,
pp. 117–127.
conference:
name: 'FSE: Foundations of Software Engineering'
date_created: 2018-12-11T12:09:18Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:26Z
day: '01'
doi: 10.1145/1181775.1181790
extern: 1
month: '01'
page: 117 - 127
publication_status: published
publisher: ACM
publist_id: '206'
quality_controlled: 0
status: public
title: 'Synergy: A new algorithm for property checking'
type: conference
year: '2006'
...
---
_id: '4526'
abstract:
- lang: eng
text: 'We designed and implemented a new programming language called Hierarchical
Timing Language (HTL) for hard realtime systems. Critical timing constraints are
specified within the language,and ensured by the compiler. Programs in HTL are
extensible in two dimensions without changing their timing behavior: new program
modules can be added, and individual program tasks can be refined. The mechanism
supporting time invariance under parallel composition is that different program
modules communicate at specified instances of time. Time invariance under refinement
is achieved by conservative scheduling of the top level. HTL is a coordination
language, in that individual tasks can be implemented in "foreign" languages.
As a case study, we present a distributed HTL implementation of an automotive
steer-by-wire controller.'
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Daniel
full_name: Iercan, Daniel
last_name: Iercan
- first_name: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
- first_name: Alberto
full_name: Sangiovanni-Vincentelli, Alberto
last_name: Sangiovanni Vincentelli
citation:
ama: 'Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. A hierarchical
coordination language for interacting real-time tasks. In: ACM; 2006:132-141.
doi:10.1145/1176887.1176907'
apa: 'Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., & Sangiovanni Vincentelli,
A. (2006). A hierarchical coordination language for interacting real-time tasks
(pp. 132–141). Presented at the EMSOFT: Embedded Software , ACM. https://doi.org/10.1145/1176887.1176907'
chicago: Ghosal, Arkadeb, Thomas A Henzinger, Daniel Iercan, Christoph Kirsch, and
Alberto Sangiovanni Vincentelli. “A Hierarchical Coordination Language for Interacting
Real-Time Tasks,” 132–41. ACM, 2006. https://doi.org/10.1145/1176887.1176907.
ieee: 'A. Ghosal, T. A. Henzinger, D. Iercan, C. Kirsch, and A. Sangiovanni Vincentelli,
“A hierarchical coordination language for interacting real-time tasks,” presented
at the EMSOFT: Embedded Software , 2006, pp. 132–141.'
ista: 'Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. 2006.
A hierarchical coordination language for interacting real-time tasks. EMSOFT:
Embedded Software , 132–141.'
mla: Ghosal, Arkadeb, et al. A Hierarchical Coordination Language for Interacting
Real-Time Tasks. ACM, 2006, pp. 132–41, doi:10.1145/1176887.1176907.
short: A. Ghosal, T.A. Henzinger, D. Iercan, C. Kirsch, A. Sangiovanni Vincentelli,
in:, ACM, 2006, pp. 132–141.
conference:
name: 'EMSOFT: Embedded Software '
date_created: 2018-12-11T12:09:18Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:27Z
day: '01'
doi: 10.1145/1176887.1176907
extern: 1
month: '01'
page: 132 - 141
publication_status: published
publisher: ACM
publist_id: '201'
quality_controlled: 0
status: public
title: A hierarchical coordination language for interacting real-time tasks
type: conference
year: '2006'
...
---
_id: '4528'
abstract:
- lang: eng
text: Computational modeling of biological systems is becoming increasingly common
as scientists attempt to understand biological phenomena in their full complexity.
Here we distinguish between two types of biological models mathematical and computational
- according to their different representations of biological phenomena and their
diverse potential. We call the approach of constructing computational models of
biological systems executable biology, as it focuses on the design of executable
computer algorithms that mimic biological phenomena. We give an overview of the
main modeling efforts in this direction, and discuss some of the new challenges
that executable biology poses for computer science and biology. We argue that
for executable biology to reach its full potential as a mainstream biological
technique, formal and algorithmic approaches must be integrated into biological
research, driving biology towards a more precise engineering discipline.
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Fisher J, Henzinger TA. Executable biology. In: IEEE; 2006:1675-1682. doi:10.1109/WSC.2006.322942'
apa: 'Fisher, J., & Henzinger, T. A. (2006). Executable biology (pp. 1675–1682).
Presented at the WSC: Winter Simulation Conference, IEEE. https://doi.org/10.1109/WSC.2006.322942'
chicago: Fisher, Jasmin, and Thomas A Henzinger. “Executable Biology,” 1675–82.
IEEE, 2006. https://doi.org/10.1109/WSC.2006.322942.
ieee: 'J. Fisher and T. A. Henzinger, “Executable biology,” presented at the WSC:
Winter Simulation Conference, 2006, pp. 1675–1682.'
ista: 'Fisher J, Henzinger TA. 2006. Executable biology. WSC: Winter Simulation
Conference, 1675–1682.'
mla: Fisher, Jasmin, and Thomas A. Henzinger. Executable Biology. IEEE, 2006,
pp. 1675–82, doi:10.1109/WSC.2006.322942.
short: J. Fisher, T.A. Henzinger, in:, IEEE, 2006, pp. 1675–1682.
conference:
name: 'WSC: Winter Simulation Conference'
date_created: 2018-12-11T12:09:19Z
date_published: 2006-12-03T00:00:00Z
date_updated: 2021-01-12T07:59:28Z
day: '03'
doi: 10.1109/WSC.2006.322942
extern: 1
month: '12'
page: 1675 - 1682
publication_status: published
publisher: IEEE
publist_id: '197'
quality_controlled: 0
status: public
title: Executable biology
type: conference
year: '2006'
...
---
_id: '4538'
abstract:
- lang: eng
text: A stochastic graph game is played by two players on a game graph with probabilistic
transitions. We consider stochastic graph games with ω-regular winning conditions
specified as parity objectives. These games lie in NP ∩ coNP. We present a strategy
improvement algorithm for stochastic parity games; this is the first non-brute-force
algorithm for solving these games. From the strategy improvement algorithm we
obtain a randomized subexponential-time algorithm to solve such games.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Henzinger TA. Strategy improvement and randomized subexponential
algorithms for stochastic parity games. In: Vol 3884. Springer; 2006:512-523.
doi:10.1007/11672142_42'
apa: 'Chatterjee, K., & Henzinger, T. A. (2006). Strategy improvement and randomized
subexponential algorithms for stochastic parity games (Vol. 3884, pp. 512–523).
Presented at the STACS: Theoretical Aspects of Computer Science, Springer. https://doi.org/10.1007/11672142_42'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Strategy Improvement and
Randomized Subexponential Algorithms for Stochastic Parity Games,” 3884:512–23.
Springer, 2006. https://doi.org/10.1007/11672142_42.
ieee: 'K. Chatterjee and T. A. Henzinger, “Strategy improvement and randomized subexponential
algorithms for stochastic parity games,” presented at the STACS: Theoretical Aspects
of Computer Science, 2006, vol. 3884, pp. 512–523.'
ista: 'Chatterjee K, Henzinger TA. 2006. Strategy improvement and randomized subexponential
algorithms for stochastic parity games. STACS: Theoretical Aspects of Computer
Science, LNCS, vol. 3884, 512–523.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Strategy Improvement and
Randomized Subexponential Algorithms for Stochastic Parity Games. Vol. 3884,
Springer, 2006, pp. 512–23, doi:10.1007/11672142_42.
short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 512–523.
conference:
name: 'STACS: Theoretical Aspects of Computer Science'
date_created: 2018-12-11T12:09:22Z
date_published: 2006-02-14T00:00:00Z
date_updated: 2021-01-12T07:59:32Z
day: '14'
doi: 10.1007/11672142_42
extern: 1
intvolume: ' 3884'
month: '02'
page: 512 - 523
publication_status: published
publisher: Springer
publist_id: '184'
quality_controlled: 0
status: public
title: Strategy improvement and randomized subexponential algorithms for stochastic
parity games
type: conference
volume: 3884
year: '2006'
...
---
_id: '4539'
abstract:
- lang: eng
text: Games on graphs with ω-regular objectives provide a model for the control
and synthesis of reactive systems. Every ω-regular objective can be decomposed
into a safety part and a liveness part. The liveness part ensures that something
good happens “eventually.” Two main strengths of the classical, infinite-limit
formulation of liveness are robustness (independence from the granularity of transitions)
and simplicity (abstraction of complicated time bounds). However, the classical
liveness formulation suffers from the drawback that the time until something good
happens may be unbounded. A stronger formulation of liveness, so-called finitary
liveness, overcomes this drawback, while still retaining robustness and simplicity.
Finitary liveness requires that there exists an unknown, fixed bound b such that
something good happens within b transitions. While for one-shot liveness (reachability)
objectives, classical and finitary liveness coincide, for repeated liveness (Büchi)
objectives, the finitary formulation is strictly stronger. In this work we study
games with finitary parity and Streett (fairness) objectives. We prove the determinacy
of these games, present algorithms for solving these games, and characterize the
memory requirements of winning strategies. Our algorithms can be used, for example,
for synthesizing controllers that do not let the response time of a system increase
without bound.
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327
and the NSF ITR grant CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Henzinger TA. Finitary winning in omega-regular games. In: Vol
3920. Springer; 2006:257-271. doi:10.1007/11691372_17'
apa: 'Chatterjee, K., & Henzinger, T. A. (2006). Finitary winning in omega-regular
games (Vol. 3920, pp. 257–271). Presented at the TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, Springer. https://doi.org/10.1007/11691372_17'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Finitary Winning in Omega-Regular
Games,” 3920:257–71. Springer, 2006. https://doi.org/10.1007/11691372_17.
ieee: 'K. Chatterjee and T. A. Henzinger, “Finitary winning in omega-regular games,”
presented at the TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, 2006, vol. 3920, pp. 257–271.'
ista: 'Chatterjee K, Henzinger TA. 2006. Finitary winning in omega-regular games.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 3920, 257–271.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Finitary Winning in Omega-Regular
Games. Vol. 3920, Springer, 2006, pp. 257–71, doi:10.1007/11691372_17.
short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 257–271.
conference:
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
date_created: 2018-12-11T12:09:22Z
date_published: 2006-03-15T00:00:00Z
date_updated: 2021-01-12T07:59:32Z
day: '15'
doi: 10.1007/11691372_17
extern: 1
intvolume: ' 3920'
month: '03'
page: 257 - 271
publication_status: published
publisher: Springer
publist_id: '183'
quality_controlled: 0
status: public
title: Finitary winning in omega-regular games
type: conference
volume: 3920
year: '2006'
...