---
_id: '3864'
abstract:
- lang: eng
text: 'Often one has a preference order among the different systems that satisfy
a given specification. Under a probabilistic assumption about the possible inputs,
such a preference order is naturally expressed by a weighted automaton, which
assigns to each word a value, such that a system is preferred if it generates
a higher expected value. We solve the following optimal-synthesis problem: given
an omega-regular specification, a Markov chain that describes the distribution
of inputs, and a weighted automaton that measures how well a system satisfies
the given specification tinder the given input assumption, synthesize a system
that optimizes the measured value. For safety specifications and measures that
are defined by mean-payoff automata, the optimal-synthesis problem amounts to
finding a strategy in a Markov decision process (MDP) that is optimal for a long-run
average reward objective, which can be done in polynomial time. For general omega-regular
specifications, the solution rests on a new, polynomial-time algorithm for computing
optimal strategies in MDPs with mean-payoff parity objectives. We present some
experimental results showing optimal systems that were automatically generated
in this way.'
acknowledgement: This research was supported by the European Union project COMBEST
and the European Network of Excellence ArtistDesign.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Rohit
full_name: Singh, Rohit
last_name: Singh
citation:
ama: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing
systems in probabilistic environments. In: Vol 6174. Springer; 2010:380-395. doi:10.1007/978-3-642-14295-6_34'
apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., & Singh, R. (2010). Measuring
and synthesizing systems in probabilistic environments (Vol. 6174, pp. 380–395).
Presented at the CAV: Computer Aided Verification, Edinburgh, United Kingdom:
Springer. https://doi.org/10.1007/978-3-642-14295-6_34'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit
Singh. “Measuring and Synthesizing Systems in Probabilistic Environments,” 6174:380–95.
Springer, 2010. https://doi.org/10.1007/978-3-642-14295-6_34.
ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and
synthesizing systems in probabilistic environments,” presented at the CAV: Computer
Aided Verification, Edinburgh, United Kingdom, 2010, vol. 6174, pp. 380–395.'
ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2010. Measuring and synthesizing
systems in probabilistic environments. CAV: Computer Aided Verification, LNCS,
vol. 6174, 380–395.'
mla: Chatterjee, Krishnendu, et al. Measuring and Synthesizing Systems in Probabilistic
Environments. Vol. 6174, Springer, 2010, pp. 380–95, doi:10.1007/978-3-642-14295-6_34.
short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, in:, Springer, 2010,
pp. 380–395.
conference:
end_date: 2010-07-19
location: Edinburgh, United Kingdom
name: 'CAV: Computer Aided Verification'
start_date: 201-07-15
date_created: 2018-12-11T12:05:35Z
date_published: 2010-07-09T00:00:00Z
date_updated: 2023-02-23T10:17:28Z
day: '09'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_34
intvolume: ' 6174'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1004.0739
month: '07'
oa: 1
oa_version: Preprint
page: 380 - 395
publication_status: published
publisher: Springer
publist_id: '2313'
quality_controlled: '1'
related_material:
record:
- id: '1856'
relation: later_version
status: public
scopus_import: 1
status: public
title: Measuring and synthesizing systems in probabilistic environments
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...
---
_id: '3865'
abstract:
- lang: eng
text: We introduce a technique for debugging multi-threaded C programs and analyzing
the impact of source code changes, and its implementation in the prototype tool
DIRECT. Our approach uses a combination of source code instrumentation and runtime
management. The source code along with a test harness is instrumented to monitor
Operating System (OS) and user defined function calls. DIRECT tracks all concurrency
control primitives and, optionally, data from the program. DIRECT maintains an
abstract global state that combines information from every thread, including the
sequence of function calls and concurrency primitives executed. The runtime manager
can insert delays, provoking thread inter-leavings that may exhibit bugs that
are difficult to reach otherwise. The runtime manager collects an approximation
of the reachable state space and uses this approximation to assess the impact
of change in a new version of the program.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
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: Vishwanath
full_name: Raman, Vishwanath
last_name: Raman
- first_name: César
full_name: Sánchez, César
last_name: Sánchez
citation:
ama: 'Chatterjee K, De Alfaro L, Raman V, Sánchez C. Analyzing the impact of change
in multi-threaded programs. In: Rosenblum D, Taenzer G, eds. Vol 6013. Springer;
2010:293-307. doi:10.1007/978-3-642-12029-9_21'
apa: 'Chatterjee, K., De Alfaro, L., Raman, V., & Sánchez, C. (2010). Analyzing
the impact of change in multi-threaded programs. In D. Rosenblum & G. Taenzer
(Eds.) (Vol. 6013, pp. 293–307). Presented at the FASE: Fundamental Approaches
To Software Engineering, Paphos, Cyprus: Springer. https://doi.org/10.1007/978-3-642-12029-9_21'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, Vishwanath Raman, and César Sánchez.
“Analyzing the Impact of Change in Multi-Threaded Programs.” edited by David Rosenblum
and Gabriele Taenzer, 6013:293–307. Springer, 2010. https://doi.org/10.1007/978-3-642-12029-9_21.
ieee: 'K. Chatterjee, L. De Alfaro, V. Raman, and C. Sánchez, “Analyzing the impact
of change in multi-threaded programs,” presented at the FASE: Fundamental Approaches
To Software Engineering, Paphos, Cyprus, 2010, vol. 6013, pp. 293–307.'
ista: 'Chatterjee K, De Alfaro L, Raman V, Sánchez C. 2010. Analyzing the impact
of change in multi-threaded programs. FASE: Fundamental Approaches To Software
Engineering, LNCS, vol. 6013, 293–307.'
mla: Chatterjee, Krishnendu, et al. Analyzing the Impact of Change in Multi-Threaded
Programs. Edited by David Rosenblum and Gabriele Taenzer, vol. 6013, Springer,
2010, pp. 293–307, doi:10.1007/978-3-642-12029-9_21.
short: K. Chatterjee, L. De Alfaro, V. Raman, C. Sánchez, in:, D. Rosenblum, G.
Taenzer (Eds.), Springer, 2010, pp. 293–307.
conference:
end_date: 2010-03-28
location: Paphos, Cyprus
name: 'FASE: Fundamental Approaches To Software Engineering'
start_date: 2010-03-20
date_created: 2018-12-11T12:05:35Z
date_published: 2010-04-21T00:00:00Z
date_updated: 2021-01-12T07:52:47Z
day: '21'
department:
- _id: KrCh
doi: 10.1007/978-3-642-12029-9_21
editor:
- first_name: David
full_name: Rosenblum, David
last_name: Rosenblum
- first_name: Gabriele
full_name: Taenzer, Gabriele
last_name: Taenzer
intvolume: ' 6013'
language:
- iso: eng
month: '04'
oa_version: None
page: 293 - 307
publication_status: published
publisher: Springer
publist_id: '2315'
quality_controlled: '1'
scopus_import: 1
status: public
title: Analyzing the impact of change in multi-threaded programs
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6013
year: '2010'
...
---
_id: '3866'
abstract:
- lang: eng
text: Systems ought to behave reasonably even in circumstances that are not anticipated
in their specifications. We propose a definition of robustness for liveness specifications
which prescribes, for any number of environment assumptions that are violated,
a minimal number of system guarantees that must still be fulfilled. This notion
of robustness can be formulated and realized using a Generalized Reactivity formula.
We present an algorithm for synthesizing robust systems from such formulas. For
the important special case of Generalized Reactivity formulas of rank 1, our algorithm
improves the complexity of [PPS06] for large specifications with a small number
of assumptions and guarantees.
alternative_title:
- LNCS
author:
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Karin
full_name: Greimel, Karin
last_name: Greimel
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
citation:
ama: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Robustness in
the presence of liveness. In: Touili T, Cook B, Jackson P, eds. Vol 6174. Springer;
2010:410-424. doi:10.1007/978-3-642-14295-6_36'
apa: 'Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., & Jobstmann,
B. (2010). Robustness in the presence of liveness. In T. Touili, B. Cook, &
P. Jackson (Eds.) (Vol. 6174, pp. 410–424). Presented at the CAV: Computer Aided
Verification, Edinburgh, UK: Springer. https://doi.org/10.1007/978-3-642-14295-6_36'
chicago: Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger,
and Barbara Jobstmann. “Robustness in the Presence of Liveness.” edited by Tayssir
Touili, Byron Cook, and Paul Jackson, 6174:410–24. Springer, 2010. https://doi.org/10.1007/978-3-642-14295-6_36.
ieee: 'R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Robustness
in the presence of liveness,” presented at the CAV: Computer Aided Verification,
Edinburgh, UK, 2010, vol. 6174, pp. 410–424.'
ista: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2010. Robustness
in the presence of liveness. CAV: Computer Aided Verification, LNCS, vol. 6174,
410–424.'
mla: Bloem, Roderick, et al. Robustness in the Presence of Liveness. Edited
by Tayssir Touili et al., vol. 6174, Springer, 2010, pp. 410–24, doi:10.1007/978-3-642-14295-6_36.
short: R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, T.
Touili, B. Cook, P. Jackson (Eds.), Springer, 2010, pp. 410–424.
conference:
end_date: 2010-07-19
location: Edinburgh, UK
name: 'CAV: Computer Aided Verification'
start_date: 2010-07-15
date_created: 2018-12-11T12:05:36Z
date_published: 2010-07-01T00:00:00Z
date_updated: 2021-01-12T07:52:47Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_36
ec_funded: 1
editor:
- first_name: Tayssir
full_name: Touili, Tayssir
last_name: Touili
- first_name: Byron
full_name: Cook, Byron
last_name: Cook
- first_name: Paul
full_name: Jackson, Paul
last_name: Jackson
file:
- access_level: open_access
checksum: 9d204611c8d7855bed8134f8708a0010
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:52Z
date_updated: 2020-07-14T12:46:19Z
file_id: '5243'
file_name: IST-2012-54-v1+1_Robustness_in_the_presence_of_liveness.pdf
file_size: 213083
relation: main_file
file_date_updated: 2020-07-14T12:46:19Z
has_accepted_license: '1'
intvolume: ' 6174'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 410 - 424
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '2310'
pubrep_id: '54'
quality_controlled: '1'
scopus_import: 1
status: public
title: Robustness in the presence of liveness
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...
---
_id: '3867'
abstract:
- lang: eng
text: Weighted automata are nondeterministic automata with numerical weights on
transitions. They can define quantitative languages L that assign to each word
w a real number L(w). In the case of infinite words, the value of a run is naturally
computed as the maximum, limsup, liminf, limit-average, or discounted-sum of the
transition weights. The value of a word w is the supremum of the values of the
runs over w. We study expressiveness and closure questions about these quantitative
languages. We first show that the set of words with value greater than a threshold
can be omega-regular for deterministic limit-average and discounted-sum automata,
while this set is always omega-regular when the threshold is isolated (i.e., some
neighborhood around the threshold contains no word). In the latter case, we prove
that the omega-regular language is robust against small perturbations of the transition
weights. We next consider automata with transition weights 0 or 1 and show that
they are as expressive as general weighted automata in the limit-average case,
but not in the discounted-sum case. Third, for quantitative languages L-1 and
L-2, we consider the operations max(L-1, L-2), min(L-1, L-2), and 1 - L-1, which
generalize the boolean operations on languages, as well as the sum L-1 + L-2.
We establish the closure properties of all classes of quantitative languages with
respect to these four operations.
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Chatterjee K, Doyen L, Henzinger TA. Expressiveness and closure properties
for quantitative languages. Logical Methods in Computer Science. 2010;6(3):1-23.
doi:10.2168/LMCS-6(3:10)2010
apa: Chatterjee, K., Doyen, L., & Henzinger, T. A. (2010). Expressiveness and
closure properties for quantitative languages. Logical Methods in Computer
Science. International Federation of Computational Logic. https://doi.org/10.2168/LMCS-6(3:10)2010
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Expressiveness
and Closure Properties for Quantitative Languages.” Logical Methods in Computer
Science. International Federation of Computational Logic, 2010. https://doi.org/10.2168/LMCS-6(3:10)2010.
ieee: K. Chatterjee, L. Doyen, and T. A. Henzinger, “Expressiveness and closure
properties for quantitative languages,” Logical Methods in Computer Science,
vol. 6, no. 3. International Federation of Computational Logic, pp. 1–23, 2010.
ista: Chatterjee K, Doyen L, Henzinger TA. 2010. Expressiveness and closure properties
for quantitative languages. Logical Methods in Computer Science. 6(3), 1–23.
mla: Chatterjee, Krishnendu, et al. “Expressiveness and Closure Properties for Quantitative
Languages.” Logical Methods in Computer Science, vol. 6, no. 3, International
Federation of Computational Logic, 2010, pp. 1–23, doi:10.2168/LMCS-6(3:10)2010.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, Logical Methods in Computer Science
6 (2010) 1–23.
date_created: 2018-12-11T12:05:36Z
date_published: 2010-08-30T00:00:00Z
date_updated: 2023-02-23T12:15:42Z
day: '30'
ddc:
- '000'
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.2168/LMCS-6(3:10)2010
ec_funded: 1
file:
- access_level: open_access
checksum: 0243da726476817f2ea33b48b78be696
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:54Z
date_updated: 2020-07-14T12:46:19Z
file_id: '5312'
file_name: IST-2012-55-v1+1_Expressiveness_Closure_Properties_Quantitative_Languages.pdf
file_size: 216598
relation: main_file
- access_level: open_access
checksum: 5e512b8503a9cb263de26331c4ee9cf2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:55Z
date_updated: 2020-07-14T12:46:19Z
file_id: '5313'
file_name: IST-2016-55-v2+1_1007.4018.pdf
file_size: 302416
relation: main_file
file_date_updated: 2020-07-14T12:46:19Z
has_accepted_license: '1'
intvolume: ' 6'
issue: '3'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '08'
oa: 1
oa_version: Published Version
page: 1 - 23
project:
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
publication: Logical Methods in Computer Science
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '2311'
pubrep_id: '504'
quality_controlled: '1'
related_material:
record:
- id: '4540'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Expressiveness and closure properties for quantitative languages
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6
year: '2010'
...
---
_id: '3868'
abstract:
- lang: eng
text: Simulation and bisimulation metrics for stochastic systems provide a quantitative
generalization of the classical simulation and bisimulation relations. These metrics
capture the similarity of states with respect to quantitative specifications written
in the quantitative mu-calculus and related probabilistic logics. We first show
that the metrics provide a bound for the difference in long-run average and discounted
average behavior across states, indicating that the metrics can be used both in
system verification, and in performance evaluation. For turn-based games and MDPs,
we provide a polynomial-time algorithm for the computation of the one-step metric
distance between states. The algorithm is based on linear programming; it improves
on the previous known exponential-time algorithm based on a reduction to the theory
of reals. We then present PSPACE algorithms for both the decision problem and
the problem of approximating the metric distance between two states, matching
the best known algorithms for Markov chains. For the bisimulation kernel of the
metric our algorithm works in time O(n(4)) for both turn-based games and MDPs;
improving the previously best known O(n(9).log(n)) time algorithm for MDPs. For
a concurrent game G, we show that computing the exact distance be tween states
is at least as hard as computing the value of concurrent reachability games and
the square-root-sum problem in computational geometry. We show that checking whether
the metric distance is bounded by a rational r, can be done via a reduction to
the theory of real closed fields, involving a formula with three quantifier alternations,
yielding O(vertical bar G vertical bar(O(vertical bar G vertical bar 5))) time
complexity, improving the previously known reduction, which yielded O(vertical
bar G vertical bar(O(vertical bar G vertical bar 7))) time complexity. These algorithms
can be iterated to approximate the metrics using binary search
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
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: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Vishwanath
full_name: Raman, Vishwanath
last_name: Raman
citation:
ama: Chatterjee K, De Alfaro L, Majumdar R, Raman V. Algorithms for game metrics.
Logical Methods in Computer Science. 2010;6(3):1-27. doi:10.2168/LMCS-6(3:13)2010
apa: Chatterjee, K., De Alfaro, L., Majumdar, R., & Raman, V. (2010). Algorithms
for game metrics. Logical Methods in Computer Science. International Federation
of Computational Logic. https://doi.org/10.2168/LMCS-6(3:13)2010
chicago: Chatterjee, Krishnendu, Luca De Alfaro, Ritankar Majumdar, and Vishwanath
Raman. “Algorithms for Game Metrics.” Logical Methods in Computer Science.
International Federation of Computational Logic, 2010. https://doi.org/10.2168/LMCS-6(3:13)2010.
ieee: K. Chatterjee, L. De Alfaro, R. Majumdar, and V. Raman, “Algorithms for game
metrics,” Logical Methods in Computer Science, vol. 6, no. 3. International
Federation of Computational Logic, pp. 1–27, 2010.
ista: Chatterjee K, De Alfaro L, Majumdar R, Raman V. 2010. Algorithms for game
metrics. Logical Methods in Computer Science. 6(3), 1–27.
mla: Chatterjee, Krishnendu, et al. “Algorithms for Game Metrics.” Logical Methods
in Computer Science, vol. 6, no. 3, International Federation of Computational
Logic, 2010, pp. 1–27, doi:10.2168/LMCS-6(3:13)2010.
short: K. Chatterjee, L. De Alfaro, R. Majumdar, V. Raman, Logical Methods in Computer
Science 6 (2010) 1–27.
date_created: 2018-12-11T12:05:36Z
date_published: 2010-09-01T00:00:00Z
date_updated: 2023-02-23T11:30:18Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.2168/LMCS-6(3:13)2010
file:
- access_level: open_access
checksum: a18988135fef3016c93808ecb15b55f5
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:11Z
date_updated: 2020-07-14T12:46:19Z
file_id: '4671'
file_name: IST-2015-370-v1+1_0809.4326.pdf
file_size: 346527
relation: main_file
file_date_updated: 2020-07-14T12:46:19Z
has_accepted_license: '1'
intvolume: ' 6'
issue: '3'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 1 - 27
publication: Logical Methods in Computer Science
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '2312'
pubrep_id: '370'
quality_controlled: '1'
related_material:
record:
- id: '3504'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Algorithms for game metrics
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 6
year: '2010'
...
---
_id: '3901'
abstract:
- lang: eng
text: We are interested in 3-dimensional images given as arrays of voxels with intensity
values. Extending these values to acontinuous function, we study the robustness
of homology classes in its level and interlevel sets, that is, the amount of perturbationneeded
to destroy these classes. The structure of the homology classes and their robustness,
over all level and interlevel sets, can bevisualized by a triangular diagram of
dots obtained by computing the extended persistence of the function. We give a
fast hierarchicalalgorithm using the dual complexes of oct-tree approximations
of the function. In addition, we show that for balanced oct-trees, thedual complexes
are geometrically realized in $R^3$ and can thus be used to construct level and
interlevel sets. We apply these tools tostudy 3-dimensional images of plant root
systems.
author:
- first_name: Paul
full_name: Bendich, Paul
id: 43F6EC54-F248-11E8-B48F-1D18A9856A87
last_name: Bendich
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Michael
full_name: Kerber, Michael
id: 36E4574A-F248-11E8-B48F-1D18A9856A87
last_name: Kerber
orcid: 0000-0002-8030-9299
citation:
ama: Bendich P, Edelsbrunner H, Kerber M. Computing robustness and persistence for
images. IEEE Transactions of Visualization and Computer Graphics. 2010;16(6):1251-1260.
doi:10.1109/TVCG.2010.139
apa: Bendich, P., Edelsbrunner, H., & Kerber, M. (2010). Computing robustness
and persistence for images. IEEE Transactions of Visualization and Computer
Graphics. IEEE. https://doi.org/10.1109/TVCG.2010.139
chicago: Bendich, Paul, Herbert Edelsbrunner, and Michael Kerber. “Computing Robustness
and Persistence for Images.” IEEE Transactions of Visualization and Computer
Graphics. IEEE, 2010. https://doi.org/10.1109/TVCG.2010.139.
ieee: P. Bendich, H. Edelsbrunner, and M. Kerber, “Computing robustness and persistence
for images,” IEEE Transactions of Visualization and Computer Graphics,
vol. 16, no. 6. IEEE, pp. 1251–1260, 2010.
ista: Bendich P, Edelsbrunner H, Kerber M. 2010. Computing robustness and persistence
for images. IEEE Transactions of Visualization and Computer Graphics. 16(6), 1251–1260.
mla: Bendich, Paul, et al. “Computing Robustness and Persistence for Images.” IEEE
Transactions of Visualization and Computer Graphics, vol. 16, no. 6, IEEE,
2010, pp. 1251–60, doi:10.1109/TVCG.2010.139.
short: P. Bendich, H. Edelsbrunner, M. Kerber, IEEE Transactions of Visualization
and Computer Graphics 16 (2010) 1251–1260.
date_created: 2018-12-11T12:05:47Z
date_published: 2010-10-28T00:00:00Z
date_updated: 2021-01-12T07:53:04Z
day: '28'
ddc:
- '000'
department:
- _id: HeEd
doi: 10.1109/TVCG.2010.139
file:
- access_level: open_access
checksum: f6d813c04f4b46023cec6b9a17f15472
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:10Z
date_updated: 2020-07-14T12:46:21Z
file_id: '5262'
file_name: IST-2016-536-v1+1_2010-J-02-PersistenceforImages.pdf
file_size: 721994
relation: main_file
file_date_updated: 2020-07-14T12:46:21Z
has_accepted_license: '1'
intvolume: ' 16'
issue: '6'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 1251 - 1260
publication: IEEE Transactions of Visualization and Computer Graphics
publication_status: published
publisher: IEEE
publist_id: '2253'
pubrep_id: '536'
quality_controlled: '1'
scopus_import: 1
status: public
title: Computing robustness and persistence for images
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 16
year: '2010'
...
---
_id: '3962'
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Holger
full_name: Pflicke, Holger
id: CAA57A9A-5B61-11E9-B130-E0C1E1F2C83D
last_name: Pflicke
citation:
ama: Pflicke H. Dendritic cell migration across basement membranes in the skin.
2010.
apa: Pflicke, H. (2010). Dendritic cell migration across basement membranes
in the skin. Institute of Science and Technology Austria.
chicago: Pflicke, Holger. “ Dendritic Cell Migration across Basement Membranes
in the Skin.” Institute of Science and Technology Austria, 2010.
ieee: H. Pflicke, “ Dendritic cell migration across basement membranes in the skin,”
Institute of Science and Technology Austria, 2010.
ista: Pflicke H. 2010. Dendritic cell migration across basement membranes in the
skin. Institute of Science and Technology Austria.
mla: Pflicke, Holger. Dendritic Cell Migration across Basement Membranes in
the Skin. Institute of Science and Technology Austria, 2010.
short: H. Pflicke, Dendritic Cell Migration across Basement Membranes in the Skin,
Institute of Science and Technology Austria, 2010.
date_created: 2018-12-11T12:06:08Z
date_published: 2010-07-01T00:00:00Z
date_updated: 2023-09-07T11:28:47Z
day: '01'
degree_awarded: PhD
department:
- _id: CaHe
- _id: GradSch
language:
- iso: eng
month: '07'
oa_version: None
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '2165'
status: public
supervisor:
- first_name: Carl-Philipp J
full_name: Heisenberg, Carl-Philipp J
id: 39427864-F248-11E8-B48F-1D18A9856A87
last_name: Heisenberg
orcid: 0000-0002-0912-4566
title: "\uFEFF\uFEFFDendritic cell migration across basement membranes in the skin"
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2010'
...
---
_id: '4134'
abstract:
- lang: eng
text: 'All species are restricted in their distribution. Currently, ecological models
can only explain such limits if patches vary in quality, leading to asymmetrical
dispersal, or if genetic variation is too low at the margins for adaptation. However,
population genetic models suggest that the increase in genetic variance resulting
from dispersal should allow adaptation to almost any ecological gradient. Clearly
therefore, these models miss something that prevents evolution in natural populations.
We developed an individual-based simulation to explore stochastic effects in these
models. At high carrying capacities, our simulations largely agree with deterministic
predictions. However, when carrying capacity is low, the population fails to establish
for a wide range of parameter values where adaptation was expected from previous
models. Stochastic or transient effects appear critical around the boundaries
in parameter space between simulation behaviours. Dispersal, gradient steepness,
and population density emerge as key factors determining adaptation on an ecological
gradient. '
acknowledgement: We are very grateful to Nick Barton.
author:
- first_name: Jon
full_name: Bridle, Jon
last_name: Bridle
- first_name: Jitka
full_name: Polechova, Jitka
id: 3BBFB084-F248-11E8-B48F-1D18A9856A87
last_name: Polechova
orcid: 0000-0003-0951-3112
- first_name: Masakado
full_name: Kawata, Masakado
last_name: Kawata
- first_name: Roger
full_name: Butlin, Roger
last_name: Butlin
citation:
ama: Bridle J, Polechova J, Kawata M, Butlin R. Why is adaptation prevented at ecological
margins? New insights from individual-based simulations. Ecology Letters.
2010;13(4):485-494. doi:10.1111/j.1461-0248.2010.01442.x
apa: Bridle, J., Polechova, J., Kawata, M., & Butlin, R. (2010). Why is adaptation
prevented at ecological margins? New insights from individual-based simulations.
Ecology Letters. Wiley-Blackwell. https://doi.org/10.1111/j.1461-0248.2010.01442.x
chicago: Bridle, Jon, Jitka Polechova, Masakado Kawata, and Roger Butlin. “Why Is
Adaptation Prevented at Ecological Margins? New Insights from Individual-Based
Simulations.” Ecology Letters. Wiley-Blackwell, 2010. https://doi.org/10.1111/j.1461-0248.2010.01442.x.
ieee: J. Bridle, J. Polechova, M. Kawata, and R. Butlin, “Why is adaptation prevented
at ecological margins? New insights from individual-based simulations,” Ecology
Letters, vol. 13, no. 4. Wiley-Blackwell, pp. 485–494, 2010.
ista: Bridle J, Polechova J, Kawata M, Butlin R. 2010. Why is adaptation prevented
at ecological margins? New insights from individual-based simulations. Ecology
Letters. 13(4), 485–494.
mla: Bridle, Jon, et al. “Why Is Adaptation Prevented at Ecological Margins? New
Insights from Individual-Based Simulations.” Ecology Letters, vol. 13,
no. 4, Wiley-Blackwell, 2010, pp. 485–94, doi:10.1111/j.1461-0248.2010.01442.x.
short: J. Bridle, J. Polechova, M. Kawata, R. Butlin, Ecology Letters 13 (2010)
485–494.
date_created: 2018-12-11T12:07:08Z
date_published: 2010-03-15T00:00:00Z
date_updated: 2021-01-12T07:54:45Z
day: '15'
department:
- _id: NiBa
doi: 10.1111/j.1461-0248.2010.01442.x
ec_funded: 1
intvolume: ' 13'
issue: '4'
language:
- iso: eng
month: '03'
oa_version: None
page: 485 - 494
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: Ecology Letters
publication_status: published
publisher: Wiley-Blackwell
publist_id: '1987'
quality_controlled: '1'
scopus_import: 1
status: public
title: Why is adaptation prevented at ecological margins? New insights from individual-based
simulations
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2010'
...
---
_id: '4157'
abstract:
- lang: eng
text: Integrin- and cadherin-mediated adhesion is central for cell and tissue morphogenesis,
allowing cells and tissues to change shape without loosing integrity. Studies
predominantly in cell culture showed that mechanosensation through adhesion structures
is achieved by force-mediated modulation of their molecular composition. The specific
molecular composition of adhesion sites in turn determines their signalling activity
and dynamic reorganization. Here, we will review how adhesion sites respond to
mecanical stimuli, and how spatially and temporally regulated signalling from
different adhesion sites controls cell migration and tissue morphogenesis.
acknowledged_ssus:
- _id: Bio
author:
- first_name: Ekaterina
full_name: Papusheva, Ekaterina
id: 41DB591E-F248-11E8-B48F-1D18A9856A87
last_name: Papusheva
- first_name: Carl-Philipp J
full_name: Heisenberg, Carl-Philipp J
id: 39427864-F248-11E8-B48F-1D18A9856A87
last_name: Heisenberg
orcid: 0000-0002-0912-4566
citation:
ama: 'Papusheva E, Heisenberg C-PJ. Spatial organization of adhesion: force-dependent
regulation and function in tissue morphogenesis. EMBO Journal. 2010;29(16):2753-2768.
doi:10.1038/emboj.2010.182'
apa: 'Papusheva, E., & Heisenberg, C.-P. J. (2010). Spatial organization of
adhesion: force-dependent regulation and function in tissue morphogenesis. EMBO
Journal. Wiley-Blackwell. https://doi.org/10.1038/emboj.2010.182'
chicago: 'Papusheva, Ekaterina, and Carl-Philipp J Heisenberg. “Spatial Organization
of Adhesion: Force-Dependent Regulation and Function in Tissue Morphogenesis.”
EMBO Journal. Wiley-Blackwell, 2010. https://doi.org/10.1038/emboj.2010.182.'
ieee: 'E. Papusheva and C.-P. J. Heisenberg, “Spatial organization of adhesion:
force-dependent regulation and function in tissue morphogenesis,” EMBO Journal,
vol. 29, no. 16. Wiley-Blackwell, pp. 2753–2768, 2010.'
ista: 'Papusheva E, Heisenberg C-PJ. 2010. Spatial organization of adhesion: force-dependent
regulation and function in tissue morphogenesis. EMBO Journal. 29(16), 2753–2768.'
mla: 'Papusheva, Ekaterina, and Carl-Philipp J. Heisenberg. “Spatial Organization
of Adhesion: Force-Dependent Regulation and Function in Tissue Morphogenesis.”
EMBO Journal, vol. 29, no. 16, Wiley-Blackwell, 2010, pp. 2753–68, doi:10.1038/emboj.2010.182.'
short: E. Papusheva, C.-P.J. Heisenberg, EMBO Journal 29 (2010) 2753–2768.
date_created: 2018-12-11T12:07:17Z
date_published: 2010-08-18T00:00:00Z
date_updated: 2021-01-12T07:54:55Z
day: '18'
department:
- _id: Bio
- _id: CaHe
doi: 10.1038/emboj.2010.182
external_id:
pmid:
- '20717145'
intvolume: ' 29'
issue: '16'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC2924654/
month: '08'
oa: 1
oa_version: Submitted Version
page: 2753 - 2768
pmid: 1
publication: EMBO Journal
publication_status: published
publisher: Wiley-Blackwell
publist_id: '1962'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Spatial organization of adhesion: force-dependent regulation and function
in tissue morphogenesis'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 29
year: '2010'
...
---
_id: '4243'
abstract:
- lang: eng
text: We investigate a new model for populations evolving in a spatial continuum.
This model can be thought of as a spatial version of the Lambda-Fleming-Viot process.
It explicitly incorporates both small scale reproduction events and large scale
extinction-recolonisation events. The lineages ancestral to a sample from a population
evolving according to this model can be described in terms of a spatial version
of the Lambda-coalescent. Using a technique of Evans (1997), we prove existence
and uniqueness in law for the model. We then investigate the asymptotic behaviour
of the genealogy of a finite number of individuals sampled uniformly at random
(or more generally `far enough apart') from a two-dimensional torus of sidelength
L as L tends to infinity. Under appropriate conditions (and on a suitable timescale)
we can obtain as limiting genealogical processes a Kingman coalescent, a more
general Lambda-coalescent or a system of coalescing Brownian motions (with a non-local
coalescence mechanism).
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
- first_name: Alison
full_name: Etheridge, Alison
last_name: Etheridge
- first_name: Amandine
full_name: Véber, Amandine
last_name: Véber
citation:
ama: Barton NH, Etheridge A, Véber A. A new model for evolution in a spatial continuum.
Electronic Journal of Probability. 2010;15(7):162-216. doi:10.1214/EJP.v15-741
apa: Barton, N. H., Etheridge, A., & Véber, A. (2010). A new model for evolution
in a spatial continuum. Electronic Journal of Probability. Institute of
Mathematical Statistics. https://doi.org/10.1214/EJP.v15-741
chicago: Barton, Nicholas H, Alison Etheridge, and Amandine Véber. “A New Model
for Evolution in a Spatial Continuum.” Electronic Journal of Probability.
Institute of Mathematical Statistics, 2010. https://doi.org/10.1214/EJP.v15-741.
ieee: N. H. Barton, A. Etheridge, and A. Véber, “A new model for evolution in a
spatial continuum,” Electronic Journal of Probability, vol. 15, no. 7.
Institute of Mathematical Statistics, pp. 162–216, 2010.
ista: Barton NH, Etheridge A, Véber A. 2010. A new model for evolution in a spatial
continuum. Electronic Journal of Probability. 15(7), 162–216.
mla: Barton, Nicholas H., et al. “A New Model for Evolution in a Spatial Continuum.”
Electronic Journal of Probability, vol. 15, no. 7, Institute of Mathematical
Statistics, 2010, pp. 162–216, doi:10.1214/EJP.v15-741.
short: N.H. Barton, A. Etheridge, A. Véber, Electronic Journal of Probability 15
(2010) 162–216.
date_created: 2018-12-11T12:07:48Z
date_published: 2010-02-03T00:00:00Z
date_updated: 2021-01-12T07:55:34Z
day: '03'
ddc:
- '576'
department:
- _id: NiBa
doi: 10.1214/EJP.v15-741
file:
- access_level: open_access
checksum: bab577546dd4e8f882e9a9dd645cd01e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:21Z
date_updated: 2020-07-14T12:46:26Z
file_id: '5140'
file_name: IST-2015-369-v1+1_741-2535-1-PB.pdf
file_size: 450171
relation: main_file
file_date_updated: 2020-07-14T12:46:26Z
has_accepted_license: '1'
intvolume: ' 15'
issue: '7'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: 162 - 216
publication: Electronic Journal of Probability
publication_status: published
publisher: Institute of Mathematical Statistics
publist_id: '1863'
pubrep_id: '369'
quality_controlled: '1'
scopus_import: 1
status: public
title: A new model for evolution in a spatial continuum
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2010'
...
---
_id: '4339'
abstract:
- lang: ger
text: Mit diesem Buch möchten wir einen Überblick der aktuellen Diskussion zum Thema
Bibliothek 2.0 geben und den Stand der tatsächlichen Umsetzung der Web 2.0-Ansätze
in deutschsprachigen Bibliotheken beleuchten. An dieser Stelle ist die Frage erlaubt,
warum es zu einer Zeit, in der es bereits die ersten "Web 3.0"- Konferenzen gibt,
eines Handbuches der Bibliothek 2.0 noch bedarf. Und warum es überhaupt ein deutschsprachiges
Handbuch zur Bibliothek 2.0 braucht, wo es doch bereits verschiedenste Publikationen
zu diesem Thema aus anderen Ländern, insbesondere des angloamerikanischen Raums
gibt. Ist dazu nicht bereits alles gesagt?
author:
- first_name: Julia
full_name: Bergmann, Julia
last_name: Bergmann
- first_name: Patrick
full_name: Danowski, Patrick
id: 2EBD1598-F248-11E8-B48F-1D18A9856A87
last_name: Danowski
orcid: 0000-0002-6026-4409
citation:
ama: 'Bergmann J, Danowski P. Ist Bibliothek 2.0 überhaupt noch relevant? – Eine
Einleitung in das Handbuch. In: Bergmann J, Danowski P, eds. Handbuch Bibliothek
2.0. Bibliotheks- und Informationspraxis 41. De Gruyter; 2010:5-20. doi:10.1515/9783110232103'
apa: Bergmann, J., & Danowski, P. (2010). Ist Bibliothek 2.0 überhaupt noch
relevant? – Eine Einleitung in das Handbuch. In J. Bergmann & P. Danowski
(Eds.), Handbuch Bibliothek 2.0 (pp. 5–20). De Gruyter. https://doi.org/10.1515/9783110232103
chicago: Bergmann, Julia, and Patrick Danowski. “Ist Bibliothek 2.0 Überhaupt Noch
Relevant? – Eine Einleitung in Das Handbuch.” In Handbuch Bibliothek 2.0,
edited by Julia Bergmann and Patrick Danowski, 5–20. Bibliotheks- Und Informationspraxis
41. De Gruyter, 2010. https://doi.org/10.1515/9783110232103.
ieee: J. Bergmann and P. Danowski, “Ist Bibliothek 2.0 überhaupt noch relevant?
– Eine Einleitung in das Handbuch,” in Handbuch Bibliothek 2.0, J. Bergmann
and P. Danowski, Eds. De Gruyter, 2010, pp. 5–20.
ista: 'Bergmann J, Danowski P. 2010.Ist Bibliothek 2.0 überhaupt noch relevant?
– Eine Einleitung in das Handbuch. In: Handbuch Bibliothek 2.0. , 5–20.'
mla: Bergmann, Julia, and Patrick Danowski. “Ist Bibliothek 2.0 Überhaupt Noch Relevant?
– Eine Einleitung in Das Handbuch.” Handbuch Bibliothek 2.0, edited by
Julia Bergmann and Patrick Danowski, De Gruyter, 2010, pp. 5–20, doi:10.1515/9783110232103.
short: J. Bergmann, P. Danowski, in:, J. Bergmann, P. Danowski (Eds.), Handbuch
Bibliothek 2.0, De Gruyter, 2010, pp. 5–20.
date_created: 2018-12-11T12:08:21Z
date_published: 2010-09-23T00:00:00Z
date_updated: 2021-01-12T07:56:15Z
day: '23'
ddc:
- '020'
department:
- _id: E-Lib
doi: 10.1515/9783110232103
editor:
- first_name: Julia
full_name: Bergmann, Julia
last_name: Bergmann
- first_name: Patrick
full_name: Danowski, Patrick
id: 2EBD1598-F248-11E8-B48F-1D18A9856A87
last_name: Danowski
orcid: 0000-0002-6026-4409
file:
- access_level: open_access
checksum: d42cedd48fffa85d75046f396a309fc3
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:06Z
date_updated: 2020-07-14T12:46:27Z
file_id: '5123'
file_name: IST-2012-12-v1+1_9783110232103.5.pdf
file_size: 567580
relation: main_file
file_date_updated: 2020-07-14T12:46:27Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 5 - 20
publication: Handbuch Bibliothek 2.0
publication_status: published
publisher: De Gruyter
publist_id: '1235'
pubrep_id: '12'
quality_controlled: '1'
series_title: Bibliotheks- und Informationspraxis 41
status: public
title: Ist Bibliothek 2.0 überhaupt noch relevant? – Eine Einleitung in das Handbuch
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: book_chapter
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4346'
abstract:
- lang: eng
text: With the term "Library 2.0" the editors mean an institution which applies
the principles of the Web 2.0 such as openness, re-use, collaboration and interaction
in the entire organization. Libraries are extending their service offerings and
work processes to include the potential of Web 2.0 technologies. This changes
the job description and self-image of librarians. The collective volume offers
a complete overview of the topic Library 2.0 and the current state of developments
from a technological, sociological, information theoretical and practice-oriented
perspective.
alternative_title:
- Bibliotheks- und Informationspraxis
article_processing_charge: No
citation:
ama: Danowski P, Bergmann J, eds. Handbuch Bibliothek 2.0. Vol 41. De Gruyter;
2010. doi:10.1515/9783110232103
apa: Danowski, P., & Bergmann, J. (Eds.). (2010). Handbuch Bibliothek 2.0
(Vol. 41). De Gruyter. https://doi.org/10.1515/9783110232103
chicago: Danowski, Patrick, and Julia Bergmann, eds. Handbuch Bibliothek 2.0.
Vol. 41. Bibliothekspraxis. De Gruyter, 2010. https://doi.org/10.1515/9783110232103.
ieee: P. Danowski and J. Bergmann, Eds., Handbuch Bibliothek 2.0, vol. 41.
De Gruyter, 2010.
ista: Danowski P, Bergmann J eds. 2010. Handbuch Bibliothek 2.0, De Gruyter, 405p.
mla: Danowski, Patrick, and Julia Bergmann, editors. Handbuch Bibliothek 2.0.
Vol. 41, De Gruyter, 2010, doi:10.1515/9783110232103.
short: P. Danowski, J. Bergmann, eds., Handbuch Bibliothek 2.0, De Gruyter, 2010.
date_created: 2018-12-11T12:08:23Z
date_published: 2010-09-01T00:00:00Z
date_updated: 2021-12-22T14:41:57Z
day: '01'
department:
- _id: E-Lib
doi: 10.1515/9783110232103
editor:
- first_name: Patrick
full_name: Danowski, Patrick
id: 2EBD1598-F248-11E8-B48F-1D18A9856A87
last_name: Danowski
orcid: 0000-0002-6026-4409
- first_name: Julia
full_name: Bergmann, Julia
last_name: Bergmann
language:
- iso: ger
main_file_link:
- open_access: '1'
url: https://www.degruyter.com/document/doi/10.1515/9783110232103/html
month: '09'
oa: 1
oa_version: Published Version
page: '405'
publication_identifier:
eisbn:
- 9-783-1102-3210-3
isbn:
- 9-783-1102-3209-7
publication_status: published
publisher: De Gruyter
publist_id: '1228'
quality_controlled: '1'
series_title: Bibliothekspraxis
status: public
title: Handbuch Bibliothek 2.0
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: book_editor
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: ' 41'
year: '2010'
...
---
_id: '4361'
abstract:
- lang: eng
text: Depth-bounded processes form the most expressive known fragment of the π-calculus
for which interesting verification problems are still decidable. In this paper
we develop an adequate domain of limits for the well-structured transition systems
that are induced by depth-bounded processes. An immediate consequence of our result
is that there exists a forward algorithm that decides the covering problem for
this class. Unlike backward algorithms, the forward algorithm terminates even
if the depth of the process is not known a priori. More importantly, our result
suggests a whole spectrum of forward algorithms that enable the effective verification
of a large class of mobile systems.
alternative_title:
- LNCS
author:
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Wies T, Zufferey D, Henzinger TA. Forward analysis of depth-bounded processes.
In: Ong L, ed. Vol 6014. Springer; 2010:94-108. doi:10.1007/978-3-642-12032-9_8'
apa: 'Wies, T., Zufferey, D., & Henzinger, T. A. (2010). Forward analysis of
depth-bounded processes. In L. Ong (Ed.) (Vol. 6014, pp. 94–108). Presented at
the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos,
Cyprus: Springer. https://doi.org/10.1007/978-3-642-12032-9_8'
chicago: Wies, Thomas, Damien Zufferey, and Thomas A Henzinger. “Forward Analysis
of Depth-Bounded Processes.” edited by Luke Ong, 6014:94–108. Springer, 2010.
https://doi.org/10.1007/978-3-642-12032-9_8.
ieee: 'T. Wies, D. Zufferey, and T. A. Henzinger, “Forward analysis of depth-bounded
processes,” presented at the FoSSaCS: Foundations of Software Science and Computation
Structures, Paphos, Cyprus, 2010, vol. 6014, pp. 94–108.'
ista: 'Wies T, Zufferey D, Henzinger TA. 2010. Forward analysis of depth-bounded
processes. FoSSaCS: Foundations of Software Science and Computation Structures,
LNCS, vol. 6014, 94–108.'
mla: Wies, Thomas, et al. Forward Analysis of Depth-Bounded Processes. Edited
by Luke Ong, vol. 6014, Springer, 2010, pp. 94–108, doi:10.1007/978-3-642-12032-9_8.
short: T. Wies, D. Zufferey, T.A. Henzinger, in:, L. Ong (Ed.), Springer, 2010,
pp. 94–108.
conference:
end_date: 2010-03-28
location: Paphos, Cyprus
name: 'FoSSaCS: Foundations of Software Science and Computation Structures'
start_date: 2010-03-20
date_created: 2018-12-11T12:08:27Z
date_published: 2010-03-01T00:00:00Z
date_updated: 2023-09-07T11:36:36Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-12032-9_8
editor:
- first_name: Luke
full_name: Ong, Luke
last_name: Ong
file:
- access_level: open_access
checksum: 3e610de84937d821316362658239134a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:17Z
date_updated: 2020-07-14T12:46:27Z
file_id: '4677'
file_name: IST-2012-50-v1+1_Forward_analysis_of_depth-bounded_processes.pdf
file_size: 240766
relation: main_file
file_date_updated: 2020-07-14T12:46:27Z
has_accepted_license: '1'
intvolume: ' 6014'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
page: 94 - 108
publication_status: published
publisher: Springer
publist_id: '1099'
pubrep_id: '50'
quality_controlled: '1'
related_material:
record:
- id: '1405'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Forward analysis of depth-bounded processes
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6014
year: '2010'
...
---
_id: '4362'
abstract:
- lang: eng
text: Software transactional memories (STMs) promise simple and efficient concurrent
programming. Several correctness properties have been proposed for STMs. Based
on a bounded conflict graph algorithm for verifying correctness of STMs, we develop
TRACER, a tool for runtime verification of STM implementations. The novelty of
TRACER lies in the way it combines coarse and precise runtime analyses to guarantee
sound and complete verification in an efficient manner. We implement TRACER in
the TL2 STM implementation. We evaluate the performance of TRACER on STAMP benchmarks.
While a precise runtime verification technique based on conflict graphs results
in an average slowdown of 60x, the two-level approach of TRACER performs complete
verification with an average slowdown of around 25x across different benchmarks.
alternative_title:
- LNCS
author:
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Singh V. Runtime verification for software transactional memories. In: Sokolsky
O, Rosu G, Tilmann N, et al., eds. Vol 6418. Springer; 2010:421-435. doi:10.1007/978-3-642-16612-9_32'
apa: 'Singh, V. (2010). Runtime verification for software transactional memories.
In O. Sokolsky, G. Rosu, N. Tilmann, H. Barringer, Y. Falcone, B. Finkbeiner,
… G. Pace (Eds.) (Vol. 6418, pp. 421–435). Presented at the RV: International
Conference on Runtime Verification, St. Julians, Malta: Springer. https://doi.org/10.1007/978-3-642-16612-9_32'
chicago: Singh, Vasu. “Runtime Verification for Software Transactional Memories.”
edited by Oleg Sokolsky, Grigore Rosu, Nikolai Tilmann, Howard Barringer, Ylies
Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, and Gordon Pace, 6418:421–35.
Springer, 2010. https://doi.org/10.1007/978-3-642-16612-9_32.
ieee: 'V. Singh, “Runtime verification for software transactional memories,” presented
at the RV: International Conference on Runtime Verification, St. Julians, Malta,
2010, vol. 6418, pp. 421–435.'
ista: 'Singh V. 2010. Runtime verification for software transactional memories.
RV: International Conference on Runtime Verification, LNCS, vol. 6418, 421–435.'
mla: Singh, Vasu. Runtime Verification for Software Transactional Memories.
Edited by Oleg Sokolsky et al., vol. 6418, Springer, 2010, pp. 421–35, doi:10.1007/978-3-642-16612-9_32.
short: V. Singh, in:, O. Sokolsky, G. Rosu, N. Tilmann, H. Barringer, Y. Falcone,
B. Finkbeiner, K. Havelund, I. Lee, G. Pace (Eds.), Springer, 2010, pp. 421–435.
conference:
end_date: 2010-11-04
location: St. Julians, Malta
name: 'RV: International Conference on Runtime Verification'
start_date: 2010-11-01
date_created: 2018-12-11T12:08:28Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:25Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-16612-9_32
editor:
- first_name: Oleg
full_name: Sokolsky, Oleg
last_name: Sokolsky
- first_name: Grigore
full_name: Rosu, Grigore
last_name: Rosu
- first_name: Nikolai
full_name: Tilmann, Nikolai
last_name: Tilmann
- first_name: Howard
full_name: Barringer, Howard
last_name: Barringer
- first_name: Ylies
full_name: Falcone, Ylies
last_name: Falcone
- first_name: Bernd
full_name: Finkbeiner, Bernd
last_name: Finkbeiner
- first_name: Klaus
full_name: Havelund, Klaus
last_name: Havelund
- first_name: Insup
full_name: Lee, Insup
last_name: Lee
- first_name: Gordon
full_name: Pace, Gordon
last_name: Pace
intvolume: ' 6418'
language:
- iso: eng
month: '01'
oa_version: None
page: 421 - 435
publication_status: published
publisher: Springer
publist_id: '1096'
quality_controlled: '1'
scopus_import: 1
status: public
title: Runtime verification for software transactional memories
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6418
year: '2010'
...
---
_id: '4369'
abstract:
- lang: eng
text: In this paper we propose a novel technique for constructing timed automata
from properties expressed in the logic mtl, under bounded-variability assumptions.
We handle full mtl and include all future operators. Our construction is based
on separation of the continuous time monitoring of the input sequence and discrete
predictions regarding the future. The separation of the continuous from the discrete
allows us to determinize our automata in an exponential construction that does
not increase the number of clocks. This leads to a doubly exponential construction
from mtl to deterministic timed automata, compared with triply exponential using
existing approaches. We offer an alternative to the existing approach to linear
real-time model checking, which has never been implemented. It further offers
a unified framework for model checking, runtime monitoring, and synthesis, in
an approach that can reuse tools, implementations, and insights from the discrete
setting.
alternative_title:
- LNCS
author:
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Nickovic D, Piterman N. From MTL to deterministic timed automata. In: Henzinger
TA, Chatterjee K, eds. Vol 6246. Springer; 2010:152-167. doi:10.1007/978-3-642-15297-9_13'
apa: 'Nickovic, D., & Piterman, N. (2010). From MTL to deterministic timed automata.
In T. A. Henzinger & K. Chatterjee (Eds.) (Vol. 6246, pp. 152–167). Presented
at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg,
Austria: Springer. https://doi.org/10.1007/978-3-642-15297-9_13'
chicago: Nickovic, Dejan, and Nir Piterman. “From MTL to Deterministic Timed Automata.”
edited by Thomas A. Henzinger and Krishnendu Chatterjee, 6246:152–67. Springer,
2010. https://doi.org/10.1007/978-3-642-15297-9_13.
ieee: 'D. Nickovic and N. Piterman, “From MTL to deterministic timed automata,”
presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg,
Austria, 2010, vol. 6246, pp. 152–167.'
ista: 'Nickovic D, Piterman N. 2010. From MTL to deterministic timed automata. FORMATS:
Formal Modeling and Analysis of Timed Systems, LNCS, vol. 6246, 152–167.'
mla: Nickovic, Dejan, and Nir Piterman. From MTL to Deterministic Timed Automata.
Edited by Thomas A. Henzinger and Krishnendu Chatterjee, vol. 6246, Springer,
2010, pp. 152–67, doi:10.1007/978-3-642-15297-9_13.
short: D. Nickovic, N. Piterman, in:, T.A. Henzinger, K. Chatterjee (Eds.), Springer,
2010, pp. 152–167.
conference:
end_date: 2010-09-10
location: Klosterneuburg, Austria
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
start_date: 2010-09-08
date_created: 2018-12-11T12:08:30Z
date_published: 2010-09-08T00:00:00Z
date_updated: 2021-01-12T07:56:27Z
day: '08'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-15297-9_13
ec_funded: 1
editor:
- first_name: Thomas A.
full_name: Henzinger, Thomas A.
last_name: Henzinger
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
last_name: Chatterjee
file:
- access_level: open_access
checksum: b0ca5f5fbe8a3d20ccbc6f51a344a459
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:43Z
date_updated: 2020-07-14T12:46:27Z
file_id: '5028'
file_name: IST-2012-49-v1+1_From_MTL_to_deterministic_timed_automata.pdf
file_size: 249789
relation: main_file
file_date_updated: 2020-07-14T12:46:27Z
has_accepted_license: '1'
intvolume: ' 6246'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 152 - 167
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '1090'
pubrep_id: '49'
quality_controlled: '1'
scopus_import: 1
status: public
title: From MTL to deterministic timed automata
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6246
year: '2010'
...
---
_id: '4378'
abstract:
- lang: eng
text: 'Techniques such as verification condition generation, predicate abstraction,
and expressive type systems reduce software verification to proving formulas in
expressive logics. Programs and their specifications often make use of data structures
such as sets, multisets, algebraic data types, or graphs. Consequently, formulas
generated from verification also involve such data structures. To automate the
proofs of such formulas we propose a logic (a “calculus”) of such data structures.
We build the calculus by starting from decidable logics of individual data structures,
and connecting them through functions and sets, in ways that go beyond the frameworks
such as Nelson-Oppen. The result are new decidable logics that can simultaneously
specify properties of different kinds of data structures and overcome the limitations
of the individual logics. Several of our decidable logics include abstraction
functions that map a data structure into its more abstract view (a tree into a
multiset, a multiset into a set), into a numerical quantity (the size or the height),
or into the truth value of a candidate data structure invariant (sortedness, or
the heap property). For algebraic data types, we identify an asymptotic many-to-one
condition on the abstraction function that guarantees the existence of a decision
procedure. In addition to the combination based on abstraction functions, we can
combine multiple data structure theories if they all reduce to the same data structure
logic. As an instance of this approach, we describe a decidable logic whose formulas
are propositional combinations of formulas in: weak monadic second-order logic
of two successors, two-variable logic with counting, multiset algebra with Presburger
arithmetic, the Bernays-Schönfinkel-Ramsey class of first-order logic, and the
logic of algebraic data types with the set content function. The subformulas in
this combination can share common variables that refer to sets of objects along
with the common set algebra operations. Such sound and complete combination is
possible because the relations on sets definable in the component logics are all
expressible in Boolean Algebra with Presburger Arithmetic. Presburger arithmetic
and its new extensions play an important role in our decidability results. In
several cases, when we combine logics that belong to NP, we can prove the satisfiability
for the combined logic is still in NP.'
alternative_title:
- LNCS
author:
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
- first_name: Ruzica
full_name: Piskac, Ruzica
last_name: Piskac
- first_name: Philippe
full_name: Suter, Philippe
last_name: Suter
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Kuncak V, Piskac R, Suter P, Wies T. Building a calculus of data structures.
In: Barthe G, Hermenegildo M, eds. Vol 5944. Springer; 2010:26-44. doi:10.1007/978-3-642-11319-2_6'
apa: 'Kuncak, V., Piskac, R., Suter, P., & Wies, T. (2010). Building a calculus
of data structures. In G. Barthe & M. Hermenegildo (Eds.) (Vol. 5944, pp.
26–44). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
Madrid, Spain: Springer. https://doi.org/10.1007/978-3-642-11319-2_6'
chicago: Kuncak, Viktor, Ruzica Piskac, Philippe Suter, and Thomas Wies. “Building
a Calculus of Data Structures.” edited by Gilles Barthe and Manuel Hermenegildo,
5944:26–44. Springer, 2010. https://doi.org/10.1007/978-3-642-11319-2_6.
ieee: 'V. Kuncak, R. Piskac, P. Suter, and T. Wies, “Building a calculus of data
structures,” presented at the VMCAI: Verification, Model Checking and Abstract
Interpretation, Madrid, Spain, 2010, vol. 5944, pp. 26–44.'
ista: 'Kuncak V, Piskac R, Suter P, Wies T. 2010. Building a calculus of data structures.
VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 5944,
26–44.'
mla: Kuncak, Viktor, et al. Building a Calculus of Data Structures. Edited
by Gilles Barthe and Manuel Hermenegildo, vol. 5944, Springer, 2010, pp. 26–44,
doi:10.1007/978-3-642-11319-2_6.
short: V. Kuncak, R. Piskac, P. Suter, T. Wies, in:, G. Barthe, M. Hermenegildo
(Eds.), Springer, 2010, pp. 26–44.
conference:
end_date: 2010-01-19
location: Madrid, Spain
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2010-01-17
date_created: 2018-12-11T12:08:33Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:31Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-11319-2_6
editor:
- first_name: Gilles
full_name: Barthe, Gilles
last_name: Barthe
- first_name: Manuel
full_name: Hermenegildo, Manuel
last_name: Hermenegildo
intvolume: ' 5944'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://infoscience.epfl.ch/record/161290/
month: '01'
oa: 1
oa_version: Submitted Version
page: 26 - 44
publication_status: published
publisher: Springer
publist_id: '1081'
quality_controlled: '1'
scopus_import: 1
status: public
title: Building a calculus of data structures
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 5944
year: '2010'
...
---
_id: '4380'
abstract:
- lang: eng
text: Cloud computing is an emerging paradigm aimed to offer users pay-per-use computing
resources, while leaving the burden of managing the computing infrastructure to
the cloud provider. We present a new programming and pricing model that gives
the cloud user the flexibility of trading execution speed and price on a per-job
basis. We discuss the scheduling and resource management challenges for the cloud
provider that arise in the implementation of this model. We argue that techniques
from real-time and embedded software can be useful in this context.
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Anmol
full_name: Tomar, Anmol
id: 3D8D36B6-F248-11E8-B48F-1D18A9856A87
last_name: Tomar
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. A marketplace for cloud
resources. In: ACM; 2010:1-8. doi:10.1145/1879021.1879022'
apa: 'Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010).
A marketplace for cloud resources (pp. 1–8). Presented at the EMSOFT: Embedded
Software , Arizona, USA: ACM. https://doi.org/10.1145/1879021.1879022'
chicago: Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey.
“A Marketplace for Cloud Resources,” 1–8. ACM, 2010. https://doi.org/10.1145/1879021.1879022.
ieee: 'T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “A marketplace
for cloud resources,” presented at the EMSOFT: Embedded Software , Arizona, USA,
2010, pp. 1–8.'
ista: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. A marketplace for
cloud resources. EMSOFT: Embedded Software , 1–8.'
mla: Henzinger, Thomas A., et al. A Marketplace for Cloud Resources. ACM,
2010, pp. 1–8, doi:10.1145/1879021.1879022.
short: T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2010,
pp. 1–8.
conference:
end_date: 2010-10-29
location: Arizona, USA
name: 'EMSOFT: Embedded Software '
start_date: 2010-10-24
date_created: 2018-12-11T12:08:33Z
date_published: 2010-10-24T00:00:00Z
date_updated: 2021-01-12T07:56:32Z
day: '24'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/1879021.1879022
file:
- access_level: open_access
checksum: 7680dd24016810710f7c977bc94f85e9
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:42Z
date_updated: 2020-07-14T12:46:28Z
file_id: '4767'
file_name: IST-2012-48-v1+1_A_marketplace_for_cloud_resources.pdf
file_size: 222626
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 1 - 8
publication_status: published
publisher: ACM
publist_id: '1078'
pubrep_id: '48'
quality_controlled: '1'
scopus_import: 1
status: public
title: A marketplace for cloud resources
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4381'
abstract:
- lang: eng
text: Cloud computing aims to give users virtually unlimited pay-per-use computing
resources without the burden of managing the underlying infrastructure. We claim
that, in order to realize the full potential of cloud computing, the user must
be presented with a pricing model that offers flexibility at the requirements
level, such as a choice between different degrees of execution speed and the cloud
provider must be presented with a programming model that offers flexibility at
the execution level, such as a choice between different scheduling policies. In
such a flexible framework, with each job, the user purchases a virtual computer
with the desired speed and cost characteristics, and the cloud provider can optimize
the utilization of resources across a stream of jobs from different users. We
designed a flexible framework to test our hypothesis, which is called FlexPRICE
(Flexible Provisioning of Resources in a Cloud Environment) and works as follows.
A user presents a job to the cloud. The cloud finds different schedules to execute
the job and presents a set of quotes to the user in terms of price and duration
for the execution. The user then chooses a particular quote and the cloud is obliged
to execute the job according to the chosen quote. FlexPRICE thus hides the complexity
of the actual scheduling decisions from the user, but still provides enough flexibility
to meet the users actual demands. We implemented FlexPRICE in a simulator called
PRICES that allows us to experiment with our framework. We observe that FlexPRICE
provides a wide range of execution options-from fast and expensive to slow and
cheap-- for the whole spectrum of data-intensive and computation-intensive jobs.
We also observe that the set of quotes computed by FlexPRICE do not vary as the
number of simultaneous jobs increases.
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Anmol
full_name: Tomar, Anmol
id: 3D8D36B6-F248-11E8-B48F-1D18A9856A87
last_name: Tomar
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. FlexPRICE: Flexible provisioning
of resources in a cloud environment. In: IEEE; 2010:83-90. doi:10.1109/CLOUD.2010.71'
apa: 'Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010).
FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90).
Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. https://doi.org/10.1109/CLOUD.2010.71'
chicago: 'Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien
Zufferey. “FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment,”
83–90. IEEE, 2010. https://doi.org/10.1109/CLOUD.2010.71.'
ieee: 'T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “FlexPRICE:
Flexible provisioning of resources in a cloud environment,” presented at the CLOUD:
Cloud Computing, Miami, USA, 2010, pp. 83–90.'
ista: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. FlexPRICE: Flexible
provisioning of resources in a cloud environment. CLOUD: Cloud Computing, 83–90.'
mla: 'Henzinger, Thomas A., et al. FlexPRICE: Flexible Provisioning of Resources
in a Cloud Environment. IEEE, 2010, pp. 83–90, doi:10.1109/CLOUD.2010.71.'
short: T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010,
pp. 83–90.
conference:
end_date: 2010-07-10
location: Miami, USA
name: 'CLOUD: Cloud Computing'
start_date: 2010-07-05
date_created: 2018-12-11T12:08:33Z
date_published: 2010-08-26T00:00:00Z
date_updated: 2021-01-12T07:56:33Z
day: '26'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1109/CLOUD.2010.71
file:
- access_level: open_access
checksum: 98e534675339a8e2beca08890d048145
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:03Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5188'
file_name: IST-2012-47-v1+1_FlexPRICE-_Flexible_provisioning_of_resources_in_a_cloud_environment.pdf
file_size: 467436
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 83 - 90
publication_status: published
publisher: IEEE
publist_id: '1077'
pubrep_id: '47'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'FlexPRICE: Flexible provisioning of resources in a cloud environment'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4382'
abstract:
- lang: eng
text: 'Transactional memory (TM) has shown potential to simplify the task of writing
concurrent programs. Inspired by classical work on databases, formal definitions
of the semantics of TM executions have been proposed. Many of these definitions
assumed that accesses to shared data are solely performed through transactions.
In practice, due to legacy code and concurrency libraries, transactions in a TM
have to share data with non-transactional operations. The semantics of such interaction,
while widely discussed by practitioners, lacks a clear formal specification. Those
interactions can vary, sometimes in subtle ways, between TM implementations and
underlying memory models. We propose a correctness condition for TMs, parametrized
opacity, to formally capture the now folklore notion of strong atomicity by stipulating
the two following intuitive requirements: first, every transaction appears as
if it is executed instantaneously with respect to other transactions and non-transactional
operations, and second, non-transactional operations conform to the given underlying
memory model. We investigate the inherent cost of implementing parametrized opacity.
We first prove that parametrized opacity requires either instrumenting non-transactional
operations (for most memory models) or writing to memory by transactions using
potentially expensive read-modify-write instructions (such as compare-and-swap).
Then, we show that for a class of practical relaxed memory models, parametrized
opacity can indeed be implemented with constant-time instrumentation of non-transactional
writes and no instrumentation of non-transactional reads. We show that, in practice,
parametrizing the notion of correctness allows developing more efficient TM implementations.'
author:
- first_name: Rachid
full_name: Guerraoui, Rachid
last_name: Guerraoui
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Michal
full_name: Kapalka, Michal
last_name: Kapalka
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Guerraoui R, Henzinger TA, Kapalka M, Singh V. Transactions in the jungle.
In: ACM; 2010:263-272. doi:10.1145/1810479.1810529'
apa: 'Guerraoui, R., Henzinger, T. A., Kapalka, M., & Singh, V. (2010). Transactions
in the jungle (pp. 263–272). Presented at the SPAA: ACM Symposium on Parallel
Algorithms and Architectures, Santorini, Greece: ACM. https://doi.org/10.1145/1810479.1810529'
chicago: Guerraoui, Rachid, Thomas A Henzinger, Michal Kapalka, and Vasu Singh.
“Transactions in the Jungle,” 263–72. ACM, 2010. https://doi.org/10.1145/1810479.1810529.
ieee: 'R. Guerraoui, T. A. Henzinger, M. Kapalka, and V. Singh, “Transactions in
the jungle,” presented at the SPAA: ACM Symposium on Parallel Algorithms and Architectures,
Santorini, Greece, 2010, pp. 263–272.'
ista: 'Guerraoui R, Henzinger TA, Kapalka M, Singh V. 2010. Transactions in the
jungle. SPAA: ACM Symposium on Parallel Algorithms and Architectures, 263–272.'
mla: Guerraoui, Rachid, et al. Transactions in the Jungle. ACM, 2010, pp.
263–72, doi:10.1145/1810479.1810529.
short: R. Guerraoui, T.A. Henzinger, M. Kapalka, V. Singh, in:, ACM, 2010, pp. 263–272.
conference:
end_date: 2010-06-15
location: Santorini, Greece
name: 'SPAA: ACM Symposium on Parallel Algorithms and Architectures'
start_date: 2010-06-13
date_created: 2018-12-11T12:08:34Z
date_published: 2010-06-13T00:00:00Z
date_updated: 2021-01-12T07:56:33Z
day: '13'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/1810479.1810529
file:
- access_level: open_access
checksum: f2ad6c00a6304da34bf21bcdcfd36c4b
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:28Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5080'
file_name: IST-2012-46-v1+1_Transactions_in_the_jungle.pdf
file_size: 246409
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 263 - 272
publication_status: published
publisher: ACM
publist_id: '1076'
pubrep_id: '46'
quality_controlled: '1'
status: public
title: Transactions in the jungle
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4388'
abstract:
- lang: eng
text: GIST is a tool that (a) solves the qualitative analysis problem of turn-based
probabilistic games with ω-regular objectives; and (b) synthesizes reasonable
environment assumptions for synthesis of unrealizable specifications. Our tool
provides the first and efficient implementations of several reduction-based techniques
to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic
games for synthesizing environment assumptions for unrealizable specifications.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. GIST: A solver for
probabilistic games. In: Vol 6174. Springer; 2010:665-669. doi:10.1007/978-3-642-14295-6_57'
apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., & Radhakrishna, A. (2010).
GIST: A solver for probabilistic games (Vol. 6174, pp. 665–669). Presented at
the CAV: Computer Aided Verification, Edinburgh, UK: Springer. https://doi.org/10.1007/978-3-642-14295-6_57'
chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Arjun
Radhakrishna. “GIST: A Solver for Probabilistic Games,” 6174:665–69. Springer,
2010. https://doi.org/10.1007/978-3-642-14295-6_57.'
ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and A. Radhakrishna, “GIST:
A solver for probabilistic games,” presented at the CAV: Computer Aided Verification,
Edinburgh, UK, 2010, vol. 6174, pp. 665–669.'
ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. 2010. GIST: A solver
for probabilistic games. CAV: Computer Aided Verification, LNCS, vol. 6174, 665–669.'
mla: 'Chatterjee, Krishnendu, et al. GIST: A Solver for Probabilistic Games.
Vol. 6174, Springer, 2010, pp. 665–69, doi:10.1007/978-3-642-14295-6_57.'
short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, A. Radhakrishna, in:, Springer,
2010, pp. 665–669.
conference:
end_date: 2010-07-17
location: Edinburgh, UK
name: 'CAV: Computer Aided Verification'
start_date: 2010-07-15
date_created: 2018-12-11T12:08:36Z
date_published: 2010-07-01T00:00:00Z
date_updated: 2023-02-23T12:24:17Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_57
ec_funded: 1
external_id:
arxiv:
- '1004.2367'
file:
- access_level: open_access
checksum: 0b2ef8c4037ffccc6902d93081af24f7
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:33Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5221'
file_name: IST-2012-43-v1+1_GIST-_A_solver_for_probabilistic_games.pdf
file_size: 293605
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
intvolume: ' 6174'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 665 - 669
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '1068'
pubrep_id: '43'
quality_controlled: '1'
related_material:
record:
- id: '5393'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: 'GIST: A solver for probabilistic games'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...