---
_id: '1670'
abstract:
- lang: eng
text: Planning in hybrid domains poses a special challenge due to the involved mixed
discrete-continuous dynamics. A recent solving approach for such domains is based
on applying model checking techniques on a translation of PDDL+ planning problems
to hybrid automata. However, the proposed translation is limited because must
behavior is only overapproximated, and hence, processes and events are not reflected
exactly. In this paper, we present the theoretical foundation of an exact PDDL+
translation. We propose a schema to convert a hybrid automaton with must transitions
into an equivalent hybrid automaton featuring only may transitions.
acknowledgement: This work was partly supported by the German Research Foundation
(DFG) as part of the Transregional Collaborative Research Center “Automatic Verification
and Analysis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/), by the
European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science
Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and
by the Swiss National Science Foundation (SNSF) as part of the project “Automated
Reformulation and Pruning in Factored State Spaces (ARAP)”.
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Daniele
full_name: Magazzeni, Daniele
last_name: Magazzeni
- first_name: Stefano
full_name: Minopoli, Stefano
last_name: Minopoli
- first_name: Martin
full_name: Wehrle, Martin
last_name: Wehrle
citation:
ama: 'Bogomolov S, Magazzeni D, Minopoli S, Wehrle M. PDDL+ planning with hybrid
automata: Foundations of translating must behavior. In: AAAI Press; 2015:42-46.'
apa: 'Bogomolov, S., Magazzeni, D., Minopoli, S., & Wehrle, M. (2015). PDDL+
planning with hybrid automata: Foundations of translating must behavior (pp. 42–46).
Presented at the ICAPS: International Conference on Automated Planning and Scheduling,
Jerusalem, Israel: AAAI Press.'
chicago: 'Bogomolov, Sergiy, Daniele Magazzeni, Stefano Minopoli, and Martin Wehrle.
“PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior,”
42–46. AAAI Press, 2015.'
ieee: 'S. Bogomolov, D. Magazzeni, S. Minopoli, and M. Wehrle, “PDDL+ planning with
hybrid automata: Foundations of translating must behavior,” presented at the ICAPS:
International Conference on Automated Planning and Scheduling, Jerusalem, Israel,
2015, pp. 42–46.'
ista: 'Bogomolov S, Magazzeni D, Minopoli S, Wehrle M. 2015. PDDL+ planning with
hybrid automata: Foundations of translating must behavior. ICAPS: International
Conference on Automated Planning and Scheduling, 42–46.'
mla: 'Bogomolov, Sergiy, et al. PDDL+ Planning with Hybrid Automata: Foundations
of Translating Must Behavior. AAAI Press, 2015, pp. 42–46.'
short: S. Bogomolov, D. Magazzeni, S. Minopoli, M. Wehrle, in:, AAAI Press, 2015,
pp. 42–46.
conference:
end_date: 2015-06-11
location: Jerusalem, Israel
name: 'ICAPS: International Conference on Automated Planning and Scheduling'
start_date: 2015-06-07
date_created: 2018-12-11T11:53:23Z
date_published: 2015-06-01T00:00:00Z
date_updated: 2021-01-12T06:52:25Z
day: '01'
department:
- _id: ToHe
ec_funded: 1
language:
- iso: eng
main_file_link:
- url: https://www.aaai.org/ocs/index.php/ICAPS/ICAPS15/paper/view/10606/10394
month: '06'
oa_version: None
page: 42 - 46
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: AAAI Press
publist_id: '5479'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'PDDL+ planning with hybrid automata: Foundations of translating must behavior'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1671'
abstract:
- lang: eng
text: This paper studies the concrete security of PRFs and MACs obtained by keying
hash functions based on the sponge paradigm. One such hash function is KECCAK,
selected as NIST’s new SHA-3 standard. In contrast to other approaches like HMAC,
the exact security of keyed sponges is not well understood. Indeed, recent security
analyses delivered concrete security bounds which are far from existing attacks.
This paper aims to close this gap. We prove (nearly) exact bounds on the concrete
PRF security of keyed sponges using a random permutation. These bounds are tight
for the most relevant ranges of parameters, i.e., for messages of length (roughly)
l ≤ min{2n/4, 2r} blocks, where n is the state size and r is the desired output
length; and for l ≤ q queries (to the construction or the underlying permutation).
Moreover, we also improve standard-model bounds. As an intermediate step of independent
interest, we prove tight bounds on the PRF security of the truncated CBC-MAC construction,
which operates as plain CBC-MAC, but only returns a prefix of the output.
alternative_title:
- LNCS
author:
- first_name: Peter
full_name: Gazi, Peter
id: 3E0BFE38-F248-11E8-B48F-1D18A9856A87
last_name: Gazi
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
- first_name: Stefano
full_name: Tessaro, Stefano
last_name: Tessaro
citation:
ama: 'Gazi P, Pietrzak KZ, Tessaro S. The exact PRF security of truncation: Tight
bounds for keyed sponges and truncated CBC. In: Vol 9215. Springer; 2015:368-387.
doi:10.1007/978-3-662-47989-6_18'
apa: 'Gazi, P., Pietrzak, K. Z., & Tessaro, S. (2015). The exact PRF security
of truncation: Tight bounds for keyed sponges and truncated CBC (Vol. 9215, pp.
368–387). Presented at the CRYPTO: International Cryptology Conference, Santa
Barbara, CA, United States: Springer. https://doi.org/10.1007/978-3-662-47989-6_18'
chicago: 'Gazi, Peter, Krzysztof Z Pietrzak, and Stefano Tessaro. “The Exact PRF
Security of Truncation: Tight Bounds for Keyed Sponges and Truncated CBC,” 9215:368–87.
Springer, 2015. https://doi.org/10.1007/978-3-662-47989-6_18.'
ieee: 'P. Gazi, K. Z. Pietrzak, and S. Tessaro, “The exact PRF security of truncation:
Tight bounds for keyed sponges and truncated CBC,” presented at the CRYPTO: International
Cryptology Conference, Santa Barbara, CA, United States, 2015, vol. 9215, pp.
368–387.'
ista: 'Gazi P, Pietrzak KZ, Tessaro S. 2015. The exact PRF security of truncation:
Tight bounds for keyed sponges and truncated CBC. CRYPTO: International Cryptology
Conference, LNCS, vol. 9215, 368–387.'
mla: 'Gazi, Peter, et al. The Exact PRF Security of Truncation: Tight Bounds
for Keyed Sponges and Truncated CBC. Vol. 9215, Springer, 2015, pp. 368–87,
doi:10.1007/978-3-662-47989-6_18.'
short: P. Gazi, K.Z. Pietrzak, S. Tessaro, in:, Springer, 2015, pp. 368–387.
conference:
end_date: 2015-08-20
location: Santa Barbara, CA, United States
name: 'CRYPTO: International Cryptology Conference'
start_date: 2015-08-16
date_created: 2018-12-11T11:53:23Z
date_published: 2015-08-01T00:00:00Z
date_updated: 2021-01-12T06:52:25Z
day: '01'
ddc:
- '004'
- '005'
department:
- _id: KrPi
doi: 10.1007/978-3-662-47989-6_18
ec_funded: 1
file:
- access_level: open_access
checksum: 17d854227b3b753fd34f5d29e5b5a32e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:38Z
date_updated: 2020-07-14T12:45:11Z
file_id: '4827'
file_name: IST-2016-673-v1+1_053.pdf
file_size: 592296
relation: main_file
file_date_updated: 2020-07-14T12:45:11Z
has_accepted_license: '1'
intvolume: ' 9215'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 368 - 387
project:
- _id: 258C570E-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '259668'
name: Provable Security for Physical Cryptography
publication_status: published
publisher: Springer
publist_id: '5478'
pubrep_id: '673'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'The exact PRF security of truncation: Tight bounds for keyed sponges and truncated
CBC'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9215
year: '2015'
...
---
_id: '1672'
abstract:
- lang: eng
text: Composable notions of incoercibility aim to forbid a coercer from using anything
beyond the coerced parties’ inputs and outputs to catch them when they try to
deceive him. Existing definitions are restricted to weak coercion types, and/or
are not universally composable. Furthermore, they often make too strong assumptions
on the knowledge of coerced parties—e.g., they assume they known the identities
and/or the strategies of other coerced parties, or those of corrupted parties—
which makes them unsuitable for applications of incoercibility such as e-voting,
where colluding adversarial parties may attempt to coerce honest voters, e.g.,
by offering them money for a promised vote, and use their own view to check that
the voter keeps his end of the bargain. In this work we put forward the first
universally composable notion of incoercible multi-party computation, which satisfies
the above intuition and does not assume collusions among coerced parties or knowledge
of the corrupted set. We define natural notions of UC incoercibility corresponding
to standard coercion-types, i.e., receipt-freeness and resistance to full-active
coercion. Importantly, our suggested notion has the unique property that it builds
on top of the well studied UC framework by Canetti instead of modifying it. This
guarantees backwards compatibility, and allows us to inherit results from the
rich UC literature. We then present MPC protocols which realize our notions of
UC incoercibility given access to an arguably minimal setup—namely honestly generate
tamper-proof hardware performing a very simple cryptographic operation—e.g., a
smart card. This is, to our knowledge, the first proposed construction of an MPC
protocol (for more than two parties) that is incoercibly secure and universally
composable, and therefore the first construction of a universally composable receipt-free
e-voting protocol.
acknowledgement: Joël Alwen was supported by the ERC starting grant (259668-PSPC).
Rafail Ostrovsky was supported in part by NSF grants 09165174, 1065276, 1118126
and 1136174, US-Israel BSF grant 2008411, OKAWA Foundation Research Award, IBM Faculty
Research Award, Xerox Faculty Research Award, B. John Garrick Foundation Award,
Teradata Research Award, Lockheed-Martin Corporation Research Award, and the Defense
Advanced Research Projects Agency through the U.S. Office of Naval Research under
Contract N00014 -11 -1-0392. The views expressed are those of the author and do
not reflect the official policy or position of the Department of Defense or the
U.S. Government. Vassilis Zikas was supported in part by the Swiss National Science
Foundation (SNF) via the Ambizione grant PZ00P-2142549.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Joel F
full_name: Alwen, Joel F
id: 2A8DFA8C-F248-11E8-B48F-1D18A9856A87
last_name: Alwen
- first_name: Rafail
full_name: Ostrovsky, Rafail
last_name: Ostrovsky
- first_name: Hongsheng
full_name: Zhou, Hongsheng
last_name: Zhou
- first_name: Vassilis
full_name: Zikas, Vassilis
last_name: Zikas
citation:
ama: 'Alwen JF, Ostrovsky R, Zhou H, Zikas V. Incoercible multi-party computation
and universally composable receipt-free voting. In: Advances in Cryptology
- CRYPTO 2015. Vol 9216. Lecture Notes in Computer Science. Springer; 2015:763-780.
doi:10.1007/978-3-662-48000-7_37'
apa: 'Alwen, J. F., Ostrovsky, R., Zhou, H., & Zikas, V. (2015). Incoercible
multi-party computation and universally composable receipt-free voting. In Advances
in Cryptology - CRYPTO 2015 (Vol. 9216, pp. 763–780). Santa Barbara, CA, United
States: Springer. https://doi.org/10.1007/978-3-662-48000-7_37'
chicago: Alwen, Joel F, Rafail Ostrovsky, Hongsheng Zhou, and Vassilis Zikas. “Incoercible
Multi-Party Computation and Universally Composable Receipt-Free Voting.” In Advances
in Cryptology - CRYPTO 2015, 9216:763–80. Lecture Notes in Computer Science.
Springer, 2015. https://doi.org/10.1007/978-3-662-48000-7_37.
ieee: J. F. Alwen, R. Ostrovsky, H. Zhou, and V. Zikas, “Incoercible multi-party
computation and universally composable receipt-free voting,” in Advances in
Cryptology - CRYPTO 2015, Santa Barbara, CA, United States, 2015, vol. 9216,
pp. 763–780.
ista: 'Alwen JF, Ostrovsky R, Zhou H, Zikas V. 2015. Incoercible multi-party computation
and universally composable receipt-free voting. Advances in Cryptology - CRYPTO
2015. CRYPTO: International Cryptology ConferenceLecture Notes in Computer Science,
LNCS, vol. 9216, 763–780.'
mla: Alwen, Joel F., et al. “Incoercible Multi-Party Computation and Universally
Composable Receipt-Free Voting.” Advances in Cryptology - CRYPTO 2015,
vol. 9216, Springer, 2015, pp. 763–80, doi:10.1007/978-3-662-48000-7_37.
short: J.F. Alwen, R. Ostrovsky, H. Zhou, V. Zikas, in:, Advances in Cryptology
- CRYPTO 2015, Springer, 2015, pp. 763–780.
conference:
end_date: 2015-08-20
location: Santa Barbara, CA, United States
name: 'CRYPTO: International Cryptology Conference'
start_date: 2015-08-16
date_created: 2018-12-11T11:53:23Z
date_published: 2015-08-01T00:00:00Z
date_updated: 2022-06-07T09:51:55Z
day: '01'
ddc:
- '000'
department:
- _id: KrPi
doi: 10.1007/978-3-662-48000-7_37
ec_funded: 1
file:
- access_level: open_access
checksum: 5b6649e80d1f781a8910f7cce6427f78
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:55:29Z
date_updated: 2020-07-14T12:45:11Z
file_id: '7853'
file_name: 2015_CRYPTO_Alwen.pdf
file_size: 397363
relation: main_file
file_date_updated: 2020-07-14T12:45:11Z
has_accepted_license: '1'
intvolume: ' 9216'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 763 - 780
project:
- _id: 258C570E-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '259668'
name: Provable Security for Physical Cryptography
publication: Advances in Cryptology - CRYPTO 2015
publication_identifier:
eisbn:
- 978-3-662-48000-7
isbn:
- 978-3-662-47999-5
publication_status: published
publisher: Springer
publist_id: '5476'
quality_controlled: '1'
scopus_import: '1'
series_title: Lecture Notes in Computer Science
status: public
title: Incoercible multi-party computation and universally composable receipt-free
voting
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9216
year: '2015'
...
---
_id: '1673'
abstract:
- lang: eng
text: 'When a new mutant arises in a population, there is a probability it outcompetes
the residents and fixes. The structure of the population can affect this fixation
probability. Suppressing population structures reduce the difference between two
competing variants, while amplifying population structures enhance the difference.
Suppressors are ubiquitous and easy to construct, but amplifiers for the large
population limit are more elusive and only a few examples have been discovered.
Whether or not a population structure is an amplifier of selection depends on
the probability distribution for the placement of the invading mutant. First,
we prove that there exist only bounded amplifiers for adversarial placement-that
is, for arbitrary initial conditions. Next, we show that the Star population structure,
which is known to amplify for mutants placed uniformly at random, does not amplify
for mutants that arise through reproduction and are therefore placed proportional
to the temperatures of the vertices. Finally, we construct population structures
that amplify for all mutational events that arise through reproduction, uniformly
at random, or through some combination of the two. '
acknowledgement: 'K.C. gratefully acknowledges support from ERC Start grant no. (279307:
Graph Games), Austrian Science Fund (FWF) grant no. P23499-N23, and FWF NFN grant
no. S11407-N23 (RiSE). '
article_number: '20150114'
author:
- first_name: Ben
full_name: Adlam, Ben
last_name: Adlam
- 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: Nowak, Martin
last_name: Nowak
citation:
ama: 'Adlam B, Chatterjee K, Nowak M. Amplifiers of selection. Proceedings of
the Royal Society A: Mathematical, Physical and Engineering Sciences. 2015;471(2181).
doi:10.1098/rspa.2015.0114'
apa: 'Adlam, B., Chatterjee, K., & Nowak, M. (2015). Amplifiers of selection.
Proceedings of the Royal Society A: Mathematical, Physical and Engineering
Sciences. Royal Society of London. https://doi.org/10.1098/rspa.2015.0114'
chicago: 'Adlam, Ben, Krishnendu Chatterjee, and Martin Nowak. “Amplifiers of Selection.”
Proceedings of the Royal Society A: Mathematical, Physical and Engineering
Sciences. Royal Society of London, 2015. https://doi.org/10.1098/rspa.2015.0114.'
ieee: 'B. Adlam, K. Chatterjee, and M. Nowak, “Amplifiers of selection,” Proceedings
of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol.
471, no. 2181. Royal Society of London, 2015.'
ista: 'Adlam B, Chatterjee K, Nowak M. 2015. Amplifiers of selection. Proceedings
of the Royal Society A: Mathematical, Physical and Engineering Sciences. 471(2181),
20150114.'
mla: 'Adlam, Ben, et al. “Amplifiers of Selection.” Proceedings of the Royal
Society A: Mathematical, Physical and Engineering Sciences, vol. 471, no.
2181, 20150114, Royal Society of London, 2015, doi:10.1098/rspa.2015.0114.'
short: 'B. Adlam, K. Chatterjee, M. Nowak, Proceedings of the Royal Society A: Mathematical,
Physical and Engineering Sciences 471 (2015).'
date_created: 2018-12-11T11:53:24Z
date_published: 2015-09-08T00:00:00Z
date_updated: 2021-01-12T06:52:26Z
day: '08'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1098/rspa.2015.0114
ec_funded: 1
file:
- access_level: open_access
checksum: e613d94d283c776322403a28aad11bdd
content_type: application/pdf
creator: kschuh
date_created: 2019-04-18T12:39:56Z
date_updated: 2020-07-14T12:45:11Z
file_id: '6342'
file_name: 2015_rspa_Adlam.pdf
file_size: 391466
relation: main_file
file_date_updated: 2020-07-14T12:45:11Z
has_accepted_license: '1'
intvolume: ' 471'
issue: '2181'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: 'Proceedings of the Royal Society A: Mathematical, Physical and Engineering
Sciences'
publication_status: published
publisher: Royal Society of London
publist_id: '5477'
quality_controlled: '1'
scopus_import: 1
status: public
title: Amplifiers of selection
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 471
year: '2015'
...
---
_id: '1674'
abstract:
- lang: eng
text: We consider N × N random matrices of the form H = W + V where W is a real
symmetric Wigner matrix and V a random or deterministic, real, diagonal matrix
whose entries are independent of W. We assume subexponential decay for the matrix
entries of W and we choose V so that the eigenvalues of W and V are typically
of the same order. For a large class of diagonal matrices V, we show that the
rescaled distribution of the extremal eigenvalues is given by the Tracy-Widom
distribution F1 in the limit of large N. Our proofs also apply to the complex
Hermitian setting, i.e. when W is a complex Hermitian Wigner matrix.
article_number: '1550018'
author:
- first_name: Jioon
full_name: Lee, Jioon
last_name: Lee
- first_name: Kevin
full_name: Schnelli, Kevin
id: 434AD0AE-F248-11E8-B48F-1D18A9856A87
last_name: Schnelli
orcid: 0000-0003-0954-3231
citation:
ama: Lee J, Schnelli K. Edge universality for deformed Wigner matrices. Reviews
in Mathematical Physics. 2015;27(8). doi:10.1142/S0129055X1550018X
apa: Lee, J., & Schnelli, K. (2015). Edge universality for deformed Wigner matrices.
Reviews in Mathematical Physics. World Scientific Publishing. https://doi.org/10.1142/S0129055X1550018X
chicago: Lee, Jioon, and Kevin Schnelli. “Edge Universality for Deformed Wigner
Matrices.” Reviews in Mathematical Physics. World Scientific Publishing,
2015. https://doi.org/10.1142/S0129055X1550018X.
ieee: J. Lee and K. Schnelli, “Edge universality for deformed Wigner matrices,”
Reviews in Mathematical Physics, vol. 27, no. 8. World Scientific Publishing,
2015.
ista: Lee J, Schnelli K. 2015. Edge universality for deformed Wigner matrices. Reviews
in Mathematical Physics. 27(8), 1550018.
mla: Lee, Jioon, and Kevin Schnelli. “Edge Universality for Deformed Wigner Matrices.”
Reviews in Mathematical Physics, vol. 27, no. 8, 1550018, World Scientific
Publishing, 2015, doi:10.1142/S0129055X1550018X.
short: J. Lee, K. Schnelli, Reviews in Mathematical Physics 27 (2015).
date_created: 2018-12-11T11:53:24Z
date_published: 2015-09-01T00:00:00Z
date_updated: 2021-01-12T06:52:26Z
day: '01'
department:
- _id: LaEr
doi: 10.1142/S0129055X1550018X
intvolume: ' 27'
issue: '8'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1407.8015
month: '09'
oa: 1
oa_version: Preprint
publication: Reviews in Mathematical Physics
publication_status: published
publisher: World Scientific Publishing
publist_id: '5475'
quality_controlled: '1'
scopus_import: 1
status: public
title: Edge universality for deformed Wigner matrices
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 27
year: '2015'
...
---
_id: '1675'
abstract:
- lang: eng
text: Proofs of work (PoW) have been suggested by Dwork and Naor (Crypto’92) as
protection to a shared resource. The basic idea is to ask the service requestor
to dedicate some non-trivial amount of computational work to every request. The
original applications included prevention of spam and protection against denial
of service attacks. More recently, PoWs have been used to prevent double spending
in the Bitcoin digital currency system. In this work, we put forward an alternative
concept for PoWs - so-called proofs of space (PoS), where a service requestor
must dedicate a significant amount of disk space as opposed to computation. We
construct secure PoS schemes in the random oracle model (with one additional mild
assumption required for the proof to go through), using graphs with high “pebbling
complexity” and Merkle hash-trees. We discuss some applications, including follow-up
work where a decentralized digital currency scheme called Spacecoin is constructed
that uses PoS (instead of wasteful PoW like in Bitcoin) to prevent double spending.
The main technical contribution of this work is the construction of (directed,
loop-free) graphs on N vertices with in-degree O(log logN) such that even if one
places Θ(N) pebbles on the nodes of the graph, there’s a constant fraction of
nodes that needs Θ(N) steps to be pebbled (where in every step one can put a pebble
on a node if all its parents have a pebble).
alternative_title:
- LNCS
author:
- first_name: Stefan
full_name: Dziembowski, Stefan
last_name: Dziembowski
- first_name: Sebastian
full_name: Faust, Sebastian
last_name: Faust
- first_name: Vladimir
full_name: Kolmogorov, Vladimir
id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
last_name: Kolmogorov
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
citation:
ama: Dziembowski S, Faust S, Kolmogorov V, Pietrzak KZ. Proofs of space. 2015;9216:585-605.
doi:10.1007/978-3-662-48000-7_29
apa: 'Dziembowski, S., Faust, S., Kolmogorov, V., & Pietrzak, K. Z. (2015).
Proofs of space. Presented at the CRYPTO: International Cryptology Conference,
Santa Barbara, CA, United States: Springer. https://doi.org/10.1007/978-3-662-48000-7_29'
chicago: Dziembowski, Stefan, Sebastian Faust, Vladimir Kolmogorov, and Krzysztof
Z Pietrzak. “Proofs of Space.” Lecture Notes in Computer Science. Springer, 2015.
https://doi.org/10.1007/978-3-662-48000-7_29.
ieee: S. Dziembowski, S. Faust, V. Kolmogorov, and K. Z. Pietrzak, “Proofs of space,”
vol. 9216. Springer, pp. 585–605, 2015.
ista: Dziembowski S, Faust S, Kolmogorov V, Pietrzak KZ. 2015. Proofs of space.
9216, 585–605.
mla: Dziembowski, Stefan, et al. Proofs of Space. Vol. 9216, Springer, 2015,
pp. 585–605, doi:10.1007/978-3-662-48000-7_29.
short: S. Dziembowski, S. Faust, V. Kolmogorov, K.Z. Pietrzak, 9216 (2015) 585–605.
conference:
end_date: 2015-08-20
location: Santa Barbara, CA, United States
name: 'CRYPTO: International Cryptology Conference'
start_date: 2015-08-16
date_created: 2018-12-11T11:53:24Z
date_published: 2015-08-01T00:00:00Z
date_updated: 2023-02-23T10:35:50Z
day: '01'
department:
- _id: VlKo
- _id: KrPi
doi: 10.1007/978-3-662-48000-7_29
ec_funded: 1
intvolume: ' 9216'
language:
- iso: eng
month: '08'
oa_version: None
page: 585 - 605
project:
- _id: 25FBA906-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '616160'
name: 'Discrete Optimization in Computer Vision: Theory and Practice'
- _id: 258C570E-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '259668'
name: Provable Security for Physical Cryptography
publication_status: published
publisher: Springer
publist_id: '5474'
pubrep_id: '671'
quality_controlled: '1'
related_material:
record:
- id: '2274'
relation: earlier_version
status: public
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Proofs of space
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9216
year: '2015'
...
---
_id: '1676'
author:
- first_name: Michael K
full_name: Sixt, Michael K
id: 41E9FBEA-F248-11E8-B48F-1D18A9856A87
last_name: Sixt
orcid: 0000-0002-6620-9179
- first_name: Erez
full_name: Raz, Erez
last_name: Raz
citation:
ama: 'Sixt MK, Raz E. Editorial overview: Cell adhesion and migration. Current
Opinion in Cell Biology. 2015;36(10):4-6. doi:10.1016/j.ceb.2015.09.004'
apa: 'Sixt, M. K., & Raz, E. (2015). Editorial overview: Cell adhesion and migration.
Current Opinion in Cell Biology. Elsevier. https://doi.org/10.1016/j.ceb.2015.09.004'
chicago: 'Sixt, Michael K, and Erez Raz. “Editorial Overview: Cell Adhesion and
Migration.” Current Opinion in Cell Biology. Elsevier, 2015. https://doi.org/10.1016/j.ceb.2015.09.004.'
ieee: 'M. K. Sixt and E. Raz, “Editorial overview: Cell adhesion and migration,”
Current Opinion in Cell Biology, vol. 36, no. 10. Elsevier, pp. 4–6, 2015.'
ista: 'Sixt MK, Raz E. 2015. Editorial overview: Cell adhesion and migration. Current
Opinion in Cell Biology. 36(10), 4–6.'
mla: 'Sixt, Michael K., and Erez Raz. “Editorial Overview: Cell Adhesion and Migration.”
Current Opinion in Cell Biology, vol. 36, no. 10, Elsevier, 2015, pp. 4–6,
doi:10.1016/j.ceb.2015.09.004.'
short: M.K. Sixt, E. Raz, Current Opinion in Cell Biology 36 (2015) 4–6.
date_created: 2018-12-11T11:53:25Z
date_published: 2015-10-01T00:00:00Z
date_updated: 2021-01-12T06:52:27Z
day: '01'
department:
- _id: MiSi
doi: 10.1016/j.ceb.2015.09.004
intvolume: ' 36'
issue: '10'
language:
- iso: eng
month: '10'
oa_version: None
page: 4 - 6
publication: Current Opinion in Cell Biology
publication_status: published
publisher: Elsevier
publist_id: '5473'
scopus_import: 1
status: public
title: 'Editorial overview: Cell adhesion and migration'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 36
year: '2015'
...
---
_id: '1677'
abstract:
- lang: eng
text: We consider real symmetric and complex Hermitian random matrices with the
additional symmetry hxy = hN-y,N-x. The matrix elements are independent (up to
the fourfold symmetry) and not necessarily identically distributed. This ensemble
naturally arises as the Fourier transform of a Gaussian orthogonal ensemble. Italso
occurs as the flip matrix model - an approximation of the two-dimensional Anderson
model at small disorder. We show that the density of states converges to the Wigner
semicircle law despite the new symmetry type. We also prove the local version
of the semicircle law on the optimal scale.
article_number: '103301'
author:
- first_name: Johannes
full_name: Alt, Johannes
id: 36D3D8B6-F248-11E8-B48F-1D18A9856A87
last_name: Alt
citation:
ama: Alt J. The local semicircle law for random matrices with a fourfold symmetry.
Journal of Mathematical Physics. 2015;56(10). doi:10.1063/1.4932606
apa: Alt, J. (2015). The local semicircle law for random matrices with a fourfold
symmetry. Journal of Mathematical Physics. American Institute of Physics.
https://doi.org/10.1063/1.4932606
chicago: Alt, Johannes. “The Local Semicircle Law for Random Matrices with a Fourfold
Symmetry.” Journal of Mathematical Physics. American Institute of Physics,
2015. https://doi.org/10.1063/1.4932606.
ieee: J. Alt, “The local semicircle law for random matrices with a fourfold symmetry,”
Journal of Mathematical Physics, vol. 56, no. 10. American Institute of
Physics, 2015.
ista: Alt J. 2015. The local semicircle law for random matrices with a fourfold
symmetry. Journal of Mathematical Physics. 56(10), 103301.
mla: Alt, Johannes. “The Local Semicircle Law for Random Matrices with a Fourfold
Symmetry.” Journal of Mathematical Physics, vol. 56, no. 10, 103301, American
Institute of Physics, 2015, doi:10.1063/1.4932606.
short: J. Alt, Journal of Mathematical Physics 56 (2015).
date_created: 2018-12-11T11:53:25Z
date_published: 2015-10-09T00:00:00Z
date_updated: 2023-09-07T12:38:08Z
day: '09'
department:
- _id: LaEr
doi: 10.1063/1.4932606
ec_funded: 1
intvolume: ' 56'
issue: '10'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1506.04683
month: '10'
oa: 1
oa_version: Preprint
project:
- _id: 258DCDE6-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '338804'
name: Random matrices, universality and disordered quantum systems
publication: Journal of Mathematical Physics
publication_status: published
publisher: American Institute of Physics
publist_id: '5472'
quality_controlled: '1'
related_material:
record:
- id: '149'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: The local semicircle law for random matrices with a fourfold symmetry
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 56
year: '2015'
...
---
_id: '1678'
abstract:
- lang: eng
text: High-throughput live-cell screens are intricate elements of systems biology
studies and drug discovery pipelines. Here, we demonstrate an optogenetics-assisted
method that avoids the need for chemical activators and reporters, reduces the
number of operational steps and increases information content in a cell-based
small-molecule screen against human protein kinases, including an orphan receptor
tyrosine kinase. This blueprint for all-optical screening can be adapted to many
drug targets and cellular processes.
acknowledgement: 'This work was supported by grants from the European Union Seventh
Framework Programme (CIG-303564 to H.J. and ERC-StG-311166 to S.M.B.N.), the Human
Frontier Science Program (RGY0084_2012 to H.J.) and the Herzfelder Foundation (to
M.G.). A.I.-P. was supported by a Ramon Areces fellowship, and E.R. by the graduate
program MolecularDrugTargets (Austrian Science Fund (FWF): W 1232) and a FemTech
fellowship (3580812 Austrian Research Promotion Agency).'
author:
- first_name: Álvaro
full_name: Inglés Prieto, Álvaro
id: 2A9DB292-F248-11E8-B48F-1D18A9856A87
last_name: Inglés Prieto
orcid: 0000-0002-5409-8571
- first_name: Eva
full_name: Gschaider-Reichhart, Eva
id: 3FEE232A-F248-11E8-B48F-1D18A9856A87
last_name: Gschaider-Reichhart
orcid: 0000-0002-7218-7738
- first_name: Markus
full_name: Muellner, Markus
last_name: Muellner
- first_name: Matthias
full_name: Nowak, Matthias
id: 30845DAA-F248-11E8-B48F-1D18A9856A87
last_name: Nowak
- first_name: Sebastian
full_name: Nijman, Sebastian
last_name: Nijman
- first_name: Michael
full_name: Grusch, Michael
last_name: Grusch
- first_name: Harald L
full_name: Janovjak, Harald L
id: 33BA6C30-F248-11E8-B48F-1D18A9856A87
last_name: Janovjak
orcid: 0000-0002-8023-9315
citation:
ama: Inglés Prieto Á, Gschaider-Reichhart E, Muellner M, et al. Light-assisted small-molecule
screening against protein kinases. Nature Chemical Biology. 2015;11(12):952-954.
doi:10.1038/nchembio.1933
apa: Inglés Prieto, Á., Gschaider-Reichhart, E., Muellner, M., Nowak, M., Nijman,
S., Grusch, M., & Janovjak, H. L. (2015). Light-assisted small-molecule screening
against protein kinases. Nature Chemical Biology. Nature Publishing Group.
https://doi.org/10.1038/nchembio.1933
chicago: Inglés Prieto, Álvaro, Eva Gschaider-Reichhart, Markus Muellner, Matthias
Nowak, Sebastian Nijman, Michael Grusch, and Harald L Janovjak. “Light-Assisted
Small-Molecule Screening against Protein Kinases.” Nature Chemical Biology.
Nature Publishing Group, 2015. https://doi.org/10.1038/nchembio.1933.
ieee: Á. Inglés Prieto et al., “Light-assisted small-molecule screening against
protein kinases,” Nature Chemical Biology, vol. 11, no. 12. Nature Publishing
Group, pp. 952–954, 2015.
ista: Inglés Prieto Á, Gschaider-Reichhart E, Muellner M, Nowak M, Nijman S, Grusch
M, Janovjak HL. 2015. Light-assisted small-molecule screening against protein
kinases. Nature Chemical Biology. 11(12), 952–954.
mla: Inglés Prieto, Álvaro, et al. “Light-Assisted Small-Molecule Screening against
Protein Kinases.” Nature Chemical Biology, vol. 11, no. 12, Nature Publishing
Group, 2015, pp. 952–54, doi:10.1038/nchembio.1933.
short: Á. Inglés Prieto, E. Gschaider-Reichhart, M. Muellner, M. Nowak, S. Nijman,
M. Grusch, H.L. Janovjak, Nature Chemical Biology 11 (2015) 952–954.
date_created: 2018-12-11T11:53:25Z
date_published: 2015-10-12T00:00:00Z
date_updated: 2023-09-07T12:49:09Z
day: '12'
ddc:
- '571'
department:
- _id: HaJa
- _id: LifeSc
doi: 10.1038/nchembio.1933
ec_funded: 1
file:
- access_level: open_access
checksum: e9fb251dfcb7cd209b83f17867e61321
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:51Z
date_updated: 2020-07-14T12:45:12Z
file_id: '4842'
file_name: IST-2017-837-v1+1_ingles-prieto.pdf
file_size: 1308364
relation: main_file
file_date_updated: 2020-07-14T12:45:12Z
has_accepted_license: '1'
intvolume: ' 11'
issue: '12'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 952 - 954
project:
- _id: 25548C20-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '303564'
name: Microbial Ion Channels for Synthetic Neurobiology
- _id: 255BFFFA-B435-11E9-9278-68D0E5697425
grant_number: RGY0084/2012
name: In situ real-time imaging of neurotransmitter signaling using designer optical
sensors (HFSP Young Investigator)
- _id: 255A6082-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: W1232-B24
name: Molecular Drug Targets
publication: Nature Chemical Biology
publication_status: published
publisher: Nature Publishing Group
publist_id: '5471'
pubrep_id: '837'
quality_controlled: '1'
related_material:
record:
- id: '418'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Light-assisted small-molecule screening against protein kinases
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 11
year: '2015'
...
---
_id: '1679'
article_number: '091102'
author:
- first_name: Grégoire M
full_name: Lemoult, Grégoire M
id: 4787FE80-F248-11E8-B48F-1D18A9856A87
last_name: Lemoult
- first_name: Philipp
full_name: Maier, Philipp
id: 384F7C04-F248-11E8-B48F-1D18A9856A87
last_name: Maier
- first_name: Björn
full_name: Hof, Björn
id: 3A374330-F248-11E8-B48F-1D18A9856A87
last_name: Hof
orcid: 0000-0003-2057-2754
citation:
ama: Lemoult GM, Maier P, Hof B. Taylor’s Forest. Physics of Fluids. 2015;27(9).
doi:10.1063/1.4930850
apa: Lemoult, G. M., Maier, P., & Hof, B. (2015). Taylor’s Forest. Physics
of Fluids. American Institute of Physics. https://doi.org/10.1063/1.4930850
chicago: Lemoult, Grégoire M, Philipp Maier, and Björn Hof. “Taylor’s Forest.” Physics
of Fluids. American Institute of Physics, 2015. https://doi.org/10.1063/1.4930850.
ieee: G. M. Lemoult, P. Maier, and B. Hof, “Taylor’s Forest,” Physics of Fluids,
vol. 27, no. 9. American Institute of Physics, 2015.
ista: Lemoult GM, Maier P, Hof B. 2015. Taylor’s Forest. Physics of Fluids. 27(9),
091102.
mla: Lemoult, Grégoire M., et al. “Taylor’s Forest.” Physics of Fluids, vol.
27, no. 9, 091102, American Institute of Physics, 2015, doi:10.1063/1.4930850.
short: G.M. Lemoult, P. Maier, B. Hof, Physics of Fluids 27 (2015).
date_created: 2018-12-11T11:53:26Z
date_published: 2015-09-24T00:00:00Z
date_updated: 2021-01-12T06:52:28Z
day: '24'
ddc:
- '532'
department:
- _id: BjHo
doi: 10.1063/1.4930850
file:
- access_level: open_access
checksum: 604bba3c2496aadb3efcff77de01ce6c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:35Z
date_updated: 2020-07-14T12:45:12Z
file_id: '5019'
file_name: IST-2017-748-v1+1_1.4930850.pdf
file_size: 872366
relation: main_file
file_date_updated: 2020-07-14T12:45:12Z
has_accepted_license: '1'
intvolume: ' 27'
issue: '9'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
publication: Physics of Fluids
publication_status: published
publisher: American Institute of Physics
publist_id: '5469'
pubrep_id: '748'
quality_controlled: '1'
scopus_import: 1
status: public
title: Taylor's Forest
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: 27
year: '2015'
...
---
_id: '1680'
abstract:
- lang: eng
text: We consider the satisfiability problem for modal logic over first-order definable
classes of frames.We confirm the conjecture from Hemaspaandra and Schnoor [2008]
that modal logic is decidable over classes definable by universal Horn formulae.
We provide a full classification of Horn formulae with respect to the complexity
of the corresponding satisfiability problem. It turns out, that except for the
trivial case of inconsistent formulae, local satisfiability is eitherNP-complete
or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete,
or ExpTime-complete. We also show that the finite satisfiability problem for modal
logic over Horn definable classes of frames is decidable. On the negative side,
we show undecidability of two related problems. First, we exhibit a simple universal
three-variable formula defining the class of frames over which modal logic is
undecidable. Second, we consider the satisfiability problem of bimodal logic over
Horn definable classes of frames, and also present a formula leading to undecidability.
article_number: '2'
author:
- first_name: Jakub
full_name: Michaliszyn, Jakub
last_name: Michaliszyn
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
- first_name: Emanuel
full_name: Kieroňski, Emanuel
last_name: Kieroňski
citation:
ama: Michaliszyn J, Otop J, Kieroňski E. On the decidability of elementary modal
logics. ACM Transactions on Computational Logic. 2015;17(1). doi:10.1145/2817825
apa: Michaliszyn, J., Otop, J., & Kieroňski, E. (2015). On the decidability
of elementary modal logics. ACM Transactions on Computational Logic. ACM.
https://doi.org/10.1145/2817825
chicago: Michaliszyn, Jakub, Jan Otop, and Emanuel Kieroňski. “On the Decidability
of Elementary Modal Logics.” ACM Transactions on Computational Logic. ACM,
2015. https://doi.org/10.1145/2817825.
ieee: J. Michaliszyn, J. Otop, and E. Kieroňski, “On the decidability of elementary
modal logics,” ACM Transactions on Computational Logic, vol. 17, no. 1.
ACM, 2015.
ista: Michaliszyn J, Otop J, Kieroňski E. 2015. On the decidability of elementary
modal logics. ACM Transactions on Computational Logic. 17(1), 2.
mla: Michaliszyn, Jakub, et al. “On the Decidability of Elementary Modal Logics.”
ACM Transactions on Computational Logic, vol. 17, no. 1, 2, ACM, 2015,
doi:10.1145/2817825.
short: J. Michaliszyn, J. Otop, E. Kieroňski, ACM Transactions on Computational
Logic 17 (2015).
date_created: 2018-12-11T11:53:26Z
date_published: 2015-09-01T00:00:00Z
date_updated: 2021-01-12T06:52:29Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2817825
ec_funded: 1
intvolume: ' 17'
issue: '1'
language:
- iso: eng
month: '09'
oa_version: None
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: ACM Transactions on Computational Logic
publication_status: published
publisher: ACM
publist_id: '5468'
quality_controlled: '1'
status: public
title: On the decidability of elementary modal logics
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 17
year: '2015'
...
---
_id: '1681'
abstract:
- lang: eng
text: In many social situations, individuals endeavor to find the single best possible
partner, but are constrained to evaluate the candidates in sequence. Examples
include the search for mates, economic partnerships, or any other long-term ties
where the choice to interact involves two parties. Surprisingly, however, previous
theoretical work on mutual choice problems focuses on finding equilibrium solutions,
while ignoring the evolutionary dynamics of decisions. Empirically, this may be
of high importance, as some equilibrium solutions can never be reached unless
the population undergoes radical changes and a sufficient number of individuals
change their decisions simultaneously. To address this question, we apply a mutual
choice sequential search problem in an evolutionary game-theoretical model that
allows one to find solutions that are favored by evolution. As an example, we
study the influence of sequential search on the evolutionary dynamics of cooperation.
For this, we focus on the classic snowdrift game and the prisoner’s dilemma game.
article_processing_charge: No
article_type: original
author:
- first_name: Tadeas
full_name: Priklopil, Tadeas
id: 3C869AA0-F248-11E8-B48F-1D18A9856A87
last_name: Priklopil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Priklopil T, Chatterjee K. Evolution of decisions in population games with
sequentially searching individuals. Games. 2015;6(4):413-437. doi:10.3390/g6040413
apa: Priklopil, T., & Chatterjee, K. (2015). Evolution of decisions in population
games with sequentially searching individuals. Games. MDPI. https://doi.org/10.3390/g6040413
chicago: Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in
Population Games with Sequentially Searching Individuals.” Games. MDPI,
2015. https://doi.org/10.3390/g6040413.
ieee: T. Priklopil and K. Chatterjee, “Evolution of decisions in population games
with sequentially searching individuals,” Games, vol. 6, no. 4. MDPI, pp.
413–437, 2015.
ista: Priklopil T, Chatterjee K. 2015. Evolution of decisions in population games
with sequentially searching individuals. Games. 6(4), 413–437.
mla: Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population
Games with Sequentially Searching Individuals.” Games, vol. 6, no. 4, MDPI,
2015, pp. 413–37, doi:10.3390/g6040413.
short: T. Priklopil, K. Chatterjee, Games 6 (2015) 413–437.
date_created: 2018-12-11T11:53:26Z
date_published: 2015-09-29T00:00:00Z
date_updated: 2023-10-17T11:42:52Z
day: '29'
ddc:
- '000'
department:
- _id: NiBa
- _id: KrCh
doi: 10.3390/g6040413
ec_funded: 1
file:
- access_level: open_access
checksum: 912e1acbaf201100f447a43e4d5958bd
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:41Z
date_updated: 2020-07-14T12:45:12Z
file_id: '4959'
file_name: IST-2016-448-v1+1_games-06-00413.pdf
file_size: 518832
relation: main_file
file_date_updated: 2020-07-14T12:45:12Z
has_accepted_license: '1'
intvolume: ' 6'
issue: '4'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 413 - 437
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Games
publication_identifier:
eissn:
- 2073-4336
publication_status: published
publisher: MDPI
publist_id: '5467'
pubrep_id: '448'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Evolution of decisions in population games with sequentially searching individuals
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: 6
year: '2015'
...
---
_id: '1682'
abstract:
- lang: eng
text: 'We study the problem of robust satisfiability of systems of nonlinear equations,
namely, whether for a given continuous function f:K→ ℝn on a finite simplicial
complex K and α > 0, it holds that each function g: K → ℝn such that ||g -
f || ∞ < α, has a root in K. Via a reduction to the extension problem of maps
into a sphere, we particularly show that this problem is decidable in polynomial
time for every fixed n, assuming dimK ≤ 2n - 3. This is a substantial extension
of previous computational applications of topological degree and related concepts
in numerical and interval analysis. Via a reverse reduction, we prove that the
problem is undecidable when dim K > 2n - 2, where the threshold comes from
the stable range in homotopy theory. For the lucidity of our exposition, we focus
on the setting when f is simplexwise linear. Such functions can approximate general
continuous functions, and thus we get approximation schemes and undecidability
of the robust satisfiability in other possible settings.'
article_number: '26'
author:
- first_name: Peter
full_name: Franek, Peter
last_name: Franek
- first_name: Marek
full_name: Krcál, Marek
id: 33E21118-F248-11E8-B48F-1D18A9856A87
last_name: Krcál
citation:
ama: Franek P, Krcál M. Robust satisfiability of systems of equations. Journal
of the ACM. 2015;62(4). doi:10.1145/2751524
apa: Franek, P., & Krcál, M. (2015). Robust satisfiability of systems of equations.
Journal of the ACM. ACM. https://doi.org/10.1145/2751524
chicago: Franek, Peter, and Marek Krcál. “Robust Satisfiability of Systems of Equations.”
Journal of the ACM. ACM, 2015. https://doi.org/10.1145/2751524.
ieee: P. Franek and M. Krcál, “Robust satisfiability of systems of equations,” Journal
of the ACM, vol. 62, no. 4. ACM, 2015.
ista: Franek P, Krcál M. 2015. Robust satisfiability of systems of equations. Journal
of the ACM. 62(4), 26.
mla: Franek, Peter, and Marek Krcál. “Robust Satisfiability of Systems of Equations.”
Journal of the ACM, vol. 62, no. 4, 26, ACM, 2015, doi:10.1145/2751524.
short: P. Franek, M. Krcál, Journal of the ACM 62 (2015).
date_created: 2018-12-11T11:53:27Z
date_published: 2015-08-01T00:00:00Z
date_updated: 2021-01-12T06:52:30Z
day: '01'
department:
- _id: UlWa
- _id: HeEd
doi: 10.1145/2751524
intvolume: ' 62'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1402.0858
month: '08'
oa: 1
oa_version: Preprint
publication: Journal of the ACM
publication_status: published
publisher: ACM
publist_id: '5466'
quality_controlled: '1'
scopus_import: 1
status: public
title: Robust satisfiability of systems of equations
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 62
year: '2015'
...
---
_id: '1683'
abstract:
- lang: eng
text: The 1 MDa, 45-subunit proton-pumping NADH-ubiquinone oxidoreductase (complex
I) is the largest complex of the mitochondrial electron transport chain. The molecular
mechanism of complex I is central to the metabolism of cells, but has yet to be
fully characterized. The last two years have seen steady progress towards this
goal with the first atomic-resolution structure of the entire bacterial complex
I, a 5 Å cryo-electron microscopy map of bovine mitochondrial complex I and a
∼3.8 Å resolution X-ray crystallographic study of mitochondrial complex I from
yeast Yarrowia lipotytica. In this review we will discuss what we have learned
from these studies and what remains to be elucidated.
author:
- first_name: Jame A
full_name: Letts, Jame A
id: 322DA418-F248-11E8-B48F-1D18A9856A87
last_name: Letts
orcid: 0000-0002-9864-3586
- first_name: Leonid A
full_name: Sazanov, Leonid A
id: 338D39FE-F248-11E8-B48F-1D18A9856A87
last_name: Sazanov
orcid: 0000-0002-0977-7989
citation:
ama: 'Letts JA, Sazanov LA. Gaining mass: The structure of respiratory complex I-from
bacterial towards mitochondrial versions. Current Opinion in Structural Biology.
2015;33(8):135-145. doi:10.1016/j.sbi.2015.08.008'
apa: 'Letts, J. A., & Sazanov, L. A. (2015). Gaining mass: The structure of
respiratory complex I-from bacterial towards mitochondrial versions. Current
Opinion in Structural Biology. Elsevier. https://doi.org/10.1016/j.sbi.2015.08.008'
chicago: 'Letts, James A, and Leonid A Sazanov. “Gaining Mass: The Structure of
Respiratory Complex I-from Bacterial towards Mitochondrial Versions.” Current
Opinion in Structural Biology. Elsevier, 2015. https://doi.org/10.1016/j.sbi.2015.08.008.'
ieee: 'J. A. Letts and L. A. Sazanov, “Gaining mass: The structure of respiratory
complex I-from bacterial towards mitochondrial versions,” Current Opinion in
Structural Biology, vol. 33, no. 8. Elsevier, pp. 135–145, 2015.'
ista: 'Letts JA, Sazanov LA. 2015. Gaining mass: The structure of respiratory complex
I-from bacterial towards mitochondrial versions. Current Opinion in Structural
Biology. 33(8), 135–145.'
mla: 'Letts, James A., and Leonid A. Sazanov. “Gaining Mass: The Structure of Respiratory
Complex I-from Bacterial towards Mitochondrial Versions.” Current Opinion in
Structural Biology, vol. 33, no. 8, Elsevier, 2015, pp. 135–45, doi:10.1016/j.sbi.2015.08.008.'
short: J.A. Letts, L.A. Sazanov, Current Opinion in Structural Biology 33 (2015)
135–145.
date_created: 2018-12-11T11:53:27Z
date_published: 2015-08-01T00:00:00Z
date_updated: 2021-01-12T06:52:30Z
day: '01'
department:
- _id: LeSa
doi: 10.1016/j.sbi.2015.08.008
intvolume: ' 33'
issue: '8'
language:
- iso: eng
month: '08'
oa_version: None
page: 135 - 145
publication: Current Opinion in Structural Biology
publication_status: published
publisher: Elsevier
publist_id: '5465'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Gaining mass: The structure of respiratory complex I-from bacterial towards
mitochondrial versions'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 33
year: '2015'
...
---
_id: '1685'
abstract:
- lang: eng
text: "Given a graph G cellularly embedded on a surface Σ of genus g, a cut graph
is a subgraph of G such that cutting Σ along G yields a topological disk. We provide
a fixed parameter tractable approximation scheme for the problem of computing
the shortest cut graph, that is, for any ε > 0, we show how to compute a (1 + ε)
approximation of the shortest cut graph in time f(ε, g)n3.\r\nOur techniques first
rely on the computation of a spanner for the problem using the technique of brick
decompositions, to reduce the problem to the case of bounded tree-width. Then,
to solve the bounded tree-width case, we introduce a variant of the surface-cut
decomposition of Rué, Sau and Thilikos, which may be of independent interest."
alternative_title:
- LNCS
author:
- first_name: Vincent
full_name: Cohen Addad, Vincent
last_name: Cohen Addad
- first_name: Arnaud N
full_name: De Mesmay, Arnaud N
id: 3DB2F25C-F248-11E8-B48F-1D18A9856A87
last_name: De Mesmay
citation:
ama: 'Cohen Addad V, de Mesmay AN. A fixed parameter tractable approximation scheme
for the optimal cut graph of a surface. In: Vol 9294. Springer; 2015:386-398.
doi:10.1007/978-3-662-48350-3_33'
apa: 'Cohen Addad, V., & de Mesmay, A. N. (2015). A fixed parameter tractable
approximation scheme for the optimal cut graph of a surface (Vol. 9294, pp. 386–398).
Presented at the ESA: European Symposium on Algorithms, Patras, Greece: Springer.
https://doi.org/10.1007/978-3-662-48350-3_33'
chicago: Cohen Addad, Vincent, and Arnaud N de Mesmay. “A Fixed Parameter Tractable
Approximation Scheme for the Optimal Cut Graph of a Surface,” 9294:386–98. Springer,
2015. https://doi.org/10.1007/978-3-662-48350-3_33.
ieee: 'V. Cohen Addad and A. N. de Mesmay, “A fixed parameter tractable approximation
scheme for the optimal cut graph of a surface,” presented at the ESA: European
Symposium on Algorithms, Patras, Greece, 2015, vol. 9294, pp. 386–398.'
ista: 'Cohen Addad V, de Mesmay AN. 2015. A fixed parameter tractable approximation
scheme for the optimal cut graph of a surface. ESA: European Symposium on Algorithms,
LNCS, vol. 9294, 386–398.'
mla: Cohen Addad, Vincent, and Arnaud N. de Mesmay. A Fixed Parameter Tractable
Approximation Scheme for the Optimal Cut Graph of a Surface. Vol. 9294, Springer,
2015, pp. 386–98, doi:10.1007/978-3-662-48350-3_33.
short: V. Cohen Addad, A.N. de Mesmay, in:, Springer, 2015, pp. 386–398.
conference:
end_date: 2015-09-16
location: Patras, Greece
name: 'ESA: European Symposium on Algorithms'
start_date: 2015-09-14
date_created: 2018-12-11T11:53:27Z
date_published: 2015-09-01T00:00:00Z
date_updated: 2021-01-12T06:52:31Z
day: '01'
department:
- _id: UlWa
doi: 10.1007/978-3-662-48350-3_33
ec_funded: 1
intvolume: ' 9294'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1507.01688
month: '09'
oa: 1
oa_version: Preprint
page: 386 - 398
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5462'
quality_controlled: '1'
scopus_import: 1
status: public
title: A fixed parameter tractable approximation scheme for the optimal cut graph
of a surface
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9294
year: '2015'
...
---
_id: '1686'
author:
- first_name: Eva
full_name: Kiermaier, Eva
id: 3EB04B78-F248-11E8-B48F-1D18A9856A87
last_name: Kiermaier
orcid: 0000-0001-6165-5738
- first_name: Michael K
full_name: Sixt, Michael K
id: 41E9FBEA-F248-11E8-B48F-1D18A9856A87
last_name: Sixt
orcid: 0000-0002-6620-9179
citation:
ama: 'Kiermaier E, Sixt MK. Fragmented communication between immune cells: Neutrophils
blaze a trail with migratory cues for T cells to follow to sites of infection.
Science. 2015;349(6252):1055-1056. doi:10.1126/science.aad0867'
apa: 'Kiermaier, E., & Sixt, M. K. (2015). Fragmented communication between
immune cells: Neutrophils blaze a trail with migratory cues for T cells to follow
to sites of infection. Science. American Association for the Advancement
of Science. https://doi.org/10.1126/science.aad0867'
chicago: 'Kiermaier, Eva, and Michael K Sixt. “Fragmented Communication between
Immune Cells: Neutrophils Blaze a Trail with Migratory Cues for T Cells to Follow
to Sites of Infection.” Science. American Association for the Advancement
of Science, 2015. https://doi.org/10.1126/science.aad0867.'
ieee: 'E. Kiermaier and M. K. Sixt, “Fragmented communication between immune cells:
Neutrophils blaze a trail with migratory cues for T cells to follow to sites of
infection,” Science, vol. 349, no. 6252. American Association for the Advancement
of Science, pp. 1055–1056, 2015.'
ista: 'Kiermaier E, Sixt MK. 2015. Fragmented communication between immune cells:
Neutrophils blaze a trail with migratory cues for T cells to follow to sites of
infection. Science. 349(6252), 1055–1056.'
mla: 'Kiermaier, Eva, and Michael K. Sixt. “Fragmented Communication between Immune
Cells: Neutrophils Blaze a Trail with Migratory Cues for T Cells to Follow to
Sites of Infection.” Science, vol. 349, no. 6252, American Association
for the Advancement of Science, 2015, pp. 1055–56, doi:10.1126/science.aad0867.'
short: E. Kiermaier, M.K. Sixt, Science 349 (2015) 1055–1056.
date_created: 2018-12-11T11:53:28Z
date_published: 2015-09-04T00:00:00Z
date_updated: 2021-01-12T06:52:31Z
day: '04'
department:
- _id: MiSi
doi: 10.1126/science.aad0867
intvolume: ' 349'
issue: '6252'
language:
- iso: eng
month: '09'
oa_version: None
page: 1055 - 1056
publication: Science
publication_status: published
publisher: American Association for the Advancement of Science
publist_id: '5459'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Fragmented communication between immune cells: Neutrophils blaze a trail with
migratory cues for T cells to follow to sites of infection'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 349
year: '2015'
...
---
_id: '1687'
abstract:
- lang: eng
text: Guided cell movement is essential for development and integrity of animals
and crucially involved in cellular immune responses. Leukocytes are professional
migratory cells that can navigate through most types of tissues and sense a wide
range of directional cues. The responses of these cells to attractants have been
mainly explored in tissue culture settings. How leukocytes make directional decisions
in situ, within the challenging environment of a tissue maze, is less understood.
Here we review recent advances in how leukocytes sense chemical cues in complex
tissue settings and make links with paradigms of directed migration in development
and Dictyostelium discoideum amoebae.
author:
- first_name: Milka
full_name: Sarris, Milka
last_name: Sarris
- first_name: Michael K
full_name: Sixt, Michael K
id: 41E9FBEA-F248-11E8-B48F-1D18A9856A87
last_name: Sixt
orcid: 0000-0002-6620-9179
citation:
ama: 'Sarris M, Sixt MK. Navigating in tissue mazes: Chemoattractant interpretation
in complex environments. Current Opinion in Cell Biology. 2015;36(10):93-102.
doi:10.1016/j.ceb.2015.08.001'
apa: 'Sarris, M., & Sixt, M. K. (2015). Navigating in tissue mazes: Chemoattractant
interpretation in complex environments. Current Opinion in Cell Biology.
Elsevier. https://doi.org/10.1016/j.ceb.2015.08.001'
chicago: 'Sarris, Milka, and Michael K Sixt. “Navigating in Tissue Mazes: Chemoattractant
Interpretation in Complex Environments.” Current Opinion in Cell Biology.
Elsevier, 2015. https://doi.org/10.1016/j.ceb.2015.08.001.'
ieee: 'M. Sarris and M. K. Sixt, “Navigating in tissue mazes: Chemoattractant interpretation
in complex environments,” Current Opinion in Cell Biology, vol. 36, no.
10. Elsevier, pp. 93–102, 2015.'
ista: 'Sarris M, Sixt MK. 2015. Navigating in tissue mazes: Chemoattractant interpretation
in complex environments. Current Opinion in Cell Biology. 36(10), 93–102.'
mla: 'Sarris, Milka, and Michael K. Sixt. “Navigating in Tissue Mazes: Chemoattractant
Interpretation in Complex Environments.” Current Opinion in Cell Biology,
vol. 36, no. 10, Elsevier, 2015, pp. 93–102, doi:10.1016/j.ceb.2015.08.001.'
short: M. Sarris, M.K. Sixt, Current Opinion in Cell Biology 36 (2015) 93–102.
date_created: 2018-12-11T11:53:28Z
date_published: 2015-10-01T00:00:00Z
date_updated: 2021-01-12T06:52:31Z
day: '01'
ddc:
- '570'
department:
- _id: MiSi
doi: 10.1016/j.ceb.2015.08.001
ec_funded: 1
file:
- access_level: open_access
checksum: c29973924b790aab02fdd91857759cfb
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:21Z
date_updated: 2020-07-14T12:45:12Z
file_id: '4875'
file_name: IST-2016-445-v1+1_1-s2.0-S0955067415001064-main.pdf
file_size: 797964
relation: main_file
file_date_updated: 2020-07-14T12:45:12Z
has_accepted_license: '1'
intvolume: ' 36'
issue: '10'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 93 - 102
project:
- _id: 25A603A2-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '281556'
name: Cytoskeletal force generation and force transduction of migrating leukocytes
(EU)
publication: Current Opinion in Cell Biology
publication_status: published
publisher: Elsevier
publist_id: '5458'
pubrep_id: '445'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Navigating in tissue mazes: Chemoattractant interpretation in complex environments'
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: 36
year: '2015'
...
---
_id: '1688'
abstract:
- lang: eng
text: 'We estimate the selection constant in the following geometric selection theorem
by Pach: For every positive integer d, there is a constant (Formula presented.)
such that whenever (Formula presented.) are n-element subsets of (Formula presented.),
we can find a point (Formula presented.) and subsets (Formula presented.) for
every i∈[d+1], each of size at least cdn, such that p belongs to all rainbowd-simplices
determined by (Formula presented.) simplices with one vertex in each Yi. We show
a super-exponentially decreasing upper bound (Formula presented.). The ideas used
in the proof of the upper bound also help us to prove Pach’s theorem with (Formula
presented.), which is a lower bound doubly exponentially decreasing in d (up to
some polynomial in the exponent). For comparison, Pach’s original approach yields
a triply exponentially decreasing lower bound. On the other hand, Fox, Pach, and
Suk recently obtained a hypergraph density result implying a proof of Pach’s theorem
with (Formula presented.). In our construction for the upper bound, we use the
fact that the minimum solid angle of every d-simplex is super-exponentially small.
This fact was previously unknown and might be of independent interest. For the
lower bound, we improve the ‘separation’ part of the argument by showing that
in one of the key steps only d+1 separations are necessary, compared to 2d separations
in the original proof. We also provide a measure version of Pach’s theorem.'
acknowledgement: R. K. was supported by the Russian Foundation for Basic Research
Grant 15-31-20403 (mol_a_ved) and grant 15-01-99563. J. K., Z. P., and M. T. were
partially supported by ERC Advanced Research Grant No. 267165 (DISCONV) and by the
project CE-ITI (GAČR P202/12/G061) of the Czech Science Foundation. J. K. was also
partially supported by Swiss National Science Foundation Grants 200021-137574 and
200020-14453. P. P., Z. P., and M. T. were partially supported by the Charles University
Grant GAUK 421511. P. P. was also partially supported by the Charles University
Grant SVV-2014-260107. Z. P. was also partially supported by the Charles University
Grant SVV-2014-260103.
author:
- first_name: Roman
full_name: Karasev, Roman
last_name: Karasev
- first_name: Jan
full_name: Kynčl, Jan
last_name: Kynčl
- first_name: Pavel
full_name: Paták, Pavel
last_name: Paták
- first_name: Zuzana
full_name: Patakova, Zuzana
last_name: Patakova
orcid: 0000-0002-3975-1683
- first_name: Martin
full_name: Tancer, Martin
id: 38AC689C-F248-11E8-B48F-1D18A9856A87
last_name: Tancer
orcid: 0000-0002-1191-6714
citation:
ama: Karasev R, Kynčl J, Paták P, Patakova Z, Tancer M. Bounds for Pach’s selection
theorem and for the minimum solid angle in a simplex. Discrete & Computational
Geometry. 2015;54(3):610-636. doi:10.1007/s00454-015-9720-z
apa: Karasev, R., Kynčl, J., Paták, P., Patakova, Z., & Tancer, M. (2015). Bounds
for Pach’s selection theorem and for the minimum solid angle in a simplex. Discrete
& Computational Geometry. Springer. https://doi.org/10.1007/s00454-015-9720-z
chicago: Karasev, Roman, Jan Kynčl, Pavel Paták, Zuzana Patakova, and Martin Tancer.
“Bounds for Pach’s Selection Theorem and for the Minimum Solid Angle in a Simplex.”
Discrete & Computational Geometry. Springer, 2015. https://doi.org/10.1007/s00454-015-9720-z.
ieee: R. Karasev, J. Kynčl, P. Paták, Z. Patakova, and M. Tancer, “Bounds for Pach’s
selection theorem and for the minimum solid angle in a simplex,” Discrete &
Computational Geometry, vol. 54, no. 3. Springer, pp. 610–636, 2015.
ista: Karasev R, Kynčl J, Paták P, Patakova Z, Tancer M. 2015. Bounds for Pach’s
selection theorem and for the minimum solid angle in a simplex. Discrete &
Computational Geometry. 54(3), 610–636.
mla: Karasev, Roman, et al. “Bounds for Pach’s Selection Theorem and for the Minimum
Solid Angle in a Simplex.” Discrete & Computational Geometry, vol.
54, no. 3, Springer, 2015, pp. 610–36, doi:10.1007/s00454-015-9720-z.
short: R. Karasev, J. Kynčl, P. Paták, Z. Patakova, M. Tancer, Discrete & Computational
Geometry 54 (2015) 610–636.
date_created: 2018-12-11T11:53:28Z
date_published: 2015-10-01T00:00:00Z
date_updated: 2021-01-12T06:52:32Z
day: '01'
department:
- _id: UlWa
doi: 10.1007/s00454-015-9720-z
intvolume: ' 54'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1403.8147
month: '10'
oa: 1
oa_version: Preprint
page: 610 - 636
publication: Discrete & Computational Geometry
publication_status: published
publisher: Springer
publist_id: '5457'
quality_controlled: '1'
scopus_import: 1
status: public
title: Bounds for Pach's selection theorem and for the minimum solid angle in a simplex
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 54
year: '2015'
...
---
_id: '1689'
abstract:
- lang: eng
text: We consider the problem of computing the set of initial states of a dynamical
system such that there exists a control strategy to ensure that the trajectories
satisfy a temporal logic specification with probability 1 (almost-surely). We
focus on discrete-time, stochastic linear dynamics and specifications given as
formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over
linear predicates in the states of the system. We propose a solution based on
iterative abstraction-refinement, and turn-based 2-player probabilistic games.
While the theoretical guarantee of our algorithm after any finite number of iterations
is only a partial solution, we show that if our algorithm terminates, then the
result is the set of satisfying initial states. Moreover, for any (partial) solution
our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction
of the temporal logic specification. We demonstrate our approach on an illustrative
case study.
author:
- first_name: Mária
full_name: Svoreňová, Mária
last_name: Svoreňová
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ivana
full_name: Cěrná, Ivana
last_name: Cěrná
- first_name: Cǎlin
full_name: Belta, Cǎlin
last_name: Belta
citation:
ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal
logic control for stochastic linear systems using abstraction refinement of probabilistic
games. In: Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control. ACM; 2015:259-268. doi:10.1145/2728606.2728608'
apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &
Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction
refinement of probabilistic games. In Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control (pp. 259–268). Seattle,
WA, United States: ACM. https://doi.org/10.1145/2728606.2728608'
chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee,
Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” In Proceedings of the
18th International Conference on Hybrid Systems: Computation and Control,
259–68. ACM, 2015. https://doi.org/10.1145/2728606.2728608.'
ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta,
“Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games,” in Proceedings of the 18th International Conference
on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015,
pp. 259–268.'
ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015.
Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games. Proceedings of the 18th International Conference on Hybrid
Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control,
259–268.'
mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” Proceedings of the 18th
International Conference on Hybrid Systems: Computation and Control, ACM,
2015, pp. 259–68, doi:10.1145/2728606.2728608.'
short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta,
in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation
and Control, ACM, 2015, pp. 259–268.'
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:29Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2023-09-20T09:43:09Z
day: '14'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2728606.2728608
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1410.5387
month: '04'
oa: 1
oa_version: Preprint
page: 259 - 268
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _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
publication: 'Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control'
publication_status: published
publisher: ACM
publist_id: '5456'
related_material:
record:
- id: '1407'
relation: later_version
status: public
scopus_import: 1
status: public
title: Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1690'
abstract:
- lang: eng
text: A number of powerful and scalable hybrid systems model checkers have recently
emerged. Although all of them honor roughly the same hybrid systems semantics,
they have drastically different model description languages. This situation (a)
makes it difficult to quickly evaluate a specific hybrid automaton model using
the different tools, (b) obstructs comparisons of reachability approaches, and
(c) impedes the widespread application of research results that perform model
modification and could benefit many of the tools. In this paper, we present Hyst,
a Hybrid Source Transformer. Hyst is a source-to-source translation tool, currently
taking input in the SpaceEx model format, and translating to the formats of HyCreate,
Flow∗, or dReach. Internally, the tool supports generic model-to-model transformation
passes that serve to both ease the translation and potentially improve reachability
results for the supported tools. Although these model transformation passes could
be implemented within each tool, the Hyst approach provides a single place for
model modification, generating modified input sources for the unmodified target
tools. Our evaluation demonstrates Hyst is capable of automatically translating
benchmarks in several classes (including affine and nonlinear hybrid automata)
to the input formats of several tools. Additionally, we illustrate a general model
transformation pass based on pseudo-invariants implemented in Hyst that illustrates
the reachability improvement.
acknowledgement: The material presented in this paper is based upon work sup-ported
by the Air Force Research Laboratory’s Information Directorate (AFRL/RI) through
the Visiting Faculty Research Program (VFRP) under contract number FA8750-13-2-0115
and the Air Force Office of Scientific Research (AFOSR). Any opinions,findings,
and conclusions or recommendations expressed in this publication are those of the
authors and do not necessarily reflect the views of the AFRL/RI or AFOSR. This work
was also partly supported in part by the German Research Foundation (DFG) as part
of the Transregional Collaborative Research Center “Automatic Verification and Analysis
of Complex Systems” (SFB/TR14 AVACS, http://www.avacs.org/), by the European Research
Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF)
under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).
author:
- first_name: Stanley
full_name: Bak, Stanley
last_name: Bak
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
citation:
ama: 'Bak S, Bogomolov S, Johnson T. HYST: A source transformation and translation
tool for hybrid automaton models. In: Springer; 2015:128-133. doi:10.1145/2728606.2728630'
apa: 'Bak, S., Bogomolov, S., & Johnson, T. (2015). HYST: A source transformation
and translation tool for hybrid automaton models (pp. 128–133). Presented at the
HSCC: Hybrid Systems - Computation and Control, Seattle, WA, United States: Springer.
https://doi.org/10.1145/2728606.2728630'
chicago: 'Bak, Stanley, Sergiy Bogomolov, and Taylor Johnson. “HYST: A Source Transformation
and Translation Tool for Hybrid Automaton Models,” 128–33. Springer, 2015. https://doi.org/10.1145/2728606.2728630.'
ieee: 'S. Bak, S. Bogomolov, and T. Johnson, “HYST: A source transformation and
translation tool for hybrid automaton models,” presented at the HSCC: Hybrid Systems
- Computation and Control, Seattle, WA, United States, 2015, pp. 128–133.'
ista: 'Bak S, Bogomolov S, Johnson T. 2015. HYST: A source transformation and translation
tool for hybrid automaton models. HSCC: Hybrid Systems - Computation and Control,
128–133.'
mla: 'Bak, Stanley, et al. HYST: A Source Transformation and Translation Tool
for Hybrid Automaton Models. Springer, 2015, pp. 128–33, doi:10.1145/2728606.2728630.'
short: S. Bak, S. Bogomolov, T. Johnson, in:, Springer, 2015, pp. 128–133.
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:29Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2021-01-12T06:52:33Z
day: '14'
department:
- _id: ToHe
doi: 10.1145/2728606.2728630
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 128 - 133
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '5454'
quality_controlled: '1'
status: public
title: 'HYST: A source transformation and translation tool for hybrid automaton models'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...