---
_id: '10602'
abstract:
- lang: eng
text: Transforming ω-automata into parity automata is traditionally done using appearance
records. We present an efficient variant of this idea, tailored to Rabin automata,
and several optimizations applicable to all appearance records. We compare the
methods experimentally and show that our method produces significantly smaller
automata than previous approaches.
acknowledgement: This work is partially funded by the German Research Foundation (DFG)
projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification
(No. 383882557), and the Alexander von Humboldt Foundation with funds from the German
Federal Ministry of Education and Research. It is an extended version of [21], including
all proofs together with further explanations and examples. Moreover, we provide
a new, more efficient construction based on (total) preorders, unifying previous
optimizations. Experiments are performed with a new, performant implementation,
comparing our approach to the current state of the art.
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Clara
full_name: Waldmann, Clara
last_name: Waldmann
- first_name: Maximilian
full_name: Weininger, Maximilian
last_name: Weininger
citation:
ama: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
with preorders. Acta Informatica. 2022;59:585-618. doi:10.1007/s00236-021-00412-y
apa: Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2022).
Index appearance record with preorders. Acta Informatica. Springer Nature.
https://doi.org/10.1007/s00236-021-00412-y
chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
“Index Appearance Record with Preorders.” Acta Informatica. Springer Nature,
2022. https://doi.org/10.1007/s00236-021-00412-y.
ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
record with preorders,” Acta Informatica, vol. 59. Springer Nature, pp.
585–618, 2022.
ista: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance
record with preorders. Acta Informatica. 59, 585–618.
mla: Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” Acta Informatica,
vol. 59, Springer Nature, 2022, pp. 585–618, doi:10.1007/s00236-021-00412-y.
short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica
59 (2022) 585–618.
date_created: 2022-01-06T12:37:27Z
date_published: 2022-10-01T00:00:00Z
date_updated: 2023-08-02T13:49:28Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s00236-021-00412-y
external_id:
isi:
- '000735765500001'
file:
- access_level: open_access
checksum: bf1c195b6aaf59e8530cf9e3a9d731f7
content_type: application/pdf
creator: cchlebak
date_created: 2022-01-07T07:50:31Z
date_updated: 2022-01-07T07:50:31Z
file_id: '10603'
file_name: 2021_ActaInfor_Křetínský.pdf
file_size: 1066082
relation: main_file
success: 1
file_date_updated: 2022-01-07T07:50:31Z
has_accepted_license: '1'
intvolume: ' 59'
isi: 1
keyword:
- computer networks and communications
- information systems
- software
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 585-618
project:
- _id: B67AFEDC-15C9-11EA-A837-991A96BB2854
name: IST Austria Open Access Fund
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Index appearance record with preorders
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 59
year: '2022'
...
---
_id: '10731'
abstract:
- lang: eng
text: Motivated by COVID-19, we develop and analyze a simple stochastic model for
the spread of disease in human population. We track how the number of infected
and critically ill people develops over time in order to estimate the demand that
is imposed on the hospital system. To keep this demand under control, we consider
a class of simple policies for slowing down and reopening society and we compare
their efficiency in mitigating the spread of the virus from several different
points of view. We find that in order to avoid overwhelming of the hospital system,
a policy must impose a harsh lockdown or it must react swiftly (or both). While
reacting swiftly is universally beneficial, being harsh pays off only when the
country is patient about reopening and when the neighboring countries coordinate
their mitigation efforts. Our work highlights the importance of acting decisively
when closing down and the importance of patience and coordination between neighboring
countries when reopening.
acknowledgement: 'K.C. acknowledges support from ERC Consolidator Grant No. (863818:
ForM-SMart). A.P. acknowledges support from FWF Grant No. J-4220. M.A.N. acknowledges
support from Office of Naval Research grant N00014-16-1-2914 and from the John Templeton
Foundation.'
article_number: '1526'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
- first_name: Josef
full_name: Tkadlec, Josef
last_name: Tkadlec
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin A.
full_name: Nowak, Martin A.
last_name: Nowak
citation:
ama: Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Infection dynamics
of COVID-19 virus under lockdown and reopening. Scientific Reports. 2022;12(1).
doi:10.1038/s41598-022-05333-5
apa: Svoboda, J., Tkadlec, J., Pavlogiannis, A., Chatterjee, K., & Nowak, M.
A. (2022). Infection dynamics of COVID-19 virus under lockdown and reopening.
Scientific Reports. Springer Nature. https://doi.org/10.1038/s41598-022-05333-5
chicago: Svoboda, Jakub, Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee,
and Martin A. Nowak. “Infection Dynamics of COVID-19 Virus under Lockdown and
Reopening.” Scientific Reports. Springer Nature, 2022. https://doi.org/10.1038/s41598-022-05333-5.
ieee: J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Infection
dynamics of COVID-19 virus under lockdown and reopening,” Scientific Reports,
vol. 12, no. 1. Springer Nature, 2022.
ista: Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2022. Infection
dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. 12(1),
1526.
mla: Svoboda, Jakub, et al. “Infection Dynamics of COVID-19 Virus under Lockdown
and Reopening.” Scientific Reports, vol. 12, no. 1, 1526, Springer Nature,
2022, doi:10.1038/s41598-022-05333-5.
short: J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Scientific
Reports 12 (2022).
date_created: 2022-02-06T23:01:30Z
date_published: 2022-01-27T00:00:00Z
date_updated: 2025-07-14T09:10:12Z
day: '27'
ddc:
- '570'
department:
- _id: KrCh
doi: 10.1038/s41598-022-05333-5
ec_funded: 1
external_id:
arxiv:
- '2012.15155'
isi:
- '000749198000039'
file:
- access_level: open_access
checksum: 247afd30c173390940f099ead35a28ed
content_type: application/pdf
creator: alisjak
date_created: 2022-02-07T14:57:59Z
date_updated: 2022-02-07T14:57:59Z
file_id: '10744'
file_name: 2022_ScientificReports_Svoboda.pdf
file_size: 2971922
relation: main_file
success: 1
file_date_updated: 2022-02-07T14:57:59Z
has_accepted_license: '1'
intvolume: ' 12'
isi: 1
issue: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Scientific Reports
publication_identifier:
eissn:
- 2045-2322
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Infection dynamics of COVID-19 virus under lockdown and reopening
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 12
year: '2022'
...
---
_id: '11402'
abstract:
- lang: eng
text: Fixed-horizon planning considers a weighted graph and asks to construct a
path that maximizes the sum of weights for a given time horizon T. However, in
many scenarios, the time horizon is not fixed, but the stopping time is chosen
according to some distribution such that the expected stopping time is T. If the
stopping-time distribution is not known, then to ensure robustness, the distribution
is chosen by an adversary as the worst-case scenario. A stationary plan for every
vertex always chooses the same outgoing edge. For fixed horizon or fixed stopping-time
distribution, stationary plans are not sufficient for optimality. Quite surprisingly
we show that when an adversary chooses the stopping-time distribution with expected
stopping-time T, then stationary plans are sufficient. While computing optimal
stationary plans for fixed horizon is NP-complete, we show that computing optimal
stationary plans under adversarial stopping-time distribution can be achieved
in polynomial time.
acknowledgement: This work was partially supported by Austrian Science Fund (FWF)
NFN Grant No RiSE/SHiNE S11407 and by the grant ERC CoG 863818 (ForM-SMArt).
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
citation:
ama: Chatterjee K, Doyen L. Graph planning with expected finite horizon. Journal
of Computer and System Sciences. 2022;129:1-21. doi:10.1016/j.jcss.2022.04.003
apa: Chatterjee, K., & Doyen, L. (2022). Graph planning with expected finite
horizon. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2022.04.003
chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Graph Planning with Expected
Finite Horizon.” Journal of Computer and System Sciences. Elsevier, 2022.
https://doi.org/10.1016/j.jcss.2022.04.003.
ieee: K. Chatterjee and L. Doyen, “Graph planning with expected finite horizon,”
Journal of Computer and System Sciences, vol. 129. Elsevier, pp. 1–21,
2022.
ista: Chatterjee K, Doyen L. 2022. Graph planning with expected finite horizon.
Journal of Computer and System Sciences. 129, 1–21.
mla: Chatterjee, Krishnendu, and Laurent Doyen. “Graph Planning with Expected Finite
Horizon.” Journal of Computer and System Sciences, vol. 129, Elsevier,
2022, pp. 1–21, doi:10.1016/j.jcss.2022.04.003.
short: K. Chatterjee, L. Doyen, Journal of Computer and System Sciences 129 (2022)
1–21.
date_created: 2022-05-22T22:01:40Z
date_published: 2022-11-01T00:00:00Z
date_updated: 2025-07-14T09:09:54Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.jcss.2022.04.003
ec_funded: 1
external_id:
arxiv:
- '1802.03642'
isi:
- '000805002800001'
intvolume: ' 129'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.1802.03642'
month: '11'
oa: 1
oa_version: Preprint
page: 1-21
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Journal of Computer and System Sciences
publication_identifier:
eissn:
- 1090-2724
issn:
- 0022-0000
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '7402'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Graph planning with expected finite horizon
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 129
year: '2022'
...
---
_id: '11459'
abstract:
- lang: eng
text: 'We present a novel approach to differential cost analysis that, given a program
revision, attempts to statically bound the difference in resource usage, or cost,
between the two program versions. Differential cost analysis is particularly interesting
because of the many compelling applications for it, such as detecting resource-use
regressions at code-review time or proving the absence of certain side-channel
vulnerabilities. One prior approach to differential cost analysis is to apply
relational reasoning that conceptually constructs a product program on which one
can over-approximate the difference in costs between the two program versions.
However, a significant challenge in any relational approach is effectively aligning
the program versions to get precise results. In this paper, our key insight is
that we can avoid the need for and the limitations of program alignment if, instead,
we bound the difference of two cost-bound summaries rather than directly bounding
the concrete cost difference. In particular, our method computes a threshold value
for the maximal difference in cost between two program versions simultaneously
using two kinds of cost-bound summaries---a potential function that evaluates
to an upper bound for the cost incurred in the first program and an anti-potential
function that evaluates to a lower bound for the cost incurred in the second.
Our method has a number of desirable properties: it can be fully automated, it
allows optimizing the threshold value on relative cost, it is suitable for programs
that are not syntactically similar, and it supports non-determinism. We have evaluated
an implementation of our approach on a number of program pairs collected from
the literature, and we find that our method computes tight threshold values on
relative cost in most examples.'
acknowledgement: "We thank Shaun Willows, Thomas Lugnet, and the Living Room Application
Vending team for suggesting threshold\r\nbounds as a developer-friendly way to interact
with a differential cost analyzer, and we thank Jim Christy, Daniel\r\nSchoepe,
and the Prime Video Automated Reasoning team for their support and helpful suggestions
throughout the\r\nproject. We also thank Michael Emmi for feedback on an earlier
version of this paper. And finally, we thank the anonymous reviewers for their useful
feedback and Aws Albarghouthi for shepherding the final version of the paper. Ðorđe
Žikelić was also partially supported by ERC CoG 863818 (FoRM-SMArt)."
article_processing_charge: No
arxiv: 1
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Bor-Yuh Evan
full_name: Chang, Bor-Yuh Evan
last_name: Chang
- first_name: Pauline
full_name: Bolignano, Pauline
last_name: Bolignano
- first_name: Franco
full_name: Raimondi, Franco
last_name: Raimondi
citation:
ama: 'Zikelic D, Chang B-YE, Bolignano P, Raimondi F. Differential cost analysis
with simultaneous potentials and anti-potentials. In: Proceedings of the 43rd
ACM SIGPLAN International Conference on Programming Language Design and Implementation.
Association for Computing Machinery; 2022:442-457. doi:10.1145/3519939.3523435'
apa: 'Zikelic, D., Chang, B.-Y. E., Bolignano, P., & Raimondi, F. (2022). Differential
cost analysis with simultaneous potentials and anti-potentials. In Proceedings
of the 43rd ACM SIGPLAN International Conference on Programming Language Design
and Implementation (pp. 442–457). San Diego, CA, United States: Association
for Computing Machinery. https://doi.org/10.1145/3519939.3523435'
chicago: Zikelic, Dorde, Bor-Yuh Evan Chang, Pauline Bolignano, and Franco Raimondi.
“Differential Cost Analysis with Simultaneous Potentials and Anti-Potentials.”
In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming
Language Design and Implementation, 442–57. Association for Computing Machinery,
2022. https://doi.org/10.1145/3519939.3523435.
ieee: D. Zikelic, B.-Y. E. Chang, P. Bolignano, and F. Raimondi, “Differential cost
analysis with simultaneous potentials and anti-potentials,” in Proceedings
of the 43rd ACM SIGPLAN International Conference on Programming Language Design
and Implementation, San Diego, CA, United States, 2022, pp. 442–457.
ista: 'Zikelic D, Chang B-YE, Bolignano P, Raimondi F. 2022. Differential cost analysis
with simultaneous potentials and anti-potentials. Proceedings of the 43rd ACM
SIGPLAN International Conference on Programming Language Design and Implementation.
PLDI: Programming Language Design and Implementation, 442–457.'
mla: Zikelic, Dorde, et al. “Differential Cost Analysis with Simultaneous Potentials
and Anti-Potentials.” Proceedings of the 43rd ACM SIGPLAN International Conference
on Programming Language Design and Implementation, Association for Computing
Machinery, 2022, pp. 442–57, doi:10.1145/3519939.3523435.
short: D. Zikelic, B.-Y.E. Chang, P. Bolignano, F. Raimondi, in:, Proceedings of
the 43rd ACM SIGPLAN International Conference on Programming Language Design and
Implementation, Association for Computing Machinery, 2022, pp. 442–457.
conference:
end_date: 2022-06-17
location: San Diego, CA, United States
name: 'PLDI: Programming Language Design and Implementation'
start_date: 2022-06-13
date_created: 2022-06-21T09:26:15Z
date_published: 2022-06-09T00:00:00Z
date_updated: 2025-07-14T09:09:54Z
day: '09'
ddc:
- '000'
department:
- _id: GradSch
- _id: KrCh
doi: 10.1145/3519939.3523435
ec_funded: 1
external_id:
arxiv:
- '2204.00870'
isi:
- '000850435600030'
file:
- access_level: open_access
checksum: 7eb915a2ca5b5ce4729321f33b2e16e1
content_type: application/pdf
creator: dernst
date_created: 2022-06-27T07:38:21Z
date_updated: 2022-06-27T07:38:21Z
file_id: '11466'
file_name: 2022_PLDI_Zikelic.pdf
file_size: 318697
relation: main_file
success: 1
file_date_updated: 2022-06-27T07:38:21Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 442-457
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming
Language Design and Implementation
publication_identifier:
isbn:
- '9781450392655'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Differential cost analysis with simultaneous potentials and anti-potentials
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2022'
...
---
_id: '11938'
abstract:
- lang: eng
text: A matching is compatible to two or more labeled point sets of size n with
labels {1, . . . , n} if its straight-line drawing on each of these point sets
is crossing-free. We study the maximum number of edges in a matching compatible
to two or more labeled point sets in general position in the plane. We show that
for any two labeled sets of n points in convex position there exists a compatible
matching with ⌊√2n + 1 − 1⌋ edges. More generally, for any ℓ labeled point sets
we construct compatible matchings of size Ω(n1/ℓ). As a corresponding upper bound,
we use probabilistic arguments to show that for any ℓ given sets of n points there
exists a labeling of each set such that the largest compatible matching has O(n2/(ℓ+1))
edges. Finally, we show that Θ(log n) copies of any set of n points are necessary
and sufficient for the existence of labelings of these point sets such that any
compatible matching consists only of a single edge.
acknowledgement: 'A.A. funded by the Marie Sklodowska-Curie grant agreement No 754411.
Z.M. partially funded by Wittgenstein Prize, Austrian Science Fund (FWF), grant
no. Z 342-N31. I.P., D.P., and B.V. partially supported by FWF within the collaborative
DACH project Arrangements and Drawings as FWF project I 3340-N35. A.P. supported
by a Schrödinger fellowship of the FWF: J-3847-N35. J.T. partially supported by
ERC Start grant no. (279307: Graph Games), FWF grant no. P23499-N23 and S11407-N23
(RiSE).'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Oswin
full_name: Aichholzer, Oswin
last_name: Aichholzer
- first_name: Alan M
full_name: Arroyo Guevara, Alan M
id: 3207FDC6-F248-11E8-B48F-1D18A9856A87
last_name: Arroyo Guevara
orcid: 0000-0003-2401-8670
- first_name: Zuzana
full_name: Masárová, Zuzana
id: 45CFE238-F248-11E8-B48F-1D18A9856A87
last_name: Masárová
orcid: 0000-0002-6660-1322
- first_name: Irene
full_name: Parada, Irene
last_name: Parada
- first_name: Daniel
full_name: Perz, Daniel
last_name: Perz
- first_name: Alexander
full_name: Pilz, Alexander
last_name: Pilz
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Birgit
full_name: Vogtenhuber, Birgit
last_name: Vogtenhuber
citation:
ama: Aichholzer O, Arroyo Guevara AM, Masárová Z, et al. On compatible matchings.
Journal of Graph Algorithms and Applications. 2022;26(2):225-240. doi:10.7155/jgaa.00591
apa: Aichholzer, O., Arroyo Guevara, A. M., Masárová, Z., Parada, I., Perz, D.,
Pilz, A., … Vogtenhuber, B. (2022). On compatible matchings. Journal of Graph
Algorithms and Applications. Brown University. https://doi.org/10.7155/jgaa.00591
chicago: Aichholzer, Oswin, Alan M Arroyo Guevara, Zuzana Masárová, Irene Parada,
Daniel Perz, Alexander Pilz, Josef Tkadlec, and Birgit Vogtenhuber. “On Compatible
Matchings.” Journal of Graph Algorithms and Applications. Brown University,
2022. https://doi.org/10.7155/jgaa.00591.
ieee: O. Aichholzer et al., “On compatible matchings,” Journal of Graph
Algorithms and Applications, vol. 26, no. 2. Brown University, pp. 225–240,
2022.
ista: Aichholzer O, Arroyo Guevara AM, Masárová Z, Parada I, Perz D, Pilz A, Tkadlec
J, Vogtenhuber B. 2022. On compatible matchings. Journal of Graph Algorithms and
Applications. 26(2), 225–240.
mla: Aichholzer, Oswin, et al. “On Compatible Matchings.” Journal of Graph Algorithms
and Applications, vol. 26, no. 2, Brown University, 2022, pp. 225–40, doi:10.7155/jgaa.00591.
short: O. Aichholzer, A.M. Arroyo Guevara, Z. Masárová, I. Parada, D. Perz, A. Pilz,
J. Tkadlec, B. Vogtenhuber, Journal of Graph Algorithms and Applications 26 (2022)
225–240.
date_created: 2022-08-21T22:01:56Z
date_published: 2022-06-01T00:00:00Z
date_updated: 2023-02-23T13:54:21Z
day: '01'
ddc:
- '000'
department:
- _id: UlWa
- _id: HeEd
- _id: KrCh
doi: 10.7155/jgaa.00591
ec_funded: 1
external_id:
arxiv:
- '2101.03928'
file:
- access_level: open_access
checksum: dc6e255e3558faff924fd9e370886c11
content_type: application/pdf
creator: dernst
date_created: 2022-08-22T06:42:42Z
date_updated: 2022-08-22T06:42:42Z
file_id: '11940'
file_name: 2022_JourGraphAlgorithmsApplic_Aichholzer.pdf
file_size: 694538
relation: main_file
success: 1
file_date_updated: 2022-08-22T06:42:42Z
has_accepted_license: '1'
intvolume: ' 26'
issue: '2'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 225-240
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
- _id: 268116B8-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z00342
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: Journal of Graph Algorithms and Applications
publication_identifier:
issn:
- 1526-1719
publication_status: published
publisher: Brown University
quality_controlled: '1'
related_material:
record:
- id: '9296'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: On compatible matchings
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 26
year: '2022'
...
---
_id: '12000'
abstract:
- lang: eng
text: "We consider the quantitative problem of obtaining lower-bounds on the probability
of termination of a given non-deterministic probabilistic program. Specifically,
given a non-termination threshold p∈[0,1], we aim for certificates proving that
the program terminates with probability at least 1−p. The basic idea of our approach
is to find a terminating stochastic invariant, i.e. a subset SI of program states
such that (i) the probability of the program ever leaving SI is no more than p,
and (ii) almost-surely, the program either leaves SI or terminates.\r\n\r\nWhile
stochastic invariants are already well-known, we provide the first proof that
the idea above is not only sound, but also complete for quantitative termination
analysis. We then introduce a novel sound and complete characterization of stochastic
invariants that enables template-based approaches for easy synthesis of quantitative
termination certificates, especially in affine or polynomial forms. Finally, by
combining this idea with the existing martingale-based methods that are relatively
complete for qualitative termination analysis, we obtain the first automated,
sound, and relatively complete algorithm for quantitative termination analysis.
Notably, our completeness guarantees for quantitative termination analysis are
as strong as the best-known methods for the qualitative variant.\r\n\r\nOur prototype
implementation demonstrates the effectiveness of our approach on various probabilistic
programs. We also demonstrate that our algorithm certifies lower bounds on termination
probability for probabilistic programs that are beyond the reach of previous methods."
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt),
the HKUST-Kaisa Joint Research Institute Project Grant HKJRI3A-055, the HKUST Startup
Grant R9272 and the European Union’s Horizon 2020 research and innovation programme
under the Marie Skłodowska-Curie Grant Agreement No. 665385.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. Sound and complete
certificates for auantitative termination analysis of probabilistic programs.
In: Proceedings of the 34th International Conference on Computer Aided Verification.
Vol 13371. Springer; 2022:55-78. doi:10.1007/978-3-031-13185-1_4'
apa: 'Chatterjee, K., Goharshady, A. K., Meggendorfer, T., & Zikelic, D. (2022).
Sound and complete certificates for auantitative termination analysis of probabilistic
programs. In Proceedings of the 34th International Conference on Computer Aided
Verification (Vol. 13371, pp. 55–78). Haifa, Israel: Springer. https://doi.org/10.1007/978-3-031-13185-1_4'
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Tobias Meggendorfer,
and Dorde Zikelic. “Sound and Complete Certificates for Auantitative Termination
Analysis of Probabilistic Programs.” In Proceedings of the 34th International
Conference on Computer Aided Verification, 13371:55–78. Springer, 2022. https://doi.org/10.1007/978-3-031-13185-1_4.
ieee: K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and D. Zikelic, “Sound and complete
certificates for auantitative termination analysis of probabilistic programs,”
in Proceedings of the 34th International Conference on Computer Aided Verification,
Haifa, Israel, 2022, vol. 13371, pp. 55–78.
ista: 'Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2022. Sound and complete
certificates for auantitative termination analysis of probabilistic programs.
Proceedings of the 34th International Conference on Computer Aided Verification.
CAV: Computer Aided Verification, LNCS, vol. 13371, 55–78.'
mla: Chatterjee, Krishnendu, et al. “Sound and Complete Certificates for Auantitative
Termination Analysis of Probabilistic Programs.” Proceedings of the 34th International
Conference on Computer Aided Verification, vol. 13371, Springer, 2022, pp.
55–78, doi:10.1007/978-3-031-13185-1_4.
short: K. Chatterjee, A.K. Goharshady, T. Meggendorfer, D. Zikelic, in:, Proceedings
of the 34th International Conference on Computer Aided Verification, Springer,
2022, pp. 55–78.
conference:
end_date: 2022-08-10
location: Haifa, Israel
name: 'CAV: Computer Aided Verification'
start_date: 2022-08-07
date_created: 2022-08-28T22:02:02Z
date_published: 2022-08-07T00:00:00Z
date_updated: 2025-07-14T09:09:58Z
day: '07'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-13185-1_4
ec_funded: 1
external_id:
isi:
- '000870304500004'
file:
- access_level: open_access
checksum: 24e0f810ec52735a90ade95198bc641d
content_type: application/pdf
creator: alisjak
date_created: 2022-08-29T09:17:01Z
date_updated: 2022-08-29T09:17:01Z
file_id: '12003'
file_name: 2022_LNCS_Chatterjee.pdf
file_size: 505094
relation: main_file
success: 1
file_date_updated: 2022-08-29T09:17:01Z
has_accepted_license: '1'
intvolume: ' 13371'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 55-78
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Proceedings of the 34th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031131844'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Sound and complete certificates for auantitative termination analysis of probabilistic
programs
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13371
year: '2022'
...
---
_id: '12101'
abstract:
- lang: eng
text: 'Spatial games form a widely-studied class of games from biology and physics
modeling the evolution of social behavior. Formally, such a game is defined by
a square (d by d) payoff matrix M and an undirected graph G. Each vertex of G
represents an individual, that initially follows some strategy i ∈ {1,2,…,d}.
In each round of the game, every individual plays the matrix game with each of
its neighbors: An individual following strategy i meeting a neighbor following
strategy j receives a payoff equal to the entry (i,j) of M. Then, each individual
updates its strategy to its neighbors'' strategy with the highest sum of payoffs,
and the next round starts. The basic computational problems consist of reachability
between configurations and the average frequency of a strategy. For general spatial
games and graphs, these problems are in PSPACE. In this paper, we examine restricted
setting: the game is a prisoner’s dilemma; and G is a subgraph of grid. We prove
that basic computational problems for spatial games with prisoner’s dilemma on
a subgraph of a grid are PSPACE-hard.'
acknowledgement: "Krishnendu Chatterjee: The research was partially supported by the
ERC CoG 863818\r\n(ForM-SMArt).\r\nIsmaël Jecker: The research was partially supported
by the ERC grant 950398 (INFSYS).\r\nJakub Svoboda: The research was partially supported
by the ERC CoG 863818 (ForM-SMArt)"
article_number: 11:1-11:14
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Ismael R
full_name: Jecker, Ismael R
id: 85D7C63E-7D5D-11E9-9C0F-98C4E5697425
last_name: Jecker
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
citation:
ama: 'Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. Complexity of spatial
games. In: 42nd IARCS Annual Conference on Foundations of Software Technology
and Theoretical Computer Science. Vol 250. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2022. doi:10.4230/LIPIcs.FSTTCS.2022.11'
apa: 'Chatterjee, K., Ibsen-Jensen, R., Jecker, I. R., & Svoboda, J. (2022).
Complexity of spatial games. In 42nd IARCS Annual Conference on Foundations
of Software Technology and Theoretical Computer Science (Vol. 250). Madras,
India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11'
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Ismael R Jecker, and Jakub
Svoboda. “Complexity of Spatial Games.” In 42nd IARCS Annual Conference on
Foundations of Software Technology and Theoretical Computer Science, Vol.
250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11.
ieee: K. Chatterjee, R. Ibsen-Jensen, I. R. Jecker, and J. Svoboda, “Complexity
of spatial games,” in 42nd IARCS Annual Conference on Foundations of Software
Technology and Theoretical Computer Science, Madras, India, 2022, vol. 250.
ista: 'Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. 2022. Complexity of spatial
games. 42nd IARCS Annual Conference on Foundations of Software Technology and
Theoretical Computer Science. FSTTC: Foundations of Software Technology and Theoretical
Computer Science vol. 250, 11:1-11:14.'
mla: Chatterjee, Krishnendu, et al. “Complexity of Spatial Games.” 42nd IARCS
Annual Conference on Foundations of Software Technology and Theoretical Computer
Science, vol. 250, 11:1-11:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2022, doi:10.4230/LIPIcs.FSTTCS.2022.11.
short: K. Chatterjee, R. Ibsen-Jensen, I.R. Jecker, J. Svoboda, in:, 42nd IARCS
Annual Conference on Foundations of Software Technology and Theoretical Computer
Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
conference:
end_date: 2022-12-20
location: Madras, India
name: 'FSTTC: Foundations of Software Technology and Theoretical Computer Science'
start_date: 2022-12-18
date_created: 2023-01-01T23:00:50Z
date_published: 2022-12-14T00:00:00Z
date_updated: 2025-07-14T09:09:55Z
day: '14'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.FSTTCS.2022.11
ec_funded: 1
file:
- access_level: open_access
checksum: a21e3ba2421e2c4a06aa2cb6d530ede1
content_type: application/pdf
creator: dernst
date_created: 2023-01-20T10:19:19Z
date_updated: 2023-01-20T10:19:19Z
file_id: '12323'
file_name: 2022_LIPICs_Chatterjee.pdf
file_size: 657396
relation: main_file
success: 1
file_date_updated: 2023-01-20T10:19:19Z
has_accepted_license: '1'
intvolume: ' 250'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 42nd IARCS Annual Conference on Foundations of Software Technology and
Theoretical Computer Science
publication_identifier:
isbn:
- '9783959772617'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Complexity of spatial games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 250
year: '2022'
...
---
_id: '12102'
abstract:
- lang: eng
text: 'Given a Markov chain M = (V, v_0, δ), with state space V and a starting state
v_0, and a probability threshold ε, an ε-core is a subset C of states that is
left with probability at most ε. More formally, C ⊆ V is an ε-core, iff ℙ[reach
(V\C)] ≤ ε. Cores have been applied in a wide variety of verification problems
over Markov chains, Markov decision processes, and probabilistic programs, as
a means of discarding uninteresting and low-probability parts of a probabilistic
system and instead being able to focus on the states that are likely to be encountered
in a real-world run. In this work, we focus on the problem of computing a minimal
ε-core in a Markov chain. Our contributions include both negative and positive
results: (i) We show that the decision problem on the existence of an ε-core of
a given size is NP-complete. This solves an open problem posed in [Jan Kretínský
and Tobias Meggendorfer, 2020]. We additionally show that the problem remains
NP-complete even when limited to acyclic Markov chains with bounded maximal vertex
degree; (ii) We provide a polynomial time algorithm for computing a minimal ε-core
on Markov chains over control-flow graphs of structured programs. A straightforward
combination of our algorithm with standard branch prediction techniques allows
one to apply the idea of cores to find a subset of program lines that are left
with low probability and then focus any desired static analysis on this core subset.'
acknowledgement: "The research was partially supported by the Hong Kong Research Grants
Council ECS\r\nProject No. 26208122, ERC CoG 863818 (FoRM-SMArt), the European Union’s
Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie
Grant Agreement No. 665385, HKUST– Kaisa Joint Research Institute Project Grant
HKJRI3A-055 and HKUST Startup Grant R9272. Ali Ahmadi and Roodabeh Safavi were interns
at HKUST."
article_number: '29'
article_processing_charge: No
author:
- first_name: Ali
full_name: Ahmadi, Ali
last_name: Ahmadi
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Roodabeh
full_name: Safavi Hemami, Roodabeh
id: 72ed2640-8972-11ed-ae7b-f9c81ec75154
last_name: Safavi Hemami
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Ahmadi A, Chatterjee K, Goharshady AK, Meggendorfer T, Safavi Hemami R, Zikelic
D. Algorithms and hardness results for computing cores of Markov chains. In: 42nd
IARCS Annual Conference on Foundations of Software Technology and Theoretical
Computer Science. Vol 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2022. doi:10.4230/LIPIcs.FSTTCS.2022.29'
apa: 'Ahmadi, A., Chatterjee, K., Goharshady, A. K., Meggendorfer, T., Safavi Hemami,
R., & Zikelic, D. (2022). Algorithms and hardness results for computing cores
of Markov chains. In 42nd IARCS Annual Conference on Foundations of Software
Technology and Theoretical Computer Science (Vol. 250). Madras, India: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29'
chicago: Ahmadi, Ali, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer,
Roodabeh Safavi Hemami, and Dorde Zikelic. “Algorithms and Hardness Results for
Computing Cores of Markov Chains.” In 42nd IARCS Annual Conference on Foundations
of Software Technology and Theoretical Computer Science, Vol. 250. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29.
ieee: A. Ahmadi, K. Chatterjee, A. K. Goharshady, T. Meggendorfer, R. Safavi Hemami,
and D. Zikelic, “Algorithms and hardness results for computing cores of Markov
chains,” in 42nd IARCS Annual Conference on Foundations of Software Technology
and Theoretical Computer Science, Madras, India, 2022, vol. 250.
ista: 'Ahmadi A, Chatterjee K, Goharshady AK, Meggendorfer T, Safavi Hemami R, Zikelic
D. 2022. Algorithms and hardness results for computing cores of Markov chains.
42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical
Computer Science. FSTTC: Foundations of Software Technology and Theoretical Computer
Science vol. 250, 29.'
mla: Ahmadi, Ali, et al. “Algorithms and Hardness Results for Computing Cores of
Markov Chains.” 42nd IARCS Annual Conference on Foundations of Software Technology
and Theoretical Computer Science, vol. 250, 29, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2022, doi:10.4230/LIPIcs.FSTTCS.2022.29.
short: A. Ahmadi, K. Chatterjee, A.K. Goharshady, T. Meggendorfer, R. Safavi Hemami,
D. Zikelic, in:, 42nd IARCS Annual Conference on Foundations of Software Technology
and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2022.
conference:
end_date: 2022-12-20
location: Madras, India
name: 'FSTTC: Foundations of Software Technology and Theoretical Computer Science'
start_date: 2022-12-18
date_created: 2023-01-01T23:00:50Z
date_published: 2022-12-14T00:00:00Z
date_updated: 2025-07-14T09:09:55Z
day: '14'
ddc:
- '000'
department:
- _id: KrCh
- _id: GradSch
doi: 10.4230/LIPIcs.FSTTCS.2022.29
ec_funded: 1
file:
- access_level: open_access
checksum: 6660c802489013f034c9e8bd57f4d46e
content_type: application/pdf
creator: dernst
date_created: 2023-01-20T10:39:44Z
date_updated: 2023-01-20T10:39:44Z
file_id: '12324'
file_name: 2022_LIPICs_Ahmadi.pdf
file_size: 872534
relation: main_file
success: 1
file_date_updated: 2023-01-20T10:39:44Z
has_accepted_license: '1'
intvolume: ' 250'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: 42nd IARCS Annual Conference on Foundations of Software Technology and
Theoretical Computer Science
publication_identifier:
isbn:
- '9783959772617'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Algorithms and hardness results for computing cores of Markov chains
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 250
year: '2022'
...
---
_id: '12767'
abstract:
- lang: eng
text: "Several problems in planning and reactive synthesis can be reduced to the
analysis of two-player quantitative graph games. Optimization is one form of analysis.
We argue that in many cases it may be better to replace the optimization problem
with the satisficing problem, where instead of searching for optimal solutions,
the goal is to search for solutions that adhere to a given threshold bound.\r\nThis
work defines and investigates the satisficing problem on a two-player graph game
with the discounted-sum cost model. We show that while the satisficing problem
can be solved using numerical methods just like the optimization problem, this
approach does not render compelling benefits over optimization. When the discount
factor is, however, an integer, we present another approach to satisficing, which
is purely based on automata methods. We show that this approach is algorithmically
more performant – both theoretically and empirically – and demonstrates the broader
applicability of satisficing over optimization."
acknowledgement: We thank anonymous reviewers for valuable inputs. This work is supported
in part by NSF grant 2030859 to the CRA for the CIFellows Project, NSF grants IIS-1527668,
CCF-1704883, IIS-1830549, the ERC CoG 863818 (ForM-SMArt), and an award from the
Maryland Procurement Office.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Suguman
full_name: Bansal, Suguman
last_name: Bansal
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Moshe Y.
full_name: Vardi, Moshe Y.
last_name: Vardi
citation:
ama: 'Bansal S, Chatterjee K, Vardi MY. On satisficing in quantitative games. In:
27th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems. Vol 12651. Springer Nature; 2021:20-37. doi:10.1007/978-3-030-72016-2'
apa: 'Bansal, S., Chatterjee, K., & Vardi, M. Y. (2021). On satisficing in quantitative
games. In 27th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 12651, pp. 20–37). Luxembourg City, Luxembourg:
Springer Nature. https://doi.org/10.1007/978-3-030-72016-2'
chicago: Bansal, Suguman, Krishnendu Chatterjee, and Moshe Y. Vardi. “On Satisficing
in Quantitative Games.” In 27th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, 12651:20–37. Springer Nature,
2021. https://doi.org/10.1007/978-3-030-72016-2.
ieee: S. Bansal, K. Chatterjee, and M. Y. Vardi, “On satisficing in quantitative
games,” in 27th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Luxembourg City, Luxembourg, 2021, vol. 12651, pp.
20–37.
ista: 'Bansal S, Chatterjee K, Vardi MY. 2021. On satisficing in quantitative games.
27th 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. 12651, 20–37.'
mla: Bansal, Suguman, et al. “On Satisficing in Quantitative Games.” 27th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems,
vol. 12651, Springer Nature, 2021, pp. 20–37, doi:10.1007/978-3-030-72016-2.
short: S. Bansal, K. Chatterjee, M.Y. Vardi, in:, 27th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, Springer
Nature, 2021, pp. 20–37.
conference:
end_date: 2021-04-01
location: Luxembourg City, Luxembourg
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2021-03-27
date_created: 2023-03-26T22:01:09Z
date_published: 2021-03-21T00:00:00Z
date_updated: 2025-07-14T09:09:51Z
day: '21'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-030-72016-2
ec_funded: 1
external_id:
arxiv:
- '2101.02594'
file:
- access_level: open_access
checksum: b020b78b23587ce7610b1aafb4e63438
content_type: application/pdf
creator: dernst
date_created: 2023-03-28T11:00:33Z
date_updated: 2023-03-28T11:00:33Z
file_id: '12777'
file_name: 2021_LNCS_Bansal.pdf
file_size: 747418
relation: main_file
success: 1
file_date_updated: 2023-03-28T11:00:33Z
has_accepted_license: '1'
intvolume: ' 12651'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: 20-37
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 27th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030720155'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: On satisficing in quantitative games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 12651
year: '2021'
...
---
_id: '8793'
abstract:
- lang: eng
text: We study optimal election sequences for repeatedly selecting a (very) small
group of leaders among a set of participants (players) with publicly known unique
ids. In every time slot, every player has to select exactly one player that it
considers to be the current leader, oblivious to the selection of the other players,
but with the overarching goal of maximizing a given parameterized global (“social”)
payoff function in the limit. We consider a quite generic model, where the local
payoff achieved by a given player depends, weighted by some arbitrary but fixed
real parameter, on the number of different leaders chosen in a round, the number
of players that choose the given player as the leader, and whether the chosen
leader has changed w.r.t. the previous round or not. The social payoff can be
the maximum, average or minimum local payoff of the players. Possible applications
include quite diverse examples such as rotating coordinator-based distributed
algorithms and long-haul formation flying of social birds. Depending on the weights
and the particular social payoff, optimal sequences can be very different, from
simple round-robin where all players chose the same leader alternatingly every
time slot to very exotic patterns, where a small group of leaders (at most 2)
is elected in every time slot. Moreover, we study the question if and when a single
player would not benefit w.r.t. its local payoff when deviating from the given
optimal sequence, i.e., when our optimal sequences are Nash equilibria in the
restricted strategy space of oblivious strategies. As this is the case for many
parameterizations of our model, our results reveal that no punishment is needed
to make it rational for the players to optimize the social payoff.
acknowledgement: "We are grateful to Matthias Függer and Thomas Nowak for having raised
our interest in the problem studied in this paper.\r\nThis work has been supported
the Austrian Science Fund (FWF) projects S11405, S11407 (RiSE), and P28182 (ADynNet)."
article_processing_charge: No
article_type: original
author:
- first_name: Martin
full_name: Zeiner, Martin
last_name: Zeiner
- first_name: Ulrich
full_name: Schmid, Ulrich
last_name: Schmid
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Zeiner M, Schmid U, Chatterjee K. Optimal strategies for selecting coordinators.
Discrete Applied Mathematics. 2021;289(1):392-415. doi:10.1016/j.dam.2020.10.022
apa: Zeiner, M., Schmid, U., & Chatterjee, K. (2021). Optimal strategies for
selecting coordinators. Discrete Applied Mathematics. Elsevier. https://doi.org/10.1016/j.dam.2020.10.022
chicago: Zeiner, Martin, Ulrich Schmid, and Krishnendu Chatterjee. “Optimal Strategies
for Selecting Coordinators.” Discrete Applied Mathematics. Elsevier, 2021.
https://doi.org/10.1016/j.dam.2020.10.022.
ieee: M. Zeiner, U. Schmid, and K. Chatterjee, “Optimal strategies for selecting
coordinators,” Discrete Applied Mathematics, vol. 289, no. 1. Elsevier,
pp. 392–415, 2021.
ista: Zeiner M, Schmid U, Chatterjee K. 2021. Optimal strategies for selecting coordinators.
Discrete Applied Mathematics. 289(1), 392–415.
mla: Zeiner, Martin, et al. “Optimal Strategies for Selecting Coordinators.” Discrete
Applied Mathematics, vol. 289, no. 1, Elsevier, 2021, pp. 392–415, doi:10.1016/j.dam.2020.10.022.
short: M. Zeiner, U. Schmid, K. Chatterjee, Discrete Applied Mathematics 289 (2021)
392–415.
date_created: 2020-11-22T23:01:26Z
date_published: 2021-01-31T00:00:00Z
date_updated: 2023-08-04T11:12:41Z
day: '31'
ddc:
- '510'
department:
- _id: KrCh
doi: 10.1016/j.dam.2020.10.022
external_id:
isi:
- '000596823800035'
file:
- access_level: open_access
checksum: f1039ff5a2d6ca116720efdb84ee9d5e
content_type: application/pdf
creator: dernst
date_created: 2021-02-04T11:28:42Z
date_updated: 2021-02-04T11:28:42Z
file_id: '9089'
file_name: 2021_DiscreteApplMath_Zeiner.pdf
file_size: 652739
relation: main_file
success: 1
file_date_updated: 2021-02-04T11:28:42Z
has_accepted_license: '1'
intvolume: ' 289'
isi: 1
issue: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 392-415
project:
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: Discrete Applied Mathematics
publication_identifier:
issn:
- 0166218X
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Optimal strategies for selecting coordinators
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 289
year: '2021'
...
---
_id: '8934'
abstract:
- lang: eng
text: "In this thesis, we consider several of the most classical and fundamental
problems in static analysis and formal verification, including invariant generation,
reachability analysis, termination analysis of probabilistic programs, data-flow
analysis, quantitative analysis of Markov chains and Markov decision processes,
and the problem of data packing in cache management.\r\nWe use techniques from
parameterized complexity theory, polyhedral geometry, and real algebraic geometry
to significantly improve the state-of-the-art, in terms of both scalability and
completeness guarantees, for the mentioned problems. In some cases, our results
are the first theoretical improvements for the respective problems in two or three
decades."
acknowledgement: 'The research was partially supported by an IBM PhD fellowship, a
Facebook PhD fellowship, and DOC fellowship #24956 of the Austrian Academy of Sciences
(OeAW).'
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
citation:
ama: Goharshady AK. Parameterized and algebro-geometric advances in static program
analysis. 2021. doi:10.15479/AT:ISTA:8934
apa: Goharshady, A. K. (2021). Parameterized and algebro-geometric advances in
static program analysis. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:8934
chicago: Goharshady, Amir Kafshdar. “Parameterized and Algebro-Geometric Advances
in Static Program Analysis.” Institute of Science and Technology Austria, 2021.
https://doi.org/10.15479/AT:ISTA:8934.
ieee: A. K. Goharshady, “Parameterized and algebro-geometric advances in static
program analysis,” Institute of Science and Technology Austria, 2021.
ista: Goharshady AK. 2021. Parameterized and algebro-geometric advances in static
program analysis. Institute of Science and Technology Austria.
mla: Goharshady, Amir Kafshdar. Parameterized and Algebro-Geometric Advances
in Static Program Analysis. Institute of Science and Technology Austria, 2021,
doi:10.15479/AT:ISTA:8934.
short: A.K. Goharshady, Parameterized and Algebro-Geometric Advances in Static Program
Analysis, Institute of Science and Technology Austria, 2021.
date_created: 2020-12-10T12:17:07Z
date_published: 2021-01-01T00:00:00Z
date_updated: 2025-06-02T08:53:47Z
day: '01'
ddc:
- '005'
degree_awarded: PhD
department:
- _id: KrCh
- _id: GradSch
doi: 10.15479/AT:ISTA:8934
file:
- access_level: open_access
checksum: d1b9db3725aed34dadd81274aeb9426c
content_type: application/pdf
creator: akafshda
date_created: 2020-12-22T20:08:44Z
date_updated: 2021-12-23T23:30:04Z
embargo: 2021-12-22
file_id: '8969'
file_name: Thesis-pdfa.pdf
file_size: 5251507
relation: main_file
- access_level: closed
checksum: 1661df7b393e6866d2460eba3c905130
content_type: application/zip
creator: akafshda
date_created: 2020-12-22T20:08:50Z
date_updated: 2021-03-04T23:30:04Z
embargo_to: open_access
file_id: '8970'
file_name: source.zip
file_size: 10636756
relation: source_file
file_date_updated: 2021-12-23T23:30:04Z
has_accepted_license: '1'
language:
- iso: eng
license: https://creativecommons.org/publicdomain/zero/1.0/
month: '01'
oa: 1
oa_version: Published Version
page: '278'
project:
- _id: 267066CE-B435-11E9-9278-68D0E5697425
name: Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies
- _id: 266EEEC0-B435-11E9-9278-68D0E5697425
name: Quantitative Game-theoretic Analysis of Blockchain Applications and Smart
Contracts
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '1386'
relation: part_of_dissertation
status: public
- id: '1437'
relation: part_of_dissertation
status: public
- id: '639'
relation: part_of_dissertation
status: public
- id: '6918'
relation: part_of_dissertation
status: public
- id: '6490'
relation: part_of_dissertation
status: public
- id: '7158'
relation: part_of_dissertation
status: public
- id: '6009'
relation: part_of_dissertation
status: public
- id: '949'
relation: part_of_dissertation
status: public
- id: '311'
relation: part_of_dissertation
status: public
- id: '7810'
relation: part_of_dissertation
status: public
- id: '8089'
relation: part_of_dissertation
status: public
- id: '8728'
relation: part_of_dissertation
status: public
- id: '5977'
relation: part_of_dissertation
status: public
- id: '6056'
relation: part_of_dissertation
status: public
- id: '6175'
relation: part_of_dissertation
status: public
- id: '6340'
relation: part_of_dissertation
status: public
- id: '6378'
relation: part_of_dissertation
status: public
- id: '6380'
relation: part_of_dissertation
status: public
- id: '66'
relation: part_of_dissertation
status: public
- id: '6780'
relation: part_of_dissertation
status: public
- id: '7014'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
title: Parameterized and algebro-geometric advances in static program analysis
tmp:
image: /images/cc_0.png
legal_code_url: https://creativecommons.org/publicdomain/zero/1.0/legalcode
name: Creative Commons Public Domain Dedication (CC0 1.0)
short: CC0 (1.0)
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2021'
...
---
_id: '9293'
abstract:
- lang: eng
text: 'We consider planning problems for graphs, Markov Decision Processes (MDPs),
and games on graphs in an explicit state space. While graphs represent the most
basic planning model, MDPs represent interaction with nature and games on graphs
represent interaction with an adversarial environment. We consider two planning
problems with k different target sets: (a) the coverage problem asks whether there
is a plan for each individual target set; and (b) the sequential target reachability
problem asks whether the targets can be reached in a given sequence. For the coverage
problem, we present a linear-time algorithm for graphs, and quadratic conditional
lower bound for MDPs and games on graphs. For the sequential target problem, we
present a linear-time algorithm for graphs, a sub-quadratic algorithm for MDPs,
and a quadratic conditional lower bound for games on graphs. Our results with
conditional lower bounds, based on the boolean matrix multiplication (BMM) conjecture
and strong exponential time hypothesis (SETH), establish (i) model-separation
results showing that for the coverage problem MDPs and games on graphs are harder
than graphs, and for the sequential reachability problem games on graphs are harder
than MDPs and graphs; and (ii) problem-separation results showing that for MDPs
the coverage problem is harder than the sequential target problem.'
article_number: '103499'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Wolfgang
full_name: Dvořák, Wolfgang
last_name: Dvořák
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Alexander
full_name: Svozil, Alexander
last_name: Svozil
citation:
ama: Chatterjee K, Dvořák W, Henzinger MH, Svozil A. Algorithms and conditional
lower bounds for planning problems. Artificial Intelligence. 2021;297(8).
doi:10.1016/j.artint.2021.103499
apa: Chatterjee, K., Dvořák, W., Henzinger, M. H., & Svozil, A. (2021). Algorithms
and conditional lower bounds for planning problems. Artificial Intelligence.
Elsevier. https://doi.org/10.1016/j.artint.2021.103499
chicago: Chatterjee, Krishnendu, Wolfgang Dvořák, Monika H Henzinger, and Alexander
Svozil. “Algorithms and Conditional Lower Bounds for Planning Problems.” Artificial
Intelligence. Elsevier, 2021. https://doi.org/10.1016/j.artint.2021.103499.
ieee: K. Chatterjee, W. Dvořák, M. H. Henzinger, and A. Svozil, “Algorithms and
conditional lower bounds for planning problems,” Artificial Intelligence,
vol. 297, no. 8. Elsevier, 2021.
ista: Chatterjee K, Dvořák W, Henzinger MH, Svozil A. 2021. Algorithms and conditional
lower bounds for planning problems. Artificial Intelligence. 297(8), 103499.
mla: Chatterjee, Krishnendu, et al. “Algorithms and Conditional Lower Bounds for
Planning Problems.” Artificial Intelligence, vol. 297, no. 8, 103499, Elsevier,
2021, doi:10.1016/j.artint.2021.103499.
short: K. Chatterjee, W. Dvořák, M.H. Henzinger, A. Svozil, Artificial Intelligence
297 (2021).
date_created: 2021-03-28T22:01:40Z
date_published: 2021-03-16T00:00:00Z
date_updated: 2023-09-26T10:41:42Z
day: '16'
department:
- _id: KrCh
doi: 10.1016/j.artint.2021.103499
external_id:
arxiv:
- '1804.07031'
isi:
- '000657537500003'
intvolume: ' 297'
isi: 1
issue: '8'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1804.07031
month: '03'
oa: 1
oa_version: Preprint
publication: Artificial Intelligence
publication_identifier:
issn:
- 0004-3702
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '35'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Algorithms and conditional lower bounds for planning problems
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 297
year: '2021'
...
---
_id: '9296'
abstract:
- lang: eng
text: ' matching is compatible to two or more labeled point sets of size n with
labels {1,…,n} if its straight-line drawing on each of these point sets is
crossing-free. We study the maximum number of edges in a matching compatible to
two or more labeled point sets in general position in the plane. We show that
for any two labeled convex sets of n points there exists a compatible matching
with ⌊2n−−√⌋ edges. More generally, for any ℓ labeled point sets we construct
compatible matchings of size Ω(n1/ℓ) . As a corresponding upper bound, we use
probabilistic arguments to show that for any ℓ given sets of n points there
exists a labeling of each set such that the largest compatible matching has O(n2/(ℓ+1)) edges.
Finally, we show that Θ(logn) copies of any set of n points are necessary and
sufficient for the existence of a labeling such that any compatible matching consists
only of a single edge.'
acknowledgement: 'A.A. funded by the Marie Skłodowska-Curie grant agreement No. 754411.
Z.M. partially funded by Wittgenstein Prize, Austrian Science Fund (FWF), grant
no. Z 342-N31. I.P., D.P., and B.V. partially supported by FWF within the collaborative
DACH project Arrangements and Drawings as FWF project I 3340-N35. A.P. supported
by a Schrödinger fellowship of the FWF: J-3847-N35. J.T. partially supported by
ERC Start grant no. (279307: Graph Games), FWF grant no. P23499-N23 and S11407-N23
(RiSE).'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Oswin
full_name: Aichholzer, Oswin
last_name: Aichholzer
- first_name: Alan M
full_name: Arroyo Guevara, Alan M
id: 3207FDC6-F248-11E8-B48F-1D18A9856A87
last_name: Arroyo Guevara
orcid: 0000-0003-2401-8670
- first_name: Zuzana
full_name: Masárová, Zuzana
id: 45CFE238-F248-11E8-B48F-1D18A9856A87
last_name: Masárová
orcid: 0000-0002-6660-1322
- first_name: Irene
full_name: Parada, Irene
last_name: Parada
- first_name: Daniel
full_name: Perz, Daniel
last_name: Perz
- first_name: Alexander
full_name: Pilz, Alexander
last_name: Pilz
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Birgit
full_name: Vogtenhuber, Birgit
last_name: Vogtenhuber
citation:
ama: 'Aichholzer O, Arroyo Guevara AM, Masárová Z, et al. On compatible matchings.
In: 15th International Conference on Algorithms and Computation. Vol 12635.
Springer Nature; 2021:221-233. doi:10.1007/978-3-030-68211-8_18'
apa: 'Aichholzer, O., Arroyo Guevara, A. M., Masárová, Z., Parada, I., Perz, D.,
Pilz, A., … Vogtenhuber, B. (2021). On compatible matchings. In 15th International
Conference on Algorithms and Computation (Vol. 12635, pp. 221–233). Yangon,
Myanmar: Springer Nature. https://doi.org/10.1007/978-3-030-68211-8_18'
chicago: Aichholzer, Oswin, Alan M Arroyo Guevara, Zuzana Masárová, Irene Parada,
Daniel Perz, Alexander Pilz, Josef Tkadlec, and Birgit Vogtenhuber. “On Compatible
Matchings.” In 15th International Conference on Algorithms and Computation,
12635:221–33. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-68211-8_18.
ieee: O. Aichholzer et al., “On compatible matchings,” in 15th International
Conference on Algorithms and Computation, Yangon, Myanmar, 2021, vol. 12635,
pp. 221–233.
ista: 'Aichholzer O, Arroyo Guevara AM, Masárová Z, Parada I, Perz D, Pilz A, Tkadlec
J, Vogtenhuber B. 2021. On compatible matchings. 15th International Conference
on Algorithms and Computation. WALCOM: Algorithms and Computation, LNCS, vol.
12635, 221–233.'
mla: Aichholzer, Oswin, et al. “On Compatible Matchings.” 15th International
Conference on Algorithms and Computation, vol. 12635, Springer Nature, 2021,
pp. 221–33, doi:10.1007/978-3-030-68211-8_18.
short: O. Aichholzer, A.M. Arroyo Guevara, Z. Masárová, I. Parada, D. Perz, A. Pilz,
J. Tkadlec, B. Vogtenhuber, in:, 15th International Conference on Algorithms and
Computation, Springer Nature, 2021, pp. 221–233.
conference:
end_date: 2021-03-02
location: Yangon, Myanmar
name: 'WALCOM: Algorithms and Computation'
start_date: 2021-02-28
date_created: 2021-03-28T22:01:41Z
date_published: 2021-02-16T00:00:00Z
date_updated: 2023-02-21T16:33:44Z
day: '16'
department:
- _id: UlWa
- _id: HeEd
- _id: KrCh
doi: 10.1007/978-3-030-68211-8_18
ec_funded: 1
external_id:
arxiv:
- '2101.03928'
intvolume: ' 12635'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2101.03928
month: '02'
oa: 1
oa_version: Preprint
page: 221-233
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
- _id: 268116B8-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z00342
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: 15th International Conference on Algorithms and Computation
publication_identifier:
eissn:
- '16113349'
isbn:
- '9783030682101'
issn:
- '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '11938'
relation: later_version
status: public
scopus_import: '1'
status: public
title: On compatible matchings
type: conference
user_id: D865714E-FA4E-11E9-B85B-F5C5E5697425
volume: 12635
year: '2021'
...
---
_id: '9381'
abstract:
- lang: eng
text: 'A game of rock-paper-scissors is an interesting example of an interaction
where none of the pure strategies strictly dominates all others, leading to a
cyclic pattern. In this work, we consider an unstable version of rock-paper-scissors
dynamics and allow individuals to make behavioural mistakes during the strategy
execution. We show that such an assumption can break a cyclic relationship leading
to a stable equilibrium emerging with only one strategy surviving. We consider
two cases: completely random mistakes when individuals have no bias towards any
strategy and a general form of mistakes. Then, we determine conditions for a strategy
to dominate all other strategies. However, given that individuals who adopt a
dominating strategy are still prone to behavioural mistakes in the observed behaviour,
we may still observe extinct strategies. That is, behavioural mistakes in strategy
execution stabilise evolutionary dynamics leading to an evolutionary stable and,
potentially, mixed co-existence equilibrium.'
acknowledgement: Authors would like to thank Christian Hilbe and Martin Nowak for
their inspiring and very helpful feedback on the manuscript.
article_number: e1008523
article_processing_charge: No
article_type: original
author:
- first_name: Maria
full_name: Kleshnina, Maria
id: 4E21749C-F248-11E8-B48F-1D18A9856A87
last_name: Kleshnina
- first_name: Sabrina S.
full_name: Streipert, Sabrina S.
last_name: Streipert
- first_name: Jerzy A.
full_name: Filar, Jerzy A.
last_name: Filar
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Kleshnina M, Streipert SS, Filar JA, Chatterjee K. Mistakes can stabilise the
dynamics of rock-paper-scissors games. PLoS Computational Biology. 2021;17(4).
doi:10.1371/journal.pcbi.1008523
apa: Kleshnina, M., Streipert, S. S., Filar, J. A., & Chatterjee, K. (2021).
Mistakes can stabilise the dynamics of rock-paper-scissors games. PLoS Computational
Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1008523
chicago: Kleshnina, Maria, Sabrina S. Streipert, Jerzy A. Filar, and Krishnendu
Chatterjee. “Mistakes Can Stabilise the Dynamics of Rock-Paper-Scissors Games.”
PLoS Computational Biology. Public Library of Science, 2021. https://doi.org/10.1371/journal.pcbi.1008523.
ieee: M. Kleshnina, S. S. Streipert, J. A. Filar, and K. Chatterjee, “Mistakes can
stabilise the dynamics of rock-paper-scissors games,” PLoS Computational Biology,
vol. 17, no. 4. Public Library of Science, 2021.
ista: Kleshnina M, Streipert SS, Filar JA, Chatterjee K. 2021. Mistakes can stabilise
the dynamics of rock-paper-scissors games. PLoS Computational Biology. 17(4),
e1008523.
mla: Kleshnina, Maria, et al. “Mistakes Can Stabilise the Dynamics of Rock-Paper-Scissors
Games.” PLoS Computational Biology, vol. 17, no. 4, e1008523, Public Library
of Science, 2021, doi:10.1371/journal.pcbi.1008523.
short: M. Kleshnina, S.S. Streipert, J.A. Filar, K. Chatterjee, PLoS Computational
Biology 17 (2021).
date_created: 2021-05-09T22:01:38Z
date_published: 2021-04-01T00:00:00Z
date_updated: 2025-07-14T09:10:04Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1371/journal.pcbi.1008523
ec_funded: 1
external_id:
isi:
- '000639711200001'
file:
- access_level: open_access
checksum: a94ebe0c4116f5047eaa6029e54d2dac
content_type: application/pdf
creator: kschuh
date_created: 2021-05-11T13:50:06Z
date_updated: 2021-05-11T13:50:06Z
file_id: '9385'
file_name: 2021_pcbi_Kleshnina.pdf
file_size: 1323820
relation: main_file
success: 1
file_date_updated: 2021-05-11T13:50:06Z
has_accepted_license: '1'
intvolume: ' 17'
isi: 1
issue: '4'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: PLoS Computational Biology
publication_identifier:
eissn:
- '15537358'
issn:
- 1553734X
publication_status: published
publisher: Public Library of Science
quality_controlled: '1'
scopus_import: '1'
status: public
title: Mistakes can stabilise the dynamics of rock-paper-scissors games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 17
year: '2021'
...
---
_id: '9393'
abstract:
- lang: eng
text: "We consider the core algorithmic problems related to verification of systems
with respect to three classical quantitative properties, namely, the mean-payoff,
the ratio, and the minimum initial credit for energy property. The algorithmic
problem given a graph and a quantitative property asks to compute the optimal
value (the infimum value over all traces) from every node of the graph. We consider
graphs with bounded treewidth—a class that contains the control flow graphs of
most programs. Let n denote the number of nodes of a graph, m the number of edges
(for bounded treewidth \U0001D45A=\U0001D442(\U0001D45B)) and W the largest absolute
value of the weights. Our main theoretical results are as follows. First, for
the minimum initial credit problem we show that (1) for general graphs the problem
can be solved in \U0001D442(\U0001D45B2⋅\U0001D45A) time and the associated decision
problem in \U0001D442(\U0001D45B⋅\U0001D45A) time, improving the previous known
\U0001D442(\U0001D45B3⋅\U0001D45A⋅log(\U0001D45B⋅\U0001D44A)) and \U0001D442(\U0001D45B2⋅\U0001D45A)
bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm
that requires \U0001D442(\U0001D45B⋅log\U0001D45B) time. Second, for bounded treewidth
graphs we present an algorithm that approximates the mean-payoff value within
a factor of 1+\U0001D716 in time \U0001D442(\U0001D45B⋅log(\U0001D45B/\U0001D716))
as compared to the classical exact algorithms on general graphs that require quadratic
time. Third, for the ratio property we present an algorithm that for bounded treewidth
graphs works in time \U0001D442(\U0001D45B⋅log(|\U0001D44E⋅\U0001D44F|))=\U0001D442(\U0001D45B⋅log(\U0001D45B⋅\U0001D44A)),
when the output is \U0001D44E\U0001D44F, as compared to the previously best known
algorithm on general graphs with running time \U0001D442(\U0001D45B2⋅log(\U0001D45B⋅\U0001D44A)).
We have implemented some of our algorithms and show that they present a significant
speedup on standard benchmarks."
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant
(279307: Graph Games), and Microsoft faculty fellows award.'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative
verification in bounded treewidth graphs. Formal Methods in System Design.
2021;57:401-428. doi:10.1007/s10703-021-00373-5
apa: Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2021). Faster algorithms
for quantitative verification in bounded treewidth graphs. Formal Methods in
System Design. Springer. https://doi.org/10.1007/s10703-021-00373-5
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
“Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.”
Formal Methods in System Design. Springer, 2021. https://doi.org/10.1007/s10703-021-00373-5.
ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for
quantitative verification in bounded treewidth graphs,” Formal Methods in System
Design, vol. 57. Springer, pp. 401–428, 2021.
ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for
quantitative verification in bounded treewidth graphs. Formal Methods in System
Design. 57, 401–428.
mla: Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification
in Bounded Treewidth Graphs.” Formal Methods in System Design, vol. 57,
Springer, 2021, pp. 401–28, doi:10.1007/s10703-021-00373-5.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System
Design 57 (2021) 401–428.
date_created: 2021-05-16T22:01:47Z
date_published: 2021-09-01T00:00:00Z
date_updated: 2023-10-10T11:13:20Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/s10703-021-00373-5
ec_funded: 1
external_id:
arxiv:
- '1504.07384'
isi:
- '000645490300001'
intvolume: ' 57'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.07384
month: '09'
oa: 1
oa_version: Preprint
page: 401-428
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Formal Methods in System Design
publication_identifier:
eissn:
- 1572-8102
issn:
- 0925-9856
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for quantitative verification in bounded treewidth graphs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 57
year: '2021'
...
---
_id: '9402'
abstract:
- lang: eng
text: Direct and indirect reciprocity are key mechanisms for the evolution of cooperation.
Direct reciprocity means that individuals use their own experience to decide whether
to cooperate with another person. Indirect reciprocity means that they also consider
the experiences of others. Although these two mechanisms are intertwined, they
are typically studied in isolation. Here, we introduce a mathematical framework
that allows us to explore both kinds of reciprocity simultaneously. We show that
the well-known ‘generous tit-for-tat’ strategy of direct reciprocity has a natural
analogue in indirect reciprocity, which we call ‘generous scoring’. Using an equilibrium
analysis, we characterize under which conditions either of the two strategies
can maintain cooperation. With simulations, we additionally explore which kind
of reciprocity evolves when members of a population engage in social learning
to adapt to their environment. Our results draw unexpected connections between
direct and indirect reciprocity while highlighting important differences regarding
their evolvability.
acknowledgement: 'This work was supported by the European Research Council CoG 863818
(ForM-SMArt) (to K.C.), the European Research Council Start Grant 279307: Graph
Games (to K.C.), and the European Research Council Starting Grant 850529: E-DIRECT
(to C.H.). The funders had no role in study design, data collection and analysis,
decision to publish or preparation of the manuscript.'
article_processing_charge: No
article_type: original
author:
- first_name: Laura
full_name: Schmid, Laura
id: 38B437DE-F248-11E8-B48F-1D18A9856A87
last_name: Schmid
orcid: 0000-0002-6978-7329
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Martin A.
full_name: Nowak, Martin A.
last_name: Nowak
citation:
ama: Schmid L, Chatterjee K, Hilbe C, Nowak MA. A unified framework of direct and
indirect reciprocity. Nature Human Behaviour. 2021;5(10):1292–1302. doi:10.1038/s41562-021-01114-8
apa: Schmid, L., Chatterjee, K., Hilbe, C., & Nowak, M. A. (2021). A unified
framework of direct and indirect reciprocity. Nature Human Behaviour. Springer
Nature. https://doi.org/10.1038/s41562-021-01114-8
chicago: Schmid, Laura, Krishnendu Chatterjee, Christian Hilbe, and Martin A. Nowak.
“A Unified Framework of Direct and Indirect Reciprocity.” Nature Human Behaviour.
Springer Nature, 2021. https://doi.org/10.1038/s41562-021-01114-8.
ieee: L. Schmid, K. Chatterjee, C. Hilbe, and M. A. Nowak, “A unified framework
of direct and indirect reciprocity,” Nature Human Behaviour, vol. 5, no.
10. Springer Nature, pp. 1292–1302, 2021.
ista: Schmid L, Chatterjee K, Hilbe C, Nowak MA. 2021. A unified framework of direct
and indirect reciprocity. Nature Human Behaviour. 5(10), 1292–1302.
mla: Schmid, Laura, et al. “A Unified Framework of Direct and Indirect Reciprocity.”
Nature Human Behaviour, vol. 5, no. 10, Springer Nature, 2021, pp. 1292–1302,
doi:10.1038/s41562-021-01114-8.
short: L. Schmid, K. Chatterjee, C. Hilbe, M.A. Nowak, Nature Human Behaviour 5
(2021) 1292–1302.
date_created: 2021-05-18T16:56:57Z
date_published: 2021-05-13T00:00:00Z
date_updated: 2025-07-14T09:10:09Z
day: '13'
ddc:
- '000'
department:
- _id: KrCh
- _id: GradSch
doi: 10.1038/s41562-021-01114-8
ec_funded: 1
external_id:
isi:
- '000650304000002'
pmid:
- '33986519'
file:
- access_level: open_access
checksum: 34f55e173f90dc1dab731063458ac780
content_type: application/pdf
creator: dernst
date_created: 2023-11-07T08:27:23Z
date_updated: 2023-11-07T08:27:23Z
file_id: '14496'
file_name: 2021_NatureHumanBehaviour_Schmid_accepted.pdf
file_size: 5232761
relation: main_file
success: 1
file_date_updated: 2023-11-07T08:27:23Z
has_accepted_license: '1'
intvolume: ' 5'
isi: 1
issue: '10'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
page: 1292–1302
pmid: 1
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Nature Human Behaviour
publication_identifier:
eissn:
- 2397-3374
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
link:
- description: News on IST Homepage
relation: press_release
url: https://ist.ac.at/en/news/the-emergence-of-cooperation/
record:
- id: '10293'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: A unified framework of direct and indirect reciprocity
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5
year: '2021'
...
---
_id: '9403'
abstract:
- lang: eng
text: Optimal decision making requires individuals to know their available options
and to anticipate correctly what consequences these options have. In many social
interactions, however, we refrain from gathering all relevant information, even
if this information would help us make better decisions and is costless to obtain.
This chapter examines several examples of “deliberate ignorance.” Two simple models
are proposed to illustrate how ignorance can evolve among self-interested and
payoff - maximizing individuals, and open problems are highlighted that lie ahead
for future research to explore.
article_processing_charge: No
author:
- first_name: Laura
full_name: Schmid, Laura
id: 38B437DE-F248-11E8-B48F-1D18A9856A87
last_name: Schmid
orcid: 0000-0002-6978-7329
- first_name: Christian
full_name: Hilbe, Christian
last_name: Hilbe
citation:
ama: 'Schmid L, Hilbe C. The evolution of strategic ignorance in strategic interaction.
In: Hertwig R, Engel C, eds. Deliberate Ignorance: Choosing Not To Know.
Vol 29. Strüngmann Forum Reports. MIT Press; 2021:139-152.'
apa: 'Schmid, L., & Hilbe, C. (2021). The evolution of strategic ignorance in
strategic interaction. In R. Hertwig & C. Engel (Eds.), Deliberate Ignorance:
Choosing Not To Know (Vol. 29, pp. 139–152). MIT Press.'
chicago: 'Schmid, Laura, and Christian Hilbe. “The Evolution of Strategic Ignorance
in Strategic Interaction.” In Deliberate Ignorance: Choosing Not To Know,
edited by Ralph Hertwig and Christoph Engel, 29:139–52. Strüngmann Forum Reports.
MIT Press, 2021.'
ieee: 'L. Schmid and C. Hilbe, “The evolution of strategic ignorance in strategic
interaction,” in Deliberate Ignorance: Choosing Not To Know, vol. 29, R.
Hertwig and C. Engel, Eds. MIT Press, 2021, pp. 139–152.'
ista: 'Schmid L, Hilbe C. 2021.The evolution of strategic ignorance in strategic
interaction. In: Deliberate Ignorance: Choosing Not To Know. vol. 29, 139–152.'
mla: 'Schmid, Laura, and Christian Hilbe. “The Evolution of Strategic Ignorance
in Strategic Interaction.” Deliberate Ignorance: Choosing Not To Know,
edited by Ralph Hertwig and Christoph Engel, vol. 29, MIT Press, 2021, pp. 139–52.'
short: 'L. Schmid, C. Hilbe, in:, R. Hertwig, C. Engel (Eds.), Deliberate Ignorance:
Choosing Not To Know, MIT Press, 2021, pp. 139–152.'
date_created: 2021-05-19T12:25:42Z
date_published: 2021-03-01T00:00:00Z
date_updated: 2023-02-23T13:57:04Z
day: '01'
department:
- _id: GradSch
- _id: KrCh
editor:
- first_name: Ralph
full_name: Hertwig, Ralph
last_name: Hertwig
- first_name: Christoph
full_name: Engel, Christoph
last_name: Engel
intvolume: ' 29'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://esforum.de/publications/PDFs/sfr29/SFR29_09_Hilbe%20and%20Schmid.pdf
month: '03'
oa: 1
oa_version: Published Version
page: 139-152
publication: 'Deliberate Ignorance: Choosing Not To Know'
publication_identifier:
isbn:
- 978-0-262-04559-9
publisher: MIT Press
quality_controlled: '1'
series_title: Strüngmann Forum Reports
status: public
title: The evolution of strategic ignorance in strategic interaction
type: book_chapter
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 29
year: '2021'
...
---
_id: '10002'
abstract:
- lang: eng
text: 'We present a faster symbolic algorithm for the following central problem
in probabilistic verification: Compute the maximal end-component (MEC) decomposition
of Markov decision processes (MDPs). This problem generalizes the SCC decomposition
problem of graphs and closed recurrent sets of Markov chains. The model of symbolic
algorithms is widely used in formal verification and model-checking, where access
to the input model is restricted to only symbolic operations (e.g., basic set
operations and computation of one-step neighborhood). For an input MDP with n vertices
and m edges, the classical symbolic algorithm from the 1990s for the MEC decomposition
requires O(n2) symbolic operations and O(1) symbolic space. The only other
symbolic algorithm for the MEC decomposition requires O(nm−−√) symbolic operations
and O(m−−√) symbolic space. A main open question is whether the worst-case O(n2) bound
for symbolic operations can be beaten. We present a symbolic algorithm that requires O˜(n1.5) symbolic
operations and O˜(n−−√) symbolic space. Moreover, the parametrization of our
algorithm provides a trade-off between symbolic operations and symbolic space:
for all 0<ϵ≤1/2 the symbolic algorithm requires O˜(n2−ϵ) symbolic operations
and O˜(nϵ) symbolic space ( O˜ hides poly-logarithmic factors). Using our techniques
we present faster algorithms for computing the almost-sure winning regions of ω
-regular objectives for MDPs. We consider the canonical parity objectives for ω
-regular objectives, and for parity objectives with d -priorities we present
an algorithm that computes the almost-sure winning region with O˜(n2−ϵ) symbolic
operations and O˜(nϵ) symbolic space, for all 0<ϵ≤1/2 .'
acknowledgement: The authors are grateful to the anonymous referees for their valuable
comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF)
through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF)
NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For
M. H. the research leading to these results has received funding from the European
Research Council under the European Unions Seventh Framework Programme (FP/2007–2013)
/ ERC Grant Agreement no. 340506.
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Wolfgang
full_name: Dvorak, Wolfgang
last_name: Dvorak
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Alexander
full_name: Svozil, Alexander
last_name: Svozil
citation:
ama: 'Chatterjee K, Dvorak W, Henzinger MH, Svozil A. Symbolic time and space tradeoffs
for probabilistic verification. In: Proceedings of the 36th Annual ACM/IEEE
Symposium on Logic in Computer Science. Institute of Electrical and Electronics
Engineers; 2021:1-13. doi:10.1109/LICS52264.2021.9470739'
apa: 'Chatterjee, K., Dvorak, W., Henzinger, M. H., & Svozil, A. (2021). Symbolic
time and space tradeoffs for probabilistic verification. In Proceedings of
the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 1–13).
Rome, Italy: Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/LICS52264.2021.9470739'
chicago: Chatterjee, Krishnendu, Wolfgang Dvorak, Monika H Henzinger, and Alexander
Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science,
1–13. Institute of Electrical and Electronics Engineers, 2021. https://doi.org/10.1109/LICS52264.2021.9470739.
ieee: K. Chatterjee, W. Dvorak, M. H. Henzinger, and A. Svozil, “Symbolic time and
space tradeoffs for probabilistic verification,” in Proceedings of the 36th
Annual ACM/IEEE Symposium on Logic in Computer Science, Rome, Italy, 2021,
pp. 1–13.
ista: 'Chatterjee K, Dvorak W, Henzinger MH, Svozil A. 2021. Symbolic time and space
tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE
Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science,
1–13.'
mla: Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic
Verification.” Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in
Computer Science, Institute of Electrical and Electronics Engineers, 2021,
pp. 1–13, doi:10.1109/LICS52264.2021.9470739.
short: K. Chatterjee, W. Dvorak, M.H. Henzinger, A. Svozil, in:, Proceedings of
the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of
Electrical and Electronics Engineers, 2021, pp. 1–13.
conference:
end_date: 2021-07-02
location: Rome, Italy
name: 'LICS: Symposium on Logic in Computer Science'
start_date: 2021-06-29
date_created: 2021-09-12T22:01:24Z
date_published: 2021-07-07T00:00:00Z
date_updated: 2025-07-14T09:10:07Z
day: '07'
department:
- _id: KrCh
doi: 10.1109/LICS52264.2021.9470739
ec_funded: 1
external_id:
arxiv:
- '2104.07466'
isi:
- '000947350400089'
isi: 1
keyword:
- Computer science
- Computational modeling
- Markov processes
- Probabilistic logic
- Formal verification
- Game Theory
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2104.07466
month: '07'
oa: 1
oa_version: Preprint
page: 1-13
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer
Science
publication_identifier:
eisbn:
- 978-1-6654-4895-6
isbn:
- 978-1-6654-4896-3
issn:
- 1043-6871
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic time and space tradeoffs for probabilistic verification
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '10004'
abstract:
- lang: eng
text: 'Markov chains are the de facto finite-state model for stochastic dynamical
systems, and Markov decision processes (MDPs) extend Markov chains by incorporating
non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization
criterion is the maximal expected total reward where the MDP stops after T steps,
which can be computed by a simple dynamic programming algorithm. We consider a
natural generalization of the problem where the stopping times can be chosen according
to a probability distribution, such that the expected stopping time is T, to optimize
the expected total reward. Quite surprisingly we establish inter-reducibility
of the expected stopping-time problem for Markov chains with the Positivity problem
(which is related to the well-known Skolem problem), for which establishing either
decidability or undecidability would be a major breakthrough. Given the hardness
of the exact problem, we consider the approximate version of the problem: we show
that it can be solved in exponential time for Markov chains and in exponential
space for MDPs.'
acknowledgement: We are grateful to the anonymous reviewers of LICS 2021 and of a
previous version of this paper for insightful comments that helped improving the
presentation. This research was partially supported by the grant ERC CoG 863818
(ForM-SMArt).
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
citation:
ama: 'Chatterjee K, Doyen L. Stochastic processes with expected stopping time. In:
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science.
Institute of Electrical and Electronics Engineers; 2021:1-13. doi:10.1109/LICS52264.2021.9470595'
apa: 'Chatterjee, K., & Doyen, L. (2021). Stochastic processes with expected
stopping time. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic
in Computer Science (pp. 1–13). Rome, Italy: Institute of Electrical and Electronics
Engineers. https://doi.org/10.1109/LICS52264.2021.9470595'
chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected
Stopping Time.” In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic
in Computer Science, 1–13. Institute of Electrical and Electronics Engineers,
2021. https://doi.org/10.1109/LICS52264.2021.9470595.
ieee: K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,”
in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science,
Rome, Italy, 2021, pp. 1–13.
ista: 'Chatterjee K, Doyen L. 2021. Stochastic processes with expected stopping
time. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science.
LICS: Symposium on Logic in Computer Science, 1–13.'
mla: Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected
Stopping Time.” Proceedings of the 36th Annual ACM/IEEE Symposium on Logic
in Computer Science, Institute of Electrical and Electronics Engineers, 2021,
pp. 1–13, doi:10.1109/LICS52264.2021.9470595.
short: K. Chatterjee, L. Doyen, in:, Proceedings of the 36th Annual ACM/IEEE Symposium
on Logic in Computer Science, Institute of Electrical and Electronics Engineers,
2021, pp. 1–13.
conference:
end_date: 2021-07-02
location: Rome, Italy
name: 'LICS: Symposium on Logic in Computer Science'
start_date: 2021-06-29
date_created: 2021-09-12T22:01:25Z
date_published: 2021-07-07T00:00:00Z
date_updated: 2025-07-14T09:10:08Z
day: '07'
department:
- _id: KrCh
doi: 10.1109/LICS52264.2021.9470595
ec_funded: 1
external_id:
arxiv:
- '2104.07278'
isi:
- '000947350400036'
isi: 1
keyword:
- Computer science
- Heuristic algorithms
- Memory management
- Automata
- Markov processes
- Probability distribution
- Complexity theory
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2104.07278
month: '07'
oa: 1
oa_version: Preprint
page: 1-13
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer
Science
publication_identifier:
eisbn:
- 978-1-6654-4895-6
isbn:
- 978-1-6654-4896-3
issn:
- 1043-6871
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Stochastic processes with expected stopping time
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '10052'
abstract:
- lang: eng
text: "A deterministic finite automaton (DFA) \U0001D49C is composite if its language
L(\U0001D49C) can be decomposed into an intersection ⋂_{i = 1}^k L(\U0001D49C_i)
of languages of smaller DFAs. Otherwise, \U0001D49C is prime. This notion of primality
was introduced by Kupferman and Mosheiff in 2013, and while they proved that we
can decide whether a DFA is composite, the precise complexity of this problem
is still open, with a doubly-exponential gap between the upper and lower bounds.
In this work, we focus on permutation DFAs, i.e., those for which the transition
monoid is a group. We provide an NP algorithm to decide whether a permutation
DFA is composite, and show that the difficulty of this problem comes from the
number of non-accepting states of the instance: we give a fixed-parameter tractable
algorithm with the number of rejecting states as the parameter. Moreover, we investigate
the class of commutative permutation DFAs. Their structural properties allow us
to decide compositionality in NL, and even in LOGSPACE if the alphabet size is
fixed. Despite this low complexity, we show that complex behaviors still arise
in this class: we provide a family of composite DFAs each requiring polynomially
many factors with respect to its size. We also consider the variant of the problem
that asks whether a DFA is k-factor composite, that is, decomposable into k smaller
DFAs, for some given integer k ∈ ℕ. We show that, for commutative permutation
DFAs, restricting the number of factors makes the decision computationally harder,
and yields a problem with tight bounds: it is NP-complete. Finally, we show that
in general, this problem is in PSPACE, and it is in LOGSPACE for DFAs with a singleton
alphabet."
acknowledgement: "Ismaël Jecker: Marie Skłodowska-Curie Grant Agreement No. 754411.
Nicolas Mazzocchi: BOSCO project PGC2018-102210-B-I00 (MCIU/AEI/FEDER, UE), BLOQUESCM
project S2018/TCS-4339, and MINECO grant RYC-2016-20281.\r\nPetra Wolf : DFG project
FE 560/9-1.\r\n"
alternative_title:
- LIPIcs
article_number: '18'
article_processing_charge: No
arxiv: 1
author:
- first_name: Ismael R
full_name: Jecker, Ismael R
id: 85D7C63E-7D5D-11E9-9C0F-98C4E5697425
last_name: Jecker
- first_name: Nicolas
full_name: Mazzocchi, Nicolas
last_name: Mazzocchi
- first_name: Petra
full_name: Wolf, Petra
last_name: Wolf
citation:
ama: 'Jecker IR, Mazzocchi N, Wolf P. Decomposing permutation automata. In: 32nd
International Conference on Concurrency Theory. Vol 203. Schloss Dagstuhl
- Leibniz Zentrum für Informatik; 2021. doi:10.4230/LIPIcs.CONCUR.2021.18'
apa: 'Jecker, I. R., Mazzocchi, N., & Wolf, P. (2021). Decomposing permutation
automata. In 32nd International Conference on Concurrency Theory (Vol.
203). Paris, France: Schloss Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2021.18'
chicago: Jecker, Ismael R, Nicolas Mazzocchi, and Petra Wolf. “Decomposing Permutation
Automata.” In 32nd International Conference on Concurrency Theory, Vol.
203. Schloss Dagstuhl - Leibniz Zentrum für Informatik, 2021. https://doi.org/10.4230/LIPIcs.CONCUR.2021.18.
ieee: I. R. Jecker, N. Mazzocchi, and P. Wolf, “Decomposing permutation automata,”
in 32nd International Conference on Concurrency Theory, Paris, France,
2021, vol. 203.
ista: 'Jecker IR, Mazzocchi N, Wolf P. 2021. Decomposing permutation automata. 32nd
International Conference on Concurrency Theory. CONCUR: Conference on Concurrency
Theory, LIPIcs, vol. 203, 18.'
mla: Jecker, Ismael R., et al. “Decomposing Permutation Automata.” 32nd International
Conference on Concurrency Theory, vol. 203, 18, Schloss Dagstuhl - Leibniz
Zentrum für Informatik, 2021, doi:10.4230/LIPIcs.CONCUR.2021.18.
short: I.R. Jecker, N. Mazzocchi, P. Wolf, in:, 32nd International Conference on
Concurrency Theory, Schloss Dagstuhl - Leibniz Zentrum für Informatik, 2021.
conference:
end_date: 2021-08-27
location: Paris, France
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2021-08-23
date_created: 2021-09-27T14:33:14Z
date_published: 2021-08-13T00:00:00Z
date_updated: 2022-05-13T08:12:52Z
day: '13'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2021.18
ec_funded: 1
external_id:
arxiv:
- '2107.04683'
file:
- access_level: open_access
checksum: 4722c81be82265cf45e78adf9db91250
content_type: application/pdf
creator: cchlebak
date_created: 2021-10-01T11:10:53Z
date_updated: 2021-10-01T11:10:53Z
file_id: '10064'
file_name: 2021_CONCUR_Jecker.pdf
file_size: 1003552
relation: main_file
success: 1
file_date_updated: 2021-10-01T11:10:53Z
has_accepted_license: '1'
intvolume: ' 203'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: 32nd International Conference on Concurrency Theory
publication_identifier:
isbn:
- 978-3-9597-7203-7
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Decomposing permutation automata
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 203
year: '2021'
...