---
_id: '1335'
abstract:
- lang: eng
text: In this paper we review various automata-theoretic formalisms for expressing
quantitative properties. We start with finite-state Boolean automata that express
the traditional regular properties. We then consider weighted ω-automata that
can measure the average density of events, which finite-state Boolean automata
cannot. However, even weighted ω-automata cannot express basic performance properties
like average response time. We finally consider two formalisms of weighted ω-automata
with monitors, where the monitors are either (a) counters or (b) weighted automata
themselves. We present a translation result to establish that these two formalisms
are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata,
and can express average response time property. They present a natural, robust,
and expressive framework for quantitative specifications, with important decidable
properties.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: 'Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol
9837. Springer; 2016:23-38. doi:10.1007/978-3-662-53413-7_2'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative monitor
automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium,
Edinburgh, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53413-7_2'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative
Monitor Automata,” 9837:23–38. Springer, 2016. https://doi.org/10.1007/978-3-662-53413-7_2.
ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative monitor automata,”
presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom, 2016,
vol. 9837, pp. 23–38.'
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata.
SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.'
mla: Chatterjee, Krishnendu, et al. Quantitative Monitor Automata. Vol. 9837,
Springer, 2016, pp. 23–38, doi:10.1007/978-3-662-53413-7_2.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38.
conference:
end_date: 2016-09-10
location: Edinburgh, United Kingdom
name: 'SAS: Static Analysis Symposium'
start_date: 2016-09-08
date_created: 2018-12-11T11:51:26Z
date_published: 2016-08-31T00:00:00Z
date_updated: 2021-01-12T06:49:58Z
day: '31'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-53413-7_2
ec_funded: 1
intvolume: ' 9837'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.06764
month: '08'
oa: 1
oa_version: Preprint
page: 23 - 38
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Springer
publist_id: '5932'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative monitor automata
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9837
year: '2016'
...
---
_id: '1518'
abstract:
- lang: eng
text: The inference of demographic history from genome data is hindered by a lack
of efficient computational approaches. In particular, it has proved difficult
to exploit the information contained in the distribution of genealogies across
the genome. We have previously shown that the generating function (GF) of genealogies
can be used to analytically compute likelihoods of demographic models from configurations
of mutations in short sequence blocks (Lohse et al. 2011). Although the GF has
a simple, recursive form, the size of such likelihood calculations explodes quickly
with the number of individuals and applications of this framework have so far
been mainly limited to small samples (pairs and triplets) for which the GF can
be written by hand. Here we investigate several strategies for exploiting the
inherent symmetries of the coalescent. In particular, we show that the GF of genealogies
can be decomposed into a set of equivalence classes that allows likelihood calculations
from nontrivial samples. Using this strategy, we automated blockwise likelihood
calculations for a general set of demographic scenarios in Mathematica. These
histories may involve population size changes, continuous migration, discrete
divergence, and admixture between multiple populations. To give a concrete example,
we calculate the likelihood for a model of isolation with migration (IM), assuming
two diploid samples without phase and outgroup information. We demonstrate the
new inference scheme with an analysis of two individual butterfly genomes from
the sister species Heliconius melpomene rosina and H. cydno.
acknowledgement: "We thank Lynsey Bunnefeld for discussions throughout the project
and Joshua Schraiber and one anonymous reviewer\r\nfor constructive comments on
an earlier version of this manuscript. This work was supported by funding from the\r\nUnited
Kingdom Natural Environment Research Council (to K.L.) (NE/I020288/1) and a grant
from the European\r\nResearch Council (250152) (to N.H.B.)."
article_processing_charge: No
article_type: original
author:
- first_name: Konrad
full_name: Lohse, Konrad
last_name: Lohse
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Simon
full_name: Martin, Simon
last_name: Martin
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Lohse K, Chmelik M, Martin S, Barton NH. Efficient strategies for calculating
blockwise likelihoods under the coalescent. Genetics. 2016;202(2):775-786.
doi:10.1534/genetics.115.183814
apa: Lohse, K., Chmelik, M., Martin, S., & Barton, N. H. (2016). Efficient strategies
for calculating blockwise likelihoods under the coalescent. Genetics. Genetics
Society of America. https://doi.org/10.1534/genetics.115.183814
chicago: Lohse, Konrad, Martin Chmelik, Simon Martin, and Nicholas H Barton. “Efficient
Strategies for Calculating Blockwise Likelihoods under the Coalescent.” Genetics.
Genetics Society of America, 2016. https://doi.org/10.1534/genetics.115.183814.
ieee: K. Lohse, M. Chmelik, S. Martin, and N. H. Barton, “Efficient strategies for
calculating blockwise likelihoods under the coalescent,” Genetics, vol.
202, no. 2. Genetics Society of America, pp. 775–786, 2016.
ista: Lohse K, Chmelik M, Martin S, Barton NH. 2016. Efficient strategies for calculating
blockwise likelihoods under the coalescent. Genetics. 202(2), 775–786.
mla: Lohse, Konrad, et al. “Efficient Strategies for Calculating Blockwise Likelihoods
under the Coalescent.” Genetics, vol. 202, no. 2, Genetics Society of America,
2016, pp. 775–86, doi:10.1534/genetics.115.183814.
short: K. Lohse, M. Chmelik, S. Martin, N.H. Barton, Genetics 202 (2016) 775–786.
date_created: 2018-12-11T11:52:29Z
date_published: 2016-02-01T00:00:00Z
date_updated: 2025-05-28T11:42:48Z
day: '01'
ddc:
- '570'
department:
- _id: KrCh
- _id: NiBa
doi: 10.1534/genetics.115.183814
ec_funded: 1
external_id:
pmid:
- '26715666'
file:
- access_level: open_access
checksum: 41c9b5d72e7fe4624dd22dfe622337d5
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:51Z
date_updated: 2020-07-14T12:45:00Z
file_id: '5241'
file_name: IST-2016-561-v1+1_Lohse_et_al_Genetics_2015.pdf
file_size: 957466
relation: main_file
file_date_updated: 2020-07-14T12:45:00Z
has_accepted_license: '1'
intvolume: ' 202'
issue: '2'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Preprint
page: 775 - 786
pmid: 1
project:
- _id: 25B07788-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '250152'
name: Limits to selection in biology and in evolutionary computation
publication: Genetics
publication_status: published
publisher: Genetics Society of America
publist_id: '5658'
pubrep_id: '561'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Efficient strategies for calculating blockwise likelihoods under the coalescent
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 202
year: '2016'
...
---
_id: '1529'
abstract:
- lang: eng
text: 'We consider partially observable Markov decision processes (POMDPs) with
a set of target states and an integer cost associated with every transition. The
optimization objective we study asks to minimize the expected total cost of reaching
a state in the target set, while ensuring that the target set is reached almost
surely (with probability 1). We show that for integer costs approximating the
optimal cost is undecidable. For positive costs, our results are as follows: (i)
we establish matching lower and upper bounds for the optimal cost, both double
exponential in the POMDP state space size; (ii) we show that the problem of approximating
the optimal cost is decidable and present approximation algorithms developing
on the existing algorithms for POMDPs with finite-horizon objectives. While the
worst-case running time of our algorithm is double exponential, we also present
efficient stopping criteria for the algorithm and show experimentally that it
performs well in many examples of interest.'
acknowledgement: 'We thank Blai Bonet for helping us with RTDP-Bel. The research was
partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant
No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty
fellows award.'
article_processing_charge: No
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: Raghav
full_name: Gupta, Raghav
last_name: Gupta
- first_name: Ayush
full_name: Kanodia, Ayush
last_name: Kanodia
citation:
ama: Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability
in POMDPs. Artificial Intelligence. 2016;234:26-48. doi:10.1016/j.artint.2016.01.007
apa: Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2016). Optimal cost
almost-sure reachability in POMDPs. Artificial Intelligence. Elsevier.
https://doi.org/10.1016/j.artint.2016.01.007
chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia.
“Optimal Cost Almost-Sure Reachability in POMDPs.” Artificial Intelligence.
Elsevier, 2016. https://doi.org/10.1016/j.artint.2016.01.007.
ieee: K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure
reachability in POMDPs,” Artificial Intelligence, vol. 234. Elsevier, pp.
26–48, 2016.
ista: Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2016. Optimal cost almost-sure
reachability in POMDPs. Artificial Intelligence. 234, 26–48.
mla: Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.”
Artificial Intelligence, vol. 234, Elsevier, 2016, pp. 26–48, doi:10.1016/j.artint.2016.01.007.
short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Artificial Intelligence
234 (2016) 26–48.
date_created: 2018-12-11T11:52:33Z
date_published: 2016-05-01T00:00:00Z
date_updated: 2023-02-23T12:25:49Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.artint.2016.01.007
ec_funded: 1
external_id:
arxiv:
- '1411.3880'
intvolume: ' 234'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1411.3880
month: '05'
oa: 1
oa_version: Preprint
page: 26 - 48
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Artificial Intelligence
publication_status: published
publisher: Elsevier
publist_id: '5642'
quality_controlled: '1'
related_material:
record:
- id: '1820'
relation: earlier_version
status: public
- id: '5425'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Optimal cost almost-sure reachability in POMDPs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 234
year: '2016'
...
---
_id: '1340'
abstract:
- lang: eng
text: We study repeated games with absorbing states, a type of two-player, zero-sum
concurrent mean-payoff games with the prototypical example being the Big Match
of Gillete (1957). These games may not allow optimal strategies but they always
have ε-optimal strategies. In this paper we design ε-optimal strategies for Player
1 in these games that use only O(log log T) space. Furthermore, we construct strategies
for Player 1 that use space s(T), for an arbitrary small unbounded non-decreasing
function s, and which guarantee an ε-optimal value for Player 1 in the limit superior
sense. The previously known strategies use space Ω(log T) and it was known that
no strategy can use constant space if it is ε-optimal even in the limit superior
sense. We also give a complementary lower bound. Furthermore, we also show that
no Markov strategy, even extended with finite memory, can ensure value greater
than 0 in the Big Match, answering a question posed by Neyman [11].
alternative_title:
- LNCS
author:
- first_name: Kristoffer
full_name: Hansen, Kristoffer
last_name: Hansen
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Michal
full_name: Koucký, Michal
last_name: Koucký
citation:
ama: 'Hansen K, Ibsen-Jensen R, Koucký M. The big match in small space. In: Vol
9928. Springer; 2016:64-76. doi:10.1007/978-3-662-53354-3_6'
apa: 'Hansen, K., Ibsen-Jensen, R., & Koucký, M. (2016). The big match in small
space (Vol. 9928, pp. 64–76). Presented at the SAGT: Symposium on Algorithmic
Game Theory, Liverpool, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53354-3_6'
chicago: Hansen, Kristoffer, Rasmus Ibsen-Jensen, and Michal Koucký. “The Big Match
in Small Space,” 9928:64–76. Springer, 2016. https://doi.org/10.1007/978-3-662-53354-3_6.
ieee: 'K. Hansen, R. Ibsen-Jensen, and M. Koucký, “The big match in small space,”
presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United
Kingdom, 2016, vol. 9928, pp. 64–76.'
ista: 'Hansen K, Ibsen-Jensen R, Koucký M. 2016. The big match in small space. SAGT:
Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 64–76.'
mla: Hansen, Kristoffer, et al. The Big Match in Small Space. Vol. 9928,
Springer, 2016, pp. 64–76, doi:10.1007/978-3-662-53354-3_6.
short: K. Hansen, R. Ibsen-Jensen, M. Koucký, in:, Springer, 2016, pp. 64–76.
conference:
end_date: 2016-09-21
location: Liverpool, United Kingdom
name: 'SAGT: Symposium on Algorithmic Game Theory'
start_date: 2016-09-19
date_created: 2018-12-11T11:51:28Z
date_published: 2016-09-01T00:00:00Z
date_updated: 2021-01-12T06:50:00Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-53354-3_6
ec_funded: 1
intvolume: ' 9928'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.07634
month: '09'
oa: 1
oa_version: Preprint
page: 64 - 76
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_status: published
publisher: Springer
publist_id: '5927'
quality_controlled: '1'
scopus_import: 1
status: public
title: The big match in small space
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9928
year: '2016'
...
---
_id: '1380'
abstract:
- lang: eng
text: We consider higher-dimensional versions of Kannan and Lipton's Orbit Problem
- determining whether a target vector space V may be reached from a starting point
x under repeated applications of a linear transformation A. Answering two questions
posed by Kannan and Lipton in the 1980s, we show that when V has dimension one,
this problem is solvable in polynomial time, and when V has dimension two or three,
the problem is in NPRP.
article_number: '23'
author:
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
- first_name: Joël
full_name: Ouaknine, Joël
last_name: Ouaknine
- first_name: James
full_name: Worrell, James
last_name: Worrell
citation:
ama: Chonev VK, Ouaknine J, Worrell J. On the complexity of the orbit problem. Journal
of the ACM. 2016;63(3). doi:10.1145/2857050
apa: Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the complexity of
the orbit problem. Journal of the ACM. ACM. https://doi.org/10.1145/2857050
chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Complexity
of the Orbit Problem.” Journal of the ACM. ACM, 2016. https://doi.org/10.1145/2857050.
ieee: V. K. Chonev, J. Ouaknine, and J. Worrell, “On the complexity of the orbit
problem,” Journal of the ACM, vol. 63, no. 3. ACM, 2016.
ista: Chonev VK, Ouaknine J, Worrell J. 2016. On the complexity of the orbit problem.
Journal of the ACM. 63(3), 23.
mla: Chonev, Ventsislav K., et al. “On the Complexity of the Orbit Problem.” Journal
of the ACM, vol. 63, no. 3, 23, ACM, 2016, doi:10.1145/2857050.
short: V.K. Chonev, J. Ouaknine, J. Worrell, Journal of the ACM 63 (2016).
date_created: 2018-12-11T11:51:41Z
date_published: 2016-06-01T00:00:00Z
date_updated: 2021-01-12T06:50:17Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2857050
intvolume: ' 63'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1303.2981
month: '06'
oa: 1
oa_version: Preprint
publication: Journal of the ACM
publication_status: published
publisher: ACM
publist_id: '5831'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the complexity of the orbit problem
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 63
year: '2016'
...
---
_id: '1386'
abstract:
- lang: eng
text: We consider nondeterministic probabilistic programs with the most basic liveness
property of termination. We present efficient methods for termination analysis
of nondeterministic probabilistic programs with polynomial guards and assignments.
Our approach is through synthesis of polynomial ranking supermartingales, that
on one hand significantly generalizes linear ranking supermartingales and on the
other hand is a counterpart of polynomial ranking-functions for proving termination
of nonprobabilistic programs. The approach synthesizes polynomial ranking-supermartingales
through Positivstellensatz's, yielding an efficient method which is not only sound,
but also semi-complete over a large subclass of programs. We show experimental
results to demonstrate that our approach can handle several classical programs
with complex polynomial guards and assignments, and can synthesize efficient quadratic
ranking-supermartingales when a linear one does not exist even for simple affine
programs.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Hongfei
full_name: Fu, Hongfei
id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
last_name: Fu
- first_name: Amir
full_name: Goharshady, Amir
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
citation:
ama: 'Chatterjee K, Fu H, Goharshady AK. Termination analysis of probabilistic programs
through Positivstellensatz’s. In: Vol 9779. Springer; 2016:3-22. doi:10.1007/978-3-319-41528-4_1'
apa: 'Chatterjee, K., Fu, H., & Goharshady, A. K. (2016). Termination analysis
of probabilistic programs through Positivstellensatz’s (Vol. 9779, pp. 3–22).
Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer.
https://doi.org/10.1007/978-3-319-41528-4_1'
chicago: Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Termination
Analysis of Probabilistic Programs through Positivstellensatz’s,” 9779:3–22. Springer,
2016. https://doi.org/10.1007/978-3-319-41528-4_1.
ieee: 'K. Chatterjee, H. Fu, and A. K. Goharshady, “Termination analysis of probabilistic
programs through Positivstellensatz’s,” presented at the CAV: Computer Aided Verification,
Toronto, Canada, 2016, vol. 9779, pp. 3–22.'
ista: 'Chatterjee K, Fu H, Goharshady AK. 2016. Termination analysis of probabilistic
programs through Positivstellensatz’s. CAV: Computer Aided Verification, LNCS,
vol. 9779, 3–22.'
mla: Chatterjee, Krishnendu, et al. Termination Analysis of Probabilistic Programs
through Positivstellensatz’s. Vol. 9779, Springer, 2016, pp. 3–22, doi:10.1007/978-3-319-41528-4_1.
short: K. Chatterjee, H. Fu, A.K. Goharshady, in:, Springer, 2016, pp. 3–22.
conference:
end_date: 2016-07-23
location: Toronto, Canada
name: 'CAV: Computer Aided Verification'
start_date: 2016-07-17
date_created: 2018-12-11T11:51:43Z
date_published: 2016-07-01T00:00:00Z
date_updated: 2024-03-25T23:30:18Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-319-41528-4_1
ec_funded: 1
intvolume: ' 9779'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1604.07169
month: '07'
oa: 1
oa_version: Preprint
page: 3 - 22
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '5824'
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Termination analysis of probabilistic programs through Positivstellensatz's
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9779
year: '2016'
...
---
_id: '1389'
abstract:
- lang: eng
text: "The continuous evolution of a wide variety of systems, including continous-time
Markov chains and linear hybrid automata, can be\r\ndescribed in terms of linear
differential equations. In this paper we study the decision problem of whether
the solution x(t) of a system of linear differential equations dx/dt = Ax reaches
a target halfspace infinitely often. This recurrent reachability problem can\r\nequivalently
be formulated as the following Infinite Zeros Problem: does a real-valued function
f:R≥0 --> R satisfying a given linear\r\ndifferential equation have infinitely
many zeros? Our main decidability result is that if the differential equation
has order at most 7, then the Infinite Zeros Problem is decidable. On the other
hand, we show that a decision procedure for the Infinite Zeros Problem at order
9 (and above) would entail a major breakthrough in Diophantine Approximation,
specifically an algorithm for computing the Lagrange constants of arbitrary real
algebraic numbers to arbitrary precision."
author:
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
- first_name: Joël
full_name: Ouaknine, Joël
last_name: Ouaknine
- first_name: James
full_name: Worrell, James
last_name: Worrell
citation:
ama: 'Chonev VK, Ouaknine J, Worrell J. On recurrent reachability for continuous
linear dynamical systems. In: LICS ’16. IEEE; 2016:515-524. doi:10.1145/2933575.2934548'
apa: 'Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On recurrent reachability
for continuous linear dynamical systems. In LICS ’16 (pp. 515–524). New
York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2934548'
chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On Recurrent Reachability
for Continuous Linear Dynamical Systems.” In LICS ’16, 515–24. IEEE, 2016.
https://doi.org/10.1145/2933575.2934548.
ieee: V. K. Chonev, J. Ouaknine, and J. Worrell, “On recurrent reachability for
continuous linear dynamical systems,” in LICS ’16, New York, NY, USA, 2016,
pp. 515–524.
ista: 'Chonev VK, Ouaknine J, Worrell J. 2016. On recurrent reachability for continuous
linear dynamical systems. LICS ’16. LICS: Logic in Computer Science, 515–524.'
mla: Chonev, Ventsislav K., et al. “On Recurrent Reachability for Continuous Linear
Dynamical Systems.” LICS ’16, IEEE, 2016, pp. 515–24, doi:10.1145/2933575.2934548.
short: V.K. Chonev, J. Ouaknine, J. Worrell, in:, LICS ’16, IEEE, 2016, pp. 515–524.
conference:
end_date: 2018-07-08
location: New York, NY, USA
name: 'LICS: Logic in Computer Science'
start_date: 2018-07-05
date_created: 2018-12-11T11:51:44Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2021-01-12T06:50:20Z
day: '05'
department:
- _id: KrCh
doi: 10.1145/2933575.2934548
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1507.03632
month: '07'
oa: 1
oa_version: Preprint
page: 515 - 524
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: LICS '16
publication_status: published
publisher: IEEE
publist_id: '5820'
quality_controlled: '1'
scopus_import: 1
status: public
title: On recurrent reachability for continuous linear dynamical systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1397'
abstract:
- lang: eng
text: 'We study partially observable Markov decision processes (POMDPs) with objectives
used in verification and artificial intelligence. The qualitative analysis problem
given a POMDP and an objective asks whether there is a strategy (policy) to ensure
that the objective is satisfied almost surely (with probability 1), resp. with
positive probability (with probability greater than 0). For POMDPs with limit-average
payoff, where a reward value in the interval [0,1] is associated to every transition,
and the payoff of an infinite path is the long-run average of the rewards, we
consider two types of path constraints: (i) a quantitative limit-average constraint
defines the set of paths where the payoff is at least a given threshold L1 = 1.
Our main results for qualitative limit-average constraint under almost-sure winning
are as follows: (i) the problem of deciding the existence of a finite-memory controller
is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory
controller is undecidable. For quantitative limit-average constraints we show
that the problem of deciding the existence of a finite-memory controller is undecidable.
We present a prototype implementation of our EXPTIME algorithm. For POMDPs with
w-regular conditions specified as parity objectives, while the qualitative analysis
problems are known to be undecidable even for very special case of parity objectives,
we establish decidability (with optimal complexity) of the qualitative analysis
problems for POMDPs with parity objectives under finite-memory strategies. We
establish optimal (exponential) memory bounds and EXPTIME-completeness of the
qualitative analysis problems under finite-memory strategies for POMDPs with parity
objectives. Based on our theoretical algorithms we also present a practical approach,
where we design heuristics to deal with the exponential complexity, and have applied
our implementation on a number of well-known POMDP examples for robotics applications.
For POMDPs with a set of target states and an integer cost associated with every
transition, we study the optimization objective that asks to minimize the expected
total cost of reaching a state in the target set, while ensuring that the target
set is reached almost surely. We show that for general integer costs approximating
the optimal cost is undecidable. For positive costs, our results are as follows:
(i) we establish matching lower and upper bounds for the optimal cost, both double
and exponential in the POMDP state space size; (ii) we show that the problem of
approximating the optimal cost is decidable and present approximation algorithms
that extend existing algorithms for POMDPs with finite-horizon objectives. We
show experimentally that it performs well in many examples of interest. We study
more deeply the problem of almost-sure reachability, where given a set of target
states, the question is to decide whether there is a strategy to ensure that the
target set is reached almost surely. While in general the problem EXPTIME-complete,
in many practical cases strategies with a small amount of memory suffice. Moreover,
the existing solution to the problem is explicit, which first requires to construct
explicitly an exponential reduction to a belief-support MDP. We first study the
existence of observation-stationary strategies, which is NP-complete, and then
small-memory strategies. We present a symbolic algorithm by an efficient encoding
to SAT and using a SAT solver for the problem. We report experimental results
demonstrating the scalability of our symbolic (SAT-based) approach. Decentralized
POMDPs (DEC-POMDPs) extend POMDPs to a multi-agent setting, where several agents
operate in an uncertain environment independently to achieve a joint objective.
In this work we consider Goal DEC-POMDPs, where given a set of target states,
the objective is to ensure that the target set is reached with minimal cost. We
consider the indefinite-horizon (infinite-horizon with either discounted-sum,
or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present
a new and novel method to solve the problem that extends methods for finite-horizon
DEC-POMDPs and the real-time dynamic programming approach for POMDPs. We present
experimental results on several examples, and show that our approach presents
promising results. In the end we present a short summary of a few other results
related to verification of MDPs and POMDPs.'
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: Chmelik M. Algorithms for partially observable markov decision processes. 2016.
apa: Chmelik, M. (2016). Algorithms for partially observable markov decision
processes. Institute of Science and Technology Austria.
chicago: Chmelik, Martin. “Algorithms for Partially Observable Markov Decision Processes.”
Institute of Science and Technology Austria, 2016.
ieee: M. Chmelik, “Algorithms for partially observable markov decision processes,”
Institute of Science and Technology Austria, 2016.
ista: Chmelik M. 2016. Algorithms for partially observable markov decision processes.
Institute of Science and Technology Austria.
mla: Chmelik, Martin. Algorithms for Partially Observable Markov Decision Processes.
Institute of Science and Technology Austria, 2016.
short: M. Chmelik, Algorithms for Partially Observable Markov Decision Processes,
Institute of Science and Technology Austria, 2016.
date_created: 2018-12-11T11:51:47Z
date_published: 2016-02-01T00:00:00Z
date_updated: 2023-09-07T11:54:58Z
day: '01'
degree_awarded: PhD
department:
- _id: KrCh
language:
- iso: eng
month: '02'
oa_version: None
page: '232'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5810'
status: public
supervisor:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
title: Algorithms for partially observable markov decision processes
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2016'
...
---
_id: '1423'
abstract:
- lang: eng
text: 'Direct reciprocity is a mechanism for the evolution of cooperation based
on repeated interactions. When individuals meet repeatedly, they can use conditional
strategies to enforce cooperative outcomes that would not be feasible in one-shot
social dilemmas. Direct reciprocity requires that individuals keep track of their
past interactions and find the right response. However, there are natural bounds
on strategic complexity: Humans find it difficult to remember past interactions
accurately, especially over long timespans. Given these limitations, it is natural
to ask how complex strategies need to be for cooperation to evolve. Here, we study
stochastic evolutionary game dynamics in finite populations to systematically
compare the evolutionary performance of reactive strategies, which only respond
to the co-player''s previous move, and memory-one strategies, which take into
account the own and the co-player''s previous move. In both cases, we compare
deterministic strategy and stochastic strategy spaces. For reactive strategies
and small costs, we find that stochasticity benefits cooperation, because it allows
for generous-tit-for-tat. For memory one strategies and small costs, we find that
stochasticity does not increase the propensity for cooperation, because the deterministic
rule of win-stay, lose-shift works best. For memory one strategies and large costs,
however, stochasticity can augment cooperation.'
acknowledgement: C.H. acknowledges generous funding from the Schrödinger scholarship
of the Austrian Science Fund (FWF), J3475.
article_number: '25676'
author:
- first_name: Seung
full_name: Baek, Seung
last_name: Baek
- first_name: Hyeongchai
full_name: Jeong, Hyeongchai
last_name: Jeong
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Baek S, Jeong H, Hilbe C, Nowak M. Comparing reactive and memory-one strategies
of direct reciprocity. Scientific Reports. 2016;6. doi:10.1038/srep25676
apa: Baek, S., Jeong, H., Hilbe, C., & Nowak, M. (2016). Comparing reactive
and memory-one strategies of direct reciprocity. Scientific Reports. Nature
Publishing Group. https://doi.org/10.1038/srep25676
chicago: Baek, Seung, Hyeongchai Jeong, Christian Hilbe, and Martin Nowak. “Comparing
Reactive and Memory-One Strategies of Direct Reciprocity.” Scientific Reports.
Nature Publishing Group, 2016. https://doi.org/10.1038/srep25676.
ieee: S. Baek, H. Jeong, C. Hilbe, and M. Nowak, “Comparing reactive and memory-one
strategies of direct reciprocity,” Scientific Reports, vol. 6. Nature Publishing
Group, 2016.
ista: Baek S, Jeong H, Hilbe C, Nowak M. 2016. Comparing reactive and memory-one
strategies of direct reciprocity. Scientific Reports. 6, 25676.
mla: Baek, Seung, et al. “Comparing Reactive and Memory-One Strategies of Direct
Reciprocity.” Scientific Reports, vol. 6, 25676, Nature Publishing Group,
2016, doi:10.1038/srep25676.
short: S. Baek, H. Jeong, C. Hilbe, M. Nowak, Scientific Reports 6 (2016).
date_created: 2018-12-11T11:51:56Z
date_published: 2016-05-10T00:00:00Z
date_updated: 2021-01-12T06:50:38Z
day: '10'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/srep25676
file:
- access_level: open_access
checksum: ee17c482370d2e1b3add393710d3c696
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:08Z
date_updated: 2020-07-14T12:44:53Z
file_id: '5327'
file_name: IST-2016-590-v1+1_srep25676.pdf
file_size: 1349915
relation: main_file
file_date_updated: 2020-07-14T12:44:53Z
has_accepted_license: '1'
intvolume: ' 6'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '05'
oa: 1
oa_version: Published Version
publication: Scientific Reports
publication_status: published
publisher: Nature Publishing Group
publist_id: '5784'
pubrep_id: '590'
quality_controlled: '1'
scopus_import: 1
status: public
title: Comparing reactive and memory-one strategies of direct reciprocity
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 6
year: '2016'
...
---
_id: '1426'
abstract:
- lang: eng
text: 'Brood parasites exploit their host in order to increase their own fitness.
Typically, this results in an arms race between parasite trickery and host defence.
Thus, it is puzzling to observe hosts that accept parasitism without any resistance.
The ‘mafia’ hypothesis suggests that these hosts accept parasitism to avoid retaliation.
Retaliation has been shown to evolve when the hosts condition their response to
mafia parasites, who use depredation as a targeted response to rejection. However,
it is unclear if acceptance would also emerge when ‘farming’ parasites are present
in the population. Farming parasites use depredation to synchronize the timing
with the host, destroying mature clutches to force the host to re-nest. Herein,
we develop an evolutionary model to analyse the interaction between depredatory
parasites and their hosts. We show that coevolutionary cycles between farmers
and mafia can still induce host acceptance of brood parasites. However, this equilibrium
is unstable and in the long-run the dynamics of this host–parasite interaction
exhibits strong oscillations: when farmers are the majority, accepters conditional
to mafia (the host will reject first and only accept after retaliation by the
parasite) have a higher fitness than unconditional accepters (the host always
accepts parasitism). This leads to an increase in mafia parasites’ fitness and
in turn induce an optimal environment for accepter hosts.'
acknowledgement: C.H. gratefully acknowledges funding by the Schrödinger scholarship
of the Austrian Science Fund (FWF) J3475.
article_number: '160036'
author:
- first_name: Maria
full_name: Chakra, Maria
last_name: Chakra
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Arne
full_name: Traulsen, Arne
last_name: Traulsen
citation:
ama: Chakra M, Hilbe C, Traulsen A. Coevolutionary interactions between farmers
and mafia induce host acceptance of avian brood parasites. Royal Society Open
Science. 2016;3(5). doi:10.1098/rsos.160036
apa: Chakra, M., Hilbe, C., & Traulsen, A. (2016). Coevolutionary interactions
between farmers and mafia induce host acceptance of avian brood parasites. Royal
Society Open Science. Royal Society, The. https://doi.org/10.1098/rsos.160036
chicago: Chakra, Maria, Christian Hilbe, and Arne Traulsen. “Coevolutionary Interactions
between Farmers and Mafia Induce Host Acceptance of Avian Brood Parasites.” Royal
Society Open Science. Royal Society, The, 2016. https://doi.org/10.1098/rsos.160036.
ieee: M. Chakra, C. Hilbe, and A. Traulsen, “Coevolutionary interactions between
farmers and mafia induce host acceptance of avian brood parasites,” Royal Society
Open Science, vol. 3, no. 5. Royal Society, The, 2016.
ista: Chakra M, Hilbe C, Traulsen A. 2016. Coevolutionary interactions between farmers
and mafia induce host acceptance of avian brood parasites. Royal Society Open
Science. 3(5), 160036.
mla: Chakra, Maria, et al. “Coevolutionary Interactions between Farmers and Mafia
Induce Host Acceptance of Avian Brood Parasites.” Royal Society Open Science,
vol. 3, no. 5, 160036, Royal Society, The, 2016, doi:10.1098/rsos.160036.
short: M. Chakra, C. Hilbe, A. Traulsen, Royal Society Open Science 3 (2016).
date_created: 2018-12-11T11:51:57Z
date_published: 2016-05-01T00:00:00Z
date_updated: 2021-01-12T06:50:39Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1098/rsos.160036
file:
- access_level: open_access
checksum: bf84211b31fe87451e738ba301d729c3
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:49Z
date_updated: 2020-07-14T12:44:53Z
file_id: '5104'
file_name: IST-2016-589-v1+1_160036.full.pdf
file_size: 937002
relation: main_file
file_date_updated: 2020-07-14T12:44:53Z
has_accepted_license: '1'
intvolume: ' 3'
issue: '5'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
publication: Royal Society Open Science
publication_status: published
publisher: Royal Society, The
publist_id: '5776'
pubrep_id: '589'
quality_controlled: '1'
scopus_import: 1
status: public
title: Coevolutionary interactions between farmers and mafia induce host acceptance
of avian brood parasites
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 3
year: '2016'
...
---
_id: '1437'
abstract:
- lang: eng
text: We study algorithmic questions for concurrent systems where the transitions
are labeled from a complete, closed semiring, and path properties are algebraic
with semiring operations. The algebraic path properties can model dataflow analysis
problems, the shortest path problem, and many other natural problems that arise
in program analysis. We consider that each component of the concurrent system
is a graph with constant treewidth, a property satisfied by the controlflow graphs
of most programs. We allow for multiple possible queries, which arise naturally
in demand driven dataflow analysis. The study of multiple queries allows us to
consider the tradeoff between the resource usage of the one-time preprocessing
and for each individual query. The traditional approach constructs the product
graph of all components and applies the best-known graph algorithm on the product.
In this approach, even the answer to a single query requires the transitive closure
(i.e., the results of all possible queries), which provides no room for tradeoff
between preprocessing and query time. Our main contributions are algorithms that
significantly improve the worst-case running time of the traditional approach,
and provide various tradeoffs depending on the number of queries. For example,
in a concurrent system of two components, the traditional approach requires hexic
time in the worst case for answering one query as well as computing the transitive
closure, whereas we show that with one-time preprocessing in almost cubic time,
each subsequent query can be answered in at most linear time, and even the transitive
closure can be computed in almost quartic time. Furthermore, we establish conditional
optimality results showing that the worst-case running time of our algorithms
cannot be improved without achieving major breakthroughs in graph algorithms (i.e.,
improving the worst-case bound for the shortest path problem in general graphs).
Preliminary experimental results show that our algorithms perform favorably on
several benchmarks.
alternative_title:
- POPL
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: Amir
full_name: Goharshady, Amir
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 'Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Algorithms for
algebraic path properties in concurrent systems of constant treewidth components.
In: Vol 20-22. ACM; 2016:733-747. doi:10.1145/2837614.2837624'
apa: 'Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Pavlogiannis, A.
(2016). Algorithms for algebraic path properties in concurrent systems of constant
treewidth components (Vol. 20–22, pp. 733–747). Presented at the POPL: Principles
of Programming Languages, St. Petersburg, FL, USA: ACM. https://doi.org/10.1145/2837614.2837624'
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen,
and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent
Systems of Constant Treewidth Components,” 20–22:733–47. ACM, 2016. https://doi.org/10.1145/2837614.2837624.
ieee: 'K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Algorithms
for algebraic path properties in concurrent systems of constant treewidth components,”
presented at the POPL: Principles of Programming Languages, St. Petersburg, FL,
USA, 2016, vol. 20–22, pp. 733–747.'
ista: 'Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2016. Algorithms
for algebraic path properties in concurrent systems of constant treewidth components.
POPL: Principles of Programming Languages, POPL, vol. 20–22, 733–747.'
mla: Chatterjee, Krishnendu, et al. Algorithms for Algebraic Path Properties
in Concurrent Systems of Constant Treewidth Components. Vol. 20–22, ACM, 2016,
pp. 733–47, doi:10.1145/2837614.2837624.
short: K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, ACM,
2016, pp. 733–747.
conference:
end_date: 2016-01-22
location: St. Petersburg, FL, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2016-01-20
date_created: 2018-12-11T11:52:01Z
date_published: 2016-01-11T00:00:00Z
date_updated: 2024-03-25T23:30:18Z
day: '11'
department:
- _id: KrCh
doi: 10.1145/2837614.2837624
ec_funded: 1
external_id:
arxiv:
- '1510.07565'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1510.07565
month: '01'
oa: 1
oa_version: Preprint
page: 733 - 747
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_status: published
publisher: ACM
publist_id: '5761'
quality_controlled: '1'
related_material:
record:
- id: '5441'
relation: earlier_version
status: public
- id: '5442'
relation: earlier_version
status: public
- id: '821'
relation: dissertation_contains
status: public
- id: '6009'
relation: later_version
status: public
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Algorithms for algebraic path properties in concurrent systems of constant
treewidth components
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 20-22
year: '2016'
...
---
_id: '1438'
abstract:
- lang: eng
text: 'In this paper, we consider termination of probabilistic programs with real-valued
variables. The questions concerned are: (a) qualitative ones that ask (i) whether
the program terminates with probability 1 (almost-sure termination) and (ii) whether
the expected termination time is finite (finite termination); (b) quantitative
ones that ask (i) to approximate the expected termination time (expectation problem)
and (ii) to compute a bound B such that the probability to terminate after B steps
decreases exponentially (concentration problem). To solve these questions, we
utilize the notion of ranking supermartingales which is a powerful approach for
proving termination of probabilistic programs. In detail, we focus on algorithmic
synthesis of linear ranking-supermartingales over affine probabilistic programs
(APP''s) with both angelic and demonic non-determinism. An important subclass
of APP''s is LRAPP which is defined as the class of all APP''s over which a linear
ranking-supermartingale exists. Our main contributions are as follows. Firstly,
we show that the membership problem of LRAPP (i) can be decided in polynomial
time for APP''s with at most demonic non-determinism, and (ii) is NP-hard and
in PSPACE for APP''s with angelic non-determinism; moreover, the NP-hardness result
holds already for APP''s without probability and demonic non-determinism. Secondly,
we show that the concentration problem over LRAPP can be solved in the same complexity
as for the membership problem of LRAPP. Finally, we show that the expectation
problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP''s
without probability and non-determinism (i.e., deterministic programs). Our experimental
results demonstrate the effectiveness of our approach to answer the qualitative
and quantitative questions over APP''s with at most demonic non-determinism.'
acknowledgement: 'Supported by the Natural Science Foundation of China (NSFC) under
Grant No. 61532019 '
alternative_title:
- POPL
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: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Rouzbeh
full_name: Hasheminezhad, Rouzbeh
last_name: Hasheminezhad
citation:
ama: 'Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative
and quantitative termination problems for affine probabilistic programs. In: Vol
20-22. ACM; 2016:327-342. doi:10.1145/2837614.2837639'
apa: 'Chatterjee, K., Fu, H., Novotný, P., & Hasheminezhad, R. (2016). Algorithmic
analysis of qualitative and quantitative termination problems for affine probabilistic
programs (Vol. 20–22, pp. 327–342). Presented at the POPL: Principles of Programming
Languages, St. Petersburg, FL, USA: ACM. https://doi.org/10.1145/2837614.2837639'
chicago: Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad.
“Algorithmic Analysis of Qualitative and Quantitative Termination Problems for
Affine Probabilistic Programs,” 20–22:327–42. ACM, 2016. https://doi.org/10.1145/2837614.2837639.
ieee: 'K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic
programs,” presented at the POPL: Principles of Programming Languages, St. Petersburg,
FL, USA, 2016, vol. 20–22, pp. 327–342.'
ista: 'Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2016. Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic
programs. POPL: Principles of Programming Languages, POPL, vol. 20–22, 327–342.'
mla: Chatterjee, Krishnendu, et al. Algorithmic Analysis of Qualitative and Quantitative
Termination Problems for Affine Probabilistic Programs. Vol. 20–22, ACM, 2016,
pp. 327–42, doi:10.1145/2837614.2837639.
short: K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, in:, ACM, 2016, pp. 327–342.
conference:
end_date: 2016-01-22
location: St. Petersburg, FL, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2016-01-20
date_created: 2018-12-11T11:52:01Z
date_published: 2016-01-11T00:00:00Z
date_updated: 2023-09-19T14:38:41Z
day: '11'
department:
- _id: KrCh
doi: 10.1145/2837614.2837639
ec_funded: 1
external_id:
arxiv:
- '1510.08517'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1510.08517
month: '01'
oa: 1
oa_version: Preprint
page: 327 - 342
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: ACM
publist_id: '5760'
quality_controlled: '1'
related_material:
record:
- id: '5993'
relation: later_version
status: public
scopus_import: 1
status: public
title: Algorithmic analysis of qualitative and quantitative termination problems for
affine probabilistic programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 20-22
year: '2016'
...
---
_id: '1477'
abstract:
- lang: eng
text: We consider partially observable Markov decision processes (POMDPs) with ω-regular
conditions specified as parity objectives. The class of ω-regular languages provides
a robust specification language to express properties in verification, and parity
objectives are canonical forms to express them. The qualitative analysis problem
given a POMDP and a parity objective asks whether there is a strategy to ensure
that the objective is satisfied with probability 1 (resp. positive probability).
While the qualitative analysis problems are undecidable even for special cases
of parity objectives, we establish decidability (with optimal complexity) for
POMDPs with all parity objectives under finite-memory strategies. We establish
optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative
analysis problems under finite-memory strategies for POMDPs with parity objectives.
We also present a practical approach, where we design heuristics to deal with
the exponential complexity, and have applied our implementation on a number of
POMDP examples.
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: Mathieu
full_name: Tracol, Mathieu
id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
last_name: Tracol
citation:
ama: Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable
Markov decision processes with ω-regular objectives. Journal of Computer and
System Sciences. 2016;82(5):878-911. doi:10.1016/j.jcss.2016.02.009
apa: Chatterjee, K., Chmelik, M., & Tracol, M. (2016). What is decidable about
partially observable Markov decision processes with ω-regular objectives. Journal
of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2016.02.009
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable
about Partially Observable Markov Decision Processes with ω-Regular Objectives.”
Journal of Computer and System Sciences. Elsevier, 2016. https://doi.org/10.1016/j.jcss.2016.02.009.
ieee: K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially
observable Markov decision processes with ω-regular objectives,” Journal of
Computer and System Sciences, vol. 82, no. 5. Elsevier, pp. 878–911, 2016.
ista: Chatterjee K, Chmelik M, Tracol M. 2016. What is decidable about partially
observable Markov decision processes with ω-regular objectives. Journal of Computer
and System Sciences. 82(5), 878–911.
mla: Chatterjee, Krishnendu, et al. “What Is Decidable about Partially Observable
Markov Decision Processes with ω-Regular Objectives.” Journal of Computer and
System Sciences, vol. 82, no. 5, Elsevier, 2016, pp. 878–911, doi:10.1016/j.jcss.2016.02.009.
short: K. Chatterjee, M. Chmelik, M. Tracol, Journal of Computer and System Sciences
82 (2016) 878–911.
date_created: 2018-12-11T11:52:15Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-02-23T12:24:38Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.jcss.2016.02.009
ec_funded: 1
external_id:
arxiv:
- '1309.2802'
intvolume: ' 82'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1309.2802
month: '08'
oa: 1
oa_version: Preprint
page: 878 - 911
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Elsevier
publist_id: '5718'
quality_controlled: '1'
related_material:
record:
- id: '2295'
relation: earlier_version
status: public
- id: '5400'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: What is decidable about partially observable Markov decision processes with
ω-regular objectives
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 82
year: '2016'
...
---
_id: '5445'
abstract:
- lang: eng
text: 'We consider the quantitative analysis problem for interprocedural control-flow
graphs (ICFGs). The input consists of an ICFG, a positive weight function that
assigns every transition a positive integer-valued number, and a labelling of
the transitions (events) as good, bad, and neutral events. The weight function
assigns to each transition a numerical value that represents ameasure of how good
or bad an event is. The quantitative analysis problem asks whether there is a
run of the ICFG where the ratio of the sum of the numerical weights of good events
versus the sum of weights of bad events in the long-run is at least a given threshold
(or equivalently, to compute the maximal ratio among all valid paths in the ICFG).
The quantitative analysis problem for ICFGs can be solved in polynomial time,
and we present an efficient and practical algorithm for the problem. We show that
several problems relevant for static program analysis, such as estimating the
worst-case execution time of a program or the average energy consumption of a
mobile application, can be modeled in our framework. We have implemented our algorithm
as a tool in the Java Soot framework. We demonstrate the effectiveness of our
approach with two case studies. First, we show that our framework provides a sound
approach (no false positives) for the analysis of inefficiently-used containers.
Second, we show that our approach can also be used for static profiling of programs
which reasons about methods that are frequently invoked. Our experimental results
show that our tool scales to relatively large benchmarks, and discovers relevant
and useful information that can be used to optimize performance of the programs. '
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Pavlogiannis A, Velner Y. Quantitative Interprocedural Analysis.
IST Austria; 2016. doi:10.15479/AT:IST-2016-523-v1-1
apa: Chatterjee, K., Pavlogiannis, A., & Velner, Y. (2016). Quantitative
interprocedural analysis. IST Austria. https://doi.org/10.15479/AT:IST-2016-523-v1-1
chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. Quantitative
Interprocedural Analysis. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-523-v1-1.
ieee: K. Chatterjee, A. Pavlogiannis, and Y. Velner, Quantitative interprocedural
analysis. IST Austria, 2016.
ista: Chatterjee K, Pavlogiannis A, Velner Y. 2016. Quantitative interprocedural
analysis, IST Austria, 33p.
mla: Chatterjee, Krishnendu, et al. Quantitative Interprocedural Analysis.
IST Austria, 2016, doi:10.15479/AT:IST-2016-523-v1-1.
short: K. Chatterjee, A. Pavlogiannis, Y. Velner, Quantitative Interprocedural Analysis,
IST Austria, 2016.
date_created: 2018-12-12T11:39:22Z
date_published: 2016-03-31T00:00:00Z
date_updated: 2023-02-23T10:06:22Z
day: '31'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2016-523-v1-1
file:
- access_level: open_access
checksum: cef516fa091925b5868813e355268fb4
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:52Z
date_updated: 2020-07-14T12:46:58Z
file_id: '5513'
file_name: IST-2016-523-v1+1_main.pdf
file_size: 1012204
relation: main_file
file_date_updated: 2020-07-14T12:46:58Z
has_accepted_license: '1'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '523'
related_material:
record:
- id: '1604'
relation: later_version
status: public
status: public
title: Quantitative interprocedural analysis
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5449'
abstract:
- lang: eng
text: "The fixation probability is the probability that a new mutant introduced
in a homogeneous population eventually takes over the entire population.\r\nThe
fixation probability is a fundamental quantity of natural selection, and known
to depend on the population structure.\r\nAmplifiers of natural selection are
population structures which increase the fixation probability of advantageous
mutants, as compared to the baseline case of well-mixed populations. In this work
we focus on symmetric population structures represented as undirected graphs.
In the regime of undirected graphs, the strongest amplifier known has been the
Star graph, and the existence of undirected graphs with stronger amplification
properties has remained open for over a decade.\r\nIn this work we present the
Comet and Comet-swarm families of undirected graphs. We show that for a range
of fitness values of the mutants, the Comet and Comet-swarm graphs have fixation
probability strictly larger than the fixation probability of the Star graph, for
fixed population size and at the limit of large populations, respectively."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: 'Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on Undirected
Population Structures: Comets Beat Stars. IST Austria; 2016. doi:10.15479/AT:IST-2016-648-v1-1'
apa: 'Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Amplification
on undirected population structures: Comets beat stars. IST Austria. https://doi.org/10.15479/AT:IST-2016-648-v1-1'
chicago: 'Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. Amplification on Undirected Population Structures: Comets Beat Stars.
IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-648-v1-1.'
ieee: 'A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Amplification
on undirected population structures: Comets beat stars. IST Austria, 2016.'
ista: 'Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Amplification on
undirected population structures: Comets beat stars, IST Austria, 22p.'
mla: 'Pavlogiannis, Andreas, et al. Amplification on Undirected Population Structures:
Comets Beat Stars. IST Austria, 2016, doi:10.15479/AT:IST-2016-648-v1-1.'
short: 'A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Amplification on Undirected
Population Structures: Comets Beat Stars, IST Austria, 2016.'
date_created: 2018-12-12T11:39:24Z
date_published: 2016-11-09T00:00:00Z
date_updated: 2023-02-23T12:22:21Z
day: '09'
ddc:
- '519'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2016-648-v1-1
file:
- access_level: open_access
checksum: 8345a8c1e7d7f0cd92516d182b7fc59e
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:07Z
date_updated: 2020-07-14T12:46:58Z
file_id: '5529'
file_name: IST-2016-648-v1+1_tr.pdf
file_size: 1264221
relation: main_file
file_date_updated: 2020-07-14T12:46:58Z
has_accepted_license: '1'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Updated Version
page: '22'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '648'
related_material:
record:
- id: '512'
relation: later_version
status: public
status: public
title: 'Amplification on undirected population structures: Comets beat stars'
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5451'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Strong Amplifiers of Natural
Selection. IST Austria; 2016. doi:10.15479/AT:IST-2016-728-v1-1
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Strong
amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2016-728-v1-1
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-728-v1-1.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Strong amplifiers
of natural selection. IST Austria, 2016.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Strong amplifiers
of natural selection, IST Austria, 34p.
mla: Pavlogiannis, Andreas, et al. Strong Amplifiers of Natural Selection.
IST Austria, 2016, doi:10.15479/AT:IST-2016-728-v1-1.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Strong Amplifiers of
Natural Selection, IST Austria, 2016.
date_created: 2018-12-12T11:39:24Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2023-02-23T12:27:05Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2016-728-v1-1
file:
- access_level: open_access
checksum: 7b8bb17c322c0556acba6ac169fa71c1
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:04Z
date_updated: 2020-07-14T12:46:59Z
file_id: '5465'
file_name: IST-2016-728-v1+1_main.pdf
file_size: 1014732
relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '34'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '728'
status: public
title: Strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5452'
alternative_title:
- IST Austria Technical Report
article_processing_charge: No
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Arbitrarily Strong Amplifiers
of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2017-728-v2-1
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Arbitrarily
strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2017-728-v2-1
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria,
2016. https://doi.org/10.15479/AT:IST-2017-728-v2-1.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Arbitrarily strong
amplifiers of natural selection. IST Austria, 2016.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong
amplifiers of natural selection, IST Austria, 32p.
mla: Pavlogiannis, Andreas, et al. Arbitrarily Strong Amplifiers of Natural Selection.
IST Austria, 2016, doi:10.15479/AT:IST-2017-728-v2-1.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong
Amplifiers of Natural Selection, IST Austria, 2016.
date_created: 2018-12-12T11:39:25Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2024-02-21T13:48:42Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-728-v2-1
ec_funded: 1
file:
- access_level: open_access
checksum: 58e895f26c82f560c0f0989bf8b08599
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:52:59Z
date_updated: 2020-07-14T12:46:59Z
file_id: '5460'
file_name: IST-2017-728-v2+1_main.pdf
file_size: 811558
relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '32'
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '750'
related_material:
record:
- id: '5453'
relation: later_version
status: public
- id: '5559'
relation: popular_science
status: public
status: public
title: Arbitrarily strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5453'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Arbitrarily Strong Amplifiers
of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2017-749-v3-1
apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Arbitrarily
strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2017-749-v3-1
chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
Nowak. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria,
2016. https://doi.org/10.15479/AT:IST-2017-749-v3-1.
ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Arbitrarily strong
amplifiers of natural selection. IST Austria, 2016.
ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong
amplifiers of natural selection, IST Austria, 34p.
mla: Pavlogiannis, Andreas, et al. Arbitrarily Strong Amplifiers of Natural Selection.
IST Austria, 2016, doi:10.15479/AT:IST-2017-749-v3-1.
short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong
Amplifiers of Natural Selection, IST Austria, 2016.
date_created: 2018-12-12T11:39:25Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2023-02-23T12:27:07Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-749-v3-1
file:
- access_level: open_access
checksum: 83b0313dab3bff4bdb6ac38695026fda
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:13Z
date_updated: 2020-07-14T12:46:59Z
file_id: '5474'
file_name: IST-2017-749-v3+1_main.pdf
file_size: 1015647
relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '34'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '755'
related_material:
record:
- id: '5452'
relation: earlier_version
status: public
status: public
title: Arbitrarily strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1068'
abstract:
- lang: eng
text: 'Games on graphs provide the appropriate framework to study several central
problems in computer science, such as verification and synthesis of reactive systems.
One of the most basic objectives for games on graphs is the liveness (or Büchi)
objective that given a target set of vertices requires that some vertex in the
target set is visited infinitely often. We study generalized Büchi objectives
(i.e., conjunction of liveness objectives), and implications between two generalized
Büchi objectives (known as GR(1) objectives), that arise in numerous applications
in computer-aided verification. We present improved algorithms and conditional
super-linear lower bounds based on widely believed assumptions about the complexity
of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider
graph games with n vertices, m edges, and generalized Büchi objectives with k
conjunctions. First, we present an algorithm with running time O(k*n^2), improving
the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm
is optimal for dense graphs under (A1). Second, we show that the basic algorithm
for the problem is optimal for sparse graphs when the target sets have constant
size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions
in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1
k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time
algorithm for m > n^{1.5}. '
acknowledgement: K. C., M. H., and W. D. are partially supported by the Vienna Science
and Technology Fund (WWTF) through project ICT15-003. K. C. is partially supported
by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC
Start grant (279307
alternative_title:
- LIPIcs
article_number: '25'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Wolfgang
full_name: Dvorák, Wolfgang
last_name: Dvorák
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Veronika
full_name: Loitzenbauer, Veronika
last_name: Loitzenbauer
citation:
ama: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. Conditionally optimal
algorithms for generalized Büchi Games. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2016. doi:10.4230/LIPIcs.MFCS.2016.25'
apa: 'Chatterjee, K., Dvorák, W., Henzinger, M. H., & Loitzenbauer, V. (2016).
Conditionally optimal algorithms for generalized Büchi Games (Vol. 58). Presented
at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow, Poland:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2016.25'
chicago: Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Veronika
Loitzenbauer. “Conditionally Optimal Algorithms for Generalized Büchi Games,”
Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.MFCS.2016.25.
ieee: 'K. Chatterjee, W. Dvorák, M. H. Henzinger, and V. Loitzenbauer, “Conditionally
optimal algorithms for generalized Büchi Games,” presented at the MFCS: Mathematical
Foundations of Computer Science (SG), Krakow, Poland, 2016, vol. 58.'
ista: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. 2016. Conditionally
optimal algorithms for generalized Büchi Games. MFCS: Mathematical Foundations
of Computer Science (SG), LIPIcs, vol. 58, 25.'
mla: Chatterjee, Krishnendu, et al. Conditionally Optimal Algorithms for Generalized
Büchi Games. Vol. 58, 25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016, doi:10.4230/LIPIcs.MFCS.2016.25.
short: K. Chatterjee, W. Dvorák, M.H. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Krakow, Poland
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2016-08-22
date_created: 2018-12-11T11:49:58Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2025-06-02T08:53:50Z
day: '01'
ddc:
- '000'
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.MFCS.2016.25
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:02Z
date_updated: 2018-12-12T10:16:02Z
file_id: '5187'
file_name: IST-2017-779-v1+1_LIPIcs-MFCS-2016-25.pdf
file_size: 632786
relation: main_file
file_date_updated: 2018-12-12T10:16:02Z
has_accepted_license: '1'
intvolume: ' 58'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/3.0/
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6317'
pubrep_id: '779'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Conditionally optimal algorithms for generalized Büchi Games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 58
year: '2016'
...
---
_id: '1069'
abstract:
- lang: eng
text: "The Continuous Skolem Problem asks whether a real-valued function satisfying
a linear differen-\r\ntial equation has a zero in a given interval of real numbers.
This is a fundamental reachability\r\nproblem for continuous linear dynamical
systems, such as linear hybrid automata and continuous-\r\ntime Markov chains.
Decidability of the problem is currently open – indeed decidability is open\r\neven
for the sub-problem in which a zero is sought in a bounded interval. In this paper
we show\r\ndecidability of the bounded problem subject to Schanuel’s Conjecture,
a unifying conjecture in\r\ntranscendental number theory. We furthermore analyse
the unbounded problem in terms of the\r\nfrequencies of the differential equation,
that is, the imaginary parts of the characteristic roots.\r\nWe show that the
unbounded problem can be reduced to the bounded problem if there is at most\r\none
rationally linearly independent frequency, or if there are two rationally linearly
independent\r\nfrequencies and all characteristic roots are simple. We complete
the picture by showing that de-\r\ncidability of the unbounded problem in the
case of two (or more) rationally linearly independent\r\nfrequencies would entail
a major new effectiveness result in Diophantine approximation, namely\r\ncomputability
of the Diophantine-approximation types of all real algebraic numbers."
acknowledgement: 'Ventsislav Chonev is supported by Austrian Science Fund (FWF) NFN
Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and ERC
Advanced Grant (267989: QUAREM).'
alternative_title:
- LIPIcs
article_number: '100'
author:
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
- first_name: Joël
full_name: Ouaknine, Joël
last_name: Ouaknine
- first_name: James
full_name: Worrell, James
last_name: Worrell
citation:
ama: 'Chonev VK, Ouaknine J, Worrell J. On the skolem problem for continuous linear
dynamical systems. In: Vol 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik;
2016. doi:10.4230/LIPIcs.ICALP.2016.100'
apa: 'Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the skolem problem
for continuous linear dynamical systems (Vol. 55). Presented at the ICALP: Automata,
Languages and Programming, Rome, Italy: Schloss Dagstuhl- Leibniz-Zentrum fur
Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2016.100'
chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Skolem
Problem for Continuous Linear Dynamical Systems,” Vol. 55. Schloss Dagstuhl- Leibniz-Zentrum
fur Informatik, 2016. https://doi.org/10.4230/LIPIcs.ICALP.2016.100.
ieee: 'V. K. Chonev, J. Ouaknine, and J. Worrell, “On the skolem problem for continuous
linear dynamical systems,” presented at the ICALP: Automata, Languages and Programming,
Rome, Italy, 2016, vol. 55.'
ista: 'Chonev VK, Ouaknine J, Worrell J. 2016. On the skolem problem for continuous
linear dynamical systems. ICALP: Automata, Languages and Programming, LIPIcs,
vol. 55, 100.'
mla: Chonev, Ventsislav K., et al. On the Skolem Problem for Continuous Linear
Dynamical Systems. Vol. 55, 100, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016, doi:10.4230/LIPIcs.ICALP.2016.100.
short: V.K. Chonev, J. Ouaknine, J. Worrell, in:, Schloss Dagstuhl- Leibniz-Zentrum
fur Informatik, 2016.
conference:
end_date: 2016-07-15
location: Rome, Italy
name: 'ICALP: Automata, Languages and Programming'
start_date: 2016-07-12
date_created: 2018-12-11T11:49:59Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:48:03Z
day: '01'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ICALP.2016.100
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:26Z
date_updated: 2018-12-12T10:16:26Z
file_id: '5213'
file_name: IST-2017-778-v1+1_LIPIcs-ICALP-2016-100.pdf
file_size: 521415
relation: main_file
file_date_updated: 2018-12-12T10:16:26Z
has_accepted_license: '1'
intvolume: ' 55'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik
publist_id: '6314'
pubrep_id: '778'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the skolem problem for continuous linear dynamical systems
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 55
year: '2016'
...