---
_id: '5457'
_version: 15
abstract:
- lang: eng
text: "We consider the problem of expected cost analysis over nondeterministic probabilistic
programs, which aims at automated methods for analyzing the resource-usage of
such programs. Previous approaches for this problem could only handle nonnegative
bounded costs. However, in many scenarios, such as queuing networks or analysis
of cryptocurrency protocols, both positive and negative costs are necessary and
the costs are unbounded as well.\r\n\r\nIn this work, we present a sound and efficient
approach to obtain polynomial bounds on the expected accumulated cost of nondeterministic
probabilistic programs. Our approach can handle (a) general positive and negative
costs with bounded updates in variables; and (b) nonnegative costs with general
updates to variables. We show that several natural examples which could not be
handled by previous approaches are captured in our framework.\r\n\r\nMoreover,
our approach leads to an efficient polynomial-time algorithm, while no previous
approach for cost analysis of probabilistic programs could guarantee polynomial
runtime. Finally, we show the effectiveness of our approach by presenting experimental
results on a variety of programs, motivated by real-world applications, for which
we efficiently synthesize tight resource-usage bounds."
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: '1'
full_name: Anonymous, 1
last_name: Anonymous
- first_name: '2'
full_name: Anonymous, 2
last_name: Anonymous
- first_name: '3'
full_name: Anonymous, 3
last_name: Anonymous
- first_name: '4'
full_name: Anonymous, 4
last_name: Anonymous
- first_name: '5'
full_name: Anonymous, 5
last_name: Anonymous
- first_name: '6'
full_name: Anonymous, 6
last_name: Anonymous
citation:
ama: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4, Anonymous 5, Anonymous
6. *Cost Analysis of Nondeterministic Probabilistic Programs*. IST Austria;
2018.
apa: Anonymous, 1, Anonymous, 2, Anonymous, 3, Anonymous, 4, Anonymous, 5, &
Anonymous, 6. (2018). *Cost analysis of nondeterministic probabilistic programs*.
IST Austria.
chicago: Anonymous, 1, 2 Anonymous, 3 Anonymous, 4 Anonymous, 5 Anonymous, and 6
Anonymous. *Cost Analysis of Nondeterministic Probabilistic Programs*. IST
Austria, 2018.
ieee: 1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, 5 Anonymous, and 6 Anonymous,
*Cost analysis of nondeterministic probabilistic programs*. IST Austria,
2018.
ista: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4, Anonymous 5, Anonymous
6. 2018. Cost analysis of nondeterministic probabilistic programs, IST Austria,
27p.
mla: Anonymous, 1, et al. *Cost Analysis of Nondeterministic Probabilistic Programs*.
IST Austria, 2018.
short: 1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, 5 Anonymous, 6 Anonymous,
Cost Analysis of Nondeterministic Probabilistic Programs, IST Austria, 2018.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:26Z
date_published: 2018-11-11T00:00:00Z
date_updated: 2019-08-02T12:38:55Z
day: '11'
ddc:
- '000'
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:32Z
date_updated: 2018-12-12T11:53:32Z
file_id: '5493'
file_name: IST-2018-1066-v1+1_techreport.pdf
file_size: 4202966
open_access: 1
relation: main_file
- access_level: closed
content_type: text/plain
creator: dernst
date_created: 2019-05-10T13:22:12Z
date_updated: 2019-05-10T13:22:12Z
file_id: '6402'
file_name: authors-names.txt
file_size: 322
open_access: 0
relation: main_file
request_a_copy: 0
file_date_updated: 2019-05-10T13:22:12Z
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: '27'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '1066'
status: public
title: Cost analysis of nondeterministic probabilistic programs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2018'
...
---
_id: '6426'
_version: 27
abstract:
- lang: eng
text: Synchronous programs are easy to specify because the side effects of an operation
are finished by the time the invocation of the operation returns to the caller.
Asynchronous programs, on the other hand, are difficult to specify because there
are side effects due to pending computation scheduled as a result of the invocation
of an operation. They are also difficult to verify because of the large number
of possible interleavings of concurrent asynchronous computation threads. We show
that specifications and correctness proofs for asynchronous programs can be structured
by introducing the fiction, for proof purposes, that intermediate, non-quiescent
states of asynchronous operations can be ignored. Then, the task of specification
becomes relatively simple and the task of verification can be naturally decomposed
into smaller sub-tasks. The sub-tasks iteratively summarize, guided by the structure
of an asynchronous program, the atomic effect of non-atomic operations and the
synchronous effect of asynchronous operations. This structuring of specifications
and proofs corresponds to the introduction of multiple layers of stepwise refinement
for asynchronous programs. We present the first proof rule, called synchronization,
to reduce asynchronous invocations on a lower layer to synchronous invocations
on a higher layer. We implemented our proof method in CIVL and evaluated it on
a collection of benchmark programs.
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
citation:
ama: Henzinger TA, Kragl B, Qadeer S. *Synchronizing the Asynchronous*. IST
Austria; 2017. doi:10.15479/AT:IST-2018-853-v2-2
apa: Henzinger, T. A., Kragl, B., & Qadeer, S. (2017). *Synchronizing the
asynchronous*. IST Austria. https://doi.org/10.15479/AT:IST-2018-853-v2-2
chicago: Henzinger, Thomas A, Bernhard Kragl, and Shaz Qadeer. *Synchronizing
the Asynchronous*. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2018-853-v2-2.
ieee: T. A. Henzinger, B. Kragl, and S. Qadeer, *Synchronizing the asynchronous*.
IST Austria, 2017.
ista: Henzinger TA, Kragl B, Qadeer S. 2017. Synchronizing the asynchronous, IST
Austria, 28p.
mla: Henzinger, Thomas A., et al. *Synchronizing the Asynchronous*. IST Austria,
2017, doi:10.15479/AT:IST-2018-853-v2-2.
short: T.A. Henzinger, B. Kragl, S. Qadeer, Synchronizing the Asynchronous, IST
Austria, 2017.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2019-05-13T08:15:55Z
date_published: 2017-08-04T00:00:00Z
date_updated: 2019-11-14T08:43:31Z
day: '04'
ddc:
- '000'
department:
- _id: ToHe
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2018-853-v2-2
file:
- access_level: open_access
content_type: application/pdf
creator: dernst
date_created: 2019-05-13T08:14:44Z
date_updated: 2019-05-13T08:14:44Z
file_id: '6431'
file_name: main(1).pdf
file_size: 971347
open_access: 1
relation: main_file
success: 1
file_date_updated: 2019-05-13T08:14:44Z
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: '28'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
related_material:
record:
- id: '133'
relation: later_version
status: public
status: public
title: Synchronizing the asynchronous
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...
---
_id: '5455'
_version: 11
abstract:
- lang: eng
text: 'A fundamental algorithmic problem at the heart of static analysis is Dyck
reachability. The input is a graphwhere the edges are labeled with different types
of opening and closing parentheses, and the reachabilityinformation is computed
via paths whose parentheses are properly matched. We present new results for Dyckreachability
problems with applications to alias analysis and data-dependence analysis. Our
main contributions,that include improved upper bounds as well as lower bounds
that establish optimality guarantees, are asfollows:First, we consider Dyck reachability
on bidirected graphs, which is the standard way of performing field-sensitive
points-to analysis. Given a bidirected graph withnnodes andmedges, we present:
(i) an algorithmwith worst-case running timeO(m+n·α(n)), whereα(n)is the inverse
Ackermann function, improving thepreviously knownO(n2)time bound; (ii) a matching
lower bound that shows that our algorithm is optimalwrt to worst-case complexity;
and (iii) an optimal average-case upper bound ofO(m)time, improving thepreviously
knownO(m·logn)bound.Second, we consider the problem of context-sensitive data-dependence
analysis, where the task is to obtainanalysis summaries of library code in the
presence of callbacks. Our algorithm preprocesses libraries in almostlinear time,
after which the contribution of the library in the complexity of the client analysis
is only linear,and only wrt the number of call sites.Third, we prove that combinatorial
algorithms for Dyck reachability on general graphs with truly sub-cubic bounds
cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean
MatrixMultiplication, which is a long-standing open problem. Thus we establish
that the existing combinatorialalgorithms for Dyck reachability are (conditionally)
optimal for general graphs. We also show that the samehardness holds for graphs
of constant treewidth.Finally, we provide a prototype implementation of our algorithms
for both alias analysis and data-dependenceanalysis. Our experimental evaluation
demonstrates that the new algorithms significantly outperform allexisting methods
on the two problems, over real-world benchmarks.'
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Bhavya
full_name: Choudhary, Bhavya
last_name: Choudhary
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
citation:
ama: Chatterjee K, Choudhary B, Pavlogiannis A. *Optimal Dyck Reachability for
Data-Dependence and Alias Analysis*. IST Austria; 2017. doi:10.15479/AT:IST-2017-870-v1-1
apa: Chatterjee, K., Choudhary, B., & Pavlogiannis, A. (2017). *Optimal Dyck
reachability for data-dependence and alias analysis*. IST Austria. https://doi.org/10.15479/AT:IST-2017-870-v1-1
chicago: Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. *Optimal
Dyck Reachability for Data-Dependence and Alias Analysis*. IST Austria, 2017.
https://doi.org/10.15479/AT:IST-2017-870-v1-1.
ieee: K. Chatterjee, B. Choudhary, and A. Pavlogiannis, *Optimal Dyck reachability
for data-dependence and alias analysis*. IST Austria, 2017.
ista: Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability
for data-dependence and alias analysis, IST Austria, 37p.
mla: Chatterjee, Krishnendu, et al. *Optimal Dyck Reachability for Data-Dependence
and Alias Analysis*. IST Austria, 2017, doi:10.15479/AT:IST-2017-870-v1-1.
short: K. Chatterjee, B. Choudhary, A. Pavlogiannis, Optimal Dyck Reachability for
Data-Dependence and Alias Analysis, IST Austria, 2017.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:26Z
date_published: 2017-10-23T00:00:00Z
date_updated: 2019-08-02T12:38:55Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2017-870-v1-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:02Z
date_updated: 2018-12-12T11:54:02Z
file_id: '5524'
file_name: IST-2017-870-v1+1_main.pdf
file_size: 960491
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:54:02Z
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '37'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '870'
status: public
title: Optimal Dyck reachability for data-dependence and alias analysis
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...
---
_id: '5456'
_version: 24
abstract:
- lang: eng
text: "We present a new dynamic partial-order reduction method for stateless model
checking of concurrent programs. A common approach for exploring program behaviors
relies on enumerating the traces of the program, without storing the visited states
(aka stateless exploration). As the number of distinct traces grows exponentially,
dynamic partial-order reduction (DPOR) techniques have been successfully used
to partition the space of traces into equivalence classes (Mazurkiewicz partitioning),
with the goal of exploring only few representative traces from each class.\r\nWe
introduce a new equivalence on traces under sequential consistency semantics,
which we call the observation equivalence. Two traces are observationally equivalent
if every read event observes the same write event in both traces. While the traditional
Mazurkiewicz equivalence is control-centric, our new definition is data-centric.
We show that our observation equivalence is coarser than the Mazurkiewicz equivalence,
and in many cases even exponentially coarser. We devise a DPOR exploration of
the trace space, called data-centric DPOR, based on the observation equivalence.\r\n1.
For acyclic architectures, our algorithm is guaranteed to explore exactly one
representative trace from each observation class, while spending polynomial time
per class. Hence, our algorithm is optimal wrt the observation equivalence, and
in several cases explores exponentially fewer traces than any enumerative method
based on the Mazurkiewicz equivalence.\r\n2. For cyclic architectures, we consider
an equivalence between traces which is finer than the observation equivalence;
but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially
coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence.
\r\nFinally, we perform a basic experimental comparison between the existing Mazurkiewicz-based
DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show
a significant reduction in both running time and the number of explored equivalence
classes."
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Marek
full_name: Chalupa, Marek
last_name: Chalupa
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
- first_name: Nishant
full_name: Sinha, Nishant
last_name: Sinha
- first_name: Kapil
full_name: Vaidya, Kapil
last_name: Vaidya
citation:
ama: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. *Data-Centric
Dynamic Partial Order Reduction*. IST Austria; 2017. doi:10.15479/AT:IST-2017-872-v1-1
apa: Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., & Vaidya, K.
(2017). *Data-centric dynamic partial order reduction*. IST Austria. https://doi.org/10.15479/AT:IST-2017-872-v1-1
chicago: Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha,
and Kapil Vaidya. *Data-Centric Dynamic Partial Order Reduction*. IST Austria,
2017. https://doi.org/10.15479/AT:IST-2017-872-v1-1.
ieee: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, *Data-centric
dynamic partial order reduction*. IST Austria, 2017.
ista: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric
dynamic partial order reduction, IST Austria, 36p.
mla: Chalupa, Marek, et al. *Data-Centric Dynamic Partial Order Reduction*.
IST Austria, 2017, doi:10.15479/AT:IST-2017-872-v1-1.
short: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Data-Centric
Dynamic Partial Order Reduction, IST Austria, 2017.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:26Z
date_published: 2017-10-23T00:00:00Z
date_updated: 2019-11-14T08:43:09Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2017-872-v1-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:26Z
date_updated: 2018-12-12T11:53:26Z
file_id: '5487'
file_name: IST-2017-872-v1+1_main.pdf
file_size: 910347
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:53:26Z
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '36'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '872'
related_material:
record:
- id: '5448'
relation: earlier_version
status: public
status: public
title: Data-centric dynamic partial order reduction
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...
---
_id: '5447'
_version: 14
abstract:
- lang: eng
text: "We consider the problem of developing automated techniques to aid the average-case
complexity analysis of programs. Several classical textbook algorithms have quite
efficient average-case complexity, whereas the corresponding worst-case bounds
are either inefficient (e.g., QUICK-SORT), or completely ineffective (e.g., COUPONCOLLECTOR).
Since the main focus of average-case analysis is to obtain efficient bounds, we
consider bounds that are either logarithmic,\r\nlinear, or almost-linear (O(log
n), O(n), O(n · log n),\r\nrespectively, where n represents the size of the input).
Our main contribution is a sound approach for deriving such average-case bounds
for randomized recursive programs. Our approach is efficient (a simple linear-time
algorithm), and it is based on (a) the analysis of recurrence relations induced
by randomized algorithms, and (b) a guess-and-check technique. Our approach can
infer the asymptotically optimal average-case bounds for classical randomized
algorithms, including RANDOMIZED-SEARCH, QUICKSORT, QUICK-SELECT, COUPON-COLLECTOR,
where the worstcase\r\nbounds are either inefficient (such as linear as compared
to logarithmic of average-case, or quadratic as compared to linear or almost-linear
of average-case), or ineffective. We have implemented our approach, and the experimental
results show that we obtain the bounds efficiently for various classical algorithms."
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: '1'
full_name: Anonymous, 1
last_name: Anonymous
- first_name: '2'
full_name: Anonymous, 2
last_name: Anonymous
- first_name: '3'
full_name: Anonymous, 3
last_name: Anonymous
citation:
ama: 'Anonymous 1, Anonymous 2, Anonymous 3. *Average-Case Analysis of Programs:
Automated Recurrence Analysis for Almost-Linear Bounds*. IST Austria; 2016.'
apa: 'Anonymous, 1, Anonymous, 2, & Anonymous, 3. (2016). *Average-case analysis
of programs: Automated recurrence analysis for almost-linear bounds*. IST Austria.'
chicago: 'Anonymous, 1, 2 Anonymous, and 3 Anonymous. *Average-Case Analysis of
Programs: Automated Recurrence Analysis for Almost-Linear Bounds*. IST Austria,
2016.'
ieee: '1 Anonymous, 2 Anonymous, and 3 Anonymous, *Average-case analysis of programs:
Automated recurrence analysis for almost-linear bounds*. IST Austria, 2016.'
ista: 'Anonymous 1, Anonymous 2, Anonymous 3. 2016. Average-case analysis of programs:
Automated recurrence analysis for almost-linear bounds, IST Austria, 20p.'
mla: 'Anonymous, 1, et al. *Average-Case Analysis of Programs: Automated Recurrence
Analysis for Almost-Linear Bounds*. IST Austria, 2016.'
short: '1 Anonymous, 2 Anonymous, 3 Anonymous, Average-Case Analysis of Programs:
Automated Recurrence Analysis for Almost-Linear Bounds, IST Austria, 2016.'
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:23Z
date_published: 2016-07-15T00:00:00Z
date_updated: 2019-08-02T12:38:54Z
day: '15'
ddc:
- '000'
file:
- access_level: closed
content_type: text/plain
creator: dernst
date_created: 2019-05-10T13:32:16Z
date_updated: 2019-05-10T13:32:16Z
file_id: '6406'
file_name: listofauthors.txt
file_size: 281
open_access: 0
relation: main_file
request_a_copy: 0
- access_level: open_access
content_type: application/pdf
creator: dernst
date_created: 2019-05-10T13:32:16Z
date_updated: 2019-05-10T13:32:16Z
file_id: '6407'
file_name: popl2017b.pdf
file_size: 563642
open_access: 1
relation: main_file
success: 1
file_date_updated: 2019-05-10T13:32:16Z
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '619'
status: public
title: 'Average-case analysis of programs: Automated recurrence analysis for almost-linear
bounds'
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5448'
_version: 25
abstract:
- lang: eng
text: "We present a new dynamic partial-order reduction method for stateless model
checking of concurrent programs. A common approach for exploring program behaviors
relies on enumerating the traces of the program, without storing the visited states
(aka stateless exploration). As the number of distinct traces grows exponentially,
dynamic partial-order reduction (DPOR) techniques have been successfully used
to partition the space of traces into equivalence classes (Mazurkiewicz partitioning),
with the goal of exploring only few representative traces from each class.\r\nWe
introduce a new equivalence on traces under sequential consistency semantics,
which we call the observation equivalence. Two traces are observationally equivalent
if every read event observes the same write event in both traces. While the traditional
Mazurkiewicz equivalence is control-centric, our new definition is data-centric.
We show that our observation equivalence is coarser than the Mazurkiewicz equivalence,
and in many cases even exponentially coarser. We devise a DPOR exploration of
the trace space, called data-centric DPOR, based on the observation equivalence.\r\n1.
For acyclic architectures, our algorithm is guaranteed to explore exactly one
representative trace from each observation class, while spending polynomial time
per class. Hence, our algorithm is optimal wrt the observation equivalence, and
in several cases explores exponentially fewer traces than any enumerative method
based on the Mazurkiewicz equivalence.\r\n2. For cyclic architectures, we consider
an equivalence between traces which is finer than the observation equivalence;
but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially
coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence.
\r\nFinally, we perform a basic experimental comparison between the existing Mazurkiewicz-based
DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show
a significant reduction in both running time and the number of explored equivalence
classes."
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: '1'
full_name: Anonymous, 1
last_name: Anonymous
- first_name: '2'
full_name: Anonymous, 2
last_name: Anonymous
- first_name: '3'
full_name: Anonymous, 3
last_name: Anonymous
- first_name: '4'
full_name: Anonymous, 4
last_name: Anonymous
citation:
ama: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. *Data-Centric Dynamic
Partial Order Reduction*. IST Austria; 2016.
apa: Anonymous, 1, Anonymous, 2, Anonymous, 3, & Anonymous, 4. (2016). *Data-centric
dynamic partial order reduction*. IST Austria.
chicago: Anonymous, 1, 2 Anonymous, 3 Anonymous, and 4 Anonymous. *Data-Centric
Dynamic Partial Order Reduction*. IST Austria, 2016.
ieee: 1 Anonymous, 2 Anonymous, 3 Anonymous, and 4 Anonymous, *Data-centric dynamic
partial order reduction*. IST Austria, 2016.
ista: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. 2016. Data-centric dynamic
partial order reduction, IST Austria, 20p.
mla: Anonymous, 1, et al. *Data-Centric Dynamic Partial Order Reduction*. IST
Austria, 2016.
short: 1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, Data-Centric Dynamic
Partial Order Reduction, IST Austria, 2016.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:23Z
date_published: 2016-07-15T00:00:00Z
date_updated: 2019-11-14T08:43:09Z
day: '15'
ddc:
- '000'
external_id:
arxiv:
- '1610.01188'
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:45Z
date_updated: 2018-12-12T11:53:45Z
file_id: '5506'
file_name: IST-2016-620-v1+1_main.pdf
file_size: 538881
open_access: 1
relation: main_file
- access_level: closed
content_type: text/plain
creator: dernst
date_created: 2019-05-10T13:30:40Z
date_updated: 2019-05-10T13:30:40Z
file_id: '6405'
file_name: authornames.txt
file_size: 121
open_access: 0
relation: main_file
request_a_copy: 0
file_date_updated: 2019-05-10T13:30:40Z
language:
- iso: eng
month: '07'
oa_version: Published Version
page: '20'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '620'
related_material:
record:
- id: '5456'
relation: later_version
status: public
status: public
title: Data-centric dynamic partial order reduction
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5449'
_version: 39
abstract:
- lang: eng
text: "The fixation probability is the probability that a new mutant introduced
in a homogeneous population eventually takes over the entire population.\r\nThe
fixation probability is a fundamental quantity of natural selection, and known
to depend on the population structure.\r\nAmplifiers of natural selection are
population structures which increase the fixation probability of advantageous
mutants, as compared to the baseline case of well-mixed populations. In this work
we focus on symmetric population structures represented as undirected graphs.
In the regime of undirected graphs, the strongest amplifier known has been the
Star graph, and the existence of undirected graphs with stronger amplification
properties has remained open for over a decade.\r\nIn this work we present the
Comet and Comet-swarm families of undirected graphs. We show that for a range
of fitness values of the mutants, the Comet and Comet-swarm graphs have fixation
probability strictly larger than the fixation probability of the Star graph, for
fixed population size and at the limit of large populations, respectively."
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: 'Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. *Amplification on Undirected
Population Structures: Comets Beat Stars*. IST Austria; 2016. doi:10.15479/AT:IST-2016-648-v1-1'
apa: 'Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). *Amplification
on undirected population structures: Comets beat stars*. IST Austria. https://doi.org/10.15479/AT:IST-2016-648-v1-1'
chicago: 'Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. *Amplification on Undirected Population Structures: Comets Beat Stars*.
IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-648-v1-1.'
ieee: 'A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, *Amplification
on undirected population structures: Comets beat stars*. IST Austria, 2016.'
ista: 'Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Amplification on
undirected population structures: Comets beat stars, IST Austria, 22p.'
mla: 'Pavlogiannis, Andreas, et al. *Amplification on Undirected Population Structures:
Comets Beat Stars*. IST Austria, 2016, doi:10.15479/AT:IST-2016-648-v1-1.'
short: 'A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Amplification on Undirected
Population Structures: Comets Beat Stars, IST Austria, 2016.'
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:24Z
date_published: 2016-11-09T00:00:00Z
date_updated: 2019-11-14T08:43:08Z
day: '09'
ddc:
- '519'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2016-648-v1-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:07Z
date_updated: 2018-12-12T11:54:07Z
file_id: '5529'
file_name: IST-2016-648-v1+1_tr.pdf
file_size: 1264221
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:54:07Z
language:
- iso: eng
month: '11'
oa: 1
oa_version: Updated Version
page: '22'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '648'
related_material:
record:
- id: '512'
relation: research_paper
status: public
status: public
title: 'Amplification on undirected population structures: Comets beat stars'
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5451'
_version: 11
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. *Strong Amplifiers of Natural
Selection*. IST Austria; 2016. doi:10.15479/AT:IST-2016-728-v1-1
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). *Strong
amplifiers of natural selection*. IST Austria. https://doi.org/10.15479/AT:IST-2016-728-v1-1
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. *Strong Amplifiers of Natural Selection*. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-728-v1-1.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, *Strong amplifiers
of natural selection*. IST Austria, 2016.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Strong amplifiers
of natural selection, IST Austria, 34p.
mla: Pavlogiannis, Andreas, et al. *Strong Amplifiers of Natural Selection*.
IST Austria, 2016, doi:10.15479/AT:IST-2016-728-v1-1.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Strong Amplifiers of
Natural Selection, IST Austria, 2016.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:24Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2019-08-02T12:38:55Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2016-728-v1-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:04Z
date_updated: 2018-12-12T11:53:04Z
file_id: '5465'
file_name: IST-2016-728-v1+1_main.pdf
file_size: 1014732
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:53:04Z
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '34'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '728'
status: public
title: Strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5445'
_version: 19
abstract:
- lang: eng
text: 'We consider the quantitative analysis problem for interprocedural control-flow
graphs (ICFGs). The input consists of an ICFG, a positive weight function that
assigns every transition a positive integer-valued number, and a labelling of
the transitions (events) as good, bad, and neutral events. The weight function
assigns to each transition a numerical value that represents ameasure of how good
or bad an event is. The quantitative analysis problem asks whether there is a
run of the ICFG where the ratio of the sum of the numerical weights of good events
versus the sum of weights of bad events in the long-run is at least a given threshold
(or equivalently, to compute the maximal ratio among all valid paths in the ICFG).
The quantitative analysis problem for ICFGs can be solved in polynomial time,
and we present an efficient and practical algorithm for the problem. We show that
several problems relevant for static program analysis, such as estimating the
worst-case execution time of a program or the average energy consumption of a
mobile application, can be modeled in our framework. We have implemented our algorithm
as a tool in the Java Soot framework. We demonstrate the effectiveness of our
approach with two case studies. First, we show that our framework provides a sound
approach (no false positives) for the analysis of inefficiently-used containers.
Second, we show that our approach can also be used for static profiling of programs
which reasons about methods that are frequently invoked. Our experimental results
show that our tool scales to relatively large benchmarks, and discovers relevant
and useful information that can be used to optimize performance of the programs. '
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Pavlogiannis A, Velner Y. *Quantitative Interprocedural Analysis*.
IST Austria; 2016. doi:10.15479/AT:IST-2016-523-v1-1
apa: Chatterjee, K., Pavlogiannis, A., & Velner, Y. (2016). *Quantitative
interprocedural analysis*. IST Austria. https://doi.org/10.15479/AT:IST-2016-523-v1-1
chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. *Quantitative
Interprocedural Analysis*. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-523-v1-1.
ieee: K. Chatterjee, A. Pavlogiannis, and Y. Velner, *Quantitative interprocedural
analysis*. IST Austria, 2016.
ista: Chatterjee K, Pavlogiannis A, Velner Y. 2016. Quantitative interprocedural
analysis, IST Austria, 33p.
mla: Chatterjee, Krishnendu, et al. *Quantitative Interprocedural Analysis*.
IST Austria, 2016, doi:10.15479/AT:IST-2016-523-v1-1.
short: K. Chatterjee, A. Pavlogiannis, Y. Velner, Quantitative Interprocedural Analysis,
IST Austria, 2016.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:22Z
date_published: 2016-03-31T00:00:00Z
date_updated: 2019-11-14T08:43:08Z
day: '31'
ddc:
- '005'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2016-523-v1-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:52Z
date_updated: 2018-12-12T11:53:52Z
file_id: '5513'
file_name: IST-2016-523-v1+1_main.pdf
file_size: 1012204
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:53:52Z
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '523'
related_material:
record:
- id: '1604'
relation: later_version
status: public
status: public
title: Quantitative interprocedural analysis
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5452'
_version: 31
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. *Arbitrarily Strong Amplifiers
of Natural Selection*. IST Austria; 2016. doi:10.15479/AT:IST-2017-728-v2-1
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). *Arbitrarily
strong amplifiers of natural selection*. IST Austria. https://doi.org/10.15479/AT:IST-2017-728-v2-1
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. *Arbitrarily Strong Amplifiers of Natural Selection*. IST Austria,
2016. https://doi.org/10.15479/AT:IST-2017-728-v2-1.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, *Arbitrarily strong
amplifiers of natural selection*. IST Austria, 2016.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong
amplifiers of natural selection, IST Austria, 32p.
mla: Pavlogiannis, Andreas, et al. *Arbitrarily Strong Amplifiers of Natural Selection*.
IST Austria, 2016, doi:10.15479/AT:IST-2017-728-v2-1.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong
Amplifiers of Natural Selection, IST Austria, 2016.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:25Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2019-11-14T08:43:11Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2017-728-v2-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:52:59Z
date_updated: 2018-12-12T11:52:59Z
file_id: '5460'
file_name: IST-2017-728-v2+1_main.pdf
file_size: 811558
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:52:59Z
language:
- iso: eng
month: '12'
oa_version: Published Version
page: '32'
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '750'
related_material:
record:
- id: '5453'
relation: later_version
status: public
- id: '5559'
relation: popular_science
status: public
status: public
title: Arbitrarily strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5446'
_version: 14
abstract:
- lang: eng
text: "We study the problem of developing efficient approaches for proving termination
of recursive programs with one-dimensional arrays. Ranking functions serve as
a sound and complete approach for proving termination of non-recursive programs
without array operations. First, we generalize ranking functions to the notion
of measure functions, and prove that measure functions (i) provide a sound method
to prove termination of recursive programs (with one-dimensional arrays), and
(ii) is both sound and complete over recursive programs without array operations.
Our second contribution is the synthesis of measure functions of specific forms
in polynomial time. More precisely, we prove that (i) polynomial measure functions
over recursive programs can be synthesized in polynomial time through Farkas’
Lemma and Handelman’s Theorem, and (ii) measure functions involving logarithm
and exponentiation can be synthesized in polynomial time through abstraction of
logarithmic or exponential terms and Handelman’s Theorem. A key application of
our method is the worst-case analysis of recursive programs. While previous methods
obtain worst-case polynomial bounds of the form O(n^k), where k is an integer,
our polynomial time methods can synthesize bounds of the form O(n log n), as well
as O(n^x), where x is not an integer. We show the applicability of our automated
technique to obtain worst-case complexity of classical recursive algorithms such
as (i) Merge-Sort, the divideand-\r\nconquer algorithm for the Closest-Pair problem,
where we obtain O(n log n) worst-case bound, and (ii) Karatsuba’s algorithm for
polynomial multiplication and Strassen’s algorithm for matrix multiplication,
where we obtain O(n^x) bound, where x is not an integer and close to the best-known
bounds for the respective algorithms. Finally, we present experimental results
to demonstrate the\r\neffectiveness of our approach."
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: '1'
full_name: Anonymous, 1
last_name: Anonymous
- first_name: '2'
full_name: Anonymous, 2
last_name: Anonymous
- first_name: '3'
full_name: Anonymous, 3
last_name: Anonymous
citation:
ama: Anonymous 1, Anonymous 2, Anonymous 3. *Termination and Worst-Case Analysis
of Recursive Programs*. IST Austria; 2016.
apa: Anonymous, 1, Anonymous, 2, & Anonymous, 3. (2016). *Termination and
worst-case analysis of recursive programs*. IST Austria.
chicago: Anonymous, 1, 2 Anonymous, and 3 Anonymous. *Termination and Worst-Case
Analysis of Recursive Programs*. IST Austria, 2016.
ieee: 1 Anonymous, 2 Anonymous, and 3 Anonymous, *Termination and worst-case analysis
of recursive programs*. IST Austria, 2016.
ista: Anonymous 1, Anonymous 2, Anonymous 3. 2016. Termination and worst-case analysis
of recursive programs, IST Austria, 26p.
mla: Anonymous, 1, et al. *Termination and Worst-Case Analysis of Recursive Programs*.
IST Austria, 2016.
short: 1 Anonymous, 2 Anonymous, 3 Anonymous, Termination and Worst-Case Analysis
of Recursive Programs, IST Austria, 2016.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:23Z
date_published: 2016-07-15T00:00:00Z
date_updated: 2019-08-02T12:38:54Z
day: '15'
ddc:
- '000'
file:
- access_level: open_access
content_type: application/pdf
creator: dernst
date_created: 2019-05-10T13:27:24Z
date_updated: 2019-05-10T13:27:24Z
file_id: '6403'
file_name: popl2017a.pdf
file_size: 686241
open_access: 1
relation: main_file
success: 1
- access_level: closed
content_type: text/plain
creator: dernst
date_created: 2019-05-10T13:27:31Z
date_updated: 2019-05-10T13:27:31Z
file_id: '6404'
file_name: author_names.txt
file_size: 258
open_access: 0
relation: main_file
request_a_copy: 0
file_date_updated: 2019-05-10T13:27:31Z
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '26'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '618'
status: public
title: Termination and worst-case analysis of recursive programs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5453'
_version: 29
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. *Arbitrarily Strong Amplifiers
of Natural Selection*. IST Austria; 2016. doi:10.15479/AT:IST-2017-749-v3-1
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). *Arbitrarily
strong amplifiers of natural selection*. IST Austria. https://doi.org/10.15479/AT:IST-2017-749-v3-1
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. *Arbitrarily Strong Amplifiers of Natural Selection*. IST Austria,
2016. https://doi.org/10.15479/AT:IST-2017-749-v3-1.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, *Arbitrarily strong
amplifiers of natural selection*. IST Austria, 2016.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong
amplifiers of natural selection, IST Austria, 34p.
mla: Pavlogiannis, Andreas, et al. *Arbitrarily Strong Amplifiers of Natural Selection*.
IST Austria, 2016, doi:10.15479/AT:IST-2017-749-v3-1.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong
Amplifiers of Natural Selection, IST Austria, 2016.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:25Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2019-11-14T08:43:09Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2017-749-v3-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:13Z
date_updated: 2018-12-12T11:53:13Z
file_id: '5474'
file_name: IST-2017-749-v3+1_main.pdf
file_size: 1015647
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:53:13Z
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '34'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '755'
related_material:
record:
- id: '5452'
relation: earlier_version
status: public
status: public
title: Arbitrarily strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5430'
_version: 31
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
property, the ratio property, 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 constant treewidth, and it is well-known that the control-flow
graphs of most programs have constant treewidth. Let n denote the number of nodes
of a graph, m the number of edges (for constant treewidth graphs m = O ( n ) )
and W the largest absolute value of the weights. Our main theoretical results
are as follows. First, for constant treewidth graphs we present an algorithm that
approximates the mean-payoff value within a mul- tiplicative factor of ∊ in time
O ( n · log( n/∊ )) and linear space, as compared to the classical algorithms
that require quadratic time. Second, for the ratio property we present an algorithm
that for constant treewidth graphs works in time O ( n · log( | a · b · n | ))
= O ( n · log( n · W )) , when the output is a b , as compared to the previously
best known algorithm with running time O ( n 2 · log( n · W )) . Third, for the
minimum initial credit problem we show that (i) for general graphs the problem
can be solved in O ( n 2 · m ) time and the associated decision problem can be
solved in O ( n · m ) time, improving the previous known O ( n 3 · m · log( n
· W )) and O ( n 2 · m ) bounds, respectively; and (ii) for constant treewidth
graphs we present an algorithm that requires O ( n · log n ) time, improving the
previous known O ( n 4 · log( n · W )) bound. We have implemented some of our
algorithms and show that they present a significant speedup on standard benchmarks.
accept: '1'
alternative_title:
- IST Austria Technical Report
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
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
citation:
ama: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. *Faster Algorithms for Quantitative
Verification in Constant Treewidth Graphs*. IST Austria; 2015. doi:10.15479/AT:IST-2015-319-v1-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). *Faster
algorithms for quantitative verification in constant treewidth graphs*. IST
Austria. https://doi.org/10.15479/AT:IST-2015-319-v1-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
*Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs*.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-319-v1-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, *Faster algorithms
for quantitative verification in constant treewidth graphs*. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for
quantitative verification in constant treewidth graphs, IST Austria, 31p.
mla: Chatterjee, Krishnendu, et al. *Faster Algorithms for Quantitative Verification
in Constant Treewidth Graphs*. IST Austria, 2015, doi:10.15479/AT:IST-2015-319-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative
Verification in Constant Treewidth Graphs, IST Austria, 2015.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:17Z
date_published: 2015-02-10T00:00:00Z
date_updated: 2019-11-14T08:43:05Z
day: '10'
ddc:
- '000'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2015-319-v1-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:21Z
date_updated: 2018-12-12T11:53:21Z
file_id: '5482'
file_name: IST-2015-319-v1+1_long.pdf
file_size: 1089651
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:53:21Z
language:
- iso: eng
month: '02'
oa_version: Published Version
page: '31'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '319'
related_material:
record:
- id: '1607'
relation: later_version
status: public
- id: '5437'
relation: later_version
status: public
status: public
title: Faster algorithms for quantitative verification in constant treewidth graphs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5435'
_version: 44
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) with multiple limit-average
(or mean-payoff) objectives. \r\nThere have been two different views: (i) the
expectation semantics, where the goal is to optimize the expected mean-payoff
objective, and (ii) the satisfaction semantics, where the goal is to maximize
the probability of runs such that the mean-payoff value stays above a given vector.
\ \r\nWe consider the problem where the goal is to optimize the expectation under
the constraint that the satisfaction semantics is ensured, and thus consider a
generalization that unifies the existing semantics. Our problem captures the notion
of optimization with respect to strategies that are risk-averse (i.e., ensures
certain probabilistic guarantee).\r\nOur main results are algorithms for the decision
problem which are always polynomial in the size of the MDP.\r\nWe also show that
an approximation of the Pareto-curve can be computed in time polynomial in the
size of the MDP, and the approximation factor, but exponential in the number of
dimensions. Finally, we present a complete characterization of the strategy complexity
(in terms of memory bounds and randomization) required to solve our problem."
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Zuzana
full_name: Komarkova, Zuzana
last_name: Komarkova
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Komarkova Z, Kretinsky J. *Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes*. IST Austria; 2015. doi:10.15479/AT:IST-2015-318-v2-1
apa: Chatterjee, K., Komarkova, Z., & Kretinsky, J. (2015). *Unifying two
views on multiple mean-payoff objectives in Markov decision processes*. IST
Austria. https://doi.org/10.15479/AT:IST-2015-318-v2-1
chicago: Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. *Unifying
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes*.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-318-v2-1.
ieee: K. Chatterjee, Z. Komarkova, and J. Kretinsky, *Unifying two views on multiple
mean-payoff objectives in Markov decision processes*. IST Austria, 2015.
ista: Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple
mean-payoff objectives in Markov decision processes, IST Austria, 51p.
mla: Chatterjee, Krishnendu, et al. *Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes*. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v2-1.
short: K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple
Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:19Z
date_published: 2015-02-23T00:00:00Z
date_updated: 2019-11-14T08:43:05Z
day: '23'
ddc:
- '004'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2015-318-v2-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:03Z
date_updated: 2018-12-12T11:54:03Z
file_id: '5525'
file_name: IST-2015-318-v2+1_main.pdf
file_size: 717630
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:54:03Z
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '51'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '327'
related_material:
record:
- id: '1657'
relation: later_version
status: public
- id: '5429'
relation: earlier_version
status: public
- id: '466'
relation: later_version
status: public
status: public
title: Unifying two views on multiple mean-payoff objectives in Markov decision processes
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5442'
_version: 32
abstract:
- lang: eng
text: "We study algorithmic questions for concurrent systems where the transitions
are labeled from a complete, closed semiring, and path properties are algebraic
with semiring operations. The algebraic path properties can model dataflow analysis
problems, the shortest path problem, and many other natural properties that arise
in program analysis.\r\nWe consider that each component of the concurrent system
is a graph with constant treewidth, and it is known that the controlflow graphs
of most programs have constant treewidth. We allow for multiple possible queries,
which arise naturally in demand driven dataflow analysis problems (e.g., alias
analysis). The study of multiple queries allows us to consider the tradeoff between
the resource usage of the \\emph{one-time} preprocessing and for \\emph{each individual}
query. The traditional approaches construct the product graph of all components
and apply the best-known graph algorithm on the product. In the traditional approach,
even the answer to a single query requires the transitive closure computation
(i.e., the results of all possible queries), which provides no room for tradeoff
between preprocessing and query time.\r\n\r\nOur main contributions are algorithms
that significantly improve the worst-case running time of the traditional approach,
and provide various tradeoffs depending on the number of queries. For example,
in a concurrent system of two components, the traditional approach requires hexic
time in the worst case for answering one query as well as computing the transitive
closure, whereas we show that with one-time preprocessing in almost cubic time,
\r\neach subsequent query can be answered in at most linear time, and even the
transitive closure can be computed in almost quartic time. Furthermore, we establish
conditional optimality results that show that the worst-case running times of
our algorithms cannot be improved without achieving major breakthroughs in graph
algorithms (such as improving \r\nthe worst-case bounds for the shortest path
problem in general graphs whose current best-known bound has not been improved
in five decades). Finally, we provide a prototype implementation of our algorithms
which significantly outperforms the existing algorithmic methods on several benchmarks."
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: '1'
full_name: Anonymous, 1
last_name: Anonymous
- first_name: '2'
full_name: Anonymous, 2
last_name: Anonymous
- first_name: '3'
full_name: Anonymous, 3
last_name: Anonymous
- first_name: '4'
full_name: Anonymous, 4
last_name: Anonymous
citation:
ama: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. *Algorithms for Algebraic
Path Properties in Concurrent Systems of Constant Treewidth Components*. IST
Austria; 2015.
apa: Anonymous, 1, Anonymous, 2, Anonymous, 3, & Anonymous, 4. (2015). *Algorithms
for algebraic path properties in concurrent systems of constant treewidth components*.
IST Austria.
chicago: Anonymous, 1, 2 Anonymous, 3 Anonymous, and 4 Anonymous. *Algorithms
for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components*.
IST Austria, 2015.
ieee: 1 Anonymous, 2 Anonymous, 3 Anonymous, and 4 Anonymous, *Algorithms for
algebraic path properties in concurrent systems of constant treewidth components*.
IST Austria, 2015.
ista: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. 2015. Algorithms for algebraic
path properties in concurrent systems of constant treewidth components, IST Austria,
22p.
mla: Anonymous, 1, et al. *Algorithms for Algebraic Path Properties in Concurrent
Systems of Constant Treewidth Components*. IST Austria, 2015.
short: 1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, Algorithms for Algebraic
Path Properties in Concurrent Systems of Constant Treewidth Components, IST Austria,
2015.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:21Z
date_published: 2015-07-14T00:00:00Z
date_updated: 2019-11-14T08:43:07Z
day: '14'
ddc:
- '000'
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:37Z
date_updated: 2018-12-12T11:53:37Z
file_id: '5498'
file_name: IST-2015-343-v2+1_main.pdf
file_size: 658747
open_access: 1
relation: main_file
- access_level: closed
content_type: text/plain
creator: dernst
date_created: 2019-04-16T12:36:08Z
date_updated: 2019-04-16T14:42:18Z
file_id: '6316'
file_name: IST-2015-343-v2+2_anonymous.txt
file_size: 139
open_access: 0
relation: main_file
request_a_copy: 0
file_date_updated: 2019-04-16T14:42:18Z
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '22'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '344'
related_material:
record:
- id: '1437'
relation: later_version
status: public
- id: '5441'
relation: later_version
status: public
status: public
title: Algorithms for algebraic path properties in concurrent systems of constant
treewidth components
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5429'
_version: 44
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) with multiple limit-average
(or mean-payoff) objectives. \r\nThere have been two different views: (i) the
expectation semantics, where the goal is to optimize the expected mean-payoff
objective, and (ii) the satisfaction semantics, where the goal is to maximize
the probability of runs such that the mean-payoff value stays above a given vector.
\ \r\nWe consider the problem where the goal is to optimize the expectation under
the constraint that the satisfaction semantics is ensured, and thus consider a
generalization that unifies the existing semantics.\r\nOur problem captures the
notion of optimization with respect to strategies that are risk-averse (i.e.,
ensures certain probabilistic guarantee).\r\nOur main results are algorithms for
the decision problem which are always polynomial in the size of the MDP. We also
show that an approximation of the Pareto-curve can be computed in time polynomial
in the size of the MDP, and the approximation factor, but exponential in the number
of dimensions.\r\nFinally, we present a complete characterization of the strategy
complexity (in terms of memory bounds and randomization) required to solve our
problem."
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Zuzana
full_name: Komarkova, Zuzana
last_name: Komarkova
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Komarkova Z, Kretinsky J. *Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes*. IST Austria; 2015. doi:10.15479/AT:IST-2015-318-v1-1
apa: Chatterjee, K., Komarkova, Z., & Kretinsky, J. (2015). *Unifying two
views on multiple mean-payoff objectives in Markov decision processes*. IST
Austria. https://doi.org/10.15479/AT:IST-2015-318-v1-1
chicago: Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. *Unifying
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes*.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-318-v1-1.
ieee: K. Chatterjee, Z. Komarkova, and J. Kretinsky, *Unifying two views on multiple
mean-payoff objectives in Markov decision processes*. IST Austria, 2015.
ista: Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple
mean-payoff objectives in Markov decision processes, IST Austria, 41p.
mla: Chatterjee, Krishnendu, et al. *Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes*. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v1-1.
short: K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple
Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:17Z
date_published: 2015-01-12T00:00:00Z
date_updated: 2019-11-14T08:43:05Z
day: '12'
ddc:
- '004'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2015-318-v1-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:11Z
date_updated: 2018-12-12T11:54:11Z
file_id: '5533'
file_name: IST-2015-318-v1+1_main.pdf
file_size: 689863
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:54:11Z
language:
- iso: eng
month: '01'
oa_version: Published Version
page: '41'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '318'
related_material:
record:
- id: '1657'
relation: later_version
status: public
- id: '466'
relation: later_version
status: public
- id: '5435'
relation: later_version
status: public
status: public
title: Unifying two views on multiple mean-payoff objectives in Markov decision processes
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5443'
_version: 25
abstract:
- lang: eng
text: POMDPs are standard models for probabilistic planning problems, where an agent
interacts with an uncertain environment. We study the problem of almost-sure reachability,
where given a set of target states, the question is to decide whether there is
a policy to ensure that the target set is reached with probability 1 (almost-surely).
While in general the problem is EXPTIME-complete, in many practical cases policies
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. In this work, 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.
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Jessica
full_name: Davies, Jessica
id: 378E0060-F248-11E8-B48F-1D18A9856A87
last_name: Davies
citation:
ama: Chatterjee K, Chmelik M, Davies J. *A Symbolic SAT-Based Algorithm for Almost-Sure
Reachability with Small Strategies in POMDPs*. IST Austria; 2015. doi:10.15479/AT:IST-2015-325-v2-1
apa: Chatterjee, K., Chmelik, M., & Davies, J. (2015). *A symbolic SAT-based
algorithm for almost-sure reachability with small strategies in POMDPs*. IST
Austria. https://doi.org/10.15479/AT:IST-2015-325-v2-1
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. *A Symbolic
SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs*.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-325-v2-1.
ieee: K. Chatterjee, M. Chmelik, and J. Davies, *A symbolic SAT-based algorithm
for almost-sure reachability with small strategies in POMDPs*. IST Austria,
2015.
ista: Chatterjee K, Chmelik M, Davies J. 2015. A symbolic SAT-based algorithm for
almost-sure reachability with small strategies in POMDPs, IST Austria, 23p.
mla: Chatterjee, Krishnendu, et al. *A Symbolic SAT-Based Algorithm for Almost-Sure
Reachability with Small Strategies in POMDPs*. IST Austria, 2015, doi:10.15479/AT:IST-2015-325-v2-1.
short: K. Chatterjee, M. Chmelik, J. Davies, A Symbolic SAT-Based Algorithm for
Almost-Sure Reachability with Small Strategies in POMDPs, IST Austria, 2015.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:22Z
date_published: 2015-11-06T00:00:00Z
date_updated: 2019-11-14T08:43:08Z
day: '06'
ddc:
- '000'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2015-325-v2-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:05Z
date_updated: 2018-12-12T11:53:05Z
file_id: '5466'
file_name: IST-2015-325-v2+1_main.pdf
file_size: 412379
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:53:05Z
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: '23'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '362'
related_material:
record:
- id: '1166'
relation: later_version
status: public
status: public
title: A symbolic SAT-based algorithm for almost-sure reachability with small strategies
in POMDPs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5431'
_version: 11
abstract:
- lang: eng
text: "We consider finite-state concurrent stochastic games, played by k>=2 players
for an infinite number of rounds, where in every round, each player simultaneously
and independently of the other players chooses an action, whereafter the successor
state is determined by a probability distribution given by the current state and
the chosen actions. We consider reachability objectives that given a target set
of states require that some state in the target set is visited, and the dual safety
objectives that given a target set require that only states in the target set
are visited. We are interested in the complexity of stationary strategies measured
by their patience, which is defined as the inverse of the smallest non-zero probability
employed.\r\n\r\n Our main results are as follows: We show that in two-player
zero-sum concurrent stochastic games (with reachability objective for one player
and the complementary safety objective for the other player): (i) the optimal
bound on the patience of optimal and epsilon-optimal strategies, for both players
is doubly exponential; and (ii) even in games with a single non-absorbing state
exponential (in the number of actions) patience is necessary. In general we study
the class of non-zero-sum games admitting epsilon-Nash equilibria. We show that
if there is at least one player with reachability objective, then doubly-exponential
patience is needed in general for epsilon-Nash equilibrium strategies, whereas
in contrast if all players have safety objectives, then the optimal bound on patience
for epsilon-Nash equilibrium strategies is only exponential."
accept: '1'
alternative_title:
- IST Austria Technical Report
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
- first_name: Kristoffer
full_name: Hansen, Kristoffer
last_name: Hansen
citation:
ama: Chatterjee K, Ibsen-Jensen R, Hansen K. *The Patience of Concurrent Stochastic
Games with Safety and Reachability Objectives*. IST Austria; 2015. doi:10.15479/AT:IST-2015-322-v1-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Hansen, K. (2015). *The patience
of concurrent stochastic games with safety and reachability objectives*. IST
Austria. https://doi.org/10.15479/AT:IST-2015-322-v1-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Kristoffer Hansen. *The
Patience of Concurrent Stochastic Games with Safety and Reachability Objectives*.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-322-v1-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and K. Hansen, *The patience of concurrent
stochastic games with safety and reachability objectives*. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Hansen K. 2015. The patience of concurrent stochastic
games with safety and reachability objectives, IST Austria, 25p.
mla: Chatterjee, Krishnendu, et al. *The Patience of Concurrent Stochastic Games
with Safety and Reachability Objectives*. IST Austria, 2015, doi:10.15479/AT:IST-2015-322-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, K. Hansen, The Patience of Concurrent Stochastic
Games with Safety and Reachability Objectives, IST Austria, 2015.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:17Z
date_published: 2015-02-19T00:00:00Z
date_updated: 2019-08-02T12:38:51Z
day: '19'
ddc:
- '005'
- '519'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2015-322-v1-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:31Z
date_updated: 2018-12-12T11:53:31Z
file_id: '5491'
file_name: IST-2015-322-v1+1_safetygames.pdf
file_size: 661015
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:53:31Z
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '25'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '322'
status: public
title: The patience of concurrent stochastic games with safety and reachability objectives
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5436'
_version: 59
abstract:
- lang: eng
text: "Recently there has been a significant effort to handle quantitative properties
in formal verification and synthesis. While weighted automata over finite and
infinite words provide a natural and flexible framework to express quantitative
properties, perhaps surprisingly, some basic system properties such as average
response time cannot be expressed using weighted automata, nor in any other know
decidable formalism. In this work, we introduce nested weighted automata as a
natural extension of weighted automata which makes it possible to express important
quantitative properties such as average response time.\r\nIn nested weighted automata,
a master automaton spins off and collects results from weighted slave automata,
each of which computes a quantity along a finite portion of an infinite word.
Nested weighted automata can be viewed as the quantitative analogue of monitor
automata, which are used in run-time verification. We establish an almost complete
decidability picture for the basic decision problems about nested weighted automata,
and illustrate their applicability in several domains. In particular, nested weighted
automata can be used to decide average response time properties."
accept: '1'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Otop J. *Nested Weighted Automata*. IST Austria;
2015. doi:10.15479/AT:IST-2015-170-v2-2
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2015). *Nested weighted
automata*. IST Austria. https://doi.org/10.15479/AT:IST-2015-170-v2-2
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. *Nested Weighted
Automata*. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-170-v2-2.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, *Nested weighted automata*.
IST Austria, 2015.
ista: Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata, IST Austria,
29p.
mla: Chatterjee, Krishnendu, et al. *Nested Weighted Automata*. IST Austria,
2015, doi:10.15479/AT:IST-2015-170-v2-2.
short: K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria,
2015.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:19Z
date_published: 2015-04-24T00:00:00Z
date_updated: 2019-11-14T08:43:05Z
day: '24'
ddc:
- '000'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
- _id: ToHe
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2015-170-v2-2
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:19Z
date_updated: 2018-12-12T11:54:19Z
file_id: '5541'
file_name: IST-2015-170-v2+2_report.pdf
file_size: 569991
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:54:19Z
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '29'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '331'
related_material:
record:
- id: '1656'
relation: later_version
status: public
- id: '5415'
relation: earlier_version
status: public
- id: '467'
relation: later_version
status: public
status: public
title: Nested weighted automata
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5437'
_version: 33
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
property, the ratio property, and the minimum initial credit for energy property.
\r\nThe 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 constant treewidth, and it is well-known
that the control-flow graphs of most programs have constant treewidth. Let $n$
denote the number of nodes of a graph, $m$ the number of edges (for constant treewidth
graphs $m=O(n)$) and $W$ the largest absolute value of the weights.\r\nOur main
theoretical results are as follows.\r\nFirst, for constant treewidth graphs we
present an algorithm that approximates the mean-payoff value within a multiplicative
factor of $\\epsilon$ in time $O(n \\cdot \\log (n/\\epsilon))$ and linear space,
as compared to the classical algorithms that require quadratic time. Second, for
the ratio property we present an algorithm that for constant treewidth graphs
works in time $O(n \\cdot \\log (|a\\cdot b|))=O(n\\cdot\\log (n\\cdot W))$, when
the output is $\\frac{a}{b}$, as compared to the previously best known algorithm
with running time $O(n^2 \\cdot \\log (n\\cdot W))$. Third, for the minimum initial
credit problem we show that (i)~for general graphs the problem can be solved in
$O(n^2\\cdot m)$ time and the associated decision problem can be solved in $O(n\\cdot
m)$ time, improving the previous known $O(n^3\\cdot m\\cdot \\log (n\\cdot W))$
and $O(n^2 \\cdot m)$ bounds, respectively; and (ii)~for constant treewidth graphs
we present an algorithm that requires $O(n\\cdot \\log n)$ time, improving the
previous known $O(n^4 \\cdot \\log (n \\cdot W))$ bound.\r\nWe have implemented
some of our algorithms and show that they present a significant speedup on standard
benchmarks. "
accept: '1'
alternative_title:
- IST Austria Technical Report
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
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
citation:
ama: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. *Faster Algorithms for Quantitative
Verification in Constant Treewidth Graphs*. IST Austria; 2015. doi:10.15479/AT:IST-2015-330-v2-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). *Faster
algorithms for quantitative verification in constant treewidth graphs*. IST
Austria. https://doi.org/10.15479/AT:IST-2015-330-v2-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
*Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs*.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-330-v2-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, *Faster algorithms
for quantitative verification in constant treewidth graphs*. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for
quantitative verification in constant treewidth graphs, IST Austria, 27p.
mla: Chatterjee, Krishnendu, et al. *Faster Algorithms for Quantitative Verification
in Constant Treewidth Graphs*. IST Austria, 2015, doi:10.15479/AT:IST-2015-330-v2-1.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative
Verification in Constant Treewidth Graphs, IST Austria, 2015.
creator:
id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
login: dernst
date_created: 2018-12-12T11:39:19Z
date_published: 2015-04-27T00:00:00Z
date_updated: 2019-11-14T08:43:05Z
day: '27'
ddc:
- '000'
department:
- _id: KrCh
tree:
- _id: ResearchGroups
- _id: IST
doi: 10.15479/AT:IST-2015-330-v2-1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:12Z
date_updated: 2018-12-12T11:53:12Z
file_id: '5473'
file_name: IST-2015-330-v2+1_main.pdf
file_size: 1072137
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T11:53:12Z
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '27'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '333'
related_material:
record:
- id: '1607'
relation: later_version
status: public
- id: '5430'
relation: earlier_version
status: public
status: public
title: Faster algorithms for quantitative verification in constant treewidth graphs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...