---
_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
license: https://creativecommons.org/licenses/by/4.0/
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'
...
---
_id: '1689'
abstract:
- lang: eng
text: We consider the problem of computing the set of initial states of a dynamical
system such that there exists a control strategy to ensure that the trajectories
satisfy a temporal logic specification with probability 1 (almost-surely). We
focus on discrete-time, stochastic linear dynamics and specifications given as
formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over
linear predicates in the states of the system. We propose a solution based on
iterative abstraction-refinement, and turn-based 2-player probabilistic games.
While the theoretical guarantee of our algorithm after any finite number of iterations
is only a partial solution, we show that if our algorithm terminates, then the
result is the set of satisfying initial states. Moreover, for any (partial) solution
our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction
of the temporal logic specification. We demonstrate our approach on an illustrative
case study.
article_processing_charge: No
arxiv: 1
author:
- first_name: Mária
full_name: Svoreňová, Mária
last_name: Svoreňová
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ivana
full_name: Cěrná, Ivana
last_name: Cěrná
- first_name: Cǎlin
full_name: Belta, Cǎlin
last_name: Belta
citation:
ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal
logic control for stochastic linear systems using abstraction refinement of probabilistic
games. In: Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control. ACM; 2015:259-268. doi:10.1145/2728606.2728608'
apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &
Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction
refinement of probabilistic games. In Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control (pp. 259–268). Seattle,
WA, United States: ACM. https://doi.org/10.1145/2728606.2728608'
chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee,
Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” In Proceedings of the
18th International Conference on Hybrid Systems: Computation and Control,
259–68. ACM, 2015. https://doi.org/10.1145/2728606.2728608.'
ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta,
“Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games,” in Proceedings of the 18th International Conference
on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015,
pp. 259–268.'
ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015.
Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games. Proceedings of the 18th International Conference on Hybrid
Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control,
259–268.'
mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” Proceedings of the 18th
International Conference on Hybrid Systems: Computation and Control, ACM,
2015, pp. 259–68, doi:10.1145/2728606.2728608.'
short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta,
in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation
and Control, ACM, 2015, pp. 259–268.'
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:29Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2025-06-11T06:33:00Z
day: '14'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2728606.2728608
ec_funded: 1
external_id:
arxiv:
- '1410.5387'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1410.5387
month: '04'
oa: 1
oa_version: Preprint
page: 259 - 268
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: 'Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control'
publication_status: published
publisher: ACM
publist_id: '5456'
related_material:
record:
- id: '1407'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1691'
abstract:
- lang: eng
text: We consider a case study of the problem of deploying an autonomous air vehicle
in a partially observable, dynamic, indoor environment from a specification given
as a linear temporal logic (LTL) formula over regions of interest. We model the
motion and sensing capabilities of the vehicle as a partially observable Markov
decision process (POMDP). We adapt recent results for solving POMDPs with parity
objectives to generate a control policy. We also extend the existing framework
with a policy minimization technique to obtain a better implementable policy,
while preserving its correctness. The proposed techniques are illustrated in an
experimental setup involving an autonomous quadrotor performing surveillance in
a dynamic environment.
author:
- first_name: Mária
full_name: Svoreňová, Mária
last_name: Svoreňová
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Kevin
full_name: Leahy, Kevin
last_name: Leahy
- first_name: Hasan
full_name: Eniser, Hasan
last_name: Eniser
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ivana
full_name: Cěrná, Ivana
last_name: Cěrná
- first_name: Cǎlin
full_name: Belta, Cǎlin
last_name: Belta
citation:
ama: 'Svoreňová M, Chmelik M, Leahy K, et al. Temporal logic motion planning using
POMDPs with parity objectives: Case study paper. In: Proceedings of the 18th
International Conference on Hybrid Systems: Computation and Control. ACM;
2015:233-238. doi:10.1145/2728606.2728617'
apa: 'Svoreňová, M., Chmelik, M., Leahy, K., Eniser, H., Chatterjee, K., Cěrná,
I., & Belta, C. (2015). Temporal logic motion planning using POMDPs with parity
objectives: Case study paper. In Proceedings of the 18th International Conference
on Hybrid Systems: Computation and Control (pp. 233–238). Seattle, WA, United
States: ACM. https://doi.org/10.1145/2728606.2728617'
chicago: 'Svoreňová, Mária, Martin Chmelik, Kevin Leahy, Hasan Eniser, Krishnendu
Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Motion Planning Using
POMDPs with Parity Objectives: Case Study Paper.” In Proceedings of the 18th
International Conference on Hybrid Systems: Computation and Control, 233–38.
ACM, 2015. https://doi.org/10.1145/2728606.2728617.'
ieee: 'M. Svoreňová et al., “Temporal logic motion planning using POMDPs
with parity objectives: Case study paper,” in Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control, Seattle, WA, United
States, 2015, pp. 233–238.'
ista: 'Svoreňová M, Chmelik M, Leahy K, Eniser H, Chatterjee K, Cěrná I, Belta C.
2015. Temporal logic motion planning using POMDPs with parity objectives: Case
study paper. Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control. HSCC: Hybrid Systems - Computation and Control, 233–238.'
mla: 'Svoreňová, Mária, et al. “Temporal Logic Motion Planning Using POMDPs with
Parity Objectives: Case Study Paper.” Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 233–38,
doi:10.1145/2728606.2728617.'
short: 'M. Svoreňová, M. Chmelik, K. Leahy, H. Eniser, K. Chatterjee, I. Cěrná,
C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control, ACM, 2015, pp. 233–238.'
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:29Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2021-01-12T06:52:33Z
day: '14'
department:
- _id: KrCh
doi: 10.1145/2728606.2728617
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 233 - 238
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: 'Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control'
publication_status: published
publisher: ACM
publist_id: '5453'
scopus_import: 1
status: public
title: 'Temporal logic motion planning using POMDPs with parity objectives: Case study
paper'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1694'
abstract:
- lang: eng
text: "We introduce quantitative timed refinement and timed simulation (directed)
metrics, incorporating zenoness checks, for timed systems. These metrics assign
positive real numbers which quantify the timing mismatches between two timed systems,
amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal
timing mismatch that can arise, (2) the “steady-state” maximal timing mismatches,
where initial transient timing mismatches are ignored; and (3) the (long-run)
average timing mismatches amongst two systems. These three kinds of mismatches
constitute three important types of timing differences. Our event times are the
global times, measured from the start of the system execution, not just the time
durations of individual steps. We present algorithms over timed automata for computing
the three quantitative simulation distances to within any desired degree of accuracy.
In order to compute the values of the quantitative simulation distances, we use
a game theoretic formulation. We introduce two new kinds of objectives for two
player games on finite-state game graphs: (1) eventual debit-sum level objectives,
and (2) average debit-sum level objectives. We present algorithms for computing
the optimal values for these objectives in graph games, and then use these algorithms
to compute the values of the timed simulation distances over timed automata.\r\n"
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: Chatterjee K, Prabhu V. Quantitative temporal simulation and refinement distances
for timed systems. IEEE Transactions on Automatic Control. 2015;60(9):2291-2306.
doi:10.1109/TAC.2015.2404612
apa: Chatterjee, K., & Prabhu, V. (2015). Quantitative temporal simulation and
refinement distances for timed systems. IEEE Transactions on Automatic Control.
IEEE. https://doi.org/10.1109/TAC.2015.2404612
chicago: Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation
and Refinement Distances for Timed Systems.” IEEE Transactions on Automatic
Control. IEEE, 2015. https://doi.org/10.1109/TAC.2015.2404612.
ieee: K. Chatterjee and V. Prabhu, “Quantitative temporal simulation and refinement
distances for timed systems,” IEEE Transactions on Automatic Control, vol.
60, no. 9. IEEE, pp. 2291–2306, 2015.
ista: Chatterjee K, Prabhu V. 2015. Quantitative temporal simulation and refinement
distances for timed systems. IEEE Transactions on Automatic Control. 60(9), 2291–2306.
mla: Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation
and Refinement Distances for Timed Systems.” IEEE Transactions on Automatic
Control, vol. 60, no. 9, IEEE, 2015, pp. 2291–306, doi:10.1109/TAC.2015.2404612.
short: K. Chatterjee, V. Prabhu, IEEE Transactions on Automatic Control 60 (2015)
2291–2306.
date_created: 2018-12-11T11:53:30Z
date_published: 2015-02-24T00:00:00Z
date_updated: 2025-09-23T10:00:03Z
day: '24'
department:
- _id: KrCh
doi: 10.1109/TAC.2015.2404612
ec_funded: 1
external_id:
isi:
- '000360501800001'
intvolume: ' 60'
isi: 1
issue: '9'
language:
- iso: eng
month: '02'
oa_version: None
page: 2291 - 2306
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: IEEE Transactions on Automatic Control
publication_status: published
publisher: IEEE
publist_id: '5450'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative temporal simulation and refinement distances for timed systems
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 60
year: '2015'
...
---
_id: '1698'
abstract:
- lang: eng
text: 'In mean-payoff games, the objective of the protagonist is to ensure that
the limit average of an infinite sequence of numeric weights is nonnegative. In
energy games, the objective is to ensure that the running sum of weights is always
nonnegative. Multi-mean-payoff and multi-energy games replace individual weights
by tuples, and the limit average (resp., running sum) of each coordinate must
be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy
games and show inter-reducibility of multi-mean-payoff and multi-energy games
for finite-memory strategies. We improve the computational complexity for solving
both classes with finite-memory strategies: we prove coNP-completeness improving
the previous known EXPSPACE bound. For memoryless strategies, we show that deciding
the existence of a winning strategy for the protagonist is NP-complete. We present
the first solution of multi-mean-payoff games with infinite-memory strategies:
we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf
objectives are coNP-complete.'
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499-N23, FWF NFN Grant No S11407-N23 and S11402-N23 (RiSE), ERC Start
grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant
QUAREM (267989: Quantitative Reactive Modeling), European project Cassting (FP7-601148),
ERC Start grant (279499: inVEST).'
article_processing_charge: No
arxiv: 1
author:
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Alexander
full_name: Rabinovich, Alexander
last_name: Rabinovich
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The
complexity of multi-mean-payoff and multi-energy games. Information and Computation.
2015;241(4):177-196. doi:10.1016/j.ic.2015.03.001
apa: Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., &
Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games.
Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2015.03.001
chicago: Velner, Yaron, Krishnendu Chatterjee, Laurent Doyen, Thomas A Henzinger,
Alexander Rabinovich, and Jean Raskin. “The Complexity of Multi-Mean-Payoff and
Multi-Energy Games.” Information and Computation. Elsevier, 2015. https://doi.org/10.1016/j.ic.2015.03.001.
ieee: Y. Velner, K. Chatterjee, L. Doyen, T. A. Henzinger, A. Rabinovich, and J.
Raskin, “The complexity of multi-mean-payoff and multi-energy games,” Information
and Computation, vol. 241, no. 4. Elsevier, pp. 177–196, 2015.
ista: Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. 2015.
The complexity of multi-mean-payoff and multi-energy games. Information and Computation.
241(4), 177–196.
mla: Velner, Yaron, et al. “The Complexity of Multi-Mean-Payoff and Multi-Energy
Games.” Information and Computation, vol. 241, no. 4, Elsevier, 2015, pp.
177–96, doi:10.1016/j.ic.2015.03.001.
short: Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin,
Information and Computation 241 (2015) 177–196.
corr_author: '1'
date_created: 2018-12-11T11:53:32Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2025-09-23T13:47:20Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2015.03.001
ec_funded: 1
external_id:
arxiv:
- '1209.3234'
isi:
- '000353352800008'
intvolume: ' 241'
isi: 1
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1209.3234
month: '04'
oa: 1
oa_version: Preprint
page: 177 - 196
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '5443'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The complexity of multi-mean-payoff and multi-energy games
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 241
year: '2015'
...
---
_id: '1714'
abstract:
- lang: eng
text: 'We present a flexible framework for the automated competitive analysis of
on-line scheduling algorithms for firm-deadline real-time tasks based on multi-objective
graphs: Given a task set and an on-line scheduling algorithm specified as a labeled
transition system, along with some optional safety, liveness, and/or limit-average
constraints for the adversary, we automatically compute the competitive ratio
of the algorithm w.r.t. A clairvoyant scheduler. We demonstrate the flexibility
and power of our approach by comparing the competitive ratio of several on-line
algorithms, including Dover, that have been proposed in the past, for various
task sets. Our experimental results reveal that none of these algorithms is universally
optimal, in the sense that there are task sets where other schedulers provide
better performance. Our framework is hence a very useful design tool for selecting
optimal algorithms for a given application.'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Alexander
full_name: Kößler, Alexander
last_name: Kößler
- first_name: Ulrich
full_name: Schmid, Ulrich
last_name: Schmid
citation:
ama: 'Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. A framework for automated
competitive analysis of on-line scheduling of firm-deadline tasks. In: Real-Time
Systems Symposium. Vol 2015. IEEE; 2015:118-127. doi:10.1109/RTSS.2014.9'
apa: 'Chatterjee, K., Pavlogiannis, A., Kößler, A., & Schmid, U. (2015). A framework
for automated competitive analysis of on-line scheduling of firm-deadline tasks.
In Real-Time Systems Symposium (Vol. 2015, pp. 118–127). Rome, Italy: IEEE.
https://doi.org/10.1109/RTSS.2014.9'
chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich
Schmid. “A Framework for Automated Competitive Analysis of On-Line Scheduling
of Firm-Deadline Tasks.” In Real-Time Systems Symposium, 2015:118–27. IEEE,
2015. https://doi.org/10.1109/RTSS.2014.9.
ieee: K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “A framework for
automated competitive analysis of on-line scheduling of firm-deadline tasks,”
in Real-Time Systems Symposium, Rome, Italy, 2015, vol. 2015, no. January,
pp. 118–127.
ista: 'Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2015. A framework for automated
competitive analysis of on-line scheduling of firm-deadline tasks. Real-Time Systems
Symposium. RTSS: Real-Time Systems Symposium vol. 2015, 118–127.'
mla: Chatterjee, Krishnendu, et al. “A Framework for Automated Competitive Analysis
of On-Line Scheduling of Firm-Deadline Tasks.” Real-Time Systems Symposium,
vol. 2015, no. January, IEEE, 2015, pp. 118–27, doi:10.1109/RTSS.2014.9.
short: K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, in:, Real-Time Systems
Symposium, IEEE, 2015, pp. 118–127.
conference:
end_date: 2014-12-05
location: Rome, Italy
name: 'RTSS: Real-Time Systems Symposium'
start_date: 2014-12-02
date_created: 2018-12-11T11:53:37Z
date_published: 2015-01-15T00:00:00Z
date_updated: 2026-04-08T14:22:16Z
day: '15'
department:
- _id: KrCh
doi: 10.1109/RTSS.2014.9
external_id:
isi:
- '000569750000012'
intvolume: ' 2015'
isi: 1
issue: January
language:
- iso: eng
month: '01'
oa_version: None
page: 118 - 127
publication: Real-Time Systems Symposium
publication_status: published
publisher: IEEE
publist_id: '5417'
quality_controlled: '1'
related_material:
record:
- id: '5423'
relation: earlier_version
status: public
- id: '821'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: A framework for automated competitive analysis of on-line scheduling of firm-deadline
tasks
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 2015
year: '2015'
...
---
_id: '1846'
abstract:
- lang: eng
text: Modal transition systems (MTS) is a well-studied specification formalism of
reactive systems supporting a step-wise refinement methodology. Despite its many
advantages, the formalism as well as its currently known extensions are incapable
of expressing some practically needed aspects in the refinement process like exclusive,
conditional and persistent choices. We introduce a new model called parametric
modal transition systems (PMTS) together with a general modal refinement notion
that overcomes many of the limitations. We investigate the computational complexity
of modal and thorough refinement checking on PMTS and its subclasses and provide
a direct encoding of the modal refinement problem into quantified Boolean formulae,
allowing us to employ state-of-the-art QBF solvers for modal refinement checking.
The experiments we report on show that the feasibility of refinement checking
is more influenced by the degree of nondeterminism rather than by the syntactic
restrictions on the types of formulae allowed in the description of the PMTS.
article_processing_charge: No
article_type: original
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Kim
full_name: Larsen, Kim
last_name: Larsen
- first_name: Mikael
full_name: Möller, Mikael
last_name: Möller
- first_name: Salomon
full_name: Sickert, Salomon
last_name: Sickert
- first_name: Jiří
full_name: Srba, Jiří
last_name: Srba
citation:
ama: Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking
on parametric modal transition systems. Acta Informatica. 2015;52(2-3):269-297.
doi:10.1007/s00236-015-0215-4
apa: Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., & Srba,
J. (2015). Refinement checking on parametric modal transition systems. Acta
Informatica. Springer. https://doi.org/10.1007/s00236-015-0215-4
chicago: Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert,
and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” Acta
Informatica. Springer, 2015. https://doi.org/10.1007/s00236-015-0215-4.
ieee: N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement
checking on parametric modal transition systems,” Acta Informatica, vol.
52, no. 2–3. Springer, pp. 269–297, 2015.
ista: Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement
checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.
mla: Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.”
Acta Informatica, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:10.1007/s00236-015-0215-4.
short: N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica
52 (2015) 269–297.
corr_author: '1'
date_created: 2018-12-11T11:54:20Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2025-09-23T10:33:12Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/s00236-015-0215-4
ec_funded: 1
external_id:
isi:
- '000351160200008'
file:
- access_level: open_access
checksum: fb4037ddc4fc05f33080dd3547ede350
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:57:44Z
date_updated: 2020-07-14T12:45:19Z
file_id: '7854'
file_name: 2015_ActaInfo_Benes.pdf
file_size: 488482
relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: ' 52'
isi: 1
issue: 2-3
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 269 - 297
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Acta Informatica
publication_status: published
publisher: Springer
publist_id: '5255'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Refinement checking on parametric modal transition systems
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 52
year: '2015'
...
---
_id: '1851'
abstract:
- lang: eng
text: We consider mating strategies for females who search for males sequentially
during a season of limited length. We show that the best strategy rejects a given
male type if encountered before a time-threshold but accepts him after. For frequency-independent
benefits, we obtain the optimal time-thresholds explicitly for both discrete and
continuous distributions of males, and allow for mistakes being made in assessing
the correct male type. When the benefits are indirect (genes for the offspring)
and the population is under frequency-dependent ecological selection, the benefits
depend on the mating strategy of other females as well. This case is particularly
relevant to speciation models that seek to explore the stability of reproductive
isolation by assortative mating under frequency-dependent ecological selection.
We show that the indirect benefits are to be quantified by the reproductive values
of couples, and describe how the evolutionarily stable time-thresholds can be
found. We conclude with an example based on the Levene model, in which we analyze
the evolutionarily stable assortative mating strategies and the strength of reproductive
isolation provided by them.
article_processing_charge: No
article_type: original
author:
- first_name: Tadeas
full_name: Priklopil, Tadeas
id: 3C869AA0-F248-11E8-B48F-1D18A9856A87
last_name: Priklopil
- first_name: Eva
full_name: Kisdi, Eva
last_name: Kisdi
- first_name: Mats
full_name: Gyllenberg, Mats
last_name: Gyllenberg
citation:
ama: Priklopil T, Kisdi E, Gyllenberg M. Evolutionarily stable mating decisions
for sequentially searching females and the stability of reproductive isolation
by assortative mating. Evolution. 2015;69(4):1015-1026. doi:10.1111/evo.12618
apa: Priklopil, T., Kisdi, E., & Gyllenberg, M. (2015). Evolutionarily stable
mating decisions for sequentially searching females and the stability of reproductive
isolation by assortative mating. Evolution. Wiley. https://doi.org/10.1111/evo.12618
chicago: Priklopil, Tadeas, Eva Kisdi, and Mats Gyllenberg. “Evolutionarily Stable
Mating Decisions for Sequentially Searching Females and the Stability of Reproductive
Isolation by Assortative Mating.” Evolution. Wiley, 2015. https://doi.org/10.1111/evo.12618.
ieee: T. Priklopil, E. Kisdi, and M. Gyllenberg, “Evolutionarily stable mating decisions
for sequentially searching females and the stability of reproductive isolation
by assortative mating,” Evolution, vol. 69, no. 4. Wiley, pp. 1015–1026,
2015.
ista: Priklopil T, Kisdi E, Gyllenberg M. 2015. Evolutionarily stable mating decisions
for sequentially searching females and the stability of reproductive isolation
by assortative mating. Evolution. 69(4), 1015–1026.
mla: Priklopil, Tadeas, et al. “Evolutionarily Stable Mating Decisions for Sequentially
Searching Females and the Stability of Reproductive Isolation by Assortative Mating.”
Evolution, vol. 69, no. 4, Wiley, 2015, pp. 1015–26, doi:10.1111/evo.12618.
short: T. Priklopil, E. Kisdi, M. Gyllenberg, Evolution 69 (2015) 1015–1026.
corr_author: '1'
date_created: 2018-12-11T11:54:21Z
date_published: 2015-02-09T00:00:00Z
date_updated: 2025-09-22T14:27:30Z
day: '09'
ddc:
- '570'
department:
- _id: NiBa
- _id: KrCh
doi: 10.1111/evo.12618
ec_funded: 1
external_id:
isi:
- '000353236000014'
pmid:
- '25662095'
file:
- access_level: open_access
checksum: 1e8be0b1d7598a78cd2623d8ee8e7798
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T09:05:34Z
date_updated: 2020-07-14T12:45:19Z
file_id: '7855'
file_name: 2015_Evolution_Priklopil.pdf
file_size: 967214
relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: ' 69'
isi: 1
issue: '4'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Submitted Version
page: 1015 - 1026
pmid: 1
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: Evolution
publication_identifier:
eissn:
- 1558-5646
issn:
- 0014-3820
publication_status: published
publisher: Wiley
publist_id: '5249'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Evolutionarily stable mating decisions for sequentially searching females and
the stability of reproductive isolation by assortative mating
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 69
year: '2015'
...
---
_id: '1856'
abstract:
- lang: eng
text: 'The traditional synthesis question given a specification asks for the automatic
construction of a system that satisfies the specification, whereas often there
exists a preference order among the different systems that satisfy the given specification.
Under a probabilistic assumption about the possible inputs, such a preference
order is naturally expressed by a weighted automaton, which assigns to each word
a value, such that a system is preferred if it generates a higher expected value.
We solve the following optimal synthesis problem: given an omega-regular specification,
a Markov chain that describes the distribution of inputs, and a weighted automaton
that measures how well a system satisfies the given specification under the input
assumption, synthesize a system that optimizes the measured value. For safety
specifications and quantitative measures that are defined by mean-payoff automata,
the optimal synthesis problem reduces to finding a strategy in a Markov decision
process (MDP) that is optimal for a long-run average reward objective, which can
be achieved in polynomial time. For general omega-regular specifications along
with mean-payoff automata, the solution rests on a new, polynomial-time algorithm
for computing optimal strategies in MDPs with mean-payoff parity objectives. Our
algorithm constructs optimal strategies that consist of two memoryless strategies
and a counter. The counter is in general not bounded. To obtain a finite-state
system, we show how to construct an ε-optimal strategy with a bounded counter,
for all ε > 0. Furthermore, we show how to decide in polynomial time if it
is possible to construct an optimal finite-state system (i.e., a system without
a counter) for a given specification. We have implemented our approach and the
underlying algorithms in a tool that takes qualitative and quantitative specifications
and automatically constructs a system that satisfies the qualitative specification
and optimizes the quantitative specification, if such a system exists. We present
some experimental results showing optimal systems that were automatically generated
in this way.'
article_number: '9'
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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Rohit
full_name: Singh, Rohit
last_name: Singh
citation:
ama: Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing
systems in probabilistic environments. Journal of the ACM. 2015;62(1).
doi:10.1145/2699430
apa: Chatterjee, K., Henzinger, T. A., Jobstmann, B., & Singh, R. (2015). Measuring
and synthesizing systems in probabilistic environments. Journal of the ACM.
ACM. https://doi.org/10.1145/2699430
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit
Singh. “Measuring and Synthesizing Systems in Probabilistic Environments.” Journal
of the ACM. ACM, 2015. https://doi.org/10.1145/2699430.
ieee: K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and
synthesizing systems in probabilistic environments,” Journal of the ACM,
vol. 62, no. 1. ACM, 2015.
ista: Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2015. Measuring and synthesizing
systems in probabilistic environments. Journal of the ACM. 62(1), 9.
mla: Chatterjee, Krishnendu, et al. “Measuring and Synthesizing Systems in Probabilistic
Environments.” Journal of the ACM, vol. 62, no. 1, 9, ACM, 2015, doi:10.1145/2699430.
short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, Journal of the ACM
62 (2015).
date_created: 2018-12-11T11:54:23Z
date_published: 2015-02-01T00:00:00Z
date_updated: 2025-09-23T09:33:01Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/2699430
ec_funded: 1
external_id:
arxiv:
- '1004.0739'
isi:
- '000350563000009'
intvolume: ' 62'
isi: 1
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1004.0739
month: '02'
oa: 1
oa_version: Preprint
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: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Journal of the ACM
publication_status: published
publisher: ACM
publist_id: '5244'
quality_controlled: '1'
related_material:
record:
- id: '3864'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Measuring and synthesizing systems in probabilistic environments
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 62
year: '2015'
...
---
_id: '1873'
abstract:
- lang: eng
text: 'We consider partially observable Markov decision processes (POMDPs) with
limit-average payoff, where a reward value in the interval [0,1] is associated
with every transition, and the payoff of an infinite path is the long-run average
of the rewards. We consider two types of path constraints: (i) a quantitative
constraint defines the set of paths where the payoff is at least a given threshold
λ1ε(0,1]; and (ii) a qualitative constraint which is a special case of the quantitative
constraint with λ1=1. We consider the computation of the almost-sure winning set,
where the controller needs to ensure that the path constraint is satisfied with
probability 1. Our main results for qualitative path constraints are as follows:
(i) the problem of deciding the existence of a finite-memory controller is EXPTIME-complete;
and (ii) the problem of deciding the existence of an infinite-memory controller
is undecidable. For quantitative path constraints we show that the problem of
deciding the existence of a finite-memory controller is undecidable. We also present
a prototype implementation of our EXPTIME algorithm and experimental results on
several examples.'
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
citation:
ama: Chatterjee K, Chmelik M. POMDPs under probabilistic semantics. Artificial
Intelligence. 2015;221:46-72. doi:10.1016/j.artint.2014.12.009
apa: Chatterjee, K., & Chmelik, M. (2015). POMDPs under probabilistic semantics.
Artificial Intelligence. Elsevier. https://doi.org/10.1016/j.artint.2014.12.009
chicago: Chatterjee, Krishnendu, and Martin Chmelik. “POMDPs under Probabilistic
Semantics.” Artificial Intelligence. Elsevier, 2015. https://doi.org/10.1016/j.artint.2014.12.009.
ieee: K. Chatterjee and M. Chmelik, “POMDPs under probabilistic semantics,” Artificial
Intelligence, vol. 221. Elsevier, pp. 46–72, 2015.
ista: Chatterjee K, Chmelik M. 2015. POMDPs under probabilistic semantics. Artificial
Intelligence. 221, 46–72.
mla: Chatterjee, Krishnendu, and Martin Chmelik. “POMDPs under Probabilistic Semantics.”
Artificial Intelligence, vol. 221, Elsevier, 2015, pp. 46–72, doi:10.1016/j.artint.2014.12.009.
short: K. Chatterjee, M. Chmelik, Artificial Intelligence 221 (2015) 46–72.
corr_author: '1'
date_created: 2018-12-11T11:54:28Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2025-09-23T09:52:31Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.artint.2014.12.009
external_id:
arxiv:
- '1408.2058'
isi:
- '000350782300003'
intvolume: ' 221'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1408.2058
month: '04'
oa: 1
oa_version: Preprint
page: 46 - 72
publication: Artificial Intelligence
publication_status: published
publisher: Elsevier
publist_id: '5224'
quality_controlled: '1'
scopus_import: '1'
status: public
title: POMDPs under probabilistic semantics
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 221
year: '2015'
...
---
_id: '1882'
abstract:
- lang: eng
text: We provide a framework for compositional and iterative design and verification
of systems with quantitative information, such as rewards, time or energy. It
is based on disjunctive modal transition systems where we allow actions to bear
various types of quantitative information. Throughout the design process the actions
can be further refined and the information made more precise. We show how to compute
the results of standard operations on the systems, including the quotient (residual),
which has not been previously considered for quantitative non-deterministic systems.
Our quantitative framework has close connections to the modal nu-calculus and
is compositional with respect to general notions of distances between systems
and the standard operations.
acknowledgement: This research was funded in part by the European Research Council
(ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF)
project S11402-N23 (RiSE), and by the Czech Science Foundation, grant No. P202/12/G061.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Uli
full_name: Fahrenberg, Uli
last_name: Fahrenberg
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Axel
full_name: Legay, Axel
last_name: Legay
- first_name: Louis
full_name: Traonouez, Louis
last_name: Traonouez
citation:
ama: 'Fahrenberg U, Kretinsky J, Legay A, Traonouez L. Compositionality for quantitative
specifications. In: Vol 8997. Springer; 2015:306-324. doi:10.1007/978-3-319-15317-9_19'
apa: 'Fahrenberg, U., Kretinsky, J., Legay, A., & Traonouez, L. (2015). Compositionality
for quantitative specifications (Vol. 8997, pp. 306–324). Presented at the FACS:
Formal Aspects of Component Software, Bertinoro, Italy: Springer. https://doi.org/10.1007/978-3-319-15317-9_19'
chicago: Fahrenberg, Uli, Jan Kretinsky, Axel Legay, and Louis Traonouez. “Compositionality
for Quantitative Specifications,” 8997:306–24. Springer, 2015. https://doi.org/10.1007/978-3-319-15317-9_19.
ieee: 'U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality
for quantitative specifications,” presented at the FACS: Formal Aspects of Component
Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.'
ista: 'Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for
quantitative specifications. FACS: Formal Aspects of Component Software, LNCS,
vol. 8997, 306–324.'
mla: Fahrenberg, Uli, et al. Compositionality for Quantitative Specifications.
Vol. 8997, Springer, 2015, pp. 306–24, doi:10.1007/978-3-319-15317-9_19.
short: U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015,
pp. 306–324.
conference:
end_date: 2014-09-12
location: Bertinoro, Italy
name: 'FACS: Formal Aspects of Component Software'
start_date: 2014-09-10
corr_author: '1'
date_created: 2018-12-11T11:54:31Z
date_published: 2015-01-30T00:00:00Z
date_updated: 2025-06-11T07:22:00Z
day: '30'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-319-15317-9_19
ec_funded: 1
external_id:
arxiv:
- '1408.1256'
intvolume: ' 8997'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1408.1256
month: '01'
oa: 1
oa_version: Preprint
page: 306 - 324
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '5216'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Compositionality for quantitative specifications
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8997
year: '2015'
...
---
_id: '523'
abstract:
- lang: eng
text: We consider two-player games played on weighted directed graphs with mean-payoff
and total-payoff objectives, two classical quantitative objectives. While for
single-dimensional games the complexity and memory bounds for both objectives
coincide, we show that in contrast to multi-dimensional mean-payoff games that
are known to be coNP-complete, multi-dimensional total-payoff games are undecidable.
We introduce conservative approximations of these objectives, where the payoff
is considered over a local finite window sliding along a play, instead of the
whole play. For single dimension, we show that (i) if the window size is polynomial,
deciding the winner takes polynomial time, and (ii) the existence of a bounded
window can be decided in NP ∩ coNP, and is at least as hard as solving mean-payoff
games. For multiple dimensions, we show that (i) the problem with fixed window
size is EXPTIME-complete, and (ii) there is no primitive-recursive algorithm to
decide the existence of a bounded window.
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: Mickael
full_name: Randour, Mickael
last_name: Randour
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: Chatterjee K, Doyen L, Randour M, Raskin J. Looking at mean-payoff and total-payoff
through windows. Information and Computation. 2015;242(6):25-52. doi:10.1016/j.ic.2015.03.010
apa: Chatterjee, K., Doyen, L., Randour, M., & Raskin, J. (2015). Looking at
mean-payoff and total-payoff through windows. Information and Computation.
Elsevier. https://doi.org/10.1016/j.ic.2015.03.010
chicago: Chatterjee, Krishnendu, Laurent Doyen, Mickael Randour, and Jean Raskin.
“Looking at Mean-Payoff and Total-Payoff through Windows.” Information and
Computation. Elsevier, 2015. https://doi.org/10.1016/j.ic.2015.03.010.
ieee: K. Chatterjee, L. Doyen, M. Randour, and J. Raskin, “Looking at mean-payoff
and total-payoff through windows,” Information and Computation, vol. 242,
no. 6. Elsevier, pp. 25–52, 2015.
ista: Chatterjee K, Doyen L, Randour M, Raskin J. 2015. Looking at mean-payoff and
total-payoff through windows. Information and Computation. 242(6), 25–52.
mla: Chatterjee, Krishnendu, et al. “Looking at Mean-Payoff and Total-Payoff through
Windows.” Information and Computation, vol. 242, no. 6, Elsevier, 2015,
pp. 25–52, doi:10.1016/j.ic.2015.03.010.
short: K. Chatterjee, L. Doyen, M. Randour, J. Raskin, Information and Computation
242 (2015) 25–52.
date_created: 2018-12-11T11:46:57Z
date_published: 2015-03-24T00:00:00Z
date_updated: 2025-09-23T09:29:55Z
day: '24'
department:
- _id: KrCh
doi: 10.1016/j.ic.2015.03.010
ec_funded: 1
external_id:
arxiv:
- '1302.4248'
isi:
- '000355664900003'
intvolume: ' 242'
isi: 1
issue: '6'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1302.4248
month: '03'
oa: 1
oa_version: Preprint
page: 25 - 52
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: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '7296'
quality_controlled: '1'
related_material:
record:
- id: '2279'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Looking at mean-payoff and total-payoff through windows
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 242
year: '2015'
...
---
_id: '524'
abstract:
- lang: eng
text: 'We consider concurrent games played by two players on a finite-state graph,
where in every round the players simultaneously choose a move, and the current
state along with the joint moves determine the successor state. We study the most
fundamental objective for concurrent games, namely, mean-payoff or limit-average
objective, where a reward is associated to each transition, and the goal of player
1 is to maximize the long-run average of the rewards, and the objective of player
2 is strictly the opposite (i.e., the games are zero-sum). The path constraint
for player 1 could be qualitative, i.e., the mean-payoff is the maximal reward,
or arbitrarily close to it; or quantitative, i.e., a given threshold between the
minimal and maximal reward. We consider the computation of the almost-sure (resp.
positive) winning sets, where player 1 can ensure that the path constraint is
satisfied with probability 1 (resp. positive probability). Almost-sure winning
with qualitative constraint exactly corresponds to the question of whether there
exists a strategy to ensure that the payoff is the maximal reward of the game.
Our main results for qualitative path constraints are as follows: (1) we establish
qualitative determinacy results that show that for every state either player 1
has a strategy to ensure almost-sure (resp. positive) winning against all player-2
strategies, or player 2 has a spoiling strategy to falsify almost-sure (resp.
positive) winning against all player-1 strategies; (2) we present optimal strategy
complexity results that precisely characterize the classes of strategies required
for almost-sure and positive winning for both players; and (3) we present quadratic
time algorithms to compute the almost-sure and the positive winning sets, matching
the best known bound of the algorithms for much simpler problems (such as reachability
objectives). For quantitative constraints we show that a polynomial time solution
for the almost-sure or the positive winning set would imply a solution to a long-standing
open problem (of solving the value problem of turn-based deterministic mean-payoff
games) that is not known to be solvable in polynomial time.'
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
citation:
ama: Chatterjee K, Ibsen-Jensen R. Qualitative analysis of concurrent mean payoff
games. Information and Computation. 2015;242(6):2-24. doi:10.1016/j.ic.2015.03.009
apa: Chatterjee, K., & Ibsen-Jensen, R. (2015). Qualitative analysis of concurrent
mean payoff games. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2015.03.009
chicago: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “Qualitative Analysis
of Concurrent Mean Payoff Games.” Information and Computation. Elsevier,
2015. https://doi.org/10.1016/j.ic.2015.03.009.
ieee: K. Chatterjee and R. Ibsen-Jensen, “Qualitative analysis of concurrent mean
payoff games,” Information and Computation, vol. 242, no. 6. Elsevier,
pp. 2–24, 2015.
ista: Chatterjee K, Ibsen-Jensen R. 2015. Qualitative analysis of concurrent mean
payoff games. Information and Computation. 242(6), 2–24.
mla: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “Qualitative Analysis of Concurrent
Mean Payoff Games.” Information and Computation, vol. 242, no. 6, Elsevier,
2015, pp. 2–24, doi:10.1016/j.ic.2015.03.009.
short: K. Chatterjee, R. Ibsen-Jensen, Information and Computation 242 (2015) 2–24.
corr_author: '1'
date_created: 2018-12-11T11:46:57Z
date_published: 2015-10-11T00:00:00Z
date_updated: 2025-09-23T09:56:28Z
day: '11'
department:
- _id: KrCh
doi: 10.1016/j.ic.2015.03.009
external_id:
arxiv:
- '1409.5306'
isi:
- '000355664900002'
intvolume: ' 242'
isi: 1
issue: '6'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1409.5306
month: '10'
oa: 1
oa_version: Preprint
page: 2 - 24
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '7295'
quality_controlled: '1'
related_material:
record:
- id: '5403'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Qualitative analysis of concurrent mean payoff games
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 242
year: '2015'
...
---
_id: '5430'
abstract:
- lang: eng
text: We consider the core algorithmic problems related to verification of systems
with respect to three classical quantitative properties, namely, the mean- payoff
property, the ratio property, and the minimum initial credit for energy property.
The algorithmic problem given a graph and a quantitative property asks to compute
the optimal value (the infimum value over all traces) from every node of the graph.
We consider graphs with constant treewidth, and it is well-known that the control-flow
graphs of most programs have constant treewidth. Let n denote the number of nodes
of a graph, m the number of edges (for constant treewidth graphs m = O ( n ) )
and W the largest absolute value of the weights. Our main theoretical results
are as follows. First, for constant treewidth graphs we present an algorithm that
approximates the mean-payoff value within a mul- tiplicative factor of ∊ in time
O ( n · log( n/∊ )) and linear space, as compared to the classical algorithms
that require quadratic time. Second, for the ratio property we present an algorithm
that for constant treewidth graphs works in time O ( n · log( | a · b · n | ))
= O ( n · log( n · W )) , when the output is a b , as compared to the previously
best known algorithm with running time O ( n 2 · log( n · W )) . Third, for the
minimum initial credit problem we show that (i) for general graphs the problem
can be solved in O ( n 2 · m ) time and the associated decision problem can be
solved in O ( n · m ) time, improving the previous known O ( n 3 · m · log( n
· W )) and O ( n 2 · m ) bounds, respectively; and (ii) for constant treewidth
graphs we present an algorithm that requires O ( n · log n ) time, improving the
previous known O ( n 4 · log( n · W )) bound. We have implemented some of our
algorithms and show that they present a significant speedup on standard benchmarks.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
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. IST Austria; 2015. doi:10.15479/AT:IST-2015-319-v1-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster
algorithms for quantitative verification in constant treewidth graphs. IST
Austria. https://doi.org/10.15479/AT:IST-2015-319-v1-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-319-v1-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Faster algorithms
for quantitative verification in constant treewidth graphs. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for
quantitative verification in constant treewidth graphs, IST Austria, 31p.
mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification
in Constant Treewidth Graphs. IST Austria, 2015, doi:10.15479/AT:IST-2015-319-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative
Verification in Constant Treewidth Graphs, IST Austria, 2015.
date_created: 2018-12-12T11:39:17Z
date_published: 2015-02-10T00:00:00Z
date_updated: 2025-09-23T08:47:23Z
day: '10'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-319-v1-1
file:
- access_level: open_access
checksum: 62c6ea01e342553dcafb88a070fb1ad5
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:21Z
date_updated: 2020-07-14T12:46:52Z
file_id: '5482'
file_name: IST-2015-319-v1+1_long.pdf
file_size: 1089651
relation: main_file
file_date_updated: 2020-07-14T12:46:52Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '31'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '319'
related_material:
record:
- id: '5437'
relation: later_version
status: public
- id: '1607'
relation: later_version
status: public
status: public
title: Faster algorithms for quantitative verification in constant treewidth graphs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5431'
abstract:
- lang: eng
text: "We consider finite-state concurrent stochastic games, played by k>=2 players
for an infinite number of rounds, where in every round, each player simultaneously
and independently of the other players chooses an action, whereafter the successor
state is determined by a probability distribution given by the current state and
the chosen actions. We consider reachability objectives that given a target set
of states require that some state in the target set is visited, and the dual safety
objectives that given a target set require that only states in the target set
are visited. We are interested in the complexity of stationary strategies measured
by their patience, which is defined as the inverse of the smallest non-zero probability
employed.\r\n\r\n Our main results are as follows: We show that in two-player
zero-sum concurrent stochastic games (with reachability objective for one player
and the complementary safety objective for the other player): (i) the optimal
bound on the patience of optimal and epsilon-optimal strategies, for both players
is doubly exponential; and (ii) even in games with a single non-absorbing state
exponential (in the number of actions) patience is necessary. In general we study
the class of non-zero-sum games admitting epsilon-Nash equilibria. We show that
if there is at least one player with reachability objective, then doubly-exponential
patience is needed in general for epsilon-Nash equilibrium strategies, whereas
in contrast if all players have safety objectives, then the optimal bound on patience
for epsilon-Nash equilibrium strategies is only exponential."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Kristoffer
full_name: Hansen, Kristoffer
last_name: Hansen
citation:
ama: Chatterjee K, Ibsen-Jensen R, Hansen K. The Patience of Concurrent Stochastic
Games with Safety and Reachability Objectives. IST Austria; 2015. doi:10.15479/AT:IST-2015-322-v1-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Hansen, K. (2015). The patience
of concurrent stochastic games with safety and reachability objectives. IST
Austria. https://doi.org/10.15479/AT:IST-2015-322-v1-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Kristoffer Hansen. The
Patience of Concurrent Stochastic Games with Safety and Reachability Objectives.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-322-v1-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and K. Hansen, The patience of concurrent
stochastic games with safety and reachability objectives. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Hansen K. 2015. The patience of concurrent stochastic
games with safety and reachability objectives, IST Austria, 25p.
mla: Chatterjee, Krishnendu, et al. The Patience of Concurrent Stochastic Games
with Safety and Reachability Objectives. IST Austria, 2015, doi:10.15479/AT:IST-2015-322-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, K. Hansen, The Patience of Concurrent Stochastic
Games with Safety and Reachability Objectives, IST Austria, 2015.
date_created: 2018-12-12T11:39:17Z
date_published: 2015-02-19T00:00:00Z
date_updated: 2021-01-12T08:02:13Z
day: '19'
ddc:
- '005'
- '519'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-322-v1-1
file:
- access_level: open_access
checksum: bfb858262c30445b8e472c40069178a2
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:31Z
date_updated: 2020-07-14T12:46:53Z
file_id: '5491'
file_name: IST-2015-322-v1+1_safetygames.pdf
file_size: 661015
relation: main_file
file_date_updated: 2020-07-14T12:46:53Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '25'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '322'
status: public
title: The patience of concurrent stochastic games with safety and reachability objectives
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5432'
abstract:
- lang: eng
text: "Evolution occurs in populations of reproducing individuals. The structure
of the population affects the outcome of the evolutionary process. Evolutionary
graph theory is a powerful approach to study this phenomenon. There are two graphs.
The interaction graph specifies who interacts with whom in the context of evolution.The
replacement graph specifies who competes with whom for reproduction. \r\nThe vertices
of the two graphs are the same, and each vertex corresponds to an individual of
the population. A key quantity is the fixation probability of a new mutant. It
is defined as the probability that a newly introduced mutant (on a single vertex)
generates a lineage of offspring which eventually takes over the entire population
of resident individuals. The basic computational questions are as follows: (i)
the qualitative question asks whether the fixation probability is positive; and
(ii) the quantitative approximation question asks for an approximation of the
fixation probability. \r\nOur main results are:\r\n(1) We show that the qualitative
question is NP-complete and the quantitative approximation question is #P-hard
in the special case when the interaction and the replacement graphs coincide and
even with the restriction that the resident individuals do not reproduce (which
corresponds to an invading population taking over an empty structure).\r\n(2)
We show that in general the qualitative question is PSPACE-complete and the quantitative
approximation question is PSPACE-hard and can be solved in exponential time.\r\n"
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Chatterjee K, Ibsen-Jensen R, Nowak M. The Complexity of Evolutionary Games
on Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-323-v1-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2015). The complexity
of evolutionary games on graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-323-v1-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. The Complexity
of Evolutionary Games on Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-323-v1-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, The complexity of evolutionary
games on graphs. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Nowak M. 2015. The complexity of evolutionary
games on graphs, IST Austria, 29p.
mla: Chatterjee, Krishnendu, et al. The Complexity of Evolutionary Games on Graphs.
IST Austria, 2015, doi:10.15479/AT:IST-2015-323-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, M. Nowak, The Complexity of Evolutionary
Games on Graphs, IST Austria, 2015.
date_created: 2018-12-12T11:39:18Z
date_published: 2015-02-19T00:00:00Z
date_updated: 2023-02-23T12:26:33Z
day: '19'
ddc:
- '005'
- '576'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-323-v1-1
file:
- access_level: open_access
checksum: 546c1b291d545e7b24aaaf4199dac671
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:57Z
date_updated: 2020-07-14T12:46:53Z
file_id: '5519'
file_name: IST-2015-323-v1+1_main.pdf
file_size: 576347
relation: main_file
file_date_updated: 2020-07-14T12:46:53Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '29'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '323'
related_material:
record:
- id: '5421'
relation: earlier_version
status: public
- id: '5440'
relation: later_version
status: public
status: public
title: The complexity of evolutionary games on graphs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...