---
_id: '9620'
abstract:
- lang: eng
text: "In this note, we introduce a distributed twist on the classic coupon collector
problem: a set of m collectors wish to each obtain a set of n coupons; for this,
they can each sample coupons uniformly at random, but can also meet in pairwise
interactions, during which they can exchange coupons. By doing so, they hope to
reduce the number of coupons that must be sampled by each collector in order to
obtain a full set. This extension is natural when considering real-world manifestations
of the coupon collector phenomenon, and has been remarked upon and studied empirically
(Hayes and Hannigan 2006, Ahmad et al. 2014, Delmarcelle 2019).\r\n\r\nWe provide
the first theoretical analysis for such a scenario. We find that “coupon collecting
with friends” can indeed significantly reduce the number of coupons each collector
must sample, and raises interesting connections to the more traditional variants
of the problem. While our analysis is in most cases asymptotically tight, there
are several open questions raised, regarding finer-grained analysis of both “coupon
collecting with friends,” and of a long-studied variant of the original problem
in which a collector requires multiple full sets of coupons."
acknowledgement: Peter Davies is supported by the European Union’s Horizon2020 research
and innovation programme under the Marie Skłodowska-Curie grant agreement No. 754411.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Dan-Adrian
full_name: Alistarh, Dan-Adrian
id: 4A899BFC-F248-11E8-B48F-1D18A9856A87
last_name: Alistarh
orcid: 0000-0003-3650-940X
- first_name: Peter
full_name: Davies, Peter
id: 11396234-BB50-11E9-B24C-90FCE5697425
last_name: Davies
orcid: 0000-0002-5646-9524
citation:
ama: 'Alistarh D-A, Davies P. Collecting coupons is faster with friends. In: Structural
Information and Communication Complexity. Vol 12810. Springer Nature; 2021:3-12.
doi:10.1007/978-3-030-79527-6_1'
apa: 'Alistarh, D.-A., & Davies, P. (2021). Collecting coupons is faster with
friends. In Structural Information and Communication Complexity (Vol. 12810,
pp. 3–12). Wrocław, Poland: Springer Nature. https://doi.org/10.1007/978-3-030-79527-6_1'
chicago: Alistarh, Dan-Adrian, and Peter Davies. “Collecting Coupons Is Faster with
Friends.” In Structural Information and Communication Complexity, 12810:3–12.
Springer Nature, 2021. https://doi.org/10.1007/978-3-030-79527-6_1.
ieee: D.-A. Alistarh and P. Davies, “Collecting coupons is faster with friends,”
in Structural Information and Communication Complexity, Wrocław, Poland,
2021, vol. 12810, pp. 3–12.
ista: 'Alistarh D-A, Davies P. 2021. Collecting coupons is faster with friends.
Structural Information and Communication Complexity. SIROCCO: International Colloquium
on Structural Information and Communication Complexity, LNCS, vol. 12810, 3–12.'
mla: Alistarh, Dan-Adrian, and Peter Davies. “Collecting Coupons Is Faster with
Friends.” Structural Information and Communication Complexity, vol. 12810,
Springer Nature, 2021, pp. 3–12, doi:10.1007/978-3-030-79527-6_1.
short: D.-A. Alistarh, P. Davies, in:, Structural Information and Communication
Complexity, Springer Nature, 2021, pp. 3–12.
conference:
end_date: 2021-07-01
location: Wrocław, Poland
name: ' SIROCCO: International Colloquium on Structural Information and Communication
Complexity'
start_date: 2021-06-28
date_created: 2021-07-01T11:04:43Z
date_published: 2021-06-20T00:00:00Z
date_updated: 2023-02-23T14:02:46Z
day: '20'
ddc:
- '000'
department:
- _id: DaAl
doi: 10.1007/978-3-030-79527-6_1
ec_funded: 1
file:
- access_level: open_access
checksum: fe37fb9af3f5016c1084af9d6e7109bd
content_type: application/pdf
creator: pdavies
date_created: 2021-07-01T11:21:40Z
date_updated: 2021-07-01T11:21:40Z
file_id: '9621'
file_name: Population_Coupon_Collector.pdf
file_size: 319728
relation: main_file
file_date_updated: 2021-07-01T11:21:40Z
has_accepted_license: '1'
intvolume: ' 12810'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Preprint
page: 3-12
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: Structural Information and Communication Complexity
publication_identifier:
eisbn:
- '9783030795276'
eissn:
- 1611-3349
isbn:
- '9783030795269'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Collecting coupons is faster with friends
type: conference
user_id: D865714E-FA4E-11E9-B85B-F5C5E5697425
volume: 12810
year: '2021'
...
---
_id: '9987'
abstract:
- lang: eng
text: 'Stateless model checking (SMC) is one of the standard approaches to the verification
of concurrent programs. As scheduling non-determinism creates exponentially large
spaces of thread interleavings, SMC attempts to partition this space into equivalence
classes and explore only a few representatives from each class. The efficiency
of this approach depends on two factors: (a) the coarseness of the partitioning,
and (b) the time to generate representatives in each class. For this reason, the
search for coarse partitionings that are efficiently explorable is an active research
challenge. In this work we present RVF-SMC , a new SMC algorithm that uses a
novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are
deemed equivalent if they agree on the value obtained in each read event, and
read events induce consistent causal orderings between them. The RVF partitioning
is provably coarser than recent approaches based on Mazurkiewicz and “reads-from”
partitionings. Our experimental evaluation reveals that RVF is quite often a very
effective equivalence, as the underlying partitioning is exponentially coarser
than other approaches. Moreover, RVF-SMC generates representatives very efficiently,
as the reduction in the partitioning is often met with significant speed-ups in
the model checking task.'
acknowledgement: The research was partially funded by the ERC CoG 863818 (ForM-SMArt)
and the Vienna Science and Technology Fund (WWTF) through project ICT15-003.
alternative_title:
- LNCS
article_processing_charge: Yes
arxiv: 1
author:
- first_name: Pratyush
full_name: Agarwal, Pratyush
last_name: Agarwal
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Shreya
full_name: Pathak, Shreya
last_name: Pathak
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Viktor
full_name: Toman, Viktor
id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
last_name: Toman
orcid: 0000-0001-9036-063X
citation:
ama: 'Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. Stateless model
checking under a reads-value-from equivalence. In: 33rd International Conference
on Computer-Aided Verification . Vol 12759. Springer Nature; 2021:341-366.
doi:10.1007/978-3-030-81685-8_16'
apa: 'Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., & Toman, V.
(2021). Stateless model checking under a reads-value-from equivalence. In 33rd
International Conference on Computer-Aided Verification (Vol. 12759, pp.
341–366). Virtual: Springer Nature. https://doi.org/10.1007/978-3-030-81685-8_16'
chicago: Agarwal, Pratyush, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis,
and Viktor Toman. “Stateless Model Checking under a Reads-Value-from Equivalence.”
In 33rd International Conference on Computer-Aided Verification , 12759:341–66.
Springer Nature, 2021. https://doi.org/10.1007/978-3-030-81685-8_16.
ieee: P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, and V. Toman, “Stateless
model checking under a reads-value-from equivalence,” in 33rd International
Conference on Computer-Aided Verification , Virtual, 2021, vol. 12759, pp.
341–366.
ista: 'Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. 2021. Stateless
model checking under a reads-value-from equivalence. 33rd International Conference
on Computer-Aided Verification . CAV: Computer Aided Verification , LNCS, vol.
12759, 341–366.'
mla: Agarwal, Pratyush, et al. “Stateless Model Checking under a Reads-Value-from
Equivalence.” 33rd International Conference on Computer-Aided Verification
, vol. 12759, Springer Nature, 2021, pp. 341–66, doi:10.1007/978-3-030-81685-8_16.
short: P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, V. Toman, in:, 33rd
International Conference on Computer-Aided Verification , Springer Nature, 2021,
pp. 341–366.
conference:
end_date: 2021-07-23
location: Virtual
name: 'CAV: Computer Aided Verification '
start_date: 2021-07-20
date_created: 2021-09-05T22:01:24Z
date_published: 2021-07-15T00:00:00Z
date_updated: 2025-07-14T09:10:15Z
day: '15'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-030-81685-8_16
ec_funded: 1
external_id:
arxiv:
- '2105.06424'
isi:
- '000698732400016'
file:
- access_level: open_access
checksum: 4b346e5fbaa8b9bdf107819c7b2aadee
content_type: application/pdf
creator: dernst
date_created: 2022-05-13T07:00:20Z
date_updated: 2022-05-13T07:00:20Z
file_id: '11368'
file_name: 2021_LNCS_Agarwal.pdf
file_size: 1516756
relation: main_file
success: 1
file_date_updated: 2022-05-13T07:00:20Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 341-366
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: '33rd International Conference on Computer-Aided Verification '
publication_identifier:
eisbn:
- 978-3-030-81685-8
eissn:
- 1611-3349
isbn:
- 978-3-030-81684-1
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '10199'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Stateless model checking under a reads-value-from equivalence
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: '12759 '
year: '2021'
...
---
_id: '11771'
abstract:
- lang: eng
text: "Classic dynamic data structure problems maintain a data structure subject
to a sequence S of updates and they answer queries using the latest version of
the data structure, i.e., the data structure after processing the whole sequence.
To handle operations that change the sequence S of updates, Demaine et al. [7]
introduced retroactive data structures (RDS). A retroactive operation modifies
the update sequence S in a given position t, called time, and either creates or
cancels an update in S at time t. A fully retroactive data structure supports
queries at any time t: a query at time t is answered using only the updates of
S up to time t. While efficient RDS have been proposed for classic data structures,
e.g., stack, priority queue and binary search tree, the retroactive version of
graph problems are rarely studied.\r\n\r\nIn this paper we study retroactive graph
problems including connectivity, minimum spanning forest (MSF), maximum degree,
etc. We show that under the OMv conjecture (proposed by Henzinger et al. [15]),
there does not exist fully RDS maintaining connectivity or MSF, or incremental
fully RDS maintaining the maximum degree with \U0001D442(\U0001D45B1−\U0001D716)
time per operation, for any constant \U0001D716>0. Furthermore, We provide RDS
with almost tight time per operation. We give fully RDS for maintaining the maximum
degree, connectivity and MSF in \U0001D442̃ (\U0001D45B) time per operation. We
also give an algorithm for the incremental (insertion-only) fully retroactive
connectivity with \U0001D442̃ (1) time per operation, showing that the lower bound
cannot be extended to this setting.\r\n\r\nWe also study a restricted version
of RDS, where the only change to S is the swap of neighboring updates and show
that for this problem we can beat the above hardness result. This also implies
the first non-trivial dynamic Reeb graph computation algorithm."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Xiaowei
full_name: Wu, Xiaowei
last_name: Wu
citation:
ama: 'Henzinger MH, Wu X. Upper and lower bounds for fully retroactive graph problems.
In: 17th International Symposium on Algorithms and Data Structures. Vol
12808. Springer Nature; 2021:471–484. doi:10.1007/978-3-030-83508-8_34'
apa: 'Henzinger, M. H., & Wu, X. (2021). Upper and lower bounds for fully retroactive
graph problems. In 17th International Symposium on Algorithms and Data Structures
(Vol. 12808, pp. 471–484). Virtual: Springer Nature. https://doi.org/10.1007/978-3-030-83508-8_34'
chicago: Henzinger, Monika H, and Xiaowei Wu. “Upper and Lower Bounds for Fully
Retroactive Graph Problems.” In 17th International Symposium on Algorithms
and Data Structures, 12808:471–484. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-83508-8_34.
ieee: M. H. Henzinger and X. Wu, “Upper and lower bounds for fully retroactive graph
problems,” in 17th International Symposium on Algorithms and Data Structures,
Virtual, 2021, vol. 12808, pp. 471–484.
ista: 'Henzinger MH, Wu X. 2021. Upper and lower bounds for fully retroactive graph
problems. 17th International Symposium on Algorithms and Data Structures. WADS:
Workshop on Algorithms and Data Structures, LNCS, vol. 12808, 471–484.'
mla: Henzinger, Monika H., and Xiaowei Wu. “Upper and Lower Bounds for Fully Retroactive
Graph Problems.” 17th International Symposium on Algorithms and Data Structures,
vol. 12808, Springer Nature, 2021, pp. 471–484, doi:10.1007/978-3-030-83508-8_34.
short: M.H. Henzinger, X. Wu, in:, 17th International Symposium on Algorithms and
Data Structures, Springer Nature, 2021, pp. 471–484.
conference:
end_date: 2021-08-11
location: Virtual
name: 'WADS: Workshop on Algorithms and Data Structures'
start_date: 2021-08-09
date_created: 2022-08-08T13:01:29Z
date_published: 2021-08-09T00:00:00Z
date_updated: 2023-02-10T08:31:50Z
day: '09'
doi: 10.1007/978-3-030-83508-8_34
extern: '1'
external_id:
arxiv:
- '1910.03332'
intvolume: ' 12808'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1910.03332
month: '08'
oa: 1
oa_version: Preprint
page: 471–484
publication: 17th International Symposium on Algorithms and Data Structures
publication_identifier:
eisbn:
- '9783030835088'
eissn:
- 1611-3349
isbn:
- '9783030835071'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Upper and lower bounds for fully retroactive graph problems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 12808
year: '2021'
...
---
_id: '8623'
abstract:
- lang: eng
text: We introduce the monitoring of trace properties under assumptions. An assumption
limits the space of possible traces that the monitor may encounter. An assumption
may result from knowledge about the system that is being monitored, about the
environment, or about another, connected monitor. We define monitorability under
assumptions and study its theoretical properties. In particular, we show that
for every assumption A, the boolean combinations of properties that are safe or
co-safe relative to A are monitorable under A. We give several examples and constructions
on how an assumption can make a non-monitorable property monitorable, and how
an assumption can make a monitorable property monitorable with fewer resources,
such as integer registers.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Sarac NE. Monitorability under assumptions. In: Runtime Verification.
Vol 12399. Springer Nature; 2020:3-18. doi:10.1007/978-3-030-60508-7_1'
apa: 'Henzinger, T. A., & Sarac, N. E. (2020). Monitorability under assumptions.
In Runtime Verification (Vol. 12399, pp. 3–18). Los Angeles, CA, United
States: Springer Nature. https://doi.org/10.1007/978-3-030-60508-7_1'
chicago: Henzinger, Thomas A, and Naci E Sarac. “Monitorability under Assumptions.”
In Runtime Verification, 12399:3–18. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-60508-7_1.
ieee: T. A. Henzinger and N. E. Sarac, “Monitorability under assumptions,” in Runtime
Verification, Los Angeles, CA, United States, 2020, vol. 12399, pp. 3–18.
ista: 'Henzinger TA, Sarac NE. 2020. Monitorability under assumptions. Runtime Verification.
RV: Runtime Verification, LNCS, vol. 12399, 3–18.'
mla: Henzinger, Thomas A., and Naci E. Sarac. “Monitorability under Assumptions.”
Runtime Verification, vol. 12399, Springer Nature, 2020, pp. 3–18, doi:10.1007/978-3-030-60508-7_1.
short: T.A. Henzinger, N.E. Sarac, in:, Runtime Verification, Springer Nature, 2020,
pp. 3–18.
conference:
end_date: 2020-10-09
location: Los Angeles, CA, United States
name: 'RV: Runtime Verification'
start_date: 2020-10-06
date_created: 2020-10-07T15:05:37Z
date_published: 2020-10-02T00:00:00Z
date_updated: 2023-09-05T15:08:26Z
day: '02'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-60508-7_1
external_id:
isi:
- '000728160600001'
file:
- access_level: open_access
checksum: 00661f9b7034f52e18bf24fa552b8194
content_type: application/pdf
creator: esarac
date_created: 2020-10-15T14:28:06Z
date_updated: 2020-10-15T14:28:06Z
file_id: '8665'
file_name: monitorability.pdf
file_size: 478148
relation: main_file
success: 1
file_date_updated: 2020-10-15T14:28:06Z
has_accepted_license: '1'
intvolume: ' 12399'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 3-18
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Runtime Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030605070'
- '9783030605087'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitorability under assumptions
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 12399
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: 2025-06-02T08:53:43Z
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 Probablistic 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: '8732'
abstract:
- lang: eng
text: 'A simple drawing D(G) of a graph G is one where each pair of edges share
at most one point: either a common endpoint or a proper crossing. An edge e in
the complement of G can be inserted into D(G) if there exists a simple drawing
of G+e extending D(G). As a result of Levi’s Enlargement Lemma, if a drawing
is rectilinear (pseudolinear), that is, the edges can be extended into an arrangement
of lines (pseudolines), then any edge in the complement of G can be inserted.
In contrast, we show that it is NP -complete to decide whether one edge can
be inserted into a simple drawing. This remains true even if we assume that the
drawing is pseudocircular, that is, the edges can be extended to an arrangement
of pseudocircles. On the positive side, we show that, given an arrangement of
pseudocircles A and a pseudosegment σ , it can be decided in polynomial time
whether there exists a pseudocircle Φσ extending σ for which A∪{Φσ} is
again an arrangement of pseudocircles.'
alternative_title:
- LNCS
article_processing_charge: No
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: Fabian
full_name: Klute, Fabian
last_name: Klute
- first_name: Irene
full_name: Parada, Irene
last_name: Parada
- first_name: Raimund
full_name: Seidel, Raimund
last_name: Seidel
- first_name: Birgit
full_name: Vogtenhuber, Birgit
last_name: Vogtenhuber
- first_name: Tilo
full_name: Wiedera, Tilo
last_name: Wiedera
citation:
ama: 'Arroyo Guevara AM, Klute F, Parada I, Seidel R, Vogtenhuber B, Wiedera T.
Inserting one edge into a simple drawing is hard. In: Graph-Theoretic Concepts
in Computer Science. Vol 12301. Springer Nature; 2020:325-338. doi:10.1007/978-3-030-60440-0_26'
apa: 'Arroyo Guevara, A. M., Klute, F., Parada, I., Seidel, R., Vogtenhuber, B.,
& Wiedera, T. (2020). Inserting one edge into a simple drawing is hard. In
Graph-Theoretic Concepts in Computer Science (Vol. 12301, pp. 325–338).
Leeds, United Kingdom: Springer Nature. https://doi.org/10.1007/978-3-030-60440-0_26'
chicago: Arroyo Guevara, Alan M, Fabian Klute, Irene Parada, Raimund Seidel, Birgit
Vogtenhuber, and Tilo Wiedera. “Inserting One Edge into a Simple Drawing Is Hard.”
In Graph-Theoretic Concepts in Computer Science, 12301:325–38. Springer
Nature, 2020. https://doi.org/10.1007/978-3-030-60440-0_26.
ieee: A. M. Arroyo Guevara, F. Klute, I. Parada, R. Seidel, B. Vogtenhuber, and
T. Wiedera, “Inserting one edge into a simple drawing is hard,” in Graph-Theoretic
Concepts in Computer Science, Leeds, United Kingdom, 2020, vol. 12301, pp.
325–338.
ista: 'Arroyo Guevara AM, Klute F, Parada I, Seidel R, Vogtenhuber B, Wiedera T.
2020. Inserting one edge into a simple drawing is hard. Graph-Theoretic Concepts
in Computer Science. WG: Workshop on Graph-Theoretic Concepts in Computer Science,
LNCS, vol. 12301, 325–338.'
mla: Arroyo Guevara, Alan M., et al. “Inserting One Edge into a Simple Drawing Is
Hard.” Graph-Theoretic Concepts in Computer Science, vol. 12301, Springer
Nature, 2020, pp. 325–38, doi:10.1007/978-3-030-60440-0_26.
short: A.M. Arroyo Guevara, F. Klute, I. Parada, R. Seidel, B. Vogtenhuber, T. Wiedera,
in:, Graph-Theoretic Concepts in Computer Science, Springer Nature, 2020, pp.
325–338.
conference:
end_date: 2020-06-26
location: Leeds, United Kingdom
name: 'WG: Workshop on Graph-Theoretic Concepts in Computer Science'
start_date: 2020-06-24
date_created: 2020-11-06T08:45:03Z
date_published: 2020-10-09T00:00:00Z
date_updated: 2023-09-05T15:09:16Z
day: '09'
department:
- _id: UlWa
doi: 10.1007/978-3-030-60440-0_26
ec_funded: 1
intvolume: ' 12301'
language:
- iso: eng
month: '10'
oa_version: None
page: 325-338
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: Graph-Theoretic Concepts in Computer Science
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030604394'
- '9783030604400'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Inserting one edge into a simple drawing is hard
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 12301
year: '2020'
...
---
_id: '9299'
abstract:
- lang: eng
text: We call a multigraph non-homotopic if it can be drawn in the plane in such
a way that no two edges connecting the same pair of vertices can be continuously
transformed into each other without passing through a vertex, and no loop can
be shrunk to its end-vertex in the same way. It is easy to see that a non-homotopic
multigraph on n>1 vertices can have arbitrarily many edges. We prove that the
number of crossings between the edges of a non-homotopic multigraph with n vertices
and m>4n edges is larger than cm2n for some constant c>0 , and that this
bound is tight up to a polylogarithmic factor. We also show that the lower bound
is not asymptotically sharp as n is fixed and m⟶∞ .
acknowledgement: Supported by the National Research, Development and Innovation Office,
NKFIH, KKP-133864, K-131529, K-116769, K-132696, by the Higher Educational Institutional
Excellence Program 2019 NKFIH-1158-6/2019, the Austrian Science Fund (FWF), grant
Z 342-N31, by the Ministry of Education and Science of the Russian Federation MegaGrant
No. 075-15-2019-1926, and by the ERC Synergy Grant “Dynasnet” No. 810115. A full
version can be found at https://arxiv.org/abs/2006.14908.
article_processing_charge: No
arxiv: 1
author:
- first_name: János
full_name: Pach, János
id: E62E3130-B088-11EA-B919-BF823C25FEA4
last_name: Pach
- first_name: Gábor
full_name: Tardos, Gábor
last_name: Tardos
- first_name: Géza
full_name: Tóth, Géza
last_name: Tóth
citation:
ama: 'Pach J, Tardos G, Tóth G. Crossings between non-homotopic edges. In: 28th
International Symposium on Graph Drawing and Network Visualization. Vol 12590.
LNCS. Springer Nature; 2020:359-371. doi:10.1007/978-3-030-68766-3_28'
apa: 'Pach, J., Tardos, G., & Tóth, G. (2020). Crossings between non-homotopic
edges. In 28th International Symposium on Graph Drawing and Network Visualization
(Vol. 12590, pp. 359–371). Virtual, Online: Springer Nature. https://doi.org/10.1007/978-3-030-68766-3_28'
chicago: Pach, János, Gábor Tardos, and Géza Tóth. “Crossings between Non-Homotopic
Edges.” In 28th International Symposium on Graph Drawing and Network Visualization,
12590:359–71. LNCS. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-68766-3_28.
ieee: J. Pach, G. Tardos, and G. Tóth, “Crossings between non-homotopic edges,”
in 28th International Symposium on Graph Drawing and Network Visualization,
Virtual, Online, 2020, vol. 12590, pp. 359–371.
ista: 'Pach J, Tardos G, Tóth G. 2020. Crossings between non-homotopic edges. 28th
International Symposium on Graph Drawing and Network Visualization. GD: Graph
Drawing and Network VisualizationLNCS vol. 12590, 359–371.'
mla: Pach, János, et al. “Crossings between Non-Homotopic Edges.” 28th International
Symposium on Graph Drawing and Network Visualization, vol. 12590, Springer
Nature, 2020, pp. 359–71, doi:10.1007/978-3-030-68766-3_28.
short: J. Pach, G. Tardos, G. Tóth, in:, 28th International Symposium on Graph Drawing
and Network Visualization, Springer Nature, 2020, pp. 359–371.
conference:
end_date: 2020-09-18
location: Virtual, Online
name: 'GD: Graph Drawing and Network Visualization'
start_date: 2020-09-16
date_created: 2021-03-28T22:01:44Z
date_published: 2020-09-20T00:00:00Z
date_updated: 2021-04-06T11:32:32Z
day: '20'
department:
- _id: HeEd
doi: 10.1007/978-3-030-68766-3_28
external_id:
arxiv:
- '2006.14908'
intvolume: ' 12590'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2006.14908
month: '09'
oa: 1
oa_version: Preprint
page: 359-371
project:
- _id: 268116B8-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z00342
name: The Wittgenstein Prize
publication: 28th International Symposium on Graph Drawing and Network Visualization
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030687656'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Crossings between non-homotopic edges
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 12590
year: '2020'
...
---
_id: '7966'
abstract:
- lang: eng
text: "For 1≤m≤n, we consider a natural m-out-of-n multi-instance scenario for a
public-key encryption (PKE) scheme. An adversary, given n independent instances
of PKE, wins if he breaks at least m out of the n instances. In this work, we
are interested in the scaling factor of PKE schemes, SF, which measures how well
the difficulty of breaking m out of the n instances scales in m. That is, a scaling
factor SF=ℓ indicates that breaking m out of n instances is at least ℓ times more
difficult than breaking one single instance. A PKE scheme with small scaling factor
hence provides an ideal target for mass surveillance. In fact, the Logjam attack
(CCS 2015) implicitly exploited, among other things, an almost constant scaling
factor of ElGamal over finite fields (with shared group parameters).\r\n\r\nFor
Hashed ElGamal over elliptic curves, we use the generic group model to argue that
the scaling factor depends on the scheme's granularity. In low granularity, meaning
each public key contains its independent group parameter, the scheme has optimal
scaling factor SF=m; In medium and high granularity, meaning all public keys share
the same group parameter, the scheme still has a reasonable scaling factor SF=√m.
Our findings underline that instantiating ElGamal over elliptic curves should
be preferred to finite fields in a multi-instance scenario.\r\n\r\nAs our main
technical contribution, we derive new generic-group lower bounds of Ω(√(mp)) on
the difficulty of solving both the m-out-of-n Gap Discrete Logarithm and the m-out-of-n
Gap Computational Diffie-Hellman problem over groups of prime order p, extending
a recent result by Yun (EUROCRYPT 2015). We establish the lower bound by studying
the hardness of a related computational problem which we call the search-by-hypersurface
problem."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Benedikt
full_name: Auerbach, Benedikt
id: D33D2B18-E445-11E9-ABB7-15F4E5697425
last_name: Auerbach
orcid: 0000-0002-7553-6606
- first_name: Federico
full_name: Giacon, Federico
last_name: Giacon
- first_name: Eike
full_name: Kiltz, Eike
last_name: Kiltz
citation:
ama: 'Auerbach B, Giacon F, Kiltz E. Everybody’s a target: Scalability in public-key
encryption. In: Advances in Cryptology – EUROCRYPT 2020. Vol 12107. Springer
Nature; 2020:475-506. doi:10.1007/978-3-030-45727-3_16'
apa: 'Auerbach, B., Giacon, F., & Kiltz, E. (2020). Everybody’s a target: Scalability
in public-key encryption. In Advances in Cryptology – EUROCRYPT 2020 (Vol.
12107, pp. 475–506). Springer Nature. https://doi.org/10.1007/978-3-030-45727-3_16'
chicago: 'Auerbach, Benedikt, Federico Giacon, and Eike Kiltz. “Everybody’s a Target:
Scalability in Public-Key Encryption.” In Advances in Cryptology – EUROCRYPT
2020, 12107:475–506. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-45727-3_16.'
ieee: 'B. Auerbach, F. Giacon, and E. Kiltz, “Everybody’s a target: Scalability
in public-key encryption,” in Advances in Cryptology – EUROCRYPT 2020,
2020, vol. 12107, pp. 475–506.'
ista: 'Auerbach B, Giacon F, Kiltz E. 2020. Everybody’s a target: Scalability in
public-key encryption. Advances in Cryptology – EUROCRYPT 2020. EUROCRYPT: Theory
and Applications of Cryptographic Techniques, LNCS, vol. 12107, 475–506.'
mla: 'Auerbach, Benedikt, et al. “Everybody’s a Target: Scalability in Public-Key
Encryption.” Advances in Cryptology – EUROCRYPT 2020, vol. 12107, Springer
Nature, 2020, pp. 475–506, doi:10.1007/978-3-030-45727-3_16.'
short: B. Auerbach, F. Giacon, E. Kiltz, in:, Advances in Cryptology – EUROCRYPT
2020, Springer Nature, 2020, pp. 475–506.
conference:
end_date: 2020-05-15
name: 'EUROCRYPT: Theory and Applications of Cryptographic Techniques'
start_date: 2020-05-11
date_created: 2020-06-15T07:13:37Z
date_published: 2020-05-01T00:00:00Z
date_updated: 2023-09-05T15:06:40Z
day: '01'
department:
- _id: KrPi
doi: 10.1007/978-3-030-45727-3_16
ec_funded: 1
external_id:
isi:
- '000828688000016'
intvolume: ' 12107'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2019/364
month: '05'
oa: 1
oa_version: Submitted Version
page: 475-506
project:
- _id: 258AA5B2-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '682815'
name: Teaching Old Crypto New Tricks
publication: Advances in Cryptology – EUROCRYPT 2020
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030457266'
- '9783030457273'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: 'Everybody’s a target: Scalability in public-key encryption'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 12107
year: '2020'
...
---
_id: '8195'
abstract:
- lang: eng
text: This paper presents a foundation for refining concurrent programs with structured
control flow. The verification problem is decomposed into subproblems that aid
interactive program development, proof reuse, and automation. The formalization
in this paper is the basis of a new design and implementation of the Civl verifier.
acknowledgement: "Bernhard Kragl and Thomas A. Henzinger were supported by\r\nthe
Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award)."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
orcid: 0000-0001-7745-9117
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- 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: 'Kragl B, Qadeer S, Henzinger TA. Refinement for structured concurrent programs.
In: Computer Aided Verification. Vol 12224. Springer Nature; 2020:275-298.
doi:10.1007/978-3-030-53288-8_14'
apa: Kragl, B., Qadeer, S., & Henzinger, T. A. (2020). Refinement for structured
concurrent programs. In Computer Aided Verification (Vol. 12224, pp. 275–298).
Springer Nature. https://doi.org/10.1007/978-3-030-53288-8_14
chicago: Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Refinement for Structured
Concurrent Programs.” In Computer Aided Verification, 12224:275–98. Springer
Nature, 2020. https://doi.org/10.1007/978-3-030-53288-8_14.
ieee: B. Kragl, S. Qadeer, and T. A. Henzinger, “Refinement for structured concurrent
programs,” in Computer Aided Verification, 2020, vol. 12224, pp. 275–298.
ista: Kragl B, Qadeer S, Henzinger TA. 2020. Refinement for structured concurrent
programs. Computer Aided Verification. , LNCS, vol. 12224, 275–298.
mla: Kragl, Bernhard, et al. “Refinement for Structured Concurrent Programs.” Computer
Aided Verification, vol. 12224, Springer Nature, 2020, pp. 275–98, doi:10.1007/978-3-030-53288-8_14.
short: B. Kragl, S. Qadeer, T.A. Henzinger, in:, Computer Aided Verification, Springer
Nature, 2020, pp. 275–298.
date_created: 2020-08-03T11:45:35Z
date_published: 2020-07-14T00:00:00Z
date_updated: 2023-09-07T13:18:00Z
day: '14'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-53288-8_14
external_id:
isi:
- '000695276000014'
file:
- access_level: open_access
content_type: application/pdf
creator: dernst
date_created: 2020-08-06T08:14:54Z
date_updated: 2020-08-06T08:14:54Z
file_id: '8201'
file_name: 2020_LNCS_Kragl.pdf
file_size: 804237
relation: main_file
success: 1
file_date_updated: 2020-08-06T08:14:54Z
has_accepted_license: '1'
intvolume: ' 12224'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 275-298
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Computer Aided Verification
publication_identifier:
eisbn:
- '9783030532888'
eissn:
- 1611-3349
isbn:
- '9783030532871'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '8332'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Refinement for structured concurrent programs
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 12224
year: '2020'
...
---
_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.
date_created: 2022-03-18T11:35:51Z
date_published: 2020-04-29T00:00:00Z
date_updated: 2023-09-05T15:10:02Z
day: '29'
doi: 10.1007/978-3-030-45374-9_8
editor:
- first_name: A
full_name: Kiayias, A
last_name: Kiayias
intvolume: ' 12110'
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:
eissn:
- 1611-3349
isbn:
- '9783030453732'
- '9783030453749'
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 12110
year: '2020'
...
---
_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
- 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: 2023-09-06T11:18:08Z
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: The Wittgenstein Prize
- _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:
eissn:
- 1611-3349
isbn:
- '9783030313036'
- '9783030313043'
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11773
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: 2023-09-06T14:56:00Z
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: 2023-09-06T14:55:15Z
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: The Wittgenstein Prize
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: 2023-09-06T14:57:17Z
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: The Wittgenstein Prize
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: '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
- 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. 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: 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: 2023-09-06T15:26:06Z
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:
eissn:
- 1611-3349
isbn:
- '9783030176556'
- '9783030176563'
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11477
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: 2024-02-22T14:57:29Z
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: '6941'
abstract:
- lang: eng
text: "Bitcoin has become the most successful cryptocurrency ever deployed, and
its most distinctive feature is that it is decentralized. Its underlying protocol
(Nakamoto consensus) achieves this by using proof of work, which has the drawback
that it causes the consumption of vast amounts of energy to maintain the ledger.
Moreover, Bitcoin mining dynamics have become less distributed over time.\r\n\r\nTowards
addressing these issues, we propose SpaceMint, a cryptocurrency based on proofs
of space instead of proofs of work. Miners in SpaceMint dedicate disk space rather
than computation. We argue that SpaceMint’s design solves or alleviates several
of Bitcoin’s issues: most notably, its large energy consumption. SpaceMint also
rewards smaller miners fairly according to their contribution to the network,
thus incentivizing more distributed participation.\r\n\r\nThis paper adapts proof
of space to enable its use in cryptocurrency, studies the attacks that can arise
against a Bitcoin-like blockchain that uses proof of space, and proposes a new
blockchain format and transaction types to address these attacks. Our prototype
shows that initializing 1 TB for mining takes about a day (a one-off setup cost),
and miners spend on average just a fraction of a second per block mined. Finally,
we provide a game-theoretic analysis modeling SpaceMint as an extensive game (the
canonical game-theoretic notion for games that take place over time) and show
that this stylized game satisfies a strong equilibrium notion, thereby arguing
for SpaceMint ’s stability and consensus."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sunoo
full_name: Park, Sunoo
last_name: Park
- first_name: Albert
full_name: Kwon, Albert
last_name: Kwon
- first_name: Georg
full_name: Fuchsbauer, Georg
id: 46B4C3EE-F248-11E8-B48F-1D18A9856A87
last_name: Fuchsbauer
- first_name: Peter
full_name: Gazi, Peter
id: 3E0BFE38-F248-11E8-B48F-1D18A9856A87
last_name: Gazi
- first_name: Joel F
full_name: Alwen, Joel F
id: 2A8DFA8C-F248-11E8-B48F-1D18A9856A87
last_name: Alwen
- 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: 'Park S, Kwon A, Fuchsbauer G, Gazi P, Alwen JF, Pietrzak KZ. SpaceMint: A
cryptocurrency based on proofs of space. In: 22nd International Conference
on Financial Cryptography and Data Security. Vol 10957. Springer Nature; 2018:480-499.
doi:10.1007/978-3-662-58387-6_26'
apa: 'Park, S., Kwon, A., Fuchsbauer, G., Gazi, P., Alwen, J. F., & Pietrzak,
K. Z. (2018). SpaceMint: A cryptocurrency based on proofs of space. In 22nd
International Conference on Financial Cryptography and Data Security (Vol.
10957, pp. 480–499). Nieuwpoort, Curacao: Springer Nature. https://doi.org/10.1007/978-3-662-58387-6_26'
chicago: 'Park, Sunoo, Albert Kwon, Georg Fuchsbauer, Peter Gazi, Joel F Alwen,
and Krzysztof Z Pietrzak. “SpaceMint: A Cryptocurrency Based on Proofs of Space.”
In 22nd International Conference on Financial Cryptography and Data Security,
10957:480–99. Springer Nature, 2018. https://doi.org/10.1007/978-3-662-58387-6_26.'
ieee: 'S. Park, A. Kwon, G. Fuchsbauer, P. Gazi, J. F. Alwen, and K. Z. Pietrzak,
“SpaceMint: A cryptocurrency based on proofs of space,” in 22nd International
Conference on Financial Cryptography and Data Security, Nieuwpoort, Curacao,
2018, vol. 10957, pp. 480–499.'
ista: 'Park S, Kwon A, Fuchsbauer G, Gazi P, Alwen JF, Pietrzak KZ. 2018. SpaceMint:
A cryptocurrency based on proofs of space. 22nd International Conference on Financial
Cryptography and Data Security. FC: Financial Cryptography and Data Security,
LNCS, vol. 10957, 480–499.'
mla: 'Park, Sunoo, et al. “SpaceMint: A Cryptocurrency Based on Proofs of Space.”
22nd International Conference on Financial Cryptography and Data Security,
vol. 10957, Springer Nature, 2018, pp. 480–99, doi:10.1007/978-3-662-58387-6_26.'
short: S. Park, A. Kwon, G. Fuchsbauer, P. Gazi, J.F. Alwen, K.Z. Pietrzak, in:,
22nd International Conference on Financial Cryptography and Data Security, Springer
Nature, 2018, pp. 480–499.
conference:
end_date: 2018-03-02
location: Nieuwpoort, Curacao
name: 'FC: Financial Cryptography and Data Security'
start_date: 2018-02-26
date_created: 2019-10-14T06:35:38Z
date_published: 2018-12-07T00:00:00Z
date_updated: 2023-09-19T15:02:13Z
day: '07'
department:
- _id: KrPi
doi: 10.1007/978-3-662-58387-6_26
ec_funded: 1
external_id:
isi:
- '000540656400026'
intvolume: ' 10957'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2015/528
month: '12'
oa: 1
oa_version: Submitted Version
page: 480-499
project:
- _id: 258AA5B2-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '682815'
name: Teaching Old Crypto New Tricks
publication: 22nd International Conference on Financial Cryptography and Data Security
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783662583869'
- '9783662583876'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'SpaceMint: A cryptocurrency based on proofs of space'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10957
year: '2018'
...
---
_id: '6164'
abstract:
- lang: eng
text: In this paper, we propose an algorithm to build discrete spherical shell having
integer center and real-valued inner and outer radii on the face-centered cubic
(FCC) grid. We address the problem by mapping it to a 2D scenario and building
the shell layer by layer on hexagonal grids with additive manufacturing in mind.
The layered hexagonal grids get shifted according to need as we move from one
layer to another and forms the FCC grid in 3D. However, we restrict our computation
strictly to 2D in order to utilize symmetry and simplicity.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Girish
full_name: Koshti, Girish
last_name: Koshti
- 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
- first_name: Partha
full_name: Bhowmick, Partha
last_name: Bhowmick
citation:
ama: 'Koshti G, Biswas R, Largeteau-Skapin G, Zrour R, Andres E, Bhowmick P. Sphere
construction on the FCC grid interpreted as layered hexagonal grids in 3D. In:
19th International Workshop. Vol 11255. Cham: Springer; 2018:82-96. doi:10.1007/978-3-030-05288-1_7'
apa: 'Koshti, G., Biswas, R., Largeteau-Skapin, G., Zrour, R., Andres, E., &
Bhowmick, P. (2018). Sphere construction on the FCC grid interpreted as layered
hexagonal grids in 3D. In 19th International Workshop (Vol. 11255, pp.
82–96). Cham: Springer. https://doi.org/10.1007/978-3-030-05288-1_7'
chicago: 'Koshti, Girish, Ranita Biswas, Gaëlle Largeteau-Skapin, Rita Zrour, Eric
Andres, and Partha Bhowmick. “Sphere Construction on the FCC Grid Interpreted
as Layered Hexagonal Grids in 3D.” In 19th International Workshop, 11255:82–96.
Cham: Springer, 2018. https://doi.org/10.1007/978-3-030-05288-1_7.'
ieee: G. Koshti, R. Biswas, G. Largeteau-Skapin, R. Zrour, E. Andres, and P. Bhowmick,
“Sphere construction on the FCC grid interpreted as layered hexagonal grids in
3D,” in 19th International Workshop, Porto, Portugal, 2018, vol. 11255,
pp. 82–96.
ista: 'Koshti G, Biswas R, Largeteau-Skapin G, Zrour R, Andres E, Bhowmick P. 2018.
Sphere construction on the FCC grid interpreted as layered hexagonal grids in
3D. 19th International Workshop. IWCIA: International Workshop on Combinatorial
Image Analysis, LNCS, vol. 11255, 82–96.'
mla: Koshti, Girish, et al. “Sphere Construction on the FCC Grid Interpreted as
Layered Hexagonal Grids in 3D.” 19th International Workshop, vol. 11255,
Springer, 2018, pp. 82–96, doi:10.1007/978-3-030-05288-1_7.
short: G. Koshti, R. Biswas, G. Largeteau-Skapin, R. Zrour, E. Andres, P. Bhowmick,
in:, 19th International Workshop, Springer, Cham, 2018, pp. 82–96.
conference:
end_date: 2018-11-24
location: Porto, Portugal
name: 'IWCIA: International Workshop on Combinatorial Image Analysis'
start_date: 2018-11-22
date_created: 2019-03-21T12:16:58Z
date_published: 2018-11-22T00:00:00Z
date_updated: 2022-01-27T15:26:39Z
day: '22'
doi: 10.1007/978-3-030-05288-1_7
extern: '1'
intvolume: ' 11255'
language:
- iso: eng
month: '11'
oa_version: None
page: 82-96
place: Cham
publication: 19th International Workshop
publication_identifier:
eisbn:
- 978-3-030-05288-1
eissn:
- 1611-3349
isbn:
- 978-3-030-05287-4
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
status: public
title: Sphere construction on the FCC grid interpreted as layered hexagonal grids
in 3D
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 11255
year: '2018'
...
---
_id: '13160'
abstract:
- lang: eng
text: "Transforming deterministic ω\r\n-automata into deterministic parity automata
is traditionally done using variants of appearance records. We present a more
efficient variant of this approach, tailored to Rabin automata, and several optimizations
applicable to all appearance records. We compare the methods experimentally and
find out that our method produces smaller automata than previous approaches. Moreover,
the experiments demonstrate the potential of our method for LTL synthesis, using
LTL-to-Rabin translators. It leads to significantly smaller parity automata when
compared to state-of-the-art approaches on complex formulae."
acknowledgement: This work is partially funded by the DFG project “Verified Model
Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Clara
full_name: Waldmann, Clara
last_name: Waldmann
- first_name: Maximilian
full_name: Weininger, Maximilian
last_name: Weininger
citation:
ama: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
for transforming Rabin automata into parity automata. In: Tools and Algorithms
for the Construction and Analysis of Systems. Vol 10205. Springer; 2017:443-460.
doi:10.1007/978-3-662-54577-5_26'
apa: 'Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2017).
Index appearance record for transforming Rabin automata into parity automata.
In Tools and Algorithms for the Construction and Analysis of Systems (Vol.
10205, pp. 443–460). Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54577-5_26'
chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
“Index Appearance Record for Transforming Rabin Automata into Parity Automata.”
In Tools and Algorithms for the Construction and Analysis of Systems, 10205:443–60.
Springer, 2017. https://doi.org/10.1007/978-3-662-54577-5_26.
ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
record for transforming Rabin automata into parity automata,” in Tools and
Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden,
2017, vol. 10205, pp. 443–460.
ista: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance
record for transforming Rabin automata into parity automata. Tools and Algorithms
for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.'
mla: Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata
into Parity Automata.” Tools and Algorithms for the Construction and Analysis
of Systems, vol. 10205, Springer, 2017, pp. 443–60, doi:10.1007/978-3-662-54577-5_26.
short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and
Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2017-04-22
date_created: 2023-06-21T13:21:14Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2023-06-21T13:29:46Z
day: '31'
department:
- _id: KrCh
doi: 10.1007/978-3-662-54577-5_26
external_id:
arxiv:
- '1701.05738'
intvolume: ' 10205'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.1701.05738
month: '03'
oa: 1
oa_version: Preprint
page: 443-460
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783662545775'
eissn:
- 1611-3349
isbn:
- '9783662545768'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
status: public
title: Index appearance record for transforming Rabin automata into parity automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10205
year: '2017'
...