---
_id: '5967'
abstract:
- lang: eng
text: "The Big Match is a multi-stage two-player game. In each stage Player 1 hides
one or two pebbles in his hand, and his opponent has to guess that number; Player
1 loses a point if Player 2 is correct, and otherwise he wins a point. As soon
as Player 1 hides one pebble, the players cannot change their choices in any future
stage.\r\nBlackwell and Ferguson (1968) give an ε-optimal strategy for Player
1 that hides, in each stage, one pebble with a probability that depends on the
entire past history. Any strategy that depends just on the clock or on a finite
memory is worthless. The long-standing natural open problem has been whether every
strategy that depends just on the clock and a finite memory is worthless. We prove
that there is such a strategy that is ε-optimal. In fact, we show that just two
states of memory are sufficient.\r\n"
article_processing_charge: No
author:
- first_name: Kristoffer Arnsfelt
full_name: Hansen, Kristoffer Arnsfelt
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
- first_name: Abraham
full_name: Neyman, Abraham
last_name: Neyman
citation:
ama: 'Hansen KA, Ibsen-Jensen R, Neyman A. The Big Match with a clock and a bit
of memory. In: Proceedings of the 2018 ACM Conference on Economics and Computation
- EC ’18. ACM Press; 2018:149-150. doi:10.1145/3219166.3219198'
apa: 'Hansen, K. A., Ibsen-Jensen, R., & Neyman, A. (2018). The Big Match with
a clock and a bit of memory. In Proceedings of the 2018 ACM Conference on Economics
and Computation - EC ’18 (pp. 149–150). Ithaca, NY, United States: ACM Press.
https://doi.org/10.1145/3219166.3219198'
chicago: Hansen, Kristoffer Arnsfelt, Rasmus Ibsen-Jensen, and Abraham Neyman. “The
Big Match with a Clock and a Bit of Memory.” In Proceedings of the 2018 ACM
Conference on Economics and Computation - EC ’18, 149–50. ACM Press, 2018.
https://doi.org/10.1145/3219166.3219198.
ieee: K. A. Hansen, R. Ibsen-Jensen, and A. Neyman, “The Big Match with a clock
and a bit of memory,” in Proceedings of the 2018 ACM Conference on Economics
and Computation - EC ’18, Ithaca, NY, United States, 2018, pp. 149–150.
ista: 'Hansen KA, Ibsen-Jensen R, Neyman A. 2018. The Big Match with a clock and
a bit of memory. Proceedings of the 2018 ACM Conference on Economics and Computation
- EC ’18. EC: Conference on Economics and Computation, 149–150.'
mla: Hansen, Kristoffer Arnsfelt, et al. “The Big Match with a Clock and a Bit of
Memory.” Proceedings of the 2018 ACM Conference on Economics and Computation
- EC ’18, ACM Press, 2018, pp. 149–50, doi:10.1145/3219166.3219198.
short: K.A. Hansen, R. Ibsen-Jensen, A. Neyman, in:, Proceedings of the 2018 ACM
Conference on Economics and Computation - EC ’18, ACM Press, 2018, pp. 149–150.
conference:
end_date: 2018-06-22
location: Ithaca, NY, United States
name: 'EC: Conference on Economics and Computation'
start_date: 2018-06-18
date_created: 2019-02-13T10:31:41Z
date_published: 2018-06-18T00:00:00Z
date_updated: 2023-09-19T10:45:15Z
day: '18'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3219166.3219198
external_id:
isi:
- '000492755100020'
file:
- access_level: open_access
checksum: bb52683e349cfd864f4769a8f38f2798
content_type: application/pdf
creator: dernst
date_created: 2019-11-19T08:24:24Z
date_updated: 2020-07-14T12:47:14Z
file_id: '7054'
file_name: 2018_EC18_Hansen.pdf
file_size: 302539
relation: main_file
file_date_updated: 2020-07-14T12:47:14Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 149-150
publication: Proceedings of the 2018 ACM Conference on Economics and Computation -
EC '18
publication_identifier:
isbn:
- '9781450358293'
publication_status: published
publisher: ACM Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: The Big Match with a clock and a bit of memory
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2018'
...
---
_id: '5993'
abstract:
- lang: eng
text: 'In this article, we consider the termination problem of probabilistic programs
with real-valued variables. Thequestions concerned are: qualitative ones that
ask (i) whether the program terminates with probability 1(almost-sure termination)
and (ii) whether the expected termination time is finite (finite termination);
andquantitative ones that ask (i) to approximate the expected termination time
(expectation problem) and (ii) tocompute a boundBsuch that the probability not
to terminate afterBsteps decreases exponentially (con-centration problem). To
solve these questions, we utilize the notion of ranking supermartingales, which
isa powerful approach for proving termination of probabilistic programs. In detail,
we focus on algorithmicsynthesis of linear ranking-supermartingales over affine
probabilistic programs (Apps) with both angelic anddemonic non-determinism. An
important subclass of Apps is LRApp which is defined as the class of all Appsover
which a linear ranking-supermartingale exists.Our main contributions are as follows.
Firstly, we show that the membership problem of LRApp (i) canbe decided in polynomial
time for Apps with at most demonic non-determinism, and (ii) isNP-hard and inPSPACEfor
Apps with angelic non-determinism. Moreover, theNP-hardness result holds already
for Appswithout probability and demonic non-determinism. Secondly, we show that
the concentration problem overLRApp can be solved in the same complexity as for
the membership problem of LRApp. Finally, we show thatthe expectation problem
over LRApp can be solved in2EXPTIMEand isPSPACE-hard even for Apps withoutprobability
and non-determinism (i.e., deterministic programs). Our experimental results demonstrate
theeffectiveness of our approach to answer the qualitative and quantitative questions
over Apps with at mostdemonic non-determinism.'
article_number: '7'
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
id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
last_name: Fu
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Rouzbeh
full_name: Hasheminezhad, Rouzbeh
last_name: Hasheminezhad
citation:
ama: Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative
and quantitative termination problems for affine probabilistic programs. ACM
Transactions on Programming Languages and Systems. 2018;40(2). doi:10.1145/3174800
apa: Chatterjee, K., Fu, H., Novotný, P., & Hasheminezhad, R. (2018). Algorithmic
analysis of qualitative and quantitative termination problems for affine probabilistic
programs. ACM Transactions on Programming Languages and Systems. Association
for Computing Machinery (ACM). https://doi.org/10.1145/3174800
chicago: Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad.
“Algorithmic Analysis of Qualitative and Quantitative Termination Problems for
Affine Probabilistic Programs.” ACM Transactions on Programming Languages and
Systems. Association for Computing Machinery (ACM), 2018. https://doi.org/10.1145/3174800.
ieee: K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic
programs,” ACM Transactions on Programming Languages and Systems, vol.
40, no. 2. Association for Computing Machinery (ACM), 2018.
ista: Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2018. Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic
programs. ACM Transactions on Programming Languages and Systems. 40(2), 7.
mla: Chatterjee, Krishnendu, et al. “Algorithmic Analysis of Qualitative and Quantitative
Termination Problems for Affine Probabilistic Programs.” ACM Transactions on
Programming Languages and Systems, vol. 40, no. 2, 7, Association for Computing
Machinery (ACM), 2018, doi:10.1145/3174800.
short: K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming
Languages and Systems 40 (2018).
date_created: 2019-02-14T12:29:10Z
date_published: 2018-06-01T00:00:00Z
date_updated: 2023-09-19T14:38:42Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3174800
ec_funded: 1
external_id:
arxiv:
- '1510.08517'
isi:
- '000434634500003'
intvolume: ' 40'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1510.08517
month: '06'
oa: 1
oa_version: Submitted 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'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: ACM Transactions on Programming Languages and Systems
publication_identifier:
issn:
- 0164-0925
publication_status: published
publisher: Association for Computing Machinery (ACM)
quality_controlled: '1'
related_material:
record:
- id: '1438'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Algorithmic analysis of qualitative and quantitative termination problems for
affine probabilistic programs
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 40
year: '2018'
...
---
_id: '25'
abstract:
- lang: eng
text: 'Partially observable Markov decision processes (POMDPs) are the standard
models for planning under uncertainty with both finite and infinite horizon. Besides
the well-known discounted-sum objective, indefinite-horizon objective (aka Goal-POMDPs)
is another classical objective for POMDPs. In this case, given a set of target
states and a positive cost for each transition, the optimization objective is
to minimize the expected total cost until a target state is reached. In the literature,
RTDP-Bel or heuristic search value iteration (HSVI) have been used for solving
Goal-POMDPs. Neither of these algorithms has theoretical convergence guarantees,
and HSVI may even fail to terminate its trials. We give the following contributions:
(1) We discuss the challenges introduced in Goal-POMDPs and illustrate how they
prevent the original HSVI from converging. (2) We present a novel algorithm inspired
by HSVI, termed Goal-HSVI, and show that our algorithm has convergence guarantees.
(3) We show that Goal-HSVI outperforms RTDP-Bel on a set of well-known examples.'
acknowledgement: '∗This work has been supported by Vienna Science and Technology Fund
(WWTF) Project ICT15-003, Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE),
and ERC Starting grant (279307: Graph Games). This research was sponsored by the
Army Research Laboratory and was accomplished under Cooperative Agreement Number
W911NF-13-2-0045 (ARL Cyber Security CRA). '
article_processing_charge: No
author:
- first_name: Karel
full_name: Horák, Karel
last_name: Horák
- first_name: Branislav
full_name: Bošanský, Branislav
last_name: Bošanský
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: 'Horák K, Bošanský B, Chatterjee K. Goal-HSVI: Heuristic search value iteration
for goal-POMDPs. In: Proceedings of the Twenty-Seventh International Joint
Conference on Artificial Intelligence. Vol 2018-July. IJCAI; 2018:4764-4770.
doi:10.24963/ijcai.2018/662'
apa: 'Horák, K., Bošanský, B., & Chatterjee, K. (2018). Goal-HSVI: Heuristic
search value iteration for goal-POMDPs. In Proceedings of the Twenty-Seventh
International Joint Conference on Artificial Intelligence (Vol. 2018–July,
pp. 4764–4770). Stockholm, Sweden: IJCAI. https://doi.org/10.24963/ijcai.2018/662'
chicago: 'Horák, Karel, Branislav Bošanský, and Krishnendu Chatterjee. “Goal-HSVI:
Heuristic Search Value Iteration for Goal-POMDPs.” In Proceedings of the Twenty-Seventh
International Joint Conference on Artificial Intelligence, 2018–July:4764–70.
IJCAI, 2018. https://doi.org/10.24963/ijcai.2018/662.'
ieee: 'K. Horák, B. Bošanský, and K. Chatterjee, “Goal-HSVI: Heuristic search value
iteration for goal-POMDPs,” in Proceedings of the Twenty-Seventh International
Joint Conference on Artificial Intelligence, Stockholm, Sweden, 2018, vol.
2018–July, pp. 4764–4770.'
ista: 'Horák K, Bošanský B, Chatterjee K. 2018. Goal-HSVI: Heuristic search value
iteration for goal-POMDPs. Proceedings of the Twenty-Seventh International Joint
Conference on Artificial Intelligence. IJCAI: International Joint Conference on
Artificial Intelligence vol. 2018–July, 4764–4770.'
mla: 'Horák, Karel, et al. “Goal-HSVI: Heuristic Search Value Iteration for Goal-POMDPs.”
Proceedings of the Twenty-Seventh International Joint Conference on Artificial
Intelligence, vol. 2018–July, IJCAI, 2018, pp. 4764–70, doi:10.24963/ijcai.2018/662.'
short: K. Horák, B. Bošanský, K. Chatterjee, in:, Proceedings of the Twenty-Seventh
International Joint Conference on Artificial Intelligence, IJCAI, 2018, pp. 4764–4770.
conference:
end_date: 2018-07-19
location: Stockholm, Sweden
name: 'IJCAI: International Joint Conference on Artificial Intelligence'
start_date: 2018-07-13
date_created: 2018-12-11T11:44:13Z
date_published: 2018-07-01T00:00:00Z
date_updated: 2023-09-19T14:44:59Z
day: '01'
department:
- _id: KrCh
doi: 10.24963/ijcai.2018/662
ec_funded: 1
external_id:
isi:
- '000764175404127'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.24963/ijcai.2018/662
month: '07'
oa: 1
oa_version: Published Version
page: 4764 - 4770
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: Proceedings of the Twenty-Seventh International Joint Conference on Artificial
Intelligence
publication_status: published
publisher: IJCAI
publist_id: '8030'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Goal-HSVI: Heuristic search value iteration for goal-POMDPs'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 2018-July
year: '2018'
...
---
_id: '24'
abstract:
- lang: eng
text: Partially-observable Markov decision processes (POMDPs) with discounted-sum
payoff are a standard framework to model a wide range of problems related to decision
making under uncertainty. Traditionally, the goal has been to obtain policies
that optimize the expectation of the discounted-sum payoff. A key drawback of
the expectation measure is that even low probability events with extreme payoff
can significantly affect the expectation, and thus the obtained policies are not
necessarily risk-averse. An alternate approach is to optimize the probability
that the payoff is above a certain threshold, which allows obtaining risk-averse
policies, but ignores optimization of the expectation. We consider the expectation
optimization with probabilistic guarantee (EOPG) problem, where the goal is to
optimize the expectation ensuring that the payoff is above a given threshold with
at least a specified probability. We present several results on the EOPG problem,
including the first algorithm to solve it.
acknowledgement: "This research was supported by the Vienna Science and Technology
Fund (WWTF) grant ICT15-003; Austrian Science Fund (FWF): S11407-N23(RiSE/SHiNE);and
an ERC Start Grant (279307:Graph Games).\r\n"
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: Adrian
full_name: Elgyütt, Adrian
id: 4A2E9DBA-F248-11E8-B48F-1D18A9856A87
last_name: Elgyütt
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Owen
full_name: Rouillé, Owen
last_name: Rouillé
citation:
ama: 'Chatterjee K, Elgyütt A, Novotný P, Rouillé O. Expectation optimization with
probabilistic guarantees in POMDPs with discounted-sum objectives. In: Vol 2018.
IJCAI; 2018:4692-4699. doi:10.24963/ijcai.2018/652'
apa: 'Chatterjee, K., Elgyütt, A., Novotný, P., & Rouillé, O. (2018). Expectation
optimization with probabilistic guarantees in POMDPs with discounted-sum objectives
(Vol. 2018, pp. 4692–4699). Presented at the IJCAI: International Joint Conference
on Artificial Intelligence, Stockholm, Sweden: IJCAI. https://doi.org/10.24963/ijcai.2018/652'
chicago: Chatterjee, Krishnendu, Adrian Elgyütt, Petr Novotný, and Owen Rouillé.
“Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum
Objectives,” 2018:4692–99. IJCAI, 2018. https://doi.org/10.24963/ijcai.2018/652.
ieee: 'K. Chatterjee, A. Elgyütt, P. Novotný, and O. Rouillé, “Expectation optimization
with probabilistic guarantees in POMDPs with discounted-sum objectives,” presented
at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm,
Sweden, 2018, vol. 2018, pp. 4692–4699.'
ista: 'Chatterjee K, Elgyütt A, Novotný P, Rouillé O. 2018. Expectation optimization
with probabilistic guarantees in POMDPs with discounted-sum objectives. IJCAI:
International Joint Conference on Artificial Intelligence vol. 2018, 4692–4699.'
mla: Chatterjee, Krishnendu, et al. Expectation Optimization with Probabilistic
Guarantees in POMDPs with Discounted-Sum Objectives. Vol. 2018, IJCAI, 2018,
pp. 4692–99, doi:10.24963/ijcai.2018/652.
short: K. Chatterjee, A. Elgyütt, P. Novotný, O. Rouillé, in:, IJCAI, 2018, pp.
4692–4699.
conference:
end_date: 2018-07-19
location: Stockholm, Sweden
name: 'IJCAI: International Joint Conference on Artificial Intelligence'
start_date: 2018-07-13
date_created: 2018-12-11T11:44:13Z
date_published: 2018-07-01T00:00:00Z
date_updated: 2023-09-19T14:45:48Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.24963/ijcai.2018/652
ec_funded: 1
external_id:
arxiv:
- '1804.10601'
isi:
- '000764175404117'
intvolume: ' 2018'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1804.10601
month: '07'
oa: 1
oa_version: Preprint
page: 4692 - 4699
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: IJCAI
publist_id: '8031'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum
objectives
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 2018
year: '2018'
...
---
_id: '34'
abstract:
- lang: eng
text: Partially observable Markov decision processes (POMDPs) are widely used in
probabilistic planning problems in which an agent interacts with an environment
using noisy and imprecise sensors. We study a setting in which the sensors are
only partially defined and the goal is to synthesize “weakest” additional sensors,
such that in the resulting POMDP, there is a small-memory policy for the agent
that almost-surely (with probability 1) satisfies a reachability objective. We
show that the problem is NP-complete, and present a symbolic algorithm by encoding
the problem into SAT instances. We illustrate trade-offs between the amount of
memory of the policy and the number of additional sensors on a simple example.
We have implemented our approach and consider three classical POMDP examples from
the literature, and show that in all the examples the number of sensors can be
significantly decreased (as compared to the existing solutions in the literature)
without increasing the complexity of the policies.
alternative_title:
- ICAPS
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: Martin
full_name: Chemlík, Martin
last_name: Chemlík
- first_name: Ufuk
full_name: Topcu, Ufuk
last_name: Topcu
citation:
ama: 'Chatterjee K, Chemlík M, Topcu U. Sensor synthesis for POMDPs with reachability
objectives. In: Vol 2018. AAAI Press; 2018:47-55.'
apa: 'Chatterjee, K., Chemlík, M., & Topcu, U. (2018). Sensor synthesis for
POMDPs with reachability objectives (Vol. 2018, pp. 47–55). Presented at the ICAPS:
International Conference on Automated Planning and Scheduling, Delft, Netherlands:
AAAI Press.'
chicago: Chatterjee, Krishnendu, Martin Chemlík, and Ufuk Topcu. “Sensor Synthesis
for POMDPs with Reachability Objectives,” 2018:47–55. AAAI Press, 2018.
ieee: 'K. Chatterjee, M. Chemlík, and U. Topcu, “Sensor synthesis for POMDPs with
reachability objectives,” presented at the ICAPS: International Conference on
Automated Planning and Scheduling, Delft, Netherlands, 2018, vol. 2018, pp. 47–55.'
ista: 'Chatterjee K, Chemlík M, Topcu U. 2018. Sensor synthesis for POMDPs with
reachability objectives. ICAPS: International Conference on Automated Planning
and Scheduling, ICAPS, vol. 2018, 47–55.'
mla: Chatterjee, Krishnendu, et al. Sensor Synthesis for POMDPs with Reachability
Objectives. Vol. 2018, AAAI Press, 2018, pp. 47–55.
short: K. Chatterjee, M. Chemlík, U. Topcu, in:, AAAI Press, 2018, pp. 47–55.
conference:
end_date: 2018-06-29
location: Delft, Netherlands
name: 'ICAPS: International Conference on Automated Planning and Scheduling'
start_date: 2018-06-24
date_created: 2018-12-11T11:44:16Z
date_published: 2018-06-01T00:00:00Z
date_updated: 2023-09-19T14:44:14Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
external_id:
arxiv:
- '1710.00675'
isi:
- '000492986200006'
intvolume: ' 2018'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1710.00675
month: '06'
oa: 1
oa_version: Preprint
page: 47 - 55
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
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: AAAI Press
publist_id: '8021'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Sensor synthesis for POMDPs with reachability objectives
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 2018
year: '2018'
...
---
_id: '35'
abstract:
- lang: eng
text: 'We consider planning problems for graphs, Markov decision processes (MDPs),
and games on graphs. While graphs represent the most basic planning model, MDPs
represent interaction with nature and games on graphs represent interaction with
an adversarial environment. We consider two planning problems where there are
k different target sets, and the problems are as follows: (a) the coverage problem
asks whether there is a plan for each individual target set; and (b) the sequential
target reachability problem asks whether the targets can be reached in sequence.
For the coverage problem, we present a linear-time algorithm for graphs, and quadratic
conditional lower bound for MDPs and games on graphs. For the sequential target
problem, we present a linear-time algorithm for graphs, a sub-quadratic algorithm
for MDPs, and a quadratic conditional lower bound for games on graphs. Our results
with conditional lower bounds establish (i) model-separation results showing that
for the coverage problem MDPs and games on graphs are harder than graphs and for
the sequential reachability problem games on graphs are harder than MDPs and graphs;
and (ii) objective-separation results showing that for MDPs the coverage problem
is harder than the sequential target problem.'
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: Alexander
full_name: Svozil, Alexander
last_name: Svozil
citation:
ama: 'Chatterjee K, Dvorák W, Henzinger MH, Svozil A. Algorithms and conditional
lower bounds for planning problems. In: 28th International Conference on Automated
Planning and Scheduling . AAAI Press; 2018.'
apa: 'Chatterjee, K., Dvorák, W., Henzinger, M. H., & Svozil, A. (2018). Algorithms
and conditional lower bounds for planning problems. In 28th International Conference
on Automated Planning and Scheduling . Delft, Netherlands: AAAI Press.'
chicago: Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Alexander
Svozil. “Algorithms and Conditional Lower Bounds for Planning Problems.” In 28th
International Conference on Automated Planning and Scheduling . AAAI Press,
2018.
ieee: K. Chatterjee, W. Dvorák, M. H. Henzinger, and A. Svozil, “Algorithms and
conditional lower bounds for planning problems,” in 28th International Conference
on Automated Planning and Scheduling , Delft, Netherlands, 2018.
ista: 'Chatterjee K, Dvorák W, Henzinger MH, Svozil A. 2018. Algorithms and conditional
lower bounds for planning problems. 28th International Conference on Automated
Planning and Scheduling . ICAPS: International Conference on Automated Planning
and Scheduling.'
mla: Chatterjee, Krishnendu, et al. “Algorithms and Conditional Lower Bounds for
Planning Problems.” 28th International Conference on Automated Planning and
Scheduling , AAAI Press, 2018.
short: K. Chatterjee, W. Dvorák, M.H. Henzinger, A. Svozil, in:, 28th International
Conference on Automated Planning and Scheduling , AAAI Press, 2018.
conference:
end_date: 2018-06-29
location: Delft, Netherlands
name: 'ICAPS: International Conference on Automated Planning and Scheduling'
start_date: 2018-06-24
date_created: 2018-12-11T11:44:17Z
date_published: 2018-06-01T00:00:00Z
date_updated: 2023-09-26T10:41:41Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
external_id:
arxiv:
- '1804.07031'
isi:
- '000492986200007'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1804.07031
month: '06'
oa: 1
oa_version: None
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'
publication: '28th International Conference on Automated Planning and Scheduling '
publication_status: published
publisher: AAAI Press
publist_id: '8020'
quality_controlled: '1'
related_material:
record:
- id: '9293'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Algorithms and conditional lower bounds for planning problems
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2018'
...
---
_id: '738'
abstract:
- lang: eng
text: 'This paper is devoted to automatic competitive analysis of real-time scheduling
algorithms for firm-deadline tasksets, where only completed tasks con- tribute
some utility to the system. Given such a taskset T , the competitive ratio of
an on-line scheduling algorithm A for T is the worst-case utility ratio of A over
the utility achieved by a clairvoyant algorithm. We leverage the theory of quantitative
graph games to address the competitive analysis and competitive synthesis problems.
For the competitive analysis case, given any taskset T and any finite-memory on-
line scheduling algorithm A , we show that the competitive ratio of A in T can
be computed in polynomial time in the size of the state space of A . Our approach
is flexible as it also provides ways to model meaningful constraints on the released
task sequences that determine the competitive ratio. We provide an experimental
study of many well-known on-line scheduling algorithms, which demonstrates the
feasibility of our competitive analysis approach that effectively replaces human
ingenuity (required Preliminary versions of this paper have appeared in Chatterjee
et al. ( 2013 , 2014 ). B Andreas Pavlogiannis pavlogiannis@ist.ac.at Krishnendu
Chatterjee krish.chat@ist.ac.at Alexander Kößler koe@ecs.tuwien.ac.at Ulrich Schmid
s@ecs.tuwien.ac.at 1 IST Austria (Institute of Science and Technology Austria),
Am Campus 1, 3400 Klosterneuburg, Austria 2 Embedded Computing Systems Group,
Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria 123 Real-Time
Syst for finding worst-case scenarios) by computing power. For the competitive
synthesis case, we are just given a taskset T , and the goal is to automatically
synthesize an opti- mal on-line scheduling algorithm A , i.e., one that guarantees
the largest competitive ratio possible for T . We show how the competitive synthesis
problem can be reduced to a two-player graph game with partial information, and
establish that the compu- tational complexity of solving this game is Np -complete.
The competitive synthesis problem is hence in Np in the size of the state space
of the non-deterministic labeled transition system encoding the taskset. Overall,
the proposed framework assists in the selection of suitable scheduling algorithms
for a given taskset, which is in fact the most common situation in real-time systems
design. '
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: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Alexander
full_name: Kößler, Alexander
last_name: Kößler
- first_name: Ulrich
full_name: Schmid, Ulrich
last_name: Schmid
citation:
ama: Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. Automated competitive analysis
of real time scheduling with graph games. Real-Time Systems. 2018;54(1):166-207.
doi:10.1007/s11241-017-9293-4
apa: Chatterjee, K., Pavlogiannis, A., Kößler, A., & Schmid, U. (2018). Automated
competitive analysis of real time scheduling with graph games. Real-Time Systems.
Springer. https://doi.org/10.1007/s11241-017-9293-4
chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich
Schmid. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.”
Real-Time Systems. Springer, 2018. https://doi.org/10.1007/s11241-017-9293-4.
ieee: K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “Automated competitive
analysis of real time scheduling with graph games,” Real-Time Systems,
vol. 54, no. 1. Springer, pp. 166–207, 2018.
ista: Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2018. Automated competitive
analysis of real time scheduling with graph games. Real-Time Systems. 54(1), 166–207.
mla: Chatterjee, Krishnendu, et al. “Automated Competitive Analysis of Real Time
Scheduling with Graph Games.” Real-Time Systems, vol. 54, no. 1, Springer,
2018, pp. 166–207, doi:10.1007/s11241-017-9293-4.
short: K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, Real-Time Systems 54
(2018) 166–207.
date_created: 2018-12-11T11:48:14Z
date_published: 2018-01-01T00:00:00Z
date_updated: 2023-09-27T12:52:38Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s11241-017-9293-4
ec_funded: 1
external_id:
isi:
- '000419955500006'
file:
- access_level: open_access
checksum: c2590ef160709d8054cf29ee173f1454
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:14Z
date_updated: 2020-07-14T12:47:56Z
file_id: '5267'
file_name: IST-2018-960-v1+1_2017_Chatterjee_Automated_competetive.pdf
file_size: 1163507
relation: main_file
file_date_updated: 2020-07-14T12:47:56Z
has_accepted_license: '1'
intvolume: ' 54'
isi: 1
issue: '1'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '01'
oa: 1
oa_version: Published Version
page: 166 - 207
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _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: 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: Real-Time Systems
publication_status: published
publisher: Springer
publist_id: '6929'
pubrep_id: '960'
quality_controlled: '1'
related_material:
record:
- id: '2820'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Automated competitive analysis of real time scheduling with graph games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 54
year: '2018'
...
---
_id: '198'
abstract:
- lang: eng
text: We consider a class of students learning a language from a teacher. The situation
can be interpreted as a group of child learners receiving input from the linguistic
environment. The teacher provides sample sentences. The students try to learn
the grammar from the teacher. In addition to just listening to the teacher, the
students can also communicate with each other. The students hold hypotheses about
the grammar and change them if they receive counter evidence. The process stops
when all students have converged to the correct grammar. We study how the time
to convergence depends on the structure of the classroom by introducing and evaluating
various complexity measures. We find that structured communication between students,
although potentially introducing confusion, can greatly reduce some of the complexity
measures. Our theory can also be interpreted as applying to the scientific process,
where nature is the teacher and the scientists are the students.
article_number: '20180073'
article_processing_charge: No
article_type: original
author:
- 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
- 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: Ibsen-Jensen R, Tkadlec J, Chatterjee K, Nowak M. Language acquisition with
communication between learners. Journal of the Royal Society Interface.
2018;15(140). doi:10.1098/rsif.2018.0073
apa: Ibsen-Jensen, R., Tkadlec, J., Chatterjee, K., & Nowak, M. (2018). Language
acquisition with communication between learners. Journal of the Royal Society
Interface. The Royal Society. https://doi.org/10.1098/rsif.2018.0073
chicago: Ibsen-Jensen, Rasmus, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. “Language Acquisition with Communication between Learners.” Journal
of the Royal Society Interface. The Royal Society, 2018. https://doi.org/10.1098/rsif.2018.0073.
ieee: R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, and M. Nowak, “Language acquisition
with communication between learners,” Journal of the Royal Society Interface,
vol. 15, no. 140. The Royal Society, 2018.
ista: Ibsen-Jensen R, Tkadlec J, Chatterjee K, Nowak M. 2018. Language acquisition
with communication between learners. Journal of the Royal Society Interface. 15(140),
20180073.
mla: Ibsen-Jensen, Rasmus, et al. “Language Acquisition with Communication between
Learners.” Journal of the Royal Society Interface, vol. 15, no. 140, 20180073,
The Royal Society, 2018, doi:10.1098/rsif.2018.0073.
short: R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, M. Nowak, Journal of the Royal
Society Interface 15 (2018).
date_created: 2018-12-11T11:45:09Z
date_published: 2018-03-01T00:00:00Z
date_updated: 2023-10-18T06:36:00Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1098/rsif.2018.0073
ec_funded: 1
external_id:
isi:
- '000428576200023'
pmid:
- '29593089'
file:
- access_level: open_access
checksum: 444e1a9d98eb0e780671be82b13025f3
content_type: application/pdf
creator: dernst
date_created: 2019-02-12T07:54:37Z
date_updated: 2020-07-14T12:45:22Z
file_id: '5955'
file_name: 2018_RS_IbsenJensen.pdf
file_size: 219837
relation: main_file
file_date_updated: 2020-07-14T12:45:22Z
has_accepted_license: '1'
intvolume: ' 15'
isi: 1
issue: '140'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
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: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Journal of the Royal Society Interface
publication_identifier:
eissn:
- 1742-5662
publication_status: published
publisher: The Royal Society
publist_id: '7715'
quality_controlled: '1'
related_material:
link:
- relation: supplementary_material
url: https://dx.doi.org/10.6084/m9.figshare.c.4028971
record:
- id: '9814'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Language acquisition with communication between learners
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2018'
...
---
_id: '5751'
abstract:
- lang: eng
text: 'Because of the intrinsic randomness of the evolutionary process, a mutant
with a fitness advantage has some chance to be selected but no certainty. Any
experiment that searches for advantageous mutants will lose many of them due to
random drift. It is therefore of great interest to find population structures
that improve the odds of advantageous mutants. Such structures are called amplifiers
of natural selection: they increase the probability that advantageous mutants
are selected. Arbitrarily strong amplifiers guarantee the selection of advantageous
mutants, even for very small fitness advantage. Despite intensive research over
the past decade, arbitrarily strong amplifiers have remained rare. Here we show
how to construct a large variety of them. Our amplifiers are so simple that they
could be useful in biotechnology, when optimizing biological molecules, or as
a diagnostic tool, when searching for faster dividing cells or viruses. They could
also occur in natural population structures.'
article_number: '71'
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 A.
full_name: Nowak, Martin A.
last_name: Nowak
citation:
ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak MA. Construction of arbitrarily
strong amplifiers of natural selection using evolutionary graph theory. Communications
Biology. 2018;1(1). doi:10.1038/s42003-018-0078-7
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. A. (2018). Construction
of arbitrarily strong amplifiers of natural selection using evolutionary graph
theory. Communications Biology. Springer Nature. https://doi.org/10.1038/s42003-018-0078-7
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
A. Nowak. “Construction of Arbitrarily Strong Amplifiers of Natural Selection
Using Evolutionary Graph Theory.” Communications Biology. Springer Nature,
2018. https://doi.org/10.1038/s42003-018-0078-7.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. A. Nowak, “Construction
of arbitrarily strong amplifiers of natural selection using evolutionary graph
theory,” Communications Biology, vol. 1, no. 1. Springer Nature, 2018.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak MA. 2018. Construction of arbitrarily
strong amplifiers of natural selection using evolutionary graph theory. Communications
Biology. 1(1), 71.
mla: Pavlogiannis, Andreas, et al. “Construction of Arbitrarily Strong Amplifiers
of Natural Selection Using Evolutionary Graph Theory.” Communications Biology,
vol. 1, no. 1, 71, Springer Nature, 2018, doi:10.1038/s42003-018-0078-7.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M.A. Nowak, Communications Biology
1 (2018).
date_created: 2018-12-18T13:22:58Z
date_published: 2018-06-14T00:00:00Z
date_updated: 2024-02-21T13:48:42Z
day: '14'
ddc:
- '004'
- '519'
- '576'
department:
- _id: KrCh
doi: 10.1038/s42003-018-0078-7
ec_funded: 1
external_id:
isi:
- '000461126500071'
file:
- access_level: open_access
checksum: a9db825fa3b64a51ff3de035ec973b3e
content_type: application/pdf
creator: dernst
date_created: 2018-12-18T13:37:04Z
date_updated: 2020-07-14T12:47:10Z
file_id: '5752'
file_name: 2018_CommBiology_Pavlogiannis.pdf
file_size: 1804194
relation: main_file
file_date_updated: 2020-07-14T12:47:10Z
has_accepted_license: '1'
intvolume: ' 1'
isi: 1
issue: '1'
language:
- iso: eng
month: '06'
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: Communications Biology
publication_identifier:
issn:
- 2399-3642
publication_status: published
publisher: Springer Nature
pubrep_id: '1045'
quality_controlled: '1'
related_material:
record:
- id: '7196'
relation: part_of_dissertation
status: public
- id: '5559'
relation: popular_science
status: public
scopus_import: '1'
status: public
title: Construction of arbitrarily strong amplifiers of natural selection using evolutionary
graph theory
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: 1
year: '2018'
...
---
_id: '66'
abstract:
- lang: eng
text: 'Crypto-currencies are digital assets designed to work as a medium of exchange,
e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants).
A framework for the analysis of attacks in crypto-currencies requires (a) modeling
of game-theoretic aspects to analyze incentives for deviation from honest behavior;
(b) concurrent interactions between participants; and (c) analysis of long-term
monetary gains. Traditional game-theoretic approaches for the analysis of security
protocols consider either qualitative temporal properties such as safety and termination,
or the very special class of one-shot (stateless) games. However, to analyze general
attacks on protocols for crypto-currencies, both stateful analysis and quantitative
objectives are necessary. In this work our main contributions are as follows:
(a) we show how a class of concurrent mean-payo games, namely ergodic games, can
model various attacks that arise naturally in crypto-currencies; (b) we present
the first practical implementation of algorithms for ergodic games that scales
to model realistic problems for crypto-currencies; and (c) we present experimental
results showing that our framework can handle games with thousands of states and
millions of transitions.'
alternative_title:
- LIPIcs
article_number: '11'
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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: 'Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. Ergodic mean-payoff
games for the analysis of attacks in crypto-currencies. In: Vol 118. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPIcs.CONCUR.2018.11'
apa: 'Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Velner, Y. (2018).
Ergodic mean-payoff games for the analysis of attacks in crypto-currencies (Vol.
118). Presented at the CONCUR: Conference on Concurrency Theory, Beijing, China:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2018.11'
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen,
and Yaron Velner. “Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies,”
Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPIcs.CONCUR.2018.11.
ieee: 'K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and Y. Velner, “Ergodic
mean-payoff games for the analysis of attacks in crypto-currencies,” presented
at the CONCUR: Conference on Concurrency Theory, Beijing, China, 2018, vol. 118.'
ista: 'Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. 2018. Ergodic mean-payoff
games for the analysis of attacks in crypto-currencies. CONCUR: Conference on
Concurrency Theory, LIPIcs, vol. 118, 11.'
mla: Chatterjee, Krishnendu, et al. Ergodic Mean-Payoff Games for the Analysis
of Attacks in Crypto-Currencies. Vol. 118, 11, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2018, doi:10.4230/LIPIcs.CONCUR.2018.11.
short: K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, Y. Velner, in:, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
conference:
end_date: 2018-09-07
location: Beijing, China
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2018-09-04
date_created: 2018-12-11T11:44:27Z
date_published: 2018-09-01T00:00:00Z
date_updated: 2024-03-28T23:30:34Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2018.11
ec_funded: 1
external_id:
arxiv:
- '1806.03108'
file:
- access_level: open_access
checksum: 68a055b1aaa241cc38375083cf832a7d
content_type: application/pdf
creator: dernst
date_created: 2018-12-17T12:08:00Z
date_updated: 2020-07-14T12:47:34Z
file_id: '5696'
file_name: 2018_CONCUR_Chatterjee.pdf
file_size: 1078309
relation: main_file
file_date_updated: 2020-07-14T12:47:34Z
has_accepted_license: '1'
intvolume: ' 118'
language:
- iso: eng
month: '09'
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: 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: 266EEEC0-B435-11E9-9278-68D0E5697425
name: Quantitative Game-theoretic Analysis of Blockchain Applications and Smart
Contracts
publication_identifier:
isbn:
- 978-3-95977-087-3
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7988'
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Ergodic mean-payoff games for the analysis of attacks in crypto-currencies
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: 118
year: '2018'
...
---
_id: '311'
abstract:
- lang: eng
text: 'Smart contracts are computer programs that are executed by a network of mutually
distrusting agents, without the need of an external trusted authority. Smart contracts
handle and transfer assets of considerable value (in the form of crypto-currency
like Bitcoin). Hence, it is crucial that their implementation is bug-free. We
identify the utility (or expected payoff) of interacting with such smart contracts
as the basic and canonical quantitative property for such contracts. We present
a framework for such quantitative analysis of smart contracts. Such a formal framework
poses new and novel research challenges in programming languages, as it requires
modeling of game-theoretic aspects to analyze incentives for deviation from honest
behavior and modeling utilities which are not specified as standard temporal properties
such as safety and termination. While game-theoretic incentives have been analyzed
in the security community, their analysis has been restricted to the very special
case of stateless games. However, to analyze smart contracts, stateful analysis
is required as it must account for the different program states of the protocol.
Our main contributions are as follows: we present (i)~a simplified programming
language for smart contracts; (ii)~an automatic translation of the programs to
state-based games; (iii)~an abstraction-refinement approach to solve such games;
and (iv)~experimental results on real-world-inspired smart contracts.'
acknowledgement: 'The research was partially supported by Vienna Science and Technology
Fund (WWTF) Project ICT15-003, Austrian Science Fund (FWF) NFN Grant No S11407-N23
(RiSE/SHiNE), and ERC Starting grant (279307: Graph Games).'
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: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: 'Chatterjee K, Goharshady AK, Velner Y. Quantitative analysis of smart contracts.
In: Vol 10801. Springer; 2018:739-767. doi:10.1007/978-3-319-89884-1_26'
apa: 'Chatterjee, K., Goharshady, A. K., & Velner, Y. (2018). Quantitative analysis
of smart contracts (Vol. 10801, pp. 739–767). Presented at the ESOP: European
Symposium on Programming, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89884-1_26'
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Yaron Velner. “Quantitative
Analysis of Smart Contracts,” 10801:739–67. Springer, 2018. https://doi.org/10.1007/978-3-319-89884-1_26.
ieee: 'K. Chatterjee, A. K. Goharshady, and Y. Velner, “Quantitative analysis of
smart contracts,” presented at the ESOP: European Symposium on Programming, Thessaloniki,
Greece, 2018, vol. 10801, pp. 739–767.'
ista: 'Chatterjee K, Goharshady AK, Velner Y. 2018. Quantitative analysis of smart
contracts. ESOP: European Symposium on Programming, LNCS, vol. 10801, 739–767.'
mla: Chatterjee, Krishnendu, et al. Quantitative Analysis of Smart Contracts.
Vol. 10801, Springer, 2018, pp. 739–67, doi:10.1007/978-3-319-89884-1_26.
short: K. Chatterjee, A.K. Goharshady, Y. Velner, in:, Springer, 2018, pp. 739–767.
conference:
end_date: 2018-04-19
location: Thessaloniki, Greece
name: 'ESOP: European Symposium on Programming'
start_date: 2018-04-16
date_created: 2018-12-11T11:45:45Z
date_published: 2018-04-01T00:00:00Z
date_updated: 2024-03-28T23:30:33Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-319-89884-1_26
ec_funded: 1
file:
- access_level: open_access
checksum: 9c8a8338c571903b599b6ca93abd2cce
content_type: application/pdf
creator: dernst
date_created: 2018-12-17T15:45:49Z
date_updated: 2020-07-14T12:46:00Z
file_id: '5716'
file_name: 2018_ESOP_Chatterjee.pdf
file_size: 1394993
relation: main_file
file_date_updated: 2020-07-14T12:46:00Z
has_accepted_license: '1'
intvolume: ' 10801'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 739 - 767
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: Springer
publist_id: '7554'
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Quantitative analysis of smart contracts
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: 10801
year: '2018'
...
---
_id: '6340'
abstract:
- lang: eng
text: We present a secure approach for maintaining andreporting credit history records on the Blockchain. Our ap-proach removes third-parties such as credit reporting agen-cies from the lending process and replaces them with smartcontracts. This allows customers to interact directly with thelenders or banks while ensuring the integrity, unmalleabilityand privacy of their credit data. Additionally, each customerhas full control over complete or selective disclosure of hercredit
records, eliminating the risk of privacy violations or databreaches. Moreover,
our approach provides strong guaranteesfor the lenders as well. A lender can check
both correctness andcompleteness of the credit data disclosed to her. This is
the firstapproach that can perform all credit reporting tasks withouta central authority or changing the financial mechanisms*.
article_processing_charge: No
author:
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Ali
full_name: Behrouz, Ali
last_name: Behrouz
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: 'Goharshady AK, Behrouz A, Chatterjee K. Secure Credit Reporting on the Blockchain.
In: Proceedings of the IEEE International Conference on Blockchain. IEEE;
2018:1343-1348. doi:10.1109/Cybermatics_2018.2018.00231'
apa: 'Goharshady, A. K., Behrouz, A., & Chatterjee, K. (2018). Secure Credit
Reporting on the Blockchain. In Proceedings of the IEEE International Conference
on Blockchain (pp. 1343–1348). Halifax, Canada: IEEE. https://doi.org/10.1109/Cybermatics_2018.2018.00231'
chicago: Goharshady, Amir Kafshdar, Ali Behrouz, and Krishnendu Chatterjee. “Secure
Credit Reporting on the Blockchain.” In Proceedings of the IEEE International
Conference on Blockchain, 1343–48. IEEE, 2018. https://doi.org/10.1109/Cybermatics_2018.2018.00231.
ieee: A. K. Goharshady, A. Behrouz, and K. Chatterjee, “Secure Credit Reporting
on the Blockchain,” in Proceedings of the IEEE International Conference on
Blockchain, Halifax, Canada, 2018, pp. 1343–1348.
ista: Goharshady AK, Behrouz A, Chatterjee K. 2018. Secure Credit Reporting on the
Blockchain. Proceedings of the IEEE International Conference on Blockchain. IEEE
International Conference on Blockchain, 1343–1348.
mla: Goharshady, Amir Kafshdar, et al. “Secure Credit Reporting on the Blockchain.”
Proceedings of the IEEE International Conference on Blockchain, IEEE, 2018,
pp. 1343–48, doi:10.1109/Cybermatics_2018.2018.00231.
short: A.K. Goharshady, A. Behrouz, K. Chatterjee, in:, Proceedings of the IEEE
International Conference on Blockchain, IEEE, 2018, pp. 1343–1348.
conference:
end_date: 2018-08-03
location: Halifax, Canada
name: IEEE International Conference on Blockchain
start_date: 2018-07-30
date_created: 2019-04-18T10:37:35Z
date_published: 2018-09-01T00:00:00Z
date_updated: 2024-03-28T23:30:34Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1109/Cybermatics_2018.2018.00231
ec_funded: 1
external_id:
arxiv:
- '1805.09104'
isi:
- '000481634500196'
file:
- access_level: open_access
checksum: b25c9bb7cf6e7e6634e692d26d41ead8
content_type: application/pdf
creator: akafshda
date_created: 2019-04-18T10:36:39Z
date_updated: 2020-07-14T12:47:27Z
file_id: '6341'
file_name: blockchain2018.pdf
file_size: 624338
relation: main_file
file_date_updated: 2020-07-14T12:47:27Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '09'
oa: 1
oa_version: Submitted Version
page: 1343-1348
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 266EEEC0-B435-11E9-9278-68D0E5697425
name: Quantitative Game-theoretic Analysis of Blockchain Applications and Smart
Contracts
- _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 IEEE International Conference on Blockchain
publication_identifier:
isbn:
- '978-1-5386-7975-3 '
publication_status: published
publisher: IEEE
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Secure Credit Reporting on the Blockchain
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2018'
...
---
_id: '6009'
abstract:
- lang: eng
text: "We study algorithmic questions wrt algebraic path properties in concurrent
systems, where the transitions of the system are labeled from a complete, closed
semiring. The algebraic path properties can model dataflow analysis problems,
the shortest path problem, and many other natural problems that arise in program
analysis. We consider that each component of the concurrent system is a graph
with constant treewidth, a property satisfied by the controlflow graphs of most
programs. We allow for multiple possible queries, which arise naturally in demand
driven dataflow analysis. The study of multiple queries allows us to consider
the tradeoff between the resource usage of the one-time preprocessing and for
each individual query. The traditional approach constructs the product graph of
all components and applies the best-known graph algorithm on the product. In this
approach, even the answer to a single query requires the transitive closure (i.e.,
the results of all possible queries), which provides no room for tradeoff between
preprocessing and query time.\r\nOur main contributions are algorithms that significantly
improve the worst-case running time of the traditional approach, and provide various
tradeoffs depending on the number of queries. For example, in a concurrent system
of two components, the traditional approach requires hexic time in the worst case
for answering one query as well as computing the transitive closure, whereas we
show that with one-time preprocessing in almost cubic time, each subsequent query
can be answered in at most linear time, and even the transitive closure can be
computed in almost quartic time. Furthermore, we establish conditional optimality
results showing that the worst-case running time of our algorithms cannot be improved
without achieving major breakthroughs in graph algorithms (i.e., improving the
worst-case bound for the shortest path problem in general graphs). Preliminary
experimental results show that our algorithms perform favorably on several benchmarks.\r\n"
article_number: '9'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
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, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for
algebraic path properties in concurrent systems of constant treewidth components.
ACM Transactions on Programming Languages and Systems. 2018;40(3). doi:10.1145/3210257
apa: Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., & Pavlogiannis, A.
(2018). Algorithms for algebraic path properties in concurrent systems of constant
treewidth components. ACM Transactions on Programming Languages and Systems.
Association for Computing Machinery (ACM). https://doi.org/10.1145/3210257
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady,
and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent
Systems of Constant Treewidth Components.” ACM Transactions on Programming
Languages and Systems. Association for Computing Machinery (ACM), 2018. https://doi.org/10.1145/3210257.
ieee: K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, “Algorithms
for algebraic path properties in concurrent systems of constant treewidth components,”
ACM Transactions on Programming Languages and Systems, vol. 40, no. 3.
Association for Computing Machinery (ACM), 2018.
ista: Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2018. Algorithms
for algebraic path properties in concurrent systems of constant treewidth components.
ACM Transactions on Programming Languages and Systems. 40(3), 9.
mla: Chatterjee, Krishnendu, et al. “Algorithms for Algebraic Path Properties in
Concurrent Systems of Constant Treewidth Components.” ACM Transactions on Programming
Languages and Systems, vol. 40, no. 3, 9, Association for Computing Machinery
(ACM), 2018, doi:10.1145/3210257.
short: K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions
on Programming Languages and Systems 40 (2018).
date_created: 2019-02-14T14:31:52Z
date_published: 2018-08-01T00:00:00Z
date_updated: 2024-03-28T23:30:34Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3210257
ec_funded: 1
external_id:
arxiv:
- '1510.07565'
isi:
- '000444694800001'
intvolume: ' 40'
isi: 1
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1510.07565
month: '08'
oa: 1
oa_version: Preprint
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: ACM Transactions on Programming Languages and Systems
publication_identifier:
issn:
- 0164-0925
publication_status: published
publisher: Association for Computing Machinery (ACM)
quality_controlled: '1'
related_material:
record:
- id: '1437'
relation: earlier_version
status: public
- id: '5441'
relation: earlier_version
status: public
- id: '5442'
relation: earlier_version
status: public
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Algorithms for algebraic path properties in concurrent systems of constant
treewidth components
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 40
year: '2018'
...
---
_id: '5977'
abstract:
- lang: eng
text: 'We consider the stochastic shortest path (SSP)problem for succinct Markov
decision processes(MDPs), where the MDP consists of a set of vari-ables, and a
set of nondeterministic rules that up-date the variables. First, we show that
several ex-amples from the AI literature can be modeled assuccinct MDPs. Then
we present computationalapproaches for upper and lower bounds for theSSP problem:
(a) for computing upper bounds, ourmethod is polynomial-time in the implicit descrip-tion
of the MDP; (b) for lower bounds, we present apolynomial-time (in the size of
the implicit descrip-tion) reduction to quadratic programming. Our ap-proach is
applicable even to infinite-state MDPs.Finally, we present experimental results
to demon-strate the effectiveness of our approach on severalclassical examples
from the AI literature.'
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
id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
last_name: Fu
- first_name: Amir
full_name: Goharshady, Amir
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Nastaran
full_name: Okati, Nastaran
last_name: Okati
citation:
ama: 'Chatterjee K, Fu H, Goharshady AK, Okati N. Computational approaches for stochastic
shortest path on succinct MDPs. In: Proceedings of the Twenty-Seventh International
Joint Conference on Artificial Intelligence. Vol 2018. IJCAI; 2018:4700-4707.
doi:10.24963/ijcai.2018/653'
apa: 'Chatterjee, K., Fu, H., Goharshady, A. K., & Okati, N. (2018). Computational
approaches for stochastic shortest path on succinct MDPs. In Proceedings of
the Twenty-Seventh International Joint Conference on Artificial Intelligence
(Vol. 2018, pp. 4700–4707). Stockholm, Sweden: IJCAI. https://doi.org/10.24963/ijcai.2018/653'
chicago: Chatterjee, Krishnendu, Hongfei Fu, Amir Kafshdar Goharshady, and Nastaran
Okati. “Computational Approaches for Stochastic Shortest Path on Succinct MDPs.”
In Proceedings of the Twenty-Seventh International Joint Conference on Artificial
Intelligence, 2018:4700–4707. IJCAI, 2018. https://doi.org/10.24963/ijcai.2018/653.
ieee: K. Chatterjee, H. Fu, A. K. Goharshady, and N. Okati, “Computational approaches
for stochastic shortest path on succinct MDPs,” in Proceedings of the Twenty-Seventh
International Joint Conference on Artificial Intelligence, Stockholm, Sweden,
2018, vol. 2018, pp. 4700–4707.
ista: 'Chatterjee K, Fu H, Goharshady AK, Okati N. 2018. Computational approaches
for stochastic shortest path on succinct MDPs. Proceedings of the Twenty-Seventh
International Joint Conference on Artificial Intelligence. IJCAI: International
Joint Conference on Artificial Intelligence vol. 2018, 4700–4707.'
mla: Chatterjee, Krishnendu, et al. “Computational Approaches for Stochastic Shortest
Path on Succinct MDPs.” Proceedings of the Twenty-Seventh International Joint
Conference on Artificial Intelligence, vol. 2018, IJCAI, 2018, pp. 4700–07,
doi:10.24963/ijcai.2018/653.
short: K. Chatterjee, H. Fu, A.K. Goharshady, N. Okati, in:, Proceedings of the
Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI,
2018, pp. 4700–4707.
conference:
end_date: 2018-07-19
location: Stockholm, Sweden
name: 'IJCAI: International Joint Conference on Artificial Intelligence'
start_date: 2018-07-13
date_created: 2019-02-13T13:26:27Z
date_published: 2018-07-17T00:00:00Z
date_updated: 2024-03-28T23:30:34Z
day: '17'
department:
- _id: KrCh
doi: 10.24963/ijcai.2018/653
ec_funded: 1
external_id:
arxiv:
- '1804.08984'
isi:
- '000764175404118'
intvolume: ' 2018'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1804.08984
month: '07'
oa: 1
oa_version: Preprint
page: 4700-4707
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: Proceedings of the Twenty-Seventh International Joint Conference on Artificial
Intelligence
publication_identifier:
isbn:
- 978-099924112-7
issn:
- '10450823'
publication_status: published
publisher: IJCAI
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Computational approaches for stochastic shortest path on succinct MDPs
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 2018
year: '2018'
...
---
_id: '2'
abstract:
- lang: eng
text: Indirect reciprocity explores how humans act when their reputation is at stake,
and which social norms they use to assess the actions of others. A crucial question
in indirect reciprocity is which social norms can maintain stable cooperation
in a society. Past research has highlighted eight such norms, called “leading-eight”
strategies. This past research, however, is based on the assumption that all relevant
information about other population members is publicly available and that everyone
agrees on who is good or bad. Instead, here we explore the reputation dynamics
when information is private and noisy. We show that under these conditions, most
leading-eight strategies fail to evolve. Those leading-eight strategies that do
evolve are unable to sustain full cooperation.Indirect reciprocity is a mechanism
for cooperation based on shared moral systems and individual reputations. It assumes
that members of a community routinely observe and assess each other and that they
use this information to decide who is good or bad, and who deserves cooperation.
When information is transmitted publicly, such that all community members agree
on each other’s reputation, previous research has highlighted eight crucial moral
systems. These “leading-eight” strategies can maintain cooperation and resist
invasion by defectors. However, in real populations individuals often hold their
own private views of others. Once two individuals disagree about their opinion
of some third party, they may also see its subsequent actions in a different light.
Their opinions may further diverge over time. Herein, we explore indirect reciprocity
when information transmission is private and noisy. We find that in the presence
of perception errors, most leading-eight strategies cease to be stable. Even if
a leading-eight strategy evolves, cooperation rates may drop considerably when
errors are common. Our research highlights the role of reliable information and
synchronized reputations to maintain stable moral systems.
article_processing_charge: No
author:
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Laura
full_name: Schmid, Laura
id: 38B437DE-F248-11E8-B48F-1D18A9856A87
last_name: Schmid
orcid: 0000-0002-6978-7329
- 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: Hilbe C, Schmid L, Tkadlec J, Chatterjee K, Nowak M. Indirect reciprocity with
private, noisy, and incomplete information. PNAS. 2018;115(48):12241-12246.
doi:10.1073/pnas.1810565115
apa: Hilbe, C., Schmid, L., Tkadlec, J., Chatterjee, K., & Nowak, M. (2018).
Indirect reciprocity with private, noisy, and incomplete information. PNAS.
National Academy of Sciences. https://doi.org/10.1073/pnas.1810565115
chicago: Hilbe, Christian, Laura Schmid, Josef Tkadlec, Krishnendu Chatterjee, and
Martin Nowak. “Indirect Reciprocity with Private, Noisy, and Incomplete Information.”
PNAS. National Academy of Sciences, 2018. https://doi.org/10.1073/pnas.1810565115.
ieee: C. Hilbe, L. Schmid, J. Tkadlec, K. Chatterjee, and M. Nowak, “Indirect reciprocity
with private, noisy, and incomplete information,” PNAS, vol. 115, no. 48.
National Academy of Sciences, pp. 12241–12246, 2018.
ista: Hilbe C, Schmid L, Tkadlec J, Chatterjee K, Nowak M. 2018. Indirect reciprocity
with private, noisy, and incomplete information. PNAS. 115(48), 12241–12246.
mla: Hilbe, Christian, et al. “Indirect Reciprocity with Private, Noisy, and Incomplete
Information.” PNAS, vol. 115, no. 48, National Academy of Sciences, 2018,
pp. 12241–46, doi:10.1073/pnas.1810565115.
short: C. Hilbe, L. Schmid, J. Tkadlec, K. Chatterjee, M. Nowak, PNAS 115 (2018)
12241–12246.
date_created: 2018-12-11T11:44:05Z
date_published: 2018-11-27T00:00:00Z
date_updated: 2024-03-28T23:30:45Z
day: '27'
department:
- _id: KrCh
doi: 10.1073/pnas.1810565115
ec_funded: 1
external_id:
isi:
- '000451351000063'
pmid:
- '30429320'
intvolume: ' 115'
isi: 1
issue: '48'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pubmed/30429320
month: '11'
oa: 1
oa_version: Submitted Version
page: 12241-12246
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: 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
publication: PNAS
publication_status: published
publisher: National Academy of Sciences
quality_controlled: '1'
related_material:
link:
- description: News on IST Homepage
relation: press_release
url: https://ist.ac.at/en/news/no-cooperation-without-open-communication/
record:
- id: '10293'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Indirect reciprocity with private, noisy, and incomplete information
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 115
year: '2018'
...
---
_id: '10418'
abstract:
- lang: eng
text: We present a new proof rule for proving almost-sure termination of probabilistic
programs, including those that contain demonic non-determinism. An important question
for a probabilistic program is whether the probability mass of all its diverging
runs is zero, that is that it terminates "almost surely". Proving that can be
hard, and this paper presents a new method for doing so. It applies directly to
the program's source code, even if the program contains demonic choice. Like others,
we use variant functions (a.k.a. "super-martingales") that are real-valued and
decrease randomly on each loop iteration; but our key innovation is that the amount
as well as the probability of the decrease are parametric. We prove the soundness
of the new rule, indicate where its applicability goes beyond existing rules,
and explain its connection to classical results on denumerable (non-demonic) Markov
chains.
acknowledgement: "McIver and Morgan are grateful to David Basin and the Information
Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during
part of which this work began. And thanks particularly to Andreas Lochbihler, who
shared with us the probabilistic termination problem that led to it. They acknowledge
the support of ARC grant DP140101119. Part of this work was carried out during the
Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs
Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden.
Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4."
article_number: '33'
article_processing_charge: No
article_type: original
author:
- first_name: Annabelle
full_name: Mciver, Annabelle
last_name: Mciver
- first_name: Carroll
full_name: Morgan, Carroll
last_name: Morgan
- first_name: Benjamin Lucien
full_name: Kaminski, Benjamin Lucien
last_name: Kaminski
- first_name: Joost P
full_name: Katoen, Joost P
id: 4524F760-F248-11E8-B48F-1D18A9856A87
last_name: Katoen
citation:
ama: Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure
termination. Proceedings of the ACM on Programming Languages. 2017;2(POPL).
doi:10.1145/3158121
apa: 'Mciver, A., Morgan, C., Kaminski, B. L., & Katoen, J. P. (2017). A new
proof rule for almost-sure termination. Proceedings of the ACM on Programming
Languages. Los Angeles, CA, United States: Association for Computing Machinery.
https://doi.org/10.1145/3158121'
chicago: Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost
P Katoen. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the
ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158121.
ieee: A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule
for almost-sure termination,” Proceedings of the ACM on Programming Languages,
vol. 2, no. POPL. Association for Computing Machinery, 2017.
ista: Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure
termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.
mla: Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” Proceedings
of the ACM on Programming Languages, vol. 2, no. POPL, 33, Association for
Computing Machinery, 2017, doi:10.1145/3158121.
short: A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, 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-07T00:00:00Z
date_updated: 2021-12-07T08:04:14Z
day: '07'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/3158121
external_id:
arxiv:
- '1711.03588'
intvolume: ' 2'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://dl.acm.org/doi/10.1145/3158121
month: '12'
oa: 1
oa_version: Published Version
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: A new proof rule for almost-sure termination
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
---
_id: '464'
abstract:
- lang: eng
text: The computation of the winning set for parity objectives and for Streett objectives
in graphs as well as in game graphs are central problems in computer-aided verification,
with application to the verification of closed systems with strong fairness conditions,
the verification of open systems, checking interface compatibility, well-formedness
of specifications, and the synthesis of reactive systems. We show how to compute
the winning set on n vertices for (1) parity-3 (aka one-pair Streett) objectives
in game graphs in time O(n5/2) and for (2) k-pair Streett objectives in graphs
in time O(n2+nklogn). For both problems this gives faster algorithms for dense
graphs and represents the first improvement in asymptotic running time in 15 years.
article_number: '26'
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: Veronika
full_name: Loitzenbauer, Veronika
last_name: Loitzenbauer
citation:
ama: Chatterjee K, Henzinger MH, Loitzenbauer V. Improved algorithms for parity
and Streett objectives. Logical Methods in Computer Science. 2017;13(3).
doi:10.23638/LMCS-13(3:26)2017
apa: Chatterjee, K., Henzinger, M. H., & Loitzenbauer, V. (2017). Improved algorithms
for parity and Streett objectives. Logical Methods in Computer Science.
International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(3:26)2017
chicago: Chatterjee, Krishnendu, Monika H Henzinger, and Veronika Loitzenbauer.
“Improved Algorithms for Parity and Streett Objectives.” Logical Methods in
Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(3:26)2017.
ieee: K. Chatterjee, M. H. Henzinger, and V. Loitzenbauer, “Improved algorithms
for parity and Streett objectives,” Logical Methods in Computer Science,
vol. 13, no. 3. International Federation of Computational Logic, 2017.
ista: Chatterjee K, Henzinger MH, Loitzenbauer V. 2017. Improved algorithms for
parity and Streett objectives. Logical Methods in Computer Science. 13(3), 26.
mla: Chatterjee, Krishnendu, et al. “Improved Algorithms for Parity and Streett
Objectives.” Logical Methods in Computer Science, vol. 13, no. 3, 26, International
Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(3:26)2017.
short: K. Chatterjee, M.H. Henzinger, V. Loitzenbauer, Logical Methods in Computer
Science 13 (2017).
date_created: 2018-12-11T11:46:37Z
date_published: 2017-09-26T00:00:00Z
date_updated: 2023-02-23T10:08:55Z
day: '26'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.23638/LMCS-13(3:26)2017
ec_funded: 1
external_id:
arxiv:
- '1410.0833'
file:
- access_level: open_access
checksum: 12d469ae69b80361333d7dead965cf5d
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:27Z
date_updated: 2020-07-14T12:46:32Z
file_id: '5010'
file_name: IST-2018-956-v1+1_2017_Chatterjee_Improved_algorithms.pdf
file_size: 582940
relation: main_file
file_date_updated: 2020-07-14T12:46:32Z
has_accepted_license: '1'
intvolume: ' 13'
issue: '3'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '09'
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: 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'
publication: Logical Methods in Computer Science
publication_identifier:
issn:
- 1860-5974
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '7357'
pubrep_id: '956'
quality_controlled: '1'
related_material:
record:
- id: '1661'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Improved algorithms for parity and Streett objectives
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2017'
...
---
_id: '466'
abstract:
- lang: eng
text: 'We consider Markov decision processes (MDPs) with multiple limit-average
(or mean-payoff) objectives. There exist two different views: (i) the expectation
semantics, where the goal is to optimize the expected mean-payoff objective, and
(ii) the satisfaction semantics, where the goal is to maximize the probability
of runs such that the mean-payoff value stays above a given vector. We consider
optimization with respect to both objectives at once, thus unifying the existing
semantics. Precisely, the goal is to optimize the expectation while ensuring the
satisfaction constraint. Our problem captures the notion of optimization with
respect to strategies that are risk-averse (i.e., ensure certain probabilistic
guarantee). Our main results are as follows: First, we present algorithms for
the decision problems which are always polynomial in the size of the MDP. We also
show that an approximation of the Pareto-curve can be computed in time polynomial
in the size of the MDP, and the approximation factor, but exponential in the number
of dimensions. Second, we present a complete characterization of the strategy
complexity (in terms of memory bounds and randomization) required to solve our
problem. '
article_number: '15'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Zuzana
full_name: Křetínská, Zuzana
last_name: Křetínská
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff
objectives in Markov decision processes. Logical Methods in Computer Science.
2017;13(2). doi:10.23638/LMCS-13(2:15)2017
apa: Chatterjee, K., Křetínská, Z., & Kretinsky, J. (2017). Unifying two views
on multiple mean-payoff objectives in Markov decision processes. Logical Methods
in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(2:15)2017
chicago: Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical
Methods in Computer Science. International Federation of Computational Logic,
2017. https://doi.org/10.23638/LMCS-13(2:15)2017.
ieee: K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple
mean-payoff objectives in Markov decision processes,” Logical Methods in Computer
Science, vol. 13, no. 2. International Federation of Computational Logic,
2017.
ista: Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple
mean-payoff objectives in Markov decision processes. Logical Methods in Computer
Science. 13(2), 15.
mla: Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes.” Logical Methods in Computer Science,
vol. 13, no. 2, 15, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(2:15)2017.
short: K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science
13 (2017).
date_created: 2018-12-11T11:46:38Z
date_published: 2017-07-03T00:00:00Z
date_updated: 2023-02-23T12:26:16Z
day: '03'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.23638/LMCS-13(2:15)2017
ec_funded: 1
file:
- access_level: open_access
checksum: bfa405385ec6229ad5ead89ab5751639
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:32Z
date_updated: 2020-07-14T12:46:33Z
file_id: '5354'
file_name: IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf
file_size: 511832
relation: main_file
file_date_updated: 2020-07-14T12:46:33Z
has_accepted_license: '1'
intvolume: ' 13'
issue: '2'
language:
- iso: eng
month: '07'
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
- _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: 2590DB08-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '701309'
name: Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes
(H2020)
publication: Logical Methods in Computer Science
publication_identifier:
issn:
- '18605974'
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '7355'
pubrep_id: '957'
quality_controlled: '1'
related_material:
record:
- id: '1657'
relation: earlier_version
status: public
- id: '5429'
relation: earlier_version
status: public
- id: '5435'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Unifying two views on multiple mean-payoff objectives in Markov decision processes
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2017'
...
---
_id: '467'
abstract:
- lang: eng
text: Recently there has been a significant effort to handle quantitative properties
in formal verification and synthesis. While weighted automata over finite and
infinite words provide a natural and flexible framework to express quantitative
properties, perhaps surprisingly, some basic system properties such as average
response time cannot be expressed using weighted automata or in any other known
decidable formalism. In this work, we introduce nested weighted automata as a
natural extension of weighted automata, which makes it possible to express important
quantitative properties such as average response time. In nested weighted automata,
a master automaton spins off and collects results from weighted slave automata,
each of which computes a quantity along a finite portion of an infinite word.
Nested weighted automata can be viewed as the quantitative analogue of monitor
automata, which are used in runtime verification. We establish an almost-complete
decidability picture for the basic decision problems about nested weighted automata
and illustrate their applicability in several domains. In particular, nested weighted
automata can be used to decide average response time properties.
article_number: '31'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. ACM Transactions
on Computational Logic (TOCL). 2017;18(4). doi:10.1145/3152769
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2017). Nested weighted automata.
ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/3152769
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted
Automata.” ACM Transactions on Computational Logic (TOCL). ACM, 2017. https://doi.org/10.1145/3152769.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” ACM
Transactions on Computational Logic (TOCL), vol. 18, no. 4. ACM, 2017.
ista: Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions
on Computational Logic (TOCL). 18(4), 31.
mla: Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” ACM Transactions
on Computational Logic (TOCL), vol. 18, no. 4, 31, ACM, 2017, doi:10.1145/3152769.
short: K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational
Logic (TOCL) 18 (2017).
date_created: 2018-12-11T11:46:38Z
date_published: 2017-12-01T00:00:00Z
date_updated: 2023-02-23T12:26:19Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/3152769
ec_funded: 1
external_id:
arxiv:
- '1606.03598'
intvolume: ' 18'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1606.03598
month: '12'
oa: 1
oa_version: Preprint
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: 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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: ACM Transactions on Computational Logic (TOCL)
publication_identifier:
issn:
- '15293785'
publication_status: published
publisher: ACM
publist_id: '7354'
quality_controlled: '1'
related_material:
record:
- id: '1656'
relation: earlier_version
status: public
- id: '5415'
relation: earlier_version
status: public
- id: '5436'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Nested weighted automata
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2017'
...
---
_id: '465'
abstract:
- lang: eng
text: 'The edit distance between two words w 1 , w 2 is the minimal number of word
operations (letter insertions, deletions, and substitutions) necessary to transform
w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the
edit distance from L 1 to L 2 is the minimal number k such that for every word
from L 1 there exists a word in L 2 with edit distance at most k . We study the
edit distance computation problem between pushdown automata and their subclasses.
The problem of computing edit distance to a pushdown automaton is undecidable,
and in practice, the interesting question is to compute the edit distance from
a pushdown automaton (the implementation, a standard model for programs with recursion)
to a regular language (the specification). In this work, we present a complete
picture of decidability and complexity for the following problems: (1) deciding
whether, for a given threshold k , the edit distance from a pushdown automaton
to a finite automaton is at most k , and (2) deciding whether the edit distance
from a pushdown automaton to a finite automaton is finite. '
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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Jan
full_name: Otop, Jan
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown
automata. Logical Methods in Computer Science. 2017;13(3). doi:10.23638/LMCS-13(3:23)2017
apa: Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., & Otop, J. (2017).
Edit distance for pushdown automata. Logical Methods in Computer Science.
International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(3:23)2017
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan
Otop. “Edit Distance for Pushdown Automata.” Logical Methods in Computer Science.
International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(3:23)2017.
ieee: K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance
for pushdown automata,” Logical Methods in Computer Science, vol. 13, no.
3. International Federation of Computational Logic, 2017.
ista: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for
pushdown automata. Logical Methods in Computer Science. 13(3).
mla: Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” Logical
Methods in Computer Science, vol. 13, no. 3, International Federation of Computational
Logic, 2017, doi:10.23638/LMCS-13(3:23)2017.
short: K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods
in Computer Science 13 (2017).
date_created: 2018-12-11T11:46:37Z
date_published: 2017-09-13T00:00:00Z
date_updated: 2023-02-23T12:26:25Z
day: '13'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.23638/LMCS-13(3:23)2017
ec_funded: 1
file:
- access_level: open_access
checksum: 08041379ba408d40664f449eb5907a8f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:37Z
date_updated: 2020-07-14T12:46:33Z
file_id: '5090'
file_name: IST-2015-321-v1+1_main.pdf
file_size: 279071
relation: main_file
- access_level: open_access
checksum: 08041379ba408d40664f449eb5907a8f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:38Z
date_updated: 2020-07-14T12:46:33Z
file_id: '5091'
file_name: IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf
file_size: 279071
relation: main_file
file_date_updated: 2020-07-14T12:46:33Z
has_accepted_license: '1'
intvolume: ' 13'
issue: '3'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _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: 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: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: Logical Methods in Computer Science
publication_identifier:
issn:
- '18605974'
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '7356'
pubrep_id: '955'
quality_controlled: '1'
related_material:
record:
- id: '1610'
relation: earlier_version
status: public
- id: '5438'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Edit distance for pushdown automata
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2017'
...
---
_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
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'
...