---
_id: '18066'
abstract:
- lang: eng
text: 'Graph games lie at the algorithmic core of many automated design problems
in computer science. These are games usually played between two players on a given
graph, where the players keep moving a token along the edges according to pre-determined
rules (turn-based, concurrent, etc.), and the winner is decided based on the infinite
path (aka play) traversed by the token from a given initial position. In bidding
games, the players initially get some monetary budgets which they need to use
to bid for the privilege of moving the token at each step. Each round of bidding
affects the players'' available budgets, which is the only form of update that
the budgets experience. We introduce bidding games with charging where the players
can additionally improve their budgets during the game by collecting vertex-dependent
monetary rewards, aka the "charges." Unlike traditional bidding games (where all
charges are zero), bidding games with charging allow non-trivial recurrent behaviors.
For example, a reachability objective may require multiple detours to vertices
with high charges to earn additional budget. We show that, nonetheless, the central
property of traditional bidding games generalizes to bidding games with charging:
For each vertex there exists a threshold ratio, which is the necessary and sufficient
fraction of the total budget for winning the game from that vertex. While the
thresholds of traditional bidding games correspond to unique fixed points of linear
systems of equations, in games with charging, these fixed points are no longer
unique. This significantly complicates the proof of existence and the algorithmic
computation of thresholds for infinite-duration objectives. We also provide the
lower complexity bounds for computing thresholds for Rabin and Streett objectives,
which are the first known lower bounds in any form of bidding games (with or without
charging), and we solve the following repair problem for safety and reachability
games that have unsatisfiable objectives: Can we distribute a given amount of
charge to the players in a way such that the objective can be satisfied?'
acknowledgement: This work was supported in part by the ERC projects ERC-2020-AdG
101020093 and CoG 863818 (ForM-SMArt) and by ISF grant no. 1679/21.
alternative_title:
- LIPIcs
article_number: '8'
article_processing_charge: Yes
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Ehsan Kafshdar
full_name: Goharshady, Ehsan Kafshdar
last_name: Goharshady
- 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: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Avni G, Goharshady EK, Henzinger TA, Mallik K. Bidding games with charging.
In: 35th International Conference on Concurrency Theory. Vol 311. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:10.4230/LIPIcs.CONCUR.2024.8'
apa: 'Avni, G., Goharshady, E. K., Henzinger, T. A., & Mallik, K. (2024). Bidding
games with charging. In 35th International Conference on Concurrency Theory
(Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.CONCUR.2024.8'
chicago: Avni, Guy, Ehsan Kafshdar Goharshady, Thomas A Henzinger, and Kaushik Mallik.
“Bidding Games with Charging.” In 35th International Conference on Concurrency
Theory, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.
https://doi.org/10.4230/LIPIcs.CONCUR.2024.8.
ieee: G. Avni, E. K. Goharshady, T. A. Henzinger, and K. Mallik, “Bidding games
with charging,” in 35th International Conference on Concurrency Theory,
Calgary, Canada, 2024, vol. 311.
ista: 'Avni G, Goharshady EK, Henzinger TA, Mallik K. 2024. Bidding games with charging.
35th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency
Theory, LIPIcs, vol. 311, 8.'
mla: Avni, Guy, et al. “Bidding Games with Charging.” 35th International Conference
on Concurrency Theory, vol. 311, 8, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2024, doi:10.4230/LIPIcs.CONCUR.2024.8.
short: G. Avni, E.K. Goharshady, T.A. Henzinger, K. Mallik, in:, 35th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2024.
conference:
end_date: 2024-09-13
location: Calgary, Canada
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2024-09-09
corr_author: '1'
das_tickbox: '0'
date_created: 2024-09-15T22:01:39Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2026-10-21T12:17:18Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2024.8
ec_funded: 1
external_id:
arxiv:
- '2407.06288'
isi:
- '001556847400008'
file:
- access_level: open_access
checksum: cb6f2254b84922cd7bf224f550b73f4a
content_type: application/pdf
creator: dernst
date_created: 2024-09-17T09:35:03Z
date_updated: 2024-09-17T09:35:03Z
file_id: '18083'
file_name: 2024_LIPICS_Avni.pdf
file_size: 854430
relation: main_file
success: 1
file_date_updated: 2024-09-17T09:35:03Z
fulldoi: https://doi.org/10.4230/LIPIcs.CONCUR.2024.8
has_accepted_license: '1'
intvolume: ' 311'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 35th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959773393'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Bidding games with charging
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 311
year: '2024'
...
---
_id: '18067'
abstract:
- lang: eng
text: "An automaton \U0001D49C is history-deterministic if its nondeterminism can
be resolved on the fly, only using the prefix of the word read so far. This mild
form of nondeterminism has attracted particular attention for its applications
in synthesis problems. An automaton \U0001D49C is guidable with respect to a class
C of automata if it can fairly simulate every automaton in C, whose language is
contained in that of \U0001D49C. In other words, guidable automata are those for
which inclusion and simulation coincide, making them particularly interesting
for model-checking. We study the connection between these two notions, and specifically
the question of when they coincide. For classes of automata on which they do,
deciding guidability, an otherwise challenging decision problem, reduces to deciding
history-determinism, a problem that is starting to be well-understood for many
classes. We provide a selection of sufficient criteria for a class of automata
to guarantee the coincidence of the notions, and use them to show that the notions
coincide for the most common automata classes, among which are ω-regular automata
and many infinite-state automata with safety and reachability acceptance conditions,
including vector addition systems with states, one-counter nets, pushdown-, Parikh-,
and timed-automata. We also demonstrate that history-determinism and guidability
do not always coincide, for example, for the classes of timed automata with a
fixed number of clocks."
acknowledgement: "Udi Boker: Israel Science Foundation grant 2410/22\r\nThomas A.
Henzinger: ERC-2020-AdG 101020093 (VAMOS)\r\nKaroliina Lehtinen: ANR QUASY 23-CE48-0008-01\r\nAditya
Prakash: Chancellors’ International Scholarship from the University of Warwick and
Centre for Discrete Mathematics and Its Applications (DIMAP)"
alternative_title:
- LIPIcs
article_number: '12'
article_processing_charge: No
arxiv: 1
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- 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: Karoliina
full_name: Lehtinen, Karoliina
last_name: Lehtinen
- first_name: Aditya
full_name: Prakash, Aditya
last_name: Prakash
citation:
ama: 'Boker U, Henzinger TA, Lehtinen K, Prakash A. History-determinism vs fair
simulation. In: 35th International Conference on Concurrency Theory. Vol
311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:10.4230/LIPIcs.CONCUR.2024.12'
apa: 'Boker, U., Henzinger, T. A., Lehtinen, K., & Prakash, A. (2024). History-determinism
vs fair simulation. In 35th International Conference on Concurrency Theory
(Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.CONCUR.2024.12'
chicago: Boker, Udi, Thomas A Henzinger, Karoliina Lehtinen, and Aditya Prakash.
“History-Determinism vs Fair Simulation.” In 35th International Conference
on Concurrency Theory, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2024. https://doi.org/10.4230/LIPIcs.CONCUR.2024.12.
ieee: U. Boker, T. A. Henzinger, K. Lehtinen, and A. Prakash, “History-determinism
vs fair simulation,” in 35th International Conference on Concurrency Theory,
Calgary, Canada, 2024, vol. 311.
ista: 'Boker U, Henzinger TA, Lehtinen K, Prakash A. 2024. History-determinism vs
fair simulation. 35th International Conference on Concurrency Theory. CONCUR:
Conference on Concurrency Theory, LIPIcs, vol. 311, 12.'
mla: Boker, Udi, et al. “History-Determinism vs Fair Simulation.” 35th International
Conference on Concurrency Theory, vol. 311, 12, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2024, doi:10.4230/LIPIcs.CONCUR.2024.12.
short: U. Boker, T.A. Henzinger, K. Lehtinen, A. Prakash, in:, 35th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2024.
conference:
end_date: 2024-09-13
location: Calgary, Canada
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2024-09-09
corr_author: '1'
das_tickbox: '0'
date_created: 2024-09-15T22:01:40Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2026-10-21T12:17:34Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2024.12
ec_funded: 1
external_id:
arxiv:
- '2407.08620'
isi:
- '001556847400012'
file:
- access_level: open_access
checksum: 66db11ef8e600a434079c278050c3f09
content_type: application/pdf
creator: dernst
date_created: 2024-09-17T07:31:18Z
date_updated: 2024-09-17T07:31:18Z
file_id: '18080'
file_name: 2024_LIPICS_Boker.pdf
file_size: 766902
relation: main_file
success: 1
file_date_updated: 2024-09-17T07:31:18Z
fulldoi: https://doi.org/10.4230/LIPIcs.CONCUR.2024.12
has_accepted_license: '1'
intvolume: ' 311'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 35th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959773393'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: History-determinism vs fair simulation
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 311
year: '2024'
...
---
_id: '15376'
abstract:
- lang: eng
text: Sequential decision-making tasks often require satisfaction of multiple, partially-contradictory
objectives. Existing approaches are monolithic, where a single policy fulfills
all objectives. We present auction-based scheduling, a decentralized framework
for multi-objective sequential decision making. Each objective is fulfilled using
a separate and independent policy. Composition of policies is performed at runtime,
where at each step, the policies simultaneously bid from pre-allocated budgets
for the privilege of choosing the next action. The framework allows policies to
be independently created, modified, and replaced. We study path planning problems
on finite graphs with two temporal objectives and present algorithms to synthesize
policies together with bidding policies in a decentralized manner. We consider
three categories of decentralized synthesis problems, parameterized by the assumptions
that the policies make on each other. We identify a class of assumptions called
assume-admissible for which synthesis is always possible for graphs whose every
vertex has at most two outgoing edges.
acknowledgement: This work was supported in part by the ERC project ERC-2020-AdG 101020093
and by ISF grant no. 1679/21.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Suman
full_name: Sadhukhan, Suman
last_name: Sadhukhan
citation:
ama: 'Avni G, Mallik K, Sadhukhan S. Auction-based scheduling. In: 30th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Vol 14572. Springer Nature; 2024:153-172. doi:10.1007/978-3-031-57256-2_8'
apa: 'Avni, G., Mallik, K., & Sadhukhan, S. (2024). Auction-based scheduling.
In 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 14572, pp. 153–172). Luxembourg City, Luxembourg:
Springer Nature. https://doi.org/10.1007/978-3-031-57256-2_8'
chicago: Avni, Guy, Kaushik Mallik, and Suman Sadhukhan. “Auction-Based Scheduling.”
In 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, 14572:153–72. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-57256-2_8.
ieee: G. Avni, K. Mallik, and S. Sadhukhan, “Auction-based scheduling,” in 30th
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 153–172.
ista: 'Avni G, Mallik K, Sadhukhan S. 2024. Auction-based scheduling. 30th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 14572, 153–172.'
mla: Avni, Guy, et al. “Auction-Based Scheduling.” 30th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, vol.
14572, Springer Nature, 2024, pp. 153–72, doi:10.1007/978-3-031-57256-2_8.
short: G. Avni, K. Mallik, S. Sadhukhan, in:, 30th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, Springer Nature,
2024, pp. 153–172.
conference:
end_date: 2024-04-11
location: Luxembourg City, Luxembourg
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2024-04-06
corr_author: '1'
das_tickbox: '0'
date_created: 2024-05-12T22:01:02Z
date_published: 2024-04-05T00:00:00Z
date_updated: 2026-10-21T12:16:28Z
day: '05'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-57256-2_8
ec_funded: 1
external_id:
arxiv:
- '2310.11798'
isi:
- '001284187100008'
file:
- access_level: open_access
checksum: dbeb123510997886d11925aedbf9c400
content_type: application/pdf
creator: dernst
date_created: 2024-05-22T07:09:24Z
date_updated: 2024-05-22T07:09:24Z
file_id: '15414'
file_name: 2024_LNCS_Avni.pdf
file_size: 508191
relation: main_file
success: 1
file_date_updated: 2024-05-22T07:09:24Z
fulldoi: https://doi.org/10.1007/978-3-031-57256-2_8
has_accepted_license: '1'
intvolume: ' 14572'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 153-172
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031572555'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Auction-based scheduling
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14572
year: '2024'
...
---
_id: '17413'
abstract:
- lang: eng
text: Certification helps to increase trust in formal verification of safety-critical
systems which require assurance on their correctness. In hardware model checking,
a widely used formal verification technique, phase abstraction is considered one
of the most commonly used preprocessing techniques. We present an approach to
certify an extended form of phase abstraction using a generic certificate format.
As in earlier works our approach involves constructing a witness circuit with
an inductive invariant property that certifies the correctness of the entire model
checking process, which is then validated by an independent certificate checker.
We have implemented and evaluated the proposed approach including certification
for various preprocessing configurations on hardware model checking competition
benchmarks. As an improvement on previous work in this area, the proposed method
is able to efficiently complete certification with an overhead of a fraction of
model checking time.
acknowledgement: This work is supported by the Austrian Science Fund (FWF) under the
project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG
101020093, the Academy of Finland under the project 336092 and by a gift from Intel
Corporation.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Nils
full_name: Froleyks, Nils
last_name: Froleyks
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
- first_name: Armin
full_name: Biere, Armin
last_name: Biere
- first_name: Keijo
full_name: Heljanko, Keijo
last_name: Heljanko
citation:
ama: 'Froleyks N, Yu E, Biere A, Heljanko K. Certifying phase abstraction. In: Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics). Vol 14739. Springer Nature; 2024:284-303.
doi:10.1007/978-3-031-63498-7_17'
apa: 'Froleyks, N., Yu, E., Biere, A., & Heljanko, K. (2024). Certifying phase
abstraction. In Lecture Notes in Computer Science (including subseries Lecture
Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol.
14739, pp. 284–303). Nancy, France: Springer Nature. https://doi.org/10.1007/978-3-031-63498-7_17'
chicago: Froleyks, Nils, Emily Yu, Armin Biere, and Keijo Heljanko. “Certifying
Phase Abstraction.” In Lecture Notes in Computer Science (Including Subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
14739:284–303. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-63498-7_17.
ieee: N. Froleyks, E. Yu, A. Biere, and K. Heljanko, “Certifying phase abstraction,”
in Lecture Notes in Computer Science (including subseries Lecture Notes in
Artificial Intelligence and Lecture Notes in Bioinformatics), Nancy, France,
2024, vol. 14739, pp. 284–303.
ista: 'Froleyks N, Yu E, Biere A, Heljanko K. 2024. Certifying phase abstraction.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics). IJCAR: International Joint
Conference on Automated Reasoning, LNCS, vol. 14739, 284–303.'
mla: Froleyks, Nils, et al. “Certifying Phase Abstraction.” Lecture Notes in
Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), vol. 14739, Springer Nature, 2024, pp.
284–303, doi:10.1007/978-3-031-63498-7_17.
short: N. Froleyks, E. Yu, A. Biere, K. Heljanko, in:, Lecture Notes in Computer
Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics), Springer Nature, 2024, pp. 284–303.
conference:
end_date: 2024-07-06
location: Nancy, France
name: 'IJCAR: International Joint Conference on Automated Reasoning'
start_date: 2024-07-03
das_tickbox: '0'
date_created: 2024-08-11T22:01:13Z
date_published: 2024-07-01T00:00:00Z
date_updated: 2026-10-21T12:03:11Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-63498-7_17
ec_funded: 1
external_id:
arxiv:
- '2405.04297'
isi:
- '001273489700017'
file:
- access_level: open_access
checksum: 7d7839fc8c5c680ea3ac09f40a66e55d
content_type: application/pdf
creator: dernst
date_created: 2024-08-12T06:53:39Z
date_updated: 2024-08-12T06:53:39Z
file_id: '17414'
file_name: 2024_LNCS_Froleyks.pdf
file_size: 556902
relation: main_file
success: 1
file_date_updated: 2024-08-12T06:53:39Z
fulldoi: https://doi.org/10.1007/978-3-031-63498-7_17
has_accepted_license: '1'
intvolume: ' 14739'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 284-303
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031634970'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Certifying phase abstraction
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14739
year: '2024'
...
---
_id: '15333'
abstract:
- lang: eng
text: BUBAAK-SpLit is a tool for dynamically splitting verification tasks into parts
that can then be analyzed in parallel. It is built on top of BUBAAK, a tool designed
for running combinations of verifiers in parallel. In contrast to BUBAAK, that
directly invokes verifiers on the inputs, BUBAAK-SpLit first starts by splitting
the input program into multiple modified versions called program splits. During
the splitting process, BUBAAK-SpLit utilizes a weak verifier (in our case symbolic
execution with a short timelimit) to analyze each generated program split. If
the weak verifier fails on a program split, we split this program split again
and start the verification process again on the generated program splits. We run
the splitting process until a predefined number of hard-to-verify program splits
is generated or a splitting limit is reached. During the main verification phase,
we run a combination of BUBAAK-LEE and SLOWBEAST in parallel on the remaining
unsolved parts of the verification task.
acknowledgement: This work was partially supported by the ERC-2020-AdG 10102009 grant.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Cedric
full_name: Richter, Cedric
last_name: Richter
citation:
ama: 'Chalupa M, Richter C. Bubaak-SpLit: Split what you cannot verify (Competition
contribution). In: 30th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems. Vol 14572. Springer Nature; 2024:353–358.
doi:10.1007/978-3-031-57256-2_20'
apa: 'Chalupa, M., & Richter, C. (2024). Bubaak-SpLit: Split what you cannot
verify (Competition contribution). In 30th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (Vol. 14572, pp.
353–358). Luxembourg City, Luxembourg: Springer Nature. https://doi.org/10.1007/978-3-031-57256-2_20'
chicago: 'Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot
Verify (Competition Contribution).” In 30th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, 14572:353–358.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-57256-2_20.'
ieee: 'M. Chalupa and C. Richter, “Bubaak-SpLit: Split what you cannot verify (Competition
contribution),” in 30th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems, Luxembourg City, Luxembourg, 2024,
vol. 14572, pp. 353–358.'
ista: 'Chalupa M, Richter C. 2024. Bubaak-SpLit: Split what you cannot verify (Competition
contribution). 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
Analysis of Systems, LNCS, vol. 14572, 353–358.'
mla: 'Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify
(Competition Contribution).” 30th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, vol. 14572, Springer Nature,
2024, pp. 353–358, doi:10.1007/978-3-031-57256-2_20.'
short: M. Chalupa, C. Richter, in:, 30th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 353–358.
conference:
end_date: 2024-04-11
location: Luxembourg City, Luxembourg
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2024-04-06
corr_author: '1'
das_tickbox: '1'
dataavailabilitystatement: The submitted version of our tool contribution is archived
and available at Zenodo [2] https://zenodo.org/records/10202207. The source code
is also available on GitLab [3] https://gitlab.com/mchalupa/bubaak
date_created: 2024-04-20T18:14:06Z
date_published: 2024-04-05T00:00:00Z
date_updated: 2026-10-21T12:12:16Z
day: '05'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-57256-2_20
ec_funded: 1
external_id:
isi:
- '001284187100020'
file:
- access_level: open_access
checksum: 208c855c60824bec936b8d01d0396474
content_type: application/pdf
creator: cchlebak
date_created: 2024-04-26T11:27:26Z
date_updated: 2024-04-26T11:27:26Z
file_id: '15347'
file_name: 2024_LNCS_Chalupa.pdf
file_size: 577128
relation: main_file
success: 1
file_date_updated: 2024-04-26T11:27:26Z
fulldoi: https://doi.org/10.1007/978-3-031-57256-2_20
has_accepted_license: '1'
intvolume: ' 14572'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 353–358
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eisbn:
- '9783031572562'
eissn:
- 1611-3349
isbn:
- '9783031572555'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '23183'
relation: research_data
status: public
researchdata_availability: yes
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Bubaak-SpLit: Split what you cannot verify (Competition contribution)'
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14572
year: '2024'
...
---
_id: '15377'
abstract:
- lang: eng
text: "We provide an algorithmto solve Rabin and Streett games over graphs\r\nwith
n vertices,m edges, and k colours that runs in ˜O³mn(k!)1+o(1)´time and\r\nO(nk
logk logn) space, where ˜O hides poly-logarithmic factors. Our algorithm\r\nis
an improvement by a super quadratic dependence on k! from the currently\r\nbest
known run time of O³mn2(k!)2+o(1)´, obtained by converting a Rabin\r\ngameinto
a parity game,while simultaneously improving its exponential space\r\nrequirement.\r\nOur
main technical ingredient is a characterisation of progress measures for\r\nRabin
games using colourful trees and a combinatorial construction of succinctlyrepresented,\r\nuniversal
colourful trees. Colourful universal trees are generalisations\r\nof universal
trees used by Jurdzi´nski and Lazi´c (2017) to solve parity\r\ngames, as well
as of Rabin progress measures of Klarlund and Kozen (1991).\r\nOur algorithm for
Rabin games is a progress measure lifting algorithm where\r\nthe lifting is performed
on succinct, colourful, universal trees."
acknowledgement: This work is a part of the project VAMOS that has received funding
from the European Research Council (ERC) under the European Union’s Horizon 2020
research and innovation programme, grant agreements No 101020093. Rupak Majumdar
was partially supported by the DFG project 389792660 TRR 248-CPEC.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Irmak
full_name: Sağlam, Irmak
last_name: Sağlam
- first_name: K. S.
full_name: Thejaswini, K. S.
id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753
last_name: Thejaswini
citation:
ama: 'Majumdar R, Sağlam I, Thejaswini KS. Rabin games and colourful universal trees.
In: 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems. Vol 14572. Springer Nature; 2024:213-231. doi:10.1007/978-3-031-57256-2_11'
apa: Majumdar, R., Sağlam, I., & Thejaswini, K. S. (2024). Rabin games and colourful
universal trees. In 30th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (Vol. 14572, pp. 213–231). Springer
Nature. https://doi.org/10.1007/978-3-031-57256-2_11
chicago: Majumdar, Rupak, Irmak Sağlam, and K. S. Thejaswini. “Rabin Games and Colourful
Universal Trees.” In 30th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, 14572:213–31. Springer Nature,
2024. https://doi.org/10.1007/978-3-031-57256-2_11.
ieee: R. Majumdar, I. Sağlam, and K. S. Thejaswini, “Rabin games and colourful universal
trees,” in 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, 2024, vol. 14572, pp. 213–231.
ista: Majumdar R, Sağlam I, Thejaswini KS. 2024. Rabin games and colourful universal
trees. 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems. , LNCS, vol. 14572, 213–231.
mla: Majumdar, Rupak, et al. “Rabin Games and Colourful Universal Trees.” 30th
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, vol. 14572, Springer Nature, 2024, pp. 213–31, doi:10.1007/978-3-031-57256-2_11.
short: R. Majumdar, I. Sağlam, K.S. Thejaswini, in:, 30th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, Springer
Nature, 2024, pp. 213–231.
corr_author: '1'
das_tickbox: '0'
date_created: 2024-05-12T22:01:02Z
date_published: 2024-04-06T00:00:00Z
date_updated: 2026-10-21T12:16:56Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-57256-2_11
ec_funded: 1
external_id:
arxiv:
- '2401.07548'
isi:
- '001284187100011'
file:
- access_level: open_access
checksum: 492be74f69cd6ea42d38681082d0b521
content_type: application/pdf
creator: dernst
date_created: 2024-05-22T07:24:45Z
date_updated: 2024-05-22T07:24:45Z
file_id: '15415'
file_name: 2024_LNCS_Majumdar.pdf
file_size: 462173
relation: main_file
success: 1
file_date_updated: 2024-05-22T07:24:45Z
fulldoi: https://doi.org/10.1007/978-3-031-57256-2_11
has_accepted_license: '1'
intvolume: ' 14572'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 213-231
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031572555'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Rabin games and colourful universal trees
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14572
year: '2024'
...
---
_id: '17898'
abstract:
- lang: eng
text: 'There is an ever-growing zoo of modern neural network models that can efficiently
learn end-to-end control from visual observations. These advanced deep models,
ranging from convolutional to Vision Transformers, from small to gigantic networks,
have been extensively tested on offline image classification tasks. In this paper,
we study these vision models with respect to the open-loop training to closed-loop
generalization abilities, i.e., deployment realizes a causal feedback loop that
is not present during training. This causality gap typically emerges in robotics
applications such as autonomous driving, where a network is trained to imitate
the control commands of a human. In this setting, two situations arise: 1) Closed-loop
testing in-distribution, where the test environment shares properties with those
of offline training data. 2) Closed-loop testing under distribution shifts and
out-of-distribution. Contrary to recently reported results, we show that under
proper training guidelines, all vision architectures perform indistinguishably
well on in-distribution deployment, resolving the causality gap. In situation
2, We observe that scale is the strongest factor in improving closed-loop generalization
regardless of the choice of the model architecture. Our results predict the trend
that in the future we will see larger and larger models being used in offline-training-online-deployment
imitation learning tasks in robotic applications.'
acknowledgement: This work was partially supported in parts by the ERC-2020-AdG 101020093.
Additionally, it was partially sponsored by the United States Air Force Research
Laboratory and the United States Air Force Artificial Intelligence Accelerator and
was accomplished under Cooperative Agreement Number FA8750-19-2-1000. The views
and conclusions contained in this document are those of the authors and should not
be interpreted as representing the official policies, either expressed or implied,
of the United States Air Force or the U.S. Government. The U.S. Government is authorized
to reproduce and distribute reprints for Government purposes notwithstanding any
copyright notation herein. This work was further supported by The Boeing Company
and the Office of Naval Research (ONR) Grant N00014-18-1-2830.
article_processing_charge: No
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- first_name: Tsun Hsuan
full_name: Wang, Tsun Hsuan
last_name: Wang
- 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: Daniela
full_name: Rus, Daniela
last_name: Rus
citation:
ama: 'Lechner M, Hasani R, Amini A, Wang TH, Henzinger TA, Rus D. Overparametrization
helps offline-to-online generalization of closed-loop control from pixels. In:
Proceedings of the 2024 IEEE International Conference on Robotics and Automation.
IEEE; 2024:2774-2782. doi:10.1109/ICRA57147.2024.10610284'
apa: 'Lechner, M., Hasani, R., Amini, A., Wang, T. H., Henzinger, T. A., & Rus,
D. (2024). Overparametrization helps offline-to-online generalization of closed-loop
control from pixels. In Proceedings of the 2024 IEEE International Conference
on Robotics and Automation (pp. 2774–2782). Yokohama, Japan: IEEE. https://doi.org/10.1109/ICRA57147.2024.10610284'
chicago: Lechner, Mathias, Ramin Hasani, Alexander Amini, Tsun Hsuan Wang, Thomas
A Henzinger, and Daniela Rus. “Overparametrization Helps Offline-to-Online Generalization
of Closed-Loop Control from Pixels.” In Proceedings of the 2024 IEEE International
Conference on Robotics and Automation, 2774–82. IEEE, 2024. https://doi.org/10.1109/ICRA57147.2024.10610284.
ieee: M. Lechner, R. Hasani, A. Amini, T. H. Wang, T. A. Henzinger, and D. Rus,
“Overparametrization helps offline-to-online generalization of closed-loop control
from pixels,” in Proceedings of the 2024 IEEE International Conference on Robotics
and Automation, Yokohama, Japan, 2024, pp. 2774–2782.
ista: 'Lechner M, Hasani R, Amini A, Wang TH, Henzinger TA, Rus D. 2024. Overparametrization
helps offline-to-online generalization of closed-loop control from pixels. Proceedings
of the 2024 IEEE International Conference on Robotics and Automation. ICRA: International
Conference on Robotics and Automation, 2774–2782.'
mla: Lechner, Mathias, et al. “Overparametrization Helps Offline-to-Online Generalization
of Closed-Loop Control from Pixels.” Proceedings of the 2024 IEEE International
Conference on Robotics and Automation, IEEE, 2024, pp. 2774–82, doi:10.1109/ICRA57147.2024.10610284.
short: M. Lechner, R. Hasani, A. Amini, T.H. Wang, T.A. Henzinger, D. Rus, in:,
Proceedings of the 2024 IEEE International Conference on Robotics and Automation,
IEEE, 2024, pp. 2774–2782.
conference:
end_date: 2024-05-17
location: Yokohama, Japan
name: 'ICRA: International Conference on Robotics and Automation'
start_date: 2024-05-13
das_tickbox: '0'
date_created: 2024-09-08T22:01:13Z
date_published: 2024-08-08T00:00:00Z
date_updated: 2026-10-21T12:03:35Z
day: '08'
department:
- _id: ToHe
doi: 10.1109/ICRA57147.2024.10610284
ec_funded: 1
external_id:
isi:
- '001294576202044'
fulldoi: https://doi.org/10.1109/ICRA57147.2024.10610284
isi: 1
language:
- iso: eng
month: '08'
oa_version: None
page: 2774-2782
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the 2024 IEEE International Conference on Robotics and
Automation
publication_identifier:
isbn:
- '9798350384574'
issn:
- 1050-4729
publication_status: published
publisher: IEEE
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Overparametrization helps offline-to-online generalization of closed-loop control
from pixels
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2024'
...
---
_id: '15321'
abstract:
- lang: eng
text: Boolean Networks (BNs) are widely used as a modeling formalism in several
domains, notably systems biology and computer science. A fundamental problem in
BN analysis is the enumeration of trap spaces, which are hypercubes in the state
space that cannot be escaped once entered. Several methods have been proposed
for enumerating trap spaces, however they often suffer from scalability and efficiency
issues, particularly for large and complex models. To our knowledge, the most
efficient and recent methods for the trap space enumeration all rely on Answer
Set Programming (ASP), which has been widely applied to the analysis of BNs. Motivated
by these considerations, our work proposes a new method for enumerating trap spaces
in BNs using ASP. We evaluate the method on a mix of 250+ real-world and 400+
randomly generated BNs, showing that it enables analysis of models beyond the
capabilities of existing tools (namely pyboolnet, mpbn, trappist, and trapmvn).
acknowledgement: This work was supported by Institut Carnot STAR, Marseille, France
and by the European Union’s Horizon 2020 research and innovation programme under
the Marie Skłodowska-Curie Grant Agreement No. 101034413.
article_processing_charge: No
author:
- first_name: Giang
full_name: Trinh, Giang
last_name: Trinh
- first_name: Belaid
full_name: Benhamou, Belaid
last_name: Benhamou
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: Sylvain
full_name: Soliman, Sylvain
last_name: Soliman
citation:
ama: 'Trinh G, Benhamou B, Pastva S, Soliman S. Scalable enumeration of trap spaces
in boolean networks via answer set programming. In: Proceedings of the 38th
AAAI Conference on Artificial Intelligence. Vol 38. Association for the Advancement
of Artificial Intelligence; 2024:10714-10722. doi:10.1609/aaai.v38i9.28943'
apa: Trinh, G., Benhamou, B., Pastva, S., & Soliman, S. (2024). Scalable enumeration
of trap spaces in boolean networks via answer set programming. In Proceedings
of the 38th AAAI Conference on Artificial Intelligence (Vol. 38, pp. 10714–10722).
Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v38i9.28943
chicago: Trinh, Giang, Belaid Benhamou, Samuel Pastva, and Sylvain Soliman. “Scalable
Enumeration of Trap Spaces in Boolean Networks via Answer Set Programming.” In
Proceedings of the 38th AAAI Conference on Artificial Intelligence, 38:10714–22.
Association for the Advancement of Artificial Intelligence, 2024. https://doi.org/10.1609/aaai.v38i9.28943.
ieee: G. Trinh, B. Benhamou, S. Pastva, and S. Soliman, “Scalable enumeration of
trap spaces in boolean networks via answer set programming,” in Proceedings
of the 38th AAAI Conference on Artificial Intelligence, 2024, vol. 38, no.
9, pp. 10714–10722.
ista: Trinh G, Benhamou B, Pastva S, Soliman S. 2024. Scalable enumeration of trap
spaces in boolean networks via answer set programming. Proceedings of the 38th
AAAI Conference on Artificial Intelligence. vol. 38, 10714–10722.
mla: Trinh, Giang, et al. “Scalable Enumeration of Trap Spaces in Boolean Networks
via Answer Set Programming.” Proceedings of the 38th AAAI Conference on Artificial
Intelligence, vol. 38, no. 9, Association for the Advancement of Artificial
Intelligence, 2024, pp. 10714–22, doi:10.1609/aaai.v38i9.28943.
short: G. Trinh, B. Benhamou, S. Pastva, S. Soliman, in:, Proceedings of the 38th
AAAI Conference on Artificial Intelligence, Association for the Advancement of
Artificial Intelligence, 2024, pp. 10714–10722.
das_tickbox: '0'
date_created: 2024-04-14T22:01:02Z
date_published: 2024-03-25T00:00:00Z
date_updated: 2026-10-21T12:04:20Z
day: '25'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1609/aaai.v38i9.28943
ec_funded: 1
fulldoi: https://doi.org/10.1609/aaai.v38i9.28943
intvolume: ' 38'
issue: '9'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://amu.hal.science/hal-04523118/
month: '03'
oa: 1
oa_version: Published Version
page: 10714-10722
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Proceedings of the 38th AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- '1577358872'
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
researchdata_availability: yes (supplementary data)
scopus_import: '1'
status: public
supplementarymaterial: yes
title: Scalable enumeration of trap spaces in boolean networks via answer set programming
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 38
year: '2024'
...
---
APC_amount: 2748 EUR
OA_place: publisher
OA_type: hybrid
_id: '18521'
abstract:
- lang: eng
text: In distributed systems with processes that do not share a global clock, partial
synchrony is achieved by clock synchronization that guarantees bounded clock skew
among all applications. Existing solutions for distributed runtime verification
under partial synchrony against temporal logic specifications are exact but suffer
from significant computational overhead. In this paper, we propose an approximate
distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates
this issue by abstracting away potential interleaving behaviors. This conservative
abstraction enables a significant speedup of the distributed monitors, albeit
with a tradeoff in accuracy. We address this tradeoff with a methodology that
combines our approximate monitor with its exact counterpart, resulting in enhanced
efficiency without sacrificing precision. We evaluate our approach with multiple
experiments, showcasing its efficacy in both real-world applications and synthetic
examples.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. This
work is sponsored in part by the United States NSF CCF-2118356 award. This research
was partially funded by A-IQ Ready (Chips JU, grant agreement No. 101096658).
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Borzoo
full_name: Bonakdarpour, Borzoo
last_name: Bonakdarpour
- first_name: Anik
full_name: Momtaz, Anik
last_name: Momtaz
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. Approximate distributed monitoring
under partial synchrony: Balancing speed & accuracy. In: 24th International
Conference on Runtime Verification. Vol 15191. Springer Nature; 2024:282-301.
doi:10.1007/978-3-031-74234-7_18'
apa: 'Bonakdarpour, B., Momtaz, A., Nickovic, D., & Sarac, N. E. (2024). Approximate
distributed monitoring under partial synchrony: Balancing speed & accuracy.
In 24th International Conference on Runtime Verification (Vol. 15191, pp.
282–301). Istanbul, Turkey: Springer Nature. https://doi.org/10.1007/978-3-031-74234-7_18'
chicago: 'Bonakdarpour, Borzoo, Anik Momtaz, Dejan Nickovic, and Naci E Sarac. “Approximate
Distributed Monitoring under Partial Synchrony: Balancing Speed & Accuracy.”
In 24th International Conference on Runtime Verification, 15191:282–301.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-74234-7_18.'
ieee: 'B. Bonakdarpour, A. Momtaz, D. Nickovic, and N. E. Sarac, “Approximate distributed
monitoring under partial synchrony: Balancing speed & accuracy,” in 24th
International Conference on Runtime Verification, Istanbul, Turkey, 2024,
vol. 15191, pp. 282–301.'
ista: 'Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. 2024. Approximate distributed
monitoring under partial synchrony: Balancing speed & accuracy. 24th International
Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS,
vol. 15191, 282–301.'
mla: 'Bonakdarpour, Borzoo, et al. “Approximate Distributed Monitoring under Partial
Synchrony: Balancing Speed & Accuracy.” 24th International Conference on
Runtime Verification, vol. 15191, Springer Nature, 2024, pp. 282–301, doi:10.1007/978-3-031-74234-7_18.'
short: B. Bonakdarpour, A. Momtaz, D. Nickovic, N.E. Sarac, in:, 24th International
Conference on Runtime Verification, Springer Nature, 2024, pp. 282–301.
conference:
end_date: 2024-10-17
location: Istanbul, Turkey
name: 'RV: Conference on Runtime Verification'
start_date: 2024-10-15
corr_author: '1'
das_tickbox: '0'
date_created: 2024-11-10T23:01:58Z
date_published: 2024-10-12T00:00:00Z
date_updated: 2026-10-21T13:14:54Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
- _id: GradSch
doi: 10.1007/978-3-031-74234-7_18
ec_funded: 1
external_id:
arxiv:
- '2408.05033'
isi:
- '001420093700018'
file:
- access_level: open_access
checksum: 7b8ca21b8c19ab796fa445b0e54003ca
content_type: application/pdf
creator: dernst
date_created: 2024-11-11T09:42:28Z
date_updated: 2024-11-11T09:42:28Z
file_id: '18539'
file_name: 2024_LNCS_Bonakdarpour.pdf
file_size: 1897101
relation: main_file
success: 1
file_date_updated: 2024-11-11T09:42:28Z
fulldoi: https://doi.org/10.1007/978-3-031-74234-7_18
has_accepted_license: '1'
intvolume: ' 15191'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 282-301
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 24th International Conference on Runtime Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031742330'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Approximate distributed monitoring under partial synchrony: Balancing speed
& accuracy'
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15191
year: '2024'
...
---
OA_place: publisher
OA_type: gold
_id: '18068'
abstract:
- lang: eng
text: "We study the following refinement relation between nondeterministic state-transition
models: model ℬ strategically dominates model \U0001D49C iff every deterministic
refinement of \U0001D49C is language contained in some deterministic refinement
of ℬ. While language containment is trace inclusion, and the (fair) simulation
preorder coincides with tree inclusion, strategic dominance falls strictly between
the two and can be characterized as \"strategy inclusion\" between \U0001D49C
and ℬ: every strategy that resolves the nondeterminism of \U0001D49C is dominated
by a strategy that resolves the nondeterminism of ℬ. Strategic dominance can be
checked in 2-ExpTime by a decidable first-order Presburger logic with quantification
over words and strategies, called resolver logic. We give several other applications
of resolver logic, including checking the co-safety, co-liveness, and history-determinism
of boolean and quantitative automata, and checking the inclusion between hyperproperties
that are specified by nondeterministic boolean and quantitative automata."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. N.
Mazzocchi was affiliated with ISTA when this work was submitted for publication.
alternative_title:
- LIPIcs
article_number: '29'
article_processing_charge: Yes
arxiv: 1
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: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Strategic dominance: A new preorder
for nondeterministic processes. In: 35th International Conference on Concurrency
Theory. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024.
doi:10.4230/LIPIcs.CONCUR.2024.29'
apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2024). Strategic dominance:
A new preorder for nondeterministic processes. In 35th International Conference
on Concurrency Theory (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2024.29'
chicago: 'Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Strategic
Dominance: A New Preorder for Nondeterministic Processes.” In 35th International
Conference on Concurrency Theory, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2024. https://doi.org/10.4230/LIPIcs.CONCUR.2024.29.'
ieee: 'T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Strategic dominance:
A new preorder for nondeterministic processes,” in 35th International Conference
on Concurrency Theory, Calgary, Canada, 2024, vol. 311.'
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2024. Strategic dominance: A new preorder
for nondeterministic processes. 35th International Conference on Concurrency Theory.
CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 29.'
mla: 'Henzinger, Thomas A., et al. “Strategic Dominance: A New Preorder for Nondeterministic
Processes.” 35th International Conference on Concurrency Theory, vol. 311,
29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:10.4230/LIPIcs.CONCUR.2024.29.'
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 35th International Conference
on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.
conference:
end_date: 2024-09-13
location: Calgary, Canada
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2024-09-09
corr_author: '1'
das_tickbox: '0'
date_created: 2024-09-15T22:01:40Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2026-10-21T13:15:11Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: GradSch
doi: 10.4230/LIPIcs.CONCUR.2024.29
ec_funded: 1
external_id:
arxiv:
- '2407.10473'
isi:
- '001556847400029'
file:
- access_level: open_access
checksum: 555bd343e1fb38adeab8fc465ff4fad8
content_type: application/pdf
creator: dernst
date_created: 2024-09-17T07:48:56Z
date_updated: 2024-09-17T07:48:56Z
file_id: '18081'
file_name: 2024_LIPICS_Henzinger.pdf
file_size: 964124
relation: main_file
success: 1
file_date_updated: 2024-09-17T07:48:56Z
fulldoi: https://doi.org/10.4230/LIPIcs.CONCUR.2024.29
has_accepted_license: '1'
intvolume: ' 311'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 35th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959773393'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Strategic dominance: A new preorder for nondeterministic processes'
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 311
year: '2024'
...
---
_id: '18175'
abstract:
- lang: eng
text: Large-scale software repositories are a source of insights for software engineering.
They offer an unmatched window into the software development process at scale.
Their sheer number and size holds the promise of broadly applicable results. At
the same time, that very size presents practical challenges for scaling tools
and algorithms to millions of projects. A reasonable approach is to limit studies
to representative samples of the population of interest. Broadly applicable conclusions
can then be obtained by generalizing to the entire population. The contribution
of this paper is a standardized experimental design methodology for choosing the
inputs of studies working with large-scale repositories. We advocate for a methodology
that clearly lays out what the population of interest is, how to sample it, and
that fosters reproducibility. Along the way, we discourage researchers from using
extrinsic attributes of projects such as stars, that measure some unclear notion
of popularity.
acknowledgement: "This work was supported by the Czech Ministry of Education, Youth
and Sports under\r\nprogram ERC-CZ, grant agreement LL2325, BigCode (reg. no. CZ.02.1.01/0.0/0.0/15_003/0000421).
NSF grants CCF-1910850, CNS-1925644, and CCF-2139612, as well as the GACR EXPRO
grant 23-07580X. We would like to thank Digital Ocean for their involuntary contribution
of computational resources during the early data gathering phase of our research.
We acknoweldge the reviewers of ICSE’22, and thank the reviewers of ECOOP’23 for
their encouragments and for sticking around until 2024."
alternative_title:
- LIPIcs
article_number: '27'
article_processing_charge: No
author:
- first_name: Petr
full_name: Maj, Petr
last_name: Maj
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- first_name: Konrad
full_name: Siek, Konrad
last_name: Siek
- first_name: Luca
full_name: Di Grazia, Luca
last_name: Di Grazia
- first_name: Jan
full_name: Vitek, Jan
last_name: Vitek
citation:
ama: 'Maj P, Muroya Lei S, Siek K, Di Grazia L, Vitek J. The fault in our stars:
Designing reproducible large-scale code analysis experiments. In: 38th European
Conference on Object-Oriented Programming. Vol 313. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2024. doi:10.4230/LIPIcs.ECOOP.2024.27'
apa: 'Maj, P., Muroya Lei, S., Siek, K., Di Grazia, L., & Vitek, J. (2024).
The fault in our stars: Designing reproducible large-scale code analysis experiments.
In 38th European Conference on Object-Oriented Programming (Vol. 313).
Vienna, Austria: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ECOOP.2024.27'
chicago: 'Maj, Petr, Stefanie Muroya Lei, Konrad Siek, Luca Di Grazia, and Jan Vitek.
“The Fault in Our Stars: Designing Reproducible Large-Scale Code Analysis Experiments.”
In 38th European Conference on Object-Oriented Programming, Vol. 313. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2024. https://doi.org/10.4230/LIPIcs.ECOOP.2024.27.'
ieee: 'P. Maj, S. Muroya Lei, K. Siek, L. Di Grazia, and J. Vitek, “The fault in
our stars: Designing reproducible large-scale code analysis experiments,” in 38th
European Conference on Object-Oriented Programming, Vienna, Austria, 2024,
vol. 313.'
ista: 'Maj P, Muroya Lei S, Siek K, Di Grazia L, Vitek J. 2024. The fault in our
stars: Designing reproducible large-scale code analysis experiments. 38th European
Conference on Object-Oriented Programming. ECOOP: European Conference on Object-Oriented
Programming, LIPIcs, vol. 313, 27.'
mla: 'Maj, Petr, et al. “The Fault in Our Stars: Designing Reproducible Large-Scale
Code Analysis Experiments.” 38th European Conference on Object-Oriented Programming,
vol. 313, 27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:10.4230/LIPIcs.ECOOP.2024.27.'
short: P. Maj, S. Muroya Lei, K. Siek, L. Di Grazia, J. Vitek, in:, 38th European
Conference on Object-Oriented Programming, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2024.
conference:
end_date: 2024-09-20
location: Vienna, Austria
name: 'ECOOP: European Conference on Object-Oriented Programming'
start_date: 2024-09-16
das_tickbox: '0'
date_created: 2024-10-06T22:01:12Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2026-10-21T13:11:58Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.ECOOP.2024.27
external_id:
isi:
- '001533999700027'
file:
- access_level: open_access
checksum: 2e75d305a8c817d76a0c7f136ce34f86
content_type: application/pdf
creator: dernst
date_created: 2024-10-07T11:10:55Z
date_updated: 2024-10-07T11:10:55Z
file_id: '18184'
file_name: 2024_LIPICs_Maj.pdf
file_size: 1764222
relation: main_file
success: 1
file_date_updated: 2024-10-07T11:10:55Z
fulldoi: https://doi.org/10.4230/LIPIcs.ECOOP.2024.27
has_accepted_license: '1'
intvolume: ' 313'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
publication: 38th European Conference on Object-Oriented Programming
publication_identifier:
isbn:
- '9783959773416'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'The fault in our stars: Designing reproducible large-scale code analysis experiments'
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 313
year: '2024'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
_id: '18530'
abstract:
- lang: eng
text: "We explore the notion of history-determinism in the context of timed automata
(TA) over infinite timed words. History-deterministic (HD) automata are those
in which nondeterminism can be resolved on the fly, based on the run constructed
thus far. History-determinism is a robust property that admits different game-based
characterisations, and HD specifications allow for game-based verification without
an expensive determinization step. We show that the class of timed ω\r\n-languages
recognized by HD timed automata strictly extends that of deterministic ones, and
is strictly included in those recognised by fully non-deterministic TA. For non-deterministic
timed automata it is known that universality is already undecidable for safety/reachability
TA. For history-deterministic TA with arbitrary parity acceptance, we show that
timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-complete.
For the subclass of TA with safety or reachability acceptance, one can decide
(in EXPTIME) whether such an automaton is history-deterministic. If so, it can
effectively determinized without introducing new automaton states."
acknowledgement: This work has in parts been presented at the 33rd International Conference
on Concurrency Theory (CONCUR’22) [HLT22] and at the 16th International Workshop
on Reachability Problems (RP’22) [BHL+22]. This work was supported by the EU (ERC-2020-AdG
101020093); the EPSRC (EP/V025848/1, EP/X042596/1, EP/X017796/1 and EP/X03688X/1);
and the ANR (QUASY 23-CE48-0008-01).
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Sougata
full_name: Bose, Sougata
last_name: Bose
- 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: Karoliina
full_name: Lehtinen, Karoliina
last_name: Lehtinen
- first_name: Sven
full_name: Schewe, Sven
last_name: Schewe
- first_name: Patrick
full_name: Totzke, Patrick
last_name: Totzke
citation:
ama: Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. History-deterministic
timed automata. Logical Methods in Computer Science. 2024;20(4):1-28. doi:10.46298/lmcs-20(4:1)2024
apa: Bose, S., Henzinger, T. A., Lehtinen, K., Schewe, S., & Totzke, P. (2024).
History-deterministic timed automata. Logical Methods in Computer Science.
EPI Sciences. https://doi.org/10.46298/lmcs-20(4:1)2024
chicago: Bose, Sougata, Thomas A Henzinger, Karoliina Lehtinen, Sven Schewe, and
Patrick Totzke. “History-Deterministic Timed Automata.” Logical Methods in
Computer Science. EPI Sciences, 2024. https://doi.org/10.46298/lmcs-20(4:1)2024.
ieee: S. Bose, T. A. Henzinger, K. Lehtinen, S. Schewe, and P. Totzke, “History-deterministic
timed automata,” Logical Methods in Computer Science, vol. 20, no. 4. EPI
Sciences, pp. 1–28, 2024.
ista: Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. 2024. History-deterministic
timed automata. Logical Methods in Computer Science. 20(4), 1–28.
mla: Bose, Sougata, et al. “History-Deterministic Timed Automata.” Logical Methods
in Computer Science, vol. 20, no. 4, EPI Sciences, 2024, pp. 1–28, doi:10.46298/lmcs-20(4:1)2024.
short: S. Bose, T.A. Henzinger, K. Lehtinen, S. Schewe, P. Totzke, Logical Methods
in Computer Science 20 (2024) 1–28.
corr_author: '1'
das_tickbox: '0'
date_created: 2024-11-10T23:02:01Z
date_published: 2024-10-02T00:00:00Z
date_updated: 2026-10-21T13:12:37Z
day: '02'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.46298/lmcs-20(4:1)2024
ec_funded: 1
external_id:
arxiv:
- '2304.03183'
isi:
- '001332466900002'
file:
- access_level: open_access
checksum: 26826786a960039b9501cfc5cb4f3fe6
content_type: application/pdf
creator: dernst
date_created: 2024-11-11T08:32:02Z
date_updated: 2024-11-11T08:32:02Z
file_id: '18532'
file_name: 2024_LMCS_Bose.pdf
file_size: 563394
relation: main_file
success: 1
file_date_updated: 2024-11-11T08:32:02Z
fulldoi: https://doi.org/10.46298/lmcs-20(4:1)2024
has_accepted_license: '1'
intvolume: ' 20'
isi: 1
issue: '4'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 1-28
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Logical Methods in Computer Science
publication_identifier:
eissn:
- 1860-5974
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
related_material:
record:
- id: '12508'
relation: earlier_version
status: public
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: History-deterministic timed 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: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 20
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '18955'
abstract:
- lang: eng
text: We give a simple proof that assuming the Exponential Time Hypothesis (ETH),
determining the winner of a Rabin game cannot be done in time 2o(k log k) · nO(1),
where k is the number of pairs of vertex subsets involved in the winning condition
and n is the vertex count of the game graph. While this result follows from the
lower bounds provided by Calude et al [SIAM J. Comp. 2022], our reduction is considerably
simpler and arguably provides more insight into the complexity of the problem.
In fact, the analogous lower bounds discussed by Calude et al, for solving Muller
games and multidimensional parity games, follow as simple corollaries of our approach.
Our reduction also highlights the usefulness of a certain pivot problem — Permutation
SAT — which may be of independent interest.
acknowledgement: This work is a part of projects CUTACOMBS (Ma. Pilipczuk), BOBR (Mi.
Pilipczuk), and VAMOS (K. S. Thejaswini) that have received funding from the European
Research Council (ERC) under the European Union's Horizon 2020 research and innovation
programme, grant agreements No 714704, 948057, and 101020093, respectively. Ma.
Pilipczuk is also partially supported by Polish National Science Centre SONATA BIS-12
grant number 2022/46/E/ST6/00143.
article_processing_charge: No
arxiv: 1
author:
- first_name: Antonio
full_name: Casares, Antonio
last_name: Casares
- first_name: Marcin
full_name: Pilipczuk, Marcin
last_name: Pilipczuk
- first_name: Michał
full_name: Pilipczuk, Michał
last_name: Pilipczuk
- first_name: Uéverton S.
full_name: Souza, Uéverton S.
last_name: Souza
- first_name: K. S.
full_name: Thejaswini, K. S.
id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753
last_name: Thejaswini
citation:
ama: 'Casares A, Pilipczuk M, Pilipczuk M, Souza US, Thejaswini KS. Simple and tight
complexity lower bounds for solving Rabin games. In: 2024 Symposium on Simplicity
in Algorithms. Society for Industrial and Applied Mathematics; 2024:160-167.
doi:10.1137/1.9781611977936.16'
apa: 'Casares, A., Pilipczuk, M., Pilipczuk, M., Souza, U. S., & Thejaswini,
K. S. (2024). Simple and tight complexity lower bounds for solving Rabin games.
In 2024 Symposium on Simplicity in Algorithms (pp. 160–167). Alexandria,
VA, United States: Society for Industrial and Applied Mathematics. https://doi.org/10.1137/1.9781611977936.16'
chicago: Casares, Antonio, Marcin Pilipczuk, Michał Pilipczuk, Uéverton S. Souza,
and K. S. Thejaswini. “Simple and Tight Complexity Lower Bounds for Solving Rabin
Games.” In 2024 Symposium on Simplicity in Algorithms, 160–67. Society
for Industrial and Applied Mathematics, 2024. https://doi.org/10.1137/1.9781611977936.16.
ieee: A. Casares, M. Pilipczuk, M. Pilipczuk, U. S. Souza, and K. S. Thejaswini,
“Simple and tight complexity lower bounds for solving Rabin games,” in 2024
Symposium on Simplicity in Algorithms, Alexandria, VA, United States, 2024,
pp. 160–167.
ista: 'Casares A, Pilipczuk M, Pilipczuk M, Souza US, Thejaswini KS. 2024. Simple
and tight complexity lower bounds for solving Rabin games. 2024 Symposium on Simplicity
in Algorithms. SOSA: Symposium on Simplicity in Algorithms, 160–167.'
mla: Casares, Antonio, et al. “Simple and Tight Complexity Lower Bounds for Solving
Rabin Games.” 2024 Symposium on Simplicity in Algorithms, Society for Industrial
and Applied Mathematics, 2024, pp. 160–67, doi:10.1137/1.9781611977936.16.
short: A. Casares, M. Pilipczuk, M. Pilipczuk, U.S. Souza, K.S. Thejaswini, in:,
2024 Symposium on Simplicity in Algorithms, Society for Industrial and Applied
Mathematics, 2024, pp. 160–167.
conference:
end_date: 2024-01-10
location: Alexandria, VA, United States
name: 'SOSA: Symposium on Simplicity in Algorithms'
start_date: 2024-01-08
das_tickbox: '0'
date_created: 2025-01-29T11:55:50Z
date_published: 2024-01-01T00:00:00Z
date_updated: 2026-10-21T13:13:33Z
day: '01'
department:
- _id: ToHe
doi: 10.1137/1.9781611977936.16
ec_funded: 1
external_id:
arxiv:
- '2310.20433'
fulldoi: https://doi.org/10.1137/1.9781611977936.16
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2310.20433
month: '01'
oa: 1
oa_version: Preprint
page: 160-167
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 2024 Symposium on Simplicity in Algorithms
publication_identifier:
isbn:
- '9781611977936'
publication_status: published
publisher: Society for Industrial and Applied Mathematics
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Simple and tight complexity lower bounds for solving Rabin games
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2024'
...
---
OA_type: closed access
_id: '18599'
abstract:
- lang: eng
text: "Hypernode logic can reason about the prefix relation on stutter-reduced finite
traces through the stutter-reduced prefix predicate. We increase the expressiveness
of hypernode logic in two ways. First, we split the stutter-reduced prefix predicate
into an explicit stutter-reduction operator and the classical prefix predicate
on words. This change gives hypernode logic the ability to combine synchronous
and asynchronous reasoning by explicitly stating which parts of traces can stutter.
Second, we allow the use of regular expressions in formulas to reason about the
structure of traces. This change enables hypernode logic to describe a mixture
of trace properties and hyperproperties.\r\n\r\nWe show how to translate extended
hypernode logic formulas into multi-track automata, which are automata that read
multiple input words. Then we describe a fully online monitoring algorithm for
monitoring k-safety hyperproperties specified in the logic. We have implemented
the monitoring algorithm, and evaluated it on monitoring synchronous and asynchronous
versions of observational determinism, and on checking the privacy preservation
by compiler optimizations."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, and
by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- 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: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: 'Chalupa M, Henzinger TA, Oliveira da Costa A. Monitoring extended hypernode
logic. In: Integrated Formal Methods. Vol 15234. Springer Nature; 2024:151-171.
doi:10.1007/978-3-031-76554-4_9'
apa: Chalupa, M., Henzinger, T. A., & Oliveira da Costa, A. (2024). Monitoring
extended hypernode logic. In Integrated Formal Methods (Vol. 15234, pp.
151–171). Springer Nature. https://doi.org/10.1007/978-3-031-76554-4_9
chicago: Chalupa, Marek, Thomas A Henzinger, and Ana Oliveira da Costa. “Monitoring
Extended Hypernode Logic.” In Integrated Formal Methods, 15234:151–71.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-76554-4_9.
ieee: M. Chalupa, T. A. Henzinger, and A. Oliveira da Costa, “Monitoring extended
hypernode logic,” in Integrated Formal Methods, 2024, vol. 15234, pp. 151–171.
ista: Chalupa M, Henzinger TA, Oliveira da Costa A. 2024. Monitoring extended hypernode
logic. Integrated Formal Methods. , LNCS, vol. 15234, 151–171.
mla: Chalupa, Marek, et al. “Monitoring Extended Hypernode Logic.” Integrated
Formal Methods, vol. 15234, Springer Nature, 2024, pp. 151–71, doi:10.1007/978-3-031-76554-4_9.
short: M. Chalupa, T.A. Henzinger, A. Oliveira da Costa, in:, Integrated Formal
Methods, Springer Nature, 2024, pp. 151–171.
corr_author: '1'
das_tickbox: '0'
date_created: 2024-12-01T23:01:52Z
date_published: 2024-11-13T00:00:00Z
date_updated: 2026-10-21T13:13:13Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-031-76554-4_9
ec_funded: 1
external_id:
isi:
- '001416640500009'
fulldoi: https://doi.org/10.1007/978-3-031-76554-4_9
intvolume: ' 15234'
isi: 1
language:
- iso: eng
month: '11'
oa_version: None
page: 151-171
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: Integrated Formal Methods
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031765537'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Monitoring extended hypernode logic
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15234
year: '2024'
...
---
_id: '18177'
abstract:
- lang: eng
text: Partially Specified Boolean Networks (PSBNs) represent a family of Boolean
models resulting from possible interpretations of unknown update logics. Hybrid
extension of CTL (HCTL) has the power to express complex dynamical phenomena,
such as oscillations or stability. We present BNClassifier to classify Boolean
Networks corresponding to a given PSBN according to criteria specified in HCTL.
The implementation of the tool is fully symbolic (based on BDDs). The results
are visualised using the machine-learning-based technology of decision trees.
acknowledgement: The work has been supported by the Czech Science Foundation grant
No. GA22-10845S. This project has received funding from the European Union’s Horizon
2020 research and innovation programme under the Marie Sklodowska-Curie Grant Agreement
No. 101034413.
alternative_title:
- LNBI
article_processing_charge: No
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Luboš
full_name: Brim, Luboš
last_name: Brim
- first_name: Ondřej
full_name: Huvar, Ondřej
last_name: Huvar
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: David
full_name: Šafránek, David
last_name: Šafránek
citation:
ama: 'Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. BNClassifier: Classifying
boolean models by dynamic properties. In: Computational Methods in Systems
Biology. Vol 14971. Springer Nature; 2024:19-26. doi:10.1007/978-3-031-71671-3_2'
apa: 'Beneš, N., Brim, L., Huvar, O., Pastva, S., & Šafránek, D. (2024). BNClassifier:
Classifying boolean models by dynamic properties. In Computational Methods
in Systems Biology (Vol. 14971, pp. 19–26). Springer Nature. https://doi.org/10.1007/978-3-031-71671-3_2'
chicago: 'Beneš, Nikola, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek.
“BNClassifier: Classifying Boolean Models by Dynamic Properties.” In Computational
Methods in Systems Biology, 14971:19–26. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-71671-3_2.'
ieee: 'N. Beneš, L. Brim, O. Huvar, S. Pastva, and D. Šafránek, “BNClassifier: Classifying
boolean models by dynamic properties,” in Computational Methods in Systems
Biology, 2024, vol. 14971, pp. 19–26.'
ista: 'Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. 2024. BNClassifier: Classifying
boolean models by dynamic properties. Computational Methods in Systems Biology.
, LNBI, vol. 14971, 19–26.'
mla: 'Beneš, Nikola, et al. “BNClassifier: Classifying Boolean Models by Dynamic
Properties.” Computational Methods in Systems Biology, vol. 14971, Springer
Nature, 2024, pp. 19–26, doi:10.1007/978-3-031-71671-3_2.'
short: N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, in:, Computational Methods
in Systems Biology, Springer Nature, 2024, pp. 19–26.
das_tickbox: '0'
date_created: 2024-10-06T22:01:12Z
date_published: 2024-09-19T00:00:00Z
date_updated: 2026-10-21T13:12:17Z
day: '19'
department:
- _id: ToHe
doi: 10.1007/978-3-031-71671-3_2
ec_funded: 1
external_id:
isi:
- '001333144400002'
fulldoi: https://doi.org/10.1007/978-3-031-71671-3_2
intvolume: ' 14971'
isi: 1
language:
- iso: eng
month: '09'
oa_version: None
page: 19-26
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Computational Methods in Systems Biology
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031716706'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'BNClassifier: Classifying boolean models by dynamic properties'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14971
year: '2024'
...
---
OA_type: closed access
_id: '18563'
abstract:
- lang: eng
text: I give a personal account about the wave of new research activities that rose
in the 1990s on the specification, verification, and control of real-time systems.
acknowledgement: I thank all my collaborators over the years. None of the mentioned
contributions would have been possible without them. I also apologize for all omissions.
The selection of contributions in this essay reflects primarily my personal involvement
rather than any measure of importance.
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
citation:
ama: 'Henzinger TA. Reminiscences of a Real-Time Researcher. In: Graf S, Pettersson
P, Steffen B, eds. Real Time and Such. Vol 15230. LNCS. Cham: Springer
Nature; 2024:154-164. doi:10.1007/978-3-031-73751-0_12'
apa: 'Henzinger, T. A. (2024). Reminiscences of a Real-Time Researcher. In S. Graf,
P. Pettersson, & B. Steffen (Eds.), Real Time and Such (Vol. 15230,
pp. 154–164). Cham: Springer Nature. https://doi.org/10.1007/978-3-031-73751-0_12'
chicago: 'Henzinger, Thomas A. “Reminiscences of a Real-Time Researcher.” In Real
Time and Such, edited by Susanne Graf, Paul Pettersson, and Bernhard Steffen,
15230:154–64. LNCS. Cham: Springer Nature, 2024. https://doi.org/10.1007/978-3-031-73751-0_12.'
ieee: 'T. A. Henzinger, “Reminiscences of a Real-Time Researcher,” in Real Time
and Such, vol. 15230, S. Graf, P. Pettersson, and B. Steffen, Eds. Cham: Springer
Nature, 2024, pp. 154–164.'
ista: 'Henzinger TA. 2024.Reminiscences of a Real-Time Researcher. In: Real Time
and Such. LNCS, vol. 15230, 154–164.'
mla: Henzinger, Thomas A. “Reminiscences of a Real-Time Researcher.” Real Time
and Such, edited by Susanne Graf et al., vol. 15230, Springer Nature, 2024,
pp. 154–64, doi:10.1007/978-3-031-73751-0_12.
short: T.A. Henzinger, in:, S. Graf, P. Pettersson, B. Steffen (Eds.), Real Time
and Such, Springer Nature, Cham, 2024, pp. 154–164.
corr_author: '1'
das_tickbox: '0'
date_created: 2024-11-18T09:10:06Z
date_published: 2024-10-23T00:00:00Z
date_updated: 2026-10-21T13:12:56Z
day: '23'
department:
- _id: ToHe
doi: 10.1007/978-3-031-73751-0_12
editor:
- first_name: Susanne
full_name: Graf, Susanne
last_name: Graf
- first_name: Paul
full_name: Pettersson, Paul
last_name: Pettersson
- first_name: Bernhard
full_name: Steffen, Bernhard
last_name: Steffen
fulldoi: https://doi.org/10.1007/978-3-031-73751-0_12
intvolume: ' 15230'
language:
- iso: eng
month: '10'
oa_version: None
page: 154-164
place: Cham
publication: Real Time and Such
publication_identifier:
eisbn:
- '9783031737510'
eissn:
- 1611-3349
isbn:
- '9783031737503'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
series_title: LNCS
status: public
supplementarymaterial: no
title: Reminiscences of a Real-Time Researcher
type: book_chapter
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15230
year: '2024'
...
---
_id: '15168'
abstract:
- lang: eng
text: 'A linearly ordered (LO) k-colouring of a hypergraph is a colouring of its
vertices with colours 1, … , k such that each edge contains a unique maximal colour.
Deciding whether an input hypergraph admits LO k-colouring with a fixed number
of colours is NP-complete (and in the special case of graphs, LO colouring coincides
with the usual graph colouring). Here, we investigate the complexity of approximating
the "linearly ordered chromatic number" of a hypergraph. We prove that the following
promise problem is NP-complete: Given a 3-uniform hypergraph, distinguish between
the case that it is LO 3-colourable, and the case that it is not even LO 4-colourable.
We prove this result by a combination of algebraic, topological, and combinatorial
methods, building on and extending a topological approach for studying approximate
graph colouring introduced by Krokhin, Opršal, Wrochna, and Živný (2023).'
acknowledgement: "Marek Filakovský: This research was supported by Charles University
(project PRIMUS/\r\n21/SCI/014), the Austrian Science Fund (FWF project P31312-N35),
and MSCAfellow5_MUNI\r\n(CZ.02.01.01/00/22_010/0003229). Tamio-Vesa Nakajima: This
research was funded by UKRI EP/X024431/1 and by a Clarendon Fund Scholarship. All
data is provided in full in the results section of this paper. Jakub Opršal: This
project has received funding from the European Union’s Horizon 2020 research and
innovation programme under the Marie Skłodowska-Curie Grant Agreement No 101034413.
Uli Wagner: This research was supported by the Austrian Science Fund (FWF project
P31312-N35)."
alternative_title:
- LIPIcs
article_number: '34'
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Filakovský, Marek
id: 3E8AF77E-F248-11E8-B48F-1D18A9856A87
last_name: Filakovský
- first_name: Tamio Vesa
full_name: Nakajima, Tamio Vesa
last_name: Nakajima
- first_name: Jakub
full_name: Opršal, Jakub
id: ec596741-c539-11ec-b829-c79322a91242
last_name: Opršal
orcid: 0000-0003-1245-3456
- first_name: Gianluca
full_name: Tasinato, Gianluca
id: 0433290C-AF8F-11E9-A4C7-F729E6697425
last_name: Tasinato
- first_name: Uli
full_name: Wagner, Uli
id: 36690CA2-F248-11E8-B48F-1D18A9856A87
last_name: Wagner
orcid: 0000-0002-1494-0568
citation:
ama: 'Filakovský M, Nakajima TV, Opršal J, Tasinato G, Wagner U. Hardness of linearly
ordered 4-colouring of 3-colourable 3-uniform hypergraphs. In: 41st International
Symposium on Theoretical Aspects of Computer Science. Vol 289. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2024. doi:10.4230/LIPIcs.STACS.2024.34'
apa: 'Filakovský, M., Nakajima, T. V., Opršal, J., Tasinato, G., & Wagner, U.
(2024). Hardness of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs.
In 41st International Symposium on Theoretical Aspects of Computer Science
(Vol. 289). Clermont-Ferrand, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.STACS.2024.34'
chicago: Filakovský, Marek, Tamio Vesa Nakajima, Jakub Opršal, Gianluca Tasinato,
and Uli Wagner. “Hardness of Linearly Ordered 4-Colouring of 3-Colourable 3-Uniform
Hypergraphs.” In 41st International Symposium on Theoretical Aspects of Computer
Science, Vol. 289. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.
https://doi.org/10.4230/LIPIcs.STACS.2024.34.
ieee: M. Filakovský, T. V. Nakajima, J. Opršal, G. Tasinato, and U. Wagner, “Hardness
of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs,” in 41st
International Symposium on Theoretical Aspects of Computer Science, Clermont-Ferrand,
France, 2024, vol. 289.
ista: 'Filakovský M, Nakajima TV, Opršal J, Tasinato G, Wagner U. 2024. Hardness
of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs. 41st International
Symposium on Theoretical Aspects of Computer Science. STACS: Symposium on Theoretical
Aspects of Computer Science, LIPIcs, vol. 289, 34.'
mla: Filakovský, Marek, et al. “Hardness of Linearly Ordered 4-Colouring of 3-Colourable
3-Uniform Hypergraphs.” 41st International Symposium on Theoretical Aspects
of Computer Science, vol. 289, 34, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2024, doi:10.4230/LIPIcs.STACS.2024.34.
short: M. Filakovský, T.V. Nakajima, J. Opršal, G. Tasinato, U. Wagner, in:, 41st
International Symposium on Theoretical Aspects of Computer Science, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2024.
conference:
end_date: 2024-03-14
location: Clermont-Ferrand, France
name: 'STACS: Symposium on Theoretical Aspects of Computer Science'
start_date: 2024-03-12
corr_author: '1'
das_tickbox: '0'
date_created: 2024-03-24T23:00:59Z
date_published: 2024-03-01T00:00:00Z
date_updated: 2026-10-21T13:23:55Z
day: '01'
ddc:
- '510'
department:
- _id: UlWa
doi: 10.4230/LIPIcs.STACS.2024.34
ec_funded: 1
external_id:
arxiv:
- '2312.12981'
isi:
- '001300393400034'
file:
- access_level: open_access
checksum: 0524d4189fd1ed08989546511343edf3
content_type: application/pdf
creator: dernst
date_created: 2024-03-25T07:44:30Z
date_updated: 2024-03-25T07:44:30Z
file_id: '15175'
file_name: 2024_LIPICs_Filakovsky.pdf
file_size: 927290
relation: main_file
success: 1
file_date_updated: 2024-03-25T07:44:30Z
fulldoi: https://doi.org/10.4230/LIPIcs.STACS.2024.34
has_accepted_license: '1'
intvolume: ' 289'
isi: 1
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
project:
- _id: 26611F5C-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P31312
name: Algorithms for Embeddings and Homotopy Theory
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 41st International Symposium on Theoretical Aspects of Computer Science
publication_identifier:
eissn:
- 1868-8969
isbn:
- '9783959773119'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
record:
- id: '22247'
relation: later_version
status: public
- id: '20339'
relation: dissertation_contains
status: public
researchdata_availability: yes
scopus_import: '1'
status: public
supplementarymaterial: yes
title: Hardness of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 289
year: '2024'
...
---
OA_place: publisher
OA_type: hybrid
_id: '9651'
abstract:
- lang: eng
text: We introduce a hierachy of equivalence relations on the set of separated nets
of a given Euclidean space, indexed by concave increasing functions ϕ:(0,∞)→(0,∞).
Two separated nets are called ϕ-displacement equivalent if, roughly speaking,
there is a bijection between them which, for large radii R, displaces points of
norm at most R by something of order at most ϕ(R). We show that the spectrum of
ϕ-displacement equivalence spans from the established notion of bounded displacement
equivalence, which corresponds to bounded ϕ, to the indiscrete equivalence relation,
coresponding to ϕ(R)∈Ω(R), in which all separated nets are equivalent. In between
the two ends of this spectrum, the notions of ϕ-displacement equivalence are shown
to be pairwise distinct with respect to the asymptotic classes of ϕ(R) for R→∞.
We further undertake a comparison of our notion of ϕ-displacement equivalence
with previously studied relations on separated nets. Particular attention is given
to the interaction of the notions of ϕ-displacement equivalence with that of bilipschitz
equivalence.
acknowledgement: 'Open access funding provided by Institute of Science and Technology
(IST Austria). This work was started while both authors were employed at the University
of Innsbruck and enjoyed the full support of Austrian Science Fund (FWF): P 30902-N35.
It was continued when the first named author was employed at University of Leipzig
and the second named author was employed at Institute of Science and Technology
of Austria, where he was supported by an IST Fellowship.'
article_number: '15'
article_processing_charge: Yes (via OA deal)
article_type: original
arxiv: 1
author:
- first_name: Michael
full_name: Dymond, Michael
last_name: Dymond
- first_name: Vojtech
full_name: Kaluza, Vojtech
id: 21AE5134-9EAC-11EA-BEA2-D7BD3DDC885E
last_name: Kaluza
orcid: 0000-0002-2512-8698
citation:
ama: Dymond M, Kaluza V. Divergence of separated nets with respect to displacement
equivalence. Geometriae Dedicata. 2024;218. doi:10.1007/s10711-023-00862-3
apa: Dymond, M., & Kaluza, V. (2024). Divergence of separated nets with respect
to displacement equivalence. Geometriae Dedicata. Springer Nature. https://doi.org/10.1007/s10711-023-00862-3
chicago: Dymond, Michael, and Vojtech Kaluza. “Divergence of Separated Nets with
Respect to Displacement Equivalence.” Geometriae Dedicata. Springer Nature,
2024. https://doi.org/10.1007/s10711-023-00862-3.
ieee: M. Dymond and V. Kaluza, “Divergence of separated nets with respect to displacement
equivalence,” Geometriae Dedicata, vol. 218. Springer Nature, 2024.
ista: Dymond M, Kaluza V. 2024. Divergence of separated nets with respect to displacement
equivalence. Geometriae Dedicata. 218, 15.
mla: Dymond, Michael, and Vojtech Kaluza. “Divergence of Separated Nets with Respect
to Displacement Equivalence.” Geometriae Dedicata, vol. 218, 15, Springer
Nature, 2024, doi:10.1007/s10711-023-00862-3.
short: M. Dymond, V. Kaluza, Geometriae Dedicata 218 (2024).
corr_author: '1'
das_tickbox: '1'
dataavailabilitystatement: Data sharing not applicable to this article as no datasets
were generated or analysed during the current study.
date_created: 2021-07-14T07:01:27Z
date_published: 2024-02-01T00:00:00Z
date_updated: 2026-10-21T13:22:57Z
day: '01'
ddc:
- '510'
department:
- _id: UlWa
doi: 10.1007/s10711-023-00862-3
external_id:
arxiv:
- '2102.13046'
isi:
- '001105681500001'
pmid:
- '38021107'
file:
- access_level: open_access
checksum: 9418534ac2f3d6f1f091a8b8ccaed01e
content_type: application/pdf
creator: dernst
date_created: 2024-07-16T10:14:13Z
date_updated: 2024-07-16T10:14:13Z
file_id: '17257'
file_name: 2024_GeometriaeDedicata_Dymond.pdf
file_size: 540981
relation: main_file
success: 1
file_date_updated: 2024-07-16T10:14:13Z
fulldoi: https://doi.org/10.1007/s10711-023-00862-3
has_accepted_license: '1'
intvolume: ' 218'
isi: 1
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
pmid: 1
publication: Geometriae Dedicata
publication_identifier:
eissn:
- 1572-9168
issn:
- 0046-5755
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: not applicable
scopus_import: '1'
status: public
supplementarymaterial: no
title: Divergence of separated nets with respect to displacement 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: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 218
year: '2024'
...
---
_id: '14660'
abstract:
- lang: eng
text: "The classical Steinitz theorem states that if the origin belongs to the interior
of the convex hull of a set \U0001D446⊂ℝ\U0001D451, then there are at most 2\U0001D451
points of \U0001D446 whose convex hull contains the origin in the interior. Bárány,
Katchalski,and Pach proved the following quantitative version of Steinitz’s theorem.
Let \U0001D444 be a convex polytope in ℝ\U0001D451 containing the standard Euclidean
unit ball \U0001D401\U0001D451. Then there exist at most 2\U0001D451 vertices
of \U0001D444 whose convex hull \U0001D444′ satisfies \U0001D45F\U0001D401\U0001D451⊂\U0001D444′
with \U0001D45F⩾\U0001D451−2\U0001D451. They conjectured that \U0001D45F⩾\U0001D450\U0001D451−1∕2
holds with a universal constant \U0001D450>0. We prove \U0001D45F⩾15\U0001D4512,
the first polynomial lower bound on \U0001D45F. Furthermore, we show that \U0001D45F
is not greater than 2/√\U0001D451."
acknowledgement: M.N. was supported by the János Bolyai Scholarship of the Hungarian
Academy of Sciences aswell as the National Research, Development and Innovation
Fund (NRDI) grants K119670 andK131529, and the ÚNKP-22-5 New National Excellence
Program of the Ministry for Innovationand Technology from the source of the NRDI
as well as the ELTE TKP 2021-NKTA-62 fundingscheme
article_processing_charge: Yes (via OA deal)
article_type: original
arxiv: 1
author:
- first_name: Grigory
full_name: Ivanov, Grigory
id: 87744F66-5C6F-11EA-AFE0-D16B3DDC885E
last_name: Ivanov
orcid: 0000-0002-5021-3982
- first_name: Márton
full_name: Naszódi, Márton
last_name: Naszódi
citation:
ama: 'Ivanov G, Naszódi M. Quantitative Steinitz theorem: A polynomial bound. Bulletin
of the London Mathematical Society. 2024;56(2):796-802. doi:10.1112/blms.12965'
apa: 'Ivanov, G., & Naszódi, M. (2024). Quantitative Steinitz theorem: A polynomial
bound. Bulletin of the London Mathematical Society. London Mathematical
Society. https://doi.org/10.1112/blms.12965'
chicago: 'Ivanov, Grigory, and Márton Naszódi. “Quantitative Steinitz Theorem: A
Polynomial Bound.” Bulletin of the London Mathematical Society. London
Mathematical Society, 2024. https://doi.org/10.1112/blms.12965.'
ieee: 'G. Ivanov and M. Naszódi, “Quantitative Steinitz theorem: A polynomial bound,”
Bulletin of the London Mathematical Society, vol. 56, no. 2. London Mathematical
Society, pp. 796–802, 2024.'
ista: 'Ivanov G, Naszódi M. 2024. Quantitative Steinitz theorem: A polynomial bound.
Bulletin of the London Mathematical Society. 56(2), 796–802.'
mla: 'Ivanov, Grigory, and Márton Naszódi. “Quantitative Steinitz Theorem: A Polynomial
Bound.” Bulletin of the London Mathematical Society, vol. 56, no. 2, London
Mathematical Society, 2024, pp. 796–802, doi:10.1112/blms.12965.'
short: G. Ivanov, M. Naszódi, Bulletin of the London Mathematical Society 56 (2024)
796–802.
corr_author: '1'
das_tickbox: '0'
date_created: 2023-12-10T23:00:58Z
date_published: 2024-02-01T00:00:00Z
date_updated: 2026-10-21T13:23:20Z
day: '01'
ddc:
- '510'
department:
- _id: UlWa
doi: 10.1112/blms.12965
external_id:
arxiv:
- '2212.04308'
isi:
- '001113277100001'
file:
- access_level: open_access
checksum: 30ea0694757bc668cf7cd15ae357b35e
content_type: application/pdf
creator: dernst
date_created: 2024-07-16T10:35:10Z
date_updated: 2024-07-16T10:35:10Z
file_id: '17259'
file_name: 2024_BulletinLondonMathSoc_Ivanov.pdf
file_size: 111756
relation: main_file
success: 1
file_date_updated: 2024-07-16T10:35:10Z
fulldoi: https://doi.org/10.1112/blms.12965
has_accepted_license: '1'
intvolume: ' 56'
isi: 1
issue: '2'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: 796-802
publication: Bulletin of the London Mathematical Society
publication_identifier:
eissn:
- 1469-2120
issn:
- 0024-6093
publication_status: published
publisher: London Mathematical Society
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Quantitative Steinitz theorem: A polynomial bound'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 56
year: '2024'
...
---
OA_place: publisher
OA_type: hybrid
_id: '18617'
abstract:
- lang: eng
text: "Any complex-valued polynomial on (Rn)k decomposes into an algebraic combination
of O(n)-invariant polynomials and harmonic polynomials. This decomposition, separation
of variables, is granted to be unique if n≥2k−1. We prove that the condition n≥2k−1
is not only sufficient, but also necessary for uniqueness of the separation. Moreover,
we describe the structure of non-uniqueness of the separation in the boundary
cases when n=2k−2 and n=2k−3.\r\nFormally, we study the kernel of a multiplication
map ϕ carrying out separation of variables. We devise a general algorithmic procedure
for describing Ker ϕ in the restricted non-stable range k≤n<2k−1. In the full
non-stable range n<2k−1, we give formulas for highest weights of generators of
the kernel as well as formulas for its Hilbert series. Using the developed methods,
we obtain a list of highest weight vectors generating Ker ϕ."
acknowledgement: The author is sincerely grateful for guidance, advice and valuable
feedback from Roman Lávička.
article_processing_charge: Yes (via OA deal)
article_type: original
arxiv: 1
author:
- first_name: Daniel
full_name: Beďatš, Daniel
id: 78ea3cc9-31e7-11ee-aa02-a6169bbfe1f1
last_name: Beďatš
orcid: 0009-0004-1828-0044
citation:
ama: Beďatš D. Separation of variables for scalar-valued polynomials in the non-stable
range. Journal of Algebra. 2024;651:281-304. doi:10.1016/j.jalgebra.2024.04.013
apa: Beďatš, D. (2024). Separation of variables for scalar-valued polynomials in
the non-stable range. Journal of Algebra. Elsevier. https://doi.org/10.1016/j.jalgebra.2024.04.013
chicago: Beďatš, Daniel. “Separation of Variables for Scalar-Valued Polynomials
in the Non-Stable Range.” Journal of Algebra. Elsevier, 2024. https://doi.org/10.1016/j.jalgebra.2024.04.013.
ieee: D. Beďatš, “Separation of variables for scalar-valued polynomials in the non-stable
range,” Journal of Algebra, vol. 651. Elsevier, pp. 281–304, 2024.
ista: Beďatš D. 2024. Separation of variables for scalar-valued polynomials in the
non-stable range. Journal of Algebra. 651, 281–304.
mla: Beďatš, Daniel. “Separation of Variables for Scalar-Valued Polynomials in the
Non-Stable Range.” Journal of Algebra, vol. 651, Elsevier, 2024, pp. 281–304,
doi:10.1016/j.jalgebra.2024.04.013.
short: D. Beďatš, Journal of Algebra 651 (2024) 281–304.
corr_author: '1'
das_tickbox: '1'
dataavailabilitystatement: "No data was used for the research described in the article.\r\n"
date_created: 2024-12-04T07:58:45Z
date_published: 2024-08-01T00:00:00Z
date_updated: 2026-10-21T13:24:58Z
day: '01'
ddc:
- '510'
department:
- _id: UlWa
doi: 10.1016/j.jalgebra.2024.04.013
external_id:
arxiv:
- '2309.11154'
isi:
- '001232775600001'
file:
- access_level: open_access
checksum: 7b01c89128ba16d5334dfab389a03878
content_type: application/pdf
creator: dernst
date_created: 2024-12-09T13:56:26Z
date_updated: 2024-12-09T13:56:26Z
file_id: '18638'
file_name: 2024_JourAlgebra_Bedats.pdf
file_size: 486969
relation: main_file
success: 1
file_date_updated: 2024-12-09T13:56:26Z
fulldoi: https://doi.org/10.1016/j.jalgebra.2024.04.013
has_accepted_license: '1'
intvolume: ' 651'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 281-304
publication: Journal of Algebra
publication_identifier:
issn:
- 0021-8693
publication_status: published
publisher: Elsevier
quality_controlled: '1'
researchdata_availability: not applicable
scopus_import: '1'
status: public
supplementarymaterial: no
title: Separation of variables for scalar-valued polynomials in the non-stable range
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 651
year: '2024'
...