---
_id: '14539'
abstract:
- lang: eng
text: "Stochastic systems provide a formal framework for modelling and quantifying
uncertainty in systems and have been widely adopted in many application domains.
Formal\r\nverification and control of finite state stochastic systems, a subfield
of formal methods\r\nalso known as probabilistic model checking, is well studied.
In contrast, formal verification and control of infinite state stochastic systems
have received comparatively\r\nless attention. However, infinite state stochastic
systems commonly arise in practice.\r\nFor instance, probabilistic models that
contain continuous probability distributions such\r\nas normal or uniform, or
stochastic dynamical systems which are a classical model for\r\ncontrol under
uncertainty, both give rise to infinite state systems.\r\nThe goal of this thesis
is to contribute to laying theoretical and algorithmic foundations\r\nof fully
automated formal verification and control of infinite state stochastic systems,\r\nwith
a particular focus on systems that may be executed over a long or infinite time.\r\nWe
consider formal verification of infinite state stochastic systems in the setting
of\r\nstatic analysis of probabilistic programs and formal control in the setting
of controller\r\nsynthesis in stochastic dynamical systems. For both problems,
we present some of the\r\nfirst fully automated methods for probabilistic (a.k.a.
quantitative) reachability and\r\nsafety analysis applicable to infinite time
horizon systems. We also advance the state\r\nof the art of probability 1 (a.k.a.
qualitative) reachability analysis for both problems.\r\nFinally, for formal controller
synthesis in stochastic dynamical systems, we present a\r\nnovel framework for
learning neural network control policies in stochastic dynamical\r\nsystems with
formal guarantees on correctness with respect to quantitative reachability,\r\nsafety
or reach-avoid specifications.\r\n"
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: Zikelic D. Automated verification and control of infinite state stochastic
systems. 2023. doi:10.15479/14539
apa: Zikelic, D. (2023). Automated verification and control of infinite state
stochastic systems. Institute of Science and Technology Austria. https://doi.org/10.15479/14539
chicago: Zikelic, Dorde. “Automated Verification and Control of Infinite State Stochastic
Systems.” Institute of Science and Technology Austria, 2023. https://doi.org/10.15479/14539.
ieee: D. Zikelic, “Automated verification and control of infinite state stochastic
systems,” Institute of Science and Technology Austria, 2023.
ista: Zikelic D. 2023. Automated verification and control of infinite state stochastic
systems. Institute of Science and Technology Austria.
mla: Zikelic, Dorde. Automated Verification and Control of Infinite State Stochastic
Systems. Institute of Science and Technology Austria, 2023, doi:10.15479/14539.
short: D. Zikelic, Automated Verification and Control of Infinite State Stochastic
Systems, Institute of Science and Technology Austria, 2023.
date_created: 2023-11-15T13:39:10Z
date_published: 2023-11-15T00:00:00Z
date_updated: 2025-07-14T09:10:10Z
day: '15'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: KrCh
- _id: GradSch
doi: 10.15479/14539
ec_funded: 1
file:
- access_level: open_access
checksum: f23e002b0059ca78e1fbb864da52dd7e
content_type: application/pdf
creator: cchlebak
date_created: 2023-11-15T13:43:28Z
date_updated: 2023-11-15T13:43:28Z
file_id: '14540'
file_name: main.pdf
file_size: 2116426
relation: main_file
success: 1
- access_level: closed
checksum: 80ca37618a3c7b59866875f8be9b15ed
content_type: application/x-zip-compressed
creator: cchlebak
date_created: 2023-11-15T13:44:24Z
date_updated: 2023-11-15T13:44:24Z
file_id: '14541'
file_name: thesis_source.zip
file_size: 35884057
relation: source_file
file_date_updated: 2023-11-15T13:44:24Z
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-sa/4.0/
month: '11'
oa: 1
oa_version: Published Version
page: '256'
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_identifier:
isbn:
- 978-3-99078-036-7
issn:
- 2663 - 337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '1194'
relation: part_of_dissertation
status: public
- id: '12000'
relation: part_of_dissertation
status: public
- id: '12511'
relation: part_of_dissertation
status: public
- id: '14600'
relation: part_of_dissertation
status: public
- id: '14601'
relation: part_of_dissertation
status: public
- id: '9644'
relation: part_of_dissertation
status: public
- id: '10414'
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: Automated verification and control of infinite state stochastic systems
tmp:
image: /images/cc_by_nc_sa.png
legal_code_url: https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC
BY-NC-SA 4.0)
short: CC BY-NC-SA (4.0)
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2023'
...
---
_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: '10199'
abstract:
- lang: eng
text: The design and verification of concurrent systems remains an open challenge
due to the non-determinism that arises from the inter-process communication. In
particular, concurrent programs are notoriously difficult both to be written correctly
and to be analyzed formally, as complex thread interaction has to be accounted
for. The difficulties are further exacerbated when concurrent programs get executed
on modern-day hardware, which contains various buffering and caching mechanisms
for efficiency reasons. This causes further subtle non-determinism, which can
often produce very unintuitive behavior of the concurrent programs. Model checking
is at the forefront of tackling the verification problem, where the task is to
decide, given as input a concurrent system and a desired property, whether the
system satisfies the property. The inherent state-space explosion problem in model
checking of concurrent systems causes naïve explicit methods not to scale, thus
more inventive methods are required. One such method is stateless model checking
(SMC), which explores in memory-efficient manner the program executions rather
than the states of the program. State-of-the-art SMC is typically coupled with
partial order reduction (POR) techniques, which argue that certain executions
provably produce identical system behavior, thus limiting the amount of executions
one needs to explore in order to cover all possible behaviors. Another method
to tackle the state-space explosion is symbolic model checking, where the considered
techniques operate on a succinct implicit representation of the input system rather
than explicitly accessing the system. In this thesis we present new techniques
for verification of concurrent systems. We present several novel POR methods for
SMC of concurrent programs under various models of semantics, some of which account
for write-buffering mechanisms. Additionally, we present novel algorithms for
symbolic model checking of finite-state concurrent systems, where the desired
property of the systems is to ensure a formally defined notion of fairness.
acknowledged_ssus:
- _id: SSU
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Viktor
full_name: Toman, Viktor
id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
last_name: Toman
orcid: 0000-0001-9036-063X
citation:
ama: Toman V. Improved verification techniques for concurrent systems. 2021. doi:10.15479/at:ista:10199
apa: Toman, V. (2021). Improved verification techniques for concurrent systems.
Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:10199
chicago: Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.”
Institute of Science and Technology Austria, 2021. https://doi.org/10.15479/at:ista:10199.
ieee: V. Toman, “Improved verification techniques for concurrent systems,” Institute
of Science and Technology Austria, 2021.
ista: Toman V. 2021. Improved verification techniques for concurrent systems. Institute
of Science and Technology Austria.
mla: Toman, Viktor. Improved Verification Techniques for Concurrent Systems.
Institute of Science and Technology Austria, 2021, doi:10.15479/at:ista:10199.
short: V. Toman, Improved Verification Techniques for Concurrent Systems, Institute
of Science and Technology Austria, 2021.
date_created: 2021-10-29T20:09:01Z
date_published: 2021-10-31T00:00:00Z
date_updated: 2025-07-14T09:10:16Z
day: '31'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: GradSch
- _id: KrCh
doi: 10.15479/at:ista:10199
ec_funded: 1
file:
- access_level: open_access
checksum: 4f412a1ee60952221b499a4b1268df35
content_type: application/pdf
creator: vtoman
date_created: 2021-11-08T14:12:22Z
date_updated: 2021-11-08T14:12:22Z
file_id: '10225'
file_name: toman_th_final.pdf
file_size: 2915234
relation: main_file
- access_level: closed
checksum: 9584943f99127be2dd2963f6784c37d4
content_type: application/zip
creator: vtoman
date_created: 2021-11-08T14:12:46Z
date_updated: 2021-11-09T09:00:50Z
file_id: '10226'
file_name: toman_thesis.zip
file_size: 8616056
relation: source_file
file_date_updated: 2021-11-09T09:00:50Z
has_accepted_license: '1'
keyword:
- concurrency
- verification
- model checking
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '166'
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '10190'
relation: part_of_dissertation
status: public
- id: '9987'
relation: part_of_dissertation
status: public
- id: '141'
relation: part_of_dissertation
status: public
- id: '10191'
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: Improved verification techniques for concurrent systems
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2021'
...
---
_id: '10293'
abstract:
- lang: eng
text: "Indirect reciprocity in evolutionary game theory is a prominent mechanism
for explaining the evolution of cooperation among unrelated individuals. In contrast
to direct reciprocity, which is based on individuals meeting repeatedly, and conditionally
cooperating by using their own experiences, indirect reciprocity is based on individuals’
reputations. If a player helps another, this increases the helper’s public standing,
benefitting them in the future. This lets cooperation in the population emerge
without individuals having to meet more than once. While the two modes of reciprocity
are intertwined, they are difficult to compare. Thus, they are usually studied
in isolation. Direct reciprocity can maintain cooperation with simple strategies,
and is robust against noise even when players do not remember more\r\nthan their
partner’s last action. Meanwhile, indirect reciprocity requires its successful
strategies, or social norms, to be more complex. Exhaustive search previously
identified eight such norms, called the “leading eight”, which excel at maintaining
cooperation. However, as the first result of this thesis, we show that the leading
eight break down once we remove the fundamental assumption that information is
synchronized and public, such that everyone agrees on reputations. Once we consider
a more realistic scenario of imperfect information, where reputations are private,
and individuals occasionally misinterpret or miss observations, the leading eight
do not promote cooperation anymore. Instead, minor initial disagreements can proliferate,
fragmenting populations into subgroups. In a next step, we consider ways to mitigate
this issue. We first explore whether introducing “generosity” can stabilize cooperation
when players use the leading eight strategies in noisy environments. This approach
of modifying strategies to include probabilistic elements for coping with errors
is known to work well in direct reciprocity. However, as we show here, it fails
for the more complex norms of indirect reciprocity. Imperfect information still
prevents cooperation from evolving. On the other hand, we succeeded to show in
this thesis that modifying the leading eight to use “quantitative assessment”,
i.e. tracking reputation scores on a scale beyond good and bad, and making overall
judgments of others based on a threshold, is highly successful, even when noise
increases in the environment. Cooperation can flourish when reputations\r\nare
more nuanced, and players have a broader understanding what it means to be “good.”
Finally, we present a single theoretical framework that unites the two modes of
reciprocity despite their differences. Within this framework, we identify a novel
simple and successful strategy for indirect reciprocity, which can cope with noisy
environments and has an analogue in direct reciprocity. We can also analyze decision
making when different sources of information are available. Our results help highlight
that for sustaining cooperation, already the most simple rules of reciprocity
can be sufficient."
alternative_title:
- ISTA Thesis
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
citation:
ama: Schmid L. Evolution of cooperation via (in)direct reciprocity under imperfect
information. 2021. doi:10.15479/at:ista:10293
apa: Schmid, L. (2021). Evolution of cooperation via (in)direct reciprocity under
imperfect information. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:10293
chicago: Schmid, Laura. “Evolution of Cooperation via (in)Direct Reciprocity under
Imperfect Information.” Institute of Science and Technology Austria, 2021. https://doi.org/10.15479/at:ista:10293.
ieee: L. Schmid, “Evolution of cooperation via (in)direct reciprocity under imperfect
information,” Institute of Science and Technology Austria, 2021.
ista: Schmid L. 2021. Evolution of cooperation via (in)direct reciprocity under
imperfect information. Institute of Science and Technology Austria.
mla: Schmid, Laura. Evolution of Cooperation via (in)Direct Reciprocity under
Imperfect Information. Institute of Science and Technology Austria, 2021,
doi:10.15479/at:ista:10293.
short: L. Schmid, Evolution of Cooperation via (in)Direct Reciprocity under Imperfect
Information, Institute of Science and Technology Austria, 2021.
date_created: 2021-11-15T17:12:57Z
date_published: 2021-11-17T00:00:00Z
date_updated: 2025-07-14T09:10:09Z
day: '17'
ddc:
- '519'
- '576'
degree_awarded: PhD
department:
- _id: GradSch
- _id: KrCh
doi: 10.15479/at:ista:10293
ec_funded: 1
file:
- access_level: closed
checksum: 86a05b430756ca12ae8107b6e6f3c1e5
content_type: application/zip
creator: lschmid
date_created: 2021-11-18T12:41:46Z
date_updated: 2022-12-20T23:30:08Z
embargo_to: open_access
file_id: '10305'
file_name: submission_new.zip
file_size: 29703124
relation: source_file
- access_level: open_access
checksum: d940af042e94660c6b6a7b4f0b184d47
content_type: application/pdf
creator: lschmid
date_created: 2021-11-18T12:59:15Z
date_updated: 2022-12-20T23:30:08Z
embargo: 2022-10-18
file_id: '10306'
file_name: thesis_new_upload.pdf
file_size: 8320985
relation: main_file
file_date_updated: 2022-12-20T23:30:08Z
has_accepted_license: '1'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: '171'
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '9997'
relation: part_of_dissertation
status: public
- id: '2'
relation: part_of_dissertation
status: public
- id: '9402'
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: Evolution of cooperation via (in)direct reciprocity under imperfect information
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2021'
...
---
_id: '7196'
abstract:
- lang: eng
text: 'In this thesis we study certain mathematical aspects of evolution. The two
primary forces that drive an evolutionary process are mutation and selection.
Mutation generates new variants in a population. Selection chooses among the variants
depending on the reproductive rates of individuals. Evolutionary processes are
intrinsically random – a new mutation that is initially present in the population
at low frequency can go extinct, even if it confers a reproductive advantage.
The overall rate of evolution is largely determined by two quantities: the probability
that an invading advantageous mutation spreads through the population (called
fixation probability) and the time until it does so (called fixation time). Both
those quantities crucially depend not only on the strength of the invading mutation
but also on the population structure. In this thesis, we aim to understand how
the underlying population structure affects the overall rate of evolution. Specifically,
we study population structures that increase the fixation probability of advantageous
mutants (called amplifiers of selection). Broadly speaking, our results are of
three different types: We present various strong amplifiers, we identify regimes
under which only limited amplification is feasible, and we propose population
structures that provide different tradeoffs between high fixation probability
and short fixation time.'
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
citation:
ama: Tkadlec J. A role of graphs in evolutionary processes. 2020. doi:10.15479/AT:ISTA:7196
apa: Tkadlec, J. (2020). A role of graphs in evolutionary processes. Institute
of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:7196
chicago: Tkadlec, Josef. “A Role of Graphs in Evolutionary Processes.” Institute
of Science and Technology Austria, 2020. https://doi.org/10.15479/AT:ISTA:7196.
ieee: J. Tkadlec, “A role of graphs in evolutionary processes,” Institute of Science
and Technology Austria, 2020.
ista: Tkadlec J. 2020. A role of graphs in evolutionary processes. Institute of
Science and Technology Austria.
mla: Tkadlec, Josef. A Role of Graphs in Evolutionary Processes. Institute
of Science and Technology Austria, 2020, doi:10.15479/AT:ISTA:7196.
short: J. Tkadlec, A Role of Graphs in Evolutionary Processes, Institute of Science
and Technology Austria, 2020.
date_created: 2019-12-20T12:26:36Z
date_published: 2020-01-12T00:00:00Z
date_updated: 2023-10-17T12:29:46Z
day: '12'
ddc:
- '519'
degree_awarded: PhD
department:
- _id: KrCh
- _id: GradSch
doi: 10.15479/AT:ISTA:7196
file:
- access_level: closed
checksum: 451f8e64b0eb26bf297644ac72bfcbe9
content_type: application/zip
creator: jtkadlec
date_created: 2020-01-12T11:49:49Z
date_updated: 2020-07-14T12:47:52Z
file_id: '7255'
file_name: thesis.zip
file_size: 21100497
relation: source_file
- access_level: open_access
checksum: d8c44cbc4f939c49a8efc9d4b8bb3985
content_type: application/pdf
creator: dernst
date_created: 2020-01-28T07:32:42Z
date_updated: 2020-07-14T12:47:52Z
file_id: '7367'
file_name: 2020_Tkadlec_Thesis.pdf
file_size: 11670983
relation: main_file
file_date_updated: 2020-07-14T12:47:52Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '144'
publication_identifier:
eissn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '7210'
relation: dissertation_contains
status: public
- id: '5751'
relation: dissertation_contains
status: public
- id: '7212'
relation: dissertation_contains
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: A role of graphs in evolutionary processes
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2020'
...
---
_id: '821'
abstract:
- lang: eng
text: "This dissertation focuses on algorithmic aspects of program verification,
and presents modeling and complexity advances on several problems related to the\r\nstatic
analysis of programs, the stateless model checking of concurrent programs, and
the competitive analysis of real-time scheduling algorithms.\r\nOur contributions
can be broadly grouped into five categories.\r\n\r\nOur first contribution is
a set of new algorithms and data structures for the quantitative and data-flow
analysis of programs, based on the graph-theoretic notion of treewidth.\r\nIt
has been observed that the control-flow graphs of typical programs have special
structure, and are characterized as graphs of small treewidth.\r\nWe utilize this
structural property to provide faster algorithms for the quantitative and data-flow
analysis of recursive and concurrent programs.\r\nIn most cases we make an algebraic
treatment of the considered problem,\r\nwhere several interesting analyses, such
as the reachability, shortest path, and certain kind of data-flow analysis problems
follow as special cases. \r\nWe exploit the constant-treewidth property to obtain
algorithmic improvements for on-demand versions of the problems, \r\nand provide
data structures with various tradeoffs between the resources spent in the preprocessing
and querying phase.\r\nWe also improve on the algorithmic complexity of quantitative
problems outside the algebraic path framework,\r\nnamely of the minimum mean-payoff,
minimum ratio, and minimum initial credit for energy problems.\r\n\r\n\r\nOur
second contribution is a set of algorithms for Dyck reachability with applications
to data-dependence analysis and alias analysis.\r\nIn particular, we develop an
optimal algorithm for Dyck reachability on bidirected graphs, which are ubiquitous
in context-insensitive, field-sensitive points-to analysis.\r\nAdditionally, we
develop an efficient algorithm for context-sensitive data-dependence analysis
via Dyck reachability,\r\nwhere the task is to obtain analysis summaries of library
code in the presence of callbacks.\r\nOur algorithm preprocesses libraries in
almost linear time, after which the contribution of the library in the complexity
of the client analysis is (i)~linear in the number of call sites and (ii)~only
logarithmic in the size of the whole library, as opposed to linear in the size
of the whole library.\r\nFinally, we prove that Dyck reachability is Boolean Matrix
Multiplication-hard in general, and the hardness also holds for graphs of constant
treewidth.\r\nThis hardness result strongly indicates that there exist no combinatorial
algorithms for Dyck reachability with truly subcubic complexity.\r\n\r\n\r\nOur
third contribution is the formalization and algorithmic treatment of the Quantitative
Interprocedural Analysis framework.\r\nIn this framework, the transitions of a
recursive program are annotated as good, bad or neutral, and receive a weight
which measures\r\nthe magnitude of their respective effect.\r\nThe Quantitative
Interprocedural Analysis problem asks to determine whether there exists an infinite
run of the program where the long-run ratio of the bad weights over the good weights
is above a given threshold.\r\nWe illustrate how several quantitative problems
related to static analysis of recursive programs can be instantiated in this framework,\r\nand
present some case studies to this direction.\r\n\r\n\r\nOur fourth contribution
is a new dynamic partial-order reduction for the stateless model checking of concurrent
programs. Traditional approaches rely on the standard Mazurkiewicz equivalence
between traces, by means of partitioning the trace space into equivalence classes,
and attempting to explore a few representatives from each class.\r\nWe present
a new dynamic partial-order reduction method called the Data-centric Partial
Order Reduction (DC-DPOR).\r\nOur algorithm is based on a new equivalence between
traces, called the observation equivalence.\r\nDC-DPOR explores a coarser partitioning
of the trace space than any exploration method based on the standard Mazurkiewicz
equivalence.\r\nDepending on the program, the new partitioning can be even exponentially
coarser.\r\nAdditionally, DC-DPOR spends only polynomial time in each explored
class.\r\n\r\n\r\nOur fifth contribution is the use of automata and game-theoretic
verification techniques in the competitive analysis and synthesis of real-time
scheduling algorithms for firm-deadline tasks.\r\nOn the analysis side, we leverage
automata on infinite words to compute the competitive ratio of real-time schedulers
subject to various environmental constraints.\r\nOn the synthesis side, we introduce
a new instance of two-player mean-payoff partial-information games, and show\r\nhow
the synthesis of an optimal real-time scheduler can be reduced to computing winning
strategies in this new type of games."
acknowledgement: "First, I am thankful to my advisor, Krishnendu Chatterjee, for offering
me the opportunity to\r\nmaterialize my scientific curiosity in a remarkably wide
range of interesting topics, as well as for his constant availability and continuous
support throughout my doctoral studies. I have had the privilege of collaborating
with, discussing and getting inspired by all members of my committee: Thomas A.
Henzinger, Ulrich Schmid and Martin A. Nowak. The role of the above four people
has been very instrumental both to the research carried out for this dissertation,
and to the researcher I evolved to in the process.\r\nI have greatly enjoyed my
numerous brainstorming sessions with Rasmus Ibsen-Jensen, many\r\nof which led to
results on low-treewidth graphs presented here. I thank Alex Kößler for our\r\ndiscussions
on modeling and analyzing real-time scheduling algorithms, Yaron Velner for our\r\ncollaboration
on the Quantitative Interprocedural Analysis framework, and Nishant Sinha for our
initial discussions on partial order reduction techniques in stateless model checking.
I also thank Jan Otop, Ben Adlam, Bernhard Kragl and Josef Tkadlec for our fruitful
collaborations on\r\ntopics outside the scope of this dissertation, as well as the
interns Prateesh Goyal, Amir Kafshdar Goharshady, Samarth Mishra, Bhavya Choudhary
and Marek Chalupa, with whom I have shared my excitement on various research topics.
Together with my collaborators, I thank officemates and members of the Chatterjee
and Henzinger groups throughout the years, Thorsten Tarrach, Ventsi Chonev, Roopsha
Samanta, Przemek Daca, Mirco Giacobbe, Tanja Petrov, Ashutosh\r\nGupta, Arjun Radhakrishna,
\ Petr Novontý, Christian Hilbe, Jakob Ruess, Martin Chmelik,\r\nCezara Dragoi,
Johannes Reiter, Andrey Kupriyanov, Guy Avni, Sasha Rubin, Jessica Davies, Hongfei
Fu, Thomas Ferrère, Pavol Cerný, Ali Sezgin, Jan Kretínský, Sergiy Bogomolov, Hui\r\nKong,
Benjamin Aminof, Duc-Hiep Chu, and Damien Zufferey. Besides collaborations and
office spaces, with many of the above people I have been fortunate to share numerous
whiteboard\r\ndiscussions, as well as memorable long walks and amicable meals accompanied
by stimulating\r\nconversations. I am highly indebted to Elisabeth Hacker for her
continuous assistance in matters\r\nthat often exceeded her official duties, and
who made my integration in Austria a smooth process."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: Pavlogiannis A. Algorithmic advances in program analysis and their applications.
2017. doi:10.15479/AT:ISTA:th_854
apa: Pavlogiannis, A. (2017). Algorithmic advances in program analysis and their
applications. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:th_854
chicago: Pavlogiannis, Andreas. “Algorithmic Advances in Program Analysis and Their
Applications.” Institute of Science and Technology Austria, 2017. https://doi.org/10.15479/AT:ISTA:th_854.
ieee: A. Pavlogiannis, “Algorithmic advances in program analysis and their applications,”
Institute of Science and Technology Austria, 2017.
ista: Pavlogiannis A. 2017. Algorithmic advances in program analysis and their applications.
Institute of Science and Technology Austria.
mla: Pavlogiannis, Andreas. Algorithmic Advances in Program Analysis and Their
Applications. Institute of Science and Technology Austria, 2017, doi:10.15479/AT:ISTA:th_854.
short: A. Pavlogiannis, Algorithmic Advances in Program Analysis and Their Applications,
Institute of Science and Technology Austria, 2017.
date_created: 2018-12-11T11:48:41Z
date_published: 2017-08-09T00:00:00Z
date_updated: 2023-09-07T12:01:59Z
day: '09'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: KrCh
doi: 10.15479/AT:ISTA:th_854
ec_funded: 1
file:
- access_level: open_access
checksum: 3a3ec003f6ee73f41f82a544d63dfc77
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:44Z
date_updated: 2020-07-14T12:48:10Z
file_id: '4900'
file_name: IST-2017-854-v1+1_Pavlogiannis_Thesis_PubRep.pdf
file_size: 4103115
relation: main_file
- access_level: closed
checksum: bd2facc45ff8a2e20c5ed313c2ccaa83
content_type: application/zip
creator: dernst
date_created: 2019-04-05T07:59:31Z
date_updated: 2020-07-14T12:48:10Z
file_id: '6201'
file_name: 2017_thesis_Pavlogiannis.zip
file_size: 14744374
relation: source_file
file_date_updated: 2020-07-14T12:48:10Z
has_accepted_license: '1'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '08'
oa: 1
oa_version: Published Version
page: '418'
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'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '6828'
pubrep_id: '854'
related_material:
record:
- id: '1071'
relation: part_of_dissertation
status: public
- id: '1437'
relation: part_of_dissertation
status: public
- id: '1602'
relation: part_of_dissertation
status: public
- id: '1604'
relation: part_of_dissertation
status: public
- id: '1607'
relation: part_of_dissertation
status: public
- id: '1714'
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: Algorithmic advances in program analysis and their applications
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2017'
...
---
_id: '1397'
abstract:
- lang: eng
text: 'We study partially observable Markov decision processes (POMDPs) with objectives
used in verification and artificial intelligence. The qualitative analysis problem
given a POMDP and an objective asks whether there is a strategy (policy) to ensure
that the objective is satisfied almost surely (with probability 1), resp. with
positive probability (with probability greater than 0). For POMDPs with limit-average
payoff, where a reward value in the interval [0,1] is associated to every transition,
and the payoff of an infinite path is the long-run average of the rewards, we
consider two types of path constraints: (i) a quantitative limit-average constraint
defines the set of paths where the payoff is at least a given threshold L1 = 1.
Our main results for qualitative limit-average constraint under almost-sure winning
are as follows: (i) the problem of deciding the existence of a finite-memory controller
is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory
controller is undecidable. For quantitative limit-average constraints we show
that the problem of deciding the existence of a finite-memory controller is undecidable.
We present a prototype implementation of our EXPTIME algorithm. For POMDPs with
w-regular conditions specified as parity objectives, while the qualitative analysis
problems are known to be undecidable even for very special case of parity objectives,
we establish decidability (with optimal complexity) of the qualitative analysis
problems for POMDPs with parity objectives under finite-memory strategies. We
establish optimal (exponential) memory bounds and EXPTIME-completeness of the
qualitative analysis problems under finite-memory strategies for POMDPs with parity
objectives. Based on our theoretical algorithms we also present a practical approach,
where we design heuristics to deal with the exponential complexity, and have applied
our implementation on a number of well-known POMDP examples for robotics applications.
For POMDPs with a set of target states and an integer cost associated with every
transition, we study the optimization objective that asks to minimize the expected
total cost of reaching a state in the target set, while ensuring that the target
set is reached almost surely. We show that for general integer costs approximating
the optimal cost is undecidable. For positive costs, our results are as follows:
(i) we establish matching lower and upper bounds for the optimal cost, both double
and exponential in the POMDP state space size; (ii) we show that the problem of
approximating the optimal cost is decidable and present approximation algorithms
that extend existing algorithms for POMDPs with finite-horizon objectives. We
show experimentally that it performs well in many examples of interest. We study
more deeply the problem of almost-sure reachability, where given a set of target
states, the question is to decide whether there is a strategy to ensure that the
target set is reached almost surely. While in general the problem EXPTIME-complete,
in many practical cases strategies with a small amount of memory suffice. Moreover,
the existing solution to the problem is explicit, which first requires to construct
explicitly an exponential reduction to a belief-support MDP. We first study the
existence of observation-stationary strategies, which is NP-complete, and then
small-memory strategies. We present a symbolic algorithm by an efficient encoding
to SAT and using a SAT solver for the problem. We report experimental results
demonstrating the scalability of our symbolic (SAT-based) approach. Decentralized
POMDPs (DEC-POMDPs) extend POMDPs to a multi-agent setting, where several agents
operate in an uncertain environment independently to achieve a joint objective.
In this work we consider Goal DEC-POMDPs, where given a set of target states,
the objective is to ensure that the target set is reached with minimal cost. We
consider the indefinite-horizon (infinite-horizon with either discounted-sum,
or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present
a new and novel method to solve the problem that extends methods for finite-horizon
DEC-POMDPs and the real-time dynamic programming approach for POMDPs. We present
experimental results on several examples, and show that our approach presents
promising results. In the end we present a short summary of a few other results
related to verification of MDPs and POMDPs.'
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: Chmelik M. Algorithms for partially observable markov decision processes. 2016.
apa: Chmelik, M. (2016). Algorithms for partially observable markov decision
processes. Institute of Science and Technology Austria.
chicago: Chmelik, Martin. “Algorithms for Partially Observable Markov Decision Processes.”
Institute of Science and Technology Austria, 2016.
ieee: M. Chmelik, “Algorithms for partially observable markov decision processes,”
Institute of Science and Technology Austria, 2016.
ista: Chmelik M. 2016. Algorithms for partially observable markov decision processes.
Institute of Science and Technology Austria.
mla: Chmelik, Martin. Algorithms for Partially Observable Markov Decision Processes.
Institute of Science and Technology Austria, 2016.
short: M. Chmelik, Algorithms for Partially Observable Markov Decision Processes,
Institute of Science and Technology Austria, 2016.
date_created: 2018-12-11T11:51:47Z
date_published: 2016-02-01T00:00:00Z
date_updated: 2023-09-07T11:54:58Z
day: '01'
degree_awarded: PhD
department:
- _id: KrCh
language:
- iso: eng
month: '02'
oa_version: None
page: '232'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5810'
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: Algorithms for partially observable markov decision processes
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2016'
...
---
_id: '1400'
abstract:
- lang: eng
text: Cancer results from an uncontrolled growth of abnormal cells. Sequentially
accumulated genetic and epigenetic alterations decrease cell death and increase
cell replication. We used mathematical models to quantify the effect of driver
gene mutations. The recently developed targeted therapies can lead to dramatic
regressions. However, in solid cancers, clinical responses are often short-lived
because resistant cancer cells evolve. We estimated that approximately 50 different
mutations can confer resistance to a typical targeted therapeutic agent. We find
that resistant cells are likely to be present in expanded subclones before the
start of the treatment. The dominant strategy to prevent the evolution of resistance
is combination therapy. Our analytical results suggest that in most patients,
dual therapy, but not monotherapy, can result in long-term disease control. However,
long-term control can only occur if there are no possible mutations in the genome
that can cause cross-resistance to both drugs. Furthermore, we showed that simultaneous
therapy with two drugs is much more likely to result in long-term disease control
than sequential therapy with the same drugs. To improve our understanding of the
underlying subclonal evolution we reconstruct the evolutionary history of a patient's
cancer from next-generation sequencing data of spatially-distinct DNA samples.
Using a quantitative measure of genetic relatedness, we found that pancreatic
cancers and their metastases demonstrated a higher level of relatedness than that
expected for any two cells randomly taken from a normal tissue. This minimal amount
of genetic divergence among advanced lesions indicates that genetic heterogeneity,
when quantitatively defined, is not a fundamental feature of the natural history
of untreated pancreatic cancers. Our newly developed, phylogenomic tool Treeomics
finds evidence for seeding patterns of metastases and can directly be used to
discover rules governing the evolution of solid malignancies to transform cancer
into a more predictable disease.
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Johannes
full_name: Reiter, Johannes
id: 4A918E98-F248-11E8-B48F-1D18A9856A87
last_name: Reiter
orcid: 0000-0002-0170-7353
citation:
ama: Reiter J. The subclonal evolution of cancer. 2015.
apa: Reiter, J. (2015). The subclonal evolution of cancer. Institute of Science
and Technology Austria.
chicago: Reiter, Johannes. “The Subclonal Evolution of Cancer.” Institute of Science
and Technology Austria, 2015.
ieee: J. Reiter, “The subclonal evolution of cancer,” Institute of Science and Technology
Austria, 2015.
ista: Reiter J. 2015. The subclonal evolution of cancer. Institute of Science and
Technology Austria.
mla: Reiter, Johannes. The Subclonal Evolution of Cancer. Institute of Science
and Technology Austria, 2015.
short: J. Reiter, The Subclonal Evolution of Cancer, Institute of Science and Technology
Austria, 2015.
date_created: 2018-12-11T11:51:48Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2023-09-07T11:40:44Z
day: '01'
degree_awarded: PhD
department:
- _id: KrCh
language:
- iso: eng
month: '04'
oa_version: None
page: '183'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5807'
related_material:
record:
- id: '1709'
relation: part_of_dissertation
status: public
- id: '2000'
relation: part_of_dissertation
status: public
- id: '2247'
relation: part_of_dissertation
status: public
- id: '2816'
relation: part_of_dissertation
status: public
- id: '2858'
relation: part_of_dissertation
status: public
- id: '3157'
relation: part_of_dissertation
status: public
- id: '3260'
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: The subclonal evolution of cancer
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2015'
...