---
_id: '1325'
abstract:
- lang: eng
text: We study graphs and two-player games in which rewards are assigned to states,
and the goal of the players is to satisfy or dissatisfy certain property of the
generated outcome, given as a mean payoff property. Since the notion of mean-payoff
does not reflect possible fluctuations from the mean-payoff along a run, we propose
definitions and algorithms for capturing the stability of the system, and give
algorithms for deciding if a given mean payoff and stability objective can be
ensured in the system.
acknowledgement: "The work has been supported by the Czech Science Foundation, grant
No. 15-17564S, by EPSRC grant\r\nEP/M023656/1, and by the People Programme (Marie
Curie Actions) of the European Union’s Seventh\r\nFramework Programme (FP7/2007-2013)
under REA grant agreement no [291734]"
alternative_title:
- LIPIcs
article_number: '10'
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Forejt V, Kučera A, Novotný P. Stability in graphs and games. In:
Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.10'
apa: 'Brázdil, T., Forejt, V., Kučera, A., & Novotný, P. (2016). Stability in
graphs and games (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec
City, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.10'
chicago: Brázdil, Tomáš, Vojtěch Forejt, Antonín Kučera, and Petr Novotný. “Stability
in Graphs and Games,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.10.
ieee: 'T. Brázdil, V. Forejt, A. Kučera, and P. Novotný, “Stability in graphs and
games,” presented at the CONCUR: Concurrency Theory, Quebec City, Canada, 2016,
vol. 59.'
ista: 'Brázdil T, Forejt V, Kučera A, Novotný P. 2016. Stability in graphs and games.
CONCUR: Concurrency Theory, LIPIcs, vol. 59, 10.'
mla: Brázdil, Tomáš, et al. Stability in Graphs and Games. Vol. 59, 10, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.10.
short: T. Brázdil, V. Forejt, A. Kučera, P. Novotný, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Quebec City, Canada
name: 'CONCUR: Concurrency Theory'
start_date: 2016-08-23
date_created: 2018-12-11T11:51:23Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2016.10
ec_funded: 1
file:
- access_level: open_access
checksum: 3c2dc6ab0358f8aa8f7aa7d6c1293159
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:40Z
date_updated: 2020-07-14T12:44:44Z
file_id: '5229'
file_name: IST-2016-665-v1+1_Forejt_et_al__Stability_in_graphs_and_games.pdf
file_size: 553648
relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: ' 59'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5944'
pubrep_id: '665'
quality_controlled: '1'
scopus_import: 1
status: public
title: Stability in graphs and games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1324'
abstract:
- lang: eng
text: 'DEC-POMDPs extend POMDPs to a multi-agent setting, where several agents operate
in an uncertain environment independently to achieve a joint objective. DEC-POMDPs
have been studied with finite-horizon and infinite-horizon discounted-sum objectives,
and there exist solvers both for exact and approximate solutions. In this work
we consider Goal-DEC-POMDPs, where given a set of target states, the objective
is to ensure that the target set is reached with minimal cost. We consider the
indefinite-horizon (infinite-horizon with either discounted-sum, or undiscounted-sum,
where absorbing goal states have zero-cost) problem. We present a new and novel
method to solve the problem that extends methods for finite-horizon DEC-POMDPs
and the RTDP-Bel approach for POMDPs. We present experimental results on several
examples, and show that our approach presents promising results. Copyright '
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: 'Chatterjee K, Chmelik M. Indefinite-horizon reachability in Goal-DEC-POMDPs.
In: Proceedings of the Twenty-Sixth International Conference on International
Conference on Automated Planning and Scheduling. Vol 2016-January. AAAI Press;
2016:88-96.'
apa: 'Chatterjee, K., & Chmelik, M. (2016). Indefinite-horizon reachability
in Goal-DEC-POMDPs. In Proceedings of the Twenty-Sixth International Conference
on International Conference on Automated Planning and Scheduling (Vol. 2016–January,
pp. 88–96). London, United Kingdom: AAAI Press.'
chicago: Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability
in Goal-DEC-POMDPs.” In Proceedings of the Twenty-Sixth International Conference
on International Conference on Automated Planning and Scheduling, 2016–January:88–96.
AAAI Press, 2016.
ieee: K. Chatterjee and M. Chmelik, “Indefinite-horizon reachability in Goal-DEC-POMDPs,”
in Proceedings of the Twenty-Sixth International Conference on International
Conference on Automated Planning and Scheduling, London, United Kingdom, 2016,
vol. 2016–January, pp. 88–96.
ista: 'Chatterjee K, Chmelik M. 2016. Indefinite-horizon reachability in Goal-DEC-POMDPs.
Proceedings of the Twenty-Sixth International Conference on International Conference
on Automated Planning and Scheduling. ICAPS: International Conference on Automated
Planning and Scheduling vol. 2016–January, 88–96.'
mla: Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability
in Goal-DEC-POMDPs.” Proceedings of the Twenty-Sixth International Conference
on International Conference on Automated Planning and Scheduling, vol. 2016–January,
AAAI Press, 2016, pp. 88–96.
short: K. Chatterjee, M. Chmelik, in:, Proceedings of the Twenty-Sixth International
Conference on International Conference on Automated Planning and Scheduling, AAAI
Press, 2016, pp. 88–96.
conference:
end_date: 2016-06-17
location: London, United Kingdom
name: 'ICAPS: International Conference on Automated Planning and Scheduling'
start_date: 2016-06-12
date_created: 2018-12-11T11:51:22Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
language:
- iso: eng
main_file_link:
- url: http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/12999
month: '01'
oa_version: None
page: 88 - 96
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Proceedings of the Twenty-Sixth International Conference on International
Conference on Automated Planning and Scheduling
publication_status: published
publisher: AAAI Press
publist_id: '5946'
quality_controlled: '1'
scopus_import: 1
status: public
title: Indefinite-horizon reachability in Goal-DEC-POMDPs
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 2016-January
year: '2016'
...
---
_id: '1327'
abstract:
- lang: eng
text: 'We consider partially observable Markov decision processes (POMDPs) with
a set of target states and positive integer costs associated with every transition.
The traditional optimization objective (stochastic shortest path) asks to minimize
the expected total cost until the target set is reached. We extend the traditional
framework of POMDPs to model energy consumption, which represents a hard constraint.
The energy levels may increase and decrease with transitions, and the hard constraint
requires that the energy level must remain positive in all steps till the target
is reached. First, we present a novel algorithm for solving POMDPs with energy
levels, developing on existing POMDP solvers and using RTDP as its main method.
Our second contribution is related to policy representation. For larger POMDP
instances the policies computed by existing solvers are too large to be understandable.
We present an automated procedure based on machine learning techniques that automatically
extracts important decisions of the policy allowing us to compute succinct human
readable policies. Finally, we show experimentally that our algorithm performs
well and computes succinct policies on a number of POMDP instances from the literature
that were naturally enhanced with energy levels. '
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Anchit
full_name: Gupta, Anchit
last_name: Gupta
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. Stochastic shortest
path with energy constraints in POMDPs. In: Proceedings of the 15th International
Conference on Autonomous Agents and Multiagent Systems. ACM; 2016:1465-1466.'
apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Gupta, A., & Novotný, P. (2016).
Stochastic shortest path with energy constraints in POMDPs. In Proceedings
of the 15th International Conference on Autonomous Agents and Multiagent Systems
(pp. 1465–1466). Singapore: ACM.'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Anchit Gupta, and
Petr Novotný. “Stochastic Shortest Path with Energy Constraints in POMDPs.” In
Proceedings of the 15th International Conference on Autonomous Agents and Multiagent
Systems, 1465–66. ACM, 2016.
ieee: T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, and P. Novotný, “Stochastic
shortest path with energy constraints in POMDPs,” in Proceedings of the 15th
International Conference on Autonomous Agents and Multiagent Systems, Singapore,
2016, pp. 1465–1466.
ista: 'Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. 2016. Stochastic
shortest path with energy constraints in POMDPs. Proceedings of the 15th International
Conference on Autonomous Agents and Multiagent Systems. AAMAS: Autonomous Agents
& Multiagent Systems, 1465–1466.'
mla: Brázdil, Tomáš, et al. “Stochastic Shortest Path with Energy Constraints in
POMDPs.” Proceedings of the 15th International Conference on Autonomous Agents
and Multiagent Systems, ACM, 2016, pp. 1465–66.
short: T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, P. Novotný, in:, Proceedings
of the 15th International Conference on Autonomous Agents and Multiagent Systems,
ACM, 2016, pp. 1465–1466.
conference:
end_date: 2016-05-13
location: Singapore
name: 'AAMAS: Autonomous Agents & Multiagent Systems'
start_date: 2016-05-09
date_created: 2018-12-11T11:51:23Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:49:54Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1602.07565
month: '01'
oa: 1
oa_version: Preprint
page: 1465 - 1466
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the 15th International Conference on Autonomous Agents
and Multiagent Systems
publication_status: published
publisher: ACM
publist_id: '5942'
quality_controlled: '1'
scopus_import: 1
status: public
title: Stochastic shortest path with energy constraints in POMDPs
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1326'
abstract:
- lang: eng
text: 'Energy Markov Decision Processes (EMDPs) are finite-state Markov decision
processes where each transition is assigned an integer counter update and a rational
payoff. An EMDP configuration is a pair s(n), where s is a control state and n
is the current counter value. The configurations are changed by performing transitions
in the standard way. We consider the problem of computing a safe strategy (i.e.,
a strategy that keeps the counter non-negative) which maximizes the expected mean
payoff. '
acknowledgement: The research was funded by the Czech Science Foundation Grant No.
P202/12/G061 and by the People Programme (Marie Curie Actions) of the European Union’s
Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no [291734].
alternative_title:
- LNCS
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Kučera A, Novotný P. Optimizing the expected mean payoff in Energy
Markov Decision Processes. In: Vol 9938. Springer; 2016:32-49. doi:10.1007/978-3-319-46520-3_3'
apa: 'Brázdil, T., Kučera, A., & Novotný, P. (2016). Optimizing the expected
mean payoff in Energy Markov Decision Processes (Vol. 9938, pp. 32–49). Presented
at the ATVA: Automated Technology for Verification and Analysis, Chiba, Japan:
Springer. https://doi.org/10.1007/978-3-319-46520-3_3'
chicago: Brázdil, Tomáš, Antonín Kučera, and Petr Novotný. “Optimizing the Expected
Mean Payoff in Energy Markov Decision Processes,” 9938:32–49. Springer, 2016.
https://doi.org/10.1007/978-3-319-46520-3_3.
ieee: 'T. Brázdil, A. Kučera, and P. Novotný, “Optimizing the expected mean payoff
in Energy Markov Decision Processes,” presented at the ATVA: Automated Technology
for Verification and Analysis, Chiba, Japan, 2016, vol. 9938, pp. 32–49.'
ista: 'Brázdil T, Kučera A, Novotný P. 2016. Optimizing the expected mean payoff
in Energy Markov Decision Processes. ATVA: Automated Technology for Verification
and Analysis, LNCS, vol. 9938, 32–49.'
mla: Brázdil, Tomáš, et al. Optimizing the Expected Mean Payoff in Energy Markov
Decision Processes. Vol. 9938, Springer, 2016, pp. 32–49, doi:10.1007/978-3-319-46520-3_3.
short: T. Brázdil, A. Kučera, P. Novotný, in:, Springer, 2016, pp. 32–49.
conference:
end_date: 2016-10-20
location: Chiba, Japan
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2016-10-17
date_created: 2018-12-11T11:51:23Z
date_published: 2016-09-22T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '22'
department:
- _id: KrCh
doi: 10.1007/978-3-319-46520-3_3
ec_funded: 1
intvolume: ' 9938'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1607.00678
month: '09'
oa: 1
oa_version: Preprint
page: 32 - 49
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5943'
quality_controlled: '1'
scopus_import: 1
status: public
title: Optimizing the expected mean payoff in Energy Markov Decision Processes
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9938
year: '2016'
...
---
_id: '1333'
abstract:
- lang: eng
text: Social dilemmas force players to balance between personal and collective gain.
In many dilemmas, such as elected governments negotiating climate-change mitigation
measures, the decisions are made not by individual players but by their representatives.
However, the behaviour of representatives in social dilemmas has not been investigated
experimentally. Here inspired by the negotiations for greenhouse-gas emissions
reductions, we experimentally study a collective-risk social dilemma that involves
representatives deciding on behalf of their fellow group members. Representatives
can be re-elected or voted out after each consecutive collective-risk game. Selfish
players are preferentially elected and are hence found most frequently in the
"representatives" treatment. Across all treatments, we identify the
selfish players as extortioners. As predicted by our mathematical model, their
steadfast strategies enforce cooperation from fair players who finally compensate
almost completely the deficit caused by the extortionate co-players. Everybody
gains, but the extortionate representatives and their groups gain the most.
acknowledgement: We thank the students for participation; H.-J. Krambeck for writing
the software for the game; H. Arndt, T. Bakker, L. Becks, H. Brendelberger, S. Dobler
and T. Reusch for support; and the Max Planck Society for the Advancement of Science
for funding.
article_number: '10915'
author:
- first_name: Manfred
full_name: Milinski, Manfred
last_name: Milinski
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Dirk
full_name: Semmann, Dirk
last_name: Semmann
- first_name: Ralf
full_name: Sommerfeld, Ralf
last_name: Sommerfeld
- first_name: Jochem
full_name: Marotzke, Jochem
last_name: Marotzke
citation:
ama: Milinski M, Hilbe C, Semmann D, Sommerfeld R, Marotzke J. Humans choose representatives
who enforce cooperation in social dilemmas through extortion. Nature Communications.
2016;7. doi:10.1038/ncomms10915
apa: Milinski, M., Hilbe, C., Semmann, D., Sommerfeld, R., & Marotzke, J. (2016).
Humans choose representatives who enforce cooperation in social dilemmas through
extortion. Nature Communications. Nature Publishing Group. https://doi.org/10.1038/ncomms10915
chicago: Milinski, Manfred, Christian Hilbe, Dirk Semmann, Ralf Sommerfeld, and
Jochem Marotzke. “Humans Choose Representatives Who Enforce Cooperation in Social
Dilemmas through Extortion.” Nature Communications. Nature Publishing Group,
2016. https://doi.org/10.1038/ncomms10915.
ieee: M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, and J. Marotzke, “Humans
choose representatives who enforce cooperation in social dilemmas through extortion,”
Nature Communications, vol. 7. Nature Publishing Group, 2016.
ista: Milinski M, Hilbe C, Semmann D, Sommerfeld R, Marotzke J. 2016. Humans choose
representatives who enforce cooperation in social dilemmas through extortion.
Nature Communications. 7, 10915.
mla: Milinski, Manfred, et al. “Humans Choose Representatives Who Enforce Cooperation
in Social Dilemmas through Extortion.” Nature Communications, vol. 7, 10915,
Nature Publishing Group, 2016, doi:10.1038/ncomms10915.
short: M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, J. Marotzke, Nature Communications
7 (2016).
date_created: 2018-12-11T11:51:25Z
date_published: 2016-03-07T00:00:00Z
date_updated: 2021-01-12T06:49:57Z
day: '07'
ddc:
- '519'
- '530'
- '599'
department:
- _id: KrCh
doi: 10.1038/ncomms10915
file:
- access_level: open_access
checksum: 9ea0d7ce59a555a1cb8353d5559407cb
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:44Z
date_updated: 2020-07-14T12:44:44Z
file_id: '4834'
file_name: IST-2016-661-v1+1_ncomms10915.pdf
file_size: 1432577
relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: ' 7'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
publication: Nature Communications
publication_status: published
publisher: Nature Publishing Group
publist_id: '5935'
pubrep_id: '661'
quality_controlled: '1'
scopus_import: 1
status: public
title: Humans choose representatives who enforce cooperation in social dilemmas through
extortion
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7
year: '2016'
...
---
_id: '1335'
abstract:
- lang: eng
text: In this paper we review various automata-theoretic formalisms for expressing
quantitative properties. We start with finite-state Boolean automata that express
the traditional regular properties. We then consider weighted ω-automata that
can measure the average density of events, which finite-state Boolean automata
cannot. However, even weighted ω-automata cannot express basic performance properties
like average response time. We finally consider two formalisms of weighted ω-automata
with monitors, where the monitors are either (a) counters or (b) weighted automata
themselves. We present a translation result to establish that these two formalisms
are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata,
and can express average response time property. They present a natural, robust,
and expressive framework for quantitative specifications, with important decidable
properties.
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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: 'Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol
9837. Springer; 2016:23-38. doi:10.1007/978-3-662-53413-7_2'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative monitor
automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium,
Edinburgh, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53413-7_2'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative
Monitor Automata,” 9837:23–38. Springer, 2016. https://doi.org/10.1007/978-3-662-53413-7_2.
ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative monitor automata,”
presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom, 2016,
vol. 9837, pp. 23–38.'
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata.
SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.'
mla: Chatterjee, Krishnendu, et al. Quantitative Monitor Automata. Vol. 9837,
Springer, 2016, pp. 23–38, doi:10.1007/978-3-662-53413-7_2.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38.
conference:
end_date: 2016-09-10
location: Edinburgh, United Kingdom
name: 'SAS: Static Analysis Symposium'
start_date: 2016-09-08
date_created: 2018-12-11T11:51:26Z
date_published: 2016-08-31T00:00:00Z
date_updated: 2021-01-12T06:49:58Z
day: '31'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-53413-7_2
ec_funded: 1
intvolume: ' 9837'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.06764
month: '08'
oa: 1
oa_version: Preprint
page: 23 - 38
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Springer
publist_id: '5932'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative monitor automata
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9837
year: '2016'
...
---
_id: '1340'
abstract:
- lang: eng
text: We study repeated games with absorbing states, a type of two-player, zero-sum
concurrent mean-payoff games with the prototypical example being the Big Match
of Gillete (1957). These games may not allow optimal strategies but they always
have ε-optimal strategies. In this paper we design ε-optimal strategies for Player
1 in these games that use only O(log log T) space. Furthermore, we construct strategies
for Player 1 that use space s(T), for an arbitrary small unbounded non-decreasing
function s, and which guarantee an ε-optimal value for Player 1 in the limit superior
sense. The previously known strategies use space Ω(log T) and it was known that
no strategy can use constant space if it is ε-optimal even in the limit superior
sense. We also give a complementary lower bound. Furthermore, we also show that
no Markov strategy, even extended with finite memory, can ensure value greater
than 0 in the Big Match, answering a question posed by Neyman [11].
alternative_title:
- LNCS
author:
- first_name: Kristoffer
full_name: Hansen, Kristoffer
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: Michal
full_name: Koucký, Michal
last_name: Koucký
citation:
ama: 'Hansen K, Ibsen-Jensen R, Koucký M. The big match in small space. In: Vol
9928. Springer; 2016:64-76. doi:10.1007/978-3-662-53354-3_6'
apa: 'Hansen, K., Ibsen-Jensen, R., & Koucký, M. (2016). The big match in small
space (Vol. 9928, pp. 64–76). Presented at the SAGT: Symposium on Algorithmic
Game Theory, Liverpool, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53354-3_6'
chicago: Hansen, Kristoffer, Rasmus Ibsen-Jensen, and Michal Koucký. “The Big Match
in Small Space,” 9928:64–76. Springer, 2016. https://doi.org/10.1007/978-3-662-53354-3_6.
ieee: 'K. Hansen, R. Ibsen-Jensen, and M. Koucký, “The big match in small space,”
presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United
Kingdom, 2016, vol. 9928, pp. 64–76.'
ista: 'Hansen K, Ibsen-Jensen R, Koucký M. 2016. The big match in small space. SAGT:
Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 64–76.'
mla: Hansen, Kristoffer, et al. The Big Match in Small Space. Vol. 9928,
Springer, 2016, pp. 64–76, doi:10.1007/978-3-662-53354-3_6.
short: K. Hansen, R. Ibsen-Jensen, M. Koucký, in:, Springer, 2016, pp. 64–76.
conference:
end_date: 2016-09-21
location: Liverpool, United Kingdom
name: 'SAGT: Symposium on Algorithmic Game Theory'
start_date: 2016-09-19
date_created: 2018-12-11T11:51:28Z
date_published: 2016-09-01T00:00:00Z
date_updated: 2021-01-12T06:50:00Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-53354-3_6
ec_funded: 1
intvolume: ' 9928'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.07634
month: '09'
oa: 1
oa_version: Preprint
page: 64 - 76
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_status: published
publisher: Springer
publist_id: '5927'
quality_controlled: '1'
scopus_import: 1
status: public
title: The big match in small space
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9928
year: '2016'
...
---
_id: '1380'
abstract:
- lang: eng
text: We consider higher-dimensional versions of Kannan and Lipton's Orbit Problem
- determining whether a target vector space V may be reached from a starting point
x under repeated applications of a linear transformation A. Answering two questions
posed by Kannan and Lipton in the 1980s, we show that when V has dimension one,
this problem is solvable in polynomial time, and when V has dimension two or three,
the problem is in NPRP.
article_number: '23'
author:
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
- first_name: Joël
full_name: Ouaknine, Joël
last_name: Ouaknine
- first_name: James
full_name: Worrell, James
last_name: Worrell
citation:
ama: Chonev VK, Ouaknine J, Worrell J. On the complexity of the orbit problem. Journal
of the ACM. 2016;63(3). doi:10.1145/2857050
apa: Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the complexity of
the orbit problem. Journal of the ACM. ACM. https://doi.org/10.1145/2857050
chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Complexity
of the Orbit Problem.” Journal of the ACM. ACM, 2016. https://doi.org/10.1145/2857050.
ieee: V. K. Chonev, J. Ouaknine, and J. Worrell, “On the complexity of the orbit
problem,” Journal of the ACM, vol. 63, no. 3. ACM, 2016.
ista: Chonev VK, Ouaknine J, Worrell J. 2016. On the complexity of the orbit problem.
Journal of the ACM. 63(3), 23.
mla: Chonev, Ventsislav K., et al. “On the Complexity of the Orbit Problem.” Journal
of the ACM, vol. 63, no. 3, 23, ACM, 2016, doi:10.1145/2857050.
short: V.K. Chonev, J. Ouaknine, J. Worrell, Journal of the ACM 63 (2016).
date_created: 2018-12-11T11:51:41Z
date_published: 2016-06-01T00:00:00Z
date_updated: 2021-01-12T06:50:17Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2857050
intvolume: ' 63'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1303.2981
month: '06'
oa: 1
oa_version: Preprint
publication: Journal of the ACM
publication_status: published
publisher: ACM
publist_id: '5831'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the complexity of the orbit problem
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 63
year: '2016'
...
---
_id: '1389'
abstract:
- lang: eng
text: "The continuous evolution of a wide variety of systems, including continous-time
Markov chains and linear hybrid automata, can be\r\ndescribed in terms of linear
differential equations. In this paper we study the decision problem of whether
the solution x(t) of a system of linear differential equations dx/dt = Ax reaches
a target halfspace infinitely often. This recurrent reachability problem can\r\nequivalently
be formulated as the following Infinite Zeros Problem: does a real-valued function
f:R≥0 --> R satisfying a given linear\r\ndifferential equation have infinitely
many zeros? Our main decidability result is that if the differential equation
has order at most 7, then the Infinite Zeros Problem is decidable. On the other
hand, we show that a decision procedure for the Infinite Zeros Problem at order
9 (and above) would entail a major breakthrough in Diophantine Approximation,
specifically an algorithm for computing the Lagrange constants of arbitrary real
algebraic numbers to arbitrary precision."
author:
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
- first_name: Joël
full_name: Ouaknine, Joël
last_name: Ouaknine
- first_name: James
full_name: Worrell, James
last_name: Worrell
citation:
ama: 'Chonev VK, Ouaknine J, Worrell J. On recurrent reachability for continuous
linear dynamical systems. In: LICS ’16. IEEE; 2016:515-524. doi:10.1145/2933575.2934548'
apa: 'Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On recurrent reachability
for continuous linear dynamical systems. In LICS ’16 (pp. 515–524). New
York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2934548'
chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On Recurrent Reachability
for Continuous Linear Dynamical Systems.” In LICS ’16, 515–24. IEEE, 2016.
https://doi.org/10.1145/2933575.2934548.
ieee: V. K. Chonev, J. Ouaknine, and J. Worrell, “On recurrent reachability for
continuous linear dynamical systems,” in LICS ’16, New York, NY, USA, 2016,
pp. 515–524.
ista: 'Chonev VK, Ouaknine J, Worrell J. 2016. On recurrent reachability for continuous
linear dynamical systems. LICS ’16. LICS: Logic in Computer Science, 515–524.'
mla: Chonev, Ventsislav K., et al. “On Recurrent Reachability for Continuous Linear
Dynamical Systems.” LICS ’16, IEEE, 2016, pp. 515–24, doi:10.1145/2933575.2934548.
short: V.K. Chonev, J. Ouaknine, J. Worrell, in:, LICS ’16, IEEE, 2016, pp. 515–524.
conference:
end_date: 2018-07-08
location: New York, NY, USA
name: 'LICS: Logic in Computer Science'
start_date: 2018-07-05
date_created: 2018-12-11T11:51:44Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2021-01-12T06:50:20Z
day: '05'
department:
- _id: KrCh
doi: 10.1145/2933575.2934548
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1507.03632
month: '07'
oa: 1
oa_version: Preprint
page: 515 - 524
project:
- _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: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: LICS '16
publication_status: published
publisher: IEEE
publist_id: '5820'
quality_controlled: '1'
scopus_import: 1
status: public
title: On recurrent reachability for continuous linear dynamical systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1426'
abstract:
- lang: eng
text: 'Brood parasites exploit their host in order to increase their own fitness.
Typically, this results in an arms race between parasite trickery and host defence.
Thus, it is puzzling to observe hosts that accept parasitism without any resistance.
The ‘mafia’ hypothesis suggests that these hosts accept parasitism to avoid retaliation.
Retaliation has been shown to evolve when the hosts condition their response to
mafia parasites, who use depredation as a targeted response to rejection. However,
it is unclear if acceptance would also emerge when ‘farming’ parasites are present
in the population. Farming parasites use depredation to synchronize the timing
with the host, destroying mature clutches to force the host to re-nest. Herein,
we develop an evolutionary model to analyse the interaction between depredatory
parasites and their hosts. We show that coevolutionary cycles between farmers
and mafia can still induce host acceptance of brood parasites. However, this equilibrium
is unstable and in the long-run the dynamics of this host–parasite interaction
exhibits strong oscillations: when farmers are the majority, accepters conditional
to mafia (the host will reject first and only accept after retaliation by the
parasite) have a higher fitness than unconditional accepters (the host always
accepts parasitism). This leads to an increase in mafia parasites’ fitness and
in turn induce an optimal environment for accepter hosts.'
acknowledgement: C.H. gratefully acknowledges funding by the Schrödinger scholarship
of the Austrian Science Fund (FWF) J3475.
article_number: '160036'
author:
- first_name: Maria
full_name: Chakra, Maria
last_name: Chakra
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Arne
full_name: Traulsen, Arne
last_name: Traulsen
citation:
ama: Chakra M, Hilbe C, Traulsen A. Coevolutionary interactions between farmers
and mafia induce host acceptance of avian brood parasites. Royal Society Open
Science. 2016;3(5). doi:10.1098/rsos.160036
apa: Chakra, M., Hilbe, C., & Traulsen, A. (2016). Coevolutionary interactions
between farmers and mafia induce host acceptance of avian brood parasites. Royal
Society Open Science. Royal Society, The. https://doi.org/10.1098/rsos.160036
chicago: Chakra, Maria, Christian Hilbe, and Arne Traulsen. “Coevolutionary Interactions
between Farmers and Mafia Induce Host Acceptance of Avian Brood Parasites.” Royal
Society Open Science. Royal Society, The, 2016. https://doi.org/10.1098/rsos.160036.
ieee: M. Chakra, C. Hilbe, and A. Traulsen, “Coevolutionary interactions between
farmers and mafia induce host acceptance of avian brood parasites,” Royal Society
Open Science, vol. 3, no. 5. Royal Society, The, 2016.
ista: Chakra M, Hilbe C, Traulsen A. 2016. Coevolutionary interactions between farmers
and mafia induce host acceptance of avian brood parasites. Royal Society Open
Science. 3(5), 160036.
mla: Chakra, Maria, et al. “Coevolutionary Interactions between Farmers and Mafia
Induce Host Acceptance of Avian Brood Parasites.” Royal Society Open Science,
vol. 3, no. 5, 160036, Royal Society, The, 2016, doi:10.1098/rsos.160036.
short: M. Chakra, C. Hilbe, A. Traulsen, Royal Society Open Science 3 (2016).
date_created: 2018-12-11T11:51:57Z
date_published: 2016-05-01T00:00:00Z
date_updated: 2021-01-12T06:50:39Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1098/rsos.160036
file:
- access_level: open_access
checksum: bf84211b31fe87451e738ba301d729c3
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:49Z
date_updated: 2020-07-14T12:44:53Z
file_id: '5104'
file_name: IST-2016-589-v1+1_160036.full.pdf
file_size: 937002
relation: main_file
file_date_updated: 2020-07-14T12:44:53Z
has_accepted_license: '1'
intvolume: ' 3'
issue: '5'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
publication: Royal Society Open Science
publication_status: published
publisher: Royal Society, The
publist_id: '5776'
pubrep_id: '589'
quality_controlled: '1'
scopus_import: 1
status: public
title: Coevolutionary interactions between farmers and mafia induce host acceptance
of avian brood parasites
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 3
year: '2016'
...
---
_id: '1423'
abstract:
- lang: eng
text: 'Direct reciprocity is a mechanism for the evolution of cooperation based
on repeated interactions. When individuals meet repeatedly, they can use conditional
strategies to enforce cooperative outcomes that would not be feasible in one-shot
social dilemmas. Direct reciprocity requires that individuals keep track of their
past interactions and find the right response. However, there are natural bounds
on strategic complexity: Humans find it difficult to remember past interactions
accurately, especially over long timespans. Given these limitations, it is natural
to ask how complex strategies need to be for cooperation to evolve. Here, we study
stochastic evolutionary game dynamics in finite populations to systematically
compare the evolutionary performance of reactive strategies, which only respond
to the co-player''s previous move, and memory-one strategies, which take into
account the own and the co-player''s previous move. In both cases, we compare
deterministic strategy and stochastic strategy spaces. For reactive strategies
and small costs, we find that stochasticity benefits cooperation, because it allows
for generous-tit-for-tat. For memory one strategies and small costs, we find that
stochasticity does not increase the propensity for cooperation, because the deterministic
rule of win-stay, lose-shift works best. For memory one strategies and large costs,
however, stochasticity can augment cooperation.'
acknowledgement: C.H. acknowledges generous funding from the Schrödinger scholarship
of the Austrian Science Fund (FWF), J3475.
article_number: '25676'
author:
- first_name: Seung
full_name: Baek, Seung
last_name: Baek
- first_name: Hyeongchai
full_name: Jeong, Hyeongchai
last_name: Jeong
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Baek S, Jeong H, Hilbe C, Nowak M. Comparing reactive and memory-one strategies
of direct reciprocity. Scientific Reports. 2016;6. doi:10.1038/srep25676
apa: Baek, S., Jeong, H., Hilbe, C., & Nowak, M. (2016). Comparing reactive
and memory-one strategies of direct reciprocity. Scientific Reports. Nature
Publishing Group. https://doi.org/10.1038/srep25676
chicago: Baek, Seung, Hyeongchai Jeong, Christian Hilbe, and Martin Nowak. “Comparing
Reactive and Memory-One Strategies of Direct Reciprocity.” Scientific Reports.
Nature Publishing Group, 2016. https://doi.org/10.1038/srep25676.
ieee: S. Baek, H. Jeong, C. Hilbe, and M. Nowak, “Comparing reactive and memory-one
strategies of direct reciprocity,” Scientific Reports, vol. 6. Nature Publishing
Group, 2016.
ista: Baek S, Jeong H, Hilbe C, Nowak M. 2016. Comparing reactive and memory-one
strategies of direct reciprocity. Scientific Reports. 6, 25676.
mla: Baek, Seung, et al. “Comparing Reactive and Memory-One Strategies of Direct
Reciprocity.” Scientific Reports, vol. 6, 25676, Nature Publishing Group,
2016, doi:10.1038/srep25676.
short: S. Baek, H. Jeong, C. Hilbe, M. Nowak, Scientific Reports 6 (2016).
date_created: 2018-12-11T11:51:56Z
date_published: 2016-05-10T00:00:00Z
date_updated: 2021-01-12T06:50:38Z
day: '10'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/srep25676
file:
- access_level: open_access
checksum: ee17c482370d2e1b3add393710d3c696
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:08Z
date_updated: 2020-07-14T12:44:53Z
file_id: '5327'
file_name: IST-2016-590-v1+1_srep25676.pdf
file_size: 1349915
relation: main_file
file_date_updated: 2020-07-14T12:44:53Z
has_accepted_license: '1'
intvolume: ' 6'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
publication: Scientific Reports
publication_status: published
publisher: Nature Publishing Group
publist_id: '5784'
pubrep_id: '590'
quality_controlled: '1'
scopus_import: 1
status: public
title: Comparing reactive and memory-one strategies of direct reciprocity
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 6
year: '2016'
...
---
_id: '1518'
abstract:
- lang: eng
text: The inference of demographic history from genome data is hindered by a lack
of efficient computational approaches. In particular, it has proved difficult
to exploit the information contained in the distribution of genealogies across
the genome. We have previously shown that the generating function (GF) of genealogies
can be used to analytically compute likelihoods of demographic models from configurations
of mutations in short sequence blocks (Lohse et al. 2011). Although the GF has
a simple, recursive form, the size of such likelihood calculations explodes quickly
with the number of individuals and applications of this framework have so far
been mainly limited to small samples (pairs and triplets) for which the GF can
be written by hand. Here we investigate several strategies for exploiting the
inherent symmetries of the coalescent. In particular, we show that the GF of genealogies
can be decomposed into a set of equivalence classes that allows likelihood calculations
from nontrivial samples. Using this strategy, we automated blockwise likelihood
calculations for a general set of demographic scenarios in Mathematica. These
histories may involve population size changes, continuous migration, discrete
divergence, and admixture between multiple populations. To give a concrete example,
we calculate the likelihood for a model of isolation with migration (IM), assuming
two diploid samples without phase and outgroup information. We demonstrate the
new inference scheme with an analysis of two individual butterfly genomes from
the sister species Heliconius melpomene rosina and H. cydno.
acknowledgement: "We thank Lynsey Bunnefeld for discussions throughout the project
and Joshua Schraiber and one anonymous reviewer\r\nfor constructive comments on
an earlier version of this manuscript. This work was supported by funding from the\r\nUnited
Kingdom Natural Environment Research Council (to K.L.) (NE/I020288/1) and a grant
from the European\r\nResearch Council (250152) (to N.H.B.)."
article_processing_charge: No
article_type: original
author:
- first_name: Konrad
full_name: Lohse, Konrad
last_name: Lohse
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Simon
full_name: Martin, Simon
last_name: Martin
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Lohse K, Chmelik M, Martin S, Barton NH. Efficient strategies for calculating
blockwise likelihoods under the coalescent. Genetics. 2016;202(2):775-786.
doi:10.1534/genetics.115.183814
apa: Lohse, K., Chmelik, M., Martin, S., & Barton, N. H. (2016). Efficient strategies
for calculating blockwise likelihoods under the coalescent. Genetics. Genetics
Society of America. https://doi.org/10.1534/genetics.115.183814
chicago: Lohse, Konrad, Martin Chmelik, Simon Martin, and Nicholas H Barton. “Efficient
Strategies for Calculating Blockwise Likelihoods under the Coalescent.” Genetics.
Genetics Society of America, 2016. https://doi.org/10.1534/genetics.115.183814.
ieee: K. Lohse, M. Chmelik, S. Martin, and N. H. Barton, “Efficient strategies for
calculating blockwise likelihoods under the coalescent,” Genetics, vol.
202, no. 2. Genetics Society of America, pp. 775–786, 2016.
ista: Lohse K, Chmelik M, Martin S, Barton NH. 2016. Efficient strategies for calculating
blockwise likelihoods under the coalescent. Genetics. 202(2), 775–786.
mla: Lohse, Konrad, et al. “Efficient Strategies for Calculating Blockwise Likelihoods
under the Coalescent.” Genetics, vol. 202, no. 2, Genetics Society of America,
2016, pp. 775–86, doi:10.1534/genetics.115.183814.
short: K. Lohse, M. Chmelik, S. Martin, N.H. Barton, Genetics 202 (2016) 775–786.
date_created: 2018-12-11T11:52:29Z
date_published: 2016-02-01T00:00:00Z
date_updated: 2022-05-24T09:16:22Z
day: '01'
ddc:
- '570'
department:
- _id: KrCh
- _id: NiBa
doi: 10.1534/genetics.115.183814
ec_funded: 1
external_id:
pmid:
- '26715666'
file:
- access_level: open_access
checksum: 41c9b5d72e7fe4624dd22dfe622337d5
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:51Z
date_updated: 2020-07-14T12:45:00Z
file_id: '5241'
file_name: IST-2016-561-v1+1_Lohse_et_al_Genetics_2015.pdf
file_size: 957466
relation: main_file
file_date_updated: 2020-07-14T12:45:00Z
has_accepted_license: '1'
intvolume: ' 202'
issue: '2'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Preprint
page: 775 - 786
pmid: 1
project:
- _id: 25B07788-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '250152'
name: Limits to selection in biology and in evolutionary computation
publication: Genetics
publication_status: published
publisher: Genetics Society of America
publist_id: '5658'
pubrep_id: '561'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Efficient strategies for calculating blockwise likelihoods under the coalescent
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 202
year: '2016'
...
---
_id: '478'
abstract:
- lang: eng
text: 'Magic: the Gathering is a game about magical combat for any number of players.
Formally it is a zero-sum, imperfect information stochastic game that consists
of a potentially unbounded number of steps. We consider the problem of deciding
if a move is legal in a given single step of Magic. We show that the problem is
(a) coNP-complete in general; and (b) in P if either of two small sets of cards
are not used. Our lower bound holds even for single-player Magic games. The significant
aspects of our results are as follows: First, in most real-life game problems,
the task of deciding whether a given move is legal in a single step is trivial,
and the computationally hard task is to find the best sequence of legal moves
in the presence of multiple players. In contrast, quite uniquely our hardness
result holds for single step and with only one-player. Second, we establish efficient
algorithms for important special cases of Magic.'
alternative_title:
- Frontiers in Artificial Intelligence and Applications
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
citation:
ama: 'Chatterjee K, Ibsen-Jensen R. The complexity of deciding legality of a single
step of magic: The gathering. In: Vol 285. IOS Press; 2016:1432-1439. doi:10.3233/978-1-61499-672-9-1432'
apa: 'Chatterjee, K., & Ibsen-Jensen, R. (2016). The complexity of deciding
legality of a single step of magic: The gathering (Vol. 285, pp. 1432–1439). Presented
at the ECAI: European Conference on Artificial Intelligence, The Hague, Netherlands:
IOS Press. https://doi.org/10.3233/978-1-61499-672-9-1432'
chicago: 'Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Complexity of Deciding
Legality of a Single Step of Magic: The Gathering,” 285:1432–39. IOS Press, 2016.
https://doi.org/10.3233/978-1-61499-672-9-1432.'
ieee: 'K. Chatterjee and R. Ibsen-Jensen, “The complexity of deciding legality of
a single step of magic: The gathering,” presented at the ECAI: European Conference
on Artificial Intelligence, The Hague, Netherlands, 2016, vol. 285, pp. 1432–1439.'
ista: 'Chatterjee K, Ibsen-Jensen R. 2016. The complexity of deciding legality of
a single step of magic: The gathering. ECAI: European Conference on Artificial
Intelligence, Frontiers in Artificial Intelligence and Applications, vol. 285,
1432–1439.'
mla: 'Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Complexity of Deciding
Legality of a Single Step of Magic: The Gathering. Vol. 285, IOS Press, 2016,
pp. 1432–39, doi:10.3233/978-1-61499-672-9-1432.'
short: K. Chatterjee, R. Ibsen-Jensen, in:, IOS Press, 2016, pp. 1432–1439.
conference:
end_date: 2016-09-02
location: The Hague, Netherlands
name: 'ECAI: European Conference on Artificial Intelligence'
start_date: 2016-08-29
date_created: 2018-12-11T11:46:41Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T08:00:54Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.3233/978-1-61499-672-9-1432
file:
- access_level: open_access
checksum: 848043c812ace05e459579c923f3d3cf
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:07:59Z
date_updated: 2020-07-14T12:46:35Z
file_id: '4658'
file_name: IST-2018-950-v1+1_2016_Chatterjee_The_complexity.pdf
file_size: 2116225
relation: main_file
file_date_updated: 2020-07-14T12:46:35Z
has_accepted_license: '1'
intvolume: ' 285'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc/4.0/
month: '01'
oa: 1
oa_version: Published Version
page: 1432 - 1439
publication_status: published
publisher: IOS Press
publist_id: '7342'
pubrep_id: '950'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'The complexity of deciding legality of a single step of magic: The gathering'
tmp:
image: /images/cc_by_nc.png
legal_code_url: https://creativecommons.org/licenses/by-nc/4.0/legalcode
name: Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)
short: CC BY-NC (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 285
year: '2016'
...
---
_id: '480'
abstract:
- lang: eng
text: Graph games provide the foundation for modeling and synthesizing reactive
processes. In the synthesis of stochastic reactive processes, the traditional
model is perfect-information stochastic games, where some transitions of the game
graph are controlled by two adversarial players, and the other transitions are
executed probabilistically. We consider such games where the objective is the
conjunction of several quantitative objectives (specified as mean-payoff conditions),
which we refer to as generalized mean-payoff objectives. The basic decision problem
asks for the existence of a finite-memory strategy for a player that ensures the
generalized mean-payoff objective be satisfied with a desired probability against
all strategies of the opponent. A special case of the decision problem is the
almost-sure problem where the desired probability is 1. Previous results presented
a semi-decision procedure for -approximations of the almost-sure problem. In this
work, we show that both the almost-sure problem as well as the general basic decision
problem are coNP-complete, significantly improving the previous results. Moreover,
we show that in the case of 1-player stochastic games, randomized memoryless strategies
are sufficient and the problem can be solved in polynomial time. In contrast,
in two-player stochastic games, we show that even with randomized strategies exponential
memory is required in general, and present a matching exponential upper bound.
We also study the basic decision problem with infinite-memory strategies and present
computational complexity results for the problem. Our results are relevant in
the synthesis of stochastic reactive systems with multiple quantitative requirements.
alternative_title:
- Proceedings Symposium on Logic in Computer Science
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
citation:
ama: 'Chatterjee K, Doyen L. Perfect-information stochastic games with generalized
mean-payoff objectives. In: Vol 05-08-July-2016. IEEE; 2016:247-256. doi:10.1145/2933575.2934513'
apa: 'Chatterjee, K., & Doyen, L. (2016). Perfect-information stochastic games
with generalized mean-payoff objectives (Vol. 05-08-July-2016, pp. 247–256). Presented
at the LICS: Logic in Computer Science, New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2934513'
chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Perfect-Information Stochastic
Games with Generalized Mean-Payoff Objectives,” 05-08-July-2016:247–56. IEEE,
2016. https://doi.org/10.1145/2933575.2934513.
ieee: 'K. Chatterjee and L. Doyen, “Perfect-information stochastic games with generalized
mean-payoff objectives,” presented at the LICS: Logic in Computer Science, New
York, NY, USA, 2016, vol. 05-08-July-2016, pp. 247–256.'
ista: 'Chatterjee K, Doyen L. 2016. Perfect-information stochastic games with generalized
mean-payoff objectives. LICS: Logic in Computer Science, Proceedings Symposium
on Logic in Computer Science, vol. 05-08-July-2016, 247–256.'
mla: Chatterjee, Krishnendu, and Laurent Doyen. Perfect-Information Stochastic
Games with Generalized Mean-Payoff Objectives. Vol. 05-08-July-2016, IEEE,
2016, pp. 247–56, doi:10.1145/2933575.2934513.
short: K. Chatterjee, L. Doyen, in:, IEEE, 2016, pp. 247–256.
conference:
end_date: 2016-07-08
location: New York, NY, USA
name: 'LICS: Logic in Computer Science'
start_date: 2016-07-05
date_created: 2018-12-11T11:46:42Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2021-01-12T08:00:56Z
day: '05'
department:
- _id: KrCh
doi: 10.1145/2933575.2934513
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.06376
month: '07'
oa: 1
oa_version: Preprint
page: 247 - 256
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: IEEE
publist_id: '7340'
quality_controlled: '1'
scopus_import: 1
status: public
title: Perfect-information stochastic games with generalized mean-payoff objectives
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 05-08-July-2016
year: '2016'
...
---
_id: '1477'
abstract:
- lang: eng
text: We consider partially observable Markov decision processes (POMDPs) with ω-regular
conditions specified as parity objectives. The class of ω-regular languages provides
a robust specification language to express properties in verification, and parity
objectives are canonical forms to express them. The qualitative analysis problem
given a POMDP and a parity objective asks whether there is a strategy to ensure
that the objective is satisfied with probability 1 (resp. positive probability).
While the qualitative analysis problems are undecidable even for special cases
of parity objectives, we establish decidability (with optimal complexity) for
POMDPs with all parity objectives under finite-memory strategies. We establish
optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative
analysis problems under finite-memory strategies for POMDPs with parity objectives.
We also present a practical approach, where we design heuristics to deal with
the exponential complexity, and have applied our implementation on a number of
POMDP examples.
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Mathieu
full_name: Tracol, Mathieu
id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
last_name: Tracol
citation:
ama: Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable
Markov decision processes with ω-regular objectives. Journal of Computer and
System Sciences. 2016;82(5):878-911. doi:10.1016/j.jcss.2016.02.009
apa: Chatterjee, K., Chmelik, M., & Tracol, M. (2016). What is decidable about
partially observable Markov decision processes with ω-regular objectives. Journal
of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2016.02.009
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable
about Partially Observable Markov Decision Processes with ω-Regular Objectives.”
Journal of Computer and System Sciences. Elsevier, 2016. https://doi.org/10.1016/j.jcss.2016.02.009.
ieee: K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially
observable Markov decision processes with ω-regular objectives,” Journal of
Computer and System Sciences, vol. 82, no. 5. Elsevier, pp. 878–911, 2016.
ista: Chatterjee K, Chmelik M, Tracol M. 2016. What is decidable about partially
observable Markov decision processes with ω-regular objectives. Journal of Computer
and System Sciences. 82(5), 878–911.
mla: Chatterjee, Krishnendu, et al. “What Is Decidable about Partially Observable
Markov Decision Processes with ω-Regular Objectives.” Journal of Computer and
System Sciences, vol. 82, no. 5, Elsevier, 2016, pp. 878–911, doi:10.1016/j.jcss.2016.02.009.
short: K. Chatterjee, M. Chmelik, M. Tracol, Journal of Computer and System Sciences
82 (2016) 878–911.
date_created: 2018-12-11T11:52:15Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-02-23T12:24:38Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.jcss.2016.02.009
ec_funded: 1
external_id:
arxiv:
- '1309.2802'
intvolume: ' 82'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1309.2802
month: '08'
oa: 1
oa_version: Preprint
page: 878 - 911
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: '5718'
quality_controlled: '1'
related_material:
record:
- id: '2295'
relation: earlier_version
status: public
- id: '5400'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: What is decidable about partially observable Markov decision processes with
ω-regular objectives
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 82
year: '2016'
...
---
_id: '1529'
abstract:
- lang: eng
text: 'We consider partially observable Markov decision processes (POMDPs) with
a set of target states and an integer cost associated with every transition. The
optimization objective we study asks to minimize the expected total cost of reaching
a state in the target set, while ensuring that the target set is reached almost
surely (with probability 1). We show that for integer costs approximating the
optimal cost is undecidable. For positive costs, our results are as follows: (i)
we establish matching lower and upper bounds for the optimal cost, both double
exponential in the POMDP state space size; (ii) we show that the problem of approximating
the optimal cost is decidable and present approximation algorithms developing
on the existing algorithms for POMDPs with finite-horizon objectives. While the
worst-case running time of our algorithm is double exponential, we also present
efficient stopping criteria for the algorithm and show experimentally that it
performs well in many examples of interest.'
acknowledgement: 'We thank Blai Bonet for helping us with RTDP-Bel. The research was
partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant
No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty
fellows award.'
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: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Raghav
full_name: Gupta, Raghav
last_name: Gupta
- first_name: Ayush
full_name: Kanodia, Ayush
last_name: Kanodia
citation:
ama: Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability
in POMDPs. Artificial Intelligence. 2016;234:26-48. doi:10.1016/j.artint.2016.01.007
apa: Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2016). Optimal cost
almost-sure reachability in POMDPs. Artificial Intelligence. Elsevier.
https://doi.org/10.1016/j.artint.2016.01.007
chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia.
“Optimal Cost Almost-Sure Reachability in POMDPs.” Artificial Intelligence.
Elsevier, 2016. https://doi.org/10.1016/j.artint.2016.01.007.
ieee: K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure
reachability in POMDPs,” Artificial Intelligence, vol. 234. Elsevier, pp.
26–48, 2016.
ista: Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2016. Optimal cost almost-sure
reachability in POMDPs. Artificial Intelligence. 234, 26–48.
mla: Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.”
Artificial Intelligence, vol. 234, Elsevier, 2016, pp. 26–48, doi:10.1016/j.artint.2016.01.007.
short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Artificial Intelligence
234 (2016) 26–48.
date_created: 2018-12-11T11:52:33Z
date_published: 2016-05-01T00:00:00Z
date_updated: 2023-02-23T12:25:49Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.artint.2016.01.007
ec_funded: 1
external_id:
arxiv:
- '1411.3880'
intvolume: ' 234'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1411.3880
month: '05'
oa: 1
oa_version: Preprint
page: 26 - 48
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: Artificial Intelligence
publication_status: published
publisher: Elsevier
publist_id: '5642'
quality_controlled: '1'
related_material:
record:
- id: '1820'
relation: earlier_version
status: public
- id: '5425'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Optimal cost almost-sure reachability in POMDPs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 234
year: '2016'
...
---
_id: '5445'
abstract:
- lang: eng
text: 'We consider the quantitative analysis problem for interprocedural control-flow
graphs (ICFGs). The input consists of an ICFG, a positive weight function that
assigns every transition a positive integer-valued number, and a labelling of
the transitions (events) as good, bad, and neutral events. The weight function
assigns to each transition a numerical value that represents ameasure of how good
or bad an event is. The quantitative analysis problem asks whether there is a
run of the ICFG where the ratio of the sum of the numerical weights of good events
versus the sum of weights of bad events in the long-run is at least a given threshold
(or equivalently, to compute the maximal ratio among all valid paths in the ICFG).
The quantitative analysis problem for ICFGs can be solved in polynomial time,
and we present an efficient and practical algorithm for the problem. We show that
several problems relevant for static program analysis, such as estimating the
worst-case execution time of a program or the average energy consumption of a
mobile application, can be modeled in our framework. We have implemented our algorithm
as a tool in the Java Soot framework. We demonstrate the effectiveness of our
approach with two case studies. First, we show that our framework provides a sound
approach (no false positives) for the analysis of inefficiently-used containers.
Second, we show that our approach can also be used for static profiling of programs
which reasons about methods that are frequently invoked. Our experimental results
show that our tool scales to relatively large benchmarks, and discovers relevant
and useful information that can be used to optimize performance of the programs. '
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Pavlogiannis A, Velner Y. Quantitative Interprocedural Analysis.
IST Austria; 2016. doi:10.15479/AT:IST-2016-523-v1-1
apa: Chatterjee, K., Pavlogiannis, A., & Velner, Y. (2016). Quantitative
interprocedural analysis. IST Austria. https://doi.org/10.15479/AT:IST-2016-523-v1-1
chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. Quantitative
Interprocedural Analysis. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-523-v1-1.
ieee: K. Chatterjee, A. Pavlogiannis, and Y. Velner, Quantitative interprocedural
analysis. IST Austria, 2016.
ista: Chatterjee K, Pavlogiannis A, Velner Y. 2016. Quantitative interprocedural
analysis, IST Austria, 33p.
mla: Chatterjee, Krishnendu, et al. Quantitative Interprocedural Analysis.
IST Austria, 2016, doi:10.15479/AT:IST-2016-523-v1-1.
short: K. Chatterjee, A. Pavlogiannis, Y. Velner, Quantitative Interprocedural Analysis,
IST Austria, 2016.
date_created: 2018-12-12T11:39:22Z
date_published: 2016-03-31T00:00:00Z
date_updated: 2023-02-23T10:06:22Z
day: '31'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2016-523-v1-1
file:
- access_level: open_access
checksum: cef516fa091925b5868813e355268fb4
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:52Z
date_updated: 2020-07-14T12:46:58Z
file_id: '5513'
file_name: IST-2016-523-v1+1_main.pdf
file_size: 1012204
relation: main_file
file_date_updated: 2020-07-14T12:46:58Z
has_accepted_license: '1'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '523'
related_material:
record:
- id: '1604'
relation: later_version
status: public
status: public
title: Quantitative interprocedural analysis
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1166'
abstract:
- lang: eng
text: POMDPs are standard models for probabilistic planning problems, where an agent
interacts with an uncertain environment. We study the problem of almost-sure reachability,
where given a set of target states, the question is to decide whether there is
a policy to ensure that the target set is reached with probability 1 (almost-surely).
While in general the problem is EXPTIMEcomplete, in many practical cases policies
with a small amount of memory suffice. Moreover, the existing solution to the
problem is explicit, which first requires to construct explicitly an exponential
reduction to a belief-support MDP. In this work, we first study the existence
of observation-stationary strategies, which is NP-complete, and then small-memory
strategies. We present a symbolic algorithm by an efficient encoding to SAT and
using a SAT solver for the problem. We report experimental results demonstrating
the scalability of our symbolic (SAT-based) approach. © 2016, Association for
the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Jessica
full_name: Davies, Jessica
id: 378E0060-F248-11E8-B48F-1D18A9856A87
last_name: Davies
citation:
ama: 'Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost
sure reachability with small strategies in pomdps. In: Proceedings of the Thirtieth
AAAI Conference on Artificial Intelligence. Vol 2016. AAAI Press; 2016:3225-3232.'
apa: 'Chatterjee, K., Chmelik, M., & Davies, J. (2016). A symbolic SAT based
algorithm for almost sure reachability with small strategies in pomdps. In Proceedings
of the Thirtieth AAAI Conference on Artificial Intelligence (Vol. 2016, pp.
3225–3232). Phoenix, AZ, USA: AAAI Press.'
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic
SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.”
In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence,
2016:3225–32. AAAI Press, 2016.
ieee: K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm
for almost sure reachability with small strategies in pomdps,” in Proceedings
of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, AZ,
USA, 2016, vol. 2016, pp. 3225–3232.
ista: 'Chatterjee K, Chmelik M, Davies J. 2016. A symbolic SAT based algorithm for
almost sure reachability with small strategies in pomdps. Proceedings of the Thirtieth
AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence
vol. 2016, 3225–3232.'
mla: Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure
Reachability with Small Strategies in Pomdps.” Proceedings of the Thirtieth
AAAI Conference on Artificial Intelligence, vol. 2016, AAAI Press, 2016, pp.
3225–32.
short: K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI
Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.
conference:
end_date: 2016-02-17
location: Phoenix, AZ, USA
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2016-02-12
date_created: 2018-12-11T11:50:30Z
date_published: 2016-12-02T00:00:00Z
date_updated: 2023-02-23T12:26:41Z
day: '02'
department:
- _id: KrCh
- _id: ToHe
ec_funded: 1
intvolume: ' 2016'
language:
- iso: eng
month: '12'
oa_version: None
page: 3225 - 3232
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 Thirtieth AAAI Conference on Artificial Intelligence
publication_status: published
publisher: AAAI Press
publist_id: '6191'
quality_controlled: '1'
related_material:
link:
- relation: table_of_contents
url: https://dl.acm.org/citation.cfm?id=3016355
record:
- id: '5443'
relation: earlier_version
status: public
status: public
title: A symbolic SAT based algorithm for almost sure reachability with small strategies
in pomdps
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 2016
year: '2016'
...
---
_id: '5449'
abstract:
- lang: eng
text: "The fixation probability is the probability that a new mutant introduced
in a homogeneous population eventually takes over the entire population.\r\nThe
fixation probability is a fundamental quantity of natural selection, and known
to depend on the population structure.\r\nAmplifiers of natural selection are
population structures which increase the fixation probability of advantageous
mutants, as compared to the baseline case of well-mixed populations. In this work
we focus on symmetric population structures represented as undirected graphs.
In the regime of undirected graphs, the strongest amplifier known has been the
Star graph, and the existence of undirected graphs with stronger amplification
properties has remained open for over a decade.\r\nIn this work we present the
Comet and Comet-swarm families of undirected graphs. We show that for a range
of fitness values of the mutants, the Comet and Comet-swarm graphs have fixation
probability strictly larger than the fixation probability of the Star graph, for
fixed population size and at the limit of large populations, respectively."
alternative_title:
- IST Austria Technical Report
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. IST Austria; 2016. doi:10.15479/AT:IST-2016-648-v1-1'
apa: 'Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Amplification
on undirected population structures: Comets beat stars. IST Austria. https://doi.org/10.15479/AT:IST-2016-648-v1-1'
chicago: 'Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. Amplification on Undirected Population Structures: Comets Beat Stars.
IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-648-v1-1.'
ieee: 'A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Amplification
on undirected population structures: Comets beat stars. IST Austria, 2016.'
ista: 'Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Amplification on
undirected population structures: Comets beat stars, IST Austria, 22p.'
mla: 'Pavlogiannis, Andreas, et al. Amplification on Undirected Population Structures:
Comets Beat Stars. IST Austria, 2016, doi:10.15479/AT:IST-2016-648-v1-1.'
short: 'A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Amplification on Undirected
Population Structures: Comets Beat Stars, IST Austria, 2016.'
date_created: 2018-12-12T11:39:24Z
date_published: 2016-11-09T00:00:00Z
date_updated: 2023-02-23T12:22:21Z
day: '09'
ddc:
- '519'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2016-648-v1-1
file:
- access_level: open_access
checksum: 8345a8c1e7d7f0cd92516d182b7fc59e
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:07Z
date_updated: 2020-07-14T12:46:58Z
file_id: '5529'
file_name: IST-2016-648-v1+1_tr.pdf
file_size: 1264221
relation: main_file
file_date_updated: 2020-07-14T12:46:58Z
has_accepted_license: '1'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Updated Version
page: '22'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '648'
related_material:
record:
- id: '512'
relation: later_version
status: public
status: public
title: 'Amplification on undirected population structures: Comets beat stars'
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5453'
alternative_title:
- IST Austria Technical Report
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. Arbitrarily Strong Amplifiers
of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2017-749-v3-1
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Arbitrarily
strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2017-749-v3-1
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria,
2016. https://doi.org/10.15479/AT:IST-2017-749-v3-1.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Arbitrarily strong
amplifiers of natural selection. IST Austria, 2016.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong
amplifiers of natural selection, IST Austria, 34p.
mla: Pavlogiannis, Andreas, et al. Arbitrarily Strong Amplifiers of Natural Selection.
IST Austria, 2016, doi:10.15479/AT:IST-2017-749-v3-1.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong
Amplifiers of Natural Selection, IST Austria, 2016.
date_created: 2018-12-12T11:39:25Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2023-02-23T12:27:07Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-749-v3-1
file:
- access_level: open_access
checksum: 83b0313dab3bff4bdb6ac38695026fda
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:13Z
date_updated: 2020-07-14T12:46:59Z
file_id: '5474'
file_name: IST-2017-749-v3+1_main.pdf
file_size: 1015647
relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '34'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '755'
related_material:
record:
- id: '5452'
relation: earlier_version
status: public
status: public
title: Arbitrarily strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5451'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Strong Amplifiers of Natural
Selection. IST Austria; 2016. doi:10.15479/AT:IST-2016-728-v1-1
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Strong
amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2016-728-v1-1
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-728-v1-1.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Strong amplifiers
of natural selection. IST Austria, 2016.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Strong amplifiers
of natural selection, IST Austria, 34p.
mla: Pavlogiannis, Andreas, et al. Strong Amplifiers of Natural Selection.
IST Austria, 2016, doi:10.15479/AT:IST-2016-728-v1-1.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Strong Amplifiers of
Natural Selection, IST Austria, 2016.
date_created: 2018-12-12T11:39:24Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2023-02-23T12:27:05Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2016-728-v1-1
file:
- access_level: open_access
checksum: 7b8bb17c322c0556acba6ac169fa71c1
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:04Z
date_updated: 2020-07-14T12:46:59Z
file_id: '5465'
file_name: IST-2016-728-v1+1_main.pdf
file_size: 1014732
relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '34'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '728'
status: public
title: Strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '9867'
abstract:
- lang: eng
text: In the beginning of our experiment, subjects were asked to read a few pages
on their computer screens that would explain the rules of the subsequent game.
Here, we provide these instructions, translated from German.
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: Kristin
full_name: Hagel, Kristin
last_name: Hagel
- first_name: Manfred
full_name: Milinski, Manfred
last_name: Milinski
citation:
ama: Hilbe C, Hagel K, Milinski M. Experimental game instructions. 2016. doi:10.1371/journal.pone.0163867.s008
apa: Hilbe, C., Hagel, K., & Milinski, M. (2016). Experimental game instructions.
Public Library of Science. https://doi.org/10.1371/journal.pone.0163867.s008
chicago: Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Experimental Game
Instructions.” Public Library of Science, 2016. https://doi.org/10.1371/journal.pone.0163867.s008.
ieee: C. Hilbe, K. Hagel, and M. Milinski, “Experimental game instructions.” Public
Library of Science, 2016.
ista: Hilbe C, Hagel K, Milinski M. 2016. Experimental game instructions, Public
Library of Science, 10.1371/journal.pone.0163867.s008.
mla: Hilbe, Christian, et al. Experimental Game Instructions. Public Library
of Science, 2016, doi:10.1371/journal.pone.0163867.s008.
short: C. Hilbe, K. Hagel, M. Milinski, (2016).
date_created: 2021-08-10T08:42:00Z
date_updated: 2023-02-21T16:59:01Z
day: '04'
department:
- _id: KrCh
doi: 10.1371/journal.pone.0163867.s008
month: '10'
oa_version: Published Version
publisher: Public Library of Science
related_material:
record:
- id: '1322'
relation: used_in_publication
status: public
status: public
title: Experimental game instructions
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2016'
...
---
_id: '1322'
abstract:
- lang: eng
text: Direct reciprocity is a major mechanism for the evolution of cooperation.
Several classical studies have suggested that humans should quickly learn to adopt
reciprocal strategies to establish mutual cooperation in repeated interactions.
On the other hand, the recently discovered theory of ZD strategies has found that
subjects who use extortionate strategies are able to exploit and subdue cooperators.
Although such extortioners have been predicted to succeed in any population of
adaptive opponents, theoretical follow-up studies questioned whether extortion
can evolve in reality. However, most of these studies presumed that individuals
have similar strategic possibilities and comparable outside options, whereas asymmetries
are ubiquitous in real world applications. Here we show with a model and an economic
experiment that extortionate strategies readily emerge once subjects differ in
their strategic power. Our experiment combines a repeated social dilemma with
asymmetric partner choice. In our main treatment there is one randomly chosen
group member who is unilaterally allowed to exchange one of the other group members
after every ten rounds of the social dilemma. We find that this asymmetric replacement
opportunity generally promotes cooperation, but often the resulting payoff distribution
reflects the underlying power structure. Almost half of the subjects in a better
strategic position turn into extortioners, who quickly proceed to exploit their
peers. By adapting their cooperation probabilities consistent with ZD theory,
extortioners force their co-players to cooperate without being similarly cooperative
themselves. Comparison to non-extortionate players under the same conditions indicates
a substantial net gain to extortion. Our results thus highlight how power asymmetries
can endanger mutually beneficial interactions, and transform them into exploitative
relationships. In particular, our results indicate that the extortionate strategies
predicted from ZD theory could play a more prominent role in our daily interactions
than previously thought.
acknowledgement: 'CH was funded by the Schrödinger program of the Austrian Science
Fund (FWF) J3475. '
article_number: e0163867
author:
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Kristin
full_name: Hagel, Kristin
last_name: Hagel
- first_name: Manfred
full_name: Milinski, Manfred
last_name: Milinski
citation:
ama: Hilbe C, Hagel K, Milinski M. Asymmetric power boosts extortion in an economic
experiment. PLoS One. 2016;11(10). doi:10.1371/journal.pone.0163867
apa: Hilbe, C., Hagel, K., & Milinski, M. (2016). Asymmetric power boosts extortion
in an economic experiment. PLoS One. Public Library of Science. https://doi.org/10.1371/journal.pone.0163867
chicago: Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Asymmetric Power
Boosts Extortion in an Economic Experiment.” PLoS One. Public Library of
Science, 2016. https://doi.org/10.1371/journal.pone.0163867.
ieee: C. Hilbe, K. Hagel, and M. Milinski, “Asymmetric power boosts extortion in
an economic experiment,” PLoS One, vol. 11, no. 10. Public Library of Science,
2016.
ista: Hilbe C, Hagel K, Milinski M. 2016. Asymmetric power boosts extortion in an
economic experiment. PLoS One. 11(10), e0163867.
mla: Hilbe, Christian, et al. “Asymmetric Power Boosts Extortion in an Economic
Experiment.” PLoS One, vol. 11, no. 10, e0163867, Public Library of Science,
2016, doi:10.1371/journal.pone.0163867.
short: C. Hilbe, K. Hagel, M. Milinski, PLoS One 11 (2016).
date_created: 2018-12-11T11:51:22Z
date_published: 2016-10-04T00:00:00Z
date_updated: 2023-02-23T14:11:27Z
day: '04'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.1371/journal.pone.0163867
file:
- access_level: open_access
checksum: 6b33e394003dfe8b4ca6be1858aaa8e3
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:08Z
date_updated: 2020-07-14T12:44:44Z
file_id: '4668'
file_name: IST-2016-716-v1+1_journal.pone.0163867.PDF
file_size: 2077905
relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: ' 11'
issue: '10'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
publication: PLoS One
publication_status: published
publisher: Public Library of Science
publist_id: '5948'
pubrep_id: '716'
quality_controlled: '1'
related_material:
record:
- id: '9867'
relation: research_data
status: public
- id: '9868'
relation: research_data
status: public
scopus_import: 1
status: public
title: Asymmetric power boosts extortion in an economic experiment
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 11
year: '2016'
...
---
_id: '9868'
abstract:
- lang: eng
text: The raw data file containing the experimental decisions of all our study subjects.
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: Kristin
full_name: Hagel, Kristin
last_name: Hagel
- first_name: Manfred
full_name: Milinski, Manfred
last_name: Milinski
citation:
ama: Hilbe C, Hagel K, Milinski M. Experimental data. 2016. doi:10.1371/journal.pone.0163867.s009
apa: Hilbe, C., Hagel, K., & Milinski, M. (2016). Experimental data. Public
Library of Science. https://doi.org/10.1371/journal.pone.0163867.s009
chicago: Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Experimental Data.”
Public Library of Science, 2016. https://doi.org/10.1371/journal.pone.0163867.s009.
ieee: C. Hilbe, K. Hagel, and M. Milinski, “Experimental data.” Public Library of
Science, 2016.
ista: Hilbe C, Hagel K, Milinski M. 2016. Experimental data, Public Library of Science,
10.1371/journal.pone.0163867.s009.
mla: Hilbe, Christian, et al. Experimental Data. Public Library of Science,
2016, doi:10.1371/journal.pone.0163867.s009.
short: C. Hilbe, K. Hagel, M. Milinski, (2016).
date_created: 2021-08-10T08:45:00Z
date_published: 2016-10-04T00:00:00Z
date_updated: 2023-02-21T16:59:01Z
day: '04'
department:
- _id: KrCh
doi: 10.1371/journal.pone.0163867.s009
month: '10'
oa_version: Published Version
publisher: Public Library of Science
related_material:
record:
- id: '1322'
relation: used_in_publication
status: public
status: public
title: Experimental data
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2016'
...
---
_id: '1397'
abstract:
- lang: eng
text: 'We study partially observable Markov decision processes (POMDPs) with objectives
used in verification and artificial intelligence. The qualitative analysis problem
given a POMDP and an objective asks whether there is a strategy (policy) to ensure
that the objective is satisfied almost surely (with probability 1), resp. with
positive probability (with probability greater than 0). For POMDPs with limit-average
payoff, where a reward value in the interval [0,1] is associated to every transition,
and the payoff of an infinite path is the long-run average of the rewards, we
consider two types of path constraints: (i) a quantitative limit-average constraint
defines the set of paths where the payoff is at least a given threshold L1 = 1.
Our main results for qualitative limit-average constraint under almost-sure winning
are as follows: (i) the problem of deciding the existence of a finite-memory controller
is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory
controller is undecidable. For quantitative limit-average constraints we show
that the problem of deciding the existence of a finite-memory controller is undecidable.
We present a prototype implementation of our EXPTIME algorithm. For POMDPs with
w-regular conditions specified as parity objectives, while the qualitative analysis
problems are known to be undecidable even for very special case of parity objectives,
we establish decidability (with optimal complexity) of the qualitative analysis
problems for POMDPs with parity objectives under finite-memory strategies. We
establish optimal (exponential) memory bounds and EXPTIME-completeness of the
qualitative analysis problems under finite-memory strategies for POMDPs with parity
objectives. Based on our theoretical algorithms we also present a practical approach,
where we design heuristics to deal with the exponential complexity, and have applied
our implementation on a number of well-known POMDP examples for robotics applications.
For POMDPs with a set of target states and an integer cost associated with every
transition, we study the optimization objective that asks to minimize the expected
total cost of reaching a state in the target set, while ensuring that the target
set is reached almost surely. We show that for general integer costs approximating
the optimal cost is undecidable. For positive costs, our results are as follows:
(i) we establish matching lower and upper bounds for the optimal cost, both double
and exponential in the POMDP state space size; (ii) we show that the problem of
approximating the optimal cost is decidable and present approximation algorithms
that extend existing algorithms for POMDPs with finite-horizon objectives. We
show experimentally that it performs well in many examples of interest. We study
more deeply the problem of almost-sure reachability, where given a set of target
states, the question is to decide whether there is a strategy to ensure that the
target set is reached almost surely. While in general the problem EXPTIME-complete,
in many practical cases strategies with a small amount of memory suffice. Moreover,
the existing solution to the problem is explicit, which first requires to construct
explicitly an exponential reduction to a belief-support MDP. We first study the
existence of observation-stationary strategies, which is NP-complete, and then
small-memory strategies. We present a symbolic algorithm by an efficient encoding
to SAT and using a SAT solver for the problem. We report experimental results
demonstrating the scalability of our symbolic (SAT-based) approach. Decentralized
POMDPs (DEC-POMDPs) extend POMDPs to a multi-agent setting, where several agents
operate in an uncertain environment independently to achieve a joint objective.
In this work we consider Goal DEC-POMDPs, where given a set of target states,
the objective is to ensure that the target set is reached with minimal cost. We
consider the indefinite-horizon (infinite-horizon with either discounted-sum,
or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present
a new and novel method to solve the problem that extends methods for finite-horizon
DEC-POMDPs and the real-time dynamic programming approach for POMDPs. We present
experimental results on several examples, and show that our approach presents
promising results. In the end we present a short summary of a few other results
related to verification of MDPs and POMDPs.'
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: Chmelik M. Algorithms for partially observable markov decision processes. 2016.
apa: Chmelik, M. (2016). Algorithms for partially observable markov decision
processes. Institute of Science and Technology Austria.
chicago: Chmelik, Martin. “Algorithms for Partially Observable Markov Decision Processes.”
Institute of Science and Technology Austria, 2016.
ieee: M. Chmelik, “Algorithms for partially observable markov decision processes,”
Institute of Science and Technology Austria, 2016.
ista: Chmelik M. 2016. Algorithms for partially observable markov decision processes.
Institute of Science and Technology Austria.
mla: Chmelik, Martin. Algorithms for Partially Observable Markov Decision Processes.
Institute of Science and Technology Austria, 2016.
short: M. Chmelik, Algorithms for Partially Observable Markov Decision Processes,
Institute of Science and Technology Austria, 2016.
date_created: 2018-12-11T11:51:47Z
date_published: 2016-02-01T00:00:00Z
date_updated: 2023-09-07T11:54:58Z
day: '01'
degree_awarded: PhD
department:
- _id: KrCh
language:
- iso: eng
month: '02'
oa_version: None
page: '232'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5810'
status: public
supervisor:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
title: Algorithms for partially observable markov decision processes
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2016'
...
---
_id: '1093'
abstract:
- lang: eng
text: 'We introduce a general class of distances (metrics) between Markov chains,
which are based on linear behaviour. This class encompasses distances given topologically
(such as the total variation distance or trace distance) as well as by temporal
logics or automata. We investigate which of the distances can be approximated
by observing the systems, i.e. by black-box testing or simulation, and we provide
both negative and positive results. '
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF)
under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award),
by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced
Postdoc. Mobility Fellowship – grant number P300P2_161067."
alternative_title:
- LIPIcs
article_number: '20'
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov
chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.20'
apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Linear
distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency
Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.CONCUR.2016.20'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20.
ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances
between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City;
Canada, 2016, vol. 59.'
ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between
Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.'
mla: Daca, Przemyslaw, et al. Linear Distances between Markov Chains. Vol.
59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.20.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Quebec City; Canada
name: 'CONCUR: Concurrency Theory'
start_date: 2016-08-23
date_created: 2018-12-11T11:50:06Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
- _id: KrCh
- _id: CaGu
doi: 10.4230/LIPIcs.CONCUR.2016.20
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:39Z
date_updated: 2018-12-12T10:11:39Z
file_id: '4895'
file_name: IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf
file_size: 501827
relation: main_file
file_date_updated: 2018-12-12T10:11:39Z
has_accepted_license: '1'
intvolume: ' 59'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6283'
pubrep_id: '794'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Linear distances between Markov chains
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1071'
abstract:
- lang: eng
text: 'We consider data-structures for answering reachability and distance queries
on constant-treewidth graphs with n nodes, on the standard RAM computational model
with wordsize W=Theta(log n). Our first contribution is a data-structure that
after O(n) preprocessing time, allows (1) pair reachability queries in O(1) time;
and (2) single-source reachability queries in O(n/log n) time. This is (asymptotically)
optimal and is faster than DFS/BFS when answering more than a constant number
of single-source queries. The data-structure uses at all times O(n) space. Our
second contribution is a space-time tradeoff data-structure for distance queries.
For any epsilon in [1/2,1], we provide a data-structure with polynomial preprocessing
time that allows pair queries in O(n^{1-\epsilon} alpha(n)) time, where alpha
is the inverse of the Ackermann function, and at all times uses O(n^epsilon) space.
The input graph G is not considered in the space complexity. '
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).'
alternative_title:
- LIPIcs
article_number: '28'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 'Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Optimal reachability and a space
time tradeoff for distance queries in constant treewidth graphs. In: Vol 57. Schloss
Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:10.4230/LIPIcs.ESA.2016.28'
apa: 'Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2016). Optimal reachability
and a space time tradeoff for distance queries in constant treewidth graphs (Vol.
57). Presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark:
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. https://doi.org/10.4230/LIPIcs.ESA.2016.28'
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
“Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant
Treewidth Graphs,” Vol. 57. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016. https://doi.org/10.4230/LIPIcs.ESA.2016.28.
ieee: 'K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal reachability
and a space time tradeoff for distance queries in constant treewidth graphs,”
presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark, 2016,
vol. 57.'
ista: 'Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2016. Optimal reachability
and a space time tradeoff for distance queries in constant treewidth graphs. ESA:
European Symposium on Algorithms, LIPIcs, vol. 57, 28.'
mla: Chatterjee, Krishnendu, et al. Optimal Reachability and a Space Time Tradeoff
for Distance Queries in Constant Treewidth Graphs. Vol. 57, 28, Schloss Dagstuhl-
Leibniz-Zentrum fur Informatik, 2016, doi:10.4230/LIPIcs.ESA.2016.28.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Schloss Dagstuhl- Leibniz-Zentrum
fur Informatik, 2016.
conference:
end_date: 2016-08-24
location: Aarhus, Denmark
name: 'ESA: European Symposium on Algorithms'
start_date: 2016-08-22
date_created: 2018-12-11T11:49:59Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-09-07T12:01:58Z
day: '01'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ESA.2016.28
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:31Z
date_updated: 2018-12-12T10:14:31Z
file_id: '5084'
file_name: IST-2017-777-v1+1_LIPIcs-ESA-2016-28.pdf
file_size: 579225
relation: main_file
file_date_updated: 2018-12-12T10:14:31Z
has_accepted_license: '1'
intvolume: ' 57'
language:
- iso: eng
month: '08'
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_status: published
publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik
publist_id: '6312'
pubrep_id: '777'
quality_controlled: '1'
related_material:
record:
- id: '821'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Optimal reachability and a space time tradeoff for distance queries in constant
treewidth 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: 57
year: '2016'
...
---
_id: '1438'
abstract:
- lang: eng
text: 'In this paper, we consider termination of probabilistic programs with real-valued
variables. The questions concerned are: (a) 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); (b) quantitative
ones that ask (i) to approximate the expected termination time (expectation problem)
and (ii) to compute a bound B such that the probability to terminate after B steps
decreases exponentially (concentration problem). To solve these questions, we
utilize the notion of ranking supermartingales which is a powerful approach for
proving termination of probabilistic programs. In detail, we focus on algorithmic
synthesis of linear ranking-supermartingales over affine probabilistic programs
(APP''s) with both angelic and demonic non-determinism. An important subclass
of APP''s is LRAPP which is defined as the class of all APP''s over which a linear
ranking-supermartingale exists. Our main contributions are as follows. Firstly,
we show that the membership problem of LRAPP (i) can be decided in polynomial
time for APP''s with at most demonic non-determinism, and (ii) is NP-hard and
in PSPACE for APP''s with angelic non-determinism; moreover, the NP-hardness result
holds already for APP''s without probability and demonic non-determinism. Secondly,
we show that the concentration problem over LRAPP can be solved in the same complexity
as for the membership problem of LRAPP. Finally, we show that the expectation
problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP''s
without probability and non-determinism (i.e., deterministic programs). Our experimental
results demonstrate the effectiveness of our approach to answer the qualitative
and quantitative questions over APP''s with at most demonic non-determinism.'
acknowledgement: 'Supported by the Natural Science Foundation of China (NSFC) under
Grant No. 61532019 '
alternative_title:
- POPL
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: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- 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. In: Vol
20-22. ACM; 2016:327-342. doi:10.1145/2837614.2837639'
apa: 'Chatterjee, K., Fu, H., Novotný, P., & Hasheminezhad, R. (2016). Algorithmic
analysis of qualitative and quantitative termination problems for affine probabilistic
programs (Vol. 20–22, pp. 327–342). Presented at the POPL: Principles of Programming
Languages, St. Petersburg, FL, USA: ACM. https://doi.org/10.1145/2837614.2837639'
chicago: Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad.
“Algorithmic Analysis of Qualitative and Quantitative Termination Problems for
Affine Probabilistic Programs,” 20–22:327–42. ACM, 2016. https://doi.org/10.1145/2837614.2837639.
ieee: 'K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic
programs,” presented at the POPL: Principles of Programming Languages, St. Petersburg,
FL, USA, 2016, vol. 20–22, pp. 327–342.'
ista: 'Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2016. Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic
programs. POPL: Principles of Programming Languages, POPL, vol. 20–22, 327–342.'
mla: Chatterjee, Krishnendu, et al. Algorithmic Analysis of Qualitative and Quantitative
Termination Problems for Affine Probabilistic Programs. Vol. 20–22, ACM, 2016,
pp. 327–42, doi:10.1145/2837614.2837639.
short: K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, in:, ACM, 2016, pp. 327–342.
conference:
end_date: 2016-01-22
location: St. Petersburg, FL, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2016-01-20
date_created: 2018-12-11T11:52:01Z
date_published: 2016-01-11T00:00:00Z
date_updated: 2023-09-19T14:38:41Z
day: '11'
department:
- _id: KrCh
doi: 10.1145/2837614.2837639
ec_funded: 1
external_id:
arxiv:
- '1510.08517'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1510.08517
month: '01'
oa: 1
oa_version: Preprint
page: 327 - 342
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_status: published
publisher: ACM
publist_id: '5760'
quality_controlled: '1'
related_material:
record:
- id: '5993'
relation: later_version
status: public
scopus_import: 1
status: public
title: Algorithmic analysis of qualitative and quantitative termination problems for
affine probabilistic programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 20-22
year: '2016'
...
---
_id: '5452'
alternative_title:
- IST Austria Technical Report
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. Arbitrarily Strong Amplifiers
of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2017-728-v2-1
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Arbitrarily
strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2017-728-v2-1
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria,
2016. https://doi.org/10.15479/AT:IST-2017-728-v2-1.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Arbitrarily strong
amplifiers of natural selection. IST Austria, 2016.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong
amplifiers of natural selection, IST Austria, 32p.
mla: Pavlogiannis, Andreas, et al. Arbitrarily Strong Amplifiers of Natural Selection.
IST Austria, 2016, doi:10.15479/AT:IST-2017-728-v2-1.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong
Amplifiers of Natural Selection, IST Austria, 2016.
date_created: 2018-12-12T11:39:25Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2024-02-21T13:48:42Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-728-v2-1
ec_funded: 1
file:
- access_level: open_access
checksum: 58e895f26c82f560c0f0989bf8b08599
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:52:59Z
date_updated: 2020-07-14T12:46:59Z
file_id: '5460'
file_name: IST-2017-728-v2+1_main.pdf
file_size: 811558
relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '32'
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '750'
related_material:
record:
- id: '5453'
relation: later_version
status: public
- id: '5559'
relation: popular_science
status: public
status: public
title: Arbitrarily strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1437'
abstract:
- lang: eng
text: We study algorithmic questions for concurrent systems where the transitions
are labeled from a complete, closed semiring, and path properties are algebraic
with semiring operations. The algebraic path properties can model dataflow analysis
problems, the shortest path problem, and many other natural 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. Our 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.
alternative_title:
- POPL
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: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 'Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Algorithms for
algebraic path properties in concurrent systems of constant treewidth components.
In: Vol 20-22. ACM; 2016:733-747. doi:10.1145/2837614.2837624'
apa: 'Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Pavlogiannis, A.
(2016). Algorithms for algebraic path properties in concurrent systems of constant
treewidth components (Vol. 20–22, pp. 733–747). Presented at the POPL: Principles
of Programming Languages, St. Petersburg, FL, USA: ACM. https://doi.org/10.1145/2837614.2837624'
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen,
and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent
Systems of Constant Treewidth Components,” 20–22:733–47. ACM, 2016. https://doi.org/10.1145/2837614.2837624.
ieee: 'K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Algorithms
for algebraic path properties in concurrent systems of constant treewidth components,”
presented at the POPL: Principles of Programming Languages, St. Petersburg, FL,
USA, 2016, vol. 20–22, pp. 733–747.'
ista: 'Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2016. Algorithms
for algebraic path properties in concurrent systems of constant treewidth components.
POPL: Principles of Programming Languages, POPL, vol. 20–22, 733–747.'
mla: Chatterjee, Krishnendu, et al. Algorithms for Algebraic Path Properties
in Concurrent Systems of Constant Treewidth Components. Vol. 20–22, ACM, 2016,
pp. 733–47, doi:10.1145/2837614.2837624.
short: K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, ACM,
2016, pp. 733–747.
conference:
end_date: 2016-01-22
location: St. Petersburg, FL, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2016-01-20
date_created: 2018-12-11T11:52:01Z
date_published: 2016-01-11T00:00:00Z
date_updated: 2024-03-27T23:30:32Z
day: '11'
department:
- _id: KrCh
doi: 10.1145/2837614.2837624
ec_funded: 1
external_id:
arxiv:
- '1510.07565'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1510.07565
month: '01'
oa: 1
oa_version: Preprint
page: 733 - 747
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_status: published
publisher: ACM
publist_id: '5761'
quality_controlled: '1'
related_material:
record:
- id: '5441'
relation: earlier_version
status: public
- id: '5442'
relation: earlier_version
status: public
- id: '821'
relation: dissertation_contains
status: public
- id: '6009'
relation: later_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: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 20-22
year: '2016'
...
---
_id: '1386'
abstract:
- lang: eng
text: We consider nondeterministic probabilistic programs with the most basic liveness
property of termination. We present efficient methods for termination analysis
of nondeterministic probabilistic programs with polynomial guards and assignments.
Our approach is through synthesis of polynomial ranking supermartingales, that
on one hand significantly generalizes linear ranking supermartingales and on the
other hand is a counterpart of polynomial ranking-functions for proving termination
of nonprobabilistic programs. The approach synthesizes polynomial ranking-supermartingales
through Positivstellensatz's, yielding an efficient method which is not only sound,
but also semi-complete over a large subclass of programs. We show experimental
results to demonstrate that our approach can handle several classical programs
with complex polynomial guards and assignments, and can synthesize efficient quadratic
ranking-supermartingales when a linear one does not exist even for simple affine
programs.
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
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
citation:
ama: 'Chatterjee K, Fu H, Goharshady AK. Termination analysis of probabilistic programs
through Positivstellensatz’s. In: Vol 9779. Springer; 2016:3-22. doi:10.1007/978-3-319-41528-4_1'
apa: 'Chatterjee, K., Fu, H., & Goharshady, A. K. (2016). Termination analysis
of probabilistic programs through Positivstellensatz’s (Vol. 9779, pp. 3–22).
Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer.
https://doi.org/10.1007/978-3-319-41528-4_1'
chicago: Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Termination
Analysis of Probabilistic Programs through Positivstellensatz’s,” 9779:3–22. Springer,
2016. https://doi.org/10.1007/978-3-319-41528-4_1.
ieee: 'K. Chatterjee, H. Fu, and A. K. Goharshady, “Termination analysis of probabilistic
programs through Positivstellensatz’s,” presented at the CAV: Computer Aided Verification,
Toronto, Canada, 2016, vol. 9779, pp. 3–22.'
ista: 'Chatterjee K, Fu H, Goharshady AK. 2016. Termination analysis of probabilistic
programs through Positivstellensatz’s. CAV: Computer Aided Verification, LNCS,
vol. 9779, 3–22.'
mla: Chatterjee, Krishnendu, et al. Termination Analysis of Probabilistic Programs
through Positivstellensatz’s. Vol. 9779, Springer, 2016, pp. 3–22, doi:10.1007/978-3-319-41528-4_1.
short: K. Chatterjee, H. Fu, A.K. Goharshady, in:, Springer, 2016, pp. 3–22.
conference:
end_date: 2016-07-23
location: Toronto, Canada
name: 'CAV: Computer Aided Verification'
start_date: 2016-07-17
date_created: 2018-12-11T11:51:43Z
date_published: 2016-07-01T00:00:00Z
date_updated: 2024-03-27T23:30:32Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-319-41528-4_1
ec_funded: 1
intvolume: ' 9779'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1604.07169
month: '07'
oa: 1
oa_version: Preprint
page: 3 - 22
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '5824'
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Termination analysis of probabilistic programs through Positivstellensatz's
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9779
year: '2016'
...
---
_id: '10796'
abstract:
- lang: eng
text: 'We consider concurrent mean-payoff games, a very well-studied class of two-player
(player 1 vs player 2) zero-sum games on finite-state graphs where every transition
is assigned a reward between 0 and 1, and the payoff function is the long-run
average of the rewards. The value is the maximal expected payoff that player 1
can guarantee against all strategies of player 2. We consider the computation
of the set of states with value 1 under finite-memory strategies for player 1,
and our main results for the problem are as follows: (1) we present a polynomial-time
algorithm; (2) we show that whenever there is a finite-memory strategy, there
is a stationary strategy that does not need memory at all; and (3) we present
an optimal bound (which is double exponential) on the patience of stationary strategies
(where patience of a distribution is the inverse of the smallest positive probability
and represents a complexity measure of a stationary strategy).'
acknowledgement: "The research was partly supported by FWF Grant No P 23499-N23, FWF
NFN Grant\r\nNo S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft
faculty fellows award."
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
citation:
ama: 'Chatterjee K, Ibsen-Jensen R. The value 1 problem under finite-memory strategies
for concurrent mean-payoff games. In: Proceedings of the Twenty-Sixth Annual
ACM-SIAM Symposium on Discrete Algorithms. Vol 2015. SIAM; 2015:1018-1029.
doi:10.1137/1.9781611973730.69'
apa: 'Chatterjee, K., & Ibsen-Jensen, R. (2015). The value 1 problem under finite-memory
strategies for concurrent mean-payoff games. In Proceedings of the Twenty-Sixth
Annual ACM-SIAM Symposium on Discrete Algorithms (Vol. 2015, pp. 1018–1029).
San Diego, CA, United States: SIAM. https://doi.org/10.1137/1.9781611973730.69'
chicago: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Value 1 Problem under
Finite-Memory Strategies for Concurrent Mean-Payoff Games.” In Proceedings
of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, 2015:1018–29.
SIAM, 2015. https://doi.org/10.1137/1.9781611973730.69.
ieee: K. Chatterjee and R. Ibsen-Jensen, “The value 1 problem under finite-memory
strategies for concurrent mean-payoff games,” in Proceedings of the Twenty-Sixth
Annual ACM-SIAM Symposium on Discrete Algorithms, San Diego, CA, United States,
2015, vol. 2015, no. 1, pp. 1018–1029.
ista: 'Chatterjee K, Ibsen-Jensen R. 2015. The value 1 problem under finite-memory
strategies for concurrent mean-payoff games. Proceedings of the Twenty-Sixth Annual
ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms
vol. 2015, 1018–1029.'
mla: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Value 1 Problem under
Finite-Memory Strategies for Concurrent Mean-Payoff Games.” Proceedings of
the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, vol. 2015,
no. 1, SIAM, 2015, pp. 1018–29, doi:10.1137/1.9781611973730.69.
short: K. Chatterjee, R. Ibsen-Jensen, in:, Proceedings of the Twenty-Sixth Annual
ACM-SIAM Symposium on Discrete Algorithms, SIAM, 2015, pp. 1018–1029.
conference:
end_date: 2015-01-06
location: San Diego, CA, United States
name: 'SODA: Symposium on Discrete Algorithms'
start_date: 2015-01-04
date_created: 2022-02-25T12:18:43Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2022-02-25T12:33:32Z
day: '01'
department:
- _id: KrCh
doi: 10.1137/1.9781611973730.69
ec_funded: 1
external_id:
arxiv:
- '1409.6690'
intvolume: ' 2015'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: Preprint
page: 1018-1029
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: Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete
Algorithms
publication_identifier:
isbn:
- 978-161197374-7
publication_status: published
publisher: SIAM
quality_controlled: '1'
scopus_import: '1'
status: public
title: The value 1 problem under finite-memory strategies for concurrent mean-payoff
games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2015
year: '2015'
...
---
_id: '1499'
abstract:
- lang: eng
text: "We consider weighted automata with both positive and negative integer weights
on edges and\r\nstudy the problem of synchronization using adaptive strategies
that may only observe whether\r\nthe current weight-level is negative or nonnegative.
We show that the synchronization problem is decidable in polynomial time for deterministic
weighted automata."
acknowledgement: "The research leading to these results has received funding from
the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement
601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center
IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM),
the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein
Award), the Czech Science Foundation under grant agreement P202/12/G061, and People
Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme
(FP7/2007-2013) REA Grant No 291734."
alternative_title:
- LIPIcs
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Kim
full_name: Larsen, Kim
last_name: Larsen
- first_name: Simon
full_name: Laursen, Simon
last_name: Laursen
- first_name: Jiří
full_name: Srba, Jiří
last_name: Srba
citation:
ama: 'Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of
weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2015:142-154. doi:10.4230/LIPIcs.CONCUR.2015.142'
apa: 'Kretinsky, J., Larsen, K., Laursen, S., & Srba, J. (2015). Polynomial
time decidability of weighted synchronization under partial observability (Vol.
42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142'
chicago: Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time
Decidability of Weighted Synchronization under Partial Observability,” 42:142–54.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142.
ieee: 'J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability
of weighted synchronization under partial observability,” presented at the CONCUR:
Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.'
ista: 'Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability
of weighted synchronization under partial observability. CONCUR: Concurrency Theory,
LIPIcs, vol. 42, 142–154.'
mla: Kretinsky, Jan, et al. Polynomial Time Decidability of Weighted Synchronization
under Partial Observability. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2015, pp. 142–54, doi:10.4230/LIPIcs.CONCUR.2015.142.
short: J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2015, pp. 142–154.
conference:
end_date: 2015-09-04
location: Madrid, Spain
name: 'CONCUR: Concurrency Theory'
start_date: 2015-09-01
date_created: 2018-12-11T11:52:22Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2021-01-12T06:51:10Z
day: '01'
ddc:
- '000'
- '003'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2015.142
ec_funded: 1
file:
- access_level: open_access
checksum: 49eb5021caafaabe5356c65b9c5f8c9c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:12Z
date_updated: 2020-07-14T12:44:58Z
file_id: '4672'
file_name: IST-2016-498-v1+1_32.pdf
file_size: 623563
relation: main_file
file_date_updated: 2020-07-14T12:44:58Z
has_accepted_license: '1'
intvolume: ' 42'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 142 - 154
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5680'
pubrep_id: '498'
quality_controlled: '1'
scopus_import: 1
status: public
title: Polynomial time decidability of weighted synchronization under partial observability
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: 42
year: '2015'
...
---
_id: '1559'
abstract:
- lang: eng
text: 'There are deep, yet largely unexplored, connections between computer science
and biology. Both disciplines examine how information proliferates in time and
space. Central results in computer science describe the complexity of algorithms
that solve certain classes of problems. An algorithm is deemed efficient if it
can solve a problem in polynomial time, which means the running time of the algorithm
is a polynomial function of the length of the input. There are classes of harder
problems for which the fastest possible algorithm requires exponential time. Another
criterion is the space requirement of the algorithm. There is a crucial distinction
between algorithms that can find a solution, verify a solution, or list several
distinct solutions in given time and space. The complexity hierarchy that is generated
in this way is the foundation of theoretical computer science. Precise complexity
results can be notoriously difficult. The famous question whether polynomial time
equals nondeterministic polynomial time (i.e., P = NP) is one of the hardest open
problems in computer science and all of mathematics. Here, we consider simple
processes of ecological and evolutionary spatial dynamics. The basic question
is: What is the probability that a new invader (or a new mutant)will take over
a resident population?We derive precise complexity results for a variety of scenarios.
We therefore show that some fundamental questions in this area cannot be answered
by simple equations (assuming that P is not equal to NP).'
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: 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, Chatterjee K, Nowak M. Computational complexity of ecological
and evolutionary spatial dynamics. PNAS. 2015;112(51):15636-15641. doi:10.1073/pnas.1511366112
apa: Ibsen-Jensen, R., Chatterjee, K., & Nowak, M. (2015). Computational complexity
of ecological and evolutionary spatial dynamics. PNAS. National Academy
of Sciences. https://doi.org/10.1073/pnas.1511366112
chicago: Ibsen-Jensen, Rasmus, Krishnendu Chatterjee, and Martin Nowak. “Computational
Complexity of Ecological and Evolutionary Spatial Dynamics.” PNAS. National
Academy of Sciences, 2015. https://doi.org/10.1073/pnas.1511366112.
ieee: R. Ibsen-Jensen, K. Chatterjee, and M. Nowak, “Computational complexity of
ecological and evolutionary spatial dynamics,” PNAS, vol. 112, no. 51.
National Academy of Sciences, pp. 15636–15641, 2015.
ista: Ibsen-Jensen R, Chatterjee K, Nowak M. 2015. Computational complexity of ecological
and evolutionary spatial dynamics. PNAS. 112(51), 15636–15641.
mla: Ibsen-Jensen, Rasmus, et al. “Computational Complexity of Ecological and Evolutionary
Spatial Dynamics.” PNAS, vol. 112, no. 51, National Academy of Sciences,
2015, pp. 15636–41, doi:10.1073/pnas.1511366112.
short: R. Ibsen-Jensen, K. Chatterjee, M. Nowak, PNAS 112 (2015) 15636–15641.
date_created: 2018-12-11T11:52:43Z
date_published: 2015-12-22T00:00:00Z
date_updated: 2021-01-12T06:51:36Z
day: '22'
department:
- _id: KrCh
doi: 10.1073/pnas.1511366112
external_id:
pmid:
- '26644569'
intvolume: ' 112'
issue: '51'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4697423/
month: '12'
oa: 1
oa_version: Submitted Version
page: 15636 - 15641
pmid: 1
publication: PNAS
publication_status: published
publisher: National Academy of Sciences
publist_id: '5612'
quality_controlled: '1'
scopus_import: 1
status: public
title: Computational complexity of ecological and evolutionary spatial dynamics
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 112
year: '2015'
...
---
_id: '1594'
abstract:
- lang: eng
text: Quantitative extensions of temporal logics have recently attracted significant
attention. In this work, we study frequency LTL (fLTL), an extension of LTL which
allows to speak about frequencies of events along an execution. Such an extension
is particularly useful for probabilistic systems that often cannot fulfil strict
qualitative guarantees on the behaviour. It has been recently shown that controller
synthesis for Markov decision processes and fLTL is decidable when all the bounds
on frequencies are 1. As a step towards a complete quantitative solution, we show
that the problem is decidable for the fragment fLTL\GU, where U does not occur
in the scope of G (but still F can). Our solution is based on a novel translation
of such quantitative formulae into equivalent deterministic automata.
acknowledgement: "This work is partly supported by the German Research Council (DFG)
as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by
the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework
Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the
CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative
Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie
Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013)
REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE),
and by the ERC Start Grant (279307: Graph Games).\r\n"
alternative_title:
- LNCS
author:
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Jan
full_name: Krčál, Jan
last_name: Krčál
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: 'Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency
LTL\GU. In: Vol 9450. Springer; 2015:162-177. doi:10.1007/978-3-662-48899-7_12'
apa: 'Forejt, V., Krčál, J., & Kretinsky, J. (2015). Controller synthesis for
MDPs and frequency LTL\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic
for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer.
https://doi.org/10.1007/978-3-662-48899-7_12'
chicago: Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for
MDPs and Frequency LTL\GU,” 9450:162–77. Springer, 2015. https://doi.org/10.1007/978-3-662-48899-7_12.
ieee: 'V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and
frequency LTL\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence,
and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.'
ista: 'Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency
LTL\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS,
vol. 9450, 162–177.'
mla: Forejt, Vojtěch, et al. Controller Synthesis for MDPs and Frequency LTL\GU.
Vol. 9450, Springer, 2015, pp. 162–77, doi:10.1007/978-3-662-48899-7_12.
short: V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.
conference:
end_date: 2015-11-28
location: Suva, Fiji
name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
start_date: 2015-11-24
date_created: 2018-12-11T11:52:55Z
date_published: 2015-11-22T00:00:00Z
date_updated: 2021-01-12T06:51:50Z
day: '22'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-662-48899-7_12
ec_funded: 1
intvolume: ' 9450'
language:
- iso: eng
month: '11'
oa_version: None
page: 162 - 177
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _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: '5577'
quality_controlled: '1'
scopus_import: 1
status: public
title: Controller synthesis for MDPs and frequency LTL\GU
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9450
year: '2015'
...
---
_id: '1601'
abstract:
- lang: eng
text: We propose a flexible exchange format for ω-automata, as typically used in
formal verification, and implement support for it in a range of established tools.
Our aim is to simplify the interaction of tools, helping the research community
to build upon other people’s work. A key feature of the format is the use of very
generic acceptance conditions, specified by Boolean combinations of acceptance
primitives, rather than being limited to common cases such as Büchi, Streett,
or Rabin. Such flexibility in the choice of acceptance conditions can be exploited
in applications, for example in probabilistic model checking, and furthermore
encourages the development of acceptance-agnostic tools for automata manipulations.
The format allows acceptance conditions that are either state-based or transition-based,
and also supports alternating automata.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Tomáš
full_name: Babiak, Tomáš
last_name: Babiak
- first_name: František
full_name: Blahoudek, František
last_name: Blahoudek
- first_name: Alexandre
full_name: Duret Lutz, Alexandre
last_name: Duret Lutz
- first_name: Joachim
full_name: Klein, Joachim
last_name: Klein
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Daniel
full_name: Mueller, Daniel
last_name: Mueller
- first_name: David
full_name: Parker, David
last_name: Parker
- first_name: Jan
full_name: Strejček, Jan
last_name: Strejček
citation:
ama: 'Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format.
In: Vol 9206. Springer; 2015:479-486. doi:10.1007/978-3-319-21690-4_31'
apa: 'Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller,
D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486).
Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States:
Springer. https://doi.org/10.1007/978-3-319-21690-4_31'
chicago: Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein,
Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata
Format,” 9206:479–86. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_31.
ieee: 'T. Babiak et al., “The Hanoi omega-automata format,” presented at
the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015,
vol. 9206, pp. 479–486.'
ista: 'Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker
D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification,
LNCS, vol. 9206, 479–486.'
mla: Babiak, Tomáš, et al. The Hanoi Omega-Automata Format. Vol. 9206, Springer,
2015, pp. 479–86, doi:10.1007/978-3-319-21690-4_31.
short: T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller,
D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486.
conference:
end_date: 2015-07-24
location: San Francisco, CA, United States
name: 'CAV: Computer Aided Verification'
start_date: 2015-07-18
date_created: 2018-12-11T11:52:57Z
date_published: 2015-07-16T00:00:00Z
date_updated: 2021-01-12T06:51:54Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-319-21690-4_31
ec_funded: 1
file:
- access_level: open_access
checksum: 5885236fa88a439baba9ac6f3e801e93
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:38:12Z
date_updated: 2020-07-14T12:45:04Z
file_id: '7850'
file_name: 2015_CAV_Babiak.pdf
file_size: 1651779
relation: main_file
file_date_updated: 2020-07-14T12:45:04Z
has_accepted_license: '1'
intvolume: ' 9206'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 479 - 486
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '5566'
quality_controlled: '1'
scopus_import: 1
status: public
title: The Hanoi omega-automata format
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9206
year: '2015'
...
---
_id: '1609'
abstract:
- lang: eng
text: The synthesis problem asks for the automatic construction of a system from
its specification. In the traditional setting, the system is “constructed from
scratch” rather than composed from reusable components. However, this is rare
in practice, and almost every non-trivial software system relies heavily on the
use of libraries of reusable components. Recently, Lustig and Vardi introduced
dataflow and controlflow synthesis from libraries of reusable components. They
proved that dataflow synthesis is undecidable, while controlflow synthesis is
decidable. The problem of controlflow synthesis from libraries of probabilistic
components was considered by Nain, Lustig and Vardi, and was shown to be decidable
for qualitative analysis (that asks that the specification be satisfied with probability
1). Our main contribution for controlflow synthesis from probabilistic components
is to establish better complexity bounds for the qualitative analysis problem,
and to show that the more general quantitative problem is undecidable. For the
qualitative analysis, we show that the problem (i) is EXPTIME-complete when the
specification is given as a deterministic parity word automaton, improving the
previously known 2EXPTIME upper bound; and (ii) belongs to UP ∩ coUP and is parity-games
hard, when the specification is given directly as a parity condition on the components,
improving the previously known EXPTIME upper bound.
acknowledgement: 'This research was supported by Austrian Science Fund (FWF) Grant
No P23499- N23, FWF NFN Grant No S11407-N23 (SHiNE), ERC Start grant (279307: Graph
Games), EU FP7 Project Cassting, NSF grants CNS 1049862 and CCF-1139011, by NSF
Expeditions in Computing project “ExCAPE: Expeditions in Computer Augmented Program
Engineering”, by BSF grant 9800096, and by gift from Intel.'
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: Moshe
full_name: Vardi, Moshe
last_name: Vardi
citation:
ama: 'Chatterjee K, Doyen L, Vardi M. The complexity of synthesis from probabilistic
components. In: 42nd International Colloquium. Vol 9135. Springer Nature;
2015:108-120. doi:10.1007/978-3-662-47666-6_9'
apa: 'Chatterjee, K., Doyen, L., & Vardi, M. (2015). The complexity of synthesis
from probabilistic components. In 42nd International Colloquium (Vol. 9135,
pp. 108–120). Kyoto, Japan: Springer Nature. https://doi.org/10.1007/978-3-662-47666-6_9'
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Moshe Vardi. “The Complexity
of Synthesis from Probabilistic Components.” In 42nd International Colloquium,
9135:108–20. Springer Nature, 2015. https://doi.org/10.1007/978-3-662-47666-6_9.
ieee: K. Chatterjee, L. Doyen, and M. Vardi, “The complexity of synthesis from probabilistic
components,” in 42nd International Colloquium, Kyoto, Japan, 2015, vol.
9135, pp. 108–120.
ista: 'Chatterjee K, Doyen L, Vardi M. 2015. The complexity of synthesis from probabilistic
components. 42nd International Colloquium. ICALP: Automata, Languages and Programming,
LNCS, vol. 9135, 108–120.'
mla: Chatterjee, Krishnendu, et al. “The Complexity of Synthesis from Probabilistic
Components.” 42nd International Colloquium, vol. 9135, Springer Nature,
2015, pp. 108–20, doi:10.1007/978-3-662-47666-6_9.
short: K. Chatterjee, L. Doyen, M. Vardi, in:, 42nd International Colloquium, Springer
Nature, 2015, pp. 108–120.
conference:
end_date: 2015-07-10
location: Kyoto, Japan
name: 'ICALP: Automata, Languages and Programming'
start_date: 2015-07-06
date_created: 2018-12-11T11:53:00Z
date_published: 2015-06-20T00:00:00Z
date_updated: 2022-02-01T15:04:44Z
day: '20'
department:
- _id: KrCh
doi: 10.1007/978-3-662-47666-6_9
ec_funded: 1
intvolume: ' 9135'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1502.04844
month: '06'
oa: 1
oa_version: Preprint
page: 108 - 120
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: 42nd International Colloquium
publication_identifier:
isbn:
- 978-3-662-47665-9
publication_status: published
publisher: Springer Nature
publist_id: '5557'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The complexity of synthesis from probabilistic components
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 9135
year: '2015'
...
---
_id: '1624'
abstract:
- lang: eng
text: Population structure can facilitate evolution of cooperation. In a structured
population, cooperators can form clusters which resist exploitation by defectors.
Recently, it was observed that a shift update rule is an extremely strong amplifier
of cooperation in a one dimensional spatial model. For the shift update rule,
an individual is chosen for reproduction proportional to fecundity; the offspring
is placed next to the parent; a random individual dies. Subsequently, the population
is rearranged (shifted) until all individual cells are again evenly spaced out.
For large population size and a one dimensional population structure, the shift
update rule favors cooperation for any benefit-to-cost ratio greater than one.
But every attempt to generalize shift updating to higher dimensions while maintaining
its strong effect has failed. The reason is that in two dimensions the clusters
are fragmented by the movements caused by rearranging the cells. Here we introduce
the natural phenomenon of a repulsive force between cells of different types.
After a birth and death event, the cells are being rearranged minimizing the overall
energy expenditure. If the repulsive force is sufficiently high, shift becomes
a strong promoter of cooperation in two dimensions.
acknowledgement: 'The research was supported by the Austrian Science Fund (FWF) Grant
No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307:
Graph Games), and Microsoft Faculty Fellows award. Support from the John Templeton
foundation is gratefully acknowledged.'
article_number: '17147'
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ben
full_name: Adlam, Ben
last_name: Adlam
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. Cellular cooperation with shift
updating and repulsion. Scientific Reports. 2015;5. doi:10.1038/srep17147
apa: Pavlogiannis, A., Chatterjee, K., Adlam, B., & Nowak, M. (2015). Cellular
cooperation with shift updating and repulsion. Scientific Reports. Nature
Publishing Group. https://doi.org/10.1038/srep17147
chicago: Pavlogiannis, Andreas, Krishnendu Chatterjee, Ben Adlam, and Martin Nowak.
“Cellular Cooperation with Shift Updating and Repulsion.” Scientific Reports.
Nature Publishing Group, 2015. https://doi.org/10.1038/srep17147.
ieee: A. Pavlogiannis, K. Chatterjee, B. Adlam, and M. Nowak, “Cellular cooperation
with shift updating and repulsion,” Scientific Reports, vol. 5. Nature
Publishing Group, 2015.
ista: Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. 2015. Cellular cooperation
with shift updating and repulsion. Scientific Reports. 5, 17147.
mla: Pavlogiannis, Andreas, et al. “Cellular Cooperation with Shift Updating and
Repulsion.” Scientific Reports, vol. 5, 17147, Nature Publishing Group,
2015, doi:10.1038/srep17147.
short: A. Pavlogiannis, K. Chatterjee, B. Adlam, M. Nowak, Scientific Reports 5
(2015).
date_created: 2018-12-11T11:53:06Z
date_published: 2015-11-25T00:00:00Z
date_updated: 2021-01-12T06:52:05Z
day: '25'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/srep17147
ec_funded: 1
file:
- access_level: open_access
checksum: 38e06d8310d2087cae5f6d4d4bfe082b
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:29Z
date_updated: 2020-07-14T12:45:07Z
file_id: '4947'
file_name: IST-2016-466-v1+1_srep17147.pdf
file_size: 1021931
relation: main_file
file_date_updated: 2020-07-14T12:45:07Z
has_accepted_license: '1'
intvolume: ' 5'
language:
- iso: eng
month: '11'
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'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Scientific Reports
publication_status: published
publisher: Nature Publishing Group
publist_id: '5536'
pubrep_id: '466'
quality_controlled: '1'
scopus_import: 1
status: public
title: Cellular cooperation with shift updating and repulsion
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: 5
year: '2015'
...
---
_id: '1660'
abstract:
- lang: eng
text: We study the pattern frequency vector for runs in probabilistic Vector Addition
Systems with States (pVASS). Intuitively, each configuration of a given pVASS
is assigned one of finitely many patterns, and every run can thus be seen as an
infinite sequence of these patterns. The pattern frequency vector assigns to each
run the limit of pattern frequencies computed for longer and longer prefixes of
the run. If the limit does not exist, then the vector is undefined. We show that
for one-counter pVASS, the pattern frequency vector is defined and takes one of
finitely many values for almost all runs. Further, these values and their associated
probabilities can be approximated up to an arbitrarily small relative error in
polynomial time. For stable two-counter pVASS, we show the same result, but we
do not provide any upper complexity bound. As a byproduct of our study, we discover
counterexamples falsifying some classical results about stochastic Petri nets
published in the 80s.
alternative_title:
- LICS
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Stefan
full_name: Kiefer, Stefan
last_name: Kiefer
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Kiefer S, Kučera A, Novotný P. Long-run average behaviour of probabilistic
vector addition systems. In: IEEE; 2015:44-55. doi:10.1109/LICS.2015.15'
apa: 'Brázdil, T., Kiefer, S., Kučera, A., & Novotný, P. (2015). Long-run average
behaviour of probabilistic vector addition systems (pp. 44–55). Presented at the
LICS: Logic in Computer Science, Kyoto, Japan: IEEE. https://doi.org/10.1109/LICS.2015.15'
chicago: Brázdil, Tomáš, Stefan Kiefer, Antonín Kučera, and Petr Novotný. “Long-Run
Average Behaviour of Probabilistic Vector Addition Systems,” 44–55. IEEE, 2015.
https://doi.org/10.1109/LICS.2015.15.
ieee: 'T. Brázdil, S. Kiefer, A. Kučera, and P. Novotný, “Long-run average behaviour
of probabilistic vector addition systems,” presented at the LICS: Logic in Computer
Science, Kyoto, Japan, 2015, pp. 44–55.'
ista: 'Brázdil T, Kiefer S, Kučera A, Novotný P. 2015. Long-run average behaviour
of probabilistic vector addition systems. LICS: Logic in Computer Science, LICS,
, 44–55.'
mla: Brázdil, Tomáš, et al. Long-Run Average Behaviour of Probabilistic Vector
Addition Systems. IEEE, 2015, pp. 44–55, doi:10.1109/LICS.2015.15.
short: T. Brázdil, S. Kiefer, A. Kučera, P. Novotný, in:, IEEE, 2015, pp. 44–55.
conference:
end_date: 2015-07-10
location: Kyoto, Japan
name: 'LICS: Logic in Computer Science'
start_date: 2015-07-06
date_created: 2018-12-11T11:53:19Z
date_published: 2015-07-01T00:00:00Z
date_updated: 2021-01-12T06:52:20Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/LICS.2015.15
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1505.02655
month: '07'
oa: 1
oa_version: Preprint
page: 44 - 55
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: IEEE
publist_id: '5490'
quality_controlled: '1'
scopus_import: 1
status: public
title: Long-run average behaviour of probabilistic vector addition systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1665'
abstract:
- lang: eng
text: Which genetic alterations drive tumorigenesis and how they evolve over the
course of disease and therapy are central questions in cancer biology. Here we
identify 44 recurrently mutated genes and 11 recurrent somatic copy number variations
through whole-exome sequencing of 538 chronic lymphocytic leukaemia (CLL) and
matched germline DNA samples, 278 of which were collected in a prospective clinical
trial. These include previously unrecognized putative cancer drivers (RPS15, IKZF3),
and collectively identify RNA processing and export, MYC activity, and MAPK signalling
as central pathways involved in CLL. Clonality analysis of this large data set
further enabled reconstruction of temporal relationships between driver events.
Direct comparison between matched pre-treatment and relapse samples from 59 patients
demonstrated highly frequent clonal evolution. Thus, large sequencing data sets
of clinically informative samples enable the discovery of novel genes associated
with cancer, the network of relationships between the driver events, and their
impact on disease relapse and clinical outcome.
article_processing_charge: No
article_type: original
author:
- first_name: Dan
full_name: Landau, Dan
last_name: Landau
- first_name: Eugen
full_name: Tausch, Eugen
last_name: Tausch
- first_name: Amaro
full_name: Taylor Weiner, Amaro
last_name: Taylor Weiner
- first_name: Chip
full_name: Stewart, Chip
last_name: Stewart
- first_name: Johannes
full_name: Reiter, Johannes
id: 4A918E98-F248-11E8-B48F-1D18A9856A87
last_name: Reiter
orcid: 0000-0002-0170-7353
- first_name: Jasmin
full_name: Bahlo, Jasmin
last_name: Bahlo
- first_name: Sandra
full_name: Kluth, Sandra
last_name: Kluth
- first_name: Ivana
full_name: Božić, Ivana
last_name: Božić
- first_name: Michael
full_name: Lawrence, Michael
last_name: Lawrence
- first_name: Sebastian
full_name: Böttcher, Sebastian
last_name: Böttcher
- first_name: Scott
full_name: Carter, Scott
last_name: Carter
- first_name: Kristian
full_name: Cibulskis, Kristian
last_name: Cibulskis
- first_name: Daniel
full_name: Mertens, Daniel
last_name: Mertens
- first_name: Carrie
full_name: Sougnez, Carrie
last_name: Sougnez
- first_name: Mara
full_name: Rosenberg, Mara
last_name: Rosenberg
- first_name: Julian
full_name: Hess, Julian
last_name: Hess
- first_name: Jennifer
full_name: Edelmann, Jennifer
last_name: Edelmann
- first_name: Sabrina
full_name: Kless, Sabrina
last_name: Kless
- first_name: Michael
full_name: Kneba, Michael
last_name: Kneba
- first_name: Matthias
full_name: Ritgen, Matthias
last_name: Ritgen
- first_name: Anna
full_name: Fink, Anna
last_name: Fink
- first_name: Kirsten
full_name: Fischer, Kirsten
last_name: Fischer
- first_name: Stacey
full_name: Gabriel, Stacey
last_name: Gabriel
- first_name: Eric
full_name: Lander, Eric
last_name: Lander
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
- first_name: Hartmut
full_name: Döhner, Hartmut
last_name: Döhner
- first_name: Michael
full_name: Hallek, Michael
last_name: Hallek
- first_name: Donna
full_name: Neuberg, Donna
last_name: Neuberg
- first_name: Gad
full_name: Getz, Gad
last_name: Getz
- first_name: Stephan
full_name: Stilgenbauer, Stephan
last_name: Stilgenbauer
- first_name: Catherine
full_name: Wu, Catherine
last_name: Wu
citation:
ama: Landau D, Tausch E, Taylor Weiner A, et al. Mutations driving CLL and their
evolution in progression and relapse. Nature. 2015;526(7574):525-530. doi:10.1038/nature15395
apa: Landau, D., Tausch, E., Taylor Weiner, A., Stewart, C., Reiter, J., Bahlo,
J., … Wu, C. (2015). Mutations driving CLL and their evolution in progression
and relapse. Nature. Nature Publishing Group. https://doi.org/10.1038/nature15395
chicago: Landau, Dan, Eugen Tausch, Amaro Taylor Weiner, Chip Stewart, Johannes
Reiter, Jasmin Bahlo, Sandra Kluth, et al. “Mutations Driving CLL and Their Evolution
in Progression and Relapse.” Nature. Nature Publishing Group, 2015. https://doi.org/10.1038/nature15395.
ieee: D. Landau et al., “Mutations driving CLL and their evolution in progression
and relapse,” Nature, vol. 526, no. 7574. Nature Publishing Group, pp.
525–530, 2015.
ista: Landau D, Tausch E, Taylor Weiner A, Stewart C, Reiter J, Bahlo J, Kluth S,
Božić I, Lawrence M, Böttcher S, Carter S, Cibulskis K, Mertens D, Sougnez C,
Rosenberg M, Hess J, Edelmann J, Kless S, Kneba M, Ritgen M, Fink A, Fischer K,
Gabriel S, Lander E, Nowak M, Döhner H, Hallek M, Neuberg D, Getz G, Stilgenbauer
S, Wu C. 2015. Mutations driving CLL and their evolution in progression and relapse.
Nature. 526(7574), 525–530.
mla: Landau, Dan, et al. “Mutations Driving CLL and Their Evolution in Progression
and Relapse.” Nature, vol. 526, no. 7574, Nature Publishing Group, 2015,
pp. 525–30, doi:10.1038/nature15395.
short: D. Landau, E. Tausch, A. Taylor Weiner, C. Stewart, J. Reiter, J. Bahlo,
S. Kluth, I. Božić, M. Lawrence, S. Böttcher, S. Carter, K. Cibulskis, D. Mertens,
C. Sougnez, M. Rosenberg, J. Hess, J. Edelmann, S. Kless, M. Kneba, M. Ritgen,
A. Fink, K. Fischer, S. Gabriel, E. Lander, M. Nowak, H. Döhner, M. Hallek, D.
Neuberg, G. Getz, S. Stilgenbauer, C. Wu, Nature 526 (2015) 525–530.
date_created: 2018-12-11T11:53:21Z
date_published: 2015-10-22T00:00:00Z
date_updated: 2021-01-12T06:52:23Z
day: '22'
department:
- _id: KrCh
doi: 10.1038/nature15395
ec_funded: 1
external_id:
pmid:
- '26466571'
intvolume: ' 526'
issue: '7574'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4815041/
month: '10'
oa: 1
oa_version: Submitted Version
page: 525 - 530
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: Nature
publication_status: published
publisher: Nature Publishing Group
publist_id: '5484'
quality_controlled: '1'
scopus_import: 1
status: public
title: Mutations driving CLL and their evolution in progression and relapse
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 526
year: '2015'
...
---
_id: '1667'
abstract:
- lang: eng
text: We consider parametric version of fixed-delay continuoustime Markov chains
(or equivalently deterministic and stochastic Petri nets, DSPN) where fixed-delay
transitions are specified by parameters, rather than concrete values. Our goal
is to synthesize values of these parameters that, for a given cost function, minimise
expected total cost incurred before reaching a given set of target states. We
show that under mild assumptions, optimal values of parameters can be effectively
approximated using translation to a Markov decision process (MDP) whose actions
correspond to discretized values of these parameters. To this end we identify
and overcome several interesting phenomena arising in systems with fixed delays.
acknowledgement: The research leading to these results has received funding from the
People Programme (Marie Curie Actions) of the European Union’s Seventh Framework
Programme (FP7/2007-2013) under REA grant agreement n∘ [291734]. This work is partly
supported by the German Research Council (DFG) as part of the Transregional Collaborative
Research Center AVACS (SFB/TR 14), by the EU 7th Framework Programme under grant
agreement no. 295261 (MEALS) and 318490 (SENSATION), by the Czech Science Foundation,
grant No. 15-17564S, and by the CAS/SAFEA International Partnership Program for
Creative Research Teams.
alternative_title:
- LNCS
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: L'Uboš
full_name: Korenčiak, L'Uboš
last_name: Korenčiak
- first_name: Jan
full_name: Krčál, Jan
last_name: Krčál
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Vojtěch
full_name: Řehák, Vojtěch
last_name: Řehák
citation:
ama: Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. Optimizing performance
of continuous-time stochastic systems using timeout synthesis. 2015;9259:141-159.
doi:10.1007/978-3-319-22264-6_10
apa: 'Brázdil, T., Korenčiak, L., Krčál, J., Novotný, P., & Řehák, V. (2015).
Optimizing performance of continuous-time stochastic systems using timeout synthesis.
Presented at the QEST: Quantitative Evaluation of Systems, Madrid, Spain: Springer.
https://doi.org/10.1007/978-3-319-22264-6_10'
chicago: Brázdil, Tomáš, L’Uboš Korenčiak, Jan Krčál, Petr Novotný, and Vojtěch
Řehák. “Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout
Synthesis.” Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-319-22264-6_10.
ieee: T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, and V. Řehák, “Optimizing
performance of continuous-time stochastic systems using timeout synthesis,” vol.
9259. Springer, pp. 141–159, 2015.
ista: Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. 2015. Optimizing performance
of continuous-time stochastic systems using timeout synthesis. 9259, 141–159.
mla: Brázdil, Tomáš, et al. Optimizing Performance of Continuous-Time Stochastic
Systems Using Timeout Synthesis. Vol. 9259, Springer, 2015, pp. 141–59, doi:10.1007/978-3-319-22264-6_10.
short: T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, V. Řehák, 9259 (2015) 141–159.
conference:
end_date: 2015-09-03
location: Madrid, Spain
name: 'QEST: Quantitative Evaluation of Systems'
start_date: 2015-09-01
date_created: 2018-12-11T11:53:22Z
date_published: 2015-08-22T00:00:00Z
date_updated: 2021-01-12T06:52:24Z
day: '22'
department:
- _id: KrCh
doi: 10.1007/978-3-319-22264-6_10
ec_funded: 1
intvolume: ' 9259'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1407.4777
month: '08'
oa: 1
oa_version: Preprint
page: 141 - 159
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5482'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Optimizing performance of continuous-time stochastic systems using timeout
synthesis
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9259
year: '2015'
...
---
_id: '1673'
abstract:
- lang: eng
text: 'When a new mutant arises in a population, there is a probability it outcompetes
the residents and fixes. The structure of the population can affect this fixation
probability. Suppressing population structures reduce the difference between two
competing variants, while amplifying population structures enhance the difference.
Suppressors are ubiquitous and easy to construct, but amplifiers for the large
population limit are more elusive and only a few examples have been discovered.
Whether or not a population structure is an amplifier of selection depends on
the probability distribution for the placement of the invading mutant. First,
we prove that there exist only bounded amplifiers for adversarial placement-that
is, for arbitrary initial conditions. Next, we show that the Star population structure,
which is known to amplify for mutants placed uniformly at random, does not amplify
for mutants that arise through reproduction and are therefore placed proportional
to the temperatures of the vertices. Finally, we construct population structures
that amplify for all mutational events that arise through reproduction, uniformly
at random, or through some combination of the two. '
acknowledgement: 'K.C. gratefully acknowledges support from ERC Start grant no. (279307:
Graph Games), Austrian Science Fund (FWF) grant no. P23499-N23, and FWF NFN grant
no. S11407-N23 (RiSE). '
article_number: '20150114'
author:
- first_name: Ben
full_name: Adlam, Ben
last_name: Adlam
- 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: 'Adlam B, Chatterjee K, Nowak M. Amplifiers of selection. Proceedings of
the Royal Society A: Mathematical, Physical and Engineering Sciences. 2015;471(2181).
doi:10.1098/rspa.2015.0114'
apa: 'Adlam, B., Chatterjee, K., & Nowak, M. (2015). Amplifiers of selection.
Proceedings of the Royal Society A: Mathematical, Physical and Engineering
Sciences. Royal Society of London. https://doi.org/10.1098/rspa.2015.0114'
chicago: 'Adlam, Ben, Krishnendu Chatterjee, and Martin Nowak. “Amplifiers of Selection.”
Proceedings of the Royal Society A: Mathematical, Physical and Engineering
Sciences. Royal Society of London, 2015. https://doi.org/10.1098/rspa.2015.0114.'
ieee: 'B. Adlam, K. Chatterjee, and M. Nowak, “Amplifiers of selection,” Proceedings
of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol.
471, no. 2181. Royal Society of London, 2015.'
ista: 'Adlam B, Chatterjee K, Nowak M. 2015. Amplifiers of selection. Proceedings
of the Royal Society A: Mathematical, Physical and Engineering Sciences. 471(2181),
20150114.'
mla: 'Adlam, Ben, et al. “Amplifiers of Selection.” Proceedings of the Royal
Society A: Mathematical, Physical and Engineering Sciences, vol. 471, no.
2181, 20150114, Royal Society of London, 2015, doi:10.1098/rspa.2015.0114.'
short: 'B. Adlam, K. Chatterjee, M. Nowak, Proceedings of the Royal Society A: Mathematical,
Physical and Engineering Sciences 471 (2015).'
date_created: 2018-12-11T11:53:24Z
date_published: 2015-09-08T00:00:00Z
date_updated: 2021-01-12T06:52:26Z
day: '08'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1098/rspa.2015.0114
ec_funded: 1
file:
- access_level: open_access
checksum: e613d94d283c776322403a28aad11bdd
content_type: application/pdf
creator: kschuh
date_created: 2019-04-18T12:39:56Z
date_updated: 2020-07-14T12:45:11Z
file_id: '6342'
file_name: 2015_rspa_Adlam.pdf
file_size: 391466
relation: main_file
file_date_updated: 2020-07-14T12:45:11Z
has_accepted_license: '1'
intvolume: ' 471'
issue: '2181'
language:
- iso: eng
month: '09'
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 Royal Society A: Mathematical, Physical and Engineering
Sciences'
publication_status: published
publisher: Royal Society of London
publist_id: '5477'
quality_controlled: '1'
scopus_import: 1
status: public
title: Amplifiers of selection
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 471
year: '2015'
...
---
_id: '1691'
abstract:
- lang: eng
text: We consider a case study of the problem of deploying an autonomous air vehicle
in a partially observable, dynamic, indoor environment from a specification given
as a linear temporal logic (LTL) formula over regions of interest. We model the
motion and sensing capabilities of the vehicle as a partially observable Markov
decision process (POMDP). We adapt recent results for solving POMDPs with parity
objectives to generate a control policy. We also extend the existing framework
with a policy minimization technique to obtain a better implementable policy,
while preserving its correctness. The proposed techniques are illustrated in an
experimental setup involving an autonomous quadrotor performing surveillance in
a dynamic environment.
author:
- first_name: Mária
full_name: Svoreňová, Mária
last_name: Svoreňová
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Kevin
full_name: Leahy, Kevin
last_name: Leahy
- first_name: Hasan
full_name: Eniser, Hasan
last_name: Eniser
- 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, Chmelik M, Leahy K, et al. Temporal logic motion planning using
POMDPs with parity objectives: Case study paper. In: Proceedings of the 18th
International Conference on Hybrid Systems: Computation and Control. ACM;
2015:233-238. doi:10.1145/2728606.2728617'
apa: 'Svoreňová, M., Chmelik, M., Leahy, K., Eniser, H., Chatterjee, K., Cěrná,
I., & Belta, C. (2015). Temporal logic motion planning using POMDPs with parity
objectives: Case study paper. In Proceedings of the 18th International Conference
on Hybrid Systems: Computation and Control (pp. 233–238). Seattle, WA, United
States: ACM. https://doi.org/10.1145/2728606.2728617'
chicago: 'Svoreňová, Mária, Martin Chmelik, Kevin Leahy, Hasan Eniser, Krishnendu
Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Motion Planning Using
POMDPs with Parity Objectives: Case Study Paper.” In Proceedings of the 18th
International Conference on Hybrid Systems: Computation and Control, 233–38.
ACM, 2015. https://doi.org/10.1145/2728606.2728617.'
ieee: 'M. Svoreňová et al., “Temporal logic motion planning using POMDPs
with parity objectives: Case study paper,” in Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control, Seattle, WA, United
States, 2015, pp. 233–238.'
ista: 'Svoreňová M, Chmelik M, Leahy K, Eniser H, Chatterjee K, Cěrná I, Belta C.
2015. Temporal logic motion planning using POMDPs with parity objectives: Case
study paper. Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control. HSCC: Hybrid Systems - Computation and Control, 233–238.'
mla: 'Svoreňová, Mária, et al. “Temporal Logic Motion Planning Using POMDPs with
Parity Objectives: Case Study Paper.” Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 233–38,
doi:10.1145/2728606.2728617.'
short: 'M. Svoreňová, M. Chmelik, K. Leahy, H. Eniser, K. Chatterjee, I. Cěrná,
C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control, ACM, 2015, pp. 233–238.'
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:29Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2021-01-12T06:52:33Z
day: '14'
department:
- _id: KrCh
doi: 10.1145/2728606.2728617
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 233 - 238
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 18th International Conference on Hybrid Systems:
Computation and Control'
publication_status: published
publisher: ACM
publist_id: '5453'
scopus_import: 1
status: public
title: 'Temporal logic motion planning using POMDPs with parity objectives: Case study
paper'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1694'
abstract:
- lang: eng
text: "\r\nWe introduce quantitative timed refinement and timed simulation (directed)
metrics, incorporating zenoness checks, for timed systems. These metrics assign
positive real numbers which quantify the timing mismatches between two timed systems,
amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal
timing mismatch that can arise, (2) the “steady-state” maximal timing mismatches,
where initial transient timing mismatches are ignored; and (3) the (long-run)
average timing mismatches amongst two systems. These three kinds of mismatches
constitute three important types of timing differences. Our event times are the
global times, measured from the start of the system execution, not just the time
durations of individual steps. We present algorithms over timed automata for computing
the three quantitative simulation distances to within any desired degree of accuracy.
In order to compute the values of the quantitative simulation distances, we use
a game theoretic formulation. We introduce two new kinds of objectives for two
player games on finite-state game graphs: (1) eventual debit-sum level objectives,
and (2) average debit-sum level objectives. We present algorithms for computing
the optimal values for these objectives in graph games, and then use these algorithms
to compute the values of the timed simulation distances over timed automata.\r\n"
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: Chatterjee K, Prabhu V. Quantitative temporal simulation and refinement distances
for timed systems. IEEE Transactions on Automatic Control. 2015;60(9):2291-2306.
doi:10.1109/TAC.2015.2404612
apa: Chatterjee, K., & Prabhu, V. (2015). Quantitative temporal simulation and
refinement distances for timed systems. IEEE Transactions on Automatic Control.
IEEE. https://doi.org/10.1109/TAC.2015.2404612
chicago: Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation
and Refinement Distances for Timed Systems.” IEEE Transactions on Automatic
Control. IEEE, 2015. https://doi.org/10.1109/TAC.2015.2404612.
ieee: K. Chatterjee and V. Prabhu, “Quantitative temporal simulation and refinement
distances for timed systems,” IEEE Transactions on Automatic Control, vol.
60, no. 9. IEEE, pp. 2291–2306, 2015.
ista: Chatterjee K, Prabhu V. 2015. Quantitative temporal simulation and refinement
distances for timed systems. IEEE Transactions on Automatic Control. 60(9), 2291–2306.
mla: Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation
and Refinement Distances for Timed Systems.” IEEE Transactions on Automatic
Control, vol. 60, no. 9, IEEE, 2015, pp. 2291–306, doi:10.1109/TAC.2015.2404612.
short: K. Chatterjee, V. Prabhu, IEEE Transactions on Automatic Control 60 (2015)
2291–2306.
date_created: 2018-12-11T11:53:30Z
date_published: 2015-02-24T00:00:00Z
date_updated: 2021-01-12T06:52:34Z
day: '24'
department:
- _id: KrCh
doi: 10.1109/TAC.2015.2404612
ec_funded: 1
intvolume: ' 60'
issue: '9'
language:
- iso: eng
month: '02'
oa_version: None
page: 2291 - 2306
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: IEEE Transactions on Automatic Control
publication_status: published
publisher: IEEE
publist_id: '5450'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative temporal simulation and refinement distances for timed systems
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 60
year: '2015'
...
---
_id: '1698'
abstract:
- lang: eng
text: 'In mean-payoff games, the objective of the protagonist is to ensure that
the limit average of an infinite sequence of numeric weights is nonnegative. In
energy games, the objective is to ensure that the running sum of weights is always
nonnegative. Multi-mean-payoff and multi-energy games replace individual weights
by tuples, and the limit average (resp., running sum) of each coordinate must
be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy
games and show inter-reducibility of multi-mean-payoff and multi-energy games
for finite-memory strategies. We improve the computational complexity for solving
both classes with finite-memory strategies: we prove coNP-completeness improving
the previous known EXPSPACE bound. For memoryless strategies, we show that deciding
the existence of a winning strategy for the protagonist is NP-complete. We present
the first solution of multi-mean-payoff games with infinite-memory strategies:
we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf
objectives are coNP-complete.'
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499-N23, FWF NFN Grant No S11407-N23 and S11402-N23 (RiSE), ERC Start
grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant
QUAREM (267989: Quantitative Reactive Modeling), European project Cassting (FP7-601148),
ERC Start grant (279499: inVEST).'
author:
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
- 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
- first_name: Alexander
full_name: Rabinovich, Alexander
last_name: Rabinovich
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The
complexity of multi-mean-payoff and multi-energy games. Information and Computation.
2015;241(4):177-196. doi:10.1016/j.ic.2015.03.001
apa: Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., &
Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games.
Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2015.03.001
chicago: Velner, Yaron, Krishnendu Chatterjee, Laurent Doyen, Thomas A Henzinger,
Alexander Rabinovich, and Jean Raskin. “The Complexity of Multi-Mean-Payoff and
Multi-Energy Games.” Information and Computation. Elsevier, 2015. https://doi.org/10.1016/j.ic.2015.03.001.
ieee: Y. Velner, K. Chatterjee, L. Doyen, T. A. Henzinger, A. Rabinovich, and J.
Raskin, “The complexity of multi-mean-payoff and multi-energy games,” Information
and Computation, vol. 241, no. 4. Elsevier, pp. 177–196, 2015.
ista: Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. 2015.
The complexity of multi-mean-payoff and multi-energy games. Information and Computation.
241(4), 177–196.
mla: Velner, Yaron, et al. “The Complexity of Multi-Mean-Payoff and Multi-Energy
Games.” Information and Computation, vol. 241, no. 4, Elsevier, 2015, pp.
177–96, doi:10.1016/j.ic.2015.03.001.
short: Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin,
Information and Computation 241 (2015) 177–196.
date_created: 2018-12-11T11:53:32Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2021-01-12T06:52:36Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2015.03.001
ec_funded: 1
intvolume: ' 241'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1209.3234
month: '04'
oa: 1
oa_version: Preprint
page: 177 - 196
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: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '5443'
quality_controlled: '1'
scopus_import: 1
status: public
title: The complexity of multi-mean-payoff and multi-energy games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 241
year: '2015'
...
---
_id: '1820'
abstract:
- lang: eng
text: 'We consider partially observable Markov decision processes (POMDPs) with
a set of target states and every transition is associated with an integer cost.
The optimization objec- tive we study asks to minimize the expected total cost
till the target set is reached, while ensuring that the target set is reached
almost-surely (with probability 1). We show that for integer costs approximating
the optimal cost is undecidable. For positive costs, our results are as follows:
(i) we establish matching lower and upper bounds for the optimal cost and the
bound is double exponential; (ii) we show that the problem of approximating the
optimal cost is decidable and present ap- proximation algorithms developing on
the existing algorithms for POMDPs with finite-horizon objectives. While the worst-
case running time of our algorithm is double exponential, we present efficient
stopping criteria for the algorithm and show experimentally that it performs well
in many examples.'
acknowledgement: ' The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307:
Graph Games), and Microsoft faculty fellows award.'
alternative_title:
- Artifical Intelligence
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Raghav
full_name: Gupta, Raghav
last_name: Gupta
- first_name: Ayush
full_name: Kanodia, Ayush
last_name: Kanodia
citation:
ama: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability
in POMDPs. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial
Intelligence . Vol 5. AAAI Press; 2015:3496-3502.'
apa: 'Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2015). Optimal
cost almost-sure reachability in POMDPs. In Proceedings of the Twenty-Ninth
AAAI Conference on Artificial Intelligence (Vol. 5, pp. 3496–3502). Austin,
TX, USA: AAAI Press.'
chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia.
“Optimal Cost Almost-Sure Reachability in POMDPs.” In Proceedings of the Twenty-Ninth
AAAI Conference on Artificial Intelligence , 5:3496–3502. AAAI Press, 2015.
ieee: K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure
reachability in POMDPs,” in Proceedings of the Twenty-Ninth AAAI Conference
on Artificial Intelligence , Austin, TX, USA, 2015, vol. 5, pp. 3496–3502.
ista: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2015. Optimal cost almost-sure
reachability in POMDPs. Proceedings of the Twenty-Ninth AAAI Conference on Artificial
Intelligence . IAAI: Innovative Applications of Artificial Intelligence, Artifical
Intelligence, vol. 5, 3496–3502.'
mla: Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.”
Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence
, vol. 5, AAAI Press, 2015, pp. 3496–502.
short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, Proceedings of the
Twenty-Ninth AAAI Conference on Artificial Intelligence , AAAI Press, 2015, pp.
3496–3502.
conference:
end_date: 2015-01-30
location: Austin, TX, USA
name: 'IAAI: Innovative Applications of Artificial Intelligence'
start_date: 2015-01-25
date_created: 2018-12-11T11:54:11Z
date_published: 2015-06-01T00:00:00Z
date_updated: 2023-02-23T10:02:57Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
external_id:
arxiv:
- '1411.3880'
intvolume: ' 5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1411.3880
month: '06'
oa: 1
oa_version: Preprint
page: 3496-3502
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 Twenty-Ninth AAAI Conference on Artificial Intelligence '
publication_status: published
publisher: AAAI Press
publist_id: '5286'
quality_controlled: '1'
related_material:
record:
- id: '1529'
relation: later_version
status: public
scopus_import: 1
status: public
title: Optimal cost almost-sure reachability in POMDPs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5
year: '2015'
...
---
_id: '1838'
abstract:
- lang: eng
text: Synthesis of program parts is particularly useful for concurrent systems.
However, most approaches do not support common design tasks, like modifying a
single process without having to re-synthesize or verify the whole system. Assume-guarantee
synthesis (AGS) provides robustness against modifications of system parts, but
thus far has been limited to the perfect information setting. This means that
local variables cannot be hidden from other processes, which renders synthesis
results cumbersome or even impossible to realize.We resolve this shortcoming by
defining AGS under partial information. We analyze the complexity and decidability
in different settings, showing that the problem has a high worstcase complexity
and is undecidable in many interesting cases. Based on these observations, we
present a pragmatic algorithm based on bounded synthesis, and demonstrate its
practical applicability on several examples.
acknowledgement: 'This work was supported by the Austrian Science Fund (FWF) through
the research network RiSE (S11406-N23, S11407-N23) and grant nr. P23499-N23, by
the European Commission through an ERC Start grant (279307: Graph Games) and project
STANCE (317753), as well as by the German Research Foundation (DFG) through SFB/TR
14 AVACS and project ASDPS(JA 2357/2-1).'
alternative_title:
- LNCS
author:
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Swen
full_name: Jacobs, Swen
last_name: Jacobs
- first_name: Robert
full_name: Könighofer, Robert
last_name: Könighofer
citation:
ama: 'Bloem R, Chatterjee K, Jacobs S, Könighofer R. Assume-guarantee synthesis
for concurrent reactive programs with partial information. In: Vol 9035. Springer;
2015:517-532. doi:10.1007/978-3-662-46681-0_50'
apa: 'Bloem, R., Chatterjee, K., Jacobs, S., & Könighofer, R. (2015). Assume-guarantee
synthesis for concurrent reactive programs with partial information (Vol. 9035,
pp. 517–532). Presented at the TACAS: Tools and Algorithms for the Construction
and Analysis of Systems, London, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-46681-0_50'
chicago: Bloem, Roderick, Krishnendu Chatterjee, Swen Jacobs, and Robert Könighofer.
“Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information,”
9035:517–32. Springer, 2015. https://doi.org/10.1007/978-3-662-46681-0_50.
ieee: 'R. Bloem, K. Chatterjee, S. Jacobs, and R. Könighofer, “Assume-guarantee
synthesis for concurrent reactive programs with partial information,” presented
at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
London, United Kingdom, 2015, vol. 9035, pp. 517–532.'
ista: 'Bloem R, Chatterjee K, Jacobs S, Könighofer R. 2015. Assume-guarantee synthesis
for concurrent reactive programs with partial information. TACAS: Tools and Algorithms
for the Construction and Analysis of Systems, LNCS, vol. 9035, 517–532.'
mla: Bloem, Roderick, et al. Assume-Guarantee Synthesis for Concurrent Reactive
Programs with Partial Information. Vol. 9035, Springer, 2015, pp. 517–32,
doi:10.1007/978-3-662-46681-0_50.
short: R. Bloem, K. Chatterjee, S. Jacobs, R. Könighofer, in:, Springer, 2015, pp.
517–532.
conference:
end_date: 2015-04-18
location: London, United Kingdom
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2015-04-11
date_created: 2018-12-11T11:54:17Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2021-01-12T06:53:32Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-46681-0_50
ec_funded: 1
intvolume: ' 9035'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1411.4604
month: '01'
oa: 1
oa_version: Preprint
page: 517 - 532
project:
- _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: 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: '5264'
scopus_import: 1
status: public
title: Assume-guarantee synthesis for concurrent reactive programs with partial information
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9035
year: '2015'
...
---
_id: '1839'
abstract:
- lang: eng
text: We present MultiGain, a tool to synthesize strategies for Markov decision
processes (MDPs) with multiple mean-payoff objectives. Our models are described
in PRISM, and our tool uses the existing interface and simulator of PRISM. Our
tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives,
and also provides features such as (i) generating strategies and exploring them
for simulation, and checking them with respect to other properties; and (ii) generating
an approximate Pareto curve for two mean-payoff objectives. In addition, we present
a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives
under memoryless strategies.
alternative_title:
- LNCS
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. Multigain: A controller synthesis
tool for MDPs with multiple mean-payoff objectives. 2015;9035:181-187. doi:10.1007/978-3-662-46681-0_12'
apa: 'Brázdil, T., Chatterjee, K., Forejt, V., & Kučera, A. (2015). Multigain:
A controller synthesis tool for MDPs with multiple mean-payoff objectives. Presented
at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
London, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-46681-0_12'
chicago: 'Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera.
“Multigain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives.”
Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-662-46681-0_12.'
ieee: 'T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Multigain: A controller
synthesis tool for MDPs with multiple mean-payoff objectives,” vol. 9035. Springer,
pp. 181–187, 2015.'
ista: 'Brázdil T, Chatterjee K, Forejt V, Kučera A. 2015. Multigain: A controller
synthesis tool for MDPs with multiple mean-payoff objectives. 9035, 181–187.'
mla: 'Brázdil, Tomáš, et al. Multigain: A Controller Synthesis Tool for MDPs
with Multiple Mean-Payoff Objectives. Vol. 9035, Springer, 2015, pp. 181–87,
doi:10.1007/978-3-662-46681-0_12.'
short: T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, 9035 (2015) 181–187.
conference:
end_date: 2015-04-18
location: London, United Kingdom
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2015-04-11
date_created: 2018-12-11T11:54:18Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2020-01-21T13:18:52Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-46681-0_12
ec_funded: 1
intvolume: ' 9035'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1501.03093
month: '01'
oa: 1
oa_version: Preprint
page: 181 - 187
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_status: published
publisher: Springer
publist_id: '5263'
quality_controlled: '1'
series_title: Lecture Notes in Computer Science
status: public
title: 'Multigain: A controller synthesis tool for MDPs with multiple mean-payoff
objectives'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9035
year: '2015'
...
---
_id: '1846'
abstract:
- lang: eng
text: Modal transition systems (MTS) is a well-studied specification formalism of
reactive systems supporting a step-wise refinement methodology. Despite its many
advantages, the formalism as well as its currently known extensions are incapable
of expressing some practically needed aspects in the refinement process like exclusive,
conditional and persistent choices. We introduce a new model called parametric
modal transition systems (PMTS) together with a general modal refinement notion
that overcomes many of the limitations. We investigate the computational complexity
of modal and thorough refinement checking on PMTS and its subclasses and provide
a direct encoding of the modal refinement problem into quantified Boolean formulae,
allowing us to employ state-of-the-art QBF solvers for modal refinement checking.
The experiments we report on show that the feasibility of refinement checking
is more influenced by the degree of nondeterminism rather than by the syntactic
restrictions on the types of formulae allowed in the description of the PMTS.
article_processing_charge: No
article_type: original
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Kim
full_name: Larsen, Kim
last_name: Larsen
- first_name: Mikael
full_name: Möller, Mikael
last_name: Möller
- first_name: Salomon
full_name: Sickert, Salomon
last_name: Sickert
- first_name: Jiří
full_name: Srba, Jiří
last_name: Srba
citation:
ama: Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking
on parametric modal transition systems. Acta Informatica. 2015;52(2-3):269-297.
doi:10.1007/s00236-015-0215-4
apa: Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., & Srba,
J. (2015). Refinement checking on parametric modal transition systems. Acta
Informatica. Springer. https://doi.org/10.1007/s00236-015-0215-4
chicago: Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert,
and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” Acta
Informatica. Springer, 2015. https://doi.org/10.1007/s00236-015-0215-4.
ieee: N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement
checking on parametric modal transition systems,” Acta Informatica, vol.
52, no. 2–3. Springer, pp. 269–297, 2015.
ista: Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement
checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.
mla: Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.”
Acta Informatica, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:10.1007/s00236-015-0215-4.
short: N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica
52 (2015) 269–297.
date_created: 2018-12-11T11:54:20Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2021-01-12T06:53:35Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/s00236-015-0215-4
ec_funded: 1
file:
- access_level: open_access
checksum: fb4037ddc4fc05f33080dd3547ede350
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:57:44Z
date_updated: 2020-07-14T12:45:19Z
file_id: '7854'
file_name: 2015_ActaInfo_Benes.pdf
file_size: 488482
relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: ' 52'
issue: 2-3
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 269 - 297
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Acta Informatica
publication_status: published
publisher: Springer
publist_id: '5255'
quality_controlled: '1'
scopus_import: 1
status: public
title: Refinement checking on parametric modal transition systems
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 52
year: '2015'
...
---
_id: '1851'
abstract:
- lang: eng
text: We consider mating strategies for females who search for males sequentially
during a season of limited length. We show that the best strategy rejects a given
male type if encountered before a time-threshold but accepts him after. For frequency-independent
benefits, we obtain the optimal time-thresholds explicitly for both discrete and
continuous distributions of males, and allow for mistakes being made in assessing
the correct male type. When the benefits are indirect (genes for the offspring)
and the population is under frequency-dependent ecological selection, the benefits
depend on the mating strategy of other females as well. This case is particularly
relevant to speciation models that seek to explore the stability of reproductive
isolation by assortative mating under frequency-dependent ecological selection.
We show that the indirect benefits are to be quantified by the reproductive values
of couples, and describe how the evolutionarily stable time-thresholds can be
found. We conclude with an example based on the Levene model, in which we analyze
the evolutionarily stable assortative mating strategies and the strength of reproductive
isolation provided by them.
article_processing_charge: No
article_type: original
author:
- first_name: Tadeas
full_name: Priklopil, Tadeas
id: 3C869AA0-F248-11E8-B48F-1D18A9856A87
last_name: Priklopil
- first_name: Eva
full_name: Kisdi, Eva
last_name: Kisdi
- first_name: Mats
full_name: Gyllenberg, Mats
last_name: Gyllenberg
citation:
ama: Priklopil T, Kisdi E, Gyllenberg M. Evolutionarily stable mating decisions
for sequentially searching females and the stability of reproductive isolation
by assortative mating. Evolution. 2015;69(4):1015-1026. doi:10.1111/evo.12618
apa: Priklopil, T., Kisdi, E., & Gyllenberg, M. (2015). Evolutionarily stable
mating decisions for sequentially searching females and the stability of reproductive
isolation by assortative mating. Evolution. Wiley. https://doi.org/10.1111/evo.12618
chicago: Priklopil, Tadeas, Eva Kisdi, and Mats Gyllenberg. “Evolutionarily Stable
Mating Decisions for Sequentially Searching Females and the Stability of Reproductive
Isolation by Assortative Mating.” Evolution. Wiley, 2015. https://doi.org/10.1111/evo.12618.
ieee: T. Priklopil, E. Kisdi, and M. Gyllenberg, “Evolutionarily stable mating decisions
for sequentially searching females and the stability of reproductive isolation
by assortative mating,” Evolution, vol. 69, no. 4. Wiley, pp. 1015–1026,
2015.
ista: Priklopil T, Kisdi E, Gyllenberg M. 2015. Evolutionarily stable mating decisions
for sequentially searching females and the stability of reproductive isolation
by assortative mating. Evolution. 69(4), 1015–1026.
mla: Priklopil, Tadeas, et al. “Evolutionarily Stable Mating Decisions for Sequentially
Searching Females and the Stability of Reproductive Isolation by Assortative Mating.”
Evolution, vol. 69, no. 4, Wiley, 2015, pp. 1015–26, doi:10.1111/evo.12618.
short: T. Priklopil, E. Kisdi, M. Gyllenberg, Evolution 69 (2015) 1015–1026.
date_created: 2018-12-11T11:54:21Z
date_published: 2015-02-09T00:00:00Z
date_updated: 2022-06-07T10:52:37Z
day: '09'
ddc:
- '570'
department:
- _id: NiBa
- _id: KrCh
doi: 10.1111/evo.12618
ec_funded: 1
external_id:
pmid:
- '25662095'
file:
- access_level: open_access
checksum: 1e8be0b1d7598a78cd2623d8ee8e7798
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T09:05:34Z
date_updated: 2020-07-14T12:45:19Z
file_id: '7855'
file_name: 2015_Evolution_Priklopil.pdf
file_size: 967214
relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: ' 69'
issue: '4'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Submitted Version
page: 1015 - 1026
pmid: 1
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: Evolution
publication_identifier:
eissn:
- 1558-5646
issn:
- 0014-3820
publication_status: published
publisher: Wiley
publist_id: '5249'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Evolutionarily stable mating decisions for sequentially searching females and
the stability of reproductive isolation by assortative mating
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 69
year: '2015'
...