---
_id: '3861'
abstract:
- lang: eng
text: We introduce strategy logic, a logic that treats strategies in two-player
games as explicit first-order objects. The explicit treatment of strategies allows
us to specify properties of nonzero-sum games in a simple and natural way. We
show that the one-alternation fragment of strategy logic is strong enough to express
the existence of Nash equilibria and secure equilibria, and subsumes other logics
that were introduced to reason about games, such as ATL, ATL*, and game logic.
We show that strategy logic is decidable, by constructing tree automata that recognize
sets of strategies. While for the general logic, our decision procedure is nonelementary,
for the simple fragment that is used above we show that the complexity is polynomial
in the size of the game graph and optimal in the size of the formula (ranging
from polynomial to 2EXPTIME depending on the form of the formula).
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: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: Chatterjee K, Henzinger TA, Piterman N. Strategy logic. Information and
Computation. 2010;208(6):677-693. doi:10.1016/j.ic.2009.07.004
apa: Chatterjee, K., Henzinger, T. A., & Piterman, N. (2010). Strategy logic.
Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2009.07.004
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Nir Piterman. “Strategy
Logic.” Information and Computation. Elsevier, 2010. https://doi.org/10.1016/j.ic.2009.07.004.
ieee: K. Chatterjee, T. A. Henzinger, and N. Piterman, “Strategy logic,” Information
and Computation, vol. 208, no. 6. Elsevier, pp. 677–693, 2010.
ista: Chatterjee K, Henzinger TA, Piterman N. 2010. Strategy logic. Information
and Computation. 208(6), 677–693.
mla: Chatterjee, Krishnendu, et al. “Strategy Logic.” Information and Computation,
vol. 208, no. 6, Elsevier, 2010, pp. 677–93, doi:10.1016/j.ic.2009.07.004.
short: K. Chatterjee, T.A. Henzinger, N. Piterman, Information and Computation 208
(2010) 677–693.
date_created: 2018-12-11T12:05:34Z
date_published: 2010-06-01T00:00:00Z
date_updated: 2023-02-23T11:46:57Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2009.07.004
file:
- access_level: open_access
checksum: 13bff93f3c2a014e2908145a4517f177
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:54Z
date_updated: 2020-07-14T12:46:18Z
file_id: '4911'
file_name: IST-2012-56-v1+1_Strategy_logic.pdf
file_size: 189120
relation: main_file
file_date_updated: 2020-07-14T12:46:18Z
has_accepted_license: '1'
intvolume: ' 208'
issue: '6'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 677 - 693
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '2317'
pubrep_id: '56'
quality_controlled: '1'
related_material:
record:
- id: '3884'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Strategy logic
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 208
year: '2010'
...
---
_id: '3863'
abstract:
- lang: eng
text: 'We consider two-player parity games with imperfect information in which strategies
rely on observations that provide imperfect information about the history of a
play. To solve such games, i.e., to determine the winning regions of players and
corresponding winning strategies, one can use the subset construction to build
an equivalent perfect-information game. Recently, an algorithm that avoids the
inefficient subset construction has been proposed. The algorithm performs a fixed-point
computation in a lattice of antichains, thus maintaining a succinct representation
of state sets. However, this representation does not allow to recover winning
strategies. In this paper, we build on the antichain approach to develop an algorithm
for constructing the winning strategies in parity games of imperfect information.
One major obstacle in adapting the classical procedure is that the complementation
of attractor sets would break the invariant of downward-closedness on which the
antichain representation relies. We overcome this difficulty by decomposing problem
instances recursively into games with a combination of reachability, safety, and
simpler parity conditions. We also report on an experimental implementation of
our algorithm: to our knowledge, this is the first implementation of a procedure
for solving imperfect-information parity games on graphs.'
author:
- first_name: Dietmar
full_name: Berwanger, Dietmar
last_name: Berwanger
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: De Wulf, Martin
last_name: De Wulf
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Berwanger D, Chatterjee K, De Wulf M, Doyen L, Henzinger TA. Strategy construction
for parity games with imperfect information. Information and Computation.
2010;208(10):1206-1220. doi:10.1016/j.ic.2009.09.006
apa: Berwanger, D., Chatterjee, K., De Wulf, M., Doyen, L., & Henzinger, T.
A. (2010). Strategy construction for parity games with imperfect information.
Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2009.09.006
chicago: Berwanger, Dietmar, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen,
and Thomas A Henzinger. “Strategy Construction for Parity Games with Imperfect
Information.” Information and Computation. Elsevier, 2010. https://doi.org/10.1016/j.ic.2009.09.006.
ieee: D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, and T. A. Henzinger, “Strategy
construction for parity games with imperfect information,” Information and
Computation, vol. 208, no. 10. Elsevier, pp. 1206–1220, 2010.
ista: Berwanger D, Chatterjee K, De Wulf M, Doyen L, Henzinger TA. 2010. Strategy
construction for parity games with imperfect information. Information and Computation.
208(10), 1206–1220.
mla: Berwanger, Dietmar, et al. “Strategy Construction for Parity Games with Imperfect
Information.” Information and Computation, vol. 208, no. 10, Elsevier,
2010, pp. 1206–20, doi:10.1016/j.ic.2009.09.006.
short: D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, T.A. Henzinger, Information
and Computation 208 (2010) 1206–1220.
date_created: 2018-12-11T12:05:35Z
date_published: 2010-10-01T00:00:00Z
date_updated: 2023-02-23T11:46:47Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2009.09.006
ec_funded: 1
file:
- access_level: open_access
checksum: 29d146e4f8049dbb7f80bbf7ea3700ed
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:44Z
date_updated: 2020-07-14T12:46:18Z
file_id: '5300'
file_name: IST-2012-58-v1+1_Strategy_construction_for_parity_games_with_imperfect_information.pdf
file_size: 287496
relation: main_file
file_date_updated: 2020-07-14T12:46:18Z
has_accepted_license: '1'
intvolume: ' 208'
issue: '10'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 1206 - 1220
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '2319'
pubrep_id: '58'
quality_controlled: '1'
related_material:
record:
- id: '3880'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Strategy construction for parity games with imperfect information
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 208
year: '2010'
...
---
_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: '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: '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'
...
---
_id: '4389'
abstract:
- lang: eng
text: 'Digital components play a central role in the design of complex embedded
systems. These components are interconnected with other, possibly analog, devices
and the physical environment. This environment cannot be entirely captured and
can provide inaccurate input data to the component. It is thus important for digital
components to have a robust behavior, i.e. the presence of a small change in the
input sequences should not result in a drastic change in the output sequences.
In this paper, we study a notion of robustness for sequential circuits. However,
since sequential circuits may have parts that are naturally discontinuous (e.g.,
digital controllers with switching behavior), we need a flexible framework that
accommodates this fact and leaves discontinuous parts of the circuit out from
the robustness analysis. As a consequence, we consider sequential circuits that
have their input variables partitioned into two disjoint sets: control and disturbance
variables. Our contributions are (1) a definition of robustness for sequential
circuits as a form of continuity with respect to disturbance variables, (2) the
characterization of the exact class of sequential circuits that are robust according
to our definition, (3) an algorithm to decide whether a sequential circuit is
robust or not.'
author:
- 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
- first_name: Axel
full_name: Legay, Axel
last_name: Legay
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Doyen L, Henzinger TA, Legay A, Nickovic D. Robustness of sequential circuits.
In: IEEE; 2010:77-84. doi:10.1109/ACSD.2010.26'
apa: 'Doyen, L., Henzinger, T. A., Legay, A., & Nickovic, D. (2010). Robustness
of sequential circuits (pp. 77–84). Presented at the ACSD: Application of Concurrency
to System Design, IEEE. https://doi.org/10.1109/ACSD.2010.26'
chicago: Doyen, Laurent, Thomas A Henzinger, Axel Legay, and Dejan Nickovic. “Robustness
of Sequential Circuits,” 77–84. IEEE, 2010. https://doi.org/10.1109/ACSD.2010.26.
ieee: 'L. Doyen, T. A. Henzinger, A. Legay, and D. Nickovic, “Robustness of sequential
circuits,” presented at the ACSD: Application of Concurrency to System Design,
2010, pp. 77–84.'
ista: 'Doyen L, Henzinger TA, Legay A, Nickovic D. 2010. Robustness of sequential
circuits. ACSD: Application of Concurrency to System Design, 77–84.'
mla: Doyen, Laurent, et al. Robustness of Sequential Circuits. IEEE, 2010,
pp. 77–84, doi:10.1109/ACSD.2010.26.
short: L. Doyen, T.A. Henzinger, A. Legay, D. Nickovic, in:, IEEE, 2010, pp. 77–84.
conference:
name: 'ACSD: Application of Concurrency to System Design'
date_created: 2018-12-11T12:08:36Z
date_published: 2010-08-23T00:00:00Z
date_updated: 2021-01-12T07:56:36Z
day: '23'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1109/ACSD.2010.26
file:
- access_level: open_access
checksum: 42b2952bfc6b6974617bd554842b904a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:10Z
date_updated: 2020-07-14T12:46:28Z
file_id: '4733'
file_name: IST-2012-44-v1+1_Robustness_of_sequential_circuits.pdf
file_size: 159920
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: 77 - 84
publication_status: published
publisher: IEEE
publist_id: '1069'
pubrep_id: '44'
quality_controlled: '1'
scopus_import: 1
status: public
title: Robustness of sequential circuits
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4390'
abstract:
- lang: eng
text: Concurrent data structures with fine-grained synchronization are notoriously
difficult to implement correctly. The difficulty of reasoning about these implementations
does not stem from the number of variables or the program size, but rather from
the large number of possible interleavings. These implementations are therefore
prime candidates for model checking. We introduce an algorithm for verifying linearizability
of singly-linked heap-based concurrent data structures. We consider a model consisting
of an unbounded heap where each vertex stores an element from an unbounded data
domain, with a restricted set of operations for testing and updating pointers
and data elements. Our main result is that linearizability is decidable for programs
that invoke a fixed number of methods, possibly in parallel. This decidable fragment
covers many of the common implementation techniques — fine-grained locking, lazy
synchronization, and lock-free synchronization. We also show how the technique
can be used to verify optimistic implementations with the help of programmer annotations.
We developed a verification tool CoLT and evaluated it on a representative sample
of Java implementations of the concurrent set data structure. The tool verified
linearizability of a number of implementations, found a known error in a lock-free
implementation and proved that the corrected version is linearizable.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
- first_name: Swarat
full_name: Chaudhuri, Swarat
last_name: Chaudhuri
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
citation:
ama: 'Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. Model checking of
linearizability of concurrent list implementations. In: Vol 6174. Springer; 2010:465-479.
doi:10.1007/978-3-642-14295-6_41'
apa: 'Cerny, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., & Alur, R. (2010).
Model checking of linearizability of concurrent list implementations (Vol. 6174,
pp. 465–479). Presented at the CAV: Computer Aided Verification, Edinburgh, UK:
Springer. https://doi.org/10.1007/978-3-642-14295-6_41'
chicago: Cerny, Pavol, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, and
Rajeev Alur. “Model Checking of Linearizability of Concurrent List Implementations,”
6174:465–79. Springer, 2010. https://doi.org/10.1007/978-3-642-14295-6_41.
ieee: 'P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur, “Model
checking of linearizability of concurrent list implementations,” presented at
the CAV: Computer Aided Verification, Edinburgh, UK, 2010, vol. 6174, pp. 465–479.'
ista: 'Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. 2010. Model checking
of linearizability of concurrent list implementations. CAV: Computer Aided Verification,
LNCS, vol. 6174, 465–479.'
mla: Cerny, Pavol, et al. Model Checking of Linearizability of Concurrent List
Implementations. Vol. 6174, Springer, 2010, pp. 465–79, doi:10.1007/978-3-642-14295-6_41.
short: P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, R. Alur, in:, Springer,
2010, pp. 465–479.
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:12Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_41
file:
- access_level: open_access
checksum: 2eb211ce40b3c4988bce3a3592980704
content_type: application/pdf
creator: dernst
date_created: 2020-05-19T16:31:56Z
date_updated: 2020-07-14T12:46:28Z
file_id: '7873'
file_name: 2010_CAV_Cerny.pdf
file_size: 3633276
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: 465 - 479
publication_status: published
publisher: Springer
publist_id: '1066'
pubrep_id: '27'
quality_controlled: '1'
related_material:
record:
- id: '5391'
relation: earlier_version
status: public
status: public
title: Model checking of linearizability of concurrent list implementations
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...
---
_id: '4392'
abstract:
- lang: eng
text: 'While a boolean notion of correctness is given by a preorder on systems and
properties, a quantitative notion of correctness is defined by a distance function
on systems and properties, where the distance between a system and a property
provides a measure of “fit” or “desirability.” In this article, we explore several
ways how the simulation preorder can be generalized to a distance function. This
is done by equipping the classical simulation game between a system and a property
with quantitative objectives. In particular, for systems that satisfy a property,
a quantitative simulation game can measure the “robustness” of the satisfaction,
that is, how much the system can deviate from its nominal behavior while still
satisfying the property. For systems that violate a property, a quantitative simulation
game can measure the “seriousness” of the violation, that is, how much the property
has to be modified so that it is satisfied by the system. These distances can
be computed in polynomial time, since the computation reduces to the value problem
in limit average games with constant weights. Finally, we demonstrate how the
robustness distance can be used to measure how many transmission errors are tolerated
by error correcting codes. '
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- 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: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A. Quantitative Simulation Games. In:
Manna Z, Peled D, eds. Time For Verification: Essays in Memory of Amir Pnueli.
Vol 6200. Essays in Memory of Amir Pnueli. Springer; 2010:42-60. doi:10.1007/978-3-642-13754-9_3'
apa: 'Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2010). Quantitative Simulation
Games. In Z. Manna & D. Peled (Eds.), Time For Verification: Essays in
Memory of Amir Pnueli (Vol. 6200, pp. 42–60). Springer. https://doi.org/10.1007/978-3-642-13754-9_3'
chicago: 'Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Quantitative
Simulation Games.” In Time For Verification: Essays in Memory of Amir Pnueli,
edited by Zohar Manna and Doron Peled, 6200:42–60. Essays in Memory of Amir Pnueli.
Springer, 2010. https://doi.org/10.1007/978-3-642-13754-9_3.'
ieee: 'P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Quantitative Simulation
Games,” in Time For Verification: Essays in Memory of Amir Pnueli, vol.
6200, Z. Manna and D. Peled, Eds. Springer, 2010, pp. 42–60.'
ista: 'Cerny P, Henzinger TA, Radhakrishna A. 2010.Quantitative Simulation Games.
In: Time For Verification: Essays in Memory of Amir Pnueli. LNCS, vol. 6200, 42–60.'
mla: 'Cerny, Pavol, et al. “Quantitative Simulation Games.” Time For Verification:
Essays in Memory of Amir Pnueli, edited by Zohar Manna and Doron Peled, vol.
6200, Springer, 2010, pp. 42–60, doi:10.1007/978-3-642-13754-9_3.'
short: 'P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Z. Manna, D. Peled (Eds.),
Time For Verification: Essays in Memory of Amir Pnueli, Springer, 2010, pp. 42–60.'
date_created: 2018-12-11T12:08:37Z
date_published: 2010-07-29T00:00:00Z
date_updated: 2021-01-12T07:56:38Z
day: '29'
department:
- _id: ToHe
doi: 10.1007/978-3-642-13754-9_3
ec_funded: 1
editor:
- first_name: Zohar
full_name: Manna, Zohar
last_name: Manna
- first_name: Doron
full_name: Peled, Doron
last_name: Peled
intvolume: ' 6200'
language:
- iso: eng
month: '07'
oa_version: None
page: 42 - 60
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: 'Time For Verification: Essays in Memory of Amir Pnueli'
publication_status: published
publisher: Springer
publist_id: '1064'
quality_controlled: '1'
scopus_import: 1
series_title: Essays in Memory of Amir Pnueli
status: public
title: Quantitative Simulation Games
type: book_chapter
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6200
year: '2010'
...
---
_id: '4393'
abstract:
- lang: eng
text: Boolean notions of correctness are formalized by preorders on systems. Quantitative
measures of correctness can be formalized by real-valued distance functions between
systems, where the distance between implementation and specification provides
a measure of “fit” or “desirability.” We extend the simulation preorder to the
quantitative setting, by making each player of a simulation game pay a certain
price for her choices. We use the resulting games with quantitative objectives
to define three different simulation distances. The correctness distance measures
how much the specification must be changed in order to be satisfied by the implementation.
The coverage distance measures how much the implementation restricts the degrees
of freedom offered by the specification. The robustness distance measures how
much a system can deviate from the implementation description without violating
the specification. We consider these distances for safety as well as liveness
specifications. The distances can be computed in polynomial time for safety specifications,
and for liveness specifications given by weak fairness constraints. We show that
the distance functions satisfy the triangle inequality, that the distance between
two systems does not increase under parallel composition with a third system,
and that the distance between two systems can be bounded from above and below
by distances between abstractions of the two systems. These properties suggest
that our simulation distances provide an appropriate basis for a quantitative
theory of discrete systems. We also demonstrate how the robustness distance can
be used to measure how many transmission errors are tolerated by error correcting
codes.
acknowledgement: This work was partially supported by the European Union project COMBEST
and the European Network of Excellence ArtistDesign.
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- 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: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A. Simulation distances. In: Vol 6269.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:235-268. doi:10.1007/978-3-642-15375-4_18'
apa: 'Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2010). Simulation distances
(Vol. 6269, pp. 235–268). Presented at the CONCUR: Concurrency Theory, Paris,
France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-15375-4_18'
chicago: Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances,”
6269:235–68. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. https://doi.org/10.1007/978-3-642-15375-4_18.
ieee: 'P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” presented
at the CONCUR: Concurrency Theory, Paris, France, 2010, vol. 6269, pp. 235–268.'
ista: 'Cerny P, Henzinger TA, Radhakrishna A. 2010. Simulation distances. CONCUR:
Concurrency Theory, LNCS, vol. 6269, 235–268.'
mla: Cerny, Pavol, et al. Simulation Distances. Vol. 6269, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2010, pp. 235–68, doi:10.1007/978-3-642-15375-4_18.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2010, pp. 235–268.
conference:
end_date: 2010-09-03
location: Paris, France
name: 'CONCUR: Concurrency Theory'
start_date: 2010-08-31
date_created: 2018-12-11T12:08:37Z
date_published: 2010-11-01T00:00:00Z
date_updated: 2023-02-23T12:24:04Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-15375-4_18
ec_funded: 1
file:
- access_level: open_access
checksum: ea567903676ba8afe0507ee11313dce5
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:12Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5130'
file_name: IST-2012-42-v1+1_Simulation_distances.pdf
file_size: 198913
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
intvolume: ' 6269'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 235 - 268
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: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '1065'
pubrep_id: '42'
quality_controlled: '1'
related_material:
record:
- id: '3249'
relation: later_version
status: public
- id: '5389'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Simulation distances
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 6269
year: '2010'
...
---
_id: '4396'
abstract:
- lang: eng
text: 'Shape analysis is a promising technique to prove program properties about
recursive data structures. The challenge is to automatically determine the data-structure
type, and to supply the shape analysis with the necessary information about the
data structure. We present a stepwise approach to the selection of instrumentation
predicates for a TVLA-based shape analysis, which takes us a step closer towards
the fully automatic verification of data structures. The approach uses two techniques
to guide the refinement of shape abstractions: (1) during program exploration,
an explicit heap analysis collects sample instances of the heap structures, which
are used to identify the data structures that are manipulated by the program;
and (2) during abstraction refinement along an infeasible error path, we consider
different possible heap abstractions and choose the coarsest one that eliminates
the infeasible path. We have implemented this combined approach for automatic
shape refinement as an extension of the software model checker BLAST. Example
programs from a data-structure library that manipulate doubly-linked lists and
trees were successfully verified by our tool.'
alternative_title:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- 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: Grégory
full_name: Théoduloz, Grégory
last_name: Théoduloz
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Beyer D, Henzinger TA, Théoduloz G, Zufferey D. Shape refinement through explicit
heap analysis. In: Rosenblum D, Taenzer G, eds. Vol 6013. Springer; 2010:263-277.
doi:10.1007/978-3-642-12029-9_19'
apa: 'Beyer, D., Henzinger, T. A., Théoduloz, G., & Zufferey, D. (2010). Shape
refinement through explicit heap analysis. In D. Rosenblum & G. Taenzer (Eds.)
(Vol. 6013, pp. 263–277). Presented at the FASE: Fundamental Approaches To Software
Engineering, Paphos, Cyprus: Springer. https://doi.org/10.1007/978-3-642-12029-9_19'
chicago: Beyer, Dirk, Thomas A Henzinger, Grégory Théoduloz, and Damien Zufferey.
“Shape Refinement through Explicit Heap Analysis.” edited by David Rosenblum and
Gabriele Taenzer, 6013:263–77. Springer, 2010. https://doi.org/10.1007/978-3-642-12029-9_19.
ieee: 'D. Beyer, T. A. Henzinger, G. Théoduloz, and D. Zufferey, “Shape refinement
through explicit heap analysis,” presented at the FASE: Fundamental Approaches
To Software Engineering, Paphos, Cyprus, 2010, vol. 6013, pp. 263–277.'
ista: 'Beyer D, Henzinger TA, Théoduloz G, Zufferey D. 2010. Shape refinement through
explicit heap analysis. FASE: Fundamental Approaches To Software Engineering,
LNCS, vol. 6013, 263–277.'
mla: Beyer, Dirk, et al. Shape Refinement through Explicit Heap Analysis.
Edited by David Rosenblum and Gabriele Taenzer, vol. 6013, Springer, 2010, pp.
263–77, doi:10.1007/978-3-642-12029-9_19.
short: D. Beyer, T.A. Henzinger, G. Théoduloz, D. Zufferey, in:, D. Rosenblum, G.
Taenzer (Eds.), Springer, 2010, pp. 263–277.
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:08:38Z
date_published: 2010-04-21T00:00:00Z
date_updated: 2021-01-12T07:56:40Z
day: '21'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-12029-9_19
editor:
- first_name: David
full_name: Rosenblum, David
last_name: Rosenblum
- first_name: Gabriele
full_name: Taenzer, Gabriele
last_name: Taenzer
file:
- access_level: open_access
checksum: 7d26e59a9681487d7283eba337292b2c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:13Z
date_updated: 2020-07-14T12:46:29Z
file_id: '5332'
file_name: IST-2012-41-v1+1_Shape_refinement_through_explicit_heap_analysis.pdf
file_size: 312147
relation: main_file
file_date_updated: 2020-07-14T12:46:29Z
has_accepted_license: '1'
intvolume: ' 6013'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 263 - 277
project:
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '1061'
pubrep_id: '41'
quality_controlled: '1'
scopus_import: 1
status: public
title: Shape refinement through explicit heap analysis
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6013
year: '2010'
...
---
_id: '5393'
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 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:
- IST Austria Technical Report
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. IST Austria; 2009. doi:10.15479/AT:IST-2009-0003'
apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., & Radhakrishna, A. (2009).
Gist: A solver for probabilistic games. IST Austria. https://doi.org/10.15479/AT:IST-2009-0003'
chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Arjun
Radhakrishna. Gist: A Solver for Probabilistic Games. IST Austria, 2009.
https://doi.org/10.15479/AT:IST-2009-0003.'
ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and A. Radhakrishna, Gist:
A solver for probabilistic games. IST Austria, 2009.'
ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. 2009. Gist: A solver
for probabilistic games, IST Austria, 12p.'
mla: 'Chatterjee, Krishnendu, et al. Gist: A Solver for Probabilistic Games.
IST Austria, 2009, doi:10.15479/AT:IST-2009-0003.'
short: 'K. Chatterjee, T.A. Henzinger, B. Jobstmann, A. Radhakrishna, Gist: A Solver
for Probabilistic Games, IST Austria, 2009.'
date_created: 2018-12-12T11:39:05Z
date_published: 2009-10-09T00:00:00Z
date_updated: 2023-02-23T12:09:01Z
day: '09'
ddc:
- '000'
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2009-0003
file:
- access_level: open_access
checksum: 49551ac552915b17593a14c993845274
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:52:58Z
date_updated: 2020-07-14T12:46:43Z
file_id: '5459'
file_name: IST-2009-0003_IST-2009-0003.pdf
file_size: 386866
relation: main_file
file_date_updated: 2020-07-14T12:46:43Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '12'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '29'
related_material:
record:
- id: '4388'
relation: later_version
status: public
status: public
title: 'Gist: A solver for probabilistic games'
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2009'
...
---
_id: '5394'
abstract:
- lang: eng
text: We consider two-player games played on graphs with request-response and finitary
Streett objectives. We show these games are PSPACE-hard, improving the previous
known NP-hardness. We also improve the lower bounds on memory required by the
winning strategies for the players.
alternative_title:
- IST Austria Technical Report
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: Florian
full_name: Horn, Florian
id: 37327ACE-F248-11E8-B48F-1D18A9856A87
last_name: Horn
citation:
ama: Chatterjee K, Henzinger TA, Horn F. Improved Lower Bounds for Request-Response
and Finitary Streett Games. IST Austria; 2009. doi:10.15479/AT:IST-2009-0002
apa: Chatterjee, K., Henzinger, T. A., & Horn, F. (2009). Improved lower
bounds for request-response and finitary Streett games. IST Austria. https://doi.org/10.15479/AT:IST-2009-0002
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. Improved
Lower Bounds for Request-Response and Finitary Streett Games. IST Austria,
2009. https://doi.org/10.15479/AT:IST-2009-0002.
ieee: K. Chatterjee, T. A. Henzinger, and F. Horn, Improved lower bounds for
request-response and finitary Streett games. IST Austria, 2009.
ista: Chatterjee K, Henzinger TA, Horn F. 2009. Improved lower bounds for request-response
and finitary Streett games, IST Austria, 11p.
mla: Chatterjee, Krishnendu, et al. Improved Lower Bounds for Request-Response
and Finitary Streett Games. IST Austria, 2009, doi:10.15479/AT:IST-2009-0002.
short: K. Chatterjee, T.A. Henzinger, F. Horn, Improved Lower Bounds for Request-Response
and Finitary Streett Games, IST Austria, 2009.
date_created: 2018-12-12T11:39:05Z
date_published: 2009-09-09T00:00:00Z
date_updated: 2020-07-14T23:07:47Z
day: '09'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2009-0002
file:
- access_level: open_access
checksum: 1c50a9723fbae1b2c46d18138968efb3
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:50Z
date_updated: 2020-07-14T12:46:43Z
file_id: '5511'
file_name: IST-2009-0002_IST-2009-0002.pdf
file_size: 238091
relation: main_file
file_date_updated: 2020-07-14T12:46:43Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '11'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '30'
status: public
title: Improved lower bounds for request-response and finitary Streett games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2009'
...