---
_id: '7699'
article_processing_charge: No
article_type: original
author:
- first_name: Lora Beatrice Jaeger
full_name: Sweeney, Lora Beatrice Jaeger
id: 56BE8254-C4F0-11E9-8E45-0B23E6697425
last_name: Sweeney
orcid: 0000-0001-9242-5601
- first_name: Darcy B
full_name: Kelley, Darcy B
last_name: Kelley
citation:
ama: Sweeney LB, Kelley DB. Harnessing vocal patterns for social communication.
Current Opinion in Neurobiology. 2014;28(10):34-41. doi:10.1016/j.conb.2014.06.006
apa: Sweeney, L. B., & Kelley, D. B. (2014). Harnessing vocal patterns for social
communication. Current Opinion in Neurobiology. Elsevier. https://doi.org/10.1016/j.conb.2014.06.006
chicago: Sweeney, Lora B., and Darcy B Kelley. “Harnessing Vocal Patterns for Social
Communication.” Current Opinion in Neurobiology. Elsevier, 2014. https://doi.org/10.1016/j.conb.2014.06.006.
ieee: L. B. Sweeney and D. B. Kelley, “Harnessing vocal patterns for social communication,”
Current Opinion in Neurobiology, vol. 28, no. 10. Elsevier, pp. 34–41,
2014.
ista: Sweeney LB, Kelley DB. 2014. Harnessing vocal patterns for social communication.
Current Opinion in Neurobiology. 28(10), 34–41.
mla: Sweeney, Lora B., and Darcy B. Kelley. “Harnessing Vocal Patterns for Social
Communication.” Current Opinion in Neurobiology, vol. 28, no. 10, Elsevier,
2014, pp. 34–41, doi:10.1016/j.conb.2014.06.006.
short: L.B. Sweeney, D.B. Kelley, Current Opinion in Neurobiology 28 (2014) 34–41.
date_created: 2020-04-30T10:35:39Z
date_published: 2014-10-01T00:00:00Z
date_updated: 2024-01-31T10:14:08Z
day: '01'
doi: 10.1016/j.conb.2014.06.006
extern: '1'
intvolume: ' 28'
issue: '10'
language:
- iso: eng
month: '10'
oa_version: None
page: 34-41
publication: Current Opinion in Neurobiology
publication_identifier:
issn:
- 0959-4388
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: Harnessing vocal patterns for social communication
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 28
year: '2014'
...
---
_id: '770'
abstract:
- lang: eng
text: 'Dynamic memory reclamation is arguably the biggest open problem in concurrent
data structure design: All known solutions induce high overhead, or must be customized
to the specific data structure by the programmer, or both. This paper presents
StackTrack, the first concurrent memory reclamation scheme that can be applied
automatically by a compiler, while maintaining efficiency. StackTrack eliminates
most of the expensive bookkeeping required for memory reclamation by leveraging
the power of hardware transactional memory (HTM) in a new way: it tracks thread
variables dynamically, and in an atomic fashion. This effectively makes all memory
references visible without having threads pay the overhead of writing out this
information. Our empirical results show that this new approach matches or outperforms
prior, non-automated, techniques.'
acknowledgement: "Dan Alistarh - Part of this work was performed while the
\ author was a Postdoctoral\r\nAssociate a MIT CSAIL, supported in part by NSF
grant CCF-1217921,\r\nDoE ASCR grant ER26116/DE-SC0008923, and by grants from the
Oracle\r\nand Intel corporations.\r\nPatrick Eugester - Supported in part by DARPA
grant N11AP20014 and NSF grant CNS-\r\n1117065.\r\nMaurice Herlihy - Supported by
NSF grant 1301924.\r\nNir Shavit - Supported in part by NSF grants CCF-1217921 and
CCF-1301926, DoE\r\nASCR grant ER26116/DE-SC0008923, and by grants from the Oracle
and\r\nIntel corporations."
article_processing_charge: No
author:
- first_name: Dan-Adrian
full_name: Alistarh, Dan-Adrian
id: 4A899BFC-F248-11E8-B48F-1D18A9856A87
last_name: Alistarh
orcid: 0000-0003-3650-940X
- first_name: Patrick
full_name: Eugster, Patrick
last_name: Eugster
- first_name: Maurice
full_name: Herlihy, Maurice
last_name: Herlihy
- first_name: Alexander
full_name: Matveev, Alexander
last_name: Matveev
- first_name: Nir
full_name: Shavit, Nir
last_name: Shavit
citation:
ama: 'Alistarh D-A, Eugster P, Herlihy M, Matveev A, Shavit N. StackTrack: An automated
transactional approach to concurrent memory reclamation. In: ACM; 2014. doi:10.1145/2592798.2592808'
apa: 'Alistarh, D.-A., Eugster, P., Herlihy, M., Matveev, A., & Shavit, N. (2014).
StackTrack: An automated transactional approach to concurrent memory reclamation.
Presented at the EuroSys: European Conference on Computer Systems, ACM. https://doi.org/10.1145/2592798.2592808'
chicago: 'Alistarh, Dan-Adrian, Patrick Eugster, Maurice Herlihy, Alexander Matveev,
and Nir Shavit. “StackTrack: An Automated Transactional Approach to Concurrent
Memory Reclamation.” ACM, 2014. https://doi.org/10.1145/2592798.2592808.'
ieee: 'D.-A. Alistarh, P. Eugster, M. Herlihy, A. Matveev, and N. Shavit, “StackTrack:
An automated transactional approach to concurrent memory reclamation,” presented
at the EuroSys: European Conference on Computer Systems, 2014.'
ista: 'Alistarh D-A, Eugster P, Herlihy M, Matveev A, Shavit N. 2014. StackTrack:
An automated transactional approach to concurrent memory reclamation. EuroSys:
European Conference on Computer Systems.'
mla: 'Alistarh, Dan-Adrian, et al. StackTrack: An Automated Transactional Approach
to Concurrent Memory Reclamation. ACM, 2014, doi:10.1145/2592798.2592808.'
short: D.-A. Alistarh, P. Eugster, M. Herlihy, A. Matveev, N. Shavit, in:, ACM,
2014.
conference:
name: 'EuroSys: European Conference on Computer Systems'
date_created: 2018-12-11T11:48:24Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2023-02-23T13:14:25Z
day: '01'
doi: 10.1145/2592798.2592808
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
publication_status: published
publisher: ACM
publist_id: '6888'
status: public
title: 'StackTrack: An automated transactional approach to concurrent memory reclamation'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '771'
abstract:
- lang: eng
text: 'We consider the following natural problem: n failure-prone servers, communicating
synchronously through message passing, must assign themselves one-to-one to n
distinct items. Existing literature suggests two possible approaches to this problem.
First, model it as an instance of tight renaming in synchronous message-passing
systems; for deterministic solutions, a tight bound of ©(logn) communication rounds
is known. Second, model the scenario as an instance of randomized load-balancing,
for which elegant sub-logarithmic solutions exist. However, careful examination
reveals that known load-balancing schemes do not apply to our scenario, because
they either do not tolerate faults or do not ensure one-to-one allocation. It
is thus natural to ask if sublogarithmic solutions exist for this apparently simple
but intriguing problem. In this paper, we combine the two approaches to provide
a new randomized solution for tight renaming, which terminates in O (log log n)
communication rounds with high probability, against a strong adaptive adversary.
Our solution, called Balls-into-Leaves, combines the deterministic approach with
a new randomized scheme to obtain perfectly balanced allocations. The algorithm
arranges the items as leaves of a tree, and participants repeatedly perform random
choices among the leaves. The algorithm exchanges information in each round to
split the participants into progressively smaller groups whose random choices
do not conflict. We then extend the algorithm to terminate early in O(log log)
rounds w.h.p., where is the actual number of failures. These results imply an
exponential separation between deterministic and randomized algorithms for the
tight renaming problem in message-passing systems.'
acknowledgement: "Dan Alistarh was partially supported by the SNF Post-\r\ndoctoral
Fellows Program, NSF grant CCF-1217921, DoE\r\nASCR grant ER26116/DE-SC0008923,
and by grants from\r\nthe Oracle and Intel corporations.\r\nOksana Denysyuk and
Lu ́ıs Rodrigues were partially supported by Funda ̧c ̃ao para a Ciˆencia e Tecnologia
(FCT) via\r\nthe project PEPITA (PTDC/EEI-SCR/2776/2012) and via\r\nthe INESC-ID
multi-annual funding through the PIDDAC\r\nProgram fund grant, under project PEst-OE/EEI/LA0021/\r\n2013.\r\nNir
Shavit was supported in part by NSF grants CCF-1217921 and CCF-1301926, DoE ASCR
grant ER26116/DE-SC0008923, and by grants from the Oracle and Intel corporations."
article_processing_charge: No
author:
- first_name: Dan-Adrian
full_name: Alistarh, Dan-Adrian
id: 4A899BFC-F248-11E8-B48F-1D18A9856A87
last_name: Alistarh
orcid: 0000-0003-3650-940X
- first_name: Oksana
full_name: Denysyuk, Oksana
last_name: Denysyuk
- first_name: Luís
full_name: Rodrígues, Luís
last_name: Rodrígues
- first_name: Nir
full_name: Shavit, Nir
last_name: Shavit
citation:
ama: 'Alistarh D-A, Denysyuk O, Rodrígues L, Shavit N. Balls-into-Leaves: Sub-logarithmic
renaming in synchronous message-passing systems. In: ACM; 2014:232-241. doi:10.1145/2611462.2611499'
apa: 'Alistarh, D.-A., Denysyuk, O., Rodrígues, L., & Shavit, N. (2014). Balls-into-Leaves:
Sub-logarithmic renaming in synchronous message-passing systems (pp. 232–241).
Presented at the PODC: Principles of Distributed Computing, ACM. https://doi.org/10.1145/2611462.2611499'
chicago: 'Alistarh, Dan-Adrian, Oksana Denysyuk, Luís Rodrígues, and Nir Shavit.
“Balls-into-Leaves: Sub-Logarithmic Renaming in Synchronous Message-Passing Systems,”
232–41. ACM, 2014. https://doi.org/10.1145/2611462.2611499.'
ieee: 'D.-A. Alistarh, O. Denysyuk, L. Rodrígues, and N. Shavit, “Balls-into-Leaves:
Sub-logarithmic renaming in synchronous message-passing systems,” presented at
the PODC: Principles of Distributed Computing, 2014, pp. 232–241.'
ista: 'Alistarh D-A, Denysyuk O, Rodrígues L, Shavit N. 2014. Balls-into-Leaves:
Sub-logarithmic renaming in synchronous message-passing systems. PODC: Principles
of Distributed Computing, 232–241.'
mla: 'Alistarh, Dan-Adrian, et al. Balls-into-Leaves: Sub-Logarithmic Renaming
in Synchronous Message-Passing Systems. ACM, 2014, pp. 232–41, doi:10.1145/2611462.2611499.'
short: D.-A. Alistarh, O. Denysyuk, L. Rodrígues, N. Shavit, in:, ACM, 2014, pp.
232–241.
conference:
name: 'PODC: Principles of Distributed Computing'
date_created: 2018-12-11T11:48:25Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2023-02-23T13:14:49Z
day: '01'
doi: 10.1145/2611462.2611499
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 232 - 241
publication_status: published
publisher: ACM
publist_id: '6884'
status: public
title: 'Balls-into-Leaves: Sub-logarithmic renaming in synchronous message-passing
systems'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '772'
abstract:
- lang: eng
text: Lock-free concurrent algorithms guarantee that some concurrent operation will
always make progress in a finite number of steps. Yet programmers prefer to treat
concurrent code as if it were wait-free, guaranteeing that all operations always
make progress. Unfortunately, designing wait-free algorithms is generally a very
complex task, and the resulting algorithms are not always efficient. While obtaining
efficient wait-free algorithms has been a long-time goal for the theory community,
most non-blocking commercial code is only lock-free. This paper suggests a simple
solution to this problem. We show that, for a large class of lock-free algorithms,
under scheduling conditions which approximate those found in commercial hardware
architectures, lock-free algorithms behave as if they are wait-free. In other
words, programmers can keep on designing simple lock-free algorithms instead of
complex wait-free ones, and in practice, they will get wait-free progress. Our
main contribution is a new way of analyzing a general class of lock-free algorithms
under a stochastic scheduler. Our analysis relates the individual performance
of processes with the global performance of the system using Markov chain lifting
between a complex per-process chain and a simpler system progress chain. We show
that lock-free algorithms are not only wait-free with probability 1, but that
in fact a general subset of lock-free algorithms can be closely bounded in terms
of the average number of steps required until an operation completes. To the best
of our knowledge, this is the first attempt to analyze progress conditions, typically
stated in relation to a worst case adversary, in a stochastic model capturing
their expected asymptotic behavior.
acknowledgement: "Dan Alistarh - Part of this work was performed while the author
was a Postdoctoral Associate at MIT CSAIL, where he was supported by SNF\r\nPostdoctoral
Fellows Program, NSF grant CCF-1217921, DoE\r\nASCR grant ER26116/DE-SC0008923,
and by grants from the Oracle and Intel corporations.\r\nKeron Censor-Hillel - Shalon
Fellow\r\nNir Shavit - This work was supported in part by NSF grants CCF-1217921
and\r\nCCF-1301926, DoE ASCR grant ER26116/DE-SC0008923, and\r\nby grants from the
Oracle and Intel corporations."
article_processing_charge: No
arxiv: 1
author:
- first_name: Dan-Adrian
full_name: Alistarh, Dan-Adrian
id: 4A899BFC-F248-11E8-B48F-1D18A9856A87
last_name: Alistarh
orcid: 0000-0003-3650-940X
- first_name: Keren
full_name: Censor Hillel, Keren
last_name: Censor Hillel
- first_name: Nir
full_name: Shavit, Nir
last_name: Shavit
citation:
ama: 'Alistarh D-A, Censor Hillel K, Shavit N. Are lock-free concurrent algorithms
practically wait-free? In: ACM; 2014:714-723. doi:10.1145/2591796.2591836'
apa: 'Alistarh, D.-A., Censor Hillel, K., & Shavit, N. (2014). Are lock-free
concurrent algorithms practically wait-free? (pp. 714–723). Presented at the STOC:
Symposium on Theory of Computing, ACM. https://doi.org/10.1145/2591796.2591836'
chicago: Alistarh, Dan-Adrian, Keren Censor Hillel, and Nir Shavit. “Are Lock-Free
Concurrent Algorithms Practically Wait-Free?,” 714–23. ACM, 2014. https://doi.org/10.1145/2591796.2591836.
ieee: 'D.-A. Alistarh, K. Censor Hillel, and N. Shavit, “Are lock-free concurrent
algorithms practically wait-free?,” presented at the STOC: Symposium on Theory
of Computing, 2014, pp. 714–723.'
ista: 'Alistarh D-A, Censor Hillel K, Shavit N. 2014. Are lock-free concurrent algorithms
practically wait-free? STOC: Symposium on Theory of Computing, 714–723.'
mla: Alistarh, Dan-Adrian, et al. Are Lock-Free Concurrent Algorithms Practically
Wait-Free? ACM, 2014, pp. 714–23, doi:10.1145/2591796.2591836.
short: D.-A. Alistarh, K. Censor Hillel, N. Shavit, in:, ACM, 2014, pp. 714–723.
conference:
name: 'STOC: Symposium on Theory of Computing'
date_created: 2018-12-11T11:48:25Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2023-02-23T13:15:13Z
day: '01'
doi: 10.1145/2591796.2591836
extern: '1'
external_id:
arxiv:
- '1311.3200'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1311.3200
month: '01'
oa: 1
oa_version: Preprint
page: 714 - 723
publication_status: published
publisher: ACM
publist_id: '6885'
status: public
title: Are lock-free concurrent algorithms practically wait-free?
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '773'
abstract:
- lang: eng
text: "We describe a new randomized consensus protocol with expected message complexity
O(n2log2n) when fewer than n/2 processes may fail by crashing. This is an almost-linear
improvement over the best previously known protocol, and within logarithmic factors
of a known Ω(n2) message lower bound. The protocol further ensures that no process
sends more than O(n log3n) messages in expectation, which is again within logarithmic
factors of optimal.We also present a generalization of the algorithm to an arbitrary
number of failures t, which uses expected O(nt + t2log2t) total messages. Our
protocol uses messages of size O(log n), and can therefore scale to large networks.\r\n\r\nWe
consider the problem of consensus in the challenging classic model. In this model,
the adversary is adaptive; it can choose which processors crash at any point during
the course of the algorithm. Further, communication is via asynchronous message
passing: there is no known upper bound on the time to send a message from one
processor to another, and all messages and coin flips are seen by the adversary.\r\n\r\nOur
approach is to build a message-efficient, resilient mechanism for aggregating
individual processor votes, implementing the message-passing equivalent of a weak
shared coin. Roughly, in our protocol, a processor first announces its votes to
small groups, then propagates them to increasingly larger groups as it generates
more and more votes. To bound the number of messages that an individual process
might have to send or receive, the protocol progressively increases the weight
of generated votes. The main technical challenge is bounding the impact of votes
that are still “in flight” (generated, but not fully propagated) on the final
outcome of the shared coin, especially since such votes might have different weights.
We achieve this by leveraging the structure of the algorithm, and a technical
argument based on martingale concentration bounds. Overall, we show that it is
possible to build an efficient message-passing implementation of a shared coin,
and in the process (almost-optimally) solve the classic consensus problem in the
asynchronous message-passing model."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Dan-Adrian
full_name: Alistarh, Dan-Adrian
id: 4A899BFC-F248-11E8-B48F-1D18A9856A87
last_name: Alistarh
orcid: 0000-0003-3650-940X
- first_name: James
full_name: Aspnes, James
last_name: Aspnes
- first_name: Valerie
full_name: King, Valerie
last_name: King
- first_name: Jared
full_name: Saia, Jared
last_name: Saia
citation:
ama: 'Alistarh D-A, Aspnes J, King V, Saia J. Communication-efficient randomized
consensus. In: Kuhn F, ed. Vol 8784. Springer; 2014:61-75. doi:10.1007/978-3-662-45174-8_5'
apa: 'Alistarh, D.-A., Aspnes, J., King, V., & Saia, J. (2014). Communication-efficient
randomized consensus. In F. Kuhn (Ed.) (Vol. 8784, pp. 61–75). Presented at the
DISC: Distributed Computing, Austin, USA: Springer. https://doi.org/10.1007/978-3-662-45174-8_5'
chicago: Alistarh, Dan-Adrian, James Aspnes, Valerie King, and Jared Saia. “Communication-Efficient
Randomized Consensus.” edited by Fabian Kuhn, 8784:61–75. Springer, 2014. https://doi.org/10.1007/978-3-662-45174-8_5.
ieee: 'D.-A. Alistarh, J. Aspnes, V. King, and J. Saia, “Communication-efficient
randomized consensus,” presented at the DISC: Distributed Computing, Austin, USA,
2014, vol. 8784, pp. 61–75.'
ista: 'Alistarh D-A, Aspnes J, King V, Saia J. 2014. Communication-efficient randomized
consensus. DISC: Distributed Computing, LNCS, vol. 8784, 61–75.'
mla: Alistarh, Dan-Adrian, et al. Communication-Efficient Randomized Consensus.
Edited by Fabian Kuhn, vol. 8784, Springer, 2014, pp. 61–75, doi:10.1007/978-3-662-45174-8_5.
short: D.-A. Alistarh, J. Aspnes, V. King, J. Saia, in:, F. Kuhn (Ed.), Springer,
2014, pp. 61–75.
conference:
end_date: 2014-10-15
location: Austin, USA
name: 'DISC: Distributed Computing'
start_date: 2014-10-12
date_created: 2018-12-11T11:48:25Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2023-02-23T13:15:36Z
day: '01'
doi: 10.1007/978-3-662-45174-8_5
editor:
- first_name: Fabian
full_name: Kuhn, Fabian
last_name: Kuhn
extern: '1'
intvolume: ' 8784'
language:
- iso: eng
month: '01'
oa_version: None
page: 61 - 75
publication_status: published
publisher: Springer
publist_id: '6881'
status: public
title: Communication-efficient randomized consensus
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8784
year: '2014'
...
---
_id: '774'
abstract:
- lang: eng
text: Lock-free concurrent algorithms guarantee that some concurrent operation will
always make progress in a finite number of steps. Yet programmers would prefer
to treat concurrent code as if it were wait-free, guaranteeing that all operations
always make progress. Unfortunately, designing wait-free algorithms is in general
a complex undertaking, and the resulting algorithms are not always efficient,
so most non-blocking commercial code is only lock-free, and the design of efficient
wait-free algorithms has been left to the academic community. In [2], we suggest
a solution to this problem. We show that, for a large class of lock-free algorithms,
under scheduling conditions which approximate those found in commercial hardware
architectures, lock-free algorithms behave as if they are wait-free. In other
words, programmers can keep on designing simple lock-free algorithms instead of
complex wait-free ones, and in practice, they will get wait-free progress. Our
main contribution is a new way of analyzing a general class of lock-free algorithms
under a stochastic scheduler. Our analysis relates the individual performance
of processes with the global performance of the system using Markov chain lifting
between a complex per-process chain and a simpler system progress chain. We show
that lock-free algorithms are not only wait-free with probability 1, but that
in fact a broad subset of lock-free algorithms can be closely bounded in terms
of the average number of steps required until an operation completes.
acknowledgement: "Dan Alistarh - Part of this work was performed while the
\ author was a\r\nPostdoctoral Associate at MIT CSAIL, where he was supported
\ by SNF Postdoctoral Fellows Program, NSF grant\r\nCCF-1217921, DoE ASCR
grant ER26116/DE-SC0008923,\r\nand by grants from the Oracle and Intel corporations.\r\nKeren
Censor-Hille - Shalon Fellow\r\nNir Shavit - This work was supported in part
\ by NSF grants CCF-1217921 and CCF-1301926, DoE ASCR grant ER26116/DE-\r\nSC0008923,
and by grants from the Oracle and Intel corporations."
article_processing_charge: No
author:
- first_name: Dan-Adrian
full_name: Alistarh, Dan-Adrian
id: 4A899BFC-F248-11E8-B48F-1D18A9856A87
last_name: Alistarh
orcid: 0000-0003-3650-940X
- first_name: Keren
full_name: Censor Hille, Keren
last_name: Censor Hille
- first_name: Nir
full_name: Shavit, Nir
last_name: Shavit
citation:
ama: 'Alistarh D-A, Censor Hille K, Shavit N. Brief announcement: Are lock-free
concurrent algorithms practically wait-free? In: ACM; 2014:50-52. doi:10.1145/2611462.2611502'
apa: 'Alistarh, D.-A., Censor Hille, K., & Shavit, N. (2014). Brief announcement:
Are lock-free concurrent algorithms practically wait-free? (pp. 50–52). Presented
at the PODC: Principles of Distributed Computing, ACM. https://doi.org/10.1145/2611462.2611502'
chicago: 'Alistarh, Dan-Adrian, Keren Censor Hille, and Nir Shavit. “Brief Announcement:
Are Lock-Free Concurrent Algorithms Practically Wait-Free?,” 50–52. ACM, 2014.
https://doi.org/10.1145/2611462.2611502.'
ieee: 'D.-A. Alistarh, K. Censor Hille, and N. Shavit, “Brief announcement: Are
lock-free concurrent algorithms practically wait-free?,” presented at the PODC:
Principles of Distributed Computing, 2014, pp. 50–52.'
ista: 'Alistarh D-A, Censor Hille K, Shavit N. 2014. Brief announcement: Are lock-free
concurrent algorithms practically wait-free? PODC: Principles of Distributed Computing,
50–52.'
mla: 'Alistarh, Dan-Adrian, et al. Brief Announcement: Are Lock-Free Concurrent
Algorithms Practically Wait-Free? ACM, 2014, pp. 50–52, doi:10.1145/2611462.2611502.'
short: D.-A. Alistarh, K. Censor Hille, N. Shavit, in:, ACM, 2014, pp. 50–52.
conference:
name: 'PODC: Principles of Distributed Computing'
date_created: 2018-12-11T11:48:26Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2023-02-23T13:15:54Z
day: '01'
doi: 10.1145/2611462.2611502
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 50 - 52
publication_status: published
publisher: ACM
publist_id: '6882'
status: public
title: 'Brief announcement: Are lock-free concurrent algorithms practically wait-free?'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '7743'
abstract:
- lang: eng
text: Experimental studies have demonstrated that environmental variation can create
genotype‐environment interactions (GEIs) in the traits involved in sexual selection.
Understanding the genetic architecture of phenotype across environments will require
statistical tests that can describe both changes in genetic variance and covariance
across environments. This chapter outlines the theoretical framework for the processes
of sexual selection in the wild, identifying key parameters in wild systems, and
highlighting the potential effects of the environment. It describes the proposed
approaches for the estimation of these key parameters in a quantitative genetic
framework within naturally occurring pedigreed populations. The chapter provides
a worked example for a range of analysis methods. It aims to provide an overview
of the analytical methods that can be used to model GEIs for traits involved in
sexual selection in naturally occurring pedigreed populations.
article_processing_charge: No
author:
- first_name: Matthew Richard
full_name: Robinson, Matthew Richard
id: E5D42276-F5DA-11E9-8E24-6303E6697425
last_name: Robinson
orcid: 0000-0001-8982-8813
- first_name: Anna
full_name: Qvarnström, Anna
last_name: Qvarnström
citation:
ama: 'Robinson MR, Qvarnström A. Influence of the environment on the genetic architecture
of traits involved in sexual selection within wild populations. In: Hunt J, Hosken
D, eds. Genotype-by-Environment Interactions and Sexual Selection. Chichester,
UK: Wiley; 2014:137-168. doi:10.1002/9781118912591.ch6'
apa: 'Robinson, M. R., & Qvarnström, A. (2014). Influence of the environment
on the genetic architecture of traits involved in sexual selection within wild
populations. In J. Hunt & D. Hosken (Eds.), Genotype-by-Environment Interactions
and Sexual Selection (pp. 137–168). Chichester, UK: Wiley. https://doi.org/10.1002/9781118912591.ch6'
chicago: 'Robinson, Matthew Richard, and Anna Qvarnström. “Influence of the Environment
on the Genetic Architecture of Traits Involved in Sexual Selection within Wild
Populations.” In Genotype-by-Environment Interactions and Sexual Selection,
edited by John Hunt and David Hosken, 137–68. Chichester, UK: Wiley, 2014. https://doi.org/10.1002/9781118912591.ch6.'
ieee: 'M. R. Robinson and A. Qvarnström, “Influence of the environment on the genetic
architecture of traits involved in sexual selection within wild populations,”
in Genotype-by-Environment Interactions and Sexual Selection, J. Hunt and
D. Hosken, Eds. Chichester, UK: Wiley, 2014, pp. 137–168.'
ista: 'Robinson MR, Qvarnström A. 2014.Influence of the environment on the genetic
architecture of traits involved in sexual selection within wild populations. In:
Genotype-by-Environment Interactions and Sexual Selection. , 137–168.'
mla: Robinson, Matthew Richard, and Anna Qvarnström. “Influence of the Environment
on the Genetic Architecture of Traits Involved in Sexual Selection within Wild
Populations.” Genotype-by-Environment Interactions and Sexual Selection,
edited by John Hunt and David Hosken, Wiley, 2014, pp. 137–68, doi:10.1002/9781118912591.ch6.
short: M.R. Robinson, A. Qvarnström, in:, J. Hunt, D. Hosken (Eds.), Genotype-by-Environment
Interactions and Sexual Selection, Wiley, Chichester, UK, 2014, pp. 137–168.
date_created: 2020-04-30T10:58:39Z
date_published: 2014-08-29T00:00:00Z
date_updated: 2021-01-12T08:15:13Z
day: '29'
doi: 10.1002/9781118912591.ch6
editor:
- first_name: John
full_name: Hunt, John
last_name: Hunt
- first_name: David
full_name: Hosken, David
last_name: Hosken
extern: '1'
language:
- iso: eng
month: '08'
oa_version: None
page: 137-168
place: Chichester, UK
publication: Genotype-by-Environment Interactions and Sexual Selection
publication_identifier:
eisbn:
- '9781118912591'
isbn:
- '9780470671795'
publication_status: published
publisher: Wiley
quality_controlled: '1'
status: public
title: Influence of the environment on the genetic architecture of traits involved
in sexual selection within wild populations
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '7744'
article_processing_charge: No
article_type: original
author:
- first_name: Matthew Richard
full_name: Robinson, Matthew Richard
id: E5D42276-F5DA-11E9-8E24-6303E6697425
last_name: Robinson
orcid: 0000-0001-8982-8813
- first_name: Naomi R.
full_name: Wray, Naomi R.
last_name: Wray
- first_name: Peter M.
full_name: Visscher, Peter M.
last_name: Visscher
citation:
ama: Robinson MR, Wray NR, Visscher PM. Explaining additional genetic variation
in complex traits. Trends in Genetics. 2014;30(4):124-132. doi:10.1016/j.tig.2014.02.003
apa: Robinson, M. R., Wray, N. R., & Visscher, P. M. (2014). Explaining additional
genetic variation in complex traits. Trends in Genetics. Elsevier. https://doi.org/10.1016/j.tig.2014.02.003
chicago: Robinson, Matthew Richard, Naomi R. Wray, and Peter M. Visscher. “Explaining
Additional Genetic Variation in Complex Traits.” Trends in Genetics. Elsevier,
2014. https://doi.org/10.1016/j.tig.2014.02.003.
ieee: M. R. Robinson, N. R. Wray, and P. M. Visscher, “Explaining additional genetic
variation in complex traits,” Trends in Genetics, vol. 30, no. 4. Elsevier,
pp. 124–132, 2014.
ista: Robinson MR, Wray NR, Visscher PM. 2014. Explaining additional genetic variation
in complex traits. Trends in Genetics. 30(4), 124–132.
mla: Robinson, Matthew Richard, et al. “Explaining Additional Genetic Variation
in Complex Traits.” Trends in Genetics, vol. 30, no. 4, Elsevier, 2014,
pp. 124–32, doi:10.1016/j.tig.2014.02.003.
short: M.R. Robinson, N.R. Wray, P.M. Visscher, Trends in Genetics 30 (2014) 124–132.
date_created: 2020-04-30T10:58:58Z
date_published: 2014-04-01T00:00:00Z
date_updated: 2021-01-12T08:15:14Z
day: '01'
doi: 10.1016/j.tig.2014.02.003
extern: '1'
intvolume: ' 30'
issue: '4'
language:
- iso: eng
month: '04'
oa_version: None
page: 124-132
publication: Trends in Genetics
publication_identifier:
issn:
- 0168-9525
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: Explaining additional genetic variation in complex traits
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 30
year: '2014'
...
---
_id: '775'
abstract:
- lang: eng
text: 'The long-lived renaming problem appears in shared-memory systems where a
set of threads need to register and deregister frequently from the computation,
while concurrent operations scan the set of currently registered threads. Instances
of this problem show up in concurrent implementations of transactional memory,
flat combining, thread barriers, and memory reclamation schemes for lock-free
data structures. In this paper, we analyze a randomized solution for long-lived
renaming. The algorithmic technique we consider, called the Level Array, has previously
been used for hashing and one-shot (single-use) renaming. Our main contribution
is to prove that, in long-lived executions, where processes may register and deregister
polynomially many times, the technique guarantees constant steps on average and
O (log log n) steps with high probability for registering, unit cost for deregistering,
and O (n) steps for collect queries, where n is an upper bound on the number of
processes that may be active at any point in time. We also show that the algorithm
has the surprising property that it is self-healing: under reasonable assumptions
on the schedule, operations running while the data structure is in a degraded
state implicitly help the data structure re-balance itself. This subtle mechanism
obviates the need for expensive periodic rebuilding procedures. Our benchmarks
validate this approach, showing that, for typical use parameters, the average
number of steps a process takes to register is less than two and the worst-case
number of steps is bounded by six, even in executions with billions of operations.
We contrast this with other randomized implementations, whose worst-case behavior
we show to be unreliable, and with deterministic implementations, whose cost is
linear in n.'
article_processing_charge: No
arxiv: 1
author:
- first_name: Dan-Adrian
full_name: Alistarh, Dan-Adrian
id: 4A899BFC-F248-11E8-B48F-1D18A9856A87
last_name: Alistarh
orcid: 0000-0003-3650-940X
- first_name: Justin
full_name: Kopinsky, Justin
last_name: Kopinsky
- first_name: Alexander
full_name: Matveev, Alexander
last_name: Matveev
- first_name: Nir
full_name: Shavit, Nir
last_name: Shavit
citation:
ama: 'Alistarh D-A, Kopinsky J, Matveev A, Shavit N. The levelarray: A fast, practical
long-lived renaming algorithm. In: IEEE; 2014:348-357. doi:10.1109/ICDCS.2014.43'
apa: 'Alistarh, D.-A., Kopinsky, J., Matveev, A., & Shavit, N. (2014). The levelarray:
A fast, practical long-lived renaming algorithm (pp. 348–357). Presented at the
ICDCS: International Conference on Distributed Computing Systems, IEEE. https://doi.org/10.1109/ICDCS.2014.43'
chicago: 'Alistarh, Dan-Adrian, Justin Kopinsky, Alexander Matveev, and Nir Shavit.
“The Levelarray: A Fast, Practical Long-Lived Renaming Algorithm,” 348–57. IEEE,
2014. https://doi.org/10.1109/ICDCS.2014.43.'
ieee: 'D.-A. Alistarh, J. Kopinsky, A. Matveev, and N. Shavit, “The levelarray:
A fast, practical long-lived renaming algorithm,” presented at the ICDCS: International
Conference on Distributed Computing Systems, 2014, pp. 348–357.'
ista: 'Alistarh D-A, Kopinsky J, Matveev A, Shavit N. 2014. The levelarray: A fast,
practical long-lived renaming algorithm. ICDCS: International Conference on Distributed
Computing Systems, 348–357.'
mla: 'Alistarh, Dan-Adrian, et al. The Levelarray: A Fast, Practical Long-Lived
Renaming Algorithm. IEEE, 2014, pp. 348–57, doi:10.1109/ICDCS.2014.43.'
short: D.-A. Alistarh, J. Kopinsky, A. Matveev, N. Shavit, in:, IEEE, 2014, pp.
348–357.
conference:
name: 'ICDCS: International Conference on Distributed Computing Systems'
date_created: 2018-12-11T11:48:26Z
date_published: 2014-08-29T00:00:00Z
date_updated: 2023-02-23T13:16:18Z
day: '29'
doi: 10.1109/ICDCS.2014.43
extern: '1'
external_id:
arxiv:
- '1405.5461'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1405.5461
month: '08'
oa: 1
oa_version: Preprint
page: 348 - 357
publication_status: published
publisher: IEEE
publist_id: '6883'
status: public
title: 'The levelarray: A fast, practical long-lived renaming algorithm'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '468'
abstract:
- lang: eng
text: Invasive alien parasites and pathogens are a growing threat to biodiversity
worldwide, which can contribute to the extinction of endemic species. On the Galápagos
Islands, the invasive parasitic fly Philornis downsi poses a major threat to the
endemic avifauna. Here, we investigated the influence of this parasite on the
breeding success of two Darwin's finch species, the warbler finch (Certhidea olivacea)
and the sympatric small tree finch (Camarhynchus parvulus), on Santa Cruz Island
in 2010 and 2012. While the population of the small tree finch appeared to be
stable, the warbler finch has experienced a dramatic decline in population size
on Santa Cruz Island since 1997. We aimed to identify whether warbler finches
are particularly vulnerable during different stages of the breeding cycle. Contrary
to our prediction, breeding success was lower in the small tree finch than in
the warbler finch. In both species P. downsi had a strong negative impact on breeding
success and our data suggest that heavy rain events also lowered the fledging
success. On the one hand parents might be less efficient in compensating their
chicks' energy loss due to parasitism as they might be less efficient in foraging
on days of heavy rain. On the other hand, intense rainfalls might lead to increased
humidity and more rapid cooling of the nests. In the case of the warbler finch
we found that the control of invasive plant species with herbicides had a significant
additive negative impact on the breeding success. It is very likely that the availability
of insects (i.e. food abundance) is lower in such controlled areas, as herbicide
usage led to the removal of the entire understory. Predation seems to be a minor
factor in brood loss.
acknowledgement: The study was funded by the University of Vienna (Focus of Excellence
grant), the Galápagos Conservation Trust, and the Ethologische Gesellschaft e.V.
article_number: '0107518'
author:
- first_name: Arno
full_name: Cimadom, Arno
last_name: Cimadom
- first_name: Angel
full_name: Ulloa, Angel
last_name: Ulloa
- first_name: Patrick
full_name: Meidl, Patrick
id: 4709BCE6-F248-11E8-B48F-1D18A9856A87
last_name: Meidl
- first_name: Markus
full_name: Zöttl, Markus
last_name: Zöttl
- first_name: Elisabet
full_name: Zöttl, Elisabet
last_name: Zöttl
- first_name: Birgit
full_name: Fessl, Birgit
last_name: Fessl
- first_name: Erwin
full_name: Nemeth, Erwin
last_name: Nemeth
- first_name: Michael
full_name: Dvorak, Michael
last_name: Dvorak
- first_name: Francesca
full_name: Cunninghame, Francesca
last_name: Cunninghame
- first_name: Sabine
full_name: Tebbich, Sabine
last_name: Tebbich
citation:
ama: Cimadom A, Ulloa A, Meidl P, et al. Invasive parasites habitat change and heavy
rainfall reduce breeding success in Darwin’s finches. PLoS One. 2014;9(9).
doi:10.1371/journal.pone.0107518
apa: Cimadom, A., Ulloa, A., Meidl, P., Zöttl, M., Zöttl, E., Fessl, B., … Tebbich,
S. (2014). Invasive parasites habitat change and heavy rainfall reduce breeding
success in Darwin’s finches. PLoS One. Public Library of Science. https://doi.org/10.1371/journal.pone.0107518
chicago: Cimadom, Arno, Angel Ulloa, Patrick Meidl, Markus Zöttl, Elisabet Zöttl,
Birgit Fessl, Erwin Nemeth, Michael Dvorak, Francesca Cunninghame, and Sabine
Tebbich. “Invasive Parasites Habitat Change and Heavy Rainfall Reduce Breeding
Success in Darwin’s Finches.” PLoS One. Public Library of Science, 2014.
https://doi.org/10.1371/journal.pone.0107518.
ieee: A. Cimadom et al., “Invasive parasites habitat change and heavy rainfall
reduce breeding success in Darwin’s finches,” PLoS One, vol. 9, no. 9.
Public Library of Science, 2014.
ista: Cimadom A, Ulloa A, Meidl P, Zöttl M, Zöttl E, Fessl B, Nemeth E, Dvorak M,
Cunninghame F, Tebbich S. 2014. Invasive parasites habitat change and heavy rainfall
reduce breeding success in Darwin’s finches. PLoS One. 9(9), 0107518.
mla: Cimadom, Arno, et al. “Invasive Parasites Habitat Change and Heavy Rainfall
Reduce Breeding Success in Darwin’s Finches.” PLoS One, vol. 9, no. 9,
0107518, Public Library of Science, 2014, doi:10.1371/journal.pone.0107518.
short: A. Cimadom, A. Ulloa, P. Meidl, M. Zöttl, E. Zöttl, B. Fessl, E. Nemeth,
M. Dvorak, F. Cunninghame, S. Tebbich, PLoS One 9 (2014).
date_created: 2018-12-11T11:46:38Z
date_published: 2014-09-23T00:00:00Z
date_updated: 2021-01-12T08:00:48Z
day: '23'
ddc:
- '576'
department:
- _id: CampIT
doi: 10.1371/journal.pone.0107518
file:
- access_level: open_access
checksum: b24e7518ccd41effed0d7d9e2498f67f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:48Z
date_updated: 2020-07-14T12:46:34Z
file_id: '5103'
file_name: IST-2018-954-v1+1_2014_Meidl_Invasive_parasites.PDF
file_size: 489387
relation: main_file
file_date_updated: 2020-07-14T12:46:34Z
has_accepted_license: '1'
intvolume: ' 9'
issue: '9'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '09'
oa: 1
oa_version: Published Version
publication: PLoS One
publication_status: published
publisher: Public Library of Science
publist_id: '7352'
pubrep_id: '954'
quality_controlled: '1'
scopus_import: 1
status: public
title: Invasive parasites habitat change and heavy rainfall reduce breeding success
in Darwin's finches
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: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 9
year: '2014'
...
---
_id: '475'
abstract:
- lang: eng
text: 'First cycle games (FCG) are played on a finite graph by two players who push
a token along the edges until a vertex is repeated, and a simple cycle is formed.
The winner is determined by some fixed property Y of the sequence of labels of
the edges (or nodes) forming this cycle. These games are traditionally of interest
because of their connection with infinite-duration games such as parity and mean-payoff
games. We study the memory requirements for winning strategies of FCGs and certain
associated infinite duration games. We exhibit a simple FCG that is not memoryless
determined (this corrects a mistake in Memoryless determinacy of parity and mean
payoff games: a simple proof by Bj⋯orklund, Sandberg, Vorobyov (2004) that claims
that FCGs for which Y is closed under cyclic permutations are memoryless determined).
We show that θ (n)! memory (where n is the number of nodes in the graph), which
is always sufficient, may be necessary to win some FCGs. On the other hand, we
identify easy to check conditions on Y (i.e., Y is closed under cyclic permutations,
and both Y and its complement are closed under concatenation) that are sufficient
to ensure that the corresponding FCGs and their associated infinite duration games
are memoryless determined. We demonstrate that many games considered in the literature,
such as mean-payoff, parity, energy, etc., satisfy these conditions. On the complexity
side, we show (for efficiently computable Y) that while solving FCGs is in PSPACE,
solving some families of FCGs is PSPACE-hard. '
alternative_title:
- EPTCS
author:
- first_name: Benjamin
full_name: Aminof, Benjamin
id: 4A55BD00-F248-11E8-B48F-1D18A9856A87
last_name: Aminof
- first_name: Sasha
full_name: Rubin, Sasha
id: 2EC51194-F248-11E8-B48F-1D18A9856A87
last_name: Rubin
citation:
ama: 'Aminof B, Rubin S. First cycle games. In: Electronic Proceedings in Theoretical
Computer Science, EPTCS. Vol 146. Open Publishing Association; 2014:83-90.
doi:10.4204/EPTCS.146.11'
apa: 'Aminof, B., & Rubin, S. (2014). First cycle games. In Electronic Proceedings
in Theoretical Computer Science, EPTCS (Vol. 146, pp. 83–90). Grenoble, France:
Open Publishing Association. https://doi.org/10.4204/EPTCS.146.11'
chicago: Aminof, Benjamin, and Sasha Rubin. “First Cycle Games.” In Electronic
Proceedings in Theoretical Computer Science, EPTCS, 146:83–90. Open Publishing
Association, 2014. https://doi.org/10.4204/EPTCS.146.11.
ieee: B. Aminof and S. Rubin, “First cycle games,” in Electronic Proceedings
in Theoretical Computer Science, EPTCS, Grenoble, France, 2014, vol. 146,
pp. 83–90.
ista: 'Aminof B, Rubin S. 2014. First cycle games. Electronic Proceedings in Theoretical
Computer Science, EPTCS. SR: Strategic Reasoning, EPTCS, vol. 146, 83–90.'
mla: Aminof, Benjamin, and Sasha Rubin. “First Cycle Games.” Electronic Proceedings
in Theoretical Computer Science, EPTCS, vol. 146, Open Publishing Association,
2014, pp. 83–90, doi:10.4204/EPTCS.146.11.
short: B. Aminof, S. Rubin, in:, Electronic Proceedings in Theoretical Computer
Science, EPTCS, Open Publishing Association, 2014, pp. 83–90.
conference:
end_date: 2014-04-06
location: Grenoble, France
name: 'SR: Strategic Reasoning'
start_date: 2014-04-05
date_created: 2018-12-11T11:46:41Z
date_published: 2014-04-01T00:00:00Z
date_updated: 2021-01-12T08:00:53Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4204/EPTCS.146.11
ec_funded: 1
file:
- access_level: open_access
checksum: 4d7b4ab82980cca2b96ac7703992a8c8
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:08Z
date_updated: 2020-07-14T12:46:35Z
file_id: '5260'
file_name: IST-2018-952-v1+1_2014_Rubin_First_cycle.pdf
file_size: 100115
relation: main_file
file_date_updated: 2020-07-14T12:46:35Z
has_accepted_license: '1'
intvolume: ' 146'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 83 - 90
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Electronic Proceedings in Theoretical Computer Science, EPTCS
publication_status: published
publisher: Open Publishing Association
publist_id: '7345'
pubrep_id: '952'
quality_controlled: '1'
scopus_import: 1
status: public
title: First cycle games
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: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 146
year: '2014'
...
---
_id: '535'
abstract:
- lang: eng
text: Energy games belong to a class of turn-based two-player infinite-duration
games played on a weighted directed graph. It is one of the rare and intriguing
combinatorial problems that lie in NP∩co-NP, but are not known to be in P. The
existence of polynomial-time algorithms has been a major open problem for decades
and apart from pseudopolynomial algorithms there is no algorithm that solves any
non-trivial subclass in polynomial time. In this paper, we give several results
based on the weight structures of the graph. First, we identify a notion of penalty
and present a polynomial-time algorithm when the penalty is large. Our algorithm
is the first polynomial-time algorithm on a large class of weighted graphs. It
includes several worst-case instances on which previous algorithms, such as value
iteration and random facet algorithms, require at least sub-exponential time.
Our main technique is developing the first non-trivial approximation algorithm
and showing how to convert it to an exact algorithm. Moreover, we show that in
a practical case in verification where weights are clustered around a constant
number of values, the energy game problem can be solved in polynomial time. We
also show that the problem is still as hard as in general when the clique-width
is bounded or the graph is strongly ergodic, suggesting that restricting the graph
structure does not necessarily help.
article_processing_charge: No
article_type: original
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: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Sebastian
full_name: Krinninger, Sebastian
last_name: Krinninger
- first_name: Danupon
full_name: Nanongkai, Danupon
last_name: Nanongkai
citation:
ama: Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms
for energy games with special weight structures. Algorithmica. 2014;70(3):457-492.
doi:10.1007/s00453-013-9843-7
apa: Chatterjee, K., Henzinger, M. H., Krinninger, S., & Nanongkai, D. (2014).
Polynomial-time algorithms for energy games with special weight structures. Algorithmica.
Springer. https://doi.org/10.1007/s00453-013-9843-7
chicago: Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon
Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.”
Algorithmica. Springer, 2014. https://doi.org/10.1007/s00453-013-9843-7.
ieee: K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time
algorithms for energy games with special weight structures,” Algorithmica,
vol. 70, no. 3. Springer, pp. 457–492, 2014.
ista: Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2014. Polynomial-time
algorithms for energy games with special weight structures. Algorithmica. 70(3),
457–492.
mla: Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games
with Special Weight Structures.” Algorithmica, vol. 70, no. 3, Springer,
2014, pp. 457–92, doi:10.1007/s00453-013-9843-7.
short: K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, Algorithmica
70 (2014) 457–492.
date_created: 2018-12-11T11:47:01Z
date_published: 2014-11-01T00:00:00Z
date_updated: 2023-09-05T14:09:29Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/s00453-013-9843-7
ec_funded: 1
external_id:
arxiv:
- '1604.08234'
intvolume: ' 70'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.08234
month: '11'
oa: 1
oa_version: Preprint
page: 457 - 492
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Algorithmica
publication_status: published
publisher: Springer
publist_id: '7282'
quality_controlled: '1'
related_material:
record:
- id: '10905'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Polynomial-time algorithms for energy games with special weight structures
type: journal_article
user_id: 72615eeb-f1f3-11ec-aa25-d4573ddc34fd
volume: 70
year: '2014'
...
---
_id: '537'
abstract:
- lang: eng
text: Transgenerational effects are broader than only parental relationships. Despite
mounting evidence that multigenerational effects alter phenotypic and life-history
traits, our understanding of how they combine to determine fitness is not well
developed because of the added complexity necessary to study them. Here, we derive
a quantitative genetic model of adaptation to an extraordinary new environment
by an additive genetic component, phenotypic plasticity, maternal and grandmaternal
effects. We show how, at equilibrium, negative maternal and negative grandmaternal
effects maximize expected population mean fitness. We define negative transgenerational
effects as those that have a negative effect on trait expression in the subsequent
generation, that is, they slow, or potentially reverse, the expected evolutionary
dynamic. When maternal effects are positive, negative grandmaternal effects are
preferred. As expected under Mendelian inheritance, the grandmaternal effects
have a lower impact on fitness than the maternal effects, but this dual inheritance
model predicts a more complex relationship between maternal and grandmaternal
effects to constrain phenotypic variance and so maximize expected population mean
fitness in the offspring.
author:
- first_name: Roshan
full_name: Prizak, Roshan
id: 4456104E-F248-11E8-B48F-1D18A9856A87
last_name: Prizak
- first_name: Thomas
full_name: Ezard, Thomas
last_name: Ezard
- first_name: Rebecca
full_name: Hoyle, Rebecca
last_name: Hoyle
citation:
ama: Prizak R, Ezard T, Hoyle R. Fitness consequences of maternal and grandmaternal
effects. Ecology and Evolution. 2014;4(15):3139-3145. doi:10.1002/ece3.1150
apa: Prizak, R., Ezard, T., & Hoyle, R. (2014). Fitness consequences of maternal
and grandmaternal effects. Ecology and Evolution. Wiley-Blackwell. https://doi.org/10.1002/ece3.1150
chicago: Prizak, Roshan, Thomas Ezard, and Rebecca Hoyle. “Fitness Consequences
of Maternal and Grandmaternal Effects.” Ecology and Evolution. Wiley-Blackwell,
2014. https://doi.org/10.1002/ece3.1150.
ieee: R. Prizak, T. Ezard, and R. Hoyle, “Fitness consequences of maternal and grandmaternal
effects,” Ecology and Evolution, vol. 4, no. 15. Wiley-Blackwell, pp. 3139–3145,
2014.
ista: Prizak R, Ezard T, Hoyle R. 2014. Fitness consequences of maternal and grandmaternal
effects. Ecology and Evolution. 4(15), 3139–3145.
mla: Prizak, Roshan, et al. “Fitness Consequences of Maternal and Grandmaternal
Effects.” Ecology and Evolution, vol. 4, no. 15, Wiley-Blackwell, 2014,
pp. 3139–45, doi:10.1002/ece3.1150.
short: R. Prizak, T. Ezard, R. Hoyle, Ecology and Evolution 4 (2014) 3139–3145.
date_created: 2018-12-11T11:47:02Z
date_published: 2014-07-19T00:00:00Z
date_updated: 2021-01-12T08:01:30Z
day: '19'
ddc:
- '530'
- '571'
department:
- _id: NiBa
- _id: GaTk
doi: 10.1002/ece3.1150
file:
- access_level: open_access
checksum: e32abf75a248e7a11811fd7f60858769
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:31Z
date_updated: 2020-07-14T12:46:38Z
file_id: '4886'
file_name: IST-2018-934-v1+1_Prizak_et_al-2014-Ecology_and_Evolution.pdf
file_size: 621582
relation: main_file
file_date_updated: 2020-07-14T12:46:38Z
has_accepted_license: '1'
intvolume: ' 4'
issue: '15'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 3139 - 3145
publication: Ecology and Evolution
publication_status: published
publisher: Wiley-Blackwell
publist_id: '7280'
pubrep_id: '934'
scopus_import: 1
status: public
title: Fitness consequences of maternal and grandmaternal effects
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4
year: '2014'
...
---
_id: '5411'
abstract:
- lang: eng
text: "Model-based testing is a promising technology for black-box software and
hardware testing, in which test cases are generated automatically from high-level
specifications. Nowadays, systems typically consist of multiple interacting components
and, due to their complexity, testing presents a considerable portion of the effort
and cost in the design process. Exploiting the compositional structure of system
specifications can considerably reduce the effort in model-based testing. Moreover,
inferring properties about the system from testing its individual components allows
the designer to reduce the amount of integration testing.\r\nIn this paper, we
study compositional properties of the IOCO-testing theory. We propose a new approach
to composition and hiding operations, inspired by contract-based design and interface
theories. These operations preserve behaviors that are compatible under composition
and hiding, and prune away incompatible ones. The resulting specification characterizes
the input sequences for which the unit testing of components is sufficient to
infer the correctness of component integration without the need for further tests.
We provide a methodology that uses these results to minimize integration testing
effort, but also to detect potential weaknesses in specifications. While we focus
on asynchronous models and the IOCO conformance relation, the resulting methodology
can be applied to a broader class of systems."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Willibald
full_name: Krenn, Willibald
last_name: Krenn
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional Specifications
for IOCO Testing. IST Austria; 2014. doi:10.15479/AT:IST-2014-148-v2-1
apa: Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional
specifications for IOCO testing. IST Austria. https://doi.org/10.15479/AT:IST-2014-148-v2-1
chicago: Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic.
Compositional Specifications for IOCO Testing. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-148-v2-1.
ieee: P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, Compositional specifications
for IOCO testing. IST Austria, 2014.
ista: Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications
for IOCO testing, IST Austria, 20p.
mla: Daca, Przemyslaw, et al. Compositional Specifications for IOCO Testing.
IST Austria, 2014, doi:10.15479/AT:IST-2014-148-v2-1.
short: P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications
for IOCO Testing, IST Austria, 2014.
date_created: 2018-12-12T11:39:11Z
date_published: 2014-01-28T00:00:00Z
date_updated: 2023-02-23T10:31:07Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2014-148-v2-1
file:
- access_level: open_access
checksum: 0e03aba625cc334141a3148432aa5760
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:21Z
date_updated: 2020-07-14T12:46:46Z
file_id: '5543'
file_name: IST-2014-148-v2+1_main_tr.pdf
file_size: 534732
relation: main_file
file_date_updated: 2020-07-14T12:46:46Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '152'
related_material:
record:
- id: '2167'
relation: later_version
status: public
status: public
title: Compositional specifications for IOCO testing
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5412'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems. We focus on qualitative properties for MDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability.\r\nWe introduce a new simulation relation to capture
the refinement relation of MDPs with respect to qualitative properties, and present
discrete graph theoretic algorithms with quadratic complexity to compute the simulation
relation.\r\nWe present an automated technique for assume-guarantee style reasoning
for compositional analysis of MDPs with qualitative properties by giving a counter-example
guided abstraction-refinement approach to compute our new simulation relation.
We have implemented our algorithms and show that the compositional analysis leads
to significant improvements. "
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: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v1-1
apa: Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative
analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v1-1
chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for
Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v1-1.
ieee: K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis
of probabilistic systems. IST Austria, 2014.
ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic
systems, IST Austria, 31p.
mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v1-1.
short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic
Systems, IST Austria, 2014.
date_created: 2018-12-12T11:39:11Z
date_published: 2014-01-29T00:00:00Z
date_updated: 2023-02-23T12:25:18Z
day: '29'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-153-v1-1
file:
- access_level: open_access
checksum: 4d6cda4bebed970926403ad6ad8c745f
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:39Z
date_updated: 2020-07-14T12:46:47Z
file_id: '5500'
file_name: IST-2014-153-v1+1_main.pdf
file_size: 423322
relation: main_file
file_date_updated: 2020-07-14T12:46:47Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '31'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '153'
related_material:
record:
- id: '2063'
relation: later_version
status: public
- id: '5413'
relation: later_version
status: public
- id: '5414'
relation: later_version
status: public
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5413'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems. We focus on qualitative properties for MDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability.\r\nWe introduce a new simulation relation to capture
the refinement relation of MDPs with respect to qualitative properties, and present
discrete graph theoretic algorithms with quadratic complexity to compute the simulation
relation.\r\nWe present an automated technique for assume-guarantee style reasoning
for compositional analysis of MDPs with qualitative properties by giving a counter-example
guided abstraction-refinement approach to compute our new simulation relation.
We have implemented our algorithms and show that the compositional analysis leads
to significant improvements. "
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: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v2-2
apa: Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative
analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v2-2
chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for
Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v2-2.
ieee: K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis
of probabilistic systems. IST Austria, 2014.
ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic
systems, IST Austria, 33p.
mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v2-2.
short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic
Systems, IST Austria, 2014.
date_created: 2018-12-12T11:39:11Z
date_published: 2014-02-06T00:00:00Z
date_updated: 2023-02-23T12:25:18Z
day: '06'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-153-v2-2
file:
- access_level: open_access
checksum: ce4967a184d84863eec76c66cbac1614
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:17Z
date_updated: 2020-07-14T12:46:47Z
file_id: '5539'
file_name: IST-2014-153-v2+2_main.pdf
file_size: 606049
relation: main_file
file_date_updated: 2020-07-14T12:46:47Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '164'
related_material:
record:
- id: '2063'
relation: later_version
status: public
- id: '5412'
relation: earlier_version
status: public
- id: '5414'
relation: later_version
status: public
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5414'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems. We focus on qualitative properties for MDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability.\r\nWe introduce a new simulation relation to capture
the refinement relation of MDPs with respect to qualitative properties, and present
discrete graph theoretic algorithms with quadratic complexity to compute the simulation
relation.\r\nWe present an automated technique for assume-guarantee style reasoning
for compositional analysis of MDPs with qualitative properties by giving a counter-example
guided abstraction-refinement approach to compute our new simulation relation.
\r\nWe have implemented our algorithms and show that the compositional analysis
leads to significant improvements. "
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: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v3-1
apa: Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative
analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v3-1
chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for
Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v3-1.
ieee: K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis
of probabilistic systems. IST Austria, 2014.
ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic
systems, IST Austria, 33p.
mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v3-1.
short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic
Systems, IST Austria, 2014.
date_created: 2018-12-12T11:39:12Z
date_published: 2014-02-07T00:00:00Z
date_updated: 2023-02-23T12:25:15Z
day: '07'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-153-v3-1
file:
- access_level: open_access
checksum: 87b93fe9af71fc5c94b0eb6151537e11
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:03Z
date_updated: 2020-07-14T12:46:48Z
file_id: '5464'
file_name: IST-2014-153-v3+1_main.pdf
file_size: 606227
relation: main_file
file_date_updated: 2020-07-14T12:46:48Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '165'
related_material:
record:
- id: '2063'
relation: later_version
status: public
- id: '5412'
relation: earlier_version
status: public
- id: '5413'
relation: earlier_version
status: public
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5415'
abstract:
- lang: eng
text: 'Recently there has been a significant effort to add quantitative properties
in formal verification and synthesis. While weighted automata over finite and
infinite words provide a natural and flexible framework to express quantitative
properties, perhaps surprisingly, several basic system properties such as average
response time cannot be expressed with weighted automata. In this work, we introduce
nested weighted automata as a new formalism for expressing important quantitative
properties such as average response time. We establish an almost complete decidability
picture for the basic decision problems for nested weighted automata, and illustrate
its applicability in several domains. '
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Otop J. Nested Weighted Automata. IST Austria;
2014. doi:10.15479/AT:IST-2014-170-v1-1
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2014). Nested weighted
automata. IST Austria. https://doi.org/10.15479/AT:IST-2014-170-v1-1
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted
Automata. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-170-v1-1.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata.
IST Austria, 2014.
ista: Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria,
27p.
mla: Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria,
2014, doi:10.15479/AT:IST-2014-170-v1-1.
short: K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria,
2014.
date_created: 2018-12-12T11:39:12Z
date_published: 2014-02-19T00:00:00Z
date_updated: 2023-02-23T12:26:19Z
day: '19'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2014-170-v1-1
file:
- access_level: open_access
checksum: 31f90dcf2cf899c3f8c6427cfcc2b3c7
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:36Z
date_updated: 2020-07-14T12:46:48Z
file_id: '5497'
file_name: IST-2014-170-v1+1_main.pdf
file_size: 573457
relation: main_file
file_date_updated: 2020-07-14T12:46:48Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '27'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '170'
related_material:
record:
- id: '1656'
relation: later_version
status: public
- id: '467'
relation: later_version
status: public
- id: '5436'
relation: later_version
status: public
status: public
title: Nested weighted automata
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5416'
abstract:
- lang: eng
text: As hybrid systems involve continuous behaviors, they should be evaluated by
quantitative methods, rather than qualitative methods. In this paper we adapt
a quantitative framework, called model measuring, to the hybrid systems domain.
The model-measuring problem asks, given a model M and a specification, what is
the maximal distance such that all models within that distance from M satisfy
(or violate) the specification. A distance function on models is given as part
of the input of the problem. Distances, especially related to continuous behaviors
are more natural in the hybrid case than the discrete case. We are interested
in distances represented by monotonic hybrid automata, a hybrid counterpart of
(discrete) weighted automata, whose recognized timed languages are monotone (w.r.t.
inclusion) in the values of parameters.The contributions of this paper are twofold.
First, we give sufficient conditions under which the model-measuring problem can
be solved. Second, we discuss the modeling of distances and applications of the
model-measuring problem.
alternative_title:
- IST Austria Technical Report
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Henzinger TA, Otop J. Model Measuring for Hybrid Systems. IST Austria;
2014. doi:10.15479/AT:IST-2014-171-v1-1
apa: Henzinger, T. A., & Otop, J. (2014). Model measuring for hybrid systems.
IST Austria. https://doi.org/10.15479/AT:IST-2014-171-v1-1
chicago: Henzinger, Thomas A, and Jan Otop. Model Measuring for Hybrid Systems.
IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-171-v1-1.
ieee: T. A. Henzinger and J. Otop, Model measuring for hybrid systems. IST
Austria, 2014.
ista: Henzinger TA, Otop J. 2014. Model measuring for hybrid systems, IST Austria,
22p.
mla: Henzinger, Thomas A., and Jan Otop. Model Measuring for Hybrid Systems.
IST Austria, 2014, doi:10.15479/AT:IST-2014-171-v1-1.
short: T.A. Henzinger, J. Otop, Model Measuring for Hybrid Systems, IST Austria,
2014.
date_created: 2018-12-12T11:39:12Z
date_published: 2014-02-19T00:00:00Z
date_updated: 2023-02-23T10:33:21Z
day: '19'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2014-171-v1-1
file:
- access_level: open_access
checksum: 445456d22371e4e49aad2b9a0c13bf80
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:32Z
date_updated: 2020-07-14T12:46:49Z
file_id: '5492'
file_name: IST-2014-171-v1+1_report.pdf
file_size: 712077
relation: main_file
file_date_updated: 2020-07-14T12:46:49Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '22'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '171'
related_material:
record:
- id: '2217'
relation: later_version
status: public
status: public
title: Model measuring for hybrid systems
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5417'
abstract:
- lang: eng
text: "We define the model-measuring problem: given a model M and specification
φ, what is the maximal distance ρ such that all models M'within distance ρ from
M satisfy (or violate)φ. The model measuring problem presupposes a distance function
on models. We concentrate on automatic distance functions, which are defined by
weighted automata.\r\nThe model-measuring problem subsumes several generalizations
of the classical model-checking problem, in particular, quantitative model-checking
problems that measure the degree of satisfaction of a specification, and robustness
problems that measure how much a model can be perturbed without violating the
specification.\r\nWe show that for automatic distance functions, and ω-regular
linear-time and branching-time specifications, the model-measuring problem can
be solved.\r\nWe use automata-theoretic model-checking methods for model measuring,
replacing the emptiness question for standard word and tree automata by the optimal-weight
question for the weighted versions of these automata. We consider weighted automata
that accumulate weights by maximizing, summing, discounting, and limit averaging.
\r\nWe give several examples of using the model-measuring problem to compute various
notions of robustness and quantitative satisfaction for temporal specifications."
alternative_title:
- IST Austria Technical Report
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Henzinger TA, Otop J. From Model Checking to Model Measuring. IST Austria;
2014. doi:10.15479/AT:IST-2014-172-v1-1
apa: Henzinger, T. A., & Otop, J. (2014). From model checking to model measuring.
IST Austria. https://doi.org/10.15479/AT:IST-2014-172-v1-1
chicago: Henzinger, Thomas A, and Jan Otop. From Model Checking to Model Measuring.
IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-172-v1-1.
ieee: T. A. Henzinger and J. Otop, From model checking to model measuring.
IST Austria, 2014.
ista: Henzinger TA, Otop J. 2014. From model checking to model measuring, IST Austria,
14p.
mla: Henzinger, Thomas A., and Jan Otop. From Model Checking to Model Measuring.
IST Austria, 2014, doi:10.15479/AT:IST-2014-172-v1-1.
short: T.A. Henzinger, J. Otop, From Model Checking to Model Measuring, IST Austria,
2014.
date_created: 2018-12-12T11:39:13Z
date_published: 2014-02-19T00:00:00Z
date_updated: 2023-02-23T10:38:10Z
day: '19'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2014-172-v1-1
file:
- access_level: open_access
checksum: fcc3eab903cfcd3778b338d2d0d44d18
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:20Z
date_updated: 2020-07-14T12:46:49Z
file_id: '5481'
file_name: IST-2014-172-v1+1_report.pdf
file_size: 383052
relation: main_file
file_date_updated: 2020-07-14T12:46:49Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '14'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '175'
related_material:
record:
- id: '2327'
relation: later_version
status: public
status: public
title: From model checking to model measuring
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...