---
_id: '4249'
abstract:
- lang: eng
text: We examined causes of speciation in asexual populations in both sympatry and
parapatry, providing an alternative explanation for the speciation patterns reported
by Dieckmann and Doebeli (1999) and Doebeli and Dieckmann (2003). Both in sympatry
and parapatry, they find that speciation occurs relatively easily. We reveal that
in the sympatric clonal model, the equilibrium distribution is continuous and
the disruptive selection driving evolution of discrete clusters is only transient.
Hence, if discrete phenotypes are to remain stable in the sympatric sexual model,
there should be some source of nontransient disruptive selection that will drive
evolution of assortment. We analyze sexually reproducing populations using the
Bulmer’s infinitesimal model and show that cost-free assortment alone leads to
speciation and disruptive selection only arises when the optimal distribution
cannot be matched—in this example, because the phenotypic range is limited. In
addition, Doebeli and Dieckmann’s analyses assumed a high genetic variance and
a high mutation rate. Thus, these theoretical models do not support the conclusion
that sympatric speciation is a likely outcome of competition for resources. In
their parapatric model (Doebeli and Dieckmann 2003), clustering into distinct
phenotypes is driven by edge effects, rather than by frequency-dependent competition.
author:
- first_name: Jitka
full_name: Jitka Polechova
id: 3BBFB084-F248-11E8-B48F-1D18A9856A87
last_name: Polechova
orcid: 0000-0003-0951-3112
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: 'Polechova J, Barton NH. Speciation through competition: A critical review.
Evolution; International Journal of Organic Evolution. 2005;59(6):1194-1210.
doi:10.1111/j.0014-3820.2005.tb01771.x'
apa: 'Polechova, J., & Barton, N. H. (2005). Speciation through competition:
A critical review. Evolution; International Journal of Organic Evolution.
Wiley-Blackwell. https://doi.org/10.1111/j.0014-3820.2005.tb01771.x'
chicago: 'Polechova, Jitka, and Nicholas H Barton. “Speciation through Competition:
A Critical Review.” Evolution; International Journal of Organic Evolution.
Wiley-Blackwell, 2005. https://doi.org/10.1111/j.0014-3820.2005.tb01771.x.'
ieee: 'J. Polechova and N. H. Barton, “Speciation through competition: A critical
review,” Evolution; International Journal of Organic Evolution, vol. 59,
no. 6. Wiley-Blackwell, pp. 1194–1210, 2005.'
ista: 'Polechova J, Barton NH. 2005. Speciation through competition: A critical
review. Evolution; International Journal of Organic Evolution. 59(6), 1194–1210.'
mla: 'Polechova, Jitka, and Nicholas H. Barton. “Speciation through Competition:
A Critical Review.” Evolution; International Journal of Organic Evolution,
vol. 59, no. 6, Wiley-Blackwell, 2005, pp. 1194–210, doi:10.1111/j.0014-3820.2005.tb01771.x.'
short: J. Polechova, N.H. Barton, Evolution; International Journal of Organic Evolution
59 (2005) 1194–1210.
date_created: 2018-12-11T12:07:50Z
date_published: 2005-06-01T00:00:00Z
date_updated: 2021-01-12T07:55:36Z
day: '01'
doi: 10.1111/j.0014-3820.2005.tb01771.x
extern: 1
intvolume: ' 59'
issue: '6'
month: '06'
page: 1194 - 1210
publication: Evolution; International Journal of Organic Evolution
publication_status: published
publisher: Wiley-Blackwell
publist_id: '1849'
quality_controlled: 0
status: public
title: 'Speciation through competition: A critical review'
type: journal_article
volume: 59
year: '2005'
...
---
_id: '4251'
abstract:
- lang: eng
text: In finite populations subject to selection, genetic drift generates negative
linkage disequilibrium, on average, even if selection acts independently (i.e.
multiplicatively) upon all loci. Negative disequilibrium reduces the variance
in fitness and hence, by FISHER's Fundamental Theorem (1930), slows the rate of
increase in mean fitness. Modifiers that increase recombination eliminate the
negative disequilibria that impede selection and consequently increase in frequency
by 'hitch-hiking'. In addition, recombinant progeny are more fit on average than
non-recombinant progeny when there is negative linkage disequilibrium and loci
interact multiplicatively. For both these reasons, stochastic fluctuations in
linkage disequilibrium in finite populations favor the evolution of increased
rates of recombination, even in the absence of epistatic interactions among loci
and even when disequilibrium is initially absent. The method developed within
this paper quantifies the strength of selection on a modifier allele that increases
recombination due to stochastically generated linkage disequilibria. The analysis
indicates that, in a population subject to multiplicative selection, genetic associations
generated by drift do select for increased recombination, a result that is confirmed
by Monte Carlo simulations. Selection for a modifier that increases recombination
is highest when linkage among all loci is tight, when beneficial alleles rise
from low to high frequency, and when the population size is small.
author:
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
- first_name: Sarah
full_name: Otto, Sarah P
last_name: Otto
citation:
ama: Barton NH, Otto S. Evolution of recombination due to random drift. Genetics.
2005;169(4):2353-2370. doi:10.1534/genetics.104.032821
apa: Barton, N. H., & Otto, S. (2005). Evolution of recombination due to random
drift. Genetics. Genetics Society of America. https://doi.org/10.1534/genetics.104.032821
chicago: Barton, Nicholas H, and Sarah Otto. “Evolution of Recombination Due to
Random Drift.” Genetics. Genetics Society of America, 2005. https://doi.org/10.1534/genetics.104.032821.
ieee: N. H. Barton and S. Otto, “Evolution of recombination due to random drift,”
Genetics, vol. 169, no. 4. Genetics Society of America, pp. 2353–2370,
2005.
ista: Barton NH, Otto S. 2005. Evolution of recombination due to random drift. Genetics.
169(4), 2353–2370.
mla: Barton, Nicholas H., and Sarah Otto. “Evolution of Recombination Due to Random
Drift.” Genetics, vol. 169, no. 4, Genetics Society of America, 2005, pp.
2353–70, doi:10.1534/genetics.104.032821.
short: N.H. Barton, S. Otto, Genetics 169 (2005) 2353–2370.
date_created: 2018-12-11T12:07:51Z
date_published: 2005-03-01T00:00:00Z
date_updated: 2021-01-12T07:55:37Z
day: '01'
doi: 10.1534/genetics.104.032821
extern: 1
intvolume: ' 169'
issue: '4'
month: '03'
page: 2353 - 2370
publication: Genetics
publication_status: published
publisher: Genetics Society of America
publist_id: '1846'
quality_controlled: 0
status: public
title: Evolution of recombination due to random drift
type: journal_article
volume: 169
year: '2005'
...
---
_id: '4252'
abstract:
- lang: eng
text: Empirical studies of quantitative genetic variation have revealed robust patterns
that are observed both across traits and across species. However, these patterns
have no compelling explanation, and some of the observations even appear to be
mutually incompatible. We review and extend a major class of theoretical models,
‘mutation–selection models’, that have been proposed to explain quantitative genetic
variation. We also briefly review an alternative class of ‘balancing selection
models’. We consider to what extent the models are compatible with the general
observations, and argue that a key issue is understanding and modelling pleiotropy.
We discuss some
author:
- first_name: Toby
full_name: Johnson, Toby
last_name: Johnson
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Johnson T, Barton NH. Theoretical models of selection and mutationon quantitative
traits. Philosophical Transactions of the Royal Society of London Series B,
Biological Sciences. 2005;360(1459):1411-1425. doi:10.1098/rstb.2005.1667
apa: Johnson, T., & Barton, N. H. (2005). Theoretical models of selection and
mutationon quantitative traits. Philosophical Transactions of the Royal Society
of London. Series B, Biological Sciences. Royal Society, The. https://doi.org/10.1098/rstb.2005.1667
chicago: Johnson, Toby, and Nicholas H Barton. “Theoretical Models of Selection
and Mutationon Quantitative Traits.” Philosophical Transactions of the Royal
Society of London. Series B, Biological Sciences. Royal Society, The, 2005.
https://doi.org/10.1098/rstb.2005.1667.
ieee: T. Johnson and N. H. Barton, “Theoretical models of selection and mutationon
quantitative traits,” Philosophical Transactions of the Royal Society of London.
Series B, Biological Sciences, vol. 360, no. 1459. Royal Society, The, pp.
1411–1425, 2005.
ista: Johnson T, Barton NH. 2005. Theoretical models of selection and mutationon
quantitative traits. Philosophical Transactions of the Royal Society of London.
Series B, Biological Sciences. 360(1459), 1411–1425.
mla: Johnson, Toby, and Nicholas H. Barton. “Theoretical Models of Selection and
Mutationon Quantitative Traits.” Philosophical Transactions of the Royal Society
of London. Series B, Biological Sciences, vol. 360, no. 1459, Royal Society,
The, 2005, pp. 1411–25, doi:10.1098/rstb.2005.1667.
short: T. Johnson, N.H. Barton, Philosophical Transactions of the Royal Society
of London. Series B, Biological Sciences 360 (2005) 1411–1425.
date_created: 2018-12-11T12:07:51Z
date_published: 2005-07-29T00:00:00Z
date_updated: 2021-01-12T07:55:38Z
day: '29'
doi: 10.1098/rstb.2005.1667
extern: 1
intvolume: ' 360'
issue: '1459'
main_file_link:
- open_access: '1'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC1569515/
month: '07'
oa: 1
page: 1411 - 1425
publication: Philosophical Transactions of the Royal Society of London. Series B,
Biological Sciences
publication_status: published
publisher: Royal Society, The
publist_id: '1847'
quality_controlled: 0
status: public
title: Theoretical models of selection and mutationon quantitative traits
type: journal_article
volume: 360
year: '2005'
...
---
_id: '4367'
alternative_title:
- LNCS 3672
author:
- first_name: Andreas
full_name: Podelski,Andreas
last_name: Podelski
- first_name: Thomas
full_name: Thomas Wies
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Podelski A, Wies T. Boolean Heaps. In: Springer; 2005:267-282. doi:1550'
apa: 'Podelski, A., & Wies, T. (2005). Boolean Heaps (pp. 267–282). Presented
at the SAS: Static Analysis Symposium, Springer. https://doi.org/1550'
chicago: Podelski, Andreas, and Thomas Wies. “Boolean Heaps,” 267–82. Springer,
2005. https://doi.org/1550.
ieee: 'A. Podelski and T. Wies, “Boolean Heaps,” presented at the SAS: Static Analysis
Symposium, 2005, pp. 267–282.'
ista: 'Podelski A, Wies T. 2005. Boolean Heaps. SAS: Static Analysis Symposium,
LNCS 3672, , 267–282.'
mla: Podelski, Andreas, and Thomas Wies. Boolean Heaps. Springer, 2005, pp.
267–82, doi:1550.
short: A. Podelski, T. Wies, in:, Springer, 2005, pp. 267–282.
conference:
name: 'SAS: Static Analysis Symposium'
date_created: 2018-12-11T12:08:29Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:27Z
day: '01'
doi: '1550'
extern: 1
month: '01'
page: 267 - 282
publication_status: published
publisher: Springer
publist_id: '1092'
quality_controlled: 0
status: public
title: Boolean Heaps
type: conference
year: '2005'
...
---
_id: '4404'
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: P.
full_name: Madhusudan,P.
last_name: Madhusudan
- first_name: Wonhong
full_name: Nam,Wonhong
last_name: Nam
citation:
ama: 'Alur R, Cerny P, Madhusudan P, Nam W. Synthesis of interface specifications
for Java classes. In: ACM; 2005:98-109. doi:1542'
apa: 'Alur, R., Cerny, P., Madhusudan, P., & Nam, W. (2005). Synthesis of interface
specifications for Java classes (pp. 98–109). Presented at the POPL: Principles
of Programming Languages, ACM. https://doi.org/1542'
chicago: Alur, Rajeev, Pavol Cerny, P. Madhusudan, and Wonhong Nam. “Synthesis of
Interface Specifications for Java Classes,” 98–109. ACM, 2005. https://doi.org/1542.
ieee: 'R. Alur, P. Cerny, P. Madhusudan, and W. Nam, “Synthesis of interface specifications
for Java classes,” presented at the POPL: Principles of Programming Languages,
2005, pp. 98–109.'
ista: 'Alur R, Cerny P, Madhusudan P, Nam W. 2005. Synthesis of interface specifications
for Java classes. POPL: Principles of Programming Languages, 98–109.'
mla: Alur, Rajeev, et al. Synthesis of Interface Specifications for Java Classes.
ACM, 2005, pp. 98–109, doi:1542.
short: R. Alur, P. Cerny, P. Madhusudan, W. Nam, in:, ACM, 2005, pp. 98–109.
conference:
name: 'POPL: Principles of Programming Languages'
date_created: 2018-12-11T12:08:41Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:44Z
day: '01'
doi: '1542'
extern: 1
month: '01'
page: 98 - 109
publication_status: published
publisher: ACM
publist_id: '1053'
quality_controlled: 0
status: public
title: Synthesis of interface specifications for Java classes
type: conference
year: '2005'
...
---
_id: '4412'
abstract:
- lang: eng
text: The periodic resource model for hierarchical, compositional scheduling abstracts
task groups by resource requirements. We study this model in the presence of dataflow
constraints between the tasks within a group (intragroup dependencies), and between
tasks in different groups (inter-group dependencies). We consider two natural
semantics for dataflow constraints, namely, RTW (real-time workshop) semantics
and LET (logical execution time) semantics. We show that while RTW semantics offers
better end-to-end latency on the task group level, LET semantics allows tighter
resource bounds in the abstraction hierarchy and therefore provides better composability
properties. This result holds both for intragroup and intergroup dependencies,
as well as for shared and for distributed resources.
author:
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Matic S, Henzinger TA. Trading end-to-end latency for composability. In: IEEE;
2005:99-110. doi:10.1109/RTSS.2005.43'
apa: 'Matic, S., & Henzinger, T. A. (2005). Trading end-to-end latency for composability
(pp. 99–110). Presented at the RTSS: Real-Time Systems Symposium, IEEE. https://doi.org/10.1109/RTSS.2005.43'
chicago: Matic, Slobodan, and Thomas A Henzinger. “Trading End-to-End Latency for
Composability,” 99–110. IEEE, 2005. https://doi.org/10.1109/RTSS.2005.43.
ieee: 'S. Matic and T. A. Henzinger, “Trading end-to-end latency for composability,”
presented at the RTSS: Real-Time Systems Symposium, 2005, pp. 99–110.'
ista: 'Matic S, Henzinger TA. 2005. Trading end-to-end latency for composability.
RTSS: Real-Time Systems Symposium, 99–110.'
mla: Matic, Slobodan, and Thomas A. Henzinger. Trading End-to-End Latency for
Composability. IEEE, 2005, pp. 99–110, doi:10.1109/RTSS.2005.43.
short: S. Matic, T.A. Henzinger, in:, IEEE, 2005, pp. 99–110.
conference:
name: 'RTSS: Real-Time Systems Symposium'
date_created: 2018-12-11T12:08:43Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:47Z
day: '01'
doi: 10.1109/RTSS.2005.43
extern: 1
month: '01'
page: 99 - 110
publication_status: published
publisher: IEEE
publist_id: '317'
quality_controlled: 0
status: public
title: Trading end-to-end latency for composability
type: conference
year: '2005'
...
---
_id: '4418'
abstract:
- lang: eng
text: 'We present a new software system architecture for the implementation of hard
real-time applications. The core of the system is a microkernel whose reactivity
(interrupt handling as in synchronous reactive programs) and proactivity (task
scheduling as in traditional RTOSs) are fully programmable. The microkernel, which
we implemented on a StrongARM processor, consists of two interacting domain-specific
virtual machines, a reactive E (Embedded) machine and a proactive S (Scheduling)
machine. The microkernel code (or microcode) that runs on the microkernel is partitioned
into E and S code. E code manages the interaction of the system with the physical
environment: the execution of E code is triggered by environment interrupts, which
signal external events such as the arrival of a message or sensor value, and it
releases application tasks to the S machine. S code manages the interaction of
the system with the processor: the execution of S code is triggered by hardware
interrupts, which signal internal events such as the completion of a task or time
slice, and it dispatches application tasks to the CPU, possibly preempting a running
task. This partition of the system orthogonalizes the two main concerns of real-time
implementations: E code refers to environment time and thus defines the reactivity
of the system in a hardware- and scheduler-independent fashion; S code refers
to CPU time and defines a system scheduler. If both time lines can be reconciled,
then the code is called time safe; violations of time safety are handled again
in a programmable way, by run-time exceptions. The separation of E from S code
permits the independent programming, verification, optimization, composition,
dynamic adaptation, and reuse of both reaction and scheduling mechanisms. Our
measurements show that the system overhead is very acceptable even for large sets
of task, generally in the 0.2--0.3% range.'
author:
- first_name: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
- first_name: Marco
full_name: Sanvido, Marco A
last_name: Sanvido
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Kirsch C, Sanvido M, Henzinger TA. A programmable microkernel for real-time
systems. In: ACM; 2005:35-45. doi:10.1145/1064979.1064986'
apa: 'Kirsch, C., Sanvido, M., & Henzinger, T. A. (2005). A programmable microkernel
for real-time systems (pp. 35–45). Presented at the VEE: Virtual Execution Environments,
ACM. https://doi.org/10.1145/1064979.1064986'
chicago: Kirsch, Christoph, Marco Sanvido, and Thomas A Henzinger. “A Programmable
Microkernel for Real-Time Systems,” 35–45. ACM, 2005. https://doi.org/10.1145/1064979.1064986.
ieee: 'C. Kirsch, M. Sanvido, and T. A. Henzinger, “A programmable microkernel for
real-time systems,” presented at the VEE: Virtual Execution Environments, 2005,
pp. 35–45.'
ista: 'Kirsch C, Sanvido M, Henzinger TA. 2005. A programmable microkernel for real-time
systems. VEE: Virtual Execution Environments, 35–45.'
mla: Kirsch, Christoph, et al. A Programmable Microkernel for Real-Time Systems.
ACM, 2005, pp. 35–45, doi:10.1145/1064979.1064986.
short: C. Kirsch, M. Sanvido, T.A. Henzinger, in:, ACM, 2005, pp. 35–45.
conference:
name: 'VEE: Virtual Execution Environments'
date_created: 2018-12-11T12:08:45Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:49Z
day: '01'
doi: 10.1145/1064979.1064986
extern: 1
month: '01'
page: 35 - 45
publication_status: published
publisher: ACM
publist_id: '311'
quality_controlled: 0
status: public
title: A programmable microkernel for real-time systems
type: conference
year: '2005'
...
---
_id: '4454'
abstract:
- lang: eng
text: We define five increasingly comprehensive classes of infinite-state systems,
called STS1--STS5, whose state spaces have finitary structure. For four of these
classes, we provide examples from hybrid systems.STS1 These are the systems with
finite bisimilarity quotients. They can be analyzed symbolically by iteratively
applying predecessor and Boolean operations on state sets, starting from a finite
number of observable state sets. Any such iteration is guaranteed to terminate
in that only a finite number of state sets can be generated. This enables model
checking of the μ-calculus.STS2 These are the systems with finite similarity quotients.
They can be analyzed symbolically by iterating the predecessor and positive Boolean
operations. This enables model checking of the existential and universal fragments
of the μ-calculus.STS3 These are the systems with finite trace-equivalence quotients.
They can be analyzed symbolically by iterating the predecessor operation and a
restricted form of positive Boolean operations (intersection is restricted to
intersection with observables). This enables model checking of all ω-regular properties,
including linear temporal logic.STS4 These are the systems with finite distance-equivalence
quotients (two states are equivalent if for every distance d, the same observables
can be reached in d transitions). The systems in this class can be analyzed symbolically
by iterating the predecessor operation and terminating when no new state sets
are generated. This enables model checking of the existential conjunction-free
and universal disjunction-free fragments of the μ-calculus.STS5 These are the
systems with finite bounded-reachability quotients (two states are equivalent
if for every distance d, the same observables can be reached in d or fewer transitions).
The systems in this class can be analyzed symbolically by iterating the predecessor
operation and terminating when no new states are encountered (this is a weaker
termination condition than above). This enables model checking of reachability
properties.
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: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Jean
full_name: Raskin, Jean-François
last_name: Raskin
citation:
ama: Henzinger TA, Majumdar R, Raskin J. A classification of symbolic transition
systems. ACM Transactions on Computational Logic (TOCL). 2005;6(1):1-32.
doi:10.1145/1042038.1042039
apa: Henzinger, T. A., Majumdar, R., & Raskin, J. (2005). A classification of
symbolic transition systems. ACM Transactions on Computational Logic (TOCL).
ACM. https://doi.org/10.1145/1042038.1042039
chicago: Henzinger, Thomas A, Ritankar Majumdar, and Jean Raskin. “A Classification
of Symbolic Transition Systems.” ACM Transactions on Computational Logic (TOCL).
ACM, 2005. https://doi.org/10.1145/1042038.1042039.
ieee: T. A. Henzinger, R. Majumdar, and J. Raskin, “A classification of symbolic
transition systems,” ACM Transactions on Computational Logic (TOCL), vol.
6, no. 1. ACM, pp. 1–32, 2005.
ista: Henzinger TA, Majumdar R, Raskin J. 2005. A classification of symbolic transition
systems. ACM Transactions on Computational Logic (TOCL). 6(1), 1–32.
mla: Henzinger, Thomas A., et al. “A Classification of Symbolic Transition Systems.”
ACM Transactions on Computational Logic (TOCL), vol. 6, no. 1, ACM, 2005,
pp. 1–32, doi:10.1145/1042038.1042039.
short: T.A. Henzinger, R. Majumdar, J. Raskin, ACM Transactions on Computational
Logic (TOCL) 6 (2005) 1–32.
date_created: 2018-12-11T12:08:56Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2021-01-12T07:57:05Z
day: '01'
doi: 10.1145/1042038.1042039
extern: 1
intvolume: ' 6'
issue: '1'
month: '01'
page: 1 - 32
publication: ACM Transactions on Computational Logic (TOCL)
publication_status: published
publisher: ACM
publist_id: '272'
quality_controlled: 0
status: public
title: A classification of symbolic transition systems
type: journal_article
volume: 6
year: '2005'
...
---
_id: '4455'
abstract:
- lang: eng
text: We define quantitative similarity functions between timed transition systems
that measure the degree of closeness of two systems as a real, in contrast to
the traditional boolean yes/no approach to timed simulation and language inclusion.
Two systems are close if for each timed trace of one system, there exists a corresponding
timed trace in the other system with the same sequence of events and closely corresponding
event timings. We show that timed CTL is robust with respect to our quantitative
version of bisimilarity, in particular, if a system satisfies a formula, then
every close system satisfies a close formula. We also define a discounted version
of CTL over timed systems, which assigns to every CTL formula a real value that
is obtained by discounting real time. We prove the robustness of discounted CTL
by establishing that close states in the bisimilarity metric have close values
for all discounted CTL formulas.
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327
and the NSF grants CCR-0208875, CCR-0225610, and CCR-0427202.
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: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Vinayak
full_name: Prabhu, Vinayak S
last_name: Prabhu
citation:
ama: 'Henzinger TA, Majumdar R, Prabhu V. Quantifying similarities between timed
systems. In: Vol 3829. Springer; 2005:226-241. doi:10.1007/11603009_18'
apa: 'Henzinger, T. A., Majumdar, R., & Prabhu, V. (2005). Quantifying similarities
between timed systems (Vol. 3829, pp. 226–241). Presented at the FORMATS: Formal
Modeling and Analysis of Timed Systems, Springer. https://doi.org/10.1007/11603009_18'
chicago: Henzinger, Thomas A, Ritankar Majumdar, and Vinayak Prabhu. “Quantifying
Similarities between Timed Systems,” 3829:226–41. Springer, 2005. https://doi.org/10.1007/11603009_18.
ieee: 'T. A. Henzinger, R. Majumdar, and V. Prabhu, “Quantifying similarities between
timed systems,” presented at the FORMATS: Formal Modeling and Analysis of Timed
Systems, 2005, vol. 3829, pp. 226–241.'
ista: 'Henzinger TA, Majumdar R, Prabhu V. 2005. Quantifying similarities between
timed systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol.
3829, 226–241.'
mla: Henzinger, Thomas A., et al. Quantifying Similarities between Timed Systems.
Vol. 3829, Springer, 2005, pp. 226–41, doi:10.1007/11603009_18.
short: T.A. Henzinger, R. Majumdar, V. Prabhu, in:, Springer, 2005, pp. 226–241.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:56Z
date_published: 2005-12-13T00:00:00Z
date_updated: 2021-01-12T07:57:05Z
day: '13'
doi: 10.1007/11603009_18
extern: 1
intvolume: ' 3829'
month: '12'
page: 226 - 241
publication_status: published
publisher: Springer
publist_id: '273'
quality_controlled: 0
status: public
title: Quantifying similarities between timed systems
type: conference
volume: 3829
year: '2005'
...
---
_id: '4456'
abstract:
- lang: eng
text: 'A modular program analysis considers components independently and provides
a succinct summary for each component, which is used when checking the rest of
the system. Consider a system consisting of a library and a client. A temporal
summary, or interface, of the library specifies legal sequences of library calls.
The interface is safe if no call sequence violates the library''s internal invariants;
the interface is permissive if it contains every such sequence. Modular program
analysis requires full interfaces, which are both safe and permissive: the client
does not cause errors in the library if and only if it makes only sequences of
library calls that are allowed by the full interface of the library.Previous interface-based
methods have focused on safe interfaces, which may be too restrictive and thus
reject good clients. We present an algorithm for automatically synthesizing software
interfaces that are both safe and permissive. The algorithm generates interfaces
as graphs whose vertices are labeled with predicates over the library''s internal
state, and whose edges are labeled with library calls. The interface state is
refined incrementally until the full interface is constructed. In other words,
the algorithm automatically synthesizes a typestate system for the library, against
which any client can be checked for compatibility. We present an implementation
of the algorithm which is based on the BLAST model checker, and we evaluate some
case studies.'
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: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R. Permissive interfaces. In: ACM; 2005:31-40.
doi:10.1145/1081706.1081713'
apa: 'Henzinger, T. A., Jhala, R., & Majumdar, R. (2005). Permissive interfaces
(pp. 31–40). Presented at the FSE: Foundations of Software Engineering, ACM. https://doi.org/10.1145/1081706.1081713'
chicago: Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Permissive Interfaces,”
31–40. ACM, 2005. https://doi.org/10.1145/1081706.1081713.
ieee: 'T. A. Henzinger, R. Jhala, and R. Majumdar, “Permissive interfaces,” presented
at the FSE: Foundations of Software Engineering, 2005, pp. 31–40.'
ista: 'Henzinger TA, Jhala R, Majumdar R. 2005. Permissive interfaces. FSE: Foundations
of Software Engineering, 31–40.'
mla: Henzinger, Thomas A., et al. Permissive Interfaces. ACM, 2005, pp. 31–40,
doi:10.1145/1081706.1081713.
short: T.A. Henzinger, R. Jhala, R. Majumdar, in:, ACM, 2005, pp. 31–40.
conference:
name: 'FSE: Foundations of Software Engineering'
date_created: 2018-12-11T12:08:56Z
date_published: 2005-09-01T00:00:00Z
date_updated: 2021-01-12T07:57:06Z
day: '01'
doi: 10.1145/1081706.1081713
extern: 1
month: '09'
page: 31 - 40
publication_status: published
publisher: ACM
publist_id: '274'
quality_controlled: 0
status: public
title: Permissive interfaces
type: conference
year: '2005'
...
---
_id: '4457'
abstract:
- lang: eng
text: We present a compositional approach to the implementation of hard real-time
software running on a distributed platform. We explain how several code suppliers,
coordinated by a system integrator, can independently generate different parts
of the distributed software. The task structure, interaction, and timing is specified
as a Giotto program. Each supplier is given a part of the Giotto program and a
timing interface, from which the supplier generates task and scheduling code.
The integrator then checks, individually for each supplier, in pseudo-polynomial
time, if the supplied code meets its timing specification. If all checks succeed,
then the supplied software parts are guaranteed to work together and implement
the original Giotto program. The feasibility of the approach is demonstrated by
a prototype implementation.
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: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: 'Henzinger TA, Kirsch C, Matic S. Composable code generation for distributed
Giotto. In: ACM; 2005:21-30. doi:10.1145/1065910.1065914'
apa: 'Henzinger, T. A., Kirsch, C., & Matic, S. (2005). Composable code generation
for distributed Giotto (pp. 21–30). Presented at the LCTES: Languages, Compilers,
and Tools for Embedded Systems, ACM. https://doi.org/10.1145/1065910.1065914'
chicago: Henzinger, Thomas A, Christoph Kirsch, and Slobodan Matic. “Composable
Code Generation for Distributed Giotto,” 21–30. ACM, 2005. https://doi.org/10.1145/1065910.1065914.
ieee: 'T. A. Henzinger, C. Kirsch, and S. Matic, “Composable code generation for
distributed Giotto,” presented at the LCTES: Languages, Compilers, and Tools for
Embedded Systems, 2005, pp. 21–30.'
ista: 'Henzinger TA, Kirsch C, Matic S. 2005. Composable code generation for distributed
Giotto. LCTES: Languages, Compilers, and Tools for Embedded Systems, 21–30.'
mla: Henzinger, Thomas A., et al. Composable Code Generation for Distributed
Giotto. ACM, 2005, pp. 21–30, doi:10.1145/1065910.1065914.
short: T.A. Henzinger, C. Kirsch, S. Matic, in:, ACM, 2005, pp. 21–30.
conference:
name: 'LCTES: Languages, Compilers, and Tools for Embedded Systems'
date_created: 2018-12-11T12:08:57Z
date_published: 2005-06-01T00:00:00Z
date_updated: 2021-01-12T07:57:06Z
day: '01'
doi: 10.1145/1065910.1065914
extern: 1
month: '06'
page: 21 - 30
publication_status: published
publisher: ACM
publist_id: '275'
quality_controlled: 0
status: public
title: Composable code generation for distributed Giotto
type: conference
year: '2005'
...
---
_id: '4536'
abstract:
- lang: eng
text: 'We show how to automatically construct and refine rectangular abstractions
of systems of linear differential equations. From a hybrid automaton whose dynamics
are given by a system of linear differential equations, our method computes automatically
a sequence of rectangular hybrid automata that are increasingly precise overapproximations
of the original hybrid automaton. We prove an optimality criterion for successive
refinements. We also show that this method can take into account a safety property
to be verified, refining only relevant parts of the state space. The practicability
of the method is illustrated on a benchmark case study. '
acknowledgement: Supported in part by the AFOSR MURI grant F49620-00-1-0327 and the
NSF grants CCR-0208875 and CCR-0225610.
alternative_title:
- LNCS
author:
- 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: 'Doyen L, Henzinger TA, Raskin J. Automatic rectangular refinement of affine
hybrid systems. In: Vol 3829. Springer; 2005:144-161. doi:DOI: 10.1007/11603009_13'
apa: 'Doyen, L., Henzinger, T. A., & Raskin, J. (2005). Automatic rectangular
refinement of affine hybrid systems (Vol. 3829, pp. 144–161). Presented at the
FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. https://doi.org/DOI: 10.1007/11603009_13'
chicago: 'Doyen, Laurent, Thomas A Henzinger, and Jean Raskin. “Automatic Rectangular
Refinement of Affine Hybrid Systems,” 3829:144–61. Springer, 2005. https://doi.org/DOI: 10.1007/11603009_13.'
ieee: 'L. Doyen, T. A. Henzinger, and J. Raskin, “Automatic rectangular refinement
of affine hybrid systems,” presented at the FORMATS: Formal Modeling and Analysis
of Timed Systems, 2005, vol. 3829, pp. 144–161.'
ista: 'Doyen L, Henzinger TA, Raskin J. 2005. Automatic rectangular refinement of
affine hybrid systems. FORMATS: Formal Modeling and Analysis of Timed Systems,
LNCS, vol. 3829, 144–161.'
mla: 'Doyen, Laurent, et al. Automatic Rectangular Refinement of Affine Hybrid
Systems. Vol. 3829, Springer, 2005, pp. 144–61, doi:DOI: 10.1007/11603009_13.'
short: L. Doyen, T.A. Henzinger, J. Raskin, in:, Springer, 2005, pp. 144–161.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:09:22Z
date_published: 2005-12-13T00:00:00Z
date_updated: 2021-01-12T07:59:31Z
day: '13'
doi: 'DOI: 10.1007/11603009_13'
extern: 1
intvolume: ' 3829'
month: '12'
page: 144 - 161
publication_status: published
publisher: Springer
publist_id: '190'
quality_controlled: 0
status: public
title: Automatic rectangular refinement of affine hybrid systems
type: conference
volume: 3829
year: '2005'
...
---
_id: '4541'
abstract:
- lang: eng
text: |
Much recent research has focused on the applications of games with ω-regular objectives in the control and verification of reactive systems. However, many of the game-based models are ill-suited for these applications, because they assume that each player has complete information about the state of the system (they are “perfect-information” games). This is because in many situations, a controller does not see the private state of the plant. Such scenarios are naturally modeled by “partial-information” games. On the other hand, these games are intractable; for example, partial-information games with simple reachability objectives are 2EXPTIME-complete.
We study the intermediate case of “semiperfect-information” games, where one player has complete knowledge of the state, while the other player has only partial knowledge. This model is appropriate in control situations where a controller must cope with plant behavior that is as adversarial as possible, i.e., the controller has partial information while the plant has perfect information. As is customary, we assume that the controller and plant take turns to make moves. We show that these semiperfect-information turn-based games are equivalent to perfect-information concurrent games, where the two players choose their moves simultaneously and independently. Since the perfect-information concurrent games are well-understood, we obtain several results of how semiperfect-information turn-based games differ from perfect-information turn-based games on one hand, and from partial-information turn-based games on the other hand. In particular, semiperfect-information turn-based games can benefit from randomized strategies while the perfect-information variety cannot, and semiperfect-information turn-based games are in NP ∩ coNP for all parity objectives.
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. Semiperfect-information games. In: Vol 3821. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2005:1-18. doi:10.1007/11590156_1'
apa: 'Chatterjee, K., & Henzinger, T. A. (2005). Semiperfect-information games
(Vol. 3821, pp. 1–18). Presented at the FSTTCS: Foundations of Software Technology
and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.1007/11590156_1'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Semiperfect-Information
Games,” 3821:1–18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2005. https://doi.org/10.1007/11590156_1.
ieee: 'K. Chatterjee and T. A. Henzinger, “Semiperfect-information games,” presented
at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science,
2005, vol. 3821, pp. 1–18.'
ista: 'Chatterjee K, Henzinger TA. 2005. Semiperfect-information games. FSTTCS:
Foundations of Software Technology and Theoretical Computer Science, LNCS, vol.
3821, 1–18.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Semiperfect-Information
Games. Vol. 3821, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2005,
pp. 1–18, doi:10.1007/11590156_1.
short: K. Chatterjee, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2005, pp. 1–18.
conference:
name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
date_created: 2018-12-11T12:09:23Z
date_published: 2005-12-07T00:00:00Z
date_updated: 2021-01-12T07:59:34Z
day: '07'
doi: 10.1007/11590156_1
extern: 1
intvolume: ' 3821'
month: '12'
page: 1 - 18
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '182'
quality_controlled: 0
status: public
title: Semiperfect-information games
type: conference
volume: 3821
year: '2005'
...
---
_id: '4553'
abstract:
- lang: eng
text: 'The theory of graph games with ω-regular winning conditions is the foundation
for modeling and synthesizing reactive processes. In the case of stochastic reactive
processes, the corresponding stochastic graph games have three players, two of
them (System and Environment) behaving adversarially, and the third (Uncertainty)
behaving probabilistically. We consider two problems for stochastic graph games:
the qualitative problem asks for the set of states from which a player can win
with probability 1 (almost-sure winning); the quantitative problem asks for the
maximal probability of winning (optimal winning) from each state. We show that
for Rabin winning conditions, both problems are in NP. As these problems were
known to be NP-hard, it follows that they are NP-complete for Rabin conditions,
and dually, coNP-complete for Streett conditions. The proof proceeds by showing
that pure memoryless strategies suffice for qualitatively and quantitatively winning
stochastic graph games with Rabin conditions. This insight is of interest in its
own right, as it implies that controllers for Rabin objectives have simple implementations.
We also prove that for every ω-regular condition, optimal winning strategies are
no more complex than almost-sure winning strategies.'
acknowledgement: This research was supported in part by the ONR grant N00014-02-1-0671,
the AFOSR MURI grant F49620-00-1-0327, and the NSF 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: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- 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, De Alfaro L, Henzinger TA. The complexity of stochastic Rabin
and Streett games. In: Vol 3580. Springer; 2005:878-890. doi:10.1007/11523468_71'
apa: 'Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2005). The complexity
of stochastic Rabin and Streett games (Vol. 3580, pp. 878–890). Presented at the
ICALP: Automata, Languages and Programming, Springer. https://doi.org/10.1007/11523468_71'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “The Complexity
of Stochastic Rabin and Streett Games,” 3580:878–90. Springer, 2005. https://doi.org/10.1007/11523468_71.
ieee: 'K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “The complexity of stochastic
Rabin and Streett games,” presented at the ICALP: Automata, Languages and Programming,
2005, vol. 3580, pp. 878–890.'
ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2005. The complexity of stochastic
Rabin and Streett games. ICALP: Automata, Languages and Programming, LNCS, vol.
3580, 878–890.'
mla: Chatterjee, Krishnendu, et al. The Complexity of Stochastic Rabin and Streett
Games. Vol. 3580, Springer, 2005, pp. 878–90, doi:10.1007/11523468_71.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, Springer, 2005, pp. 878–890.
conference:
name: 'ICALP: Automata, Languages and Programming'
date_created: 2018-12-11T12:09:27Z
date_published: 2005-06-24T00:00:00Z
date_updated: 2021-01-12T07:59:39Z
day: '24'
doi: 10.1007/11523468_71
extern: 1
intvolume: ' 3580'
month: '06'
page: 878 - 890
publication_status: published
publisher: Springer
publist_id: '158'
quality_controlled: 0
status: public
title: The complexity of stochastic Rabin and Streett games
type: conference
volume: 3580
year: '2005'
...
---
_id: '4554'
abstract:
- lang: eng
text: Games played on graphs may have qualitative objectives, such as the satisfaction
of an ω-regular property, or quantitative objectives, such as the optimization
of a real-valued reward. When games are used to model reactive systems with both
fairness assumptions and quantitative (e.g., resource) constraints, then the corresponding
objective combines both a qualitative and a quantitative component. In a general
case of interest, the qualitative component is a parity condition and the quantitative
component is a mean-payoff reward. We study and solve such mean-payoff parity
games. We also prove some interesting facts about mean-payoff parity games which
distinguish them both from mean-payoff and from parity games. In particular, we
show that optimal strategies exist in mean-payoff parity games, but they may require
infinite memory.
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
- first_name: Marcin
full_name: Jurdziński, Marcin
last_name: Jurdziński
citation:
ama: 'Chatterjee K, Henzinger TA, Jurdziński M. Mean-payoff parity games. In: IEEE;
2005:178-187. doi:10.1109/LICS.2005.26'
apa: 'Chatterjee, K., Henzinger, T. A., & Jurdziński, M. (2005). Mean-payoff
parity games (pp. 178–187). Presented at the LICS: Logic in Computer Science,
IEEE. https://doi.org/10.1109/LICS.2005.26'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Marcin Jurdziński. “Mean-Payoff
Parity Games,” 178–87. IEEE, 2005. https://doi.org/10.1109/LICS.2005.26.
ieee: 'K. Chatterjee, T. A. Henzinger, and M. Jurdziński, “Mean-payoff parity games,”
presented at the LICS: Logic in Computer Science, 2005, pp. 178–187.'
ista: 'Chatterjee K, Henzinger TA, Jurdziński M. 2005. Mean-payoff parity games.
LICS: Logic in Computer Science, 178–187.'
mla: Chatterjee, Krishnendu, et al. Mean-Payoff Parity Games. IEEE, 2005,
pp. 178–87, doi:10.1109/LICS.2005.26.
short: K. Chatterjee, T.A. Henzinger, M. Jurdziński, in:, IEEE, 2005, pp. 178–187.
conference:
name: 'LICS: Logic in Computer Science'
date_created: 2018-12-11T12:09:27Z
date_published: 2005-09-19T00:00:00Z
date_updated: 2021-01-12T07:59:39Z
day: '19'
doi: 10.1109/LICS.2005.26
extern: 1
month: '09'
page: 178 - 187
publication_status: published
publisher: IEEE
publist_id: '159'
quality_controlled: 0
status: public
title: Mean-payoff parity games
type: conference
year: '2005'
...
---
_id: '4557'
abstract:
- lang: eng
text: 'Planning in adversarial and uncertain environments can be modeled as the
problem of devising strategies in stochastic perfect information games. These
games are generalizations of Markov decision processes (MDPs): there are two (adversarial)
players, and a source of randomness. The main practical obstacle to computing
winning strategies in such games is the size of the state space. In practice therefore,
one typically works with abstractions of the model. The diffculty is to come up
with an abstraction that is neither too coarse to remove all winning strategies
(plans), nor too fine to be intractable. In verification, the paradigm of counterexample-guided
abstraction refinement has been successful to construct useful but parsimonious
abstractions automatically. We extend this paradigm to probabilistic models (namely,
perfect information games and, as a special case, MDPs). This allows us to apply
the counterexample-guided abstraction paradigm to the AI planning problem. As
special cases, we get planning algorithms for MDPs and deterministic systems that
automatically construct system abstractions.'
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
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Chatterjee K, Henzinger TA, Jhala R, Majumdar R. Counterexample-guided planning.
In: AUAI Press; 2005:104-111.'
apa: 'Chatterjee, K., Henzinger, T. A., Jhala, R., & Majumdar, R. (2005). Counterexample-guided
planning (pp. 104–111). Presented at the UAI: Uncertainty in Artificial Intelligence,
AUAI Press.'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Ranjit Jhala, and Ritankar
Majumdar. “Counterexample-Guided Planning,” 104–11. AUAI Press, 2005.
ieee: 'K. Chatterjee, T. A. Henzinger, R. Jhala, and R. Majumdar, “Counterexample-guided
planning,” presented at the UAI: Uncertainty in Artificial Intelligence, 2005,
pp. 104–111.'
ista: 'Chatterjee K, Henzinger TA, Jhala R, Majumdar R. 2005. Counterexample-guided
planning. UAI: Uncertainty in Artificial Intelligence, 104–111.'
mla: Chatterjee, Krishnendu, et al. Counterexample-Guided Planning. AUAI
Press, 2005, pp. 104–11.
short: K. Chatterjee, T.A. Henzinger, R. Jhala, R. Majumdar, in:, AUAI Press, 2005,
pp. 104–111.
conference:
name: 'UAI: Uncertainty in Artificial Intelligence'
date_created: 2018-12-11T12:09:28Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:41Z
day: '01'
extern: 1
main_file_link:
- open_access: '0'
url: http://uai.sis.pitt.edu/papers/05/p104-chatterjee.pdf
month: '01'
page: 104 - 111
publication_status: published
publisher: AUAI Press
publist_id: '157'
quality_controlled: 0
status: public
title: Counterexample-guided planning
type: conference
year: '2005'
...
---
_id: '4560'
abstract:
- lang: eng
text: |
We define and study a quantitative generalization of the traditional boolean framework of model-based specification and verification. In our setting, propositions have integer values at states, and properties have integer values on traces. For example, the value of a quantitative proposition at a state may represent power consumed at the state, and the value of a quantitative property on a trace may represent energy used along the trace. The value of a quantitative property at a state, then, is the maximum (or minimum) value achievable over all possible traces from the state. In this framework, model checking can be used to compute, for example, the minimum battery capacity necessary for achieving a given objective, or the maximal achievable lifetime of a system with a given initial battery capacity. In the case of open systems, these problems require the solution of games with integer values.
Quantitative model checking and game solving is undecidable, except if bounds on the computation can be found. Indeed, many interesting quantitative properties, like minimal necessary battery capacity and maximal achievable lifetime, can be naturally specified by quantitative-bound automata, which are finite automata with integer registers whose analysis is constrained by a bound function f that maps each system K to an integer f(K). Along with the linear-time, automaton-based view of quantitative verification, we present a corresponding branching-time view based on a quantitative-bound μ-calculus, and we study the relationship, expressive power, and complexity of both views.
alternative_title:
- LNCS
author:
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
- 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
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Chakrabarti A, Chatterjee K, Henzinger TA, Kupferman O, Majumdar R. Verifying
quantitative properties using bound functions. In: Vol 3725. Springer; 2005:50-64.
doi:10.1007/11560548_7'
apa: 'Chakrabarti, A., Chatterjee, K., Henzinger, T. A., Kupferman, O., & Majumdar,
R. (2005). Verifying quantitative properties using bound functions (Vol. 3725,
pp. 50–64). Presented at the CHARME: Correct Hardware Design and Verification
Methods, Springer. https://doi.org/10.1007/11560548_7'
chicago: Chakrabarti, Arindam, Krishnendu Chatterjee, Thomas A Henzinger, Orna Kupferman,
and Ritankar Majumdar. “Verifying Quantitative Properties Using Bound Functions,”
3725:50–64. Springer, 2005. https://doi.org/10.1007/11560548_7.
ieee: 'A. Chakrabarti, K. Chatterjee, T. A. Henzinger, O. Kupferman, and R. Majumdar,
“Verifying quantitative properties using bound functions,” presented at the CHARME:
Correct Hardware Design and Verification Methods, 2005, vol. 3725, pp. 50–64.'
ista: 'Chakrabarti A, Chatterjee K, Henzinger TA, Kupferman O, Majumdar R. 2005.
Verifying quantitative properties using bound functions. CHARME: Correct Hardware
Design and Verification Methods, LNCS, vol. 3725, 50–64.'
mla: Chakrabarti, Arindam, et al. Verifying Quantitative Properties Using Bound
Functions. Vol. 3725, Springer, 2005, pp. 50–64, doi:10.1007/11560548_7.
short: A. Chakrabarti, K. Chatterjee, T.A. Henzinger, O. Kupferman, R. Majumdar,
in:, Springer, 2005, pp. 50–64.
conference:
name: 'CHARME: Correct Hardware Design and Verification Methods'
date_created: 2018-12-11T12:09:29Z
date_published: 2005-09-19T00:00:00Z
date_updated: 2021-01-12T07:59:42Z
day: '19'
doi: 10.1007/11560548_7
extern: 1
intvolume: ' 3725'
month: '09'
page: 50 - 64
publication_status: published
publisher: Springer
publist_id: '149'
quality_controlled: 0
status: public
title: Verifying quantitative properties using bound functions
type: conference
volume: 3725
year: '2005'
...
---
_id: '4576'
abstract:
- lang: eng
text: We present a language for specifying web service interfaces. A web service
interface puts three kinds of constraints on the users of the service. First,
the interface specifies the methods that can be called by a client, together with
types of input and output parameters; these are called signature constraints.
Second, the interface may specify propositional constraints on method calls and
output values that may oc- cur in a web service conversation; these are called
consis- tency constraints. Third, the interface may specify temporal constraints
on the ordering of method calls; these are called protocol constraints. The interfaces
can be used to check, first, if two or more web services are compatible, and second,
if a web service A can be safely substituted for a web ser- vice B. The algorithm
for compatibility checking verifies that two or more interfaces fulfill each others’
constraints. The algorithm for substitutivity checking verifies that service A
demands fewer and fulfills more constraints than service B.
acknowledgement: This research was supported in part by the ONR grant N00014-02-1-0671
and by the NSF grants CCR-0234690 and CCR-0225610.
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Beyer D, Chakrabarti A, Henzinger TA. Web service interfaces. In: ACM; 2005:148-159.
doi:10.1145/1060745.1060770'
apa: 'Beyer, D., Chakrabarti, A., & Henzinger, T. A. (2005). Web service interfaces
(pp. 148–159). Presented at the WWW: World Wide Web Conference, ACM. https://doi.org/10.1145/1060745.1060770'
chicago: Beyer, Dirk, Arindam Chakrabarti, and Thomas A Henzinger. “Web Service
Interfaces,” 148–59. ACM, 2005. https://doi.org/10.1145/1060745.1060770.
ieee: 'D. Beyer, A. Chakrabarti, and T. A. Henzinger, “Web service interfaces,”
presented at the WWW: World Wide Web Conference, 2005, pp. 148–159.'
ista: 'Beyer D, Chakrabarti A, Henzinger TA. 2005. Web service interfaces. WWW:
World Wide Web Conference, 148–159.'
mla: Beyer, Dirk, et al. Web Service Interfaces. ACM, 2005, pp. 148–59, doi:10.1145/1060745.1060770.
short: D. Beyer, A. Chakrabarti, T.A. Henzinger, in:, ACM, 2005, pp. 148–159.
conference:
name: 'WWW: World Wide Web Conference'
date_created: 2018-12-11T12:09:33Z
date_published: 2005-05-01T00:00:00Z
date_updated: 2021-01-12T07:59:50Z
day: '01'
doi: 10.1145/1060745.1060770
extern: 1
month: '05'
page: 148 - 159
publication_status: published
publisher: ACM
publist_id: '132'
quality_controlled: 0
status: public
title: Web service interfaces
type: conference
year: '2005'
...
---
_id: '4579'
abstract:
- lang: eng
text: BLAST is an automatic verification tool for checking temporal safety properties
of C programs. Given a C program and a temporal safety property, BLAST statically
proves that either the program satisfies the safety property or the program has
an execution trace that exhibits a violation of the property. BLAST constructs,
explores, and refines abstractions of the program state space based on lazy predicate
abstraction and interpolation-based predicate discovery. We show how BLAST can
be used to statically prove memory safety for C programs. We take a two-step approach.
First, we use Ccured, a type-based memory safety analyzer, to annotate with run-time
checks all program points that cannot be proved memory safe by the type system.
Second, we use BLAST to remove as many of the run-time checks as possible (by
proving that these checks never fail), and to generate for the remaining run-time
checks execution traces that witness them fail. Our experience shows that BLAST
can remove many of the run-time checks added by Ccured and provide useful information
to the programmer about many of the remaining checks.
acknowledgement: This research was supported in part by the NSF grants CCR-0234690,
CCR-0225610, and ITR-0326577.
alternative_title:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. Checking memory safety with BLAST.
In: Vol 3442. Springer; 2005:2-18. doi:10.1007/978-3-540-31984-9_2'
apa: 'Beyer, D., Henzinger, T. A., Jhala, R., & Majumdar, R. (2005). Checking
memory safety with BLAST (Vol. 3442, pp. 2–18). Presented at the FASE: Fundamental
Approaches To Software Engineering, Springer. https://doi.org/10.1007/978-3-540-31984-9_2'
chicago: Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “Checking
Memory Safety with BLAST,” 3442:2–18. Springer, 2005. https://doi.org/10.1007/978-3-540-31984-9_2.
ieee: 'D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “Checking memory safety
with BLAST,” presented at the FASE: Fundamental Approaches To Software Engineering,
2005, vol. 3442, pp. 2–18.'
ista: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. 2005. Checking memory safety
with BLAST. FASE: Fundamental Approaches To Software Engineering, LNCS, vol. 3442,
2–18.'
mla: Beyer, Dirk, et al. Checking Memory Safety with BLAST. Vol. 3442, Springer,
2005, pp. 2–18, doi:10.1007/978-3-540-31984-9_2.
short: D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Springer, 2005, pp.
2–18.
conference:
name: 'FASE: Fundamental Approaches To Software Engineering'
date_created: 2018-12-11T12:09:34Z
date_published: 2005-03-24T00:00:00Z
date_updated: 2021-01-12T07:59:51Z
day: '24'
doi: 10.1007/978-3-540-31984-9_2
extern: 1
intvolume: ' 3442'
month: '03'
page: 2 - 18
publication_status: published
publisher: Springer
publist_id: '131'
quality_controlled: 0
status: public
title: Checking memory safety with BLAST
type: conference
volume: 3442
year: '2005'
...
---
_id: '4624'
abstract:
- lang: eng
text: Surveying results from [5] and [6], we motivate and introduce the theory behind
formalizing rich interfaces for software and hardware components. Rich interfaces
specify the protocol aspects of component interaction. Their formalization, called
interface automata, permits a compiler to check the compatibility of component
interaction protocols. Interface automata support incremental design and independent
implementability. Incremental design means that the compatibility checking of
interfaces can proceed for partial system descriptions, without knowing the interfaces
of all components. Independent implementability means that compatible interfaces
can be refined separately, while still maintaining compatibility.
alternative_title:
- 'NATO Science Series: Mathematics, Physics, and Chemistry'
author:
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'De Alfaro L, Henzinger TA. Interface-based design. In: Vol 195. Springer;
2005:83-104. doi:10.1007/1-4020-3532-2_3'
apa: De Alfaro, L., & Henzinger, T. A. (2005). Interface-based design (Vol.
195, pp. 83–104). Presented at the Engineering Theories of Software Intensive
Systems, Springer. https://doi.org/10.1007/1-4020-3532-2_3
chicago: De Alfaro, Luca, and Thomas A Henzinger. “Interface-Based Design,” 195:83–104.
Springer, 2005. https://doi.org/10.1007/1-4020-3532-2_3.
ieee: L. De Alfaro and T. A. Henzinger, “Interface-based design,” presented at the
Engineering Theories of Software Intensive Systems, 2005, vol. 195, pp. 83–104.
ista: 'De Alfaro L, Henzinger TA. 2005. Interface-based design. Engineering Theories
of Software Intensive Systems, NATO Science Series: Mathematics, Physics, and
Chemistry, vol. 195, 83–104.'
mla: De Alfaro, Luca, and Thomas A. Henzinger. Interface-Based Design. Vol.
195, Springer, 2005, pp. 83–104, doi:10.1007/1-4020-3532-2_3.
short: L. De Alfaro, T.A. Henzinger, in:, Springer, 2005, pp. 83–104.
conference:
name: Engineering Theories of Software Intensive Systems
date_created: 2018-12-11T12:09:49Z
date_published: 2005-07-15T00:00:00Z
date_updated: 2021-01-12T08:00:36Z
day: '15'
doi: 10.1007/1-4020-3532-2_3
extern: 1
intvolume: ' 195'
month: '07'
page: 83 - 104
publication_status: published
publisher: Springer
publist_id: '85'
quality_controlled: 0
status: public
title: Interface-based design
type: conference
volume: 195
year: '2005'
...