---
_id: '9888'
abstract:
- lang: eng
text: Detailed description of the experimental prodedures, data analyses and additional
statistical analyses of the results.
article_processing_charge: No
author:
- first_name: Stephan
full_name: Wolf, Stephan
last_name: Wolf
- first_name: Dino
full_name: Mcmahon, Dino
last_name: Mcmahon
- first_name: Ka
full_name: Lim, Ka
last_name: Lim
- first_name: Christopher
full_name: Pull, Christopher
id: 3C7F4840-F248-11E8-B48F-1D18A9856A87
last_name: Pull
orcid: 0000-0003-1122-3982
- first_name: Suzanne
full_name: Clark, Suzanne
last_name: Clark
- first_name: Robert
full_name: Paxton, Robert
last_name: Paxton
- first_name: Juliet
full_name: Osborne, Juliet
last_name: Osborne
citation:
ama: Wolf S, Mcmahon D, Lim K, et al. Supporting information. 2014. doi:10.1371/journal.pone.0103989.s003
apa: Wolf, S., Mcmahon, D., Lim, K., Pull, C., Clark, S., Paxton, R., & Osborne,
J. (2014). Supporting information. Public Library of Science. https://doi.org/10.1371/journal.pone.0103989.s003
chicago: Wolf, Stephan, Dino Mcmahon, Ka Lim, Christopher Pull, Suzanne Clark, Robert
Paxton, and Juliet Osborne. “Supporting Information.” Public Library of Science,
2014. https://doi.org/10.1371/journal.pone.0103989.s003.
ieee: S. Wolf et al., “Supporting information.” Public Library of Science,
2014.
ista: Wolf S, Mcmahon D, Lim K, Pull C, Clark S, Paxton R, Osborne J. 2014. Supporting
information, Public Library of Science, 10.1371/journal.pone.0103989.s003.
mla: Wolf, Stephan, et al. Supporting Information. Public Library of Science,
2014, doi:10.1371/journal.pone.0103989.s003.
short: S. Wolf, D. Mcmahon, K. Lim, C. Pull, S. Clark, R. Paxton, J. Osborne, (2014).
date_created: 2021-08-11T14:17:53Z
date_updated: 2025-09-29T11:45:40Z
day: '06'
department:
- _id: SyCr
doi: 10.1371/journal.pone.0103989.s003
month: '08'
oa_version: Published Version
publisher: Public Library of Science
related_material:
record:
- id: '2086'
relation: used_in_publication
status: public
status: public
title: Supporting information
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2014'
...
---
_id: '9931'
abstract:
- lang: eng
text: Gene duplication is important in evolution, because it provides new raw material
for evolutionary adaptations. Several existing hypotheses about the causes of
duplicate retention and diversification differ in their emphasis on gene dosage,
subfunctionalization, and neofunctionalization. Little experimental data exist
on the relative importance of gene expression changes and changes in coding regions
for the evolution of duplicate genes. Furthermore, we do not know how strongly
the environment could affect this importance. To address these questions, we performed
evolution experiments with the TEM-1 beta lactamase gene in Escherichia coli to
study the initial stages of duplicate gene evolution in the laboratory. We mimicked
tandem duplication by inserting two copies of the TEM-1 gene on the same plasmid.
We then subjected these copies to repeated cycles of mutagenesis and selection
in various environments that contained antibiotics in different combinations and
concentrations. Our experiments showed that gene dosage is the most important
factor in the initial stages of duplicate gene evolution, and overshadows the
importance of point mutations in the coding region.
acknowledgement: We thank the Functional Genomics Center Zurich for its service in
generating sequencing data, M. Ackermann and E. Hayden for helpful discussions,
A. de Visser for comments on earlier versions of this manuscript, and M. Moser for
help with quantitative PCR. This work was supported by Swiss National Science Foundation
(grant 315230–129708), as well as through the YeastX project of SystemsX.ch, and
the University Priority Research Program in Systems Biology at the University of
Zurich. RD acknowledges support from the Forschungskredit program of the University
of Zurich. The authors declare no conflict of interest.
article_processing_charge: No
article_type: original
author:
- first_name: Riddhiman
full_name: Dhar, Riddhiman
last_name: Dhar
- first_name: Tobias
full_name: Bergmiller, Tobias
id: 2C471CFA-F248-11E8-B48F-1D18A9856A87
last_name: Bergmiller
orcid: 0000-0001-5396-4346
- first_name: Andreas
full_name: Wagner, Andreas
last_name: Wagner
citation:
ama: Dhar R, Bergmiller T, Wagner A. Increased gene dosage plays a predominant role
in the initial stages of evolution of duplicate TEM-1 beta lactamase genes. Evolution.
2014;68(6):1775-1791. doi:10.1111/evo.12373
apa: Dhar, R., Bergmiller, T., & Wagner, A. (2014). Increased gene dosage plays
a predominant role in the initial stages of evolution of duplicate TEM-1 beta
lactamase genes. Evolution. Wiley. https://doi.org/10.1111/evo.12373
chicago: Dhar, Riddhiman, Tobias Bergmiller, and Andreas Wagner. “Increased Gene
Dosage Plays a Predominant Role in the Initial Stages of Evolution of Duplicate
TEM-1 Beta Lactamase Genes.” Evolution. Wiley, 2014. https://doi.org/10.1111/evo.12373.
ieee: R. Dhar, T. Bergmiller, and A. Wagner, “Increased gene dosage plays a predominant
role in the initial stages of evolution of duplicate TEM-1 beta lactamase genes,”
Evolution, vol. 68, no. 6. Wiley, pp. 1775–1791, 2014.
ista: Dhar R, Bergmiller T, Wagner A. 2014. Increased gene dosage plays a predominant
role in the initial stages of evolution of duplicate TEM-1 beta lactamase genes.
Evolution. 68(6), 1775–1791.
mla: Dhar, Riddhiman, et al. “Increased Gene Dosage Plays a Predominant Role in
the Initial Stages of Evolution of Duplicate TEM-1 Beta Lactamase Genes.” Evolution,
vol. 68, no. 6, Wiley, 2014, pp. 1775–91, doi:10.1111/evo.12373.
short: R. Dhar, T. Bergmiller, A. Wagner, Evolution 68 (2014) 1775–1791.
date_created: 2021-08-17T09:03:09Z
date_published: 2014-06-03T00:00:00Z
date_updated: 2025-09-29T13:20:48Z
day: '03'
department:
- _id: CaGu
doi: 10.1111/evo.12373
external_id:
isi:
- '000337558900019'
pmid:
- '24495000'
intvolume: ' 68'
isi: 1
issue: '6'
language:
- iso: eng
month: '06'
oa_version: None
page: 1775-1791
pmid: 1
publication: Evolution
publication_identifier:
eissn:
- 1558-5646
issn:
- 0014-3820
publication_status: published
publisher: Wiley
quality_controlled: '1'
related_material:
record:
- id: '9932'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Increased gene dosage plays a predominant role in the initial stages of evolution
of duplicate TEM-1 beta lactamase genes
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 68
year: '2014'
...
---
_id: '9932'
abstract:
- lang: eng
text: Gene duplication is important in evolution, because it provides new raw material
for evolutionary adaptations. Several existing hypotheses about the causes of
duplicate retention and diversification differ in their emphasis on gene dosage,
sub-functionalization, and neo-functionalization. Little experimental data exists
on the relative importance of gene expression changes and changes in coding regions
for the evolution of duplicate genes. Furthermore, we do not know how strongly
the environment could affect this importance. To address these questions, we performed
evolution experiments with the TEM-1 beta lactamase gene in E. coli to study the
initial stages of duplicate gene evolution in the laboratory. We mimicked tandem
duplication by inserting two copies of the TEM-1 gene on the same plasmid. We
then subjected these copies to repeated cycles of mutagenesis and selection in
various environments that contained antibiotics in different combinations and
concentrations. Our experiments showed that gene dosage is the most important
factor in the initial stages of duplicate gene evolution, and overshadows the
importance of point mutations in the coding region.
article_processing_charge: No
author:
- first_name: Riddhiman
full_name: Dhar, Riddhiman
last_name: Dhar
- first_name: Tobias
full_name: Bergmiller, Tobias
id: 2C471CFA-F248-11E8-B48F-1D18A9856A87
last_name: Bergmiller
orcid: 0000-0001-5396-4346
- first_name: Andreas
full_name: Wagner, Andreas
last_name: Wagner
citation:
ama: 'Dhar R, Bergmiller T, Wagner A. Data from: Increased gene dosage plays a predominant
role in the initial stages of evolution of duplicate TEM-1 beta lactamase genes.
2014. doi:10.5061/dryad.jc402'
apa: 'Dhar, R., Bergmiller, T., & Wagner, A. (2014). Data from: Increased gene
dosage plays a predominant role in the initial stages of evolution of duplicate
TEM-1 beta lactamase genes. Dryad. https://doi.org/10.5061/dryad.jc402'
chicago: 'Dhar, Riddhiman, Tobias Bergmiller, and Andreas Wagner. “Data from: Increased
Gene Dosage Plays a Predominant Role in the Initial Stages of Evolution of Duplicate
TEM-1 Beta Lactamase Genes.” Dryad, 2014. https://doi.org/10.5061/dryad.jc402.'
ieee: 'R. Dhar, T. Bergmiller, and A. Wagner, “Data from: Increased gene dosage
plays a predominant role in the initial stages of evolution of duplicate TEM-1
beta lactamase genes.” Dryad, 2014.'
ista: 'Dhar R, Bergmiller T, Wagner A. 2014. Data from: Increased gene dosage plays
a predominant role in the initial stages of evolution of duplicate TEM-1 beta
lactamase genes, Dryad, 10.5061/dryad.jc402.'
mla: 'Dhar, Riddhiman, et al. Data from: Increased Gene Dosage Plays a Predominant
Role in the Initial Stages of Evolution of Duplicate TEM-1 Beta Lactamase Genes.
Dryad, 2014, doi:10.5061/dryad.jc402.'
short: R. Dhar, T. Bergmiller, A. Wagner, (2014).
date_created: 2021-08-17T09:11:40Z
date_published: 2014-01-27T00:00:00Z
date_updated: 2025-09-29T13:20:47Z
day: '27'
department:
- _id: CaGu
doi: 10.5061/dryad.jc402
main_file_link:
- open_access: '1'
url: https://doi.org/10.5061/dryad.jc402
month: '01'
oa: 1
oa_version: Published Version
publisher: Dryad
related_material:
record:
- id: '9931'
relation: used_in_publication
status: public
status: public
title: 'Data from: Increased gene dosage plays a predominant role in the initial stages
of evolution of duplicate TEM-1 beta lactamase genes'
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2014'
...
---
_id: '2905'
abstract:
- lang: eng
text: "Persistent homology is a recent grandchild of homology that has found use
in\r\nscience and engineering as well as in mathematics. This paper surveys the
method as well\r\nas the applications, neglecting completeness in favor of highlighting
ideas and directions."
acknowledgement: This research is partially supported by NSF under grant DBI-0820624,
by ESF under the Research Networking Programme, and by the Russian Government Project
11.G34.31.0053.
article_processing_charge: No
author:
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Dmitriy
full_name: Morozovy, Dmitriy
last_name: Morozovy
citation:
ama: 'Edelsbrunner H, Morozovy D. Persistent homology: Theory and practice. In:
EMS Press; 2014:31-50. doi:10.4171/120-1/3'
apa: 'Edelsbrunner, H., & Morozovy, D. (2014). Persistent homology: Theory and
practice (pp. 31–50). Presented at the ECM: European Congress of Mathematics,
Kraków, Poland: EMS Press. https://doi.org/10.4171/120-1/3'
chicago: 'Edelsbrunner, Herbert, and Dmitriy Morozovy. “Persistent Homology: Theory
and Practice,” 31–50. EMS Press, 2014. https://doi.org/10.4171/120-1/3.'
ieee: 'H. Edelsbrunner and D. Morozovy, “Persistent homology: Theory and practice,”
presented at the ECM: European Congress of Mathematics, Kraków, Poland, 2014,
pp. 31–50.'
ista: 'Edelsbrunner H, Morozovy D. 2014. Persistent homology: Theory and practice.
ECM: European Congress of Mathematics, 31–50.'
mla: 'Edelsbrunner, Herbert, and Dmitriy Morozovy. Persistent Homology: Theory
and Practice. EMS Press, 2014, pp. 31–50, doi:10.4171/120-1/3.'
short: H. Edelsbrunner, D. Morozovy, in:, EMS Press, 2014, pp. 31–50.
conference:
end_date: 2012-07-07
location: Kraków, Poland
name: 'ECM: European Congress of Mathematics'
start_date: 2012-07-02
corr_author: '1'
das_tickbox: '1'
date_created: 2018-12-11T12:00:16Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2026-07-06T11:55:48Z
day: '01'
ddc:
- '000'
department:
- _id: HeEd
doi: 10.4171/120-1/3
file:
- access_level: open_access
checksum: 1d4a046f1af945c407c5c4d411d4c5e4
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:43Z
date_updated: 2020-07-14T12:45:52Z
file_id: '5232'
file_name: IST-2016-544-v1+1_2012-P-11-PHTheoryPractice.pdf
file_size: 435320
relation: main_file
file_date_updated: 2020-07-14T12:45:52Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 31 - 50
publication_status: published
publisher: EMS Press
publist_id: '3842'
pubrep_id: '544'
quality_controlled: '1'
status: public
title: 'Persistent homology: Theory and practice'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '1904'
abstract:
- lang: eng
text: We prove a Strichartz inequality for a system of orthonormal functions, with
an optimal behavior of the constant in the limit of a large number of functions.
The estimate generalizes the usual Strichartz inequality, in the same fashion
as the Lieb-Thirring inequality generalizes the Sobolev inequality. As an application,
we consider the Schrödinger equation with a time-dependent potential and we show
the existence of the wave operator in Schatten spaces.
article_processing_charge: No
arxiv: 1
author:
- first_name: Rupert
full_name: Frank, Rupert
last_name: Frank
- first_name: Mathieu
full_name: Lewin, Mathieu
last_name: Lewin
- first_name: Élliott
full_name: Lieb, Élliott
last_name: Lieb
- first_name: Robert
full_name: Seiringer, Robert
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
citation:
ama: Frank R, Lewin M, Lieb É, Seiringer R. Strichartz inequality for orthonormal
functions. Journal of the European Mathematical Society. 2014;16(7):1507-1526.
doi:10.4171/JEMS/467
apa: Frank, R., Lewin, M., Lieb, É., & Seiringer, R. (2014). Strichartz inequality
for orthonormal functions. Journal of the European Mathematical Society.
EMS Press. https://doi.org/10.4171/JEMS/467
chicago: Frank, Rupert, Mathieu Lewin, Élliott Lieb, and Robert Seiringer. “Strichartz
Inequality for Orthonormal Functions.” Journal of the European Mathematical
Society. EMS Press, 2014. https://doi.org/10.4171/JEMS/467.
ieee: R. Frank, M. Lewin, É. Lieb, and R. Seiringer, “Strichartz inequality for
orthonormal functions,” Journal of the European Mathematical Society, vol.
16, no. 7. EMS Press, pp. 1507–1526, 2014.
ista: Frank R, Lewin M, Lieb É, Seiringer R. 2014. Strichartz inequality for orthonormal
functions. Journal of the European Mathematical Society. 16(7), 1507–1526.
mla: Frank, Rupert, et al. “Strichartz Inequality for Orthonormal Functions.” Journal
of the European Mathematical Society, vol. 16, no. 7, EMS Press, 2014, pp.
1507–26, doi:10.4171/JEMS/467.
short: R. Frank, M. Lewin, É. Lieb, R. Seiringer, Journal of the European Mathematical
Society 16 (2014) 1507–1526.
das_tickbox: '1'
date_created: 2018-12-11T11:54:38Z
date_published: 2014-08-23T00:00:00Z
date_updated: 2026-07-06T11:56:08Z
day: '23'
department:
- _id: RoSe
doi: 10.4171/JEMS/467
external_id:
arxiv:
- '1306.1309'
isi:
- '000345494900006'
intvolume: ' 16'
isi: 1
issue: '7'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1306.1309
month: '08'
oa: 1
oa_version: Submitted Version
page: 1507 - 1526
project:
- _id: 26450934-B435-11E9-9278-68D0E5697425
name: NSERC Postdoctoral fellowship
publication: Journal of the European Mathematical Society
publication_status: published
publisher: EMS Press
publist_id: '5191'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Strichartz inequality for orthonormal functions
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16
year: '2014'
...
---
_id: '2233'
abstract:
- lang: eng
text: ' A discounted-sum automaton (NDA) is a nondeterministic finite automaton
with edge weights, valuing a run by the discounted sum of visited edge weights.
More precisely, the weight in the i-th position of the run is divided by λi, where
the discount factor λ is a fixed rational number greater than 1. The value of
a word is the minimal value of the automaton runs on it. Discounted summation
is a common and useful measuring scheme, especially for infinite sequences, reflecting
the assumption that earlier weights are more important than later weights. Unfortunately,
determinization of NDAs, which is often essential in formal verification, is,
in general, not possible. We provide positive news, showing that every NDA with
an integral discount factor is determinizable. We complete the picture by proving
that the integers characterize exactly the discount factors that guarantee determinizability:
for every nonintegral rational discount factor λ, there is a nondeterminizable
λ-NDA. We also prove that the class of NDAs with integral discount factors enjoys
closure under the algebraic operations min, max, addition, and subtraction, which
is not the case for general NDAs nor for deterministic NDAs. For general NDAs,
we look into approximate determinization, which is always possible as the influence
of a word''s suffix decays. We show that the naive approach, of unfolding the
automaton computations up to a sufficient level, is doubly exponential in the
discount factor. We provide an alternative construction for approximate determinization,
which is singly exponential in the discount factor, in the precision, and in the
number of states. We also prove matching lower bounds, showing that the exponential
dependency on each of these three parameters cannot be avoided. All our results
hold equally for automata over finite words and for automata over infinite words. '
article_processing_charge: No
author:
- first_name: Udi
full_name: Boker, Udi
last_name: Boker
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Boker U, Henzinger TA. Exact and approximate determinization of discounted-sum
automata. Logical Methods in Computer Science. 2014;10(1). doi:10.2168/LMCS-10(1:10)2014
apa: Boker, U., & Henzinger, T. A. (2014). Exact and approximate determinization
of discounted-sum automata. Logical Methods in Computer Science. International
Federation for Computational Logic. https://doi.org/10.2168/LMCS-10(1:10)2014
chicago: Boker, Udi, and Thomas A Henzinger. “Exact and Approximate Determinization
of Discounted-Sum Automata.” Logical Methods in Computer Science. International
Federation for Computational Logic, 2014. https://doi.org/10.2168/LMCS-10(1:10)2014.
ieee: U. Boker and T. A. Henzinger, “Exact and approximate determinization of discounted-sum
automata,” Logical Methods in Computer Science, vol. 10, no. 1. International
Federation for Computational Logic, 2014.
ista: Boker U, Henzinger TA. 2014. Exact and approximate determinization of discounted-sum
automata. Logical Methods in Computer Science. 10(1).
mla: Boker, Udi, and Thomas A. Henzinger. “Exact and Approximate Determinization
of Discounted-Sum Automata.” Logical Methods in Computer Science, vol.
10, no. 1, International Federation for Computational Logic, 2014, doi:10.2168/LMCS-10(1:10)2014.
short: U. Boker, T.A. Henzinger, Logical Methods in Computer Science 10 (2014).
das_tickbox: '1'
date_created: 2018-12-11T11:56:28Z
date_published: 2014-02-13T00:00:00Z
date_updated: 2026-07-06T13:22:33Z
day: '13'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.2168/LMCS-10(1:10)2014
ec_funded: 1
external_id:
isi:
- '000333744700015'
file:
- access_level: open_access
checksum: 9f6ea2e2d8d4a32ff0becc29d835bbf8
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:07:45Z
date_updated: 2020-07-14T12:45:34Z
file_id: '4643'
file_name: IST-2015-389-v1+1_1401.3957.pdf
file_size: 550936
relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: ' 10'
isi: 1
issue: '1'
language:
- iso: eng
month: '02'
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: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Logical Methods in Computer Science
publication_identifier:
issn:
- 1860-5974
publication_status: published
publisher: International Federation for Computational Logic
publist_id: '4728'
pubrep_id: '389'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Exact and approximate determinization of discounted-sum automata
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10
year: '2014'
...
---
_id: '2234'
abstract:
- lang: eng
text: We study Markov decision processes (MDPs) with multiple limit-average (or
mean-payoff) functions. We consider two different objectives, namely, expectation
and satisfaction objectives. Given an MDP with κ limit-average functions, in the
expectation objective the goal is to maximize the expected limit-average value,
and in the satisfaction objective the goal is to maximize the probability of runs
such that the limit-average value stays above a given vector. We show that under
the expectation objective, in contrast to the case of one limit-average function,
both randomization and memory are necessary for strategies even for ε-approximation,
and that finite-memory randomized strategies are sufficient for achieving Pareto
optimal values. Under the satisfaction objective, in contrast to the case of one
limit-average function, infinite memory is necessary for strategies achieving
a specific value (i.e. randomized finite-memory strategies are not sufficient),
whereas memoryless randomized strategies are sufficient for ε-approximation, for
all ε > 0. We further prove that the decision problems for both expectation
and satisfaction objectives can be solved in polynomial time and the trade-off
curve (Pareto curve) can be ε-approximated in time polynomial in the size of the
MDP and 1/ε, and exponential in the number of limit-average functions, for all
ε > 0. Our analysis also reveals flaws in previous work for MDPs with multiple
mean-payoff functions under the expectation objective, corrects the flaws, and
allows us to obtain improved results.
article_processing_charge: No
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Václav
full_name: Brožek, Václav
last_name: Brožek
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
citation:
ama: Brázdil T, Brožek V, Chatterjee K, Forejt V, Kučera A. Markov decision processes
with multiple long-run average objectives. Logical Methods in Computer Science.
2014;10(1). doi:10.2168/LMCS-10(1:13)2014
apa: Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., & Kučera, A. (2014).
Markov decision processes with multiple long-run average objectives. Logical
Methods in Computer Science. International Federation for Computational Logic.
https://doi.org/10.2168/LMCS-10(1:13)2014
chicago: Brázdil, Tomáš, Václav Brožek, Krishnendu Chatterjee, Vojtěch Forejt, and
Antonín Kučera. “Markov Decision Processes with Multiple Long-Run Average Objectives.”
Logical Methods in Computer Science. International Federation for Computational
Logic, 2014. https://doi.org/10.2168/LMCS-10(1:13)2014.
ieee: T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, and A. Kučera, “Markov decision
processes with multiple long-run average objectives,” Logical Methods in Computer
Science, vol. 10, no. 1. International Federation for Computational Logic,
2014.
ista: Brázdil T, Brožek V, Chatterjee K, Forejt V, Kučera A. 2014. Markov decision
processes with multiple long-run average objectives. Logical Methods in Computer
Science. 10(1).
mla: Brázdil, Tomáš, et al. “Markov Decision Processes with Multiple Long-Run Average
Objectives.” Logical Methods in Computer Science, vol. 10, no. 1, International
Federation for Computational Logic, 2014, doi:10.2168/LMCS-10(1:13)2014.
short: T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, A. Kučera, Logical Methods
in Computer Science 10 (2014).
das_tickbox: '1'
date_created: 2018-12-11T11:56:29Z
date_published: 2014-02-14T00:00:00Z
date_updated: 2026-07-06T13:23:35Z
day: '14'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.2168/LMCS-10(1:13)2014
ec_funded: 1
external_id:
isi:
- '000333744700001'
file:
- access_level: open_access
checksum: 803edcc2d8c1acfba44a9ec43a5eb9f0
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:07:57Z
date_updated: 2020-07-14T12:45:34Z
file_id: '4656'
file_name: IST-2016-428-v1+1_1104.3489.pdf
file_size: 375388
relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: ' 10'
isi: 1
issue: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Logical Methods in Computer Science
publication_identifier:
issn:
- 1860-5974
publication_status: published
publisher: International Federation for Computational Logic
publist_id: '4727'
pubrep_id: '428'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Markov decision processes with multiple long-run average objectives
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: 10
year: '2014'
...
---
_id: '2265'
abstract:
- lang: eng
text: Coordinated migration of newly-born neurons to their target territories is
essential for correct neuronal circuit assembly in the developing brain. Although
a cohort of signaling pathways has been implicated in the regulation of cortical
projection neuron migration, the precise molecular mechanisms and how a balanced
interplay of cell-autonomous and non-autonomous functions of candidate signaling
molecules controls the discrete steps in the migration process, are just being
revealed. In this chapter, I will focally review recent advances that improved
our understanding of the cell-autonomous and possible cell-nonautonomous functions
of the evolutionarily conserved LIS1/NDEL1-complex in regulating the sequential
steps of cortical projection neuron migration. I will then elaborate on the emerging
concept that the Reelin signaling pathway, acts exactly at precise stages in the
course of cortical projection neuron migration. Lastly, I will discuss how finely
tuned transcriptional programs and downstream effectors govern particular aspects
in driving radial migration at discrete stages and how they regulate the precise
positioning of cortical projection neurons in the developing cerebral cortex.
alternative_title:
- Advances in Experimental Medicine and Biology
article_processing_charge: No
author:
- first_name: Simon
full_name: Hippenmeyer, Simon
id: 37B36620-F248-11E8-B48F-1D18A9856A87
last_name: Hippenmeyer
orcid: 0000-0003-2279-1061
citation:
ama: 'Hippenmeyer S. Molecular pathways controlling the sequential steps of cortical
projection neuron migration. In: Nguyen L, ed. Cellular and Molecular Control
of Neuronal Migration. Vol 800. Springer; 2014:1-24. doi:10.1007/978-94-007-7687-6_1'
apa: Hippenmeyer, S. (2014). Molecular pathways controlling the sequential steps
of cortical projection neuron migration. In L. Nguyen (Ed.), Cellular and Molecular
Control of Neuronal Migration (Vol. 800, pp. 1–24). Springer. https://doi.org/10.1007/978-94-007-7687-6_1
chicago: Hippenmeyer, Simon. “Molecular Pathways Controlling the Sequential Steps
of Cortical Projection Neuron Migration.” In Cellular and Molecular Control
of Neuronal Migration, edited by Laurent Nguyen, 800:1–24. Springer, 2014.
https://doi.org/10.1007/978-94-007-7687-6_1.
ieee: S. Hippenmeyer, “Molecular pathways controlling the sequential steps of cortical
projection neuron migration,” in Cellular and Molecular Control of Neuronal
Migration, vol. 800, L. Nguyen, Ed. Springer, 2014, pp. 1–24.
ista: 'Hippenmeyer S. 2014.Molecular pathways controlling the sequential steps of
cortical projection neuron migration. In: Cellular and Molecular Control of Neuronal
Migration. Advances in Experimental Medicine and Biology, vol. 800, 1–24.'
mla: Hippenmeyer, Simon. “Molecular Pathways Controlling the Sequential Steps of
Cortical Projection Neuron Migration.” Cellular and Molecular Control of Neuronal
Migration, edited by Laurent Nguyen, vol. 800, Springer, 2014, pp. 1–24, doi:10.1007/978-94-007-7687-6_1.
short: S. Hippenmeyer, in:, L. Nguyen (Ed.), Cellular and Molecular Control of Neuronal
Migration, Springer, 2014, pp. 1–24.
corr_author: '1'
das_tickbox: '1'
date_created: 2018-12-11T11:56:39Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2026-07-07T13:04:40Z
day: '01'
department:
- _id: SiHi
doi: 10.1007/978-94-007-7687-6_1
editor:
- first_name: Laurent
full_name: Nguyen, Laurent
last_name: Nguyen
external_id:
isi:
- '000333646000002'
intvolume: ' 800'
isi: 1
language:
- iso: eng
month: '01'
oa_version: None
page: 1 - 24
publication: Cellular and Molecular Control of Neuronal Migration
publication_status: published
publisher: Springer
publist_id: '4679'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Molecular pathways controlling the sequential steps of cortical projection
neuron migration
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 800
year: '2014'
...
---
_id: '2027'
abstract:
- lang: eng
text: We present a general framework for applying machine-learning algorithms to
the verification of Markov decision processes (MDPs). The primary goal of these
techniques is to improve performance by avoiding an exhaustive exploration of
the state space. Our framework focuses on probabilistic reachability, which is
a core property for verification, and is illustrated through two distinct instantiations.
The first assumes that full knowledge of the MDP is available, and performs a
heuristic-driven partial exploration of the model, yielding precise lower and
upper bounds on the required probability. The second tackles the case where we
may only sample the MDP, and yields probabilistic guarantees, again in terms of
both the lower and upper bounds, which provides efficient stopping criteria for
the approximation. The latter is the first extension of statistical model checking
for unbounded properties inMDPs. In contrast with other related techniques, our
approach is not restricted to time-bounded (finite-horizon) or discounted properties,
nor does it assume any particular properties of the MDP. We also show how our
methods extend to LTL objectives. We present experimental results showing the
performance of our framework on several examples.
acknowledgement: This research was funded in part by the European Research Council
(ERC) under grant agreement 246967 (VERIWARE), by the EU FP7 project HIERATIC, by
the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Marta
full_name: Kwiatkowska, Marta
last_name: Kwiatkowska
- first_name: David
full_name: Parker, David
last_name: Parker
- first_name: Mateusz
full_name: Ujma, Mateusz
last_name: Ujma
citation:
ama: 'Brázdil T, Chatterjee K, Chmelik M, et al. Verification of Markov decision
processes using learning algorithms. In: 12th International Symposium on Automated
Technology for Verification and Analysis. Vol 8837. Springer; 2014:98-114.
doi:10.1007/978-3-319-11936-6_8'
apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska,
M., … Ujma, M. (2014). Verification of Markov decision processes using learning
algorithms. In 12th International Symposium on Automated Technology for Verification
and Analysis (Vol. 8837, pp. 98–114). Sydney, Australia: Springer. https://doi.org/10.1007/978-3-319-11936-6_8'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt,
Jan Kretinsky, Marta Kwiatkowska, David Parker, and Mateusz Ujma. “Verification
of Markov Decision Processes Using Learning Algorithms.” In 12th International
Symposium on Automated Technology for Verification and Analysis, 8837:98–114.
Springer, 2014. https://doi.org/10.1007/978-3-319-11936-6_8.
ieee: T. Brázdil et al., “Verification of Markov decision processes using
learning algorithms,” in 12th International Symposium on Automated Technology
for Verification and Analysis, Sydney, Australia, 2014, vol. 8837, pp. 98–114.
ista: 'Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M,
Parker D, Ujma M. 2014. Verification of Markov decision processes using learning
algorithms. 12th International Symposium on Automated Technology for Verification
and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS,
vol. 8837, 98–114.'
mla: Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning
Algorithms.” 12th International Symposium on Automated Technology for Verification
and Analysis, vol. 8837, Springer, 2014, pp. 98–114, doi:10.1007/978-3-319-11936-6_8.
short: T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska,
D. Parker, M. Ujma, in:, 12th International Symposium on Automated Technology
for Verification and Analysis, Springer, 2014, pp. 98–114.
conference:
end_date: 2014-11-07
location: Sydney, Australia
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2014-11-03
das_tickbox: '1'
date_created: 2018-12-11T11:55:17Z
date_published: 2014-11-01T00:00:00Z
date_updated: 2026-07-07T13:15:34Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-11936-6_8
ec_funded: 1
external_id:
arxiv:
- '1402.2967'
intvolume: ' 8837'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1402.2967
month: '11'
oa: 1
oa_version: Submitted Version
page: 98 - 114
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 26241A12-B435-11E9-9278-68D0E5697425
grant_number: '24696'
name: Light-regulated ligand traps for spatio-temporal inhibition of cell signaling
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 12th International Symposium on Automated Technology for Verification
and Analysis
publication_status: published
publisher: Springer
publist_id: '5046'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Verification of Markov decision processes using learning algorithms
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8837
year: '2014'
...
---
_id: '2028'
abstract:
- lang: eng
text: 'Understanding the dynamics of noisy neurons remains an important challenge
in neuroscience. Here, we describe a simple probabilistic model that accurately
describes the firing behavior in a large class (type II) of neurons. To demonstrate
the usefulness of this model, we show how it accurately predicts the interspike
interval (ISI) distributions, bursting patterns and mean firing rates found by:
(1) simulations of the classic Hodgkin-Huxley model with channel noise, (2) experimental
data from squid giant axon with a noisy input current and (3) experimental data
on noisy firing from a neuron within the suprachiasmatic nucleus (SCN). This simple
model has 6 parameters, however, in some cases, two of these parameters are coupled
and only 5 parameters account for much of the known behavior. From these parameters,
many properties of spiking can be found through simple calculation. Thus, we show
how the complex effects of noise can be understood through a simple and general
probabilistic model.'
acknowledgement: 'This work is supported by AFOSR grant FA 9550-11-1-0165, program
grant RPG 24/2012 from the Human Frontiers of Science (DBF) and travel support from
the European Commission Marie Curie International Reintegration Grant PIRG04-GA-2008-239429
(KB). DP was supported by NIHR01 GM104987 and the Wyss Institute of Biologically
Inspired Engineering. '
article_processing_charge: No
author:
- first_name: Katarina
full_name: Bodova, Katarina
id: 2BA24EA0-F248-11E8-B48F-1D18A9856A87
last_name: Bodova
orcid: 0000-0002-7214-0171
- first_name: David
full_name: Paydarfar, David
last_name: Paydarfar
- first_name: Daniel
full_name: Forger, Daniel
last_name: Forger
citation:
ama: Bodova K, Paydarfar D, Forger D. Characterizing spiking in noisy type II neurons.
Journal of Theoretical Biology. 2014;365:40-54. doi:10.1016/j.jtbi.2014.09.041
apa: Bodova, K., Paydarfar, D., & Forger, D. (2014). Characterizing spiking
in noisy type II neurons. Journal of Theoretical Biology. Academic Press.
https://doi.org/10.1016/j.jtbi.2014.09.041
chicago: Bodova, Katarina, David Paydarfar, and Daniel Forger. “Characterizing Spiking
in Noisy Type II Neurons.” Journal of Theoretical Biology. Academic Press,
2014. https://doi.org/10.1016/j.jtbi.2014.09.041.
ieee: K. Bodova, D. Paydarfar, and D. Forger, “Characterizing spiking in noisy type
II neurons,” Journal of Theoretical Biology, vol. 365. Academic Press,
pp. 40–54, 2014.
ista: Bodova K, Paydarfar D, Forger D. 2014. Characterizing spiking in noisy type
II neurons. Journal of Theoretical Biology. 365, 40–54.
mla: Bodova, Katarina, et al. “Characterizing Spiking in Noisy Type II Neurons.”
Journal of Theoretical Biology, vol. 365, Academic Press, 2014, pp. 40–54,
doi:10.1016/j.jtbi.2014.09.041.
short: K. Bodova, D. Paydarfar, D. Forger, Journal of Theoretical Biology 365 (2014)
40–54.
corr_author: '1'
das_tickbox: '1'
date_created: 2018-12-11T11:55:18Z
date_published: 2014-10-12T00:00:00Z
date_updated: 2026-07-07T13:13:09Z
day: '12'
ddc:
- '570'
department:
- _id: GaTk
doi: 10.1016/j.jtbi.2014.09.041
external_id:
isi:
- '000347267200005'
file:
- access_level: open_access
checksum: a9dbae18d3233b3dab6944fd3f2cd49e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:58Z
date_updated: 2020-07-14T12:45:25Z
file_id: '5316'
file_name: IST-2016-444-v1+1_1-s2.0-S0022519314005888-main.pdf
file_size: 2679222
relation: main_file
file_date_updated: 2020-07-14T12:45:25Z
has_accepted_license: '1'
intvolume: ' 365'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 40 - 54
publication: Journal of Theoretical Biology
publication_status: published
publisher: Academic Press
publist_id: '5043'
pubrep_id: '444'
quality_controlled: '1'
related_material:
link:
- relation: erratum
url: https://doi.org/10.1016/j.jtbi.2015.03.013
scopus_import: '1'
status: public
title: Characterizing spiking in noisy type II neurons
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 365
year: '2014'
...
---
_id: '5415'
abstract:
- lang: eng
text: 'Recently there has been a significant effort to add quantitative properties
in formal verification and synthesis. While weighted automata over finite and
infinite words provide a natural and flexible framework to express quantitative
properties, perhaps surprisingly, several basic system properties such as average
response time cannot be expressed with weighted automata. In this work, we introduce
nested weighted automata as a new formalism for expressing important quantitative
properties such as average response time. We establish an almost complete decidability
picture for the basic decision problems for nested weighted automata, and illustrate
its applicability in several domains. '
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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Otop J. Nested Weighted Automata. IST Austria;
2014. doi:10.15479/AT:IST-2014-170-v1-1
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2014). Nested weighted
automata. IST Austria. https://doi.org/10.15479/AT:IST-2014-170-v1-1
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted
Automata. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-170-v1-1.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata.
IST Austria, 2014.
ista: Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria,
27p.
mla: Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria,
2014, doi:10.15479/AT:IST-2014-170-v1-1.
short: K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria,
2014.
date_created: 2018-12-12T11:39:12Z
date_published: 2014-02-19T00:00:00Z
date_updated: 2026-07-07T14:01:10Z
day: '19'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2014-170-v1-1
file:
- access_level: open_access
checksum: 31f90dcf2cf899c3f8c6427cfcc2b3c7
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:36Z
date_updated: 2020-07-14T12:46:48Z
file_id: '5497'
file_name: IST-2014-170-v1+1_main.pdf
file_size: 573457
relation: main_file
file_date_updated: 2020-07-14T12:46:48Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '27'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '170'
related_material:
record:
- id: '5436'
relation: later_version
status: public
- id: '1656'
relation: later_version
status: public
- id: '467'
relation: later_version
status: public
status: public
title: Nested weighted automata
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '2038'
abstract:
- lang: eng
text: Recently, there has been an effort to add quantitative objectives to formal
verification and synthesis. We introduce and investigate the extension of temporal
logics with quantitative atomic assertions. At the heart of quantitative objectives
lies the accumulation of values along a computation. It is often the accumulated
sum, as with energy objectives, or the accumulated average, as with mean-payoff
objectives. We investigate the extension of temporal logics with the prefix-accumulation
assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable
of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the
accumulated sum and average of the values of v from the beginning of the computation
up to the current point in time. We also allow the path-accumulation assertions
LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an
entire infinite computation. We study the border of decidability for such quantitative
extensions of various temporal logics. In particular, we show that extending the
fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with
both prefix-accumulation assertions, or extending LTL with both path-accumulation
assertions, results in temporal logics whose model-checking problem is decidable.
Moreover, the prefix-accumulation assertions may be generalized with "controlled
accumulation," allowing, for example, to specify constraints on the average
waiting time between a request and a grant. On the negative side, we show that
this branching-time logic is, in a sense, the maximal logic with one or both of
the prefix-accumulation assertions that permits a decidable model-checking procedure.
Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL,
makes the problem undecidable.
acknowledgement: The research was supported in part by ERC Starting grant 278410 (QUALITY).
article_number: '27'
article_processing_charge: No
article_type: original
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- 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: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with
accumulative values. ACM Transactions on Computational Logic. 2014;15(4).
doi:10.1145/2629686
apa: Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2014). Temporal
specifications with accumulative values. ACM Transactions on Computational
Logic. ACM. https://doi.org/10.1145/2629686
chicago: Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman.
“Temporal Specifications with Accumulative Values.” ACM Transactions on Computational
Logic. ACM, 2014. https://doi.org/10.1145/2629686.
ieee: U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications
with accumulative values,” ACM Transactions on Computational Logic, vol.
15, no. 4. ACM, 2014.
ista: Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2014. Temporal specifications
with accumulative values. ACM Transactions on Computational Logic. 15(4), 27.
mla: Boker, Udi, et al. “Temporal Specifications with Accumulative Values.” ACM
Transactions on Computational Logic, vol. 15, no. 4, 27, ACM, 2014, doi:10.1145/2629686.
short: U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on
Computational Logic 15 (2014).
das_tickbox: '1'
date_created: 2018-12-11T11:55:21Z
date_published: 2014-09-16T00:00:00Z
date_updated: 2026-07-07T14:01:43Z
day: '16'
ddc:
- '000'
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2629686
ec_funded: 1
external_id:
isi:
- '000345570700002'
file:
- access_level: open_access
checksum: 354c41d37500b56320afce94cf9a99c2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:59Z
date_updated: 2020-07-14T12:45:26Z
file_id: '4851'
file_name: IST-2014-192-v1+1_AccumulativeValues.pdf
file_size: 346184
relation: main_file
file_date_updated: 2020-07-14T12:45:26Z
has_accepted_license: '1'
intvolume: ' 15'
isi: 1
issue: '4'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: ACM Transactions on Computational Logic
publication_status: published
publisher: ACM
publist_id: '5013'
pubrep_id: '192'
quality_controlled: '1'
related_material:
record:
- id: '5385'
relation: earlier_version
status: public
- id: '3356'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Temporal specifications with accumulative values
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2014'
...
---
OA_place: repository
OA_type: green
_id: '1903'
abstract:
- lang: eng
text: 'We consider two-player zero-sum partial-observation stochastic games on graphs.
Based on the information available to the players these games can be classified
as follows: (a) general partial-observation (both players have partial view of
the game); (b) one-sided partial-observation (one player has partial-observation
and the other player has complete-observation); and (c) perfect-observation (both
players have complete view of the game). The one-sided partial-observation games
subsumes the important special case of one-player partial-observation stochastic
games (or partial-observation Markov decision processes (POMDPs)). Based on the
randomization available for the strategies, (a) the players may not be allowed
to use randomization (pure strategies), or (b) they may choose a probability distribution
over actions but the actual random choice is external and not visible to the player
(actions invisible), or (c) they may use full randomization. We consider all these
classes of games with reachability, and parity objectives that can express all
ω-regular objectives. The analysis problems are classified into the qualitative
analysis that asks for the existence of a strategy that ensures the objective
with probability 1; and the quantitative analysis that asks for the existence
of a strategy that ensures the objective with probability at least λ (0,1). In
this talk we will cover a wide range of results: for perfect-observation games;
for POMDPs; for one-sided partial-observation games; and for general partial-observation
games.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: 'Chatterjee K. Partial-observation stochastic reachability and parity games.
In: Vol 8634. Springer; 2014:1-4. doi:10.1007/978-3-662-44522-8_1'
apa: 'Chatterjee, K. (2014). Partial-observation stochastic reachability and parity
games (Vol. 8634, pp. 1–4). Presented at the MFCS: Mathematical Foundations of
Computer Science, Budapest, Hungary: Springer. https://doi.org/10.1007/978-3-662-44522-8_1'
chicago: Chatterjee, Krishnendu. “Partial-Observation Stochastic Reachability and
Parity Games,” 8634:1–4. Springer, 2014. https://doi.org/10.1007/978-3-662-44522-8_1.
ieee: 'K. Chatterjee, “Partial-observation stochastic reachability and parity games,”
presented at the MFCS: Mathematical Foundations of Computer Science, Budapest,
Hungary, 2014, vol. 8634, no. PART 1, pp. 1–4.'
ista: 'Chatterjee K. 2014. Partial-observation stochastic reachability and parity
games. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 8634, 1–4.'
mla: Chatterjee, Krishnendu. Partial-Observation Stochastic Reachability and
Parity Games. Vol. 8634, no. PART 1, Springer, 2014, pp. 1–4, doi:10.1007/978-3-662-44522-8_1.
short: K. Chatterjee, in:, Springer, 2014, pp. 1–4.
conference:
end_date: 2014-08-29
location: Budapest, Hungary
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2014-08-25
corr_author: '1'
date_created: 2018-12-11T11:54:38Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2026-07-07T14:01:25Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-44522-8_1
ec_funded: 1
intvolume: ' 8634'
issue: PART 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.15479/AT:IST-2011-0007
month: '01'
oa: 1
oa_version: Preprint
page: 1 - 4
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_status: published
publisher: Springer
publist_id: '5192'
pubrep_id: '141'
quality_controlled: '1'
related_material:
record:
- id: '5381'
relation: earlier_version
status: public
- id: '2211'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Partial-observation stochastic reachability and parity games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8634
year: '2014'
...
---
_id: '2211'
abstract:
- lang: eng
text: 'In two-player finite-state stochastic games of partial observation on graphs,
in every state of the graph, the players simultaneously choose an action, and
their joint actions determine a probability distribution over the successor states.
The game is played for infinitely many rounds and thus the players construct an
infinite path in the graph. We consider reachability objectives where the first
player tries to ensure a target state to be visited almost-surely (i.e., with
probability 1) or positively (i.e., with positive probability), no matter the
strategy of the second player. We classify such games according to the information
and to the power of randomization available to the players. On the basis of information,
the game can be one-sided with either (a) player 1, or (b) player 2 having partial
observation (and the other player has perfect observation), or two-sided with
(c) both players having partial observation. On the basis of randomization, (a)
the players may not be allowed to use randomization (pure strategies), or (b)
they may choose a probability distribution over actions but the actual random
choice is external and not visible to the player (actions invisible), or (c) they
may use full randomization. Our main results for pure strategies are as follows:
(1) For one-sided games with player 2 having perfect observation we show that
(in contrast to full randomized strategies) belief-based (subset-construction
based) strategies are not sufficient, and we present an exponential upper bound
on memory both for almost-sure and positive winning strategies; we show that the
problem of deciding the existence of almost-sure and positive winning strategies
for player 1 is EXPTIME-complete and present symbolic algorithms that avoid the
explicit exponential construction. (2) For one-sided games with player 1 having
perfect observation we show that nonelementarymemory is both necessary and sufficient
for both almost-sure and positive winning strategies. (3) We show that for the
general (two-sided) case finite-memory strategies are sufficient for both positive
and almost-sure winning, and at least nonelementary memory is required. We establish
the equivalence of the almost-sure winning problems for pure strategies and for
randomized strategies with actions invisible. Our equivalence result exhibit serious
flaws in previous results of the literature: we show a nonelementary memory lower
bound for almost-sure winning whereas an exponential upper bound was previously
claimed.'
article_number: '16'
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
citation:
ama: 'Chatterjee K, Doyen L. Partial-observation stochastic games: How to win when
belief fails. ACM Transactions on Computational Logic. 2014;15(2). doi:10.1145/2579821'
apa: 'Chatterjee, K., & Doyen, L. (2014). Partial-observation stochastic games:
How to win when belief fails. ACM Transactions on Computational Logic.
ACM. https://doi.org/10.1145/2579821'
chicago: 'Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic
Games: How to Win When Belief Fails.” ACM Transactions on Computational Logic.
ACM, 2014. https://doi.org/10.1145/2579821.'
ieee: 'K. Chatterjee and L. Doyen, “Partial-observation stochastic games: How to
win when belief fails,” ACM Transactions on Computational Logic, vol. 15,
no. 2. ACM, 2014.'
ista: 'Chatterjee K, Doyen L. 2014. Partial-observation stochastic games: How to
win when belief fails. ACM Transactions on Computational Logic. 15(2), 16.'
mla: 'Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic
Games: How to Win When Belief Fails.” ACM Transactions on Computational Logic,
vol. 15, no. 2, 16, ACM, 2014, doi:10.1145/2579821.'
short: K. Chatterjee, L. Doyen, ACM Transactions on Computational Logic 15 (2014).
das_tickbox: '1'
date_created: 2018-12-11T11:56:21Z
date_published: 2014-04-01T00:00:00Z
date_updated: 2026-07-07T14:01:26Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2579821
external_id:
arxiv:
- '1107.2141'
isi:
- '000336005000006'
intvolume: ' 15'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1107.2141
month: '04'
oa: 1
oa_version: Preprint
publication: ACM Transactions on Computational Logic
publication_status: published
publisher: ACM
publist_id: '4759'
quality_controlled: '1'
related_material:
record:
- id: '5381'
relation: earlier_version
status: public
- id: '1903'
relation: earlier_version
status: public
- id: '2955'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: 'Partial-observation stochastic games: How to win when belief fails'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2014'
...
---
_id: '2054'
abstract:
- lang: eng
text: 'We study two-player concurrent games on finite-state graphs played for an
infinite number of rounds, where in each round, the two players (player 1 and
player 2) choose their moves independently and simultaneously; the current state
and the two moves determine the successor state. The objectives are ω-regular
winning conditions specified as parity objectives. We consider the qualitative
analysis problems: the computation of the almost-sure and limit-sure winning set
of states, where player 1 can ensure to win with probability 1 and with probability
arbitrarily close to 1, respectively. In general the almost-sure and limit-sure
winning strategies require both infinite-memory as well as infinite-precision
(to describe probabilities). While the qualitative analysis problem for concurrent
parity games with infinite-memory, infinite-precision randomized strategies was
studied before, we study the bounded-rationality problem for qualitative analysis
of concurrent parity games, where the strategy set for player 1 is restricted
to bounded-resource strategies. In terms of precision, strategies can be deterministic,
uniform, finite-precision, or infinite-precision; and in terms of memory, strategies
can be memoryless, finite-memory, or infinite-memory. We present a precise and
complete characterization of the qualitative winning sets for all combinations
of classes of strategies. In particular, we show that uniform memoryless strategies
are as powerful as finite-precision infinite-memory strategies, and infinite-precision
memoryless strategies are as powerful as infinite-precision finite-memory strategies.
We show that the winning sets can be computed in (n2d+3) time, where n is the
size of the game structure and 2d is the number of priorities (or colors), and
our algorithms are symbolic. The membership problem of whether a state belongs
to a winning set can be decided in NP ∩ coNP. Our symbolic algorithms are based
on a characterization of the winning sets as μ-calculus formulas, however, our
μ-calculus formulas are crucially different from the ones for concurrent parity
games (without bounded rationality); and our memoryless witness strategy constructions
are significantly different from the infinite-memory witness strategy constructions
for concurrent parity games.'
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
citation:
ama: 'Chatterjee K. Qualitative concurrent parity games: Bounded rationality. In:
Baldan P, Gorla D, eds. Lecture Notes in Computer Science (Including Subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:544-559. doi:10.1007/978-3-662-44584-6_37'
apa: 'Chatterjee, K. (2014). Qualitative concurrent parity games: Bounded rationality.
In P. Baldan & D. Gorla (Eds.), Lecture Notes in Computer Science (including
subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
(Vol. 8704, pp. 544–559). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.1007/978-3-662-44584-6_37'
chicago: 'Chatterjee, Krishnendu. “Qualitative Concurrent Parity Games: Bounded
Rationality.” In Lecture Notes in Computer Science (Including Subseries Lecture
Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited
by Paolo Baldan and Daniele Gorla, 8704:544–59. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2014. https://doi.org/10.1007/978-3-662-44584-6_37.'
ieee: 'K. Chatterjee, “Qualitative concurrent parity games: Bounded rationality,”
in Lecture Notes in Computer Science (including subseries Lecture Notes in
Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy,
2014, vol. 8704, pp. 544–559.'
ista: 'Chatterjee K. 2014. Qualitative concurrent parity games: Bounded rationality.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory,
LNCS, vol. 8704, 544–559.'
mla: 'Chatterjee, Krishnendu. “Qualitative Concurrent Parity Games: Bounded Rationality.”
Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan
and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2014, pp. 544–59, doi:10.1007/978-3-662-44584-6_37.'
short: K. Chatterjee, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer
Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014,
pp. 544–559.
conference:
end_date: 2014-09-05
location: Rome, Italy
name: 'CONCUR: Concurrency Theory'
start_date: 2014-09-02
corr_author: '1'
date_created: 2018-12-11T11:55:27Z
date_published: 2014-09-01T00:00:00Z
date_updated: 2026-07-07T14:02:37Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-44584-6_37
ec_funded: 1
editor:
- first_name: Paolo
full_name: Baldan, Paolo
last_name: Baldan
- first_name: Daniele
full_name: Gorla, Daniele
last_name: Gorla
intvolume: ' 8704'
language:
- iso: eng
month: '09'
oa_version: None
page: 544 - 559
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: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4992'
quality_controlled: '1'
related_material:
record:
- id: '3354'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: 'Qualitative concurrent parity games: Bounded rationality'
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 8704
year: '2014'
...
---
_id: '535'
abstract:
- lang: eng
text: Energy games belong to a class of turn-based two-player infinite-duration
games played on a weighted directed graph. It is one of the rare and intriguing
combinatorial problems that lie in NP∩co-NP, but are not known to be in P. The
existence of polynomial-time algorithms has been a major open problem for decades
and apart from pseudopolynomial algorithms there is no algorithm that solves any
non-trivial subclass in polynomial time. In this paper, we give several results
based on the weight structures of the graph. First, we identify a notion of penalty
and present a polynomial-time algorithm when the penalty is large. Our algorithm
is the first polynomial-time algorithm on a large class of weighted graphs. It
includes several worst-case instances on which previous algorithms, such as value
iteration and random facet algorithms, require at least sub-exponential time.
Our main technique is developing the first non-trivial approximation algorithm
and showing how to convert it to an exact algorithm. Moreover, we show that in
a practical case in verification where weights are clustered around a constant
number of values, the energy game problem can be solved in polynomial time. We
also show that the problem is still as hard as in general when the clique-width
is bounded or the graph is strongly ergodic, suggesting that restricting the graph
structure does not necessarily help.
article_processing_charge: No
article_type: original
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: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Sebastian
full_name: Krinninger, Sebastian
last_name: Krinninger
- first_name: Danupon
full_name: Nanongkai, Danupon
last_name: Nanongkai
citation:
ama: Chatterjee K, Henzinger M, Krinninger S, Nanongkai D. Polynomial-time algorithms
for energy games with special weight structures. Algorithmica. 2014;70(3):457-492.
doi:10.1007/s00453-013-9843-7
apa: Chatterjee, K., Henzinger, M., Krinninger, S., & Nanongkai, D. (2014).
Polynomial-time algorithms for energy games with special weight structures. Algorithmica.
Springer. https://doi.org/10.1007/s00453-013-9843-7
chicago: Chatterjee, Krishnendu, Monika Henzinger, Sebastian Krinninger, and Danupon
Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.”
Algorithmica. Springer, 2014. https://doi.org/10.1007/s00453-013-9843-7.
ieee: K. Chatterjee, M. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time
algorithms for energy games with special weight structures,” Algorithmica,
vol. 70, no. 3. Springer, pp. 457–492, 2014.
ista: Chatterjee K, Henzinger M, Krinninger S, Nanongkai D. 2014. Polynomial-time
algorithms for energy games with special weight structures. Algorithmica. 70(3),
457–492.
mla: Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games
with Special Weight Structures.” Algorithmica, vol. 70, no. 3, Springer,
2014, pp. 457–92, doi:10.1007/s00453-013-9843-7.
short: K. Chatterjee, M. Henzinger, S. Krinninger, D. Nanongkai, Algorithmica 70
(2014) 457–492.
date_created: 2018-12-11T11:47:01Z
date_published: 2014-11-01T00:00:00Z
date_updated: 2026-07-08T05:50:38Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/s00453-013-9843-7
ec_funded: 1
external_id:
arxiv:
- '1604.08234'
isi:
- '000340552300005'
intvolume: ' 70'
isi: 1
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.08234
month: '11'
oa: 1
oa_version: Preprint
page: 457 - 492
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: Algorithmica
publication_status: published
publisher: Springer
publist_id: '7282'
quality_controlled: '1'
related_material:
record:
- id: '10905'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Polynomial-time algorithms for energy games with special weight structures
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 70
year: '2014'
...
---
_id: '1872'
abstract:
- lang: eng
text: Extensionality axioms are common when reasoning about data collections, such
as arrays and functions in program analysis, or sets in mathematics. An extensionality
axiom asserts that two collections are equal if they consist of the same elements
at the same indices. Using extensionality is often required to show that two collections
are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly,
while humans have no problem with proving such set identities using extensionality,
they are very hard for superposition theorem provers because of the calculi they
use. In this paper we show how addition of a new inference rule, called extensionality
resolution, allows first-order theorem provers to easily solve problems no modern
first-order theorem prover can solve. We illustrate this by running the VAMPIRE
theorem prover with extensionality resolution on a number of set theory and array
problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP
library of first-order problems that were never solved before by any prover.
acknowledgement: This research was supported in part by the Austrian National Research
Network RiSE (S11410-N23).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Laura
full_name: Kovács, Laura
last_name: Kovács
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
orcid: 0000-0001-7745-9117
- first_name: Andrei
full_name: Voronkov, Andrei
last_name: Voronkov
citation:
ama: 'Gupta A, Kovács L, Kragl B, Voronkov A. Extensional crisis and proving identity.
In: 12th International Symposium on Automated Technology for Verification and
Analysis. Vol 8837. Springer; 2014:185-200. doi:10.1007/978-3-319-11936-6_14'
apa: 'Gupta, A., Kovács, L., Kragl, B., & Voronkov, A. (2014). Extensional crisis
and proving identity. In 12th International Symposium on Automated Technology
for Verification and Analysis (Vol. 8837, pp. 185–200). Sydney, Australia:
Springer. https://doi.org/10.1007/978-3-319-11936-6_14'
chicago: Gupta, Ashutosh, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. “Extensional
Crisis and Proving Identity.” In 12th International Symposium on Automated
Technology for Verification and Analysis, 8837:185–200. Springer, 2014. https://doi.org/10.1007/978-3-319-11936-6_14.
ieee: A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, “Extensional crisis and proving
identity,” in 12th International Symposium on Automated Technology for Verification
and Analysis, Sydney, Australia, 2014, vol. 8837, pp. 185–200.
ista: 'Gupta A, Kovács L, Kragl B, Voronkov A. 2014. Extensional crisis and proving
identity. 12th International Symposium on Automated Technology for Verification
and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS,
vol. 8837, 185–200.'
mla: Gupta, Ashutosh, et al. “Extensional Crisis and Proving Identity.” 12th
International Symposium on Automated Technology for Verification and Analysis,
vol. 8837, Springer, 2014, pp. 185–200, doi:10.1007/978-3-319-11936-6_14.
short: A. Gupta, L. Kovács, B. Kragl, A. Voronkov, in:, 12th International Symposium
on Automated Technology for Verification and Analysis, Springer, 2014, pp. 185–200.
conference:
end_date: 2014-11-07
location: Sydney, Australia
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2014-11-03
das_tickbox: '1'
date_created: 2018-12-11T11:54:28Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2026-07-08T06:49:33Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-11936-6_14
ec_funded: 1
file:
- access_level: open_access
checksum: af4bd3fc1f4c93075e4dc5cbf625fe7b
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:15Z
date_updated: 2020-07-14T12:45:19Z
file_id: '4801'
file_name: IST-2016-641-v1+1_atva2014.pdf
file_size: 244294
relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: ' 8837'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 185 - 200
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication: 12th International Symposium on Automated Technology for Verification
and Analysis
publication_status: published
publisher: Springer
publist_id: '5226'
pubrep_id: '641'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Extensional crisis and proving identity
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8837
year: '2014'
...
---
_id: '1999'
abstract:
- lang: eng
text: Selection for disease control is believed to have contributed to shape the
organisation of insect societies — leading to interaction patterns that mitigate
disease transmission risk within colonies, conferring them ‘organisational immunity’.
Recent studies combining epidemiological models with social network analysis have
identified general properties of interaction networks that may hinder propagation
of infection within groups. These can be prophylactic and/or induced upon pathogen
exposure. Here we review empirical evidence for these two types of organisational
immunity in social insects and describe the individual-level behaviours that underlie
it. We highlight areas requiring further investigation, and emphasise the need
for tighter links between theory and empirical research and between individual-level
and collective-level analyses.
article_processing_charge: No
author:
- first_name: Nathalie
full_name: Stroeymeyt, Nathalie
last_name: Stroeymeyt
- first_name: Barbara E
full_name: Casillas Perez, Barbara E
id: 351ED2AA-F248-11E8-B48F-1D18A9856A87
last_name: Casillas Perez
- first_name: Sylvia
full_name: Cremer, Sylvia
id: 2F64EC8C-F248-11E8-B48F-1D18A9856A87
last_name: Cremer
orcid: 0000-0002-2193-3868
citation:
ama: Stroeymeyt N, Casillas Perez BE, Cremer S. Organisational immunity in social
insects. Current Opinion in Insect Science. 2014;5(1):1-15. doi:10.1016/j.cois.2014.09.001
apa: Stroeymeyt, N., Casillas Perez, B. E., & Cremer, S. (2014). Organisational
immunity in social insects. Current Opinion in Insect Science. Elsevier.
https://doi.org/10.1016/j.cois.2014.09.001
chicago: Stroeymeyt, Nathalie, Barbara E Casillas Perez, and Sylvia Cremer. “Organisational
Immunity in Social Insects.” Current Opinion in Insect Science. Elsevier,
2014. https://doi.org/10.1016/j.cois.2014.09.001.
ieee: N. Stroeymeyt, B. E. Casillas Perez, and S. Cremer, “Organisational immunity
in social insects,” Current Opinion in Insect Science, vol. 5, no. 1. Elsevier,
pp. 1–15, 2014.
ista: Stroeymeyt N, Casillas Perez BE, Cremer S. 2014. Organisational immunity in
social insects. Current Opinion in Insect Science. 5(1), 1–15.
mla: Stroeymeyt, Nathalie, et al. “Organisational Immunity in Social Insects.” Current
Opinion in Insect Science, vol. 5, no. 1, Elsevier, 2014, pp. 1–15, doi:10.1016/j.cois.2014.09.001.
short: N. Stroeymeyt, B.E. Casillas Perez, S. Cremer, Current Opinion in Insect
Science 5 (2014) 1–15.
corr_author: '1'
date_created: 2018-12-11T11:55:08Z
date_published: 2014-11-01T00:00:00Z
date_updated: 2026-07-25T22:30:49Z
day: '01'
department:
- _id: SyCr
doi: 10.1016/j.cois.2014.09.001
ec_funded: 1
external_id:
isi:
- '000209578900002'
intvolume: ' 5'
isi: 1
issue: '1'
language:
- iso: eng
month: '11'
oa_version: None
page: 1 - 15
project:
- _id: 25DC711C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '243071'
name: 'Social Vaccination in Ant Colonies: from Individual Mechanisms to Society
Effects'
publication: Current Opinion in Insect Science
publication_status: published
publisher: Elsevier
publist_id: '5080'
quality_controlled: '1'
related_material:
record:
- id: '6383'
relation: dissertation_contains
- id: '6435'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Organisational immunity in social insects
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 5
year: '2014'
...
---
_id: '10895'
abstract:
- lang: eng
text: 'Due to their sessile lifestyles, plants need to deal with the limitations
and stresses imposed by the changing environment. Plants cope with these by a
remarkable developmental flexibility, which is embedded in their strategy to survive.
Plants can adjust their size, shape and number of organs, bend according to gravity
and light, and regenerate tissues that were damaged, utilizing a coordinating,
intercellular signal, the plant hormone, auxin. Another versatile signal is the
cation, Ca2+, which is a crucial second messenger for many rapid cellular processes
during responses to a wide range of endogenous and environmental signals, such
as hormones, light, drought stress and others. Auxin is a good candidate for one
of these Ca2+-activating signals. However, the role of auxin-induced Ca2+ signaling
is poorly understood. Here, we will provide an overview of possible developmental
and physiological roles, as well as mechanisms underlying the interconnection
of Ca2+ and auxin signaling. '
article_processing_charge: No
article_type: original
author:
- first_name: Steffen
full_name: Vanneste, Steffen
last_name: Vanneste
- first_name: Jiří
full_name: Friml, Jiří
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
citation:
ama: 'Vanneste S, Friml J. Calcium: The missing link in auxin action. Plants.
2013;2(4):650-675. doi:10.3390/plants2040650'
apa: 'Vanneste, S., & Friml, J. (2013). Calcium: The missing link in auxin action.
Plants. MDPI. https://doi.org/10.3390/plants2040650'
chicago: 'Vanneste, Steffen, and Jiří Friml. “Calcium: The Missing Link in Auxin
Action.” Plants. MDPI, 2013. https://doi.org/10.3390/plants2040650.'
ieee: 'S. Vanneste and J. Friml, “Calcium: The missing link in auxin action,” Plants,
vol. 2, no. 4. MDPI, pp. 650–675, 2013.'
ista: 'Vanneste S, Friml J. 2013. Calcium: The missing link in auxin action. Plants.
2(4), 650–675.'
mla: 'Vanneste, Steffen, and Jiří Friml. “Calcium: The Missing Link in Auxin Action.”
Plants, vol. 2, no. 4, MDPI, 2013, pp. 650–75, doi:10.3390/plants2040650.'
short: S. Vanneste, J. Friml, Plants 2 (2013) 650–675.
corr_author: '1'
date_created: 2022-03-21T07:13:49Z
date_published: 2013-10-21T00:00:00Z
date_updated: 2024-10-09T21:01:52Z
day: '21'
ddc:
- '580'
department:
- _id: JiFr
doi: 10.3390/plants2040650
external_id:
pmid:
- '27137397'
file:
- access_level: open_access
checksum: fb4ff2e820e344e253c9197544610be6
content_type: application/pdf
creator: dernst
date_created: 2022-03-21T12:12:56Z
date_updated: 2022-03-21T12:12:56Z
file_id: '10916'
file_name: 2013_Plants_Vanneste.pdf
file_size: 670188
relation: main_file
success: 1
file_date_updated: 2022-03-21T12:12:56Z
has_accepted_license: '1'
intvolume: ' 2'
issue: '4'
keyword:
- Plant Science
- Ecology
- Ecology
- Evolution
- Behavior and Systematics
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 650-675
pmid: 1
publication: Plants
publication_identifier:
issn:
- 2223-7747
publication_status: published
publisher: MDPI
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Calcium: The missing link in auxin action'
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2013'
...
---
_id: '10897'
abstract:
- lang: eng
text: Taking images is an efficient way to collect data about the physical world.
It can be done fast and in exquisite detail. By definition, image processing is
the field that concerns itself with the computation aimed at harnessing the information
contained in images [10]. This talk is concerned with topological information.
Our main thesis is that persistent homology [5] is a useful method to quantify
and summarize topological information, building a bridge that connects algebraic
topology with applications. We provide supporting evidence for this thesis by
touching upon four technical developments in the overlap between persistent homology
and image processing.
acknowledgement: This research is partially supported by the European Science Foundation
(ESF) under the Research Network Programme, the European Union under the Toposys
Project FP7-ICT-318493-STREP, the Russian Government under the Mega Project 11.G34.31.0053.
article_processing_charge: No
author:
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
citation:
ama: 'Edelsbrunner H. Persistent homology in image processing. In: Graph-Based
Representations in Pattern Recognition. Vol 7877. LNCS. Berlin, Heidelberg:
Springer Nature; 2013:182-183. doi:10.1007/978-3-642-38221-5_19'
apa: 'Edelsbrunner, H. (2013). Persistent homology in image processing. In Graph-Based
Representations in Pattern Recognition (Vol. 7877, pp. 182–183). Berlin, Heidelberg:
Springer Nature. https://doi.org/10.1007/978-3-642-38221-5_19'
chicago: 'Edelsbrunner, Herbert. “Persistent Homology in Image Processing.” In Graph-Based
Representations in Pattern Recognition, 7877:182–83. LNCS. Berlin, Heidelberg:
Springer Nature, 2013. https://doi.org/10.1007/978-3-642-38221-5_19.'
ieee: H. Edelsbrunner, “Persistent homology in image processing,” in Graph-Based
Representations in Pattern Recognition, Vienna, Austria, 2013, vol. 7877,
pp. 182–183.
ista: 'Edelsbrunner H. 2013. Persistent homology in image processing. Graph-Based
Representations in Pattern Recognition. GbRPR: Graph-based Representations in
Pattern RecognitionLNCS vol. 7877, 182–183.'
mla: Edelsbrunner, Herbert. “Persistent Homology in Image Processing.” Graph-Based
Representations in Pattern Recognition, vol. 7877, Springer Nature, 2013,
pp. 182–83, doi:10.1007/978-3-642-38221-5_19.
short: H. Edelsbrunner, in:, Graph-Based Representations in Pattern Recognition,
Springer Nature, Berlin, Heidelberg, 2013, pp. 182–183.
conference:
end_date: 2013-05-17
location: Vienna, Austria
name: 'GbRPR: Graph-based Representations in Pattern Recognition'
start_date: 2013-05-15
corr_author: '1'
date_created: 2022-03-21T07:30:33Z
date_published: 2013-06-01T00:00:00Z
date_updated: 2025-04-15T08:37:54Z
day: '01'
department:
- _id: HeEd
doi: 10.1007/978-3-642-38221-5_19
ec_funded: 1
intvolume: ' 7877'
language:
- iso: eng
month: '06'
oa_version: None
page: 182-183
place: Berlin, Heidelberg
project:
- _id: 255D761E-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '318493'
name: Topological Complex Systems
publication: Graph-Based Representations in Pattern Recognition
publication_identifier:
eisbn:
- '9783642382215'
eissn:
- 1611-3349
isbn:
- '9783642382208'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Persistent homology in image processing
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7877
year: '2013'
...