---
_id: '4237'
abstract:
- lang: eng
text: The growth function of populations is central in biomathematics. The main
dogma is the existence of density-dependence mechanisms, which can be modelled
with distinct functional forms that depend on the size of the Population. One
important class of regulatory functions is the theta-logistic, which generalizes
the logistic equation. Using this model as a motivation, this paper introduces
a simple dynamical reformulation that generalizes many growth functions. The reformulation
consists of two equations, one for population size, and one for the growth rate.
Furthermore, the model shows that although population is density-dependent, the
dynamics of the growth rate does not depend either on population size, nor on
the carrying capacity. Actually, the growth equation is uncoupled from the population
size equation, and the model has only two parameters, a Malthusian parameter rho
and a competition coefficient theta. Distinct sign combinations of these parameters
reproduce not only the family of theta-logistics, but also the van Bertalanffy,
Gompertz and Potential Growth equations, among other possibilities. It is also
shown that, except for two critical points, there is a general size-scaling relation
that includes those appearing in the most important allometric theories, including
the recently proposed Metabolic Theory of Ecology. With this model, several issues
of general interest are discussed such as the growth of animal population, extinctions,
cell growth and allometry, and the effect of environment over a population. (c)
2005 Elsevier Ltd. All rights reserved.
article_processing_charge: No
author:
- first_name: Harold
full_name: de Vladar, Harold
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: de Vladar
orcid: 0000-0002-5985-7653
citation:
ama: de Vladar H. Density-dependence as a size-independent regulatory mechanism.
Journal of Theoretical Biology. 2006;238(2):245-256. doi:3802
apa: de Vladar, H. (2006). Density-dependence as a size-independent regulatory mechanism.
Journal of Theoretical Biology. Elsevier. https://doi.org/3802
chicago: Vladar, Harold de. “Density-Dependence as a Size-Independent Regulatory
Mechanism.” Journal of Theoretical Biology. Elsevier, 2006. https://doi.org/3802.
ieee: H. de Vladar, “Density-dependence as a size-independent regulatory mechanism,”
Journal of Theoretical Biology, vol. 238, no. 2. Elsevier, pp. 245–256,
2006.
ista: de Vladar H. 2006. Density-dependence as a size-independent regulatory mechanism.
Journal of Theoretical Biology. 238(2), 245–256.
mla: de Vladar, Harold. “Density-Dependence as a Size-Independent Regulatory Mechanism.”
Journal of Theoretical Biology, vol. 238, no. 2, Elsevier, 2006, pp. 245–56,
doi:3802.
short: H. de Vladar, Journal of Theoretical Biology 238 (2006) 245–256.
date_created: 2018-12-11T12:07:46Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:31Z
day: '01'
doi: '3802'
extern: '1'
intvolume: ' 238'
issue: '2'
language:
- iso: eng
month: '01'
oa_version: None
page: 245 - 256
publication: Journal of Theoretical Biology
publication_status: published
publisher: Elsevier
publist_id: '1878'
status: public
title: Density-dependence as a size-independent regulatory mechanism
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 238
year: '2006'
...
---
_id: '4235'
author:
- first_name: Harold
full_name: Harold Vladar
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: Vladar
orcid: 0000-0002-5985-7653
- first_name: J.
full_name: González,J. A
last_name: González
citation:
ama: de Vladar H, González J. Dynamic response of cancer under the influence of
immunological activity and therapy. Journal of Theoretical Biology. 2006:91-109.
apa: de Vladar, H., & González, J. (2006). Dynamic response of cancer under
the influence of immunological activity and therapy. Journal of Theoretical
Biology. Elsevier.
chicago: Vladar, Harold de, and J. González. “Dynamic Response of Cancer under the
Influence of Immunological Activity and Therapy.” Journal of Theoretical Biology.
Elsevier, 2006.
ieee: H. de Vladar and J. González, “Dynamic response of cancer under the influence
of immunological activity and therapy,” Journal of Theoretical Biology.
Elsevier, pp. 91–109, 2006.
ista: de Vladar H, González J. 2006. Dynamic response of cancer under the influence
of immunological activity and therapy. Journal of Theoretical Biology., 91–109.
mla: de Vladar, Harold, and J. González. “Dynamic Response of Cancer under the Influence
of Immunological Activity and Therapy.” Journal of Theoretical Biology,
Elsevier, 2006, pp. 91–109.
short: H. de Vladar, J. González, Journal of Theoretical Biology (2006) 91–109.
date_created: 2018-12-11T12:07:45Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:30Z
day: '01'
extern: 1
month: '01'
page: 91 - 109
publication: Journal of Theoretical Biology
publication_status: published
publisher: Elsevier
publist_id: '1879'
quality_controlled: 0
status: public
title: Dynamic response of cancer under the influence of immunological activity and
therapy
type: journal_article
year: '2006'
...
---
_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: '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: '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: '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: '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: '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: '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: '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: '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: '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'
...
---
_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: '4551'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) with multiple discounted reward
objectives. Such MDPs occur in design problems where one wishes to simultaneously
optimize several criteria, for example, latency and power. The possible trade-offs
between the different objectives are characterized by the Pareto curve. We show
that every Pareto-optimal point can be achieved by a memoryless strategy; however,
unlike in the single-objective case, the memoryless strategy may require randomization.
Moreover, we show that the Pareto curve can be approximated in polynomial time
in the size of the MDP. Additionally, we study the problem if a given value vector
is realizable by any strategy, and show that it can be decided in polynomial time;
but the question whether it is realizable by a deterministic memoryless strategy
is NP-complete. These results provide efficient algorithms for design exploration
in MDP models with multiple objectives.\nThis research was supported in part by
the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690,
and CCR-0427202. "
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327,
and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202.
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: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- 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, Majumdar R, Henzinger TA. Markov decision processes with multiple
objectives. In: Vol 3884. Springer; 2006:325-336. doi:10.1007/11672142_26'
apa: 'Chatterjee, K., Majumdar, R., & Henzinger, T. A. (2006). Markov decision
processes with multiple objectives (Vol. 3884, pp. 325–336). Presented at the
STACS: Theoretical Aspects of Computer Science, Springer. https://doi.org/10.1007/11672142_26'
chicago: Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Markov
Decision Processes with Multiple Objectives,” 3884:325–36. Springer, 2006. https://doi.org/10.1007/11672142_26.
ieee: 'K. Chatterjee, R. Majumdar, and T. A. Henzinger, “Markov decision processes
with multiple objectives,” presented at the STACS: Theoretical Aspects of Computer
Science, 2006, vol. 3884, pp. 325–336.'
ista: 'Chatterjee K, Majumdar R, Henzinger TA. 2006. Markov decision processes with
multiple objectives. STACS: Theoretical Aspects of Computer Science, LNCS, vol.
3884, 325–336.'
mla: Chatterjee, Krishnendu, et al. Markov Decision Processes with Multiple Objectives.
Vol. 3884, Springer, 2006, pp. 325–36, doi:10.1007/11672142_26.
short: K. Chatterjee, R. Majumdar, T.A. Henzinger, in:, Springer, 2006, pp. 325–336.
conference:
name: 'STACS: Theoretical Aspects of Computer Science'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-02-14T00:00:00Z
date_updated: 2021-01-12T07:59:38Z
day: '14'
doi: 10.1007/11672142_26
extern: 1
intvolume: ' 3884'
month: '02'
page: 325 - 336
publication_status: published
publisher: Springer
publist_id: '161'
quality_controlled: 0
status: public
title: Markov decision processes with multiple objectives
type: conference
volume: 3884
year: '2006'
...