---
_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
article_processing_charge: No
arxiv: 1
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
corr_author: '1'
date_created: 2018-12-11T11:51:43Z
date_published: 2016-07-01T00:00:00Z
date_updated: 2026-09-02T22:30:58Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-319-41528-4_1
ec_funded: 1
external_id:
arxiv:
- '1604.07169'
isi:
- '000387731200001'
intvolume: ' 9779'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9779
year: '2016'
...
---
_id: '1481'
abstract:
- lang: eng
text: 'Simple board games, like Tic-Tac-Toe and CONNECT-4, play an important role
not only in the development of mathematical and logical skills, but also in the
emotional and social development. In this paper, we address the problem of generating
targeted starting positions for such games. This can facilitate new approaches
for bringing novice players to mastery, and also leads to discovery of interesting
game variants. We present an approach that generates starting states of varying
hardness levels for player 1 in a two-player board game, given rules of the board
game, the desired number of steps required for player 1 to win, and the expertise
levels of the two players. Our approach leverages symbolic methods and iterative
simulation to efficiently search the extremely large state space. We present experimental
results that include discovery of states of varying hardness levels for several
simple grid-based board games. The presence of such states for standard game variants
like 4×4 Tic-Tac-Toe opens up new games to be played that have never been played
as the default start state is heavily biased. '
acknowledgement: "A Technical Report of this paper is available at: \r\nhttps://repository.ist.ac.at/id/eprint/146.\r\n"
article_processing_charge: No
arxiv: 1
author:
- first_name: Umair
full_name: Ahmed, Umair
last_name: Ahmed
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Sumit
full_name: Gulwani, Sumit
last_name: Gulwani
citation:
ama: 'Ahmed U, Chatterjee K, Gulwani S. Automatic generation of alternative starting
positions for simple traditional board games. In: Proceedings of the Twenty-Ninth
AAAI Conference on Artificial Intelligence. Vol 2. AAAI Press; 2015:745-752.'
apa: 'Ahmed, U., Chatterjee, K., & Gulwani, S. (2015). Automatic generation
of alternative starting positions for simple traditional board games. In Proceedings
of the Twenty-Ninth AAAI Conference on Artificial Intelligence (Vol. 2, pp.
745–752). Austin, TX, USA: AAAI Press.'
chicago: Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. “Automatic Generation
of Alternative Starting Positions for Simple Traditional Board Games.” In Proceedings
of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2:745–52.
AAAI Press, 2015.
ieee: U. Ahmed, K. Chatterjee, and S. Gulwani, “Automatic generation of alternative
starting positions for simple traditional board games,” in Proceedings of the
Twenty-Ninth AAAI Conference on Artificial Intelligence, Austin, TX, USA,
2015, vol. 2, pp. 745–752.
ista: 'Ahmed U, Chatterjee K, Gulwani S. 2015. Automatic generation of alternative
starting positions for simple traditional board games. Proceedings of the Twenty-Ninth
AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence
vol. 2, 745–752.'
mla: Ahmed, Umair, et al. “Automatic Generation of Alternative Starting Positions
for Simple Traditional Board Games.” Proceedings of the Twenty-Ninth AAAI Conference
on Artificial Intelligence, vol. 2, AAAI Press, 2015, pp. 745–52.
short: U. Ahmed, K. Chatterjee, S. Gulwani, in:, Proceedings of the Twenty-Ninth
AAAI Conference on Artificial Intelligence, AAAI Press, 2015, pp. 745–752.
conference:
end_date: 2015-01-30
location: Austin, TX, USA
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2015-01-25
date_created: 2018-12-11T11:52:16Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2025-05-19T11:10:17Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
external_id:
arxiv:
- '1411.4023'
intvolume: ' 2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/download/9523/9300
month: '01'
oa: 1
oa_version: None
page: 745 - 752
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: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence
publication_status: published
publisher: AAAI Press
publist_id: '5713'
quality_controlled: '1'
related_material:
record:
- id: '5410'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Automatic generation of alternative starting positions for simple traditional
board games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
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: 2025-04-15T06:26:02Z
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: Formal methods for the design and analysis of complex systems
- _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: '1501'
abstract:
- lang: eng
text: 'We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems. We focus on qualitative properties for MDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability. We introduce a new simulation relation to capture
the refinement relation of MDPs with respect to qualitative properties, and present
discrete graph algorithms with quadratic complexity to compute the simulation
relation. We present an automated technique for assume-guarantee style reasoning
for compositional analysis of two-player games by giving a counterexample guided
abstraction-refinement approach to compute our new simulation relation. We show
a tight link between two-player games and MDPs, and as a consequence the results
for games are lifted to MDPs with qualitative properties. We have implemented
our algorithms and show that the compositional analysis leads to significant improvements. '
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE),
and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games),
Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive
Modeling).'
article_processing_charge: No
arxiv: 1
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: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
citation:
ama: Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative
properties in Markov decision processes. Formal Methods in System Design.
2015;47(2):230-264. doi:10.1007/s10703-015-0235-2
apa: Chatterjee, K., Chmelik, M., & Daca, P. (2015). CEGAR for compositional
analysis of qualitative properties in Markov decision processes. Formal Methods
in System Design. Springer. https://doi.org/10.1007/s10703-015-0235-2
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for
Compositional Analysis of Qualitative Properties in Markov Decision Processes.”
Formal Methods in System Design. Springer, 2015. https://doi.org/10.1007/s10703-015-0235-2.
ieee: K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis
of qualitative properties in Markov decision processes,” Formal Methods in
System Design, vol. 47, no. 2. Springer, pp. 230–264, 2015.
ista: Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of
qualitative properties in Markov decision processes. Formal Methods in System
Design. 47(2), 230–264.
mla: Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative
Properties in Markov Decision Processes.” Formal Methods in System Design,
vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:10.1007/s10703-015-0235-2.
short: K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015)
230–264.
corr_author: '1'
date_created: 2018-12-11T11:52:23Z
date_published: 2015-10-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10703-015-0235-2
ec_funded: 1
external_id:
arxiv:
- '1405.0835'
isi:
- '000361752300003'
intvolume: ' 47'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1405.0835
month: '10'
oa: 1
oa_version: Preprint
page: 230 - 264
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
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '5677'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: CEGAR for compositional analysis of qualitative properties in Markov decision
processes
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 47
year: '2015'
...
---
_id: '1502'
abstract:
- lang: eng
text: We extend the theory of input-output conformance with operators for merge
and quotient. The former is useful when testing against multiple requirements
or views. The latter can be used to generate tests for patches of an already tested
system. Both operators can combine systems with different action alphabets, which
is usually the case when constructing complex systems and specifications from
parts, for instance different views as well as newly defined functionality of
a~previous version of the system.
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF)
projects S11402-N23(RiSE) and Z211-N23 (Wittgestein Award), by People Programme
(Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013)
under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373
(nSafeCer). Jan Křetínský has been partially supported by the Czech Science Foundation,
grant No. P202/12/G061. Nikola Beneš has been supported by the\r\nMEYS project
No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for
Scientific Excellence."
alternative_title:
- 'Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based
Software Engineering '
article_processing_charge: No
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- 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: Dejan
full_name: Nickovic, Dejan
last_name: Nickovic
citation:
ama: 'Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition
operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:10.1145/2737166.2737175'
apa: 'Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., & Nickovic, D. (2015).
Complete composition operators for IOCO-testing theory (pp. 101–110). Presented
at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM.
https://doi.org/10.1145/2737166.2737175'
chicago: Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and
Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10.
ACM, 2015. https://doi.org/10.1145/2737166.2737175.
ieee: 'N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete
composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based
Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.'
ista: 'Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition
operators for IOCO-testing theory. CBSE: Component-Based Software Engineering
, Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based
Software Engineering , , 101–110.'
mla: Beneš, Nikola, et al. Complete Composition Operators for IOCO-Testing Theory.
ACM, 2015, pp. 101–10, doi:10.1145/2737166.2737175.
short: N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015,
pp. 101–110.
conference:
end_date: 2015-05-08
location: Montreal, QC, Canada
name: 'CBSE: Component-Based Software Engineering '
start_date: 2015-05-04
date_created: 2018-12-11T11:52:24Z
date_published: 2015-05-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2737166.2737175
ec_funded: 1
external_id:
isi:
- '000380554800013'
file:
- access_level: open_access
checksum: c6ce681035c163a158751f240cb7d389
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:46Z
date_updated: 2020-07-14T12:44:59Z
file_id: '5303'
file_name: IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf
file_size: 467561
relation: main_file
file_date_updated: 2020-07-14T12:44:59Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
page: 101 - 110
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: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_identifier:
isbn:
- 978-1-4503-3471-6
publication_status: published
publisher: ACM
publist_id: '5676'
pubrep_id: '625'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Complete composition operators for IOCO-testing theory
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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).'
article_processing_charge: No
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.
corr_author: '1'
date_created: 2018-12-11T11:52:43Z
date_published: 2015-12-22T00:00:00Z
date_updated: 2025-09-23T08:20:08Z
day: '22'
department:
- _id: KrCh
doi: 10.1073/pnas.1511366112
external_id:
isi:
- '000366916000044'
pmid:
- '26644569'
intvolume: ' 112'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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
article_processing_charge: No
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: 2025-09-23T08:21:59Z
day: '22'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-662-48899-7_12
ec_funded: 1
external_id:
isi:
- '000375574900012'
intvolume: ' 9450'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9450
year: '2015'
...
---
_id: '1598'
abstract:
- lang: eng
text: 'We consider Markov decision processes (MDPs) with specifications given as
Büchi (liveness) objectives, and examine the problem of computing the set of almost-sure
winning vertices such that the objective can be ensured with probability 1 from
these vertices. We study for the first time the average-case complexity of the
classical algorithm for computing the set of almost-sure winning vertices for
MDPs with Büchi objectives. Our contributions are as follows: First, we show that
for MDPs with constant out-degree the expected number of iterations is at most
logarithmic and the average-case running time is linear (as compared to the worst-case
linear number of iterations and quadratic time complexity). Second, for the average-case
analysis over all MDPs we show that the expected number of iterations is constant
and the average-case running time is linear (again as compared to the worst-case
linear number of iterations and quadratic time complexity). Finally we also show
that when all MDPs are equally likely, the probability that the classical algorithm
requires more than a constant number of iterations is exponentially small.'
acknowledgement: "The research was supported by FWF Grant No. P 23499-N23, FWF NFN
Grant No. S11407-N23 (RiSE), ERC Start Grant (279307: Graph Games), and the Microsoft
Faculty Fellows Award. Nisarg Shah is also supported by NSF Grant CCF-1215883.\r\n"
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Manas
full_name: Joglekar, Manas
last_name: Joglekar
- first_name: Nisarg
full_name: Shah, Nisarg
last_name: Shah
citation:
ama: Chatterjee K, Joglekar M, Shah N. Average case analysis of the classical algorithm
for Markov decision processes with Büchi objectives. Theoretical Computer Science.
2015;573(3):71-89. doi:10.1016/j.tcs.2015.01.050
apa: Chatterjee, K., Joglekar, M., & Shah, N. (2015). Average case analysis
of the classical algorithm for Markov decision processes with Büchi objectives.
Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2015.01.050
chicago: Chatterjee, Krishnendu, Manas Joglekar, and Nisarg Shah. “Average Case
Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives.”
Theoretical Computer Science. Elsevier, 2015. https://doi.org/10.1016/j.tcs.2015.01.050.
ieee: K. Chatterjee, M. Joglekar, and N. Shah, “Average case analysis of the classical
algorithm for Markov decision processes with Büchi objectives,” Theoretical
Computer Science, vol. 573, no. 3. Elsevier, pp. 71–89, 2015.
ista: Chatterjee K, Joglekar M, Shah N. 2015. Average case analysis of the classical
algorithm for Markov decision processes with Büchi objectives. Theoretical Computer
Science. 573(3), 71–89.
mla: Chatterjee, Krishnendu, et al. “Average Case Analysis of the Classical Algorithm
for Markov Decision Processes with Büchi Objectives.” Theoretical Computer
Science, vol. 573, no. 3, Elsevier, 2015, pp. 71–89, doi:10.1016/j.tcs.2015.01.050.
short: K. Chatterjee, M. Joglekar, N. Shah, Theoretical Computer Science 573 (2015)
71–89.
date_created: 2018-12-11T11:52:56Z
date_published: 2015-03-30T00:00:00Z
date_updated: 2025-09-23T08:00:31Z
day: '30'
department:
- _id: KrCh
doi: 10.1016/j.tcs.2015.01.050
ec_funded: 1
external_id:
arxiv:
- '1202.4175'
isi:
- '000350835500007'
intvolume: ' 573'
isi: 1
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1202.4175
month: '03'
oa: 1
oa_version: Preprint
page: 71 - 89
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: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '5571'
quality_controlled: '1'
related_material:
record:
- id: '2715'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Average case analysis of the classical algorithm for Markov decision processes
with Büchi objectives
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 573
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: 2025-09-23T13:50:55Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-319-21690-4_31
ec_funded: 1
external_id:
isi:
- '000364182900031'
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'
isi: 1
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: Formal methods for the design and analysis of complex systems
- _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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9206
year: '2015'
...
---
_id: '1602'
abstract:
- lang: eng
text: Interprocedural analysis is at the heart of numerous applications in programming
languages, such as alias analysis, constant propagation, etc. Recursive state
machines (RSMs) are standard models for interprocedural analysis. We consider
a general framework with RSMs where the transitions are labeled from a semiring,
and path properties are algebraic with semiring operations. RSMs with algebraic
path properties can model interprocedural dataflow analysis problems, the shortest
path problem, the most probable path problem, etc. The traditional algorithms
for interprocedural analysis focus on path properties where the starting point
is fixed as the entry point of a specific method. In this work, we consider possible
multiple queries as required in many applications such as in alias analysis. The
study of multiple queries allows us to bring in a very important algorithmic distinction
between the resource usage of the one-time preprocessing vs for each individual
query. The second aspect that we consider is that the control flow graphs for
most programs have constant treewidth. Our main contributions are simple and implementable
algorithms that supportmultiple queries for algebraic path properties for RSMs
that have constant treewidth. Our theoretical results show that our algorithms
have small additional one-time preprocessing, but can answer subsequent queries
significantly faster as compared to the current best-known solutions for several
important problems, such as interprocedural reachability and shortest path. We
provide a prototype implementation for interprocedural reachability and intraprocedural
shortest path that gives a significant speed-up on several benchmarks.
acknowledgement: We thank anonymous reviewers for helpful comments to improve the
presentation of the paper.
arxiv: 1
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
- first_name: Prateesh
full_name: Goyal, Prateesh
last_name: Goyal
citation:
ama: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. Faster algorithms for
algebraic path properties in recursive state machines with constant treewidth.
ACM SIGPLAN Notices. 2015;50(1):97-109. doi:10.1145/2676726.2676979
apa: 'Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A., & Goyal, P. (2015).
Faster algorithms for algebraic path properties in recursive state machines with
constant treewidth. ACM SIGPLAN Notices. Mumbai, India: ACM. https://doi.org/10.1145/2676726.2676979'
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, and
Prateesh Goyal. “Faster Algorithms for Algebraic Path Properties in Recursive
State Machines with Constant Treewidth.” ACM SIGPLAN Notices. ACM, 2015.
https://doi.org/10.1145/2676726.2676979.
ieee: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, and P. Goyal, “Faster algorithms
for algebraic path properties in recursive state machines with constant treewidth,”
ACM SIGPLAN Notices, vol. 50, no. 1. ACM, pp. 97–109, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. 2015. Faster algorithms
for algebraic path properties in recursive state machines with constant treewidth.
ACM SIGPLAN Notices. 50(1), 97–109.
mla: Chatterjee, Krishnendu, et al. “Faster Algorithms for Algebraic Path Properties
in Recursive State Machines with Constant Treewidth.” ACM SIGPLAN Notices,
vol. 50, no. 1, ACM, 2015, pp. 97–109, doi:10.1145/2676726.2676979.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, P. Goyal, ACM SIGPLAN Notices
50 (2015) 97–109.
conference:
end_date: 2015-01-17
location: Mumbai, India
name: 'SIGPLAN: Symposium on Principles of Programming Languages'
start_date: 2015-01-15
date_created: 2018-12-11T11:52:58Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2026-04-08T14:22:16Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2676726.2676979
ec_funded: 1
external_id:
arxiv:
- '1410.7724'
intvolume: ' 50'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1410.7724
month: '01'
oa: 1
oa_version: Preprint
page: 97 - 109
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'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: ACM SIGPLAN Notices
publication_status: published
publisher: ACM
publist_id: '5565'
quality_controlled: '1'
related_material:
record:
- id: '821'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Faster algorithms for algebraic path properties in recursive state machines
with constant treewidth
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 50
year: '2015'
...
---
_id: '1603'
abstract:
- lang: eng
text: "For deterministic systems, a counterexample to a property can simply be an
error trace, whereas counterexamples in probabilistic systems are necessarily
more complex. For instance, a set of erroneous traces with a sufficient cumulative
probability mass can be used. Since these are too large objects to understand
and manipulate, compact representations such as subchains have been considered.
In the case of probabilistic systems with non-determinism, the situation is even
more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism)
is a straightforward choice, we take a different approach. Instead, we focus on
the strategy itself, and extract the most important decisions it makes, and present
its succinct representation.\r\nThe key tools we employ to achieve this are (1)
introducing a concept of importance of a state w.r.t. the strategy, and (2) learning
using decision trees. There are three main consequent advantages of our approach.
Firstly, it exploits the quantitative information on states, stressing the more
important decisions. Secondly, it leads to a greater variability and degree of
freedom in representing the strategies. Thirdly, the representation uses a self-explanatory
data structure. In summary, our approach produces more succinct and more explainable
strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental
results show that we can extract several rules describing the strategy even for
very large systems that do not fit in memory, and based on the rules explain the
erroneous behaviour."
acknowledgement: This research was funded in part by Austrian Science Fund (FWF) Grant
No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award),
European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989
(QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme
(Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013)
REA Grant No 291734.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
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: Andreas
full_name: Fellner, Andreas
id: 42BABFB4-F248-11E8-B48F-1D18A9856A87
last_name: Fellner
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: 'Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample
explanation by learning small strategies in Markov decision processes. In: Vol
9206. Springer; 2015:158-177. doi:10.1007/978-3-319-21690-4_10'
apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., & Kretinsky, J.
(2015). Counterexample explanation by learning small strategies in Markov decision
processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification,
San Francisco, CA, United States: Springer. https://doi.org/10.1007/978-3-319-21690-4_10'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner,
and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in
Markov Decision Processes,” 9206:158–77. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_10.
ieee: 'T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample
explanation by learning small strategies in Markov decision processes,” presented
at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015,
vol. 9206, pp. 158–177.'
ista: 'Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample
explanation by learning small strategies in Markov decision processes. CAV: Computer
Aided Verification, LNCS, vol. 9206, 158–177.'
mla: Brázdil, Tomáš, et al. Counterexample Explanation by Learning Small Strategies
in Markov Decision Processes. Vol. 9206, Springer, 2015, pp. 158–77, doi:10.1007/978-3-319-21690-4_10.
short: T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer,
2015, pp. 158–177.
conference:
end_date: 2015-07-24
location: San Francisco, CA, United States
name: 'CAV: Computer Aided Verification'
start_date: 2015-07-18
corr_author: '1'
date_created: 2018-12-11T11:52:58Z
date_published: 2015-07-16T00:00:00Z
date_updated: 2025-09-23T08:23:16Z
day: '16'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-21690-4_10
ec_funded: 1
external_id:
arxiv:
- '1502.02834'
isi:
- '000364182900010'
intvolume: ' 9206'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1502.02834
month: '07'
oa: 1
oa_version: Preprint
page: 158 - 177
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_identifier:
eisbn:
- 978-3-319-21690-4
publication_status: published
publisher: Springer
publist_id: '5564'
quality_controlled: '1'
related_material:
record:
- id: '5549'
relation: research_paper
status: public
scopus_import: '1'
status: public
title: Counterexample explanation by learning small strategies in Markov decision
processes
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9206
year: '2015'
...
---
_id: '1604'
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.
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.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 2015;50(1):539-551.
doi:10.1145/2676726.2676968
apa: 'Chatterjee, K., Pavlogiannis, A., & Velner, Y. (2015). Quantitative interprocedural
analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . Mumbai, India:
ACM. https://doi.org/10.1145/2676726.2676968'
chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. “Quantitative
Interprocedural Analysis.” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT
. ACM, 2015. https://doi.org/10.1145/2676726.2676968.
ieee: K. Chatterjee, A. Pavlogiannis, and Y. Velner, “Quantitative interprocedural
analysis,” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT , vol. 50,
no. 1. ACM, pp. 539–551, 2015.
ista: Chatterjee K, Pavlogiannis A, Velner Y. 2015. Quantitative interprocedural
analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 50(1), 539–551.
mla: Chatterjee, Krishnendu, et al. “Quantitative Interprocedural Analysis.” Proceedings
of the 42nd Annual ACM SIGPLAN-SIGACT , vol. 50, no. 1, ACM, 2015, pp. 539–51,
doi:10.1145/2676726.2676968.
short: K. Chatterjee, A. Pavlogiannis, Y. Velner, Proceedings of the 42nd Annual
ACM SIGPLAN-SIGACT 50 (2015) 539–551.
conference:
end_date: 2015-01-17
location: Mumbai, India
name: 'SIGPLAN: Symposium on Principles of Programming Languages'
start_date: 2015-01-15
corr_author: '1'
date_created: 2018-12-11T11:52:59Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2026-04-08T14:22:16Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2676726.2676968
ec_funded: 1
intvolume: ' 50'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 539 - 551
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'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 'Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT '
publication_identifier:
isbn:
- 978-1-4503-3300-9
publication_status: published
publisher: ACM
publist_id: '5563'
pubrep_id: '523'
quality_controlled: '1'
related_material:
record:
- id: '5445'
relation: earlier_version
status: public
- id: '821'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Quantitative interprocedural analysis
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 50
year: '2015'
...
---
_id: '1607'
abstract:
- lang: eng
text: We consider the core algorithmic problems related to verification of systems
with respect to three classical quantitative properties, namely, the mean-payoff
property, the ratio property, and the minimum initial credit for energy property.
The algorithmic problem given a graph and a quantitative property asks to compute
the optimal value (the infimum value over all traces) from every node of the graph.
We consider graphs with constant treewidth, and it is well-known that the control-flow
graphs of most programs have constant treewidth. Let n denote the number of nodes
of a graph, m the number of edges (for constant treewidth graphs m=O(n)) and W
the largest absolute value of the weights. Our main theoretical results are as
follows. First, for constant treewidth graphs we present an algorithm that approximates
the mean-payoff value within a multiplicative factor of ϵ in time O(n⋅log(n/ϵ))
and linear space, as compared to the classical algorithms that require quadratic
time. Second, for the ratio property we present an algorithm that for constant
treewidth graphs works in time O(n⋅log(|a⋅b|))=O(n⋅log(n⋅W)), when the output
is ab, as compared to the previously best known algorithm with running time O(n2⋅log(n⋅W)).
Third, for the minimum initial credit problem we show that (i) for general graphs
the problem can be solved in O(n2⋅m) time and the associated decision problem
can be solved in O(n⋅m) time, improving the previous known O(n3⋅m⋅log(n⋅W)) and
O(n2⋅m) bounds, respectively; and (ii) for constant treewidth graphs we present
an algorithm that requires O(n⋅logn) time, improving the previous known O(n4⋅log(n⋅W))
bound. We have implemented some of our algorithms and show that they present a
significant speedup on standard benchmarks.
acknowledgement: 'The research was partly supported by 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.'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
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. Faster algorithms for quantitative
verification in constant treewidth graphs. In: Vol 9206. Springer; 2015:140-157.
doi:10.1007/978-3-319-21690-4_9'
apa: 'Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster algorithms
for quantitative verification in constant treewidth graphs (Vol. 9206, pp. 140–157).
Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States:
Springer. https://doi.org/10.1007/978-3-319-21690-4_9'
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
“Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs,”
9206:140–57. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_9.
ieee: 'K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for
quantitative verification in constant treewidth graphs,” presented at the CAV:
Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206,
pp. 140–157.'
ista: 'Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for
quantitative verification in constant treewidth graphs. CAV: Computer Aided Verification,
LNCS, vol. 9206, 140–157.'
mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification
in Constant Treewidth Graphs. Vol. 9206, Springer, 2015, pp. 140–57, doi:10.1007/978-3-319-21690-4_9.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Springer, 2015, pp.
140–157.
conference:
end_date: 2015-07-24
location: San Francisco, CA, United States
name: 'CAV: Computer Aided Verification'
start_date: 2015-07-18
corr_author: '1'
date_created: 2018-12-11T11:52:59Z
date_published: 2015-07-16T00:00:00Z
date_updated: 2026-04-08T14:22:16Z
day: '16'
department:
- _id: KrCh
doi: 10.1007/978-3-319-21690-4_9
ec_funded: 1
external_id:
arxiv:
- '1504.07384'
isi:
- '000364182900009'
intvolume: ' 9206'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1504.07384
month: '07'
oa: 1
oa_version: Preprint
page: 140 - 157
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_status: published
publisher: Springer
publist_id: '5560'
quality_controlled: '1'
related_material:
record:
- id: '5430'
relation: earlier_version
status: public
- id: '5437'
relation: earlier_version
status: public
- id: '821'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Faster algorithms for quantitative verification in constant treewidth graphs
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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
arxiv: 1
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
corr_author: '1'
date_created: 2018-12-11T11:53:00Z
date_published: 2015-06-20T00:00:00Z
date_updated: 2025-09-23T13:48:35Z
day: '20'
department:
- _id: KrCh
doi: 10.1007/978-3-662-47666-6_9
ec_funded: 1
external_id:
arxiv:
- '1502.04844'
isi:
- '000364317900009'
intvolume: ' 9135'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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'
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: 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).
corr_author: '1'
date_created: 2018-12-11T11:53:06Z
date_published: 2015-11-25T00:00:00Z
date_updated: 2025-09-23T08:13:52Z
day: '25'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/srep17147
ec_funded: 1
external_id:
isi:
- '000365299500001'
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'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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
article_processing_charge: No
arxiv: 1
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: 2025-09-23T09:27:49Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/LICS.2015.15
ec_funded: 1
external_id:
arxiv:
- '1505.02655'
isi:
- '000380427100007'
isi: 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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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: 2025-09-23T09:37:33Z
day: '22'
department:
- _id: KrCh
doi: 10.1038/nature15395
ec_funded: 1
external_id:
isi:
- '000364026100040'
pmid:
- '26466571'
intvolume: ' 526'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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
article_processing_charge: No
arxiv: 1
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: 2025-09-23T09:46:46Z
day: '22'
department:
- _id: KrCh
doi: 10.1007/978-3-319-22264-6_10
ec_funded: 1
external_id:
arxiv:
- '1407.4777'
isi:
- '000363574600012'
intvolume: ' 9259'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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'
article_processing_charge: No
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: 2025-09-23T07:46:22Z
day: '08'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1098/rspa.2015.0114
ec_funded: 1
external_id:
isi:
- '000363482200005'
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'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 471
year: '2015'
...
---
_id: '1681'
abstract:
- lang: eng
text: In many social situations, individuals endeavor to find the single best possible
partner, but are constrained to evaluate the candidates in sequence. Examples
include the search for mates, economic partnerships, or any other long-term ties
where the choice to interact involves two parties. Surprisingly, however, previous
theoretical work on mutual choice problems focuses on finding equilibrium solutions,
while ignoring the evolutionary dynamics of decisions. Empirically, this may be
of high importance, as some equilibrium solutions can never be reached unless
the population undergoes radical changes and a sufficient number of individuals
change their decisions simultaneously. To address this question, we apply a mutual
choice sequential search problem in an evolutionary game-theoretical model that
allows one to find solutions that are favored by evolution. As an example, we
study the influence of sequential search on the evolutionary dynamics of cooperation.
For this, we focus on the classic snowdrift game and the prisoner’s dilemma game.
article_processing_charge: No
article_type: original
author:
- first_name: Tadeas
full_name: Priklopil, Tadeas
id: 3C869AA0-F248-11E8-B48F-1D18A9856A87
last_name: Priklopil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Priklopil T, Chatterjee K. Evolution of decisions in population games with
sequentially searching individuals. Games. 2015;6(4):413-437. doi:10.3390/g6040413
apa: Priklopil, T., & Chatterjee, K. (2015). Evolution of decisions in population
games with sequentially searching individuals. Games. MDPI. https://doi.org/10.3390/g6040413
chicago: Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in
Population Games with Sequentially Searching Individuals.” Games. MDPI,
2015. https://doi.org/10.3390/g6040413.
ieee: T. Priklopil and K. Chatterjee, “Evolution of decisions in population games
with sequentially searching individuals,” Games, vol. 6, no. 4. MDPI, pp.
413–437, 2015.
ista: Priklopil T, Chatterjee K. 2015. Evolution of decisions in population games
with sequentially searching individuals. Games. 6(4), 413–437.
mla: Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population
Games with Sequentially Searching Individuals.” Games, vol. 6, no. 4, MDPI,
2015, pp. 413–37, doi:10.3390/g6040413.
short: T. Priklopil, K. Chatterjee, Games 6 (2015) 413–437.
corr_author: '1'
date_created: 2018-12-11T11:53:26Z
date_published: 2015-09-29T00:00:00Z
date_updated: 2025-04-15T06:50:21Z
day: '29'
ddc:
- '000'
department:
- _id: NiBa
- _id: KrCh
doi: 10.3390/g6040413
ec_funded: 1
file:
- access_level: open_access
checksum: 912e1acbaf201100f447a43e4d5958bd
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:41Z
date_updated: 2020-07-14T12:45:12Z
file_id: '4959'
file_name: IST-2016-448-v1+1_games-06-00413.pdf
file_size: 518832
relation: main_file
file_date_updated: 2020-07-14T12:45:12Z
has_accepted_license: '1'
intvolume: ' 6'
issue: '4'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 413 - 437
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: Games
publication_identifier:
eissn:
- 2073-4336
publication_status: published
publisher: MDPI
publist_id: '5467'
pubrep_id: '448'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Evolution of decisions in population games with sequentially searching individuals
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: 6
year: '2015'
...