---
_id: '10865'
abstract:
- lang: eng
text: "We introduce the notion of Witness Maps as a cryptographic notion of a proof
system. A Unique Witness Map (UWM) deterministically maps all witnesses for an
\ NP statement to a single representative witness, resulting in a computationally
sound, deterministic-prover, non-interactive witness independent proof system.
A relaxation of UWM, called Compact Witness Map (CWM), maps all the witnesses
to a small number of witnesses, resulting in a “lossy” deterministic-prover, non-interactive
proof-system. We also define a Dual Mode Witness Map (DMWM) which adds an “extractable”
mode to a CWM.\r\nOur main construction is a DMWM for all NP relations, assuming
sub-exponentially secure indistinguishability obfuscation ( iO ), along with
standard cryptographic assumptions. The DMWM construction relies on a CWM and
a new primitive called Cumulative All-Lossy-But-One Trapdoor Functions (C-ALBO-TDF),
both of which are in turn instantiated based on iO and other primitives. Our
instantiation of a CWM is in fact a UWM; in turn, we show that a UWM implies Witness
Encryption. Along the way to constructing UWM and C-ALBO-TDF, we also construct,
from standard assumptions, Puncturable Digital Signatures and a new primitive
called Cumulative Lossy Trapdoor Functions (C-LTDF). The former improves up on
a construction of Bellare et al. (Eurocrypt 2016), who relied on sub-exponentially
secure iO and sub-exponentially secure OWF.\r\nAs an application of our constructions,
we show how to use a DMWM to construct the first leakage and tamper-resilient
signatures with a deterministic signer, thereby solving a decade old open problem
posed by Katz and Vaikunthanathan (Asiacrypt 2009), by Boyle, Segev and Wichs
(Eurocrypt 2011), as well as by Faonio and Venturi (Asiacrypt 2016). Our construction
achieves the optimal leakage rate of 1−o(1) ."
acknowledgement: We would like to thank the anonymous reviewers of PKC 2019 for their
useful comments and suggestions. We thank Omer Paneth for pointing out to us the
connection between Unique Witness Maps (UWM) and Witness encryption (WE). The first
author would like to acknowledge Pandu Rangan for his involvement during the initial
discussion phase of the project.
article_processing_charge: No
author:
- first_name: Suvradip
full_name: Chakraborty, Suvradip
id: B9CD0494-D033-11E9-B219-A439E6697425
last_name: Chakraborty
- first_name: Manoj
full_name: Prabhakaran, Manoj
last_name: Prabhakaran
- first_name: Daniel
full_name: Wichs, Daniel
last_name: Wichs
citation:
ama: 'Chakraborty S, Prabhakaran M, Wichs D. Witness maps and applications. In:
Kiayias A, ed. Public-Key Cryptography. Vol 12110. LNCS. Cham: Springer
Nature; 2020:220-246. doi:10.1007/978-3-030-45374-9_8'
apa: 'Chakraborty, S., Prabhakaran, M., & Wichs, D. (2020). Witness maps and
applications. In A. Kiayias (Ed.), Public-Key Cryptography (Vol. 12110,
pp. 220–246). Cham: Springer Nature. https://doi.org/10.1007/978-3-030-45374-9_8'
chicago: 'Chakraborty, Suvradip, Manoj Prabhakaran, and Daniel Wichs. “Witness Maps
and Applications.” In Public-Key Cryptography, edited by A Kiayias, 12110:220–46.
LNCS. Cham: Springer Nature, 2020. https://doi.org/10.1007/978-3-030-45374-9_8.'
ieee: 'S. Chakraborty, M. Prabhakaran, and D. Wichs, “Witness maps and applications,”
in Public-Key Cryptography, vol. 12110, A. Kiayias, Ed. Cham: Springer
Nature, 2020, pp. 220–246.'
ista: 'Chakraborty S, Prabhakaran M, Wichs D. 2020.Witness maps and applications.
In: Public-Key Cryptography. vol. 12110, 220–246.'
mla: Chakraborty, Suvradip, et al. “Witness Maps and Applications.” Public-Key
Cryptography, edited by A Kiayias, vol. 12110, Springer Nature, 2020, pp.
220–46, doi:10.1007/978-3-030-45374-9_8.
short: S. Chakraborty, M. Prabhakaran, D. Wichs, in:, A. Kiayias (Ed.), Public-Key
Cryptography, Springer Nature, Cham, 2020, pp. 220–246.
corr_author: '1'
date_created: 2022-03-18T11:35:51Z
date_published: 2020-04-29T00:00:00Z
date_updated: 2026-04-16T10:21:31Z
day: '29'
doi: 10.1007/978-3-030-45374-9_8
editor:
- first_name: A
full_name: Kiayias, A
last_name: Kiayias
external_id:
isi:
- '001299210200008'
intvolume: ' 12110'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2020/090
month: '04'
oa: 1
oa_version: Preprint
page: 220-246
place: Cham
publication: Public-Key Cryptography
publication_identifier:
eisbn:
- '9783030453749'
eissn:
- 1611-3349
isbn:
- '9783030453732'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Witness maps and applications
type: book_chapter
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 12110
year: '2020'
...
---
_id: '7810'
abstract:
- lang: eng
text: "Interprocedural data-flow analyses form an expressive and useful paradigm
of numerous static analysis applications, such as live variables analysis, alias
analysis and null pointers analysis. The most widely-used framework for interprocedural
data-flow analysis is IFDS, which encompasses distributive data-flow functions
over a finite domain. On-demand data-flow analyses restrict the focus of the analysis
on specific program locations and data facts. This setting provides a natural
split between (i) an offline (or preprocessing) phase, where the program is partially
analyzed and analysis summaries are created, and (ii) an online (or query) phase,
where analysis queries arrive on demand and the summaries are used to speed up
answering queries.\r\nIn this work, we consider on-demand IFDS analyses where
the queries concern program locations of the same procedure (aka same-context
queries). We exploit the fact that flow graphs of programs have low treewidth
to develop faster algorithms that are space and time optimal for many common data-flow
analyses, in both the preprocessing and the query phase. We also use treewidth
to develop query solutions that are embarrassingly parallelizable, i.e. the total
work for answering each query is split to a number of threads such that each thread
performs only a constant amount of work. Finally, we implement a static analyzer
based on our algorithms, and perform a series of on-demand analysis experiments
on standard benchmarks. Our experimental results show a drastic speed-up of the
queries after only a lightweight preprocessing phase, which significantly outperforms
existing techniques."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 'Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Optimal and perfectly
parallel algorithms for on-demand data-flow analysis. In: European Symposium
on Programming. Vol 12075. Springer Nature; 2020:112-140. doi:10.1007/978-3-030-44914-8_5'
apa: 'Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Pavlogiannis, A.
(2020). Optimal and perfectly parallel algorithms for on-demand data-flow analysis.
In European Symposium on Programming (Vol. 12075, pp. 112–140). Dublin,
Ireland: Springer Nature. https://doi.org/10.1007/978-3-030-44914-8_5'
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen,
and Andreas Pavlogiannis. “Optimal and Perfectly Parallel Algorithms for On-Demand
Data-Flow Analysis.” In European Symposium on Programming, 12075:112–40.
Springer Nature, 2020. https://doi.org/10.1007/978-3-030-44914-8_5.
ieee: K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal
and perfectly parallel algorithms for on-demand data-flow analysis,” in European
Symposium on Programming, Dublin, Ireland, 2020, vol. 12075, pp. 112–140.
ista: 'Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2020. Optimal
and perfectly parallel algorithms for on-demand data-flow analysis. European Symposium
on Programming. ESOP: Programming Languages and Systems, LNCS, vol. 12075, 112–140.'
mla: Chatterjee, Krishnendu, et al. “Optimal and Perfectly Parallel Algorithms for
On-Demand Data-Flow Analysis.” European Symposium on Programming, vol.
12075, Springer Nature, 2020, pp. 112–40, doi:10.1007/978-3-030-44914-8_5.
short: K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, European
Symposium on Programming, Springer Nature, 2020, pp. 112–140.
conference:
end_date: 2020-04-30
location: Dublin, Ireland
name: 'ESOP: Programming Languages and Systems'
start_date: 2020-04-25
corr_author: '1'
date_created: 2020-05-10T22:00:50Z
date_published: 2020-04-18T00:00:00Z
date_updated: 2026-05-31T22:31:17Z
day: '18'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-030-44914-8_5
external_id:
isi:
- '000681656800005'
file:
- access_level: open_access
checksum: 8618b80f4cf7b39a60e61a6445ad9807
content_type: application/pdf
creator: dernst
date_created: 2020-05-26T13:34:48Z
date_updated: 2020-07-14T12:48:03Z
file_id: '7895'
file_name: 2020_LNCS_Chatterjee.pdf
file_size: 651250
relation: main_file
file_date_updated: 2020-07-14T12:48:03Z
has_accepted_license: '1'
intvolume: ' 12075'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 112-140
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 266EEEC0-B435-11E9-9278-68D0E5697425
name: Quantitative Game-theoretic Analysis of Blockchain Applications and Smart
Contracts
- _id: 267066CE-B435-11E9-9278-68D0E5697425
name: Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies
publication: European Symposium on Programming
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030449131'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Optimal and perfectly parallel algorithms for on-demand data-flow analysis
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: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 12075
year: '2020'
...
---
_id: '8728'
abstract:
- lang: eng
text: Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are
two standard formalisms in system analysis. Their main associated quantitative
objectives are hitting probabilities, discounted sum, and mean payoff. Although
there are many techniques for computing these objectives in general MCs/MDPs,
they have not been thoroughly studied in terms of parameterized algorithms, particularly
when treewidth is used as the parameter. This is in sharp contrast to qualitative
objectives for MCs, MDPs and graph games, for which treewidth-based algorithms
yield significant complexity improvements. In this work, we show that treewidth
can also be used to obtain faster algorithms for the quantitative problems. For
an MC with n states and m transitions, we show that each of the classical quantitative
objectives can be computed in O((n+m)⋅t2) time, given a tree decomposition
of the MC with width t. Our results also imply a bound of O(κ⋅(n+m)⋅t2) for
each objective on MDPs, where κ is the number of strategy-iteration refinements
required for the given input and objective. Finally, we make an experimental evaluation
of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark
suite. Our experiments show that on low-treewidth MCs and MDPs, our algorithms
outperform existing well-established methods by one or more orders of magnitude.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ali
full_name: Asadi, Ali
last_name: Asadi
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Kiarash
full_name: Mohammadi, Kiarash
last_name: Mohammadi
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 'Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. Faster
algorithms for quantitative analysis of MCs and MDPs with small treewidth. In:
Automated Technology for Verification and Analysis. Vol 12302. Springer
Nature; 2020:253-270. doi:10.1007/978-3-030-59152-6_14'
apa: 'Asadi, A., Chatterjee, K., Goharshady, A. K., Mohammadi, K., & Pavlogiannis,
A. (2020). Faster algorithms for quantitative analysis of MCs and MDPs with small
treewidth. In Automated Technology for Verification and Analysis (Vol.
12302, pp. 253–270). Hanoi, Vietnam: Springer Nature. https://doi.org/10.1007/978-3-030-59152-6_14'
chicago: Asadi, Ali, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi,
and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Analysis of MCs
and MDPs with Small Treewidth.” In Automated Technology for Verification and
Analysis, 12302:253–70. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-59152-6_14.
ieee: A. Asadi, K. Chatterjee, A. K. Goharshady, K. Mohammadi, and A. Pavlogiannis,
“Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth,”
in Automated Technology for Verification and Analysis, Hanoi, Vietnam,
2020, vol. 12302, pp. 253–270.
ista: 'Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. 2020.
Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth.
Automated Technology for Verification and Analysis. ATVA: Automated Technology
for Verification and Analysis, LNCS, vol. 12302, 253–270.'
mla: Asadi, Ali, et al. “Faster Algorithms for Quantitative Analysis of MCs and
MDPs with Small Treewidth.” Automated Technology for Verification and Analysis,
vol. 12302, Springer Nature, 2020, pp. 253–70, doi:10.1007/978-3-030-59152-6_14.
short: A. Asadi, K. Chatterjee, A.K. Goharshady, K. Mohammadi, A. Pavlogiannis,
in:, Automated Technology for Verification and Analysis, Springer Nature, 2020,
pp. 253–270.
conference:
end_date: 2020-10-23
location: Hanoi, Vietnam
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2020-10-19
date_created: 2020-11-06T07:30:05Z
date_published: 2020-10-12T00:00:00Z
date_updated: 2026-05-31T22:31:17Z
day: '12'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-030-59152-6_14
external_id:
isi:
- '000723555700014'
file:
- access_level: open_access
checksum: ae83f27e5b189d5abc2e7514f1b7e1b5
content_type: application/pdf
creator: dernst
date_created: 2020-11-06T07:41:03Z
date_updated: 2020-11-06T07:41:03Z
file_id: '8729'
file_name: 2020_LNCS_ATVA_Asadi_accepted.pdf
file_size: 726648
relation: main_file
success: 1
file_date_updated: 2020-11-06T07:41:03Z
has_accepted_license: '1'
intvolume: ' 12302'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 253-270
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 267066CE-B435-11E9-9278-68D0E5697425
name: Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies
publication: Automated Technology for Verification and Analysis
publication_identifier:
eisbn:
- '9783030591526'
eissn:
- 1611-3349
isbn:
- '9783030591519'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 12302
year: '2020'
...
---
_id: '18269'
abstract:
- lang: eng
text: 'In the past few years, deep learning-based methods have demonstrated enormous
success for solving inverse problems in medical imaging. In this work, we address
the following question: Given a set of measurements obtained from real imaging
experiments, what is the best way to use a learnable model and the physics of
the modality to solve the inverse problem and reconstruct the latent image? Standard
supervised learning based methods approach this problem by collecting data sets
of known latent images and their corresponding measurements. However, these methods
are often impractical due to the lack of availability of appropriately sized training
sets, and, more generally, due to the inherent difficulty in measuring the “groundtruth”
latent image. In light of this, we propose a self-supervised approach to training
inverse models in medical imaging in the absence of aligned data. Our method only
requiring access to the measurements and the forward model at training. We showcase
its effectiveness on inverse problems arising in accelerated magnetic resonance
imaging (MRI). '
article_processing_charge: No
author:
- first_name: Ortal
full_name: Senouf, Ortal
last_name: Senouf
- first_name: Sanketh
full_name: Vedula, Sanketh
last_name: Vedula
- first_name: Tomer
full_name: Weiss, Tomer
last_name: Weiss
- first_name: Alexander
full_name: Bronstein, Alexander
id: 58f3726e-7cba-11ef-ad8b-e6e8cb3904e6
last_name: Bronstein
orcid: 0000-0001-9699-8730
- first_name: Oleg
full_name: Michailovich, Oleg
last_name: Michailovich
- first_name: Michael
full_name: Zibulevsky, Michael
last_name: Zibulevsky
citation:
ama: 'Senouf O, Vedula S, Weiss T, Bronstein AM, Michailovich O, Zibulevsky M. Self-supervised
learning of inverse problem solvers in medical imaging. In: First MICCAI Workshop,
DART 2019, and First International Workshop, MIL3ID 2019. Vol 11795. Springer
International Publishing; 2019:111-119. doi:10.1007/978-3-030-33391-1_13'
apa: 'Senouf, O., Vedula, S., Weiss, T., Bronstein, A. M., Michailovich, O., &
Zibulevsky, M. (2019). Self-supervised learning of inverse problem solvers in
medical imaging. In First MICCAI Workshop, DART 2019, and First International
Workshop, MIL3ID 2019 (Vol. 11795, pp. 111–119). Shenzhen, China: Springer
International Publishing. https://doi.org/10.1007/978-3-030-33391-1_13'
chicago: Senouf, Ortal, Sanketh Vedula, Tomer Weiss, Alex M. Bronstein, Oleg Michailovich,
and Michael Zibulevsky. “Self-Supervised Learning of Inverse Problem Solvers in
Medical Imaging.” In First MICCAI Workshop, DART 2019, and First International
Workshop, MIL3ID 2019, 11795:111–19. Springer International Publishing, 2019.
https://doi.org/10.1007/978-3-030-33391-1_13.
ieee: O. Senouf, S. Vedula, T. Weiss, A. M. Bronstein, O. Michailovich, and M. Zibulevsky,
“Self-supervised learning of inverse problem solvers in medical imaging,” in First
MICCAI Workshop, DART 2019, and First International Workshop, MIL3ID 2019,
Shenzhen, China, 2019, vol. 11795, pp. 111–119.
ista: 'Senouf O, Vedula S, Weiss T, Bronstein AM, Michailovich O, Zibulevsky M.
2019. Self-supervised learning of inverse problem solvers in medical imaging.
First MICCAI Workshop, DART 2019, and First International Workshop, MIL3ID 2019.
DART: MICCAI Workshop on Domain Adaptation and Representation Transfer and MIL3ID:
International Workshop on Medical Image Learning with Less Labels and Imperfect
Data vol. 11795, 111–119.'
mla: Senouf, Ortal, et al. “Self-Supervised Learning of Inverse Problem Solvers
in Medical Imaging.” First MICCAI Workshop, DART 2019, and First International
Workshop, MIL3ID 2019, vol. 11795, Springer International Publishing, 2019,
pp. 111–19, doi:10.1007/978-3-030-33391-1_13.
short: O. Senouf, S. Vedula, T. Weiss, A.M. Bronstein, O. Michailovich, M. Zibulevsky,
in:, First MICCAI Workshop, DART 2019, and First International Workshop, MIL3ID
2019, Springer International Publishing, 2019, pp. 111–119.
conference:
end_date: 2019-10-17
location: Shenzhen, China
name: 'DART: MICCAI Workshop on Domain Adaptation and Representation Transfer and
MIL3ID: International Workshop on Medical Image Learning with Less Labels and
Imperfect Data'
start_date: 2019-10-13
date_created: 2024-10-09T07:41:33Z
date_published: 2019-10-12T00:00:00Z
date_updated: 2025-01-23T14:50:36Z
day: '12'
doi: 10.1007/978-3-030-33391-1_13
extern: '1'
intvolume: ' 11795'
language:
- iso: eng
month: '10'
oa_version: None
page: 111 - 119
publication: First MICCAI Workshop, DART 2019, and First International Workshop, MIL3ID
2019
publication_identifier:
eisbn:
- '9783030333911'
eissn:
- 1611-3349
isbn:
- '9783030333904'
issn:
- 0302-9743
publication_status: published
publisher: Springer International Publishing
quality_controlled: '1'
scopus_import: '1'
status: public
title: Self-supervised learning of inverse problem solvers in medical imaging
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 11795
year: '2019'
...
---
_id: '6163'
abstract:
- lang: eng
text: We propose a new non-orthogonal basis to express the 3D Euclidean space in
terms of a regular grid. Every grid point, each represented by integer 3-coordinates,
corresponds to rhombic dodecahedron centroid. Rhombic dodecahedron is a space
filling polyhedron which represents the close packing of spheres in 3D space and
the Voronoi structures of the face centered cubic (FCC) lattice. In order to illustrate
the interest of the new coordinate system, we propose the characterization of
3D digital plane with its topological features, such as the interrelation between
the thickness of the digital plane and the separability constraint we aim to obtain.
A characterization of a 3D digital sphere with relevant topological features is
proposed as well with the help of a 48 symmetry that comes with the new coordinate
system.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ranita
full_name: Biswas, Ranita
id: 3C2B033E-F248-11E8-B48F-1D18A9856A87
last_name: Biswas
orcid: 0000-0002-5372-7890
- first_name: Gaëlle
full_name: Largeteau-Skapin, Gaëlle
last_name: Largeteau-Skapin
- first_name: Rita
full_name: Zrour, Rita
last_name: Zrour
- first_name: Eric
full_name: Andres, Eric
last_name: Andres
citation:
ama: 'Biswas R, Largeteau-Skapin G, Zrour R, Andres E. Rhombic dodecahedron grid—coordinate
system and 3D digital object definitions. In: 21st IAPR International Conference
on Discrete Geometry for Computer Imagery. Vol 11414. Berlin, Heidelberg:
Springer Berlin Heidelberg; 2019:27-37. doi:10.1007/978-3-030-14085-4_3'
apa: 'Biswas, R., Largeteau-Skapin, G., Zrour, R., & Andres, E. (2019). Rhombic
dodecahedron grid—coordinate system and 3D digital object definitions. In 21st
IAPR International Conference on Discrete Geometry for Computer Imagery (Vol.
11414, pp. 27–37). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-030-14085-4_3'
chicago: 'Biswas, Ranita, Gaëlle Largeteau-Skapin, Rita Zrour, and Eric Andres.
“Rhombic Dodecahedron Grid—Coordinate System and 3D Digital Object Definitions.”
In 21st IAPR International Conference on Discrete Geometry for Computer Imagery,
11414:27–37. Berlin, Heidelberg: Springer Berlin Heidelberg, 2019. https://doi.org/10.1007/978-3-030-14085-4_3.'
ieee: R. Biswas, G. Largeteau-Skapin, R. Zrour, and E. Andres, “Rhombic dodecahedron
grid—coordinate system and 3D digital object definitions,” in 21st IAPR International
Conference on Discrete Geometry for Computer Imagery, Marne-la-Vallée, France,
2019, vol. 11414, pp. 27–37.
ista: 'Biswas R, Largeteau-Skapin G, Zrour R, Andres E. 2019. Rhombic dodecahedron
grid—coordinate system and 3D digital object definitions. 21st IAPR International
Conference on Discrete Geometry for Computer Imagery. DGCI: International Conference
on Discrete Geometry for Computer Imagery, LNCS, vol. 11414, 27–37.'
mla: Biswas, Ranita, et al. “Rhombic Dodecahedron Grid—Coordinate System and 3D
Digital Object Definitions.” 21st IAPR International Conference on Discrete
Geometry for Computer Imagery, vol. 11414, Springer Berlin Heidelberg, 2019,
pp. 27–37, doi:10.1007/978-3-030-14085-4_3.
short: R. Biswas, G. Largeteau-Skapin, R. Zrour, E. Andres, in:, 21st IAPR International
Conference on Discrete Geometry for Computer Imagery, Springer Berlin Heidelberg,
Berlin, Heidelberg, 2019, pp. 27–37.
conference:
end_date: 2019-03-28
location: Marne-la-Vallée, France
name: 'DGCI: International Conference on Discrete Geometry for Computer Imagery'
start_date: 2019-03-26
date_created: 2019-03-21T12:12:19Z
date_published: 2019-02-23T00:00:00Z
date_updated: 2022-01-27T14:25:17Z
day: '23'
doi: 10.1007/978-3-030-14085-4_3
extern: '1'
intvolume: ' 11414'
language:
- iso: eng
month: '02'
oa_version: None
page: 27-37
place: Berlin, Heidelberg
publication: 21st IAPR International Conference on Discrete Geometry for Computer
Imagery
publication_identifier:
isbn:
- 978-3-6624-6446-5
- 978-3-6624-6447-2
issn:
- 0302-9743
- 1611-3349
publication_status: published
publisher: Springer Berlin Heidelberg
quality_controlled: '1'
status: public
title: Rhombic dodecahedron grid—coordinate system and 3D digital object definitions
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 11414
year: '2019'
...
---
_id: '6462'
abstract:
- lang: eng
text: A controller is a device that interacts with a plant. At each time point,it
reads the plant’s state and issues commands with the goal that the plant oper-ates
optimally. Constructing optimal controllers is a fundamental and challengingproblem.
Machine learning techniques have recently been successfully applied totrain controllers,
yet they have limitations. Learned controllers are monolithic andhard to reason
about. In particular, it is difficult to add features without retraining,to guarantee
any level of performance, and to achieve acceptable performancewhen encountering
untrained scenarios. These limitations can be addressed bydeploying quantitative
run-timeshieldsthat serve as a proxy for the controller.At each time point, the
shield reads the command issued by the controller andmay choose to alter it before
passing it on to the plant. We show how optimalshields that interfere as little
as possible while guaranteeing a desired level ofcontroller performance, can be
generated systematically and automatically usingreactive synthesis. First, we abstract the plant by building a stochastic model.Second,
we consider the learned controller to be a black box. Third, we mea-surecontroller
performanceandshield interferenceby two quantitative run-timemeasures that are
formally defined using weighted automata. Then, the problemof constructing a shield
that guarantees maximal performance with minimal inter-ference is the problem
of finding an optimal strategy in a stochastic2-player game“controller versus
shield” played on the abstract state space of the plant with aquantitative objective
obtained from combining the performance and interferencemeasures. We illustrate
the effectiveness of our approach by automatically con-structing lightweight shields
for learned traffic-light controllers in various roadnetworks. The shields we
generate avoid liveness bugs, improve controller per-formance in untrained and
changing traffic situations, and add features to learnedcontrollers, such as giving
priority to emergency vehicles.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Bettina
full_name: Konighofer, Bettina
last_name: Konighofer
- first_name: Stefan
full_name: Pranger, Stefan
last_name: Pranger
citation:
ama: 'Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. Run-time
optimization for learned controllers through quantitative games. In: 31st International
Conference on Computer-Aided Verification. Vol 11561. Springer; 2019:630-649.
doi:10.1007/978-3-030-25540-4_36'
apa: 'Avni, G., Bloem, R., Chatterjee, K., Henzinger, T. A., Konighofer, B., &
Pranger, S. (2019). Run-time optimization for learned controllers through quantitative
games. In 31st International Conference on Computer-Aided Verification
(Vol. 11561, pp. 630–649). New York, NY, United States: Springer. https://doi.org/10.1007/978-3-030-25540-4_36'
chicago: Avni, Guy, Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, Bettina
Konighofer, and Stefan Pranger. “Run-Time Optimization for Learned Controllers
through Quantitative Games.” In 31st International Conference on Computer-Aided
Verification, 11561:630–49. Springer, 2019. https://doi.org/10.1007/978-3-030-25540-4_36.
ieee: G. Avni, R. Bloem, K. Chatterjee, T. A. Henzinger, B. Konighofer, and S. Pranger,
“Run-time optimization for learned controllers through quantitative games,” in
31st International Conference on Computer-Aided Verification, New York,
NY, United States, 2019, vol. 11561, pp. 630–649.
ista: 'Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. 2019.
Run-time optimization for learned controllers through quantitative games. 31st
International Conference on Computer-Aided Verification. CAV: Computer Aided Verification,
LNCS, vol. 11561, 630–649.'
mla: Avni, Guy, et al. “Run-Time Optimization for Learned Controllers through Quantitative
Games.” 31st International Conference on Computer-Aided Verification, vol.
11561, Springer, 2019, pp. 630–49, doi:10.1007/978-3-030-25540-4_36.
short: G. Avni, R. Bloem, K. Chatterjee, T.A. Henzinger, B. Konighofer, S. Pranger,
in:, 31st International Conference on Computer-Aided Verification, Springer, 2019,
pp. 630–649.
conference:
end_date: 2019-07-18
location: New York, NY, United States
name: 'CAV: Computer Aided Verification'
start_date: 2019-07-13
corr_author: '1'
date_created: 2019-05-16T11:22:30Z
date_published: 2019-07-12T00:00:00Z
date_updated: 2025-04-15T06:26:05Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-030-25540-4_36
external_id:
isi:
- '000491468000036'
file:
- access_level: open_access
checksum: c231579f2485c6fd4df17c9443a4d80b
content_type: application/pdf
creator: dernst
date_created: 2019-08-14T09:35:24Z
date_updated: 2020-07-14T12:47:31Z
file_id: '6816'
file_name: 2019_CAV_Avni.pdf
file_size: 659766
relation: main_file
file_date_updated: 2020-07-14T12:47:31Z
has_accepted_license: '1'
intvolume: ' 11561'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 630-649
project:
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: 31st International Conference on Computer-Aided Verification
publication_identifier:
isbn:
- '9783030255398'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Run-time optimization for learned controllers through quantitative 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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 11561
year: '2019'
...
---
_id: '6482'
abstract:
- lang: eng
text: 'Computer vision systems for automatic image categorization have become accurate
and reliable enough that they can run continuously for days or even years as components
of real-world commercial applications. A major open problem in this context, however,
is quality control. Good classification performance can only be expected if systems
run under the specific conditions, in particular data distributions, that they
were trained for. Surprisingly, none of the currently used deep network architectures
have a built-in functionality that could detect if a network operates on data
from a distribution it was not trained for, such that potentially a warning to
the human users could be triggered. In this work, we describe KS(conf), a procedure
for detecting such outside of specifications (out-of-specs) operation, based on
statistical testing of the network outputs. We show by extensive experiments using
the ImageNet, AwA2 and DAVIS datasets on a variety of ConvNets architectures that
KS(conf) reliably detects out-of-specs situations. It furthermore has a number
of properties that make it a promising candidate for practical deployment: it
is easy to implement, adds almost no overhead to the system, works with all networks,
including pretrained ones, and requires no a priori knowledge of how the data
distribution could change. '
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Rémy
full_name: Sun, Rémy
last_name: Sun
- first_name: Christoph
full_name: Lampert, Christoph
id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
last_name: Lampert
orcid: 0000-0001-8622-7887
citation:
ama: 'Sun R, Lampert C. KS(conf): A light-weight test if a ConvNet operates outside
of Its specifications. In: Vol 11269. Springer Nature; 2019:244-259. doi:10.1007/978-3-030-12939-2_18'
apa: 'Sun, R., & Lampert, C. (2019). KS(conf): A light-weight test if a ConvNet
operates outside of Its specifications (Vol. 11269, pp. 244–259). Presented at
the GCPR: Conference on Pattern Recognition, Stuttgart, Germany: Springer Nature.
https://doi.org/10.1007/978-3-030-12939-2_18'
chicago: 'Sun, Rémy, and Christoph Lampert. “KS(Conf): A Light-Weight Test If a
ConvNet Operates Outside of Its Specifications,” 11269:244–59. Springer Nature,
2019. https://doi.org/10.1007/978-3-030-12939-2_18.'
ieee: 'R. Sun and C. Lampert, “KS(conf): A light-weight test if a ConvNet operates
outside of Its specifications,” presented at the GCPR: Conference on Pattern Recognition,
Stuttgart, Germany, 2019, vol. 11269, pp. 244–259.'
ista: 'Sun R, Lampert C. 2019. KS(conf): A light-weight test if a ConvNet operates
outside of Its specifications. GCPR: Conference on Pattern Recognition, LNCS,
vol. 11269, 244–259.'
mla: 'Sun, Rémy, and Christoph Lampert. KS(Conf): A Light-Weight Test If a ConvNet
Operates Outside of Its Specifications. Vol. 11269, Springer Nature, 2019,
pp. 244–59, doi:10.1007/978-3-030-12939-2_18.'
short: R. Sun, C. Lampert, in:, Springer Nature, 2019, pp. 244–259.
conference:
end_date: 2018-10-12
location: Stuttgart, Germany
name: 'GCPR: Conference on Pattern Recognition'
start_date: 2018-10-09
date_created: 2019-05-24T09:48:36Z
date_published: 2019-02-14T00:00:00Z
date_updated: 2025-04-15T07:10:25Z
day: '14'
department:
- _id: ChLa
doi: 10.1007/978-3-030-12939-2_18
ec_funded: 1
external_id:
arxiv:
- '1804.04171'
intvolume: ' 11269'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1804.04171
month: '02'
oa: 1
oa_version: Preprint
page: 244-259
project:
- _id: 2532554C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '308036'
name: Lifelong Learning of Visual Scene Understanding
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030129385'
- '9783030129392'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '6944'
relation: later_version
status: public
scopus_import: '1'
status: public
title: 'KS(conf): A light-weight test if a ConvNet operates outside of Its specifications'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11269
year: '2019'
...
---
_id: '6493'
abstract:
- lang: eng
text: We present two algorithmic approaches for synthesizing linear hybrid automata
from experimental data. Unlike previous approaches, our algorithms work without
a template and generate an automaton with nondeterministic guards and invariants,
and with an arbitrary number and topology of modes. They thus construct a succinct
model from the data and provide formal guarantees. In particular, (1) the generated
automaton can reproduce the data up to a specified tolerance and (2) the automaton
is tight, given the first guarantee. Our first approach encodes the synthesis
problem as a logical formula in the theory of linear arithmetic, which can then
be solved by an SMT solver. This approach minimizes the number of modes in the
resulting model but is only feasible for limited data sets. To address scalability,
we propose a second approach that does not enforce to find a minimal model. The
algorithm constructs an initial automaton and then iteratively extends the automaton
based on processing new data. Therefore the algorithm is well-suited for online
and synthesis-in-the-loop applications. The core of the algorithm is a membership
query that checks whether, within the specified tolerance, a given data set can
result from the execution of a given automaton. We solve this membership problem
for linear hybrid automata by repeated reachability computations. We demonstrate
the effectiveness of the algorithm on synthetic data sets and on cardiac-cell
measurements.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Miriam
full_name: Garcia Soto, Miriam
id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
last_name: Garcia Soto
orcid: 0000−0003−2936−5719
- 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: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Luka
full_name: Zeleznik, Luka
id: 3ADCA2E4-F248-11E8-B48F-1D18A9856A87
last_name: Zeleznik
citation:
ama: 'Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. Membership-based synthesis
of linear hybrid automata. In: 31st International Conference on Computer-Aided
Verification. Vol 11561. Springer; 2019:297-314. doi:10.1007/978-3-030-25540-4_16'
apa: 'Garcia Soto, M., Henzinger, T. A., Schilling, C., & Zeleznik, L. (2019).
Membership-based synthesis of linear hybrid automata. In 31st International
Conference on Computer-Aided Verification (Vol. 11561, pp. 297–314). New York
City, NY, USA: Springer. https://doi.org/10.1007/978-3-030-25540-4_16'
chicago: Garcia Soto, Miriam, Thomas A Henzinger, Christian Schilling, and Luka
Zeleznik. “Membership-Based Synthesis of Linear Hybrid Automata.” In 31st International
Conference on Computer-Aided Verification, 11561:297–314. Springer, 2019.
https://doi.org/10.1007/978-3-030-25540-4_16.
ieee: M. Garcia Soto, T. A. Henzinger, C. Schilling, and L. Zeleznik, “Membership-based
synthesis of linear hybrid automata,” in 31st International Conference on Computer-Aided
Verification, New York City, NY, USA, 2019, vol. 11561, pp. 297–314.
ista: 'Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. 2019. Membership-based
synthesis of linear hybrid automata. 31st International Conference on Computer-Aided
Verification. CAV: Computer-Aided Verification, LNCS, vol. 11561, 297–314.'
mla: Garcia Soto, Miriam, et al. “Membership-Based Synthesis of Linear Hybrid Automata.”
31st International Conference on Computer-Aided Verification, vol. 11561,
Springer, 2019, pp. 297–314, doi:10.1007/978-3-030-25540-4_16.
short: M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International
Conference on Computer-Aided Verification, Springer, 2019, pp. 297–314.
conference:
end_date: 2019-07-18
location: New York City, NY, USA
name: 'CAV: Computer-Aided Verification'
start_date: 2019-07-15
corr_author: '1'
date_created: 2019-05-27T07:09:53Z
date_published: 2019-07-12T00:00:00Z
date_updated: 2025-04-15T06:26:13Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-25540-4_16
ec_funded: 1
external_id:
isi:
- '000491468000016'
file:
- access_level: open_access
checksum: 1f1d61b83a151031745ef70a501da3d6
content_type: application/pdf
creator: dernst
date_created: 2019-08-14T11:05:30Z
date_updated: 2020-07-14T12:47:32Z
file_id: '6817'
file_name: 2019_CAV_GarciaSoto.pdf
file_size: 674795
relation: main_file
file_date_updated: 2020-07-14T12:47:32Z
has_accepted_license: '1'
intvolume: ' 11561'
isi: 1
keyword:
- Synthesis
- Linear hybrid automaton
- Membership
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 297-314
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
- _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: Formal methods for the design and analysis of complex systems
publication: 31st International Conference on Computer-Aided Verification
publication_identifier:
isbn:
- '9783030255398'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Membership-based synthesis of linear hybrid automata
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 11561
year: '2019'
...
---
_id: '6726'
abstract:
- lang: eng
text: Randomness is an essential part of any secure cryptosystem, but many constructions
rely on distributions that are not uniform. This is particularly true for lattice
based cryptosystems, which more often than not make use of discrete Gaussian distributions
over the integers. For practical purposes it is crucial to evaluate the impact
that approximation errors have on the security of a scheme to provide the best
possible trade-off between security and performance. Recent years have seen surprising
results allowing to use relatively low precision while maintaining high levels
of security. A key insight in these results is that sampling a distribution with
low relative error can provide very strong security guarantees. Since floating
point numbers provide guarantees on the relative approximation error, they seem
a suitable tool in this setting, but it is not obvious which sampling algorithms
can actually profit from them. While previous works have shown that inversion
sampling can be adapted to provide a low relative error (Pöppelmann et al., CHES
2014; Prest, ASIACRYPT 2017), other works have called into question if this is
possible for other sampling techniques (Zheng et al., Eprint report 2018/309).
In this work, we consider all sampling algorithms that are popular in the cryptographic
setting and analyze the relationship of floating point precision and the resulting
relative error. We show that all of the algorithms either natively achieve a low
relative error or can be adapted to do so.
article_processing_charge: No
author:
- first_name: Michael
full_name: Walter, Michael
id: 488F98B0-F248-11E8-B48F-1D18A9856A87
last_name: Walter
orcid: 0000-0003-3186-2482
citation:
ama: 'Walter M. Sampling the integers with low relative error. In: Buchmann J, Nitaj
A, Rachidi T, eds. Progress in Cryptology – AFRICACRYPT 2019. Vol 11627.
LNCS. Cham: Springer Nature; 2019:157-180. doi:10.1007/978-3-030-23696-0_9'
apa: 'Walter, M. (2019). Sampling the integers with low relative error. In J. Buchmann,
A. Nitaj, & T. Rachidi (Eds.), Progress in Cryptology – AFRICACRYPT 2019
(Vol. 11627, pp. 157–180). Cham: Springer Nature. https://doi.org/10.1007/978-3-030-23696-0_9'
chicago: 'Walter, Michael. “Sampling the Integers with Low Relative Error.” In Progress
in Cryptology – AFRICACRYPT 2019, edited by J Buchmann, A Nitaj, and T Rachidi,
11627:157–80. LNCS. Cham: Springer Nature, 2019. https://doi.org/10.1007/978-3-030-23696-0_9.'
ieee: 'M. Walter, “Sampling the integers with low relative error,” in Progress
in Cryptology – AFRICACRYPT 2019, vol. 11627, J. Buchmann, A. Nitaj, and T.
Rachidi, Eds. Cham: Springer Nature, 2019, pp. 157–180.'
ista: 'Walter M. 2019.Sampling the integers with low relative error. In: Progress
in Cryptology – AFRICACRYPT 2019. vol. 11627, 157–180.'
mla: Walter, Michael. “Sampling the Integers with Low Relative Error.” Progress
in Cryptology – AFRICACRYPT 2019, edited by J Buchmann et al., vol. 11627,
Springer Nature, 2019, pp. 157–80, doi:10.1007/978-3-030-23696-0_9.
short: M. Walter, in:, J. Buchmann, A. Nitaj, T. Rachidi (Eds.), Progress in Cryptology
– AFRICACRYPT 2019, Springer Nature, Cham, 2019, pp. 157–180.
conference:
end_date: 2019-07-11
location: Rabat, Morocco
name: 'AFRICACRYPT: International Conference on Cryptology in Africa'
start_date: 2019-07-09
date_created: 2019-07-29T12:25:31Z
date_published: 2019-06-29T00:00:00Z
date_updated: 2025-09-10T10:38:28Z
day: '29'
department:
- _id: KrPi
doi: 10.1007/978-3-030-23696-0_9
ec_funded: 1
editor:
- first_name: J
full_name: Buchmann, J
last_name: Buchmann
- first_name: A
full_name: Nitaj, A
last_name: Nitaj
- first_name: T
full_name: Rachidi, T
last_name: Rachidi
external_id:
isi:
- '001299240700009'
intvolume: ' 11627'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2019/068
month: '06'
oa: 1
oa_version: Preprint
page: 157-180
place: Cham
project:
- _id: 258AA5B2-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '682815'
name: Teaching Old Crypto New Tricks
publication: Progress in Cryptology – AFRICACRYPT 2019
publication_identifier:
eisbn:
- 978-3-0302-3696-0
eissn:
- 1611-3349
isbn:
- 978-3-0302-3695-3
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Sampling the integers with low relative error
type: book_chapter
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 11627
year: '2019'
...
---
_id: '6822'
abstract:
- lang: eng
text: "In two-player games on graphs, the players move a token through a graph to
produce an infinite path, which determines the qualitative winner or quantitative
payoff of the game. In bidding games, in each turn, we hold an auction between
the two players to determine which player moves the token. Bidding games have
largely been studied with concrete bidding mechanisms that are variants of a first-price
auction: in each turn both players simultaneously submit bids, the higher\r\nbidder
moves the token, and pays his bid to the lower bidder in Richman bidding, to the
bank in poorman bidding, and in taxman bidding, the bid is split between the other
player and the bank according to a predefined constant factor. Bidding games are
deterministic games. They have an intriguing connection with a fragment of stochastic
games called \r\n randomturn games. We study, for the first time, a combination
of bidding games with probabilistic behavior; namely, we study bidding games that
are played on Markov decision processes, where the players bid for the right to
choose the next action, which determines the probability distribution according
to which the next vertex is chosen. We study parity and meanpayoff bidding games
on MDPs and extend results from the deterministic bidding setting to the probabilistic
one."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- 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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Petr
full_name: Novotny, Petr
last_name: Novotny
citation:
ama: 'Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. Bidding games on Markov decision
processes. In: Proceedings of the 13th International Conference of Reachability
Problems. Vol 11674. Springer; 2019:1-12. doi:10.1007/978-3-030-30806-3_1'
apa: 'Avni, G., Henzinger, T. A., Ibsen-Jensen, R., & Novotny, P. (2019). Bidding
games on Markov decision processes. In Proceedings of the 13th International
Conference of Reachability Problems (Vol. 11674, pp. 1–12). Brussels, Belgium:
Springer. https://doi.org/10.1007/978-3-030-30806-3_1'
chicago: Avni, Guy, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Petr Novotny. “Bidding
Games on Markov Decision Processes.” In Proceedings of the 13th International
Conference of Reachability Problems, 11674:1–12. Springer, 2019. https://doi.org/10.1007/978-3-030-30806-3_1.
ieee: G. Avni, T. A. Henzinger, R. Ibsen-Jensen, and P. Novotny, “Bidding games
on Markov decision processes,” in Proceedings of the 13th International Conference
of Reachability Problems, Brussels, Belgium, 2019, vol. 11674, pp. 1–12.
ista: 'Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. 2019. Bidding games on Markov
decision processes. Proceedings of the 13th International Conference of Reachability
Problems. RP: Reachability Problems, LNCS, vol. 11674, 1–12.'
mla: Avni, Guy, et al. “Bidding Games on Markov Decision Processes.” Proceedings
of the 13th International Conference of Reachability Problems, vol. 11674,
Springer, 2019, pp. 1–12, doi:10.1007/978-3-030-30806-3_1.
short: G. Avni, T.A. Henzinger, R. Ibsen-Jensen, P. Novotny, in:, Proceedings of
the 13th International Conference of Reachability Problems, Springer, 2019, pp.
1–12.
conference:
end_date: 2019-09-13
location: Brussels, Belgium
name: 'RP: Reachability Problems'
start_date: 2019-09-11
date_created: 2019-08-19T07:58:10Z
date_published: 2019-09-06T00:00:00Z
date_updated: 2025-09-10T10:39:56Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-30806-3_1
external_id:
isi:
- '001333747500001'
file:
- access_level: open_access
checksum: 45ebbc709af2b247d28c7c293c01504b
content_type: application/pdf
creator: gavni
date_created: 2019-08-19T07:56:40Z
date_updated: 2020-07-14T12:47:41Z
file_id: '6823'
file_name: prob.pdf
file_size: 436635
relation: main_file
file_date_updated: 2020-07-14T12:47:41Z
has_accepted_license: '1'
intvolume: ' 11674'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 1-12
project:
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: ' Proceedings of the 13th International Conference of Reachability Problems'
publication_identifier:
isbn:
- 978-303030805-6
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Bidding games on Markov decision processes
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 11674
year: '2019'
...
---
_id: '6942'
abstract:
- lang: eng
text: "Graph games and Markov decision processes (MDPs) are standard models in reactive
synthesis and verification of probabilistic systems with nondeterminism. The class
of \U0001D714 -regular winning conditions; e.g., safety, reachability, liveness,
parity conditions; provides a robust and expressive specification formalism for
properties that arise in analysis of reactive systems. The resolutions of nondeterminism
in games and MDPs are represented as strategies, and we consider succinct representation
of such strategies. The decision-tree data structure from machine learning retains
the flavor of decisions of strategies and allows entropy-based minimization to
obtain succinct trees. However, in contrast to traditional machine-learning problems
where small errors are allowed, for winning strategies in graph games and MDPs
no error is allowed, and the decision tree must represent the entire strategy.
In this work we propose decision trees with linear classifiers for representation
of strategies in graph games and MDPs. We have implemented strategy representation
using this data structure and we present experimental results for problems on
graph games and MDPs, which show that this new data structure presents a much
more efficient strategy representation as compared to standard decision trees."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Pranav
full_name: Ashok, Pranav
last_name: Ashok
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Jan
full_name: Křetínský, Jan
last_name: Křetínský
- first_name: Christoph
full_name: Lampert, Christoph
id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
last_name: Lampert
orcid: 0000-0001-8622-7887
- first_name: Viktor
full_name: Toman, Viktor
id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
last_name: Toman
orcid: 0000-0001-9036-063X
citation:
ama: 'Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. Strategy
representation by decision trees with linear classifiers. In: 16th International
Conference on Quantitative Evaluation of Systems. Vol 11785. Springer Nature;
2019:109-128. doi:10.1007/978-3-030-30281-8_7'
apa: 'Ashok, P., Brázdil, T., Chatterjee, K., Křetínský, J., Lampert, C., &
Toman, V. (2019). Strategy representation by decision trees with linear classifiers.
In 16th International Conference on Quantitative Evaluation of Systems
(Vol. 11785, pp. 109–128). Glasgow, United Kingdom: Springer Nature. https://doi.org/10.1007/978-3-030-30281-8_7'
chicago: Ashok, Pranav, Tomáš Brázdil, Krishnendu Chatterjee, Jan Křetínský, Christoph
Lampert, and Viktor Toman. “Strategy Representation by Decision Trees with Linear
Classifiers.” In 16th International Conference on Quantitative Evaluation of
Systems, 11785:109–28. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-30281-8_7.
ieee: P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, and V. Toman,
“Strategy representation by decision trees with linear classifiers,” in 16th
International Conference on Quantitative Evaluation of Systems, Glasgow, United
Kingdom, 2019, vol. 11785, pp. 109–128.
ista: 'Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. 2019.
Strategy representation by decision trees with linear classifiers. 16th International
Conference on Quantitative Evaluation of Systems. QEST: Quantitative Evaluation
of Systems, LNCS, vol. 11785, 109–128.'
mla: Ashok, Pranav, et al. “Strategy Representation by Decision Trees with Linear
Classifiers.” 16th International Conference on Quantitative Evaluation of Systems,
vol. 11785, Springer Nature, 2019, pp. 109–28, doi:10.1007/978-3-030-30281-8_7.
short: P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, V. Toman,
in:, 16th International Conference on Quantitative Evaluation of Systems, Springer
Nature, 2019, pp. 109–128.
conference:
end_date: 2019-09-12
location: Glasgow, United Kingdom
name: 'QEST: Quantitative Evaluation of Systems'
start_date: 2019-09-10
date_created: 2019-10-14T06:57:49Z
date_published: 2019-09-04T00:00:00Z
date_updated: 2025-04-14T13:51:05Z
day: '04'
department:
- _id: KrCh
- _id: ChLa
doi: 10.1007/978-3-030-30281-8_7
external_id:
arxiv:
- '1906.08178'
isi:
- '000679281300007'
intvolume: ' 11785'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1906.08178
month: '09'
oa: 1
oa_version: Preprint
page: 109-128
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: 16th International Conference on Quantitative Evaluation of Systems
publication_identifier:
eisbn:
- '9783030302818'
isbn:
- '9783030302801'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Strategy representation by decision trees with linear classifiers
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 11785
year: '2019'
...
---
_id: '7228'
abstract:
- lang: eng
text: "Traditional concurrent programming involves manipulating shared mutable state.
Alternatives to this programming style are communicating sequential processes
(CSP) and actor models, which share data via explicit communication. These models
have been known for almost half a century, and have recently had started to gain
significant traction among modern programming languages. The common abstraction
for communication between several processes is the channel. Although channels
are similar to producer-consumer data structures, they have different semantics
and support additional operations, such as the select expression. Despite their
growing popularity, most known implementations of channels use lock-based data
structures and can be rather inefficient.\r\n\r\nIn this paper, we present the
first efficient lock-free algorithm for implementing a communication channel for
CSP programming. We provide implementations and experimental results in the Kotlin
and Go programming languages. Our new algorithm outperforms existing implementations
on many workloads, while providing non-blocking progress guarantee. Our design
can serve as an example of how to construct general communication data structures
for CSP and actor models. "
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Nikita
full_name: Koval, Nikita
id: 2F4DB10C-F248-11E8-B48F-1D18A9856A87
last_name: Koval
- 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: Roman
full_name: Elizarov, Roman
last_name: Elizarov
citation:
ama: 'Koval N, Alistarh D-A, Elizarov R. Scalable FIFO channels for programming
via communicating sequential processes. In: 25th Anniversary of Euro-Par.
Vol 11725. Springer Nature; 2019:317-333. doi:10.1007/978-3-030-29400-7_23'
apa: 'Koval, N., Alistarh, D.-A., & Elizarov, R. (2019). Scalable FIFO channels
for programming via communicating sequential processes. In 25th Anniversary
of Euro-Par (Vol. 11725, pp. 317–333). Göttingen, Germany: Springer Nature.
https://doi.org/10.1007/978-3-030-29400-7_23'
chicago: Koval, Nikita, Dan-Adrian Alistarh, and Roman Elizarov. “Scalable FIFO
Channels for Programming via Communicating Sequential Processes.” In 25th Anniversary
of Euro-Par, 11725:317–33. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-29400-7_23.
ieee: N. Koval, D.-A. Alistarh, and R. Elizarov, “Scalable FIFO channels for programming
via communicating sequential processes,” in 25th Anniversary of Euro-Par,
Göttingen, Germany, 2019, vol. 11725, pp. 317–333.
ista: 'Koval N, Alistarh D-A, Elizarov R. 2019. Scalable FIFO channels for programming
via communicating sequential processes. 25th Anniversary of Euro-Par. Euro-Par:
European Conference on Parallel Processing, LNCS, vol. 11725, 317–333.'
mla: Koval, Nikita, et al. “Scalable FIFO Channels for Programming via Communicating
Sequential Processes.” 25th Anniversary of Euro-Par, vol. 11725, Springer
Nature, 2019, pp. 317–33, doi:10.1007/978-3-030-29400-7_23.
short: N. Koval, D.-A. Alistarh, R. Elizarov, in:, 25th Anniversary of Euro-Par,
Springer Nature, 2019, pp. 317–333.
conference:
end_date: 2019-08-30
location: Göttingen, Germany
name: 'Euro-Par: European Conference on Parallel Processing'
start_date: 2019-08-26
date_created: 2020-01-05T23:00:46Z
date_published: 2019-08-13T00:00:00Z
date_updated: 2023-09-06T14:53:59Z
day: '13'
department:
- _id: DaAl
doi: 10.1007/978-3-030-29400-7_23
external_id:
isi:
- '000851061400023'
intvolume: ' 11725'
isi: 1
language:
- iso: eng
month: '08'
oa_version: None
page: 317-333
publication: 25th Anniversary of Euro-Par
publication_identifier:
eissn:
- 1611-3349
isbn:
- 978-3-0302-9399-4
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Scalable FIFO channels for programming via communicating sequential processes
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11725
year: '2019'
...
---
_id: '7230'
abstract:
- lang: eng
text: Simple drawings of graphs are those in which each pair of edges share at most
one point, either a common endpoint or a proper crossing. In this paper we study
the problem of extending a simple drawing D(G) of a graph G by inserting a set
of edges from the complement of G into D(G) such that the result is a simple drawing.
In the context of rectilinear drawings, the problem is trivial. For pseudolinear
drawings, the existence of such an extension follows from Levi’s enlargement lemma.
In contrast, we prove that deciding if a given set of edges can be inserted into
a simple drawing is NP-complete. Moreover, we show that the maximization version
of the problem is APX-hard. We also present a polynomial-time algorithm for deciding
whether one edge uv can be inserted into D(G) when {u,v} is a dominating set for
the graph G.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Alan M
full_name: Arroyo Guevara, Alan M
id: 3207FDC6-F248-11E8-B48F-1D18A9856A87
last_name: Arroyo Guevara
orcid: 0000-0003-2401-8670
- first_name: Martin
full_name: Derka, Martin
last_name: Derka
- first_name: Irene
full_name: Parada, Irene
last_name: Parada
citation:
ama: 'Arroyo Guevara AM, Derka M, Parada I. Extending simple drawings. In: 27th
International Symposium on Graph Drawing and Network Visualization. Vol 11904.
Springer Nature; 2019:230-243. doi:10.1007/978-3-030-35802-0_18'
apa: 'Arroyo Guevara, A. M., Derka, M., & Parada, I. (2019). Extending simple
drawings. In 27th International Symposium on Graph Drawing and Network Visualization
(Vol. 11904, pp. 230–243). Prague, Czech Republic: Springer Nature. https://doi.org/10.1007/978-3-030-35802-0_18'
chicago: Arroyo Guevara, Alan M, Martin Derka, and Irene Parada. “Extending Simple
Drawings.” In 27th International Symposium on Graph Drawing and Network Visualization,
11904:230–43. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-35802-0_18.
ieee: A. M. Arroyo Guevara, M. Derka, and I. Parada, “Extending simple drawings,”
in 27th International Symposium on Graph Drawing and Network Visualization,
Prague, Czech Republic, 2019, vol. 11904, pp. 230–243.
ista: 'Arroyo Guevara AM, Derka M, Parada I. 2019. Extending simple drawings. 27th
International Symposium on Graph Drawing and Network Visualization. GD: Graph
Drawing and Network Visualization, LNCS, vol. 11904, 230–243.'
mla: Arroyo Guevara, Alan M., et al. “Extending Simple Drawings.” 27th International
Symposium on Graph Drawing and Network Visualization, vol. 11904, Springer
Nature, 2019, pp. 230–43, doi:10.1007/978-3-030-35802-0_18.
short: A.M. Arroyo Guevara, M. Derka, I. Parada, in:, 27th International Symposium
on Graph Drawing and Network Visualization, Springer Nature, 2019, pp. 230–243.
conference:
end_date: 2019-09-20
location: Prague, Czech Republic
name: 'GD: Graph Drawing and Network Visualization'
start_date: 2019-09-17
date_created: 2020-01-05T23:00:47Z
date_published: 2019-11-28T00:00:00Z
date_updated: 2025-04-14T07:44:07Z
day: '28'
department:
- _id: UlWa
doi: 10.1007/978-3-030-35802-0_18
ec_funded: 1
external_id:
arxiv:
- '1908.08129'
isi:
- '000612918800018'
intvolume: ' 11904'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1908.08129
month: '11'
oa: 1
oa_version: Preprint
page: 230-243
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: 27th International Symposium on Graph Drawing and Network Visualization
publication_identifier:
eissn:
- 1611-3349
isbn:
- 978-3-0303-5801-3
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Extending simple drawings
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11904
year: '2019'
...
---
_id: '7231'
abstract:
- lang: eng
text: Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation
for nonlinear systems with polynomial dynamics, which leverages a combination
of barrier certificates. PBT has advantages over traditional time-step based methods
in dealing with those nonlinear dynamical systems in which there is a large difference
in speed between trajectories, producing an overapproximation that is time independent.
However, the existing approach for PBT is not efficient due to the application
of interval methods for enclosure-box computation, and it can only deal with continuous
dynamical systems without uncertainty. In this paper, we extend the approach with
the ability to handle both continuous and hybrid dynamical systems with uncertainty
that can reside in parameters and/or noise. We also improve the efficiency of
the method significantly, by avoiding the use of interval-based methods for the
enclosure-box computation without loosing soundness. We have developed a C++ prototype
implementing the proposed approach and we evaluate it on several benchmarks. The
experiments show that our approach is more efficient and precise than other methods
in the literature.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Kong H, Bartocci E, Jiang Y, Henzinger TA. Piecewise robust barrier tubes
for nonlinear hybrid systems with uncertainty. In: 17th International Conference
on Formal Modeling and Analysis of Timed Systems. Vol 11750. Springer Nature;
2019:123-141. doi:10.1007/978-3-030-29662-9_8'
apa: 'Kong, H., Bartocci, E., Jiang, Y., & Henzinger, T. A. (2019). Piecewise
robust barrier tubes for nonlinear hybrid systems with uncertainty. In 17th
International Conference on Formal Modeling and Analysis of Timed Systems
(Vol. 11750, pp. 123–141). Amsterdam, The Netherlands: Springer Nature. https://doi.org/10.1007/978-3-030-29662-9_8'
chicago: Kong, Hui, Ezio Bartocci, Yu Jiang, and Thomas A Henzinger. “Piecewise
Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” In 17th
International Conference on Formal Modeling and Analysis of Timed Systems,
11750:123–41. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-29662-9_8.
ieee: H. Kong, E. Bartocci, Y. Jiang, and T. A. Henzinger, “Piecewise robust barrier
tubes for nonlinear hybrid systems with uncertainty,” in 17th International
Conference on Formal Modeling and Analysis of Timed Systems, Amsterdam, The
Netherlands, 2019, vol. 11750, pp. 123–141.
ista: 'Kong H, Bartocci E, Jiang Y, Henzinger TA. 2019. Piecewise robust barrier
tubes for nonlinear hybrid systems with uncertainty. 17th International Conference
on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and
Analysis of Timed Systems, LNCS, vol. 11750, 123–141.'
mla: Kong, Hui, et al. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems
with Uncertainty.” 17th International Conference on Formal Modeling and Analysis
of Timed Systems, vol. 11750, Springer Nature, 2019, pp. 123–41, doi:10.1007/978-3-030-29662-9_8.
short: H. Kong, E. Bartocci, Y. Jiang, T.A. Henzinger, in:, 17th International Conference
on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 123–141.
conference:
end_date: 2019-08-29
location: Amsterdam, The Netherlands
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
start_date: 2019-08-27
date_created: 2020-01-05T23:00:47Z
date_published: 2019-08-13T00:00:00Z
date_updated: 2025-04-15T06:26:06Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-030-29662-9_8
external_id:
arxiv:
- '1907.11514'
isi:
- '000611677700008'
intvolume: ' 11750'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1907.11514
month: '08'
oa: 1
oa_version: Preprint
page: 123-141
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: 17th International Conference on Formal Modeling and Analysis of Timed
Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- 978-3-0302-9661-2
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11750
year: '2019'
...
---
_id: '7232'
abstract:
- lang: eng
text: 'We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism
which extends STL by capturing the discrete/ continuous time duality found in
many cyber-physical systems (CPS), as well as mixed-signal electronic designs.
In STL−MX, properties of components with continuous dynamics are expressed in
STL, while specifications of components with discrete dynamics are written in
LTL. To combine the two layers, we evaluate formulas on two traces, discrete-
and continuous-time, and introduce two interface operators that map signals, properties
and their satisfaction signals across the two time domains. We show that STL-mx
has the expressive power of STL supplemented with an implicit T-periodic clock
signal. We develop and implement an algorithm for monitoring STL-mx formulas and
illustrate the approach using a mixed-signal example. '
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: 17th
International Conference on Formal Modeling and Analysis of Timed Systems.
Vol 11750. Springer Nature; 2019:59-75. doi:10.1007/978-3-030-29662-9_4'
apa: 'Ferrere, T., Maler, O., & Nickovic, D. (2019). Mixed-time signal temporal
logic. In 17th International Conference on Formal Modeling and Analysis of
Timed Systems (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer
Nature. https://doi.org/10.1007/978-3-030-29662-9_4'
chicago: Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal
Logic.” In 17th International Conference on Formal Modeling and Analysis of
Timed Systems, 11750:59–75. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-29662-9_4.
ieee: T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,”
in 17th International Conference on Formal Modeling and Analysis of Timed Systems,
Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75.
ista: 'Ferrere T, Maler O, Nickovic D. 2019. Mixed-time signal temporal logic. 17th
International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS:
Formal Modeling and Anaysis of Timed Systems, LNCS, vol. 11750, 59–75.'
mla: Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” 17th International
Conference on Formal Modeling and Analysis of Timed Systems, vol. 11750, Springer
Nature, 2019, pp. 59–75, doi:10.1007/978-3-030-29662-9_4.
short: T. Ferrere, O. Maler, D. Nickovic, in:, 17th International Conference on
Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 59–75.
conference:
end_date: 2019-08-29
location: Amsterdam, The Netherlands
name: 'FORMATS: Formal Modeling and Anaysis of Timed Systems'
start_date: 2019-08-27
date_created: 2020-01-05T23:00:48Z
date_published: 2019-08-13T00:00:00Z
date_updated: 2025-04-15T06:26:06Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-030-29662-9_4
external_id:
isi:
- '000611677700004'
intvolume: ' 11750'
isi: 1
language:
- iso: eng
month: '08'
oa_version: None
page: 59-75
project:
- _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: Formal methods for the design and analysis of complex systems
publication: 17th International Conference on Formal Modeling and Analysis of Timed
Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- 978-3-0302-9661-2
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Mixed-time signal temporal logic
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11750
year: '2019'
...
---
_id: '7183'
abstract:
- lang: eng
text: 'A probabilistic vector addition system with states (pVASS) is a finite state
Markov process augmented with non-negative integer counters that can be incremented
or decremented during each state transition, blocking any behaviour that would
cause a counter to decrease below zero. The pVASS can be used as abstractions
of probabilistic programs with many decidable properties. The use of pVASS as
abstractions requires the presence of nondeterminism in the model. In this paper,
we develop techniques for checking fast termination of pVASS with nondeterminism.
That is, for every initial configuration of size n, we consider the worst expected
number of transitions needed to reach a configuration with some counter negative
(the expected termination time). We show that the problem whether the asymptotic
expected termination time is linear is decidable in polynomial time for a certain
natural class of pVASS with nondeterminism. Furthermore, we show the following
dichotomy: if the asymptotic expected termination time is not linear, then it
is at least quadratic, i.e., in Ω(n2).'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Tomás
full_name: Brázdil, Tomás
last_name: Brázdil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Antonín
full_name: Kucera, Antonín
last_name: Kucera
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Dominik
full_name: Velan, Dominik
last_name: Velan
citation:
ama: 'Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. Deciding fast termination
for probabilistic VASS with nondeterminism. In: International Symposium on
Automated Technology for Verification and Analysis. Vol 11781. Springer Nature;
2019:462-478. doi:10.1007/978-3-030-31784-3_27'
apa: 'Brázdil, T., Chatterjee, K., Kucera, A., Novotný, P., & Velan, D. (2019).
Deciding fast termination for probabilistic VASS with nondeterminism. In International
Symposium on Automated Technology for Verification and Analysis (Vol. 11781,
pp. 462–478). Taipei, Taiwan: Springer Nature. https://doi.org/10.1007/978-3-030-31784-3_27'
chicago: Brázdil, Tomás, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, and
Dominik Velan. “Deciding Fast Termination for Probabilistic VASS with Nondeterminism.”
In International Symposium on Automated Technology for Verification and Analysis,
11781:462–78. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-31784-3_27.
ieee: T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, and D. Velan, “Deciding
fast termination for probabilistic VASS with nondeterminism,” in International
Symposium on Automated Technology for Verification and Analysis, Taipei, Taiwan,
2019, vol. 11781, pp. 462–478.
ista: 'Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. 2019. Deciding fast
termination for probabilistic VASS with nondeterminism. International Symposium
on Automated Technology for Verification and Analysis. ATVA: Automated TEchnology
for Verification and Analysis, LNCS, vol. 11781, 462–478.'
mla: Brázdil, Tomás, et al. “Deciding Fast Termination for Probabilistic VASS with
Nondeterminism.” International Symposium on Automated Technology for Verification
and Analysis, vol. 11781, Springer Nature, 2019, pp. 462–78, doi:10.1007/978-3-030-31784-3_27.
short: T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, D. Velan, in:, International
Symposium on Automated Technology for Verification and Analysis, Springer Nature,
2019, pp. 462–478.
conference:
end_date: 2019-10-31
location: Taipei, Taiwan
name: 'ATVA: Automated TEchnology for Verification and Analysis'
start_date: 2019-10-28
date_created: 2019-12-15T23:00:44Z
date_published: 2019-10-21T00:00:00Z
date_updated: 2026-04-16T09:51:24Z
day: '21'
department:
- _id: KrCh
doi: 10.1007/978-3-030-31784-3_27
external_id:
arxiv:
- '1907.11010'
isi:
- '000723515700027'
intvolume: ' 11781'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1907.11010
month: '10'
oa: 1
oa_version: Preprint
page: 462-478
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: International Symposium on Automated Technology for Verification and
Analysis
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030317836'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Deciding fast termination for probabilistic VASS with nondeterminism
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 11781
year: '2019'
...
---
_id: '6430'
abstract:
- lang: eng
text: "A proxy re-encryption (PRE) scheme is a public-key encryption scheme that
allows the holder of a key pk to derive a re-encryption key for any other key
\U0001D45D\U0001D458′. This re-encryption key lets anyone transform ciphertexts
under pk into ciphertexts under \U0001D45D\U0001D458′ without having to know the
underlying message, while transformations from \U0001D45D\U0001D458′ to pk should
not be possible (unidirectional). Security is defined in a multi-user setting
against an adversary that gets the users’ public keys and can ask for re-encryption
keys and can corrupt users by requesting their secret keys. Any ciphertext that
the adversary cannot trivially decrypt given the obtained secret and re-encryption
keys should be secure.\r\n\r\nAll existing security proofs for PRE only show selective
security, where the adversary must first declare the users it wants to corrupt.
This can be lifted to more meaningful adaptive security by guessing the set of
corrupted users among the n users, which loses a factor exponential in Open image
in new window , rendering the result meaningless already for moderate Open image
in new window .\r\n\r\nJafargholi et al. (CRYPTO’17) proposed a framework that
in some cases allows to give adaptive security proofs for schemes which were previously
only known to be selectively secure, while avoiding the exponential loss that
results from guessing the adaptive choices made by an adversary. We apply their
framework to PREs that satisfy some natural additional properties. Concretely,
we give a more fine-grained reduction for several unidirectional PREs, proving
adaptive security at a much smaller loss. The loss depends on the graph of users
whose edges represent the re-encryption keys queried by the adversary. For trees
and chains the loss is quasi-polynomial in the size and for general graphs it
is exponential in their depth and indegree (instead of their size as for previous
reductions). Fortunately, trees and low-depth graphs cover many, if not most,
interesting applications.\r\n\r\nOur results apply e.g. to the bilinear-map based
PRE schemes by Ateniese et al. (NDSS’05 and CT-RSA’09), Gentry’s FHE-based scheme
(STOC’09) and the LWE-based scheme by Chandran et al. (PKC’14)."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Georg
full_name: Fuchsbauer, Georg
id: 46B4C3EE-F248-11E8-B48F-1D18A9856A87
last_name: Fuchsbauer
- first_name: Chethan
full_name: Kamath Hosdurg, Chethan
id: 4BD3F30E-F248-11E8-B48F-1D18A9856A87
last_name: Kamath Hosdurg
orcid: 0009-0006-6812-7317
- first_name: Karen
full_name: Klein, Karen
id: 3E83A2F8-F248-11E8-B48F-1D18A9856A87
last_name: Klein
- 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: 'Fuchsbauer G, Kamath Hosdurg C, Klein K, Pietrzak KZ. Adaptively secure proxy
re-encryption. In: Vol 11443. Springer Nature; 2019:317-346. doi:10.1007/978-3-030-17259-6_11'
apa: 'Fuchsbauer, G., Kamath Hosdurg, C., Klein, K., & Pietrzak, K. Z. (2019).
Adaptively secure proxy re-encryption (Vol. 11443, pp. 317–346). Presented at
the PKC: Public-Key Cryptograhy, Beijing, China: Springer Nature. https://doi.org/10.1007/978-3-030-17259-6_11'
chicago: Fuchsbauer, Georg, Chethan Kamath Hosdurg, Karen Klein, and Krzysztof Z
Pietrzak. “Adaptively Secure Proxy Re-Encryption,” 11443:317–46. Springer Nature,
2019. https://doi.org/10.1007/978-3-030-17259-6_11.
ieee: 'G. Fuchsbauer, C. Kamath Hosdurg, K. Klein, and K. Z. Pietrzak, “Adaptively
secure proxy re-encryption,” presented at the PKC: Public-Key Cryptograhy, Beijing,
China, 2019, vol. 11443, pp. 317–346.'
ista: 'Fuchsbauer G, Kamath Hosdurg C, Klein K, Pietrzak KZ. 2019. Adaptively secure
proxy re-encryption. PKC: Public-Key Cryptograhy, LNCS, vol. 11443, 317–346.'
mla: Fuchsbauer, Georg, et al. Adaptively Secure Proxy Re-Encryption. Vol.
11443, Springer Nature, 2019, pp. 317–46, doi:10.1007/978-3-030-17259-6_11.
short: G. Fuchsbauer, C. Kamath Hosdurg, K. Klein, K.Z. Pietrzak, in:, Springer
Nature, 2019, pp. 317–346.
conference:
end_date: 2019-04-17
location: Beijing, China
name: 'PKC: Public-Key Cryptograhy'
start_date: 2019-04-14
date_created: 2019-05-13T08:13:46Z
date_published: 2019-04-06T00:00:00Z
date_updated: 2026-04-16T09:52:04Z
day: '06'
department:
- _id: KrPi
doi: 10.1007/978-3-030-17259-6_11
ec_funded: 1
external_id:
isi:
- '001299215500011'
intvolume: ' 11443'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2018/426
month: '04'
oa: 1
oa_version: Preprint
page: 317-346
project:
- _id: 258AA5B2-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '682815'
name: Teaching Old Crypto New Tricks
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030172589'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '10035'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Adaptively secure proxy re-encryption
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 11443
year: '2019'
...
---
_id: '7147'
abstract:
- lang: eng
text: "The expression of a gene is characterised by its transcription factors and
the function processing them. If the transcription factors are not affected by
gene products, the regulating function is often represented as a combinational
logic circuit, where the outputs (product) are determined by current input values
(transcription factors) only, and are hence independent on their relative arrival
times. However, the simultaneous arrival of transcription factors (TFs) in genetic
circuits is a strong assumption, given that the processes of transcription and
translation of a gene into a protein introduce intrinsic time delays and that
there is no global synchronisation among the arrival times of different molecular
species at molecular targets.\r\n\r\nIn this paper, we construct an experimentally
implementable genetic circuit with two inputs and a single output, such that,
in presence of small delays in input arrival, the circuit exhibits qualitatively
distinct observable phenotypes. In particular, these phenotypes are long lived
transients: they all converge to a single value, but so slowly, that they seem
stable for an extended time period, longer than typical experiment duration. We
used rule-based language to prototype our circuit, and we implemented a search
for finding the parameter combinations raising the phenotypes of interest.\r\n\r\nThe
behaviour of our prototype circuit has wide implications. First, it suggests that
GRNs can exploit event timing to create phenotypes. Second, it opens the possibility
that GRNs are using event timing to react to stimuli and memorise events, without
explicit feedback in regulation. From the modelling perspective, our prototype
circuit demonstrates the critical importance of analysing the transient dynamics
at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Calin C
full_name: Guet, Calin C
id: 47F8433E-F248-11E8-B48F-1D18A9856A87
last_name: Guet
orcid: 0000-0001-6220-2052
- 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: Claudia
full_name: Igler, Claudia
id: 46613666-F248-11E8-B48F-1D18A9856A87
last_name: Igler
orcid: 0000-0001-7777-546X
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
citation:
ama: 'Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. Transient memory in gene
regulation. In: 17th International Conference on Computational Methods in Systems
Biology. Vol 11773. Springer Nature; 2019:155-187. doi:10.1007/978-3-030-31304-3_9'
apa: 'Guet, C. C., Henzinger, T. A., Igler, C., Petrov, T., & Sezgin, A. (2019).
Transient memory in gene regulation. In 17th International Conference on Computational
Methods in Systems Biology (Vol. 11773, pp. 155–187). Trieste, Italy: Springer
Nature. https://doi.org/10.1007/978-3-030-31304-3_9'
chicago: Guet, Calin C, Thomas A Henzinger, Claudia Igler, Tatjana Petrov, and Ali
Sezgin. “Transient Memory in Gene Regulation.” In 17th International Conference
on Computational Methods in Systems Biology, 11773:155–87. Springer Nature,
2019. https://doi.org/10.1007/978-3-030-31304-3_9.
ieee: C. C. Guet, T. A. Henzinger, C. Igler, T. Petrov, and A. Sezgin, “Transient
memory in gene regulation,” in 17th International Conference on Computational
Methods in Systems Biology, Trieste, Italy, 2019, vol. 11773, pp. 155–187.
ista: 'Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. 2019. Transient memory
in gene regulation. 17th International Conference on Computational Methods in
Systems Biology. CMSB: Computational Methods in Systems Biology, LNCS, vol. 11773,
155–187.'
mla: Guet, Calin C., et al. “Transient Memory in Gene Regulation.” 17th International
Conference on Computational Methods in Systems Biology, vol. 11773, Springer
Nature, 2019, pp. 155–87, doi:10.1007/978-3-030-31304-3_9.
short: C.C. Guet, T.A. Henzinger, C. Igler, T. Petrov, A. Sezgin, in:, 17th International
Conference on Computational Methods in Systems Biology, Springer Nature, 2019,
pp. 155–187.
conference:
end_date: 2019-09-20
location: Trieste, Italy
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2019-09-18
date_created: 2019-12-04T16:07:50Z
date_published: 2019-09-17T00:00:00Z
date_updated: 2026-04-16T10:26:49Z
day: '17'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1007/978-3-030-31304-3_9
external_id:
isi:
- '000557875100009'
intvolume: ' 11773'
isi: 1
language:
- iso: eng
month: '09'
oa_version: None
page: 155-187
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 251EE76E-B435-11E9-9278-68D0E5697425
grant_number: '24573'
name: Design principles underlying genetic switch architecture
publication: 17th International Conference on Computational Methods in Systems Biology
publication_identifier:
eisbn:
- '9783030313043'
eissn:
- 1611-3349
isbn:
- '9783030313036'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Transient memory in gene regulation
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 11773
year: '2019'
...
---
_id: '7411'
abstract:
- lang: eng
text: "Proofs of sequential work (PoSW) are proof systems where a prover, upon receiving
a statement χ and a time parameter T computes a proof ϕ(χ,T) which is efficiently
and publicly verifiable. The proof can be computed in T sequential steps, but
not much less, even by a malicious party having large parallelism. A PoSW thus
serves as a proof that T units of time have passed since χ\r\n\r\nwas received.\r\n\r\nPoSW
were introduced by Mahmoody, Moran and Vadhan [MMV11], a simple and practical
construction was only recently proposed by Cohen and Pietrzak [CP18].\r\n\r\nIn
this work we construct a new simple PoSW in the random permutation model which
is almost as simple and efficient as [CP18] but conceptually very different. Whereas
the structure underlying [CP18] is a hash tree, our construction is based on skip
lists and has the interesting property that computing the PoSW is a reversible
computation.\r\nThe fact that the construction is reversible can potentially be
used for new applications like constructing proofs of replication. We also show
how to “embed” the sloth function of Lenstra and Weselowski [LW17] into our PoSW
to get a PoSW where one additionally can verify correctness of the output much
more efficiently than recomputing it (though recent constructions of “verifiable
delay functions” subsume most of the applications this construction was aiming
at)."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Hamza M
full_name: Abusalah, Hamza M
id: 40297222-F248-11E8-B48F-1D18A9856A87
last_name: Abusalah
- first_name: Chethan
full_name: Kamath Hosdurg, Chethan
id: 4BD3F30E-F248-11E8-B48F-1D18A9856A87
last_name: Kamath Hosdurg
orcid: 0009-0006-6812-7317
- first_name: Karen
full_name: Klein, Karen
id: 3E83A2F8-F248-11E8-B48F-1D18A9856A87
last_name: Klein
- 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: Michael
full_name: Walter, Michael
id: 488F98B0-F248-11E8-B48F-1D18A9856A87
last_name: Walter
orcid: 0000-0003-3186-2482
citation:
ama: 'Abusalah HM, Kamath Hosdurg C, Klein K, Pietrzak KZ, Walter M. Reversible
proofs of sequential work. In: Advances in Cryptology – EUROCRYPT 2019.
Vol 11477. Springer International Publishing; 2019:277-291. doi:10.1007/978-3-030-17656-3_10'
apa: 'Abusalah, H. M., Kamath Hosdurg, C., Klein, K., Pietrzak, K. Z., & Walter,
M. (2019). Reversible proofs of sequential work. In Advances in Cryptology
– EUROCRYPT 2019 (Vol. 11477, pp. 277–291). Darmstadt, Germany: Springer International
Publishing. https://doi.org/10.1007/978-3-030-17656-3_10'
chicago: Abusalah, Hamza M, Chethan Kamath Hosdurg, Karen Klein, Krzysztof Z Pietrzak,
and Michael Walter. “Reversible Proofs of Sequential Work.” In Advances in
Cryptology – EUROCRYPT 2019, 11477:277–91. Springer International Publishing,
2019. https://doi.org/10.1007/978-3-030-17656-3_10.
ieee: H. M. Abusalah, C. Kamath Hosdurg, K. Klein, K. Z. Pietrzak, and M. Walter,
“Reversible proofs of sequential work,” in Advances in Cryptology – EUROCRYPT
2019, Darmstadt, Germany, 2019, vol. 11477, pp. 277–291.
ista: 'Abusalah HM, Kamath Hosdurg C, Klein K, Pietrzak KZ, Walter M. 2019. Reversible
proofs of sequential work. Advances in Cryptology – EUROCRYPT 2019. EUROCRYPT:
International Conference on the Theory and Applications of Cryptographic Techniques,
LNCS, vol. 11477, 277–291.'
mla: Abusalah, Hamza M., et al. “Reversible Proofs of Sequential Work.” Advances
in Cryptology – EUROCRYPT 2019, vol. 11477, Springer International Publishing,
2019, pp. 277–91, doi:10.1007/978-3-030-17656-3_10.
short: H.M. Abusalah, C. Kamath Hosdurg, K. Klein, K.Z. Pietrzak, M. Walter, in:,
Advances in Cryptology – EUROCRYPT 2019, Springer International Publishing, 2019,
pp. 277–291.
conference:
end_date: 2019-05-23
location: Darmstadt, Germany
name: 'EUROCRYPT: International Conference on the Theory and Applications of Cryptographic
Techniques'
start_date: 2019-05-19
date_created: 2020-01-30T09:26:14Z
date_published: 2019-04-24T00:00:00Z
date_updated: 2026-04-16T10:27:47Z
day: '24'
department:
- _id: KrPi
doi: 10.1007/978-3-030-17656-3_10
ec_funded: 1
external_id:
isi:
- '000483516200010'
intvolume: ' 11477'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2019/252
month: '04'
oa: 1
oa_version: Submitted Version
page: 277-291
project:
- _id: 258AA5B2-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '682815'
name: Teaching Old Crypto New Tricks
publication: Advances in Cryptology – EUROCRYPT 2019
publication_identifier:
eisbn:
- '9783030176563'
eissn:
- 1611-3349
isbn:
- '9783030176556'
issn:
- 0302-9743
publication_status: published
publisher: Springer International Publishing
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reversible proofs of sequential work
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 11477
year: '2019'
...
---
_id: '7159'
abstract:
- lang: eng
text: 'Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a
tremendous amount of generated, measured and recorded time-series data. Extracting
temporal segments that encode patterns with useful information out of these huge
amounts of data is an extremely difficult problem. We propose shape expressions
as a declarative formalism for specifying, querying and extracting sophisticated
temporal patterns from possibly noisy data. Shape expressions are regular expressions
with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters
as atomic predicates and additional constraints on these parameters. We equip
shape expressions with a novel noisy semantics that combines regular expression
matching semantics with statistical regression. We characterize essential properties
of the formalism and propose an efficient approximate shape expression matching
procedure. We demonstrate the wide applicability of this technique on two case
studies. '
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Dejan
full_name: Ničković, Dejan
last_name: Ničković
- first_name: Xin
full_name: Qin, Xin
last_name: Qin
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Cristinel
full_name: Mateis, Cristinel
last_name: Mateis
- first_name: Jyotirmoy
full_name: Deshmukh, Jyotirmoy
last_name: Deshmukh
citation:
ama: 'Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. Shape expressions for
specifying and extracting signal features. In: 19th International Conference
on Runtime Verification. Vol 11757. Springer Nature; 2019:292-309. doi:10.1007/978-3-030-32079-9_17'
apa: 'Ničković, D., Qin, X., Ferrere, T., Mateis, C., & Deshmukh, J. (2019).
Shape expressions for specifying and extracting signal features. In 19th International
Conference on Runtime Verification (Vol. 11757, pp. 292–309). Porto, Portugal:
Springer Nature. https://doi.org/10.1007/978-3-030-32079-9_17'
chicago: Ničković, Dejan, Xin Qin, Thomas Ferrere, Cristinel Mateis, and Jyotirmoy
Deshmukh. “Shape Expressions for Specifying and Extracting Signal Features.” In
19th International Conference on Runtime Verification, 11757:292–309. Springer
Nature, 2019. https://doi.org/10.1007/978-3-030-32079-9_17.
ieee: D. Ničković, X. Qin, T. Ferrere, C. Mateis, and J. Deshmukh, “Shape expressions
for specifying and extracting signal features,” in 19th International Conference
on Runtime Verification, Porto, Portugal, 2019, vol. 11757, pp. 292–309.
ista: 'Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. 2019. Shape expressions
for specifying and extracting signal features. 19th International Conference on
Runtime Verification. RV: Runtime Verification, LNCS, vol. 11757, 292–309.'
mla: Ničković, Dejan, et al. “Shape Expressions for Specifying and Extracting Signal
Features.” 19th International Conference on Runtime Verification, vol.
11757, Springer Nature, 2019, pp. 292–309, doi:10.1007/978-3-030-32079-9_17.
short: D. Ničković, X. Qin, T. Ferrere, C. Mateis, J. Deshmukh, in:, 19th International
Conference on Runtime Verification, Springer Nature, 2019, pp. 292–309.
conference:
end_date: 2019-10-11
location: Porto, Portugal
name: 'RV: Runtime Verification'
start_date: 2019-10-08
date_created: 2019-12-09T08:47:55Z
date_published: 2019-10-01T00:00:00Z
date_updated: 2026-04-16T10:27:14Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-030-32079-9_17
external_id:
isi:
- '000570006300017'
intvolume: ' 11757'
isi: 1
language:
- iso: eng
month: '10'
oa_version: None
page: 292-309
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
publication: 19th International Conference on Runtime Verification
publication_identifier:
eisbn:
- '9783030320799'
isbn:
- '9783030320782'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Shape expressions for specifying and extracting signal features
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 11757
year: '2019'
...