---
_id: '512'
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. The fixation
probability is a fundamental quantity of natural selection, and known to depend
on the population structure. Amplifiers 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. In 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 Cometswarm 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. '
article_number: '82'
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
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- 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. Scientific Reports. 2017;7(1).
doi:10.1038/s41598-017-00107-w'
apa: 'Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2017). Amplification
on undirected population structures: Comets beat stars. Scientific Reports.
Nature Publishing Group. https://doi.org/10.1038/s41598-017-00107-w'
chicago: 'Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. “Amplification on Undirected Population Structures: Comets Beat Stars.”
Scientific Reports. Nature Publishing Group, 2017. https://doi.org/10.1038/s41598-017-00107-w.'
ieee: 'A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, “Amplification
on undirected population structures: Comets beat stars,” Scientific Reports,
vol. 7, no. 1. Nature Publishing Group, 2017.'
ista: 'Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Amplification on
undirected population structures: Comets beat stars. Scientific Reports. 7(1),
82.'
mla: 'Pavlogiannis, Andreas, et al. “Amplification on Undirected Population Structures:
Comets Beat Stars.” Scientific Reports, vol. 7, no. 1, 82, Nature Publishing
Group, 2017, doi:10.1038/s41598-017-00107-w.'
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Scientific Reports
7 (2017).
date_created: 2018-12-11T11:46:53Z
date_published: 2017-03-06T00:00:00Z
date_updated: 2023-02-23T12:26:57Z
day: '06'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.1038/s41598-017-00107-w
ec_funded: 1
file:
- access_level: open_access
checksum: 7d05cbdd914e194a019c0f91fb64e9a8
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:35Z
date_updated: 2020-07-14T12:46:36Z
file_id: '5357'
file_name: IST-2018-938-v1+1_2017_Pavlogiannis_Amplification_on.pdf
file_size: 1536783
relation: main_file
file_date_updated: 2020-07-14T12:46:36Z
has_accepted_license: '1'
intvolume: ' 7'
issue: '1'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Scientific Reports
publication_identifier:
issn:
- '20452322'
publication_status: published
publisher: Nature Publishing Group
publist_id: '7307'
pubrep_id: '938'
quality_controlled: '1'
related_material:
record:
- id: '5449'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: 'Amplification on undirected population structures: Comets beat stars'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7
year: '2017'
...
---
_id: '10416'
abstract:
- lang: eng
text: 'A fundamental algorithmic problem at the heart of static analysis is Dyck
reachability. The input is a graph where the edges are labeled with different
types of opening and closing parentheses, and the reachability information is
computed via paths whose parentheses are properly matched. We present new results
for Dyck reachability 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 as follows: First, we consider
Dyck reachability on bidirected graphs, which is the standard way of performing
field-sensitive points-to analysis. Given a bidirected graph with n nodes and
m edges, we present: (i) an algorithm with worst-case running time O(m + n · α(n)),
where α(n) is the inverse Ackermann function, improving the previously known O(n2)
time bound; (ii) a matching lower bound that shows that our algorithm is optimal
wrt to worst-case complexity; and (iii) an optimal average-case upper bound of
O(m) time, improving the previously known O(m · logn) bound. Second, we consider
the problem of context-sensitive data-dependence analysis, where the task is to
obtain analysis summaries of library code in the presence of callbacks. Our algorithm
preprocesses libraries in almost linear 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 Matrix Multiplication,
which is a long-standing open problem. Thus we establish that the existing combinatorial
algorithms for Dyck reachability are (conditionally) optimal for general graphs.
We also show that the same hardness holds for graphs of constant treewidth. Finally,
we provide a prototype implementation of our algorithms for both alias analysis
and data-dependence analysis. Our experimental evaluation demonstrates that the
new algorithms significantly outperform all existing methods on the two problems,
over real-world benchmarks.'
acknowledgement: "The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Start grant
(279307: Graph Games).\r\n"
article_number: '30'
article_processing_charge: No
article_type: original
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
orcid: 0000-0002-8943-0722
citation:
ama: Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck reachability for data-dependence
and Alias analysis. Proceedings of the ACM on Programming Languages. 2017;2(POPL).
doi:10.1145/3158118
apa: 'Chatterjee, K., Choudhary, B., & Pavlogiannis, A. (2017). Optimal Dyck
reachability for data-dependence and Alias analysis. Proceedings of the ACM
on Programming Languages. Los Angeles, CA, United States: Association for
Computing Machinery. https://doi.org/10.1145/3158118'
chicago: Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. “Optimal
Dyck Reachability for Data-Dependence and Alias Analysis.” Proceedings of the
ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158118.
ieee: K. Chatterjee, B. Choudhary, and A. Pavlogiannis, “Optimal Dyck reachability
for data-dependence and Alias analysis,” Proceedings of the ACM on Programming
Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.
ista: Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability
for data-dependence and Alias analysis. Proceedings of the ACM on Programming
Languages. 2(POPL), 30.
mla: Chatterjee, Krishnendu, et al. “Optimal Dyck Reachability for Data-Dependence
and Alias Analysis.” Proceedings of the ACM on Programming Languages, vol.
2, no. POPL, 30, Association for Computing Machinery, 2017, doi:10.1145/3158118.
short: K. Chatterjee, B. Choudhary, A. Pavlogiannis, Proceedings of the ACM on Programming
Languages 2 (2017).
conference:
end_date: 2018-01-13
location: Los Angeles, CA, United States
name: 'POPL: Programming Languages'
start_date: 2018-01-07
date_created: 2021-12-05T23:01:48Z
date_published: 2017-12-27T00:00:00Z
date_updated: 2023-02-23T12:27:13Z
day: '27'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3158118
ec_funded: 1
external_id:
arxiv:
- '1910.00241'
file:
- access_level: open_access
checksum: faa3f7b3fe8aab84b50ed805c26a0ee5
content_type: application/pdf
creator: cchlebak
date_created: 2021-12-07T08:06:28Z
date_updated: 2021-12-07T08:06:28Z
file_id: '10421'
file_name: 2017_ACMProgLang_Chatterjee.pdf
file_size: 460188
relation: main_file
success: 1
file_date_updated: 2021-12-07T08:06:28Z
has_accepted_license: '1'
intvolume: ' 2'
issue: POPL
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '5455'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Optimal Dyck reachability for data-dependence and Alias analysis
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
---
_id: '5455'
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.'
alternative_title:
- IST Austria Technical Report
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Bhavya
full_name: Choudhary, Bhavya
last_name: Choudhary
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: Chatterjee K, 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.
date_created: 2018-12-12T11:39:26Z
date_published: 2017-10-23T00:00:00Z
date_updated: 2023-02-21T15:54:10Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-870-v1-1
file:
- access_level: open_access
checksum: 177a84a46e3ac17e87b31534ad16a4c9
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:02Z
date_updated: 2020-07-14T12:46:59Z
file_id: '5524'
file_name: IST-2017-870-v1+1_main.pdf
file_size: 960491
relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
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'
related_material:
record:
- id: '10416'
relation: later_version
status: public
status: public
title: Optimal Dyck reachability for data-dependence and alias analysis
type: technical_report
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2017'
...
---
_id: '10417'
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\n\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."
acknowledgement: "The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499- N23, FWF\r\nNFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant
(279307: Graph Games), and Czech\r\nScience Foundation grant GBP202/12/G061."
article_number: '31'
article_processing_charge: No
article_type: original
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
orcid: 0000-0002-8943-0722
- 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. Proceedings of the ACM on Programming Languages.
2017;2(POPL). doi:10.1145/3158119
apa: 'Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., & Vaidya, K.
(2017). Data-centric dynamic partial order reduction. Proceedings of the ACM
on Programming Languages. Los Angeles, CA, United States: Association for
Computing Machinery. https://doi.org/10.1145/3158119'
chicago: Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha,
and Kapil Vaidya. “Data-Centric Dynamic Partial Order Reduction.” Proceedings
of the ACM on Programming Languages. Association for Computing Machinery,
2017. https://doi.org/10.1145/3158119.
ieee: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, “Data-centric
dynamic partial order reduction,” Proceedings of the ACM on Programming Languages,
vol. 2, no. POPL. Association for Computing Machinery, 2017.
ista: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric
dynamic partial order reduction. Proceedings of the ACM on Programming Languages.
2(POPL), 31.
mla: Chalupa, Marek, et al. “Data-Centric Dynamic Partial Order Reduction.” Proceedings
of the ACM on Programming Languages, vol. 2, no. POPL, 31, Association for
Computing Machinery, 2017, doi:10.1145/3158119.
short: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings
of the ACM on Programming Languages 2 (2017).
conference:
end_date: 2018-01-13
location: Los Angeles, CA, United States
name: 'POPL: Programming Languages'
start_date: 2018-01-07
date_created: 2021-12-05T23:01:49Z
date_published: 2017-12-27T00:00:00Z
date_updated: 2023-02-23T12:27:16Z
day: '27'
department:
- _id: KrCh
doi: 10.1145/3158119
ec_funded: 1
external_id:
arxiv:
- '1610.01188'
intvolume: ' 2'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://dl.acm.org/doi/10.1145/3158119
month: '12'
oa: 1
oa_version: Published Version
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: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '5448'
relation: earlier_version
status: public
- id: '5456'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Data-centric dynamic partial order reduction
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
---
_id: '5456'
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."
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
orcid: 0000-0002-8943-0722
- 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.
date_created: 2018-12-12T11:39:26Z
date_published: 2017-10-23T00:00:00Z
date_updated: 2023-02-23T12:26:54Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-872-v1-1
file:
- access_level: open_access
checksum: d2635c4cf013000f0a1b09e80f9e4ab7
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:26Z
date_updated: 2020-07-14T12:46:59Z
file_id: '5487'
file_name: IST-2017-872-v1+1_main.pdf
file_size: 910347
relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
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: '10417'
relation: later_version
status: public
- 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: '551'
abstract:
- lang: eng
text: 'Evolutionary graph theory studies the evolutionary dynamics in a population
structure given as a connected graph. Each node of the graph represents an individual
of the population, and edges determine how offspring are placed. We consider the
classical birth-death Moran process where there are two types of individuals,
namely, the residents with fitness 1 and mutants with fitness r. The fitness indicates
the reproductive strength. The evolutionary dynamics happens as follows: in the
initial step, in a population of all resident individuals a mutant is introduced,
and then at each step, an individual is chosen proportional to the fitness of
its type to reproduce, and the offspring replaces a neighbor uniformly at random.
The process stops when all individuals are either residents or mutants. The probability
that all individuals in the end are mutants is called the fixation probability,
which is a key factor in the rate of evolution. We consider the problem of approximating
the fixation probability. The class of algorithms that is extremely relevant for
approximation of the fixation probabilities is the Monte-Carlo simulation of the
process. Previous results present a polynomial-time Monte-Carlo algorithm for
undirected graphs when r is given in unary. First, we present a simple modification:
instead of simulating each step, we discard ineffective steps, where no node changes
type (i.e., either residents replace residents, or mutants replace mutants). Using
the above simple modification and our result that the number of effective steps
is concentrated around the expected number of effective steps, we present faster
polynomial-time Monte-Carlo algorithms for undirected graphs. Our algorithms are
always at least a factor O(n2/ log n) faster as compared to the previous algorithms,
where n is the number of nodes, and is polynomial even if r is given in binary.
We also present lower bounds showing that the upper bound on the expected number
of effective steps we present is asymptotically tight for undirected graphs. '
alternative_title:
- LIPIcs
article_number: '61'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: 'Chatterjee K, Ibsen-Jensen R, Nowak M. Faster Monte Carlo algorithms for fixation
probability of the Moran process on undirected graphs. In: Leibniz International
Proceedings in Informatics. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für
Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.61'
apa: 'Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2017). Faster Monte Carlo
algorithms for fixation probability of the Moran process on undirected graphs.
In Leibniz International Proceedings in Informatics (Vol. 83). Aalborg,
Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.61'
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. “Faster
Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected
Graphs.” In Leibniz International Proceedings in Informatics, Vol. 83.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.61.
ieee: K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, “Faster Monte Carlo algorithms
for fixation probability of the Moran process on undirected graphs,” in Leibniz
International Proceedings in Informatics, Aalborg, Denmark, 2017, vol. 83.
ista: 'Chatterjee K, Ibsen-Jensen R, Nowak M. 2017. Faster Monte Carlo algorithms
for fixation probability of the Moran process on undirected graphs. Leibniz International
Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science
(SG), LIPIcs, vol. 83, 61.'
mla: Chatterjee, Krishnendu, et al. “Faster Monte Carlo Algorithms for Fixation
Probability of the Moran Process on Undirected Graphs.” Leibniz International
Proceedings in Informatics, vol. 83, 61, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.61.
short: K. Chatterjee, R. Ibsen-Jensen, M. Nowak, in:, Leibniz International Proceedings
in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
conference:
end_date: 2017-08-25
location: Aalborg, Denmark
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2017-08-21
date_created: 2018-12-11T11:47:08Z
date_published: 2017-11-01T00:00:00Z
date_updated: 2021-01-12T08:02:34Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.MFCS.2017.61
file:
- access_level: open_access
checksum: 2eed5224c0e4e259484a1d71acb8ba6a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:04Z
date_updated: 2020-07-14T12:47:00Z
file_id: '5322'
file_name: IST-2018-924-v1+1_LIPIcs-MFCS-2017-61.pdf
file_size: 535077
relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
intvolume: ' 83'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
publication: Leibniz International Proceedings in Informatics
publication_identifier:
isbn:
- 978-395977046-0
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7263'
pubrep_id: '924'
quality_controlled: '1'
scopus_import: 1
status: public
title: Faster Monte Carlo algorithms for fixation probability of the Moran process
on undirected graphs
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 83
year: '2017'
...
---
_id: '552'
abstract:
- lang: eng
text: 'Graph games provide the foundation for modeling and synthesis of reactive
processes. Such games are played over graphs where the vertices are controlled
by two adversarial players. We consider graph games where the objective of the
first player is the conjunction of a qualitative objective (specified as a parity
condition) and a quantitative objective (specified as a meanpayoff condition).
There are two variants of the problem, namely, the threshold problem where the
quantitative goal is to ensure that the mean-payoff value is above a threshold,
and the value problem where the quantitative goal is to ensure the optimal mean-payoff
value; in both cases ensuring the qualitative parity objective. The previous best-known
algorithms for game graphs with n vertices, m edges, parity objectives with d
priorities, and maximal absolute reward value W for mean-payoff objectives, are
as follows: O(nd+1 . m . w) for the threshold problem, and O(nd+2 · m · W) for
the value problem. Our main contributions are faster algorithms, and the running
times of our algorithms are as follows: O(nd-1 · m ·W) for the threshold problem,
and O(nd · m · W · log(n · W)) for the value problem. For mean-payoff parity objectives
with two priorities, our algorithms match the best-known bounds of the algorithms
for mean-payoff games (without conjunction with parity objectives). Our results
are relevant in synthesis of reactive systems with both functional requirement
(given as a qualitative objective) and performance requirement (given as a quantitative
objective).'
alternative_title:
- LIPIcs
article_number: '39'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Alexander
full_name: Svozil, Alexander
last_name: Svozil
citation:
ama: 'Chatterjee K, Henzinger MH, Svozil A. Faster algorithms for mean-payoff parity
games. In: Leibniz International Proceedings in Informatics. Vol 83. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.39'
apa: 'Chatterjee, K., Henzinger, M. H., & Svozil, A. (2017). Faster algorithms
for mean-payoff parity games. In Leibniz International Proceedings in Informatics
(Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.MFCS.2017.39'
chicago: Chatterjee, Krishnendu, Monika H Henzinger, and Alexander Svozil. “Faster
Algorithms for Mean-Payoff Parity Games.” In Leibniz International Proceedings
in Informatics, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.39.
ieee: K. Chatterjee, M. H. Henzinger, and A. Svozil, “Faster algorithms for mean-payoff
parity games,” in Leibniz International Proceedings in Informatics, Aalborg,
Denmark, 2017, vol. 83.
ista: 'Chatterjee K, Henzinger MH, Svozil A. 2017. Faster algorithms for mean-payoff
parity games. Leibniz International Proceedings in Informatics. MFCS: Mathematical
Foundations of Computer Science (SG), LIPIcs, vol. 83, 39.'
mla: Chatterjee, Krishnendu, et al. “Faster Algorithms for Mean-Payoff Parity Games.”
Leibniz International Proceedings in Informatics, vol. 83, 39, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.39.
short: K. Chatterjee, M.H. Henzinger, A. Svozil, in:, Leibniz International Proceedings
in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
conference:
end_date: 2017-08-25
location: Aalborg, Denmark
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2017-08-21
date_created: 2018-12-11T11:47:08Z
date_published: 2017-11-01T00:00:00Z
date_updated: 2023-02-14T10:06:46Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.MFCS.2017.39
ec_funded: 1
file:
- access_level: open_access
checksum: c67f4866ddbfd555afef1f63ae9a8fc7
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:57Z
date_updated: 2020-07-14T12:47:00Z
file_id: '5248'
file_name: IST-2018-923-v1+1_LIPIcs-MFCS-2017-39.pdf
file_size: 610339
relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
intvolume: ' 83'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/3.0/
month: '11'
oa: 1
oa_version: Published Version
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Leibniz International Proceedings in Informatics
publication_identifier:
isbn:
- 978-395977046-0
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7262'
pubrep_id: '923'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for mean-payoff parity games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 83
year: '2017'
...
---
_id: '553'
abstract:
- lang: eng
text: 'We consider two player, zero-sum, finite-state concurrent reachability games,
played 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. Player 1 wins iff a designated goal state is eventually 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. Our main results are as follows: We show that: (i) the optimal bound
on the patience of optimal and -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. '
alternative_title:
- LIPIcs
article_number: '55'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Kristofer
full_name: Hansen, Kristofer
last_name: Hansen
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
citation:
ama: 'Chatterjee K, Hansen K, Ibsen-Jensen R. Strategy complexity of concurrent
safety games. In: Leibniz International Proceedings in Informatics. Vol
83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.55'
apa: 'Chatterjee, K., Hansen, K., & Ibsen-Jensen, R. (2017). Strategy complexity
of concurrent safety games. In Leibniz International Proceedings in Informatics
(Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.MFCS.2017.55'
chicago: Chatterjee, Krishnendu, Kristofer Hansen, and Rasmus Ibsen-Jensen. “Strategy
Complexity of Concurrent Safety Games.” In Leibniz International Proceedings
in Informatics, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.55.
ieee: K. Chatterjee, K. Hansen, and R. Ibsen-Jensen, “Strategy complexity of concurrent
safety games,” in Leibniz International Proceedings in Informatics, Aalborg,
Denmark, 2017, vol. 83.
ista: 'Chatterjee K, Hansen K, Ibsen-Jensen R. 2017. Strategy complexity of concurrent
safety games. Leibniz International Proceedings in Informatics. MFCS: Mathematical
Foundations of Computer Science (SG), LIPIcs, vol. 83, 55.'
mla: Chatterjee, Krishnendu, et al. “Strategy Complexity of Concurrent Safety Games.”
Leibniz International Proceedings in Informatics, vol. 83, 55, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.55.
short: K. Chatterjee, K. Hansen, R. Ibsen-Jensen, in:, Leibniz International Proceedings
in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
conference:
end_date: 2017-08-25
location: Aalborg, Denmark
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2017-08-21
date_created: 2018-12-11T11:47:08Z
date_published: 2017-11-01T00:00:00Z
date_updated: 2021-01-12T08:02:35Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.MFCS.2017.55
file:
- access_level: open_access
checksum: 7101facb56ade363205c695d72dbd173
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:29Z
date_updated: 2020-07-14T12:47:00Z
file_id: '4753'
file_name: IST-2018-922-v1+1_LIPIcs-MFCS-2017-55.pdf
file_size: 549967
relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
intvolume: ' 83'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1506.02434
month: '11'
oa: 1
oa_version: Published Version
publication: Leibniz International Proceedings in Informatics
publication_identifier:
isbn:
- 978-395977046-0
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7261'
pubrep_id: '922'
quality_controlled: '1'
scopus_import: 1
status: public
title: Strategy complexity of concurrent safety games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 83
year: '2017'
...
---
_id: '625'
abstract:
- lang: eng
text: In the analysis of reactive systems a quantitative objective assigns a real
value to every trace of the system. The value decision problem for a quantitative
objective requires a trace whose value is at least a given threshold, and the
exact value decision problem requires a trace whose value is exactly the threshold.
We compare the computational complexity of the value and exact value decision
problems for classical quantitative objectives, such as sum, discounted sum, energy,
and mean-payoff for two standard models of reactive systems, namely, graphs and
graph games.
acknowledgement: 'This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23 and S11407-N23 (RiSE/SHiNE), and Z211-N23 (Wittgenstein
Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund
(WWTF) through project ICT15-003.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Doyen L, Henzinger TA. The cost of exactness in quantitative
reachability. In: Aceto L, Bacci G, Ingólfsdóttir A, Legay A, Mardare R, eds.
Models, Algorithms, Logics and Tools. Vol 10460. Theoretical Computer Science
and General Issues. Springer; 2017:367-381. doi:10.1007/978-3-319-63121-9_18'
apa: Chatterjee, K., Doyen, L., & Henzinger, T. A. (2017). The cost of exactness
in quantitative reachability. In L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay,
& R. Mardare (Eds.), Models, Algorithms, Logics and Tools (Vol. 10460,
pp. 367–381). Springer. https://doi.org/10.1007/978-3-319-63121-9_18
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “The Cost
of Exactness in Quantitative Reachability.” In Models, Algorithms, Logics and
Tools, edited by Luca Aceto, Giorgio Bacci, Anna Ingólfsdóttir, Axel Legay,
and Radu Mardare, 10460:367–81. Theoretical Computer Science and General Issues.
Springer, 2017. https://doi.org/10.1007/978-3-319-63121-9_18.
ieee: K. Chatterjee, L. Doyen, and T. A. Henzinger, “The cost of exactness in quantitative
reachability,” in Models, Algorithms, Logics and Tools, vol. 10460, L.
Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare, Eds. Springer, 2017,
pp. 367–381.
ista: 'Chatterjee K, Doyen L, Henzinger TA. 2017.The cost of exactness in quantitative
reachability. In: Models, Algorithms, Logics and Tools. LNCS, vol. 10460, 367–381.'
mla: Chatterjee, Krishnendu, et al. “The Cost of Exactness in Quantitative Reachability.”
Models, Algorithms, Logics and Tools, edited by Luca Aceto et al., vol.
10460, Springer, 2017, pp. 367–81, doi:10.1007/978-3-319-63121-9_18.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, in:, L. Aceto, G. Bacci, A. Ingólfsdóttir,
A. Legay, R. Mardare (Eds.), Models, Algorithms, Logics and Tools, Springer, 2017,
pp. 367–381.
date_created: 2018-12-11T11:47:34Z
date_published: 2017-07-25T00:00:00Z
date_updated: 2022-05-23T08:54:02Z
day: '25'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-63121-9_18
ec_funded: 1
editor:
- first_name: Luca
full_name: Aceto, Luca
last_name: Aceto
- first_name: Giorgio
full_name: Bacci, Giorgio
last_name: Bacci
- first_name: Anna
full_name: Ingólfsdóttir, Anna
last_name: Ingólfsdóttir
- first_name: Axel
full_name: Legay, Axel
last_name: Legay
- first_name: Radu
full_name: Mardare, Radu
last_name: Mardare
file:
- access_level: open_access
checksum: b2402766ec02c79801aac634bd8f9f6c
content_type: application/pdf
creator: dernst
date_created: 2019-11-19T08:06:50Z
date_updated: 2020-07-14T12:47:25Z
file_id: '7048'
file_name: 2017_ModelsAlgorithms_Chatterjee.pdf
file_size: 192826
relation: main_file
file_date_updated: 2020-07-14T12:47:25Z
has_accepted_license: '1'
intvolume: ' 10460'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 367 - 381
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Models, Algorithms, Logics and Tools
publication_identifier:
isbn:
- 978-3-319-63120-2
issn:
- 0302-9743
publication_status: published
publisher: Springer
publist_id: '7170'
quality_controlled: '1'
scopus_import: '1'
series_title: Theoretical Computer Science and General Issues
status: public
title: The cost of exactness in quantitative reachability
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10460
year: '2017'
...
---
_id: '628'
abstract:
- lang: eng
text: We consider the problem of developing automated techniques for solving recurrence
relations to aid the expected-runtime analysis of programs. The motivation is
that several classical textbook algorithms have quite efficient expected-runtime
complexity, whereas the corresponding worst-case bounds are either inefficient
(e.g., Quick-Sort), or completely ineffective (e.g., Coupon-Collector). Since
the main focus of expected-runtime analysis is to obtain efficient bounds, we
consider bounds that are either logarithmic, linear or almost-linear (O(log n),
O(n), O(n · log n), respectively, where n represents the input size). Our main
contribution is an efficient (simple linear-time algorithm) sound approach for
deriving such expected-runtime bounds for the analysis of recurrence relations
induced by randomized algorithms. The experimental results show that our approach
can efficiently derive asymptotically optimal expected-runtime bounds for recurrences
of classical randomized algorithms, including Randomized-Search, Quick-Sort, Quick-Select,
Coupon-Collector, where the worst-case bounds are either inefficient (such as
linear as compared to logarithmic expected-runtime complexity, or quadratic as
compared to linear or almost-linear expected-runtime complexity), or ineffective.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Hongfei
full_name: Fu, Hongfei
last_name: Fu
- first_name: Aniket
full_name: Murhekar, Aniket
last_name: Murhekar
citation:
ama: 'Chatterjee K, Fu H, Murhekar A. Automated recurrence analysis for almost linear
expected runtime bounds. In: Majumdar R, Kunčak V, eds. Vol 10426. Springer; 2017:118-139.
doi:10.1007/978-3-319-63387-9_6'
apa: 'Chatterjee, K., Fu, H., & Murhekar, A. (2017). Automated recurrence analysis
for almost linear expected runtime bounds. In R. Majumdar & V. Kunčak (Eds.)
(Vol. 10426, pp. 118–139). Presented at the CAV: Computer Aided Verification,
Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63387-9_6'
chicago: Chatterjee, Krishnendu, Hongfei Fu, and Aniket Murhekar. “Automated Recurrence
Analysis for Almost Linear Expected Runtime Bounds.” edited by Rupak Majumdar
and Viktor Kunčak, 10426:118–39. Springer, 2017. https://doi.org/10.1007/978-3-319-63387-9_6.
ieee: 'K. Chatterjee, H. Fu, and A. Murhekar, “Automated recurrence analysis for
almost linear expected runtime bounds,” presented at the CAV: Computer Aided Verification,
Heidelberg, Germany, 2017, vol. 10426, pp. 118–139.'
ista: 'Chatterjee K, Fu H, Murhekar A. 2017. Automated recurrence analysis for almost
linear expected runtime bounds. CAV: Computer Aided Verification, LNCS, vol. 10426,
118–139.'
mla: Chatterjee, Krishnendu, et al. Automated Recurrence Analysis for Almost
Linear Expected Runtime Bounds. Edited by Rupak Majumdar and Viktor Kunčak,
vol. 10426, Springer, 2017, pp. 118–39, doi:10.1007/978-3-319-63387-9_6.
short: K. Chatterjee, H. Fu, A. Murhekar, in:, R. Majumdar, V. Kunčak (Eds.), Springer,
2017, pp. 118–139.
conference:
end_date: 2017-07-28
location: Heidelberg, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2017-07-24
date_created: 2018-12-11T11:47:35Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2021-01-12T08:06:55Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-319-63387-9_6
ec_funded: 1
editor:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Viktor
full_name: Kunčak, Viktor
last_name: Kunčak
intvolume: ' 10426'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1705.00314
month: '01'
oa: 1
oa_version: Submitted Version
page: 118 - 139
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
isbn:
- 978-331963386-2
publication_status: published
publisher: Springer
publist_id: '7166'
quality_controlled: '1'
scopus_import: 1
status: public
title: Automated recurrence analysis for almost linear expected runtime bounds
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 10426
year: '2017'
...
---
_id: '645'
abstract:
- lang: eng
text: Markov decision processes (MDPs) are standard models for probabilistic systems
with non-deterministic behaviours. Long-run average rewards provide a mathematically
elegant formalism for expressing long term performance. Value iteration (VI) is
one of the simplest and most efficient algorithmic approaches to MDPs with other
properties, such as reachability objectives. Unfortunately, a naive extension
of VI does not work for MDPs with long-run average rewards, as there is no known
stopping criterion. In this work our contributions are threefold. (1) We refute
a conjecture related to stopping criteria for MDPs with long-run average rewards.
(2) We present two practical algorithms for MDPs with long-run average rewards
based on VI. First, we show that a combination of applying VI locally for each
maximal end-component (MEC) and VI for reachability objectives can provide approximation
guarantees. Second, extending the above approach with a simulation-guided on-demand
variant of VI, we present an anytime algorithm that is able to deal with very
large models. (3) Finally, we present experimental results showing that our methods
significantly outperform the standard approaches on several benchmarks.
alternative_title:
- LNCS
author:
- first_name: Pranav
full_name: Ashok, Pranav
last_name: Ashok
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
last_name: Meggendorfer
citation:
ama: 'Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. Value iteration
for long run average reward in markov decision processes. In: Majumdar R, Kunčak
V, eds. Vol 10426. Springer; 2017:201-221. doi:10.1007/978-3-319-63387-9_10'
apa: 'Ashok, P., Chatterjee, K., Daca, P., Kretinsky, J., & Meggendorfer, T.
(2017). Value iteration for long run average reward in markov decision processes.
In R. Majumdar & V. Kunčak (Eds.) (Vol. 10426, pp. 201–221). Presented at
the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63387-9_10'
chicago: Ashok, Pranav, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretinsky, and
Tobias Meggendorfer. “Value Iteration for Long Run Average Reward in Markov Decision
Processes.” edited by Rupak Majumdar and Viktor Kunčak, 10426:201–21. Springer,
2017. https://doi.org/10.1007/978-3-319-63387-9_10.
ieee: 'P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, and T. Meggendorfer, “Value
iteration for long run average reward in markov decision processes,” presented
at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426,
pp. 201–221.'
ista: 'Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. 2017. Value iteration
for long run average reward in markov decision processes. CAV: Computer Aided
Verification, LNCS, vol. 10426, 201–221.'
mla: Ashok, Pranav, et al. Value Iteration for Long Run Average Reward in Markov
Decision Processes. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426,
Springer, 2017, pp. 201–21, doi:10.1007/978-3-319-63387-9_10.
short: P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R.
Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.
conference:
end_date: 2017-07-28
location: Heidelberg, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2017-07-24
date_created: 2018-12-11T11:47:41Z
date_published: 2017-07-13T00:00:00Z
date_updated: 2021-01-12T08:07:32Z
day: '13'
department:
- _id: KrCh
doi: 10.1007/978-3-319-63387-9_10
ec_funded: 1
editor:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Viktor
full_name: Kunčak, Viktor
last_name: Kunčak
intvolume: ' 10426'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1705.02326
month: '07'
oa: 1
oa_version: Submitted Version
page: 201 - 221
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
isbn:
- 978-331963386-2
publication_status: published
publisher: Springer
publist_id: '7135'
quality_controlled: '1'
scopus_import: 1
status: public
title: Value iteration for long run average reward in markov decision processes
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 10426
year: '2017'
...
---
_id: '6519'
abstract:
- lang: eng
text: 'Graph games with omega-regular winning conditions provide a mathematical
framework to analyze a wide range of problems in the analysis of reactive systems
and programs (such as the synthesis of reactive systems, program repair, and the
verification of branching time properties). Parity conditions are canonical forms
to specify omega-regular winning conditions. Graph games with parity conditions
are equivalent to mu-calculus model checking, and thus a very important algorithmic
problem. Symbolic algorithms are of great significance because they provide scalable
algorithms for the analysis of large finite-state systems, as well as algorithms
for the analysis of infinite-state systems with finite quotient. A set-based symbolic
algorithm uses the basic set operations and the one-step predecessor operators.
We consider graph games with n vertices and parity conditions with c priorities
(equivalently, a mu-calculus formula with c alternations of least and greatest
fixed points). While many explicit algorithms exist for graph games with parity
conditions, for set-based symbolic algorithms there are only two algorithms (notice
that we use space to refer to the number of sets stored by a symbolic algorithm):
(a) the basic algorithm that requires O(n^c) symbolic operations and linear space;
and (b) an improved algorithm that requires O(n^{c/2+1}) symbolic operations but
also O(n^{c/2+1}) space (i.e., exponential space). In this work we present two
set-based symbolic algorithms for parity games: (a) our first algorithm requires
O(n^{c/2+1}) symbolic operations and only requires linear space; and (b) developing
on our first algorithm, we present an algorithm that requires O(n^{c/3+1}) symbolic
operations and only linear space. We also present the first linear space set-based
symbolic algorithm for parity games that requires at most a sub-exponential number
of symbolic operations. '
article_number: '18'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Wolfgang
full_name: Dvorák, Wolfgang
last_name: Dvorák
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Veronika
full_name: Loitzenbauer, Veronika
last_name: Loitzenbauer
citation:
ama: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. Improved set-based symbolic
algorithms for parity games. In: Vol 82. Schloss Dagstuhl -Leibniz-Zentrum fuer
Informatik; 2017. doi:10.4230/LIPICS.CSL.2017.18'
apa: 'Chatterjee, K., Dvorák, W., Henzinger, M. H., & Loitzenbauer, V. (2017).
Improved set-based symbolic algorithms for parity games (Vol. 82). Presented at
the CSL: Conference on Computer Science Logic, Stockholm, Sweden: Schloss Dagstuhl
-Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPICS.CSL.2017.18'
chicago: Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Veronika
Loitzenbauer. “Improved Set-Based Symbolic Algorithms for Parity Games,” Vol.
82. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2017. https://doi.org/10.4230/LIPICS.CSL.2017.18.
ieee: 'K. Chatterjee, W. Dvorák, M. H. Henzinger, and V. Loitzenbauer, “Improved
set-based symbolic algorithms for parity games,” presented at the CSL: Conference
on Computer Science Logic, Stockholm, Sweden, 2017, vol. 82.'
ista: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. 2017. Improved set-based
symbolic algorithms for parity games. CSL: Conference on Computer Science Logic
vol. 82, 18.'
mla: Chatterjee, Krishnendu, et al. Improved Set-Based Symbolic Algorithms for
Parity Games. Vol. 82, 18, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik,
2017, doi:10.4230/LIPICS.CSL.2017.18.
short: K. Chatterjee, W. Dvorák, M.H. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl
-Leibniz-Zentrum fuer Informatik, 2017.
conference:
end_date: 2017-08-24
location: Stockholm, Sweden
name: 'CSL: Conference on Computer Science Logic'
start_date: 2017-08-20
date_created: 2019-06-04T12:42:43Z
date_published: 2017-08-01T00:00:00Z
date_updated: 2023-02-14T10:08:25Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPICS.CSL.2017.18
ec_funded: 1
file:
- access_level: open_access
checksum: 7c2c9d09970af79026d7e37d9b632ef8
content_type: application/pdf
creator: kschuh
date_created: 2019-06-04T12:56:52Z
date_updated: 2020-07-14T12:47:33Z
file_id: '6520'
file_name: 2017_LIPIcs-Chatterjee.pdf
file_size: 710185
relation: main_file
file_date_updated: 2020-07-14T12:47:33Z
has_accepted_license: '1'
intvolume: ' 82'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Improved set-based symbolic algorithms for parity games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 82
year: '2017'
...
---
_id: '653'
abstract:
- lang: eng
text: The extent of heterogeneity among driver gene mutations present in naturally
occurring metastases - that is, treatment-naive metastatic disease - is largely
unknown. To address this issue, we carried out 60× whole-genome sequencing of
26 metastases from four patients with pancreatic cancer. We found that identical
mutations in known driver genes were present in every metastatic lesion for each
patient studied. Passenger gene mutations, which do not have known or predicted
functional consequences, accounted for all intratumoral heterogeneity. Even with
respect to these passenger mutations, our analysis suggests that the genetic similarity
among the founding cells of metastases was higher than that expected for any two
cells randomly taken from a normal tissue. The uniformity of known driver gene
mutations among metastases in the same patient has critical and encouraging implications
for the success of future targeted therapies in advanced-stage disease.
acknowledgement: 'We thank the Memorial Sloan Kettering Cancer Center Molecular Cytology
core facility for immunohistochemistry staining. This work was supported by Office
of Naval Research grant N00014-16-1-2914, the Bill and Melinda Gates Foundation
(OPP1148627), and a gift from B. Wu and E. Larson (M.A.N.), National Institutes
of Health grants CA179991 (C.A.I.-D. and I.B.), F31 CA180682 (A.P.M.-M.), CA43460
(B.V.), and P50 CA62924, the Monastra Foundation, the Virginia and D.K. Ludwig Fund
for Cancer Research, the Lustgarten Foundation for Pancreatic Cancer Research, the
Sol Goldman Center for Pancreatic Cancer Research, the Sol Goldman Sequencing Center,
ERC Start grant 279307: Graph Games (J.G.R., D.K., and C.K.), Austrian Science Fund
(FWF) grant P23499-N23 (J.G.R., D.K., and C.K.), and FWF NFN grant S11407-N23 RiSE/SHiNE
(J.G.R., D.K., and C.K.).'
article_processing_charge: No
article_type: original
author:
- first_name: Alvin
full_name: Makohon Moore, Alvin
last_name: Makohon Moore
- first_name: Ming
full_name: Zhang, Ming
last_name: Zhang
- first_name: Johannes
full_name: Reiter, Johannes
id: 4A918E98-F248-11E8-B48F-1D18A9856A87
last_name: Reiter
orcid: 0000-0002-0170-7353
- first_name: Ivana
full_name: Božić, Ivana
last_name: Božić
- first_name: Benjamin
full_name: Allen, Benjamin
last_name: Allen
- first_name: Deepanjan
full_name: Kundu, Deepanjan
id: 1d4c0f4f-e8a3-11ec-a351-e36772758c45
last_name: Kundu
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Fay
full_name: Wong, Fay
last_name: Wong
- first_name: Yuchen
full_name: Jiao, Yuchen
last_name: Jiao
- first_name: Zachary
full_name: Kohutek, Zachary
last_name: Kohutek
- first_name: Jungeui
full_name: Hong, Jungeui
last_name: Hong
- first_name: Marc
full_name: Attiyeh, Marc
last_name: Attiyeh
- first_name: Breanna
full_name: Javier, Breanna
last_name: Javier
- first_name: Laura
full_name: Wood, Laura
last_name: Wood
- first_name: Ralph
full_name: Hruban, Ralph
last_name: Hruban
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
- first_name: Nickolas
full_name: Papadopoulos, Nickolas
last_name: Papadopoulos
- first_name: Kenneth
full_name: Kinzler, Kenneth
last_name: Kinzler
- first_name: Bert
full_name: Vogelstein, Bert
last_name: Vogelstein
- first_name: Christine
full_name: Iacobuzio Donahue, Christine
last_name: Iacobuzio Donahue
citation:
ama: Makohon Moore A, Zhang M, Reiter J, et al. Limited heterogeneity of known driver
gene mutations among the metastases of individual patients with pancreatic cancer.
Nature Genetics. 2017;49(3):358-366. doi:10.1038/ng.3764
apa: Makohon Moore, A., Zhang, M., Reiter, J., Božić, I., Allen, B., Kundu, D.,
… Iacobuzio Donahue, C. (2017). Limited heterogeneity of known driver gene mutations
among the metastases of individual patients with pancreatic cancer. Nature
Genetics. Nature Publishing Group. https://doi.org/10.1038/ng.3764
chicago: Makohon Moore, Alvin, Ming Zhang, Johannes Reiter, Ivana Božić, Benjamin
Allen, Deepanjan Kundu, Krishnendu Chatterjee, et al. “Limited Heterogeneity of
Known Driver Gene Mutations among the Metastases of Individual Patients with Pancreatic
Cancer.” Nature Genetics. Nature Publishing Group, 2017. https://doi.org/10.1038/ng.3764.
ieee: A. Makohon Moore et al., “Limited heterogeneity of known driver gene
mutations among the metastases of individual patients with pancreatic cancer,”
Nature Genetics, vol. 49, no. 3. Nature Publishing Group, pp. 358–366,
2017.
ista: Makohon Moore A, Zhang M, Reiter J, Božić I, Allen B, Kundu D, Chatterjee
K, Wong F, Jiao Y, Kohutek Z, Hong J, Attiyeh M, Javier B, Wood L, Hruban R, Nowak
M, Papadopoulos N, Kinzler K, Vogelstein B, Iacobuzio Donahue C. 2017. Limited
heterogeneity of known driver gene mutations among the metastases of individual
patients with pancreatic cancer. Nature Genetics. 49(3), 358–366.
mla: Makohon Moore, Alvin, et al. “Limited Heterogeneity of Known Driver Gene Mutations
among the Metastases of Individual Patients with Pancreatic Cancer.” Nature
Genetics, vol. 49, no. 3, Nature Publishing Group, 2017, pp. 358–66, doi:10.1038/ng.3764.
short: A. Makohon Moore, M. Zhang, J. Reiter, I. Božić, B. Allen, D. Kundu, K. Chatterjee,
F. Wong, Y. Jiao, Z. Kohutek, J. Hong, M. Attiyeh, B. Javier, L. Wood, R. Hruban,
M. Nowak, N. Papadopoulos, K. Kinzler, B. Vogelstein, C. Iacobuzio Donahue, Nature
Genetics 49 (2017) 358–366.
date_created: 2018-12-11T11:47:43Z
date_published: 2017-03-01T00:00:00Z
date_updated: 2022-06-10T09:55:08Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/ng.3764
ec_funded: 1
external_id:
pmid:
- '28092682'
file:
- access_level: open_access
checksum: e442dc3b7420a36ec805e9bb45cc1a2e
content_type: application/pdf
creator: dernst
date_created: 2019-11-19T08:13:50Z
date_updated: 2020-07-14T12:47:33Z
file_id: '7050'
file_name: 2017_NatureGenetics_Makohon.pdf
file_size: 908099
relation: main_file
file_date_updated: 2020-07-14T12:47:33Z
has_accepted_license: '1'
intvolume: ' 49'
issue: '3'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
page: 358 - 366
pmid: 1
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: Nature Genetics
publication_identifier:
issn:
- '10614036'
publication_status: published
publisher: Nature Publishing Group
publist_id: '7092'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Limited heterogeneity of known driver gene mutations among the metastases of
individual patients with pancreatic cancer
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 49
year: '2017'
...
---
_id: '671'
abstract:
- lang: eng
text: Humans routinely use conditionally cooperative strategies when interacting
in repeated social dilemmas. They are more likely to cooperate if others cooperated
before, and are ready to retaliate if others defected. To capture the emergence
of reciprocity, most previous models consider subjects who can only choose from
a restricted set of representative strategies, or who react to the outcome of
the very last round only. As players memorize more rounds, the dimension of the
strategy space increases exponentially. This increasing computational complexity
renders simulations for individuals with higher cognitive abilities infeasible,
especially if multiplayer interactions are taken into account. Here, we take an
axiomatic approach instead. We propose several properties that a robust cooperative
strategy for a repeated multiplayer dilemma should have. These properties naturally
lead to a unique class of cooperative strategies, which contains the classical
Win-Stay Lose-Shift rule as a special case. A comprehensive numerical analysis
for the prisoner's dilemma and for the public goods game suggests that strategies
of this class readily evolve across various memory-n spaces. Our results reveal
that successful strategies depend not only on how cooperative others were in the
past but also on the respective context of cooperation.
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Vaquero
full_name: Martinez, Vaquero
last_name: Martinez
- 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: Hilbe C, Martinez V, Chatterjee K, Nowak M. Memory-n strategies of direct reciprocity.
PNAS. 2017;114(18):4715-4720. doi:10.1073/pnas.1621239114
apa: Hilbe, C., Martinez, V., Chatterjee, K., & Nowak, M. (2017). Memory-n strategies
of direct reciprocity. PNAS. National Academy of Sciences. https://doi.org/10.1073/pnas.1621239114
chicago: Hilbe, Christian, Vaquero Martinez, Krishnendu Chatterjee, and Martin Nowak.
“Memory-n Strategies of Direct Reciprocity.” PNAS. National Academy of
Sciences, 2017. https://doi.org/10.1073/pnas.1621239114.
ieee: C. Hilbe, V. Martinez, K. Chatterjee, and M. Nowak, “Memory-n strategies of
direct reciprocity,” PNAS, vol. 114, no. 18. National Academy of Sciences,
pp. 4715–4720, 2017.
ista: Hilbe C, Martinez V, Chatterjee K, Nowak M. 2017. Memory-n strategies of direct
reciprocity. PNAS. 114(18), 4715–4720.
mla: Hilbe, Christian, et al. “Memory-n Strategies of Direct Reciprocity.” PNAS,
vol. 114, no. 18, National Academy of Sciences, 2017, pp. 4715–20, doi:10.1073/pnas.1621239114.
short: C. Hilbe, V. Martinez, K. Chatterjee, M. Nowak, PNAS 114 (2017) 4715–4720.
date_created: 2018-12-11T11:47:50Z
date_published: 2017-05-02T00:00:00Z
date_updated: 2021-01-12T08:08:37Z
day: '02'
department:
- _id: KrCh
doi: 10.1073/pnas.1621239114
ec_funded: 1
external_id:
pmid:
- '28420786'
intvolume: ' 114'
issue: '18'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5422766/
month: '05'
oa: 1
oa_version: Published Version
page: 4715 - 4720
pmid: 1
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: PNAS
publication_identifier:
issn:
- '00278424'
publication_status: published
publisher: National Academy of Sciences
publist_id: '7053'
quality_controlled: '1'
scopus_import: 1
status: public
title: Memory-n strategies of direct reciprocity
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 114
year: '2017'
...
---
_id: '681'
abstract:
- lang: eng
text: Two-player games on graphs provide the theoretical framework for many important
problems such as reactive synthesis. While the traditional study of two-player
zero-sum games has been extended to multi-player games with several notions of
equilibria, they are decidable only for perfect-information games, whereas several
applications require imperfect-information. In this paper we propose a new notion
of equilibria, called doomsday equilibria, which is a strategy profile where all
players satisfy their own objective, and if any coalition of players deviates
and violates even one of the players' objective, then the objective of every player
is violated. We present algorithms and complexity results for deciding the existence
of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information
games, and for perfect-information games. We provide optimal complexity bounds
for imperfect-information games, and in most cases for perfect-information games.
article_processing_charge: No
article_type: original
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Emmanuel
full_name: Filiot, Emmanuel
last_name: Filiot
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: Chatterjee K, Doyen L, Filiot E, Raskin J. Doomsday equilibria for omega-regular
games. Information and Computation. 2017;254:296-315. doi:10.1016/j.ic.2016.10.012
apa: Chatterjee, K., Doyen, L., Filiot, E., & Raskin, J. (2017). Doomsday equilibria
for omega-regular games. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2016.10.012
chicago: Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean Raskin.
“Doomsday Equilibria for Omega-Regular Games.” Information and Computation.
Elsevier, 2017. https://doi.org/10.1016/j.ic.2016.10.012.
ieee: K. Chatterjee, L. Doyen, E. Filiot, and J. Raskin, “Doomsday equilibria for
omega-regular games,” Information and Computation, vol. 254. Elsevier,
pp. 296–315, 2017.
ista: Chatterjee K, Doyen L, Filiot E, Raskin J. 2017. Doomsday equilibria for omega-regular
games. Information and Computation. 254, 296–315.
mla: Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.”
Information and Computation, vol. 254, Elsevier, 2017, pp. 296–315, doi:10.1016/j.ic.2016.10.012.
short: K. Chatterjee, L. Doyen, E. Filiot, J. Raskin, Information and Computation
254 (2017) 296–315.
date_created: 2018-12-11T11:47:53Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-02-21T16:06:02Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.ic.2016.10.012
ec_funded: 1
external_id:
arxiv:
- '1311.3238'
intvolume: ' 254'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1311.3238
month: '06'
oa: 1
oa_version: Submitted Version
page: 296 - 315
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: Information and Computation
publication_identifier:
issn:
- '08905401'
publication_status: published
publisher: Elsevier
publist_id: '7036'
quality_controlled: '1'
related_material:
record:
- id: '10885'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Doomsday equilibria for omega-regular games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 254
year: '2017'
...
---
_id: '684'
abstract:
- lang: eng
text: We generalize winning conditions in two-player games by adding a structural
acceptance condition called obligations. Obligations are orthogonal to the linear
winning conditions that define whether a play is winning. Obligations are a declaration
that player 0 can achieve a certain value from a configuration. If the obligation
is met, the value of that configuration for player 0 is 1. We define the value
in such games and show that obligation games are determined. For Markov chains
with Borel objectives and obligations, and finite turn-based stochastic parity
games with obligations we give an alternative and simpler characterization of
the value function. Based on this simpler definition we show that the decision
problem of winning finite turn-based stochastic parity games with obligations
is in NP∩co-NP. We also show that obligation games provide a game framework for
reasoning about p-automata. © 2017 The Association for Symbolic Logic.
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: Chatterjee K, Piterman N. Obligation blackwell games and p-automata. Journal
of Symbolic Logic. 2017;82(2):420-452. doi:10.1017/jsl.2016.71
apa: Chatterjee, K., & Piterman, N. (2017). Obligation blackwell games and p-automata.
Journal of Symbolic Logic. Cambridge University Press. https://doi.org/10.1017/jsl.2016.71
chicago: Chatterjee, Krishnendu, and Nir Piterman. “Obligation Blackwell Games and
P-Automata.” Journal of Symbolic Logic. Cambridge University Press, 2017.
https://doi.org/10.1017/jsl.2016.71.
ieee: K. Chatterjee and N. Piterman, “Obligation blackwell games and p-automata,”
Journal of Symbolic Logic, vol. 82, no. 2. Cambridge University Press,
pp. 420–452, 2017.
ista: Chatterjee K, Piterman N. 2017. Obligation blackwell games and p-automata.
Journal of Symbolic Logic. 82(2), 420–452.
mla: Chatterjee, Krishnendu, and Nir Piterman. “Obligation Blackwell Games and P-Automata.”
Journal of Symbolic Logic, vol. 82, no. 2, Cambridge University Press,
2017, pp. 420–52, doi:10.1017/jsl.2016.71.
short: K. Chatterjee, N. Piterman, Journal of Symbolic Logic 82 (2017) 420–452.
date_created: 2018-12-11T11:47:54Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2021-04-16T12:10:53Z
day: '01'
department:
- _id: KrCh
doi: 10.1017/jsl.2016.71
intvolume: ' 82'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1206.5174
month: '06'
oa: 1
oa_version: Submitted Version
page: 420 - 452
publication: Journal of Symbolic Logic
publication_identifier:
eissn:
- 1943-5886
issn:
- 0022-4812
publication_status: published
publisher: Cambridge University Press
publist_id: '7026'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Obligation blackwell games and p-automata
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 82
year: '2017'
...
---
_id: '699'
abstract:
- lang: eng
text: 'In antagonistic symbioses, such as host–parasite interactions, one population’s
success is the other’s loss. In mutualistic symbioses, such as division of labor,
both parties can gain, but they might have different preferences over the possible
mutualistic arrangements. The rates of evolution of the two populations in a symbiosis
are important determinants of which population will be more successful: Faster
evolution is thought to be favored in antagonistic symbioses (the “Red Queen effect”),
but disfavored in certain mutualistic symbioses (the “Red King effect”). However,
it remains unclear which biological parameters drive these effects. Here, we analyze
the effects of the various determinants of evolutionary rate: generation time,
mutation rate, population size, and the intensity of natural selection. Our main
results hold for the case where mutation is infrequent. Slower evolution causes
a long-term advantage in an important class of mutualistic interactions. Surprisingly,
less intense selection is the strongest driver of this Red King effect, whereas
relative mutation rates and generation times have little effect. In antagonistic
interactions, faster evolution by any means is beneficial. Our results provide
insight into the demographic evolution of symbionts. '
author:
- first_name: Carl
full_name: Veller, Carl
last_name: Veller
- first_name: Laura
full_name: Hayward, Laura
last_name: Hayward
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
citation:
ama: Veller C, Hayward L, Nowak M, Hilbe C. The red queen and king in finite populations.
PNAS. 2017;114(27):E5396-E5405. doi:10.1073/pnas.1702020114
apa: Veller, C., Hayward, L., Nowak, M., & Hilbe, C. (2017). The red queen and
king in finite populations. PNAS. National Academy of Sciences. https://doi.org/10.1073/pnas.1702020114
chicago: Veller, Carl, Laura Hayward, Martin Nowak, and Christian Hilbe. “The Red
Queen and King in Finite Populations.” PNAS. National Academy of Sciences,
2017. https://doi.org/10.1073/pnas.1702020114.
ieee: C. Veller, L. Hayward, M. Nowak, and C. Hilbe, “The red queen and king in
finite populations,” PNAS, vol. 114, no. 27. National Academy of Sciences,
pp. E5396–E5405, 2017.
ista: Veller C, Hayward L, Nowak M, Hilbe C. 2017. The red queen and king in finite
populations. PNAS. 114(27), E5396–E5405.
mla: Veller, Carl, et al. “The Red Queen and King in Finite Populations.” PNAS,
vol. 114, no. 27, National Academy of Sciences, 2017, pp. E5396–405, doi:10.1073/pnas.1702020114.
short: C. Veller, L. Hayward, M. Nowak, C. Hilbe, PNAS 114 (2017) E5396–E5405.
date_created: 2018-12-11T11:48:00Z
date_published: 2017-07-03T00:00:00Z
date_updated: 2021-01-12T08:11:21Z
day: '03'
department:
- _id: KrCh
doi: 10.1073/pnas.1702020114
external_id:
pmid:
- '28630336'
intvolume: ' 114'
issue: '27'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5502615/
month: '07'
oa: 1
oa_version: Submitted Version
page: E5396 - E5405
pmid: 1
publication: PNAS
publication_identifier:
issn:
- '00278424'
publication_status: published
publisher: National Academy of Sciences
publist_id: '7002'
quality_controlled: '1'
scopus_import: 1
status: public
title: The red queen and king in finite populations
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 114
year: '2017'
...
---
_id: '711'
abstract:
- lang: eng
text: Nested weighted automata (NWA) present a robust and convenient automata-theoretic
formalism for quantitative specifications. Previous works have considered NWA
that processed input words only in the forward direction. It is natural to allow
the automata to process input words backwards as well, for example, to measure
the maximal or average time between a response and the preceding request. We therefore
introduce and study bidirectional NWA that can process input words in both directions.
First, we show that bidirectional NWA can express interesting quantitative properties
that are not expressible by forward-only NWA. Second, for the fundamental decision
problems of emptiness and universality, we establish decidability and complexity
results for the new framework which match the best-known results for the special
case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality
is achieved at no additional computational complexity. This is in stark contrast
to the unweighted case, where bidirectional finite automata are no more expressive
but exponentially more succinct than their forward-only counterparts.
alternative_title:
- LIPIcs
article_number: '5'
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
last_name: Otop
citation:
ama: 'Chatterjee K, Henzinger TA, Otop J. Bidirectional nested weighted automata.
In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.5'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2017). Bidirectional nested
weighted automata (Vol. 85). Presented at the 28th International Conference on
Concurrency Theory, CONCUR, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.5'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Bidirectional
Nested Weighted Automata,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2017. https://doi.org/10.4230/LIPIcs.CONCUR.2017.5.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Bidirectional nested weighted
automata,” presented at the 28th International Conference on Concurrency Theory,
CONCUR, Berlin, Germany, 2017, vol. 85.
ista: Chatterjee K, Henzinger TA, Otop J. 2017. Bidirectional nested weighted automata.
28th International Conference on Concurrency Theory, CONCUR, LIPIcs, vol. 85,
5.
mla: Chatterjee, Krishnendu, et al. Bidirectional Nested Weighted Automata.
Vol. 85, 5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.5.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2017.
conference:
end_date: 2017-09-08
location: Berlin, Germany
name: 28th International Conference on Concurrency Theory, CONCUR
start_date: 2017-09-05
date_created: 2018-12-11T11:48:04Z
date_published: 2017-08-01T00:00:00Z
date_updated: 2021-01-12T08:11:53Z
day: '01'
ddc:
- '004'
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2017.5
file:
- access_level: open_access
checksum: d2bda4783821a6358333fe27f11f4737
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:02Z
date_updated: 2020-07-14T12:47:49Z
file_id: '4661'
file_name: IST-2017-886-v1+1_LIPIcs-CONCUR-2017-5.pdf
file_size: 570294
relation: main_file
file_date_updated: 2020-07-14T12:47:49Z
has_accepted_license: '1'
intvolume: ' 85'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
publication_identifier:
issn:
- '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6976'
pubrep_id: '886'
quality_controlled: '1'
scopus_import: 1
status: public
title: Bidirectional nested weighted automata
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 85
year: '2017'
...
---
_id: '716'
abstract:
- lang: eng
text: 'Two-player games on graphs are central in many problems in formal verification
and program analysis, such as synthesis and verification of open systems. In this
work, we consider solving recursive game graphs (or pushdown game graphs) that
model the control flow of sequential programs with recursion.While pushdown games
have been studied before with qualitative objectives-such as reachability and
?-regular objectives- in this work, we study for the first time such games with
the most well-studied quantitative objective, the mean-payoff objective. In pushdown
games, two types of strategies are relevant: (1) global strategies, which depend
on the entire global history; and (2) modular strategies, which have only local
memory and thus do not depend on the context of invocation but rather only on
the history of the current invocation of the module. Our main results are as follows:
(1) One-player pushdown games with mean-payoff objectives under global strategies
are decidable in polynomial time. (2) Two-player pushdown games with mean-payoff
objectives under global strategies are undecidable. (3) One-player pushdown games
with mean-payoff objectives under modular strategies are NP-hard. (4) Two-player
pushdown games with mean-payoff objectives under modular strategies can be solved
in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives
under modular strategies are NP-complete). We also establish the optimal strategy
complexity by showing that global strategies for mean-payoff objectives require
infinite memory even in one-player pushdown games and memoryless modular strategies
are sufficient in two-player pushdown games. Finally, we also show that all the
problems have the same complexity if the stack boundedness condition is added,
where along with the mean-payoff objective the player must also ensure that the
stack height is bounded.'
article_type: original
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Velner Y. The complexity of mean-payoff pushdown games. Journal
of the ACM. 2017;64(5):34. doi:10.1145/3121408
apa: Chatterjee, K., & Velner, Y. (2017). The complexity of mean-payoff pushdown
games. Journal of the ACM. ACM. https://doi.org/10.1145/3121408
chicago: Chatterjee, Krishnendu, and Yaron Velner. “The Complexity of Mean-Payoff
Pushdown Games.” Journal of the ACM. ACM, 2017. https://doi.org/10.1145/3121408.
ieee: K. Chatterjee and Y. Velner, “The complexity of mean-payoff pushdown games,”
Journal of the ACM, vol. 64, no. 5. ACM, p. 34, 2017.
ista: Chatterjee K, Velner Y. 2017. The complexity of mean-payoff pushdown games.
Journal of the ACM. 64(5), 34.
mla: Chatterjee, Krishnendu, and Yaron Velner. “The Complexity of Mean-Payoff Pushdown
Games.” Journal of the ACM, vol. 64, no. 5, ACM, 2017, p. 34, doi:10.1145/3121408.
short: K. Chatterjee, Y. Velner, Journal of the ACM 64 (2017) 34.
date_created: 2018-12-11T11:48:06Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2021-01-12T08:12:08Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3121408
ec_funded: 1
external_id:
arxiv:
- '1201.2829'
intvolume: ' 64'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1201.2829
month: '09'
oa: 1
oa_version: Preprint
page: '34'
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Journal of the ACM
publication_identifier:
issn:
- '00045411'
publication_status: published
publisher: ACM
publist_id: '6964'
quality_controlled: '1'
scopus_import: 1
status: public
title: The complexity of mean-payoff pushdown games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 64
year: '2017'
...
---
_id: '717'
abstract:
- lang: eng
text: 'We consider finite-state and recursive game graphs with multidimensional
mean-payoff objectives. In recursive games two types of strategies are relevant:
global strategies and modular strategies. Our contributions are: (1) We show that
finite-state multidimensional mean-payoff games can be solved in polynomial time
if the number of dimensions and the maximal absolute value of weights are fixed;
whereas for arbitrary dimensions the problem is coNP-complete. (2) We show that
one-player recursive games with multidimensional mean-payoff objectives can be
solved in polynomial time. Both above algorithms are based on hyperplane separation
technique. (3) For recursive games we show that under modular strategies the multidimensional
problem is undecidable. We show that if the number of modules, exits, and the
maximal absolute value of the weights are fixed, then one-dimensional recursive
mean-payoff games under modular strategies can be solved in polynomial time, whereas
for unbounded number of exits or modules the problem is NP-hard.'
acknowledgement: 'The research was supported by Austrian Science Fund (FWF) Grant
No. P 23499-N23, FWF NFN Grant No. S11407-N23 (RiSE), ERC Start grant (279307: Graph
Games), Microsoft faculty fellows award, the RICH Model Toolkit (ICT COST Action
IC0901), and was carried out in partial fulfillment of the requirements for the
Ph.D. degree of the second author.'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Velner Y. Hyperplane separation technique for multidimensional
mean-payoff games. Journal of Computer and System Sciences. 2017;88:236-259.
doi:10.1016/j.jcss.2017.04.005
apa: Chatterjee, K., & Velner, Y. (2017). Hyperplane separation technique for
multidimensional mean-payoff games. Journal of Computer and System Sciences.
Academic Press. https://doi.org/10.1016/j.jcss.2017.04.005
chicago: Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique
for Multidimensional Mean-Payoff Games.” Journal of Computer and System Sciences.
Academic Press, 2017. https://doi.org/10.1016/j.jcss.2017.04.005.
ieee: K. Chatterjee and Y. Velner, “Hyperplane separation technique for multidimensional
mean-payoff games,” Journal of Computer and System Sciences, vol. 88. Academic
Press, pp. 236–259, 2017.
ista: Chatterjee K, Velner Y. 2017. Hyperplane separation technique for multidimensional
mean-payoff games. Journal of Computer and System Sciences. 88, 236–259.
mla: Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique
for Multidimensional Mean-Payoff Games.” Journal of Computer and System Sciences,
vol. 88, Academic Press, 2017, pp. 236–59, doi:10.1016/j.jcss.2017.04.005.
short: K. Chatterjee, Y. Velner, Journal of Computer and System Sciences 88 (2017)
236–259.
date_created: 2018-12-11T11:48:07Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-02-23T10:38:15Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.jcss.2017.04.005
ec_funded: 1
intvolume: ' 88'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1210.3141
month: '09'
oa: 1
oa_version: Preprint
page: 236 - 259
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Academic Press
publist_id: '6963'
quality_controlled: '1'
related_material:
record:
- id: '2329'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Hyperplane separation technique for multidimensional mean-payoff games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 88
year: '2017'
...
---
_id: '719'
abstract:
- lang: eng
text: 'The ubiquity of computation in modern machines and devices imposes a need
to assert the correctness of their behavior. Especially in the case of safety-critical
systems, their designers need to take measures that enforce their safe operation.
Formal methods has emerged as a research field that addresses this challenge:
by rigorously proving that all system executions adhere to their specifications,
the correctness of an implementation under concern can be assured. To achieve
this goal, a plethora of techniques are nowadays available, all of which are optimized
for different system types and application domains.'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rüdiger
full_name: Ehlers, Rüdiger
last_name: Ehlers
citation:
ama: 'Chatterjee K, Ehlers R. Special issue: Synthesis and SYNT 2014. Acta Informatica.
2017;54(6):543-544. doi:10.1007/s00236-017-0299-0'
apa: 'Chatterjee, K., & Ehlers, R. (2017). Special issue: Synthesis and SYNT
2014. Acta Informatica. Springer. https://doi.org/10.1007/s00236-017-0299-0'
chicago: 'Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis
and SYNT 2014.” Acta Informatica. Springer, 2017. https://doi.org/10.1007/s00236-017-0299-0.'
ieee: 'K. Chatterjee and R. Ehlers, “Special issue: Synthesis and SYNT 2014,” Acta
Informatica, vol. 54, no. 6. Springer, pp. 543–544, 2017.'
ista: 'Chatterjee K, Ehlers R. 2017. Special issue: Synthesis and SYNT 2014. Acta
Informatica. 54(6), 543–544.'
mla: 'Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis and
SYNT 2014.” Acta Informatica, vol. 54, no. 6, Springer, 2017, pp. 543–44,
doi:10.1007/s00236-017-0299-0.'
short: K. Chatterjee, R. Ehlers, Acta Informatica 54 (2017) 543–544.
date_created: 2018-12-11T11:48:07Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2021-01-12T08:12:18Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/s00236-017-0299-0
intvolume: ' 54'
issue: '6'
language:
- iso: eng
month: '09'
oa_version: None
page: 543 - 544
publication: Acta Informatica
publication_identifier:
issn:
- '00015903'
publication_status: published
publisher: Springer
publist_id: '6961'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Special issue: Synthesis and SYNT 2014'
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 54
year: '2017'
...
---
_id: '13160'
abstract:
- lang: eng
text: "Transforming deterministic ω\r\n-automata into deterministic parity automata
is traditionally done using variants of appearance records. We present a more
efficient variant of this approach, tailored to Rabin automata, and several optimizations
applicable to all appearance records. We compare the methods experimentally and
find out that our method produces smaller automata than previous approaches. Moreover,
the experiments demonstrate the potential of our method for LTL synthesis, using
LTL-to-Rabin translators. It leads to significantly smaller parity automata when
compared to state-of-the-art approaches on complex formulae."
acknowledgement: This work is partially funded by the DFG project “Verified Model
Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Clara
full_name: Waldmann, Clara
last_name: Waldmann
- first_name: Maximilian
full_name: Weininger, Maximilian
last_name: Weininger
citation:
ama: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
for transforming Rabin automata into parity automata. In: Tools and Algorithms
for the Construction and Analysis of Systems. Vol 10205. Springer; 2017:443-460.
doi:10.1007/978-3-662-54577-5_26'
apa: 'Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2017).
Index appearance record for transforming Rabin automata into parity automata.
In Tools and Algorithms for the Construction and Analysis of Systems (Vol.
10205, pp. 443–460). Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54577-5_26'
chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
“Index Appearance Record for Transforming Rabin Automata into Parity Automata.”
In Tools and Algorithms for the Construction and Analysis of Systems, 10205:443–60.
Springer, 2017. https://doi.org/10.1007/978-3-662-54577-5_26.
ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
record for transforming Rabin automata into parity automata,” in Tools and
Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden,
2017, vol. 10205, pp. 443–460.
ista: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance
record for transforming Rabin automata into parity automata. Tools and Algorithms
for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.'
mla: Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata
into Parity Automata.” Tools and Algorithms for the Construction and Analysis
of Systems, vol. 10205, Springer, 2017, pp. 443–60, doi:10.1007/978-3-662-54577-5_26.
short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and
Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2017-04-22
date_created: 2023-06-21T13:21:14Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2023-06-21T13:29:46Z
day: '31'
department:
- _id: KrCh
doi: 10.1007/978-3-662-54577-5_26
external_id:
arxiv:
- '1701.05738'
intvolume: ' 10205'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.1701.05738
month: '03'
oa: 1
oa_version: Preprint
page: 443-460
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783662545775'
eissn:
- 1611-3349
isbn:
- '9783662545768'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
status: public
title: Index appearance record for transforming Rabin automata into parity automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10205
year: '2017'
...
---
_id: '950'
abstract:
- lang: eng
text: "Two-player games on graphs are widely studied in formal methods as they model
the interaction between a system and its environment. The game is played by moving
a token throughout a graph to produce an infinite path. There are several common
modes to determine how the players move the token through the graph; e.g., in
turn-based games the players alternate turns in moving the token. We study the
bidding mode of moving the token, which, to the best of our knowledge, has never
been studied in infinite-duration games. Both players have separate budgets, which
sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously,
and a bid is legal if it does not exceed the available budget. The winner of the
bidding pays his bid to the other player and moves the token. For reachability
objectives, repeated bidding games have been studied and are called Richman games.
There, a central question is the existence and computation of threshold budgets;
namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win
the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity
games and mean-payoff games. We show the existence of threshold budgets in these
games, and reduce the problem of finding them to Richman games. We also determine
the strategy-complexity of an optimal strategy. Our most interesting result shows
that memoryless strategies suffice for mean-payoff bidding games. \r\n"
alternative_title:
- LIPIcs
article_number: '17'
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- 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: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
citation:
ama: 'Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol
85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.21'
apa: 'Avni, G., Henzinger, T. A., & Chonev, V. K. (2017). Infinite-duration
bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin,
Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21'
chicago: Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration
Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
https://doi.org/10.4230/LIPIcs.CONCUR.2017.21.
ieee: 'G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,”
presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.'
ista: 'Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR:
Concurrency Theory, LIPIcs, vol. 85, 17.'
mla: Avni, Guy, et al. Infinite-Duration Bidding Games. Vol. 85, 17, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.21.
short: G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2017.
conference:
end_date: 2017-09-07
location: Berlin, Germany
name: 'CONCUR: Concurrency Theory'
start_date: 2017-09-05
date_created: 2018-12-11T11:49:22Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-08-29T07:02:13Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2017.21
external_id:
arxiv:
- '1705.01433'
file:
- access_level: open_access
checksum: 6d5cccf755207b91ccbef95d8275b013
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:00Z
date_updated: 2020-07-14T12:48:16Z
file_id: '5318'
file_name: IST-2017-844-v1+1_concur-cr.pdf
file_size: 335170
relation: main_file
file_date_updated: 2020-07-14T12:48:16Z
has_accepted_license: '1'
intvolume: ' 85'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6466'
pubrep_id: '844'
quality_controlled: '1'
related_material:
record:
- id: '6752'
relation: later_version
status: public
scopus_import: 1
status: public
title: Infinite-duration bidding games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 85
year: '2017'
...
---
_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: '1407'
abstract:
- lang: eng
text: We consider the problem of computing the set of initial states of a dynamical
system such that there exists a control strategy to ensure that the trajectories
satisfy a temporal logic specification with probability 1 (almost-surely). We
focus on discrete-time, stochastic linear dynamics and specifications given as
formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over
linear predicates in the states of the system. We propose a solution based on
iterative abstraction-refinement, and turn-based 2-player probabilistic games.
While the theoretical guarantee of our algorithm after any finite number of iterations
is only a partial solution, we show that if our algorithm terminates, then the
result is the set of all satisfying initial states. Moreover, for any (partial)
solution our algorithm synthesizes witness control strategies to ensure almost-sure
satisfaction of the temporal logic specification. While the proposed algorithm
guarantees progress and soundness in every iteration, it is computationally demanding.
We offer an alternative, more efficient solution for the reachability properties
that decomposes the problem into a series of smaller problems of the same type.
All algorithms are demonstrated on an illustrative case study.
article_processing_charge: No
author:
- first_name: Mária
full_name: Svoreňová, Mária
last_name: Svoreňová
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ivana
full_name: Cěrná, Ivana
last_name: Cěrná
- first_name: Cǎlin
full_name: Belta, Cǎlin
last_name: Belta
citation:
ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal
logic control for stochastic linear systems using abstraction refinement of probabilistic
games. Nonlinear Analysis: Hybrid Systems. 2017;23(2):230-253. doi:10.1016/j.nahs.2016.04.006'
apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &
Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction
refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems.
Elsevier. https://doi.org/10.1016/j.nahs.2016.04.006'
chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee,
Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid
Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.04.006.'
ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta,
“Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games,” Nonlinear Analysis: Hybrid Systems, vol. 23, no.
2. Elsevier, pp. 230–253, 2017.'
ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017.
Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253.'
mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid
Systems, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:10.1016/j.nahs.2016.04.006.'
short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta,
Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.'
date_created: 2018-12-11T11:51:50Z
date_published: 2017-02-01T00:00:00Z
date_updated: 2023-09-20T09:43:09Z
day: '01'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1016/j.nahs.2016.04.006
ec_funded: 1
external_id:
arxiv:
- '1410.5387'
isi:
- '000390637000014'
intvolume: ' 23'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1410.5387
month: '02'
oa: 1
oa_version: Preprint
page: 230 - 253
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_status: published
publisher: Elsevier
publist_id: '5800'
quality_controlled: '1'
related_material:
record:
- id: '1689'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 23
year: '2017'
...
---
_id: '1294'
abstract:
- lang: eng
text: We study controller synthesis problems for finite-state Markov decision processes,
where the objective is to optimize the expected mean-payoff performance and stability
(also known as variability in the literature). We argue that the basic notion
of expressing the stability using the statistical variance of the mean payoff
is sometimes insufficient, and propose an alternative definition. We show that
a strategy ensuring both the expected mean payoff and the variance below given
bounds requires randomization and memory, under both the above definitions. We
then show that the problem of finding such a strategy can be expressed as a set
of constraints.
article_processing_charge: No
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
citation:
ama: Brázdil T, Chatterjee K, Forejt V, Kučera A. Trading performance for stability
in Markov decision processes. Journal of Computer and System Sciences.
2017;84:144-170. doi:10.1016/j.jcss.2016.09.009
apa: Brázdil, T., Chatterjee, K., Forejt, V., & Kučera, A. (2017). Trading performance
for stability in Markov decision processes. Journal of Computer and System
Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2016.09.009
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera.
“Trading Performance for Stability in Markov Decision Processes.” Journal of
Computer and System Sciences. Elsevier, 2017. https://doi.org/10.1016/j.jcss.2016.09.009.
ieee: T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Trading performance
for stability in Markov decision processes,” Journal of Computer and System
Sciences, vol. 84. Elsevier, pp. 144–170, 2017.
ista: Brázdil T, Chatterjee K, Forejt V, Kučera A. 2017. Trading performance for
stability in Markov decision processes. Journal of Computer and System Sciences.
84, 144–170.
mla: Brázdil, Tomáš, et al. “Trading Performance for Stability in Markov Decision
Processes.” Journal of Computer and System Sciences, vol. 84, Elsevier,
2017, pp. 144–70, doi:10.1016/j.jcss.2016.09.009.
short: T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, Journal of Computer and
System Sciences 84 (2017) 144–170.
date_created: 2018-12-11T11:51:12Z
date_published: 2017-03-01T00:00:00Z
date_updated: 2023-09-20T11:15:31Z
day: '01'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.1016/j.jcss.2016.09.009
ec_funded: 1
external_id:
isi:
- '000388430000011'
file:
- access_level: open_access
checksum: 91271b23cf884d7c06d33bef0cd623b1
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:30Z
date_updated: 2020-07-14T12:44:42Z
file_id: '4885'
file_name: IST-2016-717-v1+1_1-s2.0-S0022000016300897-main.pdf
file_size: 708657
relation: main_file
file_date_updated: 2020-07-14T12:44:42Z
has_accepted_license: '1'
intvolume: ' 84'
isi: 1
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: 144 - 170
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Elsevier
publist_id: '6009'
pubrep_id: '717'
quality_controlled: '1'
related_material:
record:
- id: '2305'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Trading performance for stability in Markov decision processes
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 84
year: '2017'
...
---
_id: '1080'
abstract:
- lang: eng
text: Reconstructing the evolutionary history of metastases is critical for understanding
their basic biological principles and has profound clinical implications. Genome-wide
sequencing data has enabled modern phylogenomic methods to accurately dissect
subclones and their phylogenies from noisy and impure bulk tumour samples at unprecedented
depth. However, existing methods are not designed to infer metastatic seeding
patterns. Here we develop a tool, called Treeomics, to reconstruct the phylogeny
of metastases and map subclones to their anatomic locations. Treeomics infers
comprehensive seeding patterns for pancreatic, ovarian, and prostate cancers.
Moreover, Treeomics correctly disambiguates true seeding patterns from sequencing
artifacts; 7% of variants were misclassified by conventional statistical methods.
These artifacts can skew phylogenies by creating illusory tumour heterogeneity
among distinct samples. In silico benchmarking on simulated tumour phylogenies
across a wide range of sample purities (15–95%) and sequencing depths (25-800
× ) demonstrates the accuracy of Treeomics compared with existing methods.
article_number: '14114'
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
- first_name: Alvin
full_name: Makohon Moore, Alvin
last_name: Makohon Moore
- first_name: Jeffrey
full_name: Gerold, Jeffrey
last_name: Gerold
- first_name: Ivana
full_name: Božić, Ivana
last_name: Božić
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Christine
full_name: Iacobuzio Donahue, Christine
last_name: Iacobuzio Donahue
- first_name: Bert
full_name: Vogelstein, Bert
last_name: Vogelstein
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Reiter J, Makohon Moore A, Gerold J, et al. Reconstructing metastatic seeding
patterns of human cancers. Nature Communications. 2017;8. doi:10.1038/ncomms14114
apa: Reiter, J., Makohon Moore, A., Gerold, J., Božić, I., Chatterjee, K., Iacobuzio
Donahue, C., … Nowak, M. (2017). Reconstructing metastatic seeding patterns of
human cancers. Nature Communications. Nature Publishing Group. https://doi.org/10.1038/ncomms14114
chicago: Reiter, Johannes, Alvin Makohon Moore, Jeffrey Gerold, Ivana Božić, Krishnendu
Chatterjee, Christine Iacobuzio Donahue, Bert Vogelstein, and Martin Nowak. “Reconstructing
Metastatic Seeding Patterns of Human Cancers.” Nature Communications. Nature
Publishing Group, 2017. https://doi.org/10.1038/ncomms14114.
ieee: J. Reiter et al., “Reconstructing metastatic seeding patterns of human
cancers,” Nature Communications, vol. 8. Nature Publishing Group, 2017.
ista: Reiter J, Makohon Moore A, Gerold J, Božić I, Chatterjee K, Iacobuzio Donahue
C, Vogelstein B, Nowak M. 2017. Reconstructing metastatic seeding patterns of
human cancers. Nature Communications. 8, 14114.
mla: Reiter, Johannes, et al. “Reconstructing Metastatic Seeding Patterns of Human
Cancers.” Nature Communications, vol. 8, 14114, Nature Publishing Group,
2017, doi:10.1038/ncomms14114.
short: J. Reiter, A. Makohon Moore, J. Gerold, I. Božić, K. Chatterjee, C. Iacobuzio
Donahue, B. Vogelstein, M. Nowak, Nature Communications 8 (2017).
date_created: 2018-12-11T11:50:02Z
date_published: 2017-01-31T00:00:00Z
date_updated: 2023-09-20T11:55:31Z
day: '31'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.1038/ncomms14114
ec_funded: 1
external_id:
isi:
- '000393096600001'
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:15Z
date_updated: 2018-12-12T10:15:15Z
file_id: '5133'
file_name: IST-2017-786-v1+1_ncomms14114.pdf
file_size: 897050
relation: main_file
file_date_updated: 2018-12-12T10:15:15Z
has_accepted_license: '1'
intvolume: ' 8'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: Nature Communications
publication_identifier:
issn:
- '20411723'
publication_status: published
publisher: Nature Publishing Group
publist_id: '6301'
pubrep_id: '786'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reconstructing metastatic seeding patterns of human cancers
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 8
year: '2017'
...
---
_id: '1065'
abstract:
- lang: eng
text: 'We consider the problem of reachability in pushdown graphs. We study the
problem for pushdown graphs with constant treewidth. Even for pushdown graphs
with treewidth 1, for the reachability problem we establish the following: (i)
the problem is PTIME-complete, and (ii) any subcubic algorithm for the problem
would contradict the k-clique conjecture and imply faster combinatorial algorithms
for cliques in graphs.'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Georg F
full_name: Osang, Georg F
id: 464B40D6-F248-11E8-B48F-1D18A9856A87
last_name: Osang
orcid: 0000-0002-8882-5116
citation:
ama: Chatterjee K, Osang GF. Pushdown reachability with constant treewidth. Information
Processing Letters. 2017;122:25-29. doi:10.1016/j.ipl.2017.02.003
apa: Chatterjee, K., & Osang, G. F. (2017). Pushdown reachability with constant
treewidth. Information Processing Letters. Elsevier. https://doi.org/10.1016/j.ipl.2017.02.003
chicago: Chatterjee, Krishnendu, and Georg F Osang. “Pushdown Reachability with
Constant Treewidth.” Information Processing Letters. Elsevier, 2017. https://doi.org/10.1016/j.ipl.2017.02.003.
ieee: K. Chatterjee and G. F. Osang, “Pushdown reachability with constant treewidth,”
Information Processing Letters, vol. 122. Elsevier, pp. 25–29, 2017.
ista: Chatterjee K, Osang GF. 2017. Pushdown reachability with constant treewidth.
Information Processing Letters. 122, 25–29.
mla: Chatterjee, Krishnendu, and Georg F. Osang. “Pushdown Reachability with Constant
Treewidth.” Information Processing Letters, vol. 122, Elsevier, 2017, pp.
25–29, doi:10.1016/j.ipl.2017.02.003.
short: K. Chatterjee, G.F. Osang, Information Processing Letters 122 (2017) 25–29.
date_created: 2018-12-11T11:49:57Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-09-20T12:08:18Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: HeEd
doi: 10.1016/j.ipl.2017.02.003
ec_funded: 1
external_id:
isi:
- '000399506600005'
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:17Z
date_updated: 2019-10-15T07:44:51Z
file_id: '4998'
file_name: IST-2018-991-v1+2_2018_Chatterjee_Pushdown_PREPRINT.pdf
file_size: 247657
relation: main_file
file_date_updated: 2019-10-15T07:44:51Z
has_accepted_license: '1'
intvolume: ' 122'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 25 - 29
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Information Processing Letters
publication_identifier:
issn:
- '00200190'
publication_status: published
publisher: Elsevier
publist_id: '6323'
pubrep_id: '991'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Pushdown reachability with constant treewidth
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 122
year: '2017'
...
---
_id: '1066'
abstract:
- lang: eng
text: "Simulation is an attractive alternative to language inclusion for automata
as it is an under-approximation of language inclusion, but usually has much lower
complexity. Simulation has also been extended in two orthogonal directions, namely,
(1) fair simulation, for simulation over specified set of infinite runs; and (2)
quantitative simulation, for simulation between weighted automata. While fair
trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial
time. For weighted automata, the (quantitative) language inclusion problem is
undecidable in general, whereas the (quantitative) simulation reduces to quantitative
games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we
study (quantitative) simulation for weighted automata with Büchi acceptance conditions,
i.e., we generalize fair simulation from non-weighted automata to weighted automata.
We show that imposing Büchi acceptance conditions on weighted automata changes
many fundamental properties of the simulation games, yet they still admit pseudo-polynomial
time algorithms."
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: 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
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation
games. Information and Computation. 2017;254(2):143-166. doi:10.1016/j.ic.2016.10.006
apa: Chatterjee, K., Henzinger, T. A., Otop, J., & Velner, Y. (2017). Quantitative
fair simulation games. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2016.10.006
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner.
“Quantitative Fair Simulation Games.” Information and Computation. Elsevier,
2017. https://doi.org/10.1016/j.ic.2016.10.006.
ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair
simulation games,” Information and Computation, vol. 254, no. 2. Elsevier,
pp. 143–166, 2017.
ista: Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation
games. Information and Computation. 254(2), 143–166.
mla: Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” Information
and Computation, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:10.1016/j.ic.2016.10.006.
short: K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation
254 (2017) 143–166.
date_created: 2018-12-11T11:49:58Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-09-20T12:07:48Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2016.10.006
ec_funded: 1
external_id:
isi:
- '000402025600002'
intvolume: ' 254'
isi: 1
issue: '2'
language:
- iso: eng
month: '06'
oa_version: None
page: 143 - 166
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '6322'
quality_controlled: '1'
related_material:
record:
- id: '5428'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Quantitative fair simulation games
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 254
year: '2017'
...
---
_id: '1011'
abstract:
- lang: eng
text: Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly
equivalent, are standard models for interprocedural analysis. Yet RSMs are more
convenient as they (a) explicitly model function calls and returns, and (b) specify
many natural parameters for algorithmic analysis, e.g., the number of entries
and exits. We consider a general framework where RSM transitions are labeled from
a semiring and path properties are algebraic with semiring operations, which can
model, e.g., interprocedural reachability and dataflow analysis problems. Our
main contributions are new algorithms for several fundamental problems. As compared
to a direct translation of RSMs to PDSs and the best-known existing bounds of
PDSs, our analysis algorithm improves the complexity for finite-height semirings
(that subsumes reachability and standard dataflow properties). We further consider
the problem of extracting distance values from the representation structures computed
by our algorithm, and give efficient algorithms that distinguish the complexity
of a one-time preprocessing from the complexity of each individual query. Another
advantage of our algorithm is that our improvements carry over to the concurrent
setting, where we improve the bestknown complexity for the context-bounded analysis
of concurrent RSMs. Finally, we provide a prototype implementation that gives
a significant speed-up on several benchmarks from the SLAM/SDV project.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
orcid: 0000-0001-7745-9117
- first_name: Samarth
full_name: Mishra, Samarth
last_name: Mishra
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 'Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted
recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:10.1007/978-3-662-54434-1_11'
apa: 'Chatterjee, K., Kragl, B., Mishra, S., & Pavlogiannis, A. (2017). Faster
algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201,
pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala,
Sweden: Springer. https://doi.org/10.1007/978-3-662-54434-1_11'
chicago: Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis.
“Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok
Yang, 10201:287–313. Springer, 2017. https://doi.org/10.1007/978-3-662-54434-1_11.
ieee: 'K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms
for weighted recursive state machines,” presented at the ESOP: European Symposium
on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.'
ista: 'Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms
for weighted recursive state machines. ESOP: European Symposium on Programming,
LNCS, vol. 10201, 287–313.'
mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Weighted Recursive
State Machines. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313,
doi:10.1007/978-3-662-54434-1_11.
short: K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.),
Springer, 2017, pp. 287–313.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'ESOP: European Symposium on Programming'
start_date: 2017-04-22
date_created: 2018-12-11T11:49:41Z
date_published: 2017-03-19T00:00:00Z
date_updated: 2023-09-22T09:44:50Z
day: '19'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-54434-1_11
ec_funded: 1
editor:
- first_name: Hongseok
full_name: Yang, Hongseok
last_name: Yang
external_id:
isi:
- '000681702400011'
intvolume: ' 10201'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1701.04914
month: '03'
oa: 1
oa_version: Submitted Version
page: 287 - 313
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6384'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for weighted recursive state machines
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10201
year: '2017'
...
---
_id: '1009'
abstract:
- lang: eng
text: A standard objective in partially-observable Markov decision processes (POMDPs)
is to find a policy that maximizes the expected discounted-sum payoff. However,
such policies may still permit unlikely but highly undesirable outcomes, which
is problematic especially in safety-critical applications. Recently, there has
been a surge of interest in POMDPs where the goal is to maximize the probability
to ensure that the payoff is at least a given threshold, but these approaches
do not consider any optimization beyond satisfying this threshold constraint.
In this work we go beyond both the “expectation” and “threshold” approaches and
consider a “guaranteed payoff optimization (GPO)” problem for POMDPs, where we
are given a threshold t and the objective is to find a policy σ such that a) each
possible outcome of σ yields a discounted-sum payoff of at least t, and b) the
expected discounted-sum payoff of σ is optimal (or near-optimal) among all policies
satisfying a). We present a practical approach to tackle the GPO problem and evaluate
it on standard POMDP benchmarks.
acknowledgement: 'he research leading to these results was supported by the Austrian
Science Fund (FWF) NFN Grant no. S11407-N23 (RiSE/SHiNE); two ERC Starting grants
(279307: Graph Games, 279499: inVEST); the Vienna Science and Tech- nology Fund
(WWTF) through project ICT15-003; and the People Programme (Marie Curie Actions)
of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant
agreement no. [291734].'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Guillermo
full_name: Pérez, Guillermo
last_name: Pérez
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
- first_name: Djordje
full_name: Zikelic, Djordje
last_name: Zikelic
citation:
ama: 'Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. Optimizing expectation
with guarantees in POMDPs. In: Proceedings of the 31st AAAI Conference on Artificial
Intelligence. Vol 5. AAAI Press; 2017:3725-3732.'
apa: 'Chatterjee, K., Novotný, P., Pérez, G., Raskin, J., & Zikelic, D. (2017).
Optimizing expectation with guarantees in POMDPs. In Proceedings of the 31st
AAAI Conference on Artificial Intelligence (Vol. 5, pp. 3725–3732). San Francisco,
CA, United States: AAAI Press.'
chicago: Chatterjee, Krishnendu, Petr Novotný, Guillermo Pérez, Jean Raskin, and
Djordje Zikelic. “Optimizing Expectation with Guarantees in POMDPs.” In Proceedings
of the 31st AAAI Conference on Artificial Intelligence, 5:3725–32. AAAI Press,
2017.
ieee: K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, and D. Zikelic, “Optimizing
expectation with guarantees in POMDPs,” in Proceedings of the 31st AAAI Conference
on Artificial Intelligence, San Francisco, CA, United States, 2017, vol. 5,
pp. 3725–3732.
ista: 'Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. 2017. Optimizing expectation
with guarantees in POMDPs. Proceedings of the 31st AAAI Conference on Artificial
Intelligence. AAAI: Conference on Artificial Intelligence vol. 5, 3725–3732.'
mla: Chatterjee, Krishnendu, et al. “Optimizing Expectation with Guarantees in POMDPs.”
Proceedings of the 31st AAAI Conference on Artificial Intelligence, vol.
5, AAAI Press, 2017, pp. 3725–32.
short: K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, D. Zikelic, in:, Proceedings
of the 31st AAAI Conference on Artificial Intelligence, AAAI Press, 2017, pp.
3725–3732.
conference:
end_date: 2017-02-10
location: San Francisco, CA, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2017-02-04
date_created: 2018-12-11T11:49:40Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2023-09-22T09:46:41Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
external_id:
isi:
- '000485630703107'
intvolume: ' 5'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://www.aaai.org/ocs/index.php/AAAI/AAAI17/paper/download/14354/14092
month: '01'
oa: 1
oa_version: Submitted Version
page: 3725 - 3732
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the 31st AAAI Conference on Artificial Intelligence
publication_status: published
publisher: AAAI Press
publist_id: '6387'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Optimizing expectation with guarantees in POMDPs
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 5
year: '2017'
...
---
_id: '744'
abstract:
- lang: eng
text: In evolutionary game theory interactions between individuals are often assumed
obligatory. However, in many real-life situations, individuals can decide to opt
out of an interaction depending on the information they have about the opponent.
We consider a simple evolutionary game theoretic model to study such a scenario,
where at each encounter between two individuals the type of the opponent (cooperator/defector)
is known with some probability, and where each individual either accepts or opts
out of the interaction. If the type of the opponent is unknown, a trustful individual
accepts the interaction, whereas a suspicious individual opts out of the interaction.
If either of the two individuals opt out both individuals remain without an interaction.
We show that in the prisoners dilemma optional interactions along with suspicious
behaviour facilitates the emergence of trustful cooperation.
article_processing_charge: No
article_type: original
author:
- first_name: Tadeas
full_name: Priklopil, Tadeas
id: 3C869AA0-F248-11E8-B48F-1D18A9856A87
last_name: Priklopil
- 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: Priklopil T, Chatterjee K, Nowak M. Optional interactions and suspicious behaviour
facilitates trustful cooperation in prisoners dilemma. Journal of Theoretical
Biology. 2017;433:64-72. doi:10.1016/j.jtbi.2017.08.025
apa: Priklopil, T., Chatterjee, K., & Nowak, M. (2017). Optional interactions
and suspicious behaviour facilitates trustful cooperation in prisoners dilemma.
Journal of Theoretical Biology. Elsevier. https://doi.org/10.1016/j.jtbi.2017.08.025
chicago: Priklopil, Tadeas, Krishnendu Chatterjee, and Martin Nowak. “Optional Interactions
and Suspicious Behaviour Facilitates Trustful Cooperation in Prisoners Dilemma.”
Journal of Theoretical Biology. Elsevier, 2017. https://doi.org/10.1016/j.jtbi.2017.08.025.
ieee: T. Priklopil, K. Chatterjee, and M. Nowak, “Optional interactions and suspicious
behaviour facilitates trustful cooperation in prisoners dilemma,” Journal
of Theoretical Biology, vol. 433. Elsevier, pp. 64–72, 2017.
ista: Priklopil T, Chatterjee K, Nowak M. 2017. Optional interactions and suspicious
behaviour facilitates trustful cooperation in prisoners dilemma. Journal of Theoretical
Biology. 433, 64–72.
mla: Priklopil, Tadeas, et al. “Optional Interactions and Suspicious Behaviour Facilitates
Trustful Cooperation in Prisoners Dilemma.” Journal of Theoretical Biology,
vol. 433, Elsevier, 2017, pp. 64–72, doi:10.1016/j.jtbi.2017.08.025.
short: T. Priklopil, K. Chatterjee, M. Nowak, Journal of Theoretical Biology 433
(2017) 64–72.
date_created: 2018-12-11T11:48:16Z
date_published: 2017-11-21T00:00:00Z
date_updated: 2023-09-27T12:29:02Z
day: '21'
ddc:
- '000'
- '570'
department:
- _id: KrCh
doi: 10.1016/j.jtbi.2017.08.025
ec_funded: 1
external_id:
isi:
- '000412039800007'
pmid:
- '28867224'
file:
- access_level: open_access
checksum: 4b43af1615ebf1a861840cb03d8a320c
content_type: application/pdf
creator: dernst
date_created: 2019-11-19T07:57:39Z
date_updated: 2020-07-14T12:47:58Z
file_id: '7047'
file_name: 2017_JournTheoretBio_Priklopil.pdf
file_size: 537323
relation: main_file
file_date_updated: 2020-07-14T12:47:58Z
has_accepted_license: '1'
intvolume: ' 433'
isi: 1
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 64 - 72
pmid: 1
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: ' Journal of Theoretical Biology'
publication_identifier:
issn:
- '00225193'
publication_status: published
publisher: Elsevier
publist_id: '6923'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Optional interactions and suspicious behaviour facilitates trustful cooperation
in prisoners dilemma
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 433
year: '2017'
...
---
_id: '1194'
abstract:
- lang: eng
text: 'Termination is one of the basic liveness properties, and we study the termination
problem for probabilistic programs with real-valued variables. Previous works
focused on the qualitative problem that asks whether an input program terminates
with probability~1 (almost-sure termination). A powerful approach for this qualitative
problem is the notion of ranking supermartingales with respect to a given set
of invariants. The quantitative problem (probabilistic termination) asks for bounds
on the termination probability. A fundamental and conceptual drawback of the existing
approaches to address probabilistic termination is that even though the supermartingales
consider the probabilistic behavior of the programs, the invariants are obtained
completely ignoring the probabilistic aspect. In this work we address the probabilistic
termination problem for linear-arithmetic probabilistic programs with nondeterminism.
We define the notion of {\em stochastic invariants}, which are constraints along
with a probability bound that the constraints hold. We introduce a concept of
{\em repulsing supermartingales}. First, we show that repulsing supermartingales
can be used to obtain bounds on the probability of the stochastic invariants.
Second, we show the effectiveness of repulsing supermartingales in the following
three ways: (1)~With a combination of ranking and repulsing supermartingales we
can compute lower bounds on the probability of termination; (2)~repulsing supermartingales
provide witnesses for refutation of almost-sure termination; and (3)~with a combination
of ranking and repulsing supermartingales we can establish persistence properties
of probabilistic programs. We also present results on related computational problems
and an experimental evaluation of our approach on academic examples. '
alternative_title:
- ACM SIGPLAN Notices
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Djordje
full_name: Zikelic, Djordje
last_name: Zikelic
citation:
ama: 'Chatterjee K, Novotný P, Zikelic D. Stochastic invariants for probabilistic
termination. In: Vol 52. ACM; 2017:145-160. doi:10.1145/3009837.3009873'
apa: 'Chatterjee, K., Novotný, P., & Zikelic, D. (2017). Stochastic invariants
for probabilistic termination (Vol. 52, pp. 145–160). Presented at the POPL: Principles
of Programming Languages, Paris, France: ACM. https://doi.org/10.1145/3009837.3009873'
chicago: Chatterjee, Krishnendu, Petr Novotný, and Djordje Zikelic. “Stochastic
Invariants for Probabilistic Termination,” 52:145–60. ACM, 2017. https://doi.org/10.1145/3009837.3009873.
ieee: 'K. Chatterjee, P. Novotný, and D. Zikelic, “Stochastic invariants for probabilistic
termination,” presented at the POPL: Principles of Programming Languages, Paris,
France, 2017, vol. 52, no. 1, pp. 145–160.'
ista: 'Chatterjee K, Novotný P, Zikelic D. 2017. Stochastic invariants for probabilistic
termination. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol.
52, 145–160.'
mla: Chatterjee, Krishnendu, et al. Stochastic Invariants for Probabilistic Termination.
Vol. 52, no. 1, ACM, 2017, pp. 145–60, doi:10.1145/3009837.3009873.
short: K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.
conference:
end_date: 2017-01-21
location: Paris, France
name: 'POPL: Principles of Programming Languages'
start_date: 2017-01-15
date_created: 2018-12-11T11:50:39Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2023-11-30T10:55:36Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3009837.3009873
ec_funded: 1
external_id:
isi:
- '000408311200013'
intvolume: ' 52'
isi: 1
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1611.01063
month: '01'
oa: 1
oa_version: Submitted Version
page: 145 - 160
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_identifier:
issn:
- '07308566'
publication_status: published
publisher: ACM
publist_id: '6157'
quality_controlled: '1'
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Stochastic invariants for probabilistic termination
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 52
year: '2017'
...
---
_id: '5559'
abstract:
- lang: eng
text: Strong amplifiers of natural selection
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
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- 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. 2017. doi:10.15479/AT:ISTA:51
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak , M. (2017). Strong
amplifiers of natural selection. Institute of Science and Technology Austria.
https://doi.org/10.15479/AT:ISTA:51
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak . “Strong Amplifiers of Natural Selection.” Institute of Science and Technology
Austria, 2017. https://doi.org/10.15479/AT:ISTA:51.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak , “Strong amplifiers
of natural selection.” Institute of Science and Technology Austria, 2017.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Strong amplifiers
of natural selection, Institute of Science and Technology Austria, 10.15479/AT:ISTA:51.
mla: Pavlogiannis, Andreas, et al. Strong Amplifiers of Natural Selection.
Institute of Science and Technology Austria, 2017, doi:10.15479/AT:ISTA:51.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak , (2017).
datarep_id: '51'
date_created: 2018-12-12T12:31:32Z
date_published: 2017-01-02T00:00:00Z
date_updated: 2024-02-21T13:48:42Z
day: '02'
ddc:
- '519'
department:
- _id: KrCh
doi: 10.15479/AT:ISTA:51
ec_funded: 1
file:
- access_level: open_access
checksum: b427dd46a30096a1911b245640c47af8
content_type: video/mp4
creator: system
date_created: 2018-12-12T13:05:18Z
date_updated: 2020-07-14T12:47:02Z
file_id: '5644'
file_name: IST-2017-51-v1+2_illustration.mp4
file_size: 32987015
relation: main_file
file_date_updated: 2020-07-14T12:47:02Z
has_accepted_license: '1'
keyword:
- natural selection
month: '01'
oa: 1
oa_version: Published Version
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '5452'
relation: research_paper
status: public
- id: '5751'
relation: research_paper
status: public
status: public
title: Strong amplifiers of natural selection
type: research_data
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...
---
_id: '639'
abstract:
- lang: eng
text: We study the problem of developing efficient approaches for proving worst-case
bounds of non-deterministic recursive programs. Ranking functions are sound and
complete for proving termination and worst-case bounds of non-recursive programs.
First, we apply ranking functions to recursion, resulting in measure functions,
and show that they provide a sound and complete approach to prove worst-case bounds
of non-deterministic recursive programs. Our second contribution is the synthesis
of measure functions in non-polynomial forms. We show that non-polynomial measure
functions with logarithm and exponentiation can be synthesized through abstraction
of logarithmic or exponentiation terms, Farkas’ Lemma, and Handelman’s Theorem
using linear programming. While previous methods obtain worst-case polynomial
bounds, our approach can synthesize bounds of the form O(n log n) as well as O(nr)
where r is not an integer. We present experimental results to demonstrate that
our approach can efficiently obtain worst-case bounds of classical recursive algorithms
such as Merge-Sort, Closest-Pair, Karatsuba’s algorithm and Strassen’s algorithm.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Hongfei
full_name: Fu, Hongfei
last_name: Fu
- first_name: Amir
full_name: Goharshady, Amir
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
citation:
ama: 'Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst case analysis of recursive
programs. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:41-63. doi:10.1007/978-3-319-63390-9_3'
apa: 'Chatterjee, K., Fu, H., & Goharshady, A. K. (2017). Non-polynomial worst
case analysis of recursive programs. In R. Majumdar & V. Kunčak (Eds.) (Vol.
10427, pp. 41–63). Presented at the CAV: Computer Aided Verification, Heidelberg,
Germany: Springer. https://doi.org/10.1007/978-3-319-63390-9_3'
chicago: Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial
Worst Case Analysis of Recursive Programs.” edited by Rupak Majumdar and Viktor
Kunčak, 10427:41–63. Springer, 2017. https://doi.org/10.1007/978-3-319-63390-9_3.
ieee: 'K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst case analysis
of recursive programs,” presented at the CAV: Computer Aided Verification, Heidelberg,
Germany, 2017, vol. 10427, pp. 41–63.'
ista: 'Chatterjee K, Fu H, Goharshady AK. 2017. Non-polynomial worst case analysis
of recursive programs. CAV: Computer Aided Verification, LNCS, vol. 10427, 41–63.'
mla: Chatterjee, Krishnendu, et al. Non-Polynomial Worst Case Analysis of Recursive
Programs. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer,
2017, pp. 41–63, doi:10.1007/978-3-319-63390-9_3.
short: K. Chatterjee, H. Fu, A.K. Goharshady, in:, R. Majumdar, V. Kunčak (Eds.),
Springer, 2017, pp. 41–63.
conference:
end_date: 2017-07-28
location: Heidelberg, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2017-07-24
date_created: 2018-12-11T11:47:39Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2024-03-28T23:30:33Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-319-63390-9_3
ec_funded: 1
editor:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Viktor
full_name: Kunčak, Viktor
last_name: Kunčak
external_id:
arxiv:
- '1705.00317'
intvolume: ' 10427'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1705.00317
month: '01'
oa: 1
oa_version: Submitted Version
page: 41 - 63
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
isbn:
- 978-331963389-3
publication_status: published
publisher: Springer
publist_id: '7149'
quality_controlled: '1'
related_material:
record:
- id: '7014'
relation: later_version
status: public
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Non-polynomial worst case analysis of recursive programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10427
year: '2017'
...
---
_id: '949'
abstract:
- lang: eng
text: The notion of treewidth of graphs has been exploited for faster algorithms
for several problems arising in verification and program analysis. Moreover, various
notions of balanced tree decompositions have been used for improved algorithms
supporting dynamic updates and analysis of concurrent programs. In this work,
we present a tool for constructing tree-decompositions of CFGs obtained from Java
methods, which is implemented as an extension to the widely used Soot framework.
The experimental results show that our implementation on real-world Java benchmarks
is very efficient. Our tool also provides the first implementation for balancing
tree-decompositions. In summary, we present the first tool support for exploiting
treewidth in the static analysis problems on Java programs.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir
full_name: Goharshady, Amir
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 'Chatterjee K, Goharshady AK, Pavlogiannis A. JTDec: A tool for tree decompositions
in soot. In: D’Souza D, ed. Vol 10482. Springer; 2017:59-66. doi:10.1007/978-3-319-68167-2_4'
apa: 'Chatterjee, K., Goharshady, A. K., & Pavlogiannis, A. (2017). JTDec: A
tool for tree decompositions in soot. In D. D’Souza (Ed.) (Vol. 10482, pp. 59–66).
Presented at the ATVA: Automated Technology for Verification and Analysis, Pune,
India: Springer. https://doi.org/10.1007/978-3-319-68167-2_4'
chicago: 'Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Andreas Pavlogiannis.
“JTDec: A Tool for Tree Decompositions in Soot.” edited by Deepak D’Souza, 10482:59–66.
Springer, 2017. https://doi.org/10.1007/978-3-319-68167-2_4.'
ieee: 'K. Chatterjee, A. K. Goharshady, and A. Pavlogiannis, “JTDec: A tool for
tree decompositions in soot,” presented at the ATVA: Automated Technology for
Verification and Analysis, Pune, India, 2017, vol. 10482, pp. 59–66.'
ista: 'Chatterjee K, Goharshady AK, Pavlogiannis A. 2017. JTDec: A tool for tree
decompositions in soot. ATVA: Automated Technology for Verification and Analysis,
LNCS, vol. 10482, 59–66.'
mla: 'Chatterjee, Krishnendu, et al. JTDec: A Tool for Tree Decompositions in
Soot. Edited by Deepak D’Souza, vol. 10482, Springer, 2017, pp. 59–66, doi:10.1007/978-3-319-68167-2_4.'
short: K. Chatterjee, A.K. Goharshady, A. Pavlogiannis, in:, D. D’Souza (Ed.), Springer,
2017, pp. 59–66.
conference:
end_date: 2017-10-06
location: Pune, India
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2017-10-03
date_created: 2018-12-11T11:49:22Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2024-03-28T23:30:35Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.1007/978-3-319-68167-2_4
ec_funded: 1
editor:
- first_name: Deepak
full_name: D'Souza, Deepak
last_name: D'Souza
external_id:
isi:
- '000723567800004'
file:
- access_level: open_access
checksum: a0d9f5f94dc594c4e71e78525c9942f1
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:45Z
date_updated: 2020-07-14T12:48:16Z
file_id: '4835'
file_name: IST-2017-845-v1+1_2017_Chatterjee_JTDec.pdf
file_size: 948514
relation: main_file
file_date_updated: 2020-07-14T12:48:16Z
has_accepted_license: '1'
intvolume: ' 10482'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 59 - 66
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6468'
pubrep_id: '845'
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: 'JTDec: A tool for tree decompositions in soot'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10482
year: '2017'
...
---
_id: '1068'
abstract:
- lang: eng
text: 'Games on graphs provide the appropriate framework to study several central
problems in computer science, such as verification and synthesis of reactive systems.
One of the most basic objectives for games on graphs is the liveness (or Büchi)
objective that given a target set of vertices requires that some vertex in the
target set is visited infinitely often. We study generalized Büchi objectives
(i.e., conjunction of liveness objectives), and implications between two generalized
Büchi objectives (known as GR(1) objectives), that arise in numerous applications
in computer-aided verification. We present improved algorithms and conditional
super-linear lower bounds based on widely believed assumptions about the complexity
of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider
graph games with n vertices, m edges, and generalized Büchi objectives with k
conjunctions. First, we present an algorithm with running time O(k*n^2), improving
the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm
is optimal for dense graphs under (A1). Second, we show that the basic algorithm
for the problem is optimal for sparse graphs when the target sets have constant
size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions
in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1
k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time
algorithm for m > n^{1.5}. '
acknowledgement: K. C., M. H., and W. D. are partially supported by the Vienna Science
and Technology Fund (WWTF) through project ICT15-003. K. C. is partially supported
by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC
Start grant (279307
alternative_title:
- LIPIcs
article_number: '25'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Wolfgang
full_name: Dvorák, Wolfgang
last_name: Dvorák
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Veronika
full_name: Loitzenbauer, Veronika
last_name: Loitzenbauer
citation:
ama: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. Conditionally optimal
algorithms for generalized Büchi Games. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2016. doi:10.4230/LIPIcs.MFCS.2016.25'
apa: 'Chatterjee, K., Dvorák, W., Henzinger, M. H., & Loitzenbauer, V. (2016).
Conditionally optimal algorithms for generalized Büchi Games (Vol. 58). Presented
at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow, Poland:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2016.25'
chicago: Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Veronika
Loitzenbauer. “Conditionally Optimal Algorithms for Generalized Büchi Games,”
Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.MFCS.2016.25.
ieee: 'K. Chatterjee, W. Dvorák, M. H. Henzinger, and V. Loitzenbauer, “Conditionally
optimal algorithms for generalized Büchi Games,” presented at the MFCS: Mathematical
Foundations of Computer Science (SG), Krakow, Poland, 2016, vol. 58.'
ista: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. 2016. Conditionally
optimal algorithms for generalized Büchi Games. MFCS: Mathematical Foundations
of Computer Science (SG), LIPIcs, vol. 58, 25.'
mla: Chatterjee, Krishnendu, et al. Conditionally Optimal Algorithms for Generalized
Büchi Games. Vol. 58, 25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016, doi:10.4230/LIPIcs.MFCS.2016.25.
short: K. Chatterjee, W. Dvorák, M.H. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Krakow, Poland
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2016-08-22
date_created: 2018-12-11T11:49:58Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-02-14T10:11:07Z
day: '01'
ddc:
- '000'
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.MFCS.2016.25
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:02Z
date_updated: 2018-12-12T10:16:02Z
file_id: '5187'
file_name: IST-2017-779-v1+1_LIPIcs-MFCS-2016-25.pdf
file_size: 632786
relation: main_file
file_date_updated: 2018-12-12T10:16:02Z
has_accepted_license: '1'
intvolume: ' 58'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided 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_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6317'
pubrep_id: '779'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Conditionally optimal algorithms for generalized Büchi Games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 58
year: '2016'
...
---
_id: '1069'
abstract:
- lang: eng
text: "The Continuous Skolem Problem asks whether a real-valued function satisfying
a linear differen-\r\ntial equation has a zero in a given interval of real numbers.
This is a fundamental reachability\r\nproblem for continuous linear dynamical
systems, such as linear hybrid automata and continuous-\r\ntime Markov chains.
Decidability of the problem is currently open – indeed decidability is open\r\neven
for the sub-problem in which a zero is sought in a bounded interval. In this paper
we show\r\ndecidability of the bounded problem subject to Schanuel’s Conjecture,
a unifying conjecture in\r\ntranscendental number theory. We furthermore analyse
the unbounded problem in terms of the\r\nfrequencies of the differential equation,
that is, the imaginary parts of the characteristic roots.\r\nWe show that the
unbounded problem can be reduced to the bounded problem if there is at most\r\none
rationally linearly independent frequency, or if there are two rationally linearly
independent\r\nfrequencies and all characteristic roots are simple. We complete
the picture by showing that de-\r\ncidability of the unbounded problem in the
case of two (or more) rationally linearly independent\r\nfrequencies would entail
a major new effectiveness result in Diophantine approximation, namely\r\ncomputability
of the Diophantine-approximation types of all real algebraic numbers."
acknowledgement: 'Ventsislav Chonev is supported by Austrian Science Fund (FWF) NFN
Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and ERC
Advanced Grant (267989: QUAREM).'
alternative_title:
- LIPIcs
article_number: '100'
author:
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
- first_name: Joël
full_name: Ouaknine, Joël
last_name: Ouaknine
- first_name: James
full_name: Worrell, James
last_name: Worrell
citation:
ama: 'Chonev VK, Ouaknine J, Worrell J. On the skolem problem for continuous linear
dynamical systems. In: Vol 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik;
2016. doi:10.4230/LIPIcs.ICALP.2016.100'
apa: 'Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the skolem problem
for continuous linear dynamical systems (Vol. 55). Presented at the ICALP: Automata,
Languages and Programming, Rome, Italy: Schloss Dagstuhl- Leibniz-Zentrum fur
Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2016.100'
chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Skolem
Problem for Continuous Linear Dynamical Systems,” Vol. 55. Schloss Dagstuhl- Leibniz-Zentrum
fur Informatik, 2016. https://doi.org/10.4230/LIPIcs.ICALP.2016.100.
ieee: 'V. K. Chonev, J. Ouaknine, and J. Worrell, “On the skolem problem for continuous
linear dynamical systems,” presented at the ICALP: Automata, Languages and Programming,
Rome, Italy, 2016, vol. 55.'
ista: 'Chonev VK, Ouaknine J, Worrell J. 2016. On the skolem problem for continuous
linear dynamical systems. ICALP: Automata, Languages and Programming, LIPIcs,
vol. 55, 100.'
mla: Chonev, Ventsislav K., et al. On the Skolem Problem for Continuous Linear
Dynamical Systems. Vol. 55, 100, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016, doi:10.4230/LIPIcs.ICALP.2016.100.
short: V.K. Chonev, J. Ouaknine, J. Worrell, in:, Schloss Dagstuhl- Leibniz-Zentrum
fur Informatik, 2016.
conference:
end_date: 2016-07-15
location: Rome, Italy
name: 'ICALP: Automata, Languages and Programming'
start_date: 2016-07-12
date_created: 2018-12-11T11:49:59Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:48:03Z
day: '01'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ICALP.2016.100
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:26Z
date_updated: 2018-12-12T10:16:26Z
file_id: '5213'
file_name: IST-2017-778-v1+1_LIPIcs-ICALP-2016-100.pdf
file_size: 521415
relation: main_file
file_date_updated: 2018-12-12T10:16:26Z
has_accepted_license: '1'
intvolume: ' 55'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik
publist_id: '6314'
pubrep_id: '778'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the skolem problem for continuous linear dynamical systems
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 55
year: '2016'
...
---
_id: '1070'
abstract:
- lang: eng
text: 'We present a logic that extends CTL (Computation Tree Logic) with operators
that express synchronization properties. A property is synchronized in a system
if it holds in all paths of a certain length. The new logic is obtained by using
the same path quantifiers and temporal operators as in CTL, but allowing a different
order of the quantifiers. This small syntactic variation induces a logic that
can express non-regular properties for which known extensions of MSO with equality
of path length are undecidable. We show that our variant of CTL is decidable and
that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We
analogously consider quantifier exchange in extensions of CTL, and we present
operators defined using basic operators of CTL* that express the occurrence of
infinitely many synchronization points. We show that the model-checking problem
remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide
if the Next operator is allowed in the logics, thus the classical bisimulation
quotient can be used for state-space reduction before model checking. '
acknowledgement: "This research was partially supported by Austrian Science Fund (FWF)
NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), Vienna
Science and Technology Fund (WWTF) through project ICT15-003, and European project
Cassting (FP7-601148).\r\n\r\nWe thank Stefan Göller and anonymous reviewers for
their insightful\r\ncomments and suggestions.\r\n"
alternative_title:
- LIPIcs
article_number: '98'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
citation:
ama: 'Chatterjee K, Doyen L. Computation tree logic for synchronization properties.
In: Vol 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:10.4230/LIPIcs.ICALP.2016.98'
apa: 'Chatterjee, K., & Doyen, L. (2016). Computation tree logic for synchronization
properties (Vol. 55). Presented at the ICALP: Automata, Languages and Programming,
Rome, Italy: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2016.98'
chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Computation Tree Logic for
Synchronization Properties,” Vol. 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016. https://doi.org/10.4230/LIPIcs.ICALP.2016.98.
ieee: 'K. Chatterjee and L. Doyen, “Computation tree logic for synchronization properties,”
presented at the ICALP: Automata, Languages and Programming, Rome, Italy, 2016,
vol. 55.'
ista: 'Chatterjee K, Doyen L. 2016. Computation tree logic for synchronization properties.
ICALP: Automata, Languages and Programming, LIPIcs, vol. 55, 98.'
mla: Chatterjee, Krishnendu, and Laurent Doyen. Computation Tree Logic for Synchronization
Properties. Vol. 55, 98, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016, doi:10.4230/LIPIcs.ICALP.2016.98.
short: K. Chatterjee, L. Doyen, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016.
conference:
end_date: 2016-07-15
location: Rome, Italy
name: 'ICALP: Automata, Languages and Programming'
start_date: 2016-07-12
date_created: 2018-12-11T11:49:59Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:48:03Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ICALP.2016.98
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:52Z
date_updated: 2018-12-12T10:08:52Z
file_id: '4714'
file_name: IST-2017-812-v1+1_LIPIcs-ICALP-2016-98.pdf
file_size: 546133
relation: main_file
file_date_updated: 2018-12-12T10:08:52Z
has_accepted_license: '1'
intvolume: ' 55'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik
publist_id: '6313'
pubrep_id: '812'
quality_controlled: '1'
scopus_import: 1
status: public
title: Computation tree logic for synchronization properties
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 55
year: '2016'
...
---
_id: '1090'
abstract:
- lang: eng
text: ' While weighted automata provide a natural framework to express quantitative
properties, many basic properties like average response time cannot be expressed
with weighted automata. Nested weighted automata extend weighted automata and
consist of a master automaton and a set of slave automata that are invoked by
the master automaton. Nested weighted automata are strictly more expressive than
weighted automata (e.g., average response time can be expressed with nested weighted
automata), but the basic decision questions have higher complexity (e.g., for
deterministic automata, the emptiness question for nested weighted automata is
PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME).
We consider a natural subclass of nested weighted automata where at any point
at most a bounded number k of slave automata can be active. We focus on automata
whose master value function is the limit average. We show that these nested weighted
automata with bounded width are strictly more expressive than weighted automata
(e.g., average response time with no overlapping requests can be expressed with
bound k=1, but not with non-nested weighted automata). We show that the complexity
of the basic decision problems (i.e., emptiness and universality) for the subclass
with k constant matches the complexity for weighted automata. Moreover, when k
is part of the input given in unary we establish PSPACE-completeness.'
acknowledgement: "This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award),
ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF)
through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under
grant 2014/15/D/ST6/04543."
alternative_title:
- LIPIcs
article_number: '24'
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 limit-average automata
of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2016. doi:10.4230/LIPIcs.MFCS.2016.24'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Nested weighted limit-average
automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations
of Computer Science (SG), Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2016.24'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted
Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016. https://doi.org/10.4230/LIPIcs.MFCS.2016.24.
ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average
automata of bounded width,” presented at the MFCS: Mathematical Foundations of
Computer Science (SG), Krakow; Poland, 2016, vol. 58.'
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata
of bounded width. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs,
vol. 58, 24.'
mla: Chatterjee, Krishnendu, et al. Nested Weighted Limit-Average Automata of
Bounded Width. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016, doi:10.4230/LIPIcs.MFCS.2016.24.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Krakow; Poland
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2016-08-22
date_created: 2018-12-11T11:50:05Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:48:12Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2016.24
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:31Z
date_updated: 2018-12-12T10:17:31Z
file_id: '5286'
file_name: IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf
file_size: 564560
relation: main_file
file_date_updated: 2018-12-12T10:17:31Z
has_accepted_license: '1'
intvolume: ' 58'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6286'
pubrep_id: '795'
quality_controlled: '1'
scopus_import: 1
status: public
title: Nested weighted limit-average automata of bounded width
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 58
year: '2016'
...
---
_id: '1138'
abstract:
- lang: eng
text: Automata with monitor counters, where the transitions do not depend on counter
values, and nested weighted automata are two expressive automata-theoretic frameworks
for quantitative properties. For a well-studied and wide class of quantitative
functions, we establish that automata with monitor counters and nested weighted
automata are equivalent. We study for the first time such quantitative automata
under probabilistic semantics. We show that several problems that are undecidable
for the classical questions of emptiness and universality become decidable under
the probabilistic semantics. We present a complete picture of decidability for
such automata, and even an almost-complete picture of computational complexity,
for the probabilistic questions we consider. © 2016 ACM.
acknowledgement: This research was funded in part by the European Research Council
(ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF)
projects S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499-
N23, FWF NFN Grant No S114
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. Quantitative automata under probabilistic
semantics. In: Proceedings of the 31st Annual ACM/IEEE Symposium. IEEE;
2016:76-85. doi:10.1145/2933575.2933588'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative automata
under probabilistic semantics. In Proceedings of the 31st Annual ACM/IEEE Symposium
(pp. 76–85). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2933588'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative
Automata under Probabilistic Semantics.” In Proceedings of the 31st Annual
ACM/IEEE Symposium, 76–85. IEEE, 2016. https://doi.org/10.1145/2933575.2933588.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under
probabilistic semantics,” in Proceedings of the 31st Annual ACM/IEEE Symposium,
New York, NY, USA, 2016, pp. 76–85.
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic
semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer
Science, 76–85.'
mla: Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.”
Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85,
doi:10.1145/2933575.2933588.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual
ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.
conference:
end_date: 2016-07-08
location: New York, NY, USA
name: 'LICS: Logic in Computer Science'
start_date: 2016-07-05
date_created: 2018-12-11T11:50:21Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2021-01-12T06:48:34Z
day: '05'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/2933575.2933588
ec_funded: 1
external_id:
arxiv:
- '1604.06764'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.06764
month: '07'
oa: 1
oa_version: Preprint
page: 76 - 85
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the 31st Annual ACM/IEEE Symposium
publication_status: published
publisher: IEEE
publist_id: '6220'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative automata under probabilistic semantics
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1140'
abstract:
- lang: eng
text: 'Given a model of a system and an objective, the model-checking question asks
whether the model satisfies the objective. We study polynomial-time problems in
two classical models, graphs and Markov Decision Processes (MDPs), with respect
to several fundamental -regular objectives, e.g., Rabin and Streett objectives.
For many of these problems the best-known upper bounds are quadratic or cubic,
yet no super-linear lower bounds are known. In this work our contributions are
two-fold: First, we present several improved algorithms, and second, we present
the first conditional super-linear lower bounds based on widely believed assumptions
about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication.
A separation result for two models with respect to an objective means a conditional
lower bound for one model that is strictly higher than the existing upper bound
for the other model, and similarly for two objectives with respect to a model.
Our results establish the following separation results: (1) A separation of models
(graphs and MDPs) for disjunctive queries of reachability and Büchi objectives.
(2) Two kinds of separations of objectives, both for graphs and MDPs, namely,
(2a) the separation of dual objectives such as Streett/Rabin objectives, and (2b)
the separation of conjunction and disjunction of multiple objectives of the same
type such as safety, Büchi, and coBüchi. In summary, our results establish the
first model and objective separation results for graphs and MDPs for various classical
-regular objectives. Quite strikingly, we establish conditional lower bounds for
the disjunction of objectives that are strictly higher than the existing upper
bounds for the conjunction of the same objectives. © 2016 ACM.'
acknowledgement: "K. C., M. H., and W. D. are partially supported by the
\ Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003.\r\nK.
C. is partially supported by the Austrian Science Fund (FWF)\r\nNFN Grant No S11407-N23
(RiSE/SHiNE) and an ERC Start grant\r\n(279307: Graph Games). For W. D., M. H.,
and V. L. the research\r\nleading to these results has received funding from the
European\r\nResearch Council under the European Union’s Seventh Framework\r\nProgramme
(FP/2007-2013) / ERC Grant Agreement no. 340506."
alternative_title:
- Proceedings Symposium on Logic in Computer Science
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Wolfgang
full_name: Dvoák, Wolfgang
last_name: Dvoák
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Veronika
full_name: Loitzenbauer, Veronika
last_name: Loitzenbauer
citation:
ama: 'Chatterjee K, Dvoák W, Henzinger MH, Loitzenbauer V. Model and objective separation
with conditional lower bounds: disjunction is harder than conjunction. In: Proceedings
of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE;
2016:197-206. doi:10.1145/2933575.2935304'
apa: 'Chatterjee, K., Dvoák, W., Henzinger, M. H., & Loitzenbauer, V. (2016).
Model and objective separation with conditional lower bounds: disjunction is harder
than conjunction. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic
in Computer Science (pp. 197–206). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2935304'
chicago: 'Chatterjee, Krishnendu, Wolfgang Dvoák, Monika H Henzinger, and Veronika
Loitzenbauer. “Model and Objective Separation with Conditional Lower Bounds: Disjunction
Is Harder than Conjunction.” In Proceedings of the 31st Annual ACM/IEEE Symposium
on Logic in Computer Science, 197–206. IEEE, 2016. https://doi.org/10.1145/2933575.2935304.'
ieee: 'K. Chatterjee, W. Dvoák, M. H. Henzinger, and V. Loitzenbauer, “Model and
objective separation with conditional lower bounds: disjunction is harder than
conjunction,” in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic
in Computer Science, New York, NY, USA, 2016, pp. 197–206.'
ista: 'Chatterjee K, Dvoák W, Henzinger MH, Loitzenbauer V. 2016. Model and objective
separation with conditional lower bounds: disjunction is harder than conjunction.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science.
LICS: Logic in Computer Science, Proceedings Symposium on Logic in Computer Science,
, 197–206.'
mla: 'Chatterjee, Krishnendu, et al. “Model and Objective Separation with Conditional
Lower Bounds: Disjunction Is Harder than Conjunction.” Proceedings of the 31st
Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2016, pp. 197–206,
doi:10.1145/2933575.2935304.'
short: K. Chatterjee, W. Dvoák, M.H. Henzinger, V. Loitzenbauer, in:, Proceedings
of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2016,
pp. 197–206.
conference:
end_date: 2016-07-08
location: New York, NY, USA
name: 'LICS: Logic in Computer Science'
start_date: 2016-07-05
date_created: 2018-12-11T11:50:22Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2022-09-09T11:46:17Z
day: '05'
department:
- _id: KrCh
doi: 10.1145/2933575.2935304
external_id:
arxiv:
- '1602.02670'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1602.02670
month: '07'
oa: 1
oa_version: Preprint
page: 197 - 206
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer
Science
publication_status: published
publisher: IEEE
publist_id: '6219'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Model and objective separation with conditional lower bounds: disjunction
is harder than conjunction'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1182'
abstract:
- lang: eng
text: 'Balanced knockout tournaments are ubiquitous in sports competitions and are
also used in decisionmaking and elections. The traditional computational question,
that asks to compute a draw (optimal draw) that maximizes the winning probability
for a distinguished player, has received a lot of attention. Previous works consider
the problem where the pairwise winning probabilities are known precisely, while
we study how robust is the winning probability with respect to small errors in
the pairwise winning probabilities. First, we present several illuminating examples
to establish: (a) there exist deterministic tournaments (where the pairwise winning
probabilities are 0 or 1) where one optimal draw is much more robust than the
other; and (b) in general, there exist tournaments with slightly suboptimal draws
that are more robust than all the optimal draws. The above examples motivate the
study of the computational problem of robust draws that guarantee a specified
winning probability. Second, we present a polynomial-time algorithm for approximating
the robustness of a draw for sufficiently small errors in pairwise winning probabilities,
and obtain that the stated computational problem is NP-complete. We also show
that two natural cases of deterministic tournaments where the optimal draw could
be computed in polynomial time also admit polynomial-time algorithms to compute
robust optimal draws.'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
citation:
ama: 'Chatterjee K, Ibsen-Jensen R, Tkadlec J. Robust draws in balanced knockout
tournaments. In: Vol 2016-January. AAAI Press; 2016:172-179.'
apa: 'Chatterjee, K., Ibsen-Jensen, R., & Tkadlec, J. (2016). Robust draws in
balanced knockout tournaments (Vol. 2016–January, pp. 172–179). Presented at the
IJCAI: International Joint Conference on Artificial Intelligence, New York, NY,
USA: AAAI Press.'
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Josef Tkadlec. “Robust
Draws in Balanced Knockout Tournaments,” 2016–January:172–79. AAAI Press, 2016.
ieee: 'K. Chatterjee, R. Ibsen-Jensen, and J. Tkadlec, “Robust draws in balanced
knockout tournaments,” presented at the IJCAI: International Joint Conference
on Artificial Intelligence, New York, NY, USA, 2016, vol. 2016–January, pp. 172–179.'
ista: 'Chatterjee K, Ibsen-Jensen R, Tkadlec J. 2016. Robust draws in balanced knockout
tournaments. IJCAI: International Joint Conference on Artificial Intelligence
vol. 2016–January, 172–179.'
mla: Chatterjee, Krishnendu, et al. Robust Draws in Balanced Knockout Tournaments.
Vol. 2016–January, AAAI Press, 2016, pp. 172–79.
short: K. Chatterjee, R. Ibsen-Jensen, J. Tkadlec, in:, AAAI Press, 2016, pp. 172–179.
conference:
end_date: 2016-07-15
location: New York, NY, USA
name: 'IJCAI: International Joint Conference on Artificial Intelligence'
start_date: 2016-07-09
date_created: 2018-12-11T11:50:35Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2023-02-21T10:04:26Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.05090v1
month: '01'
oa: 1
oa_version: Preprint
page: 172 - 179
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: AAAI Press
publist_id: '6171'
quality_controlled: '1'
related_material:
link:
- relation: table_of_contents
url: https://www.ijcai.org/proceedings/2016
scopus_import: 1
status: public
title: Robust draws in balanced knockout tournaments
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2016-January
year: '2016'
...
---
_id: '1200'
acknowledgement: C.H. acknowledges generous support from the ISTFELLOW program.
author:
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Arne
full_name: Traulsen, Arne
last_name: Traulsen
citation:
ama: 'Hilbe C, Traulsen A. Only the combination of mathematics and agent based simulations
can leverage the full potential of evolutionary modeling: Comment on “Evolutionary
game theory using agent-based methods” by C. Adami, J. Schossau and A. Hintze.
Physics of Life Reviews. 2016;19:29-31. doi:10.1016/j.plrev.2016.10.004'
apa: 'Hilbe, C., & Traulsen, A. (2016). Only the combination of mathematics
and agent based simulations can leverage the full potential of evolutionary modeling:
Comment on “Evolutionary game theory using agent-based methods” by C. Adami, J.
Schossau and A. Hintze. Physics of Life Reviews. Elsevier. https://doi.org/10.1016/j.plrev.2016.10.004'
chicago: 'Hilbe, Christian, and Arne Traulsen. “Only the Combination of Mathematics
and Agent Based Simulations Can Leverage the Full Potential of Evolutionary Modeling:
Comment on ‘Evolutionary Game Theory Using Agent-Based Methods’ by C. Adami, J.
Schossau and A. Hintze.” Physics of Life Reviews. Elsevier, 2016. https://doi.org/10.1016/j.plrev.2016.10.004.'
ieee: 'C. Hilbe and A. Traulsen, “Only the combination of mathematics and agent
based simulations can leverage the full potential of evolutionary modeling: Comment
on ‘Evolutionary game theory using agent-based methods’ by C. Adami, J. Schossau
and A. Hintze,” Physics of Life Reviews, vol. 19. Elsevier, pp. 29–31,
2016.'
ista: 'Hilbe C, Traulsen A. 2016. Only the combination of mathematics and agent
based simulations can leverage the full potential of evolutionary modeling: Comment
on “Evolutionary game theory using agent-based methods” by C. Adami, J. Schossau
and A. Hintze. Physics of Life Reviews. 19, 29–31.'
mla: 'Hilbe, Christian, and Arne Traulsen. “Only the Combination of Mathematics
and Agent Based Simulations Can Leverage the Full Potential of Evolutionary Modeling:
Comment on ‘Evolutionary Game Theory Using Agent-Based Methods’ by C. Adami, J.
Schossau and A. Hintze.” Physics of Life Reviews, vol. 19, Elsevier, 2016,
pp. 29–31, doi:10.1016/j.plrev.2016.10.004.'
short: C. Hilbe, A. Traulsen, Physics of Life Reviews 19 (2016) 29–31.
date_created: 2018-12-11T11:50:40Z
date_published: 2016-12-01T00:00:00Z
date_updated: 2021-01-12T06:49:03Z
day: '01'
ddc:
- '530'
department:
- _id: KrCh
doi: 10.1016/j.plrev.2016.10.004
ec_funded: 1
file:
- access_level: open_access
checksum: 95e6dc78278334b99dacbf8822509364
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:02Z
date_updated: 2020-07-14T12:44:39Z
file_id: '4855'
file_name: IST-2017-798-v1+1_comment_adami.pdf
file_size: 171352
relation: main_file
file_date_updated: 2020-07-14T12:44:39Z
has_accepted_license: '1'
intvolume: ' 19'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Submitted Version
page: 29 - 31
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: Physics of Life Reviews
publication_status: published
publisher: Elsevier
publist_id: '6150'
pubrep_id: '798'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Only the combination of mathematics and agent based simulations can leverage
the full potential of evolutionary modeling: Comment on “Evolutionary game theory
using agent-based methods” by C. Adami, J. Schossau and A. Hintze'
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 19
year: '2016'
...
---
_id: '1245'
abstract:
- lang: eng
text: 'To facilitate collaboration in massive online classrooms, instructors must
make many decisions. For instance, the following parameters need to be decided
when designing a peer-feedback system where students review each others'' essays:
the number of students each student must provide feedback to, an algorithm to
map feedback providers to receivers, constraints that ensure students do not become
free-riders (receiving feedback but not providing it), the best times to receive
feedback to improve learning etc. While instructors can answer these questions
by running experiments or invoking past experience, game-theoretic models with
data from online learning platforms can identify better initial designs for further
improvements. As an example, we explore the design space of a peer feedback system
by modeling it using game theory. Our simulations show that incentivizing students
to provide feedback requires the value obtained from receiving a feedback to exceed
the cost of providing it by a large factor (greater than 7). Furthermore, hiding
feedback from low-effort students incentivizes them to provide more feedback.'
acknowledgement: 'ERC Start Grant Graph Games 279307 supported this research. '
author:
- first_name: Vineet
full_name: Pandey, Vineet
last_name: Pandey
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: 'Pandey V, Chatterjee K. Game-theoretic models identify useful principles for
peer collaboration in online learning platforms. In: Proceedings of the ACM
Conference on Computer Supported Cooperative Work. Vol 26. ACM; 2016:365-368.
doi:10.1145/2818052.2869122'
apa: 'Pandey, V., & Chatterjee, K. (2016). Game-theoretic models identify useful
principles for peer collaboration in online learning platforms. In Proceedings
of the ACM Conference on Computer Supported Cooperative Work (Vol. 26, pp.
365–368). San Francisco, CA, USA: ACM. https://doi.org/10.1145/2818052.2869122'
chicago: Pandey, Vineet, and Krishnendu Chatterjee. “Game-Theoretic Models Identify
Useful Principles for Peer Collaboration in Online Learning Platforms.” In Proceedings
of the ACM Conference on Computer Supported Cooperative Work, 26:365–68. ACM,
2016. https://doi.org/10.1145/2818052.2869122.
ieee: V. Pandey and K. Chatterjee, “Game-theoretic models identify useful principles
for peer collaboration in online learning platforms,” in Proceedings of the
ACM Conference on Computer Supported Cooperative Work, San Francisco, CA,
USA, 2016, vol. 26, no. Februar-2016, pp. 365–368.
ista: 'Pandey V, Chatterjee K. 2016. Game-theoretic models identify useful principles
for peer collaboration in online learning platforms. Proceedings of the ACM Conference
on Computer Supported Cooperative Work. CSCW: Computer Supported Cooperative Work
and Social Computing vol. 26, 365–368.'
mla: Pandey, Vineet, and Krishnendu Chatterjee. “Game-Theoretic Models Identify
Useful Principles for Peer Collaboration in Online Learning Platforms.” Proceedings
of the ACM Conference on Computer Supported Cooperative Work, vol. 26, no.
Februar-2016, ACM, 2016, pp. 365–68, doi:10.1145/2818052.2869122.
short: V. Pandey, K. Chatterjee, in:, Proceedings of the ACM Conference on Computer
Supported Cooperative Work, ACM, 2016, pp. 365–368.
conference:
end_date: 2016-03-02
location: San Francisco, CA, USA
name: 'CSCW: Computer Supported Cooperative Work and Social Computing'
start_date: 2016-02-26
date_created: 2018-12-11T11:50:55Z
date_published: 2016-02-27T00:00:00Z
date_updated: 2021-01-12T06:49:22Z
day: '27'
department:
- _id: KrCh
doi: 10.1145/2818052.2869122
ec_funded: 1
intvolume: ' 26'
issue: Februar-2016
language:
- iso: eng
month: '02'
oa_version: None
page: 365 - 368
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the ACM Conference on Computer Supported Cooperative Work
publication_status: published
publisher: ACM
publist_id: '6083'
quality_controlled: '1'
scopus_import: 1
status: public
title: Game-theoretic models identify useful principles for peer collaboration in
online learning platforms
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 26
year: '2016'
...
---
_id: '1325'
abstract:
- lang: eng
text: We study graphs and two-player games in which rewards are assigned to states,
and the goal of the players is to satisfy or dissatisfy certain property of the
generated outcome, given as a mean payoff property. Since the notion of mean-payoff
does not reflect possible fluctuations from the mean-payoff along a run, we propose
definitions and algorithms for capturing the stability of the system, and give
algorithms for deciding if a given mean payoff and stability objective can be
ensured in the system.
acknowledgement: "The work has been supported by the Czech Science Foundation, grant
No. 15-17564S, by EPSRC grant\r\nEP/M023656/1, and by the People Programme (Marie
Curie Actions) of the European Union’s Seventh\r\nFramework Programme (FP7/2007-2013)
under REA grant agreement no [291734]"
alternative_title:
- LIPIcs
article_number: '10'
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Forejt V, Kučera A, Novotný P. Stability in graphs and games. In:
Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.10'
apa: 'Brázdil, T., Forejt, V., Kučera, A., & Novotný, P. (2016). Stability in
graphs and games (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec
City, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.10'
chicago: Brázdil, Tomáš, Vojtěch Forejt, Antonín Kučera, and Petr Novotný. “Stability
in Graphs and Games,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.10.
ieee: 'T. Brázdil, V. Forejt, A. Kučera, and P. Novotný, “Stability in graphs and
games,” presented at the CONCUR: Concurrency Theory, Quebec City, Canada, 2016,
vol. 59.'
ista: 'Brázdil T, Forejt V, Kučera A, Novotný P. 2016. Stability in graphs and games.
CONCUR: Concurrency Theory, LIPIcs, vol. 59, 10.'
mla: Brázdil, Tomáš, et al. Stability in Graphs and Games. Vol. 59, 10, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.10.
short: T. Brázdil, V. Forejt, A. Kučera, P. Novotný, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Quebec City, Canada
name: 'CONCUR: Concurrency Theory'
start_date: 2016-08-23
date_created: 2018-12-11T11:51:23Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2016.10
ec_funded: 1
file:
- access_level: open_access
checksum: 3c2dc6ab0358f8aa8f7aa7d6c1293159
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:40Z
date_updated: 2020-07-14T12:44:44Z
file_id: '5229'
file_name: IST-2016-665-v1+1_Forejt_et_al__Stability_in_graphs_and_games.pdf
file_size: 553648
relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: ' 59'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5944'
pubrep_id: '665'
quality_controlled: '1'
scopus_import: 1
status: public
title: Stability in graphs and games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1324'
abstract:
- lang: eng
text: 'DEC-POMDPs extend POMDPs to a multi-agent setting, where several agents operate
in an uncertain environment independently to achieve a joint objective. DEC-POMDPs
have been studied with finite-horizon and infinite-horizon discounted-sum objectives,
and there exist solvers both for exact and approximate solutions. 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 RTDP-Bel approach for POMDPs. We present experimental results on several
examples, and show that our approach presents promising results. Copyright '
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
citation:
ama: 'Chatterjee K, Chmelik M. Indefinite-horizon reachability in Goal-DEC-POMDPs.
In: Proceedings of the Twenty-Sixth International Conference on International
Conference on Automated Planning and Scheduling. Vol 2016-January. AAAI Press;
2016:88-96.'
apa: 'Chatterjee, K., & Chmelik, M. (2016). Indefinite-horizon reachability
in Goal-DEC-POMDPs. In Proceedings of the Twenty-Sixth International Conference
on International Conference on Automated Planning and Scheduling (Vol. 2016–January,
pp. 88–96). London, United Kingdom: AAAI Press.'
chicago: Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability
in Goal-DEC-POMDPs.” In Proceedings of the Twenty-Sixth International Conference
on International Conference on Automated Planning and Scheduling, 2016–January:88–96.
AAAI Press, 2016.
ieee: K. Chatterjee and M. Chmelik, “Indefinite-horizon reachability in Goal-DEC-POMDPs,”
in Proceedings of the Twenty-Sixth International Conference on International
Conference on Automated Planning and Scheduling, London, United Kingdom, 2016,
vol. 2016–January, pp. 88–96.
ista: 'Chatterjee K, Chmelik M. 2016. Indefinite-horizon reachability in Goal-DEC-POMDPs.
Proceedings of the Twenty-Sixth International Conference on International Conference
on Automated Planning and Scheduling. ICAPS: International Conference on Automated
Planning and Scheduling vol. 2016–January, 88–96.'
mla: Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability
in Goal-DEC-POMDPs.” Proceedings of the Twenty-Sixth International Conference
on International Conference on Automated Planning and Scheduling, vol. 2016–January,
AAAI Press, 2016, pp. 88–96.
short: K. Chatterjee, M. Chmelik, in:, Proceedings of the Twenty-Sixth International
Conference on International Conference on Automated Planning and Scheduling, AAAI
Press, 2016, pp. 88–96.
conference:
end_date: 2016-06-17
location: London, United Kingdom
name: 'ICAPS: International Conference on Automated Planning and Scheduling'
start_date: 2016-06-12
date_created: 2018-12-11T11:51:22Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
language:
- iso: eng
main_file_link:
- url: http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/12999
month: '01'
oa_version: None
page: 88 - 96
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Proceedings of the Twenty-Sixth International Conference on International
Conference on Automated Planning and Scheduling
publication_status: published
publisher: AAAI Press
publist_id: '5946'
quality_controlled: '1'
scopus_import: 1
status: public
title: Indefinite-horizon reachability in Goal-DEC-POMDPs
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 2016-January
year: '2016'
...
---
_id: '1327'
abstract:
- lang: eng
text: 'We consider partially observable Markov decision processes (POMDPs) with
a set of target states and positive integer costs associated with every transition.
The traditional optimization objective (stochastic shortest path) asks to minimize
the expected total cost until the target set is reached. We extend the traditional
framework of POMDPs to model energy consumption, which represents a hard constraint.
The energy levels may increase and decrease with transitions, and the hard constraint
requires that the energy level must remain positive in all steps till the target
is reached. First, we present a novel algorithm for solving POMDPs with energy
levels, developing on existing POMDP solvers and using RTDP as its main method.
Our second contribution is related to policy representation. For larger POMDP
instances the policies computed by existing solvers are too large to be understandable.
We present an automated procedure based on machine learning techniques that automatically
extracts important decisions of the policy allowing us to compute succinct human
readable policies. Finally, we show experimentally that our algorithm performs
well and computes succinct policies on a number of POMDP instances from the literature
that were naturally enhanced with energy levels. '
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- 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: Anchit
full_name: Gupta, Anchit
last_name: Gupta
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. Stochastic shortest
path with energy constraints in POMDPs. In: Proceedings of the 15th International
Conference on Autonomous Agents and Multiagent Systems. ACM; 2016:1465-1466.'
apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Gupta, A., & Novotný, P. (2016).
Stochastic shortest path with energy constraints in POMDPs. In Proceedings
of the 15th International Conference on Autonomous Agents and Multiagent Systems
(pp. 1465–1466). Singapore: ACM.'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Anchit Gupta, and
Petr Novotný. “Stochastic Shortest Path with Energy Constraints in POMDPs.” In
Proceedings of the 15th International Conference on Autonomous Agents and Multiagent
Systems, 1465–66. ACM, 2016.
ieee: T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, and P. Novotný, “Stochastic
shortest path with energy constraints in POMDPs,” in Proceedings of the 15th
International Conference on Autonomous Agents and Multiagent Systems, Singapore,
2016, pp. 1465–1466.
ista: 'Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. 2016. Stochastic
shortest path with energy constraints in POMDPs. Proceedings of the 15th International
Conference on Autonomous Agents and Multiagent Systems. AAMAS: Autonomous Agents
& Multiagent Systems, 1465–1466.'
mla: Brázdil, Tomáš, et al. “Stochastic Shortest Path with Energy Constraints in
POMDPs.” Proceedings of the 15th International Conference on Autonomous Agents
and Multiagent Systems, ACM, 2016, pp. 1465–66.
short: T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, P. Novotný, in:, Proceedings
of the 15th International Conference on Autonomous Agents and Multiagent Systems,
ACM, 2016, pp. 1465–1466.
conference:
end_date: 2016-05-13
location: Singapore
name: 'AAMAS: Autonomous Agents & Multiagent Systems'
start_date: 2016-05-09
date_created: 2018-12-11T11:51:23Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:49:54Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1602.07565
month: '01'
oa: 1
oa_version: Preprint
page: 1465 - 1466
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: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the 15th International Conference on Autonomous Agents
and Multiagent Systems
publication_status: published
publisher: ACM
publist_id: '5942'
quality_controlled: '1'
scopus_import: 1
status: public
title: Stochastic shortest path with energy constraints in POMDPs
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1326'
abstract:
- lang: eng
text: 'Energy Markov Decision Processes (EMDPs) are finite-state Markov decision
processes where each transition is assigned an integer counter update and a rational
payoff. An EMDP configuration is a pair s(n), where s is a control state and n
is the current counter value. The configurations are changed by performing transitions
in the standard way. We consider the problem of computing a safe strategy (i.e.,
a strategy that keeps the counter non-negative) which maximizes the expected mean
payoff. '
acknowledgement: The research was funded by the Czech Science Foundation Grant No.
P202/12/G061 and by the People Programme (Marie Curie Actions) of the European Union’s
Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no [291734].
alternative_title:
- LNCS
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Kučera A, Novotný P. Optimizing the expected mean payoff in Energy
Markov Decision Processes. In: Vol 9938. Springer; 2016:32-49. doi:10.1007/978-3-319-46520-3_3'
apa: 'Brázdil, T., Kučera, A., & Novotný, P. (2016). Optimizing the expected
mean payoff in Energy Markov Decision Processes (Vol. 9938, pp. 32–49). Presented
at the ATVA: Automated Technology for Verification and Analysis, Chiba, Japan:
Springer. https://doi.org/10.1007/978-3-319-46520-3_3'
chicago: Brázdil, Tomáš, Antonín Kučera, and Petr Novotný. “Optimizing the Expected
Mean Payoff in Energy Markov Decision Processes,” 9938:32–49. Springer, 2016.
https://doi.org/10.1007/978-3-319-46520-3_3.
ieee: 'T. Brázdil, A. Kučera, and P. Novotný, “Optimizing the expected mean payoff
in Energy Markov Decision Processes,” presented at the ATVA: Automated Technology
for Verification and Analysis, Chiba, Japan, 2016, vol. 9938, pp. 32–49.'
ista: 'Brázdil T, Kučera A, Novotný P. 2016. Optimizing the expected mean payoff
in Energy Markov Decision Processes. ATVA: Automated Technology for Verification
and Analysis, LNCS, vol. 9938, 32–49.'
mla: Brázdil, Tomáš, et al. Optimizing the Expected Mean Payoff in Energy Markov
Decision Processes. Vol. 9938, Springer, 2016, pp. 32–49, doi:10.1007/978-3-319-46520-3_3.
short: T. Brázdil, A. Kučera, P. Novotný, in:, Springer, 2016, pp. 32–49.
conference:
end_date: 2016-10-20
location: Chiba, Japan
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2016-10-17
date_created: 2018-12-11T11:51:23Z
date_published: 2016-09-22T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '22'
department:
- _id: KrCh
doi: 10.1007/978-3-319-46520-3_3
ec_funded: 1
intvolume: ' 9938'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1607.00678
month: '09'
oa: 1
oa_version: Preprint
page: 32 - 49
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5943'
quality_controlled: '1'
scopus_import: 1
status: public
title: Optimizing the expected mean payoff in Energy Markov Decision Processes
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9938
year: '2016'
...
---
_id: '1333'
abstract:
- lang: eng
text: Social dilemmas force players to balance between personal and collective gain.
In many dilemmas, such as elected governments negotiating climate-change mitigation
measures, the decisions are made not by individual players but by their representatives.
However, the behaviour of representatives in social dilemmas has not been investigated
experimentally. Here inspired by the negotiations for greenhouse-gas emissions
reductions, we experimentally study a collective-risk social dilemma that involves
representatives deciding on behalf of their fellow group members. Representatives
can be re-elected or voted out after each consecutive collective-risk game. Selfish
players are preferentially elected and are hence found most frequently in the
"representatives" treatment. Across all treatments, we identify the
selfish players as extortioners. As predicted by our mathematical model, their
steadfast strategies enforce cooperation from fair players who finally compensate
almost completely the deficit caused by the extortionate co-players. Everybody
gains, but the extortionate representatives and their groups gain the most.
acknowledgement: We thank the students for participation; H.-J. Krambeck for writing
the software for the game; H. Arndt, T. Bakker, L. Becks, H. Brendelberger, S. Dobler
and T. Reusch for support; and the Max Planck Society for the Advancement of Science
for funding.
article_number: '10915'
author:
- first_name: Manfred
full_name: Milinski, Manfred
last_name: Milinski
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Dirk
full_name: Semmann, Dirk
last_name: Semmann
- first_name: Ralf
full_name: Sommerfeld, Ralf
last_name: Sommerfeld
- first_name: Jochem
full_name: Marotzke, Jochem
last_name: Marotzke
citation:
ama: Milinski M, Hilbe C, Semmann D, Sommerfeld R, Marotzke J. Humans choose representatives
who enforce cooperation in social dilemmas through extortion. Nature Communications.
2016;7. doi:10.1038/ncomms10915
apa: Milinski, M., Hilbe, C., Semmann, D., Sommerfeld, R., & Marotzke, J. (2016).
Humans choose representatives who enforce cooperation in social dilemmas through
extortion. Nature Communications. Nature Publishing Group. https://doi.org/10.1038/ncomms10915
chicago: Milinski, Manfred, Christian Hilbe, Dirk Semmann, Ralf Sommerfeld, and
Jochem Marotzke. “Humans Choose Representatives Who Enforce Cooperation in Social
Dilemmas through Extortion.” Nature Communications. Nature Publishing Group,
2016. https://doi.org/10.1038/ncomms10915.
ieee: M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, and J. Marotzke, “Humans
choose representatives who enforce cooperation in social dilemmas through extortion,”
Nature Communications, vol. 7. Nature Publishing Group, 2016.
ista: Milinski M, Hilbe C, Semmann D, Sommerfeld R, Marotzke J. 2016. Humans choose
representatives who enforce cooperation in social dilemmas through extortion.
Nature Communications. 7, 10915.
mla: Milinski, Manfred, et al. “Humans Choose Representatives Who Enforce Cooperation
in Social Dilemmas through Extortion.” Nature Communications, vol. 7, 10915,
Nature Publishing Group, 2016, doi:10.1038/ncomms10915.
short: M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, J. Marotzke, Nature Communications
7 (2016).
date_created: 2018-12-11T11:51:25Z
date_published: 2016-03-07T00:00:00Z
date_updated: 2021-01-12T06:49:57Z
day: '07'
ddc:
- '519'
- '530'
- '599'
department:
- _id: KrCh
doi: 10.1038/ncomms10915
file:
- access_level: open_access
checksum: 9ea0d7ce59a555a1cb8353d5559407cb
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:44Z
date_updated: 2020-07-14T12:44:44Z
file_id: '4834'
file_name: IST-2016-661-v1+1_ncomms10915.pdf
file_size: 1432577
relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: ' 7'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
publication: Nature Communications
publication_status: published
publisher: Nature Publishing Group
publist_id: '5935'
pubrep_id: '661'
quality_controlled: '1'
scopus_import: 1
status: public
title: Humans choose representatives who enforce cooperation in social dilemmas through
extortion
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7
year: '2016'
...