---
_id: '958'
abstract:
- lang: eng
text: Biosensors that exploit Forster resonance energy transfer (FRET) can be used
to visualize biological and physiological processes and are capable of providing
detailed information in both spatial and temporal dimensions. In a FRET-based
biosensor, substrate binding is associated with a change in the relative positions
of two fluorophores, leading to a change in FRET efficiency that may be observed
in the fluorescence spectrum. As a result, their design requires a ligand-binding
protein that exhibits a conformational change upon binding. However, not all ligand-binding
proteins produce responsive sensors upon conjugation to fluorescent proteins or
dyes, and identifying the optimum locations for the fluorophores often involves
labor-intensive iterative design or high-throughput screening. Combining the genetic
fusion of a fluorescent protein to the ligand-binding protein with site-specific
covalent attachment of a fluorescent dye can allow fine control over the positions
of the two fluorophores, allowing the construction of very sensitive sensors.
This relies upon the accurate prediction of the locations of the two fluorophores
in bound and unbound states. In this chapter, we describe a method for computational
identification of dye-attachment sites that allows the use of cysteine modification
to attach synthetic dyes that can be paired with a fluorescent protein for the
purposes of creating FRET sensors.
alternative_title:
- Methods in Molecular Biology
author:
- first_name: Joshua
full_name: Mitchell, Joshua
last_name: Mitchell
- first_name: William
full_name: Zhang, William
last_name: Zhang
- first_name: Michel
full_name: Herde, Michel
last_name: Herde
- first_name: Christian
full_name: Henneberger, Christian
last_name: Henneberger
- first_name: Harald L
full_name: Janovjak, Harald L
id: 33BA6C30-F248-11E8-B48F-1D18A9856A87
last_name: Janovjak
orcid: 0000-0002-8023-9315
- first_name: Megan
full_name: O'Mara, Megan
last_name: O'Mara
- first_name: Colin
full_name: Jackson, Colin
last_name: Jackson
citation:
ama: 'Mitchell J, Zhang W, Herde M, et al. Method for developing optical sensors
using a synthetic dye fluorescent protein FRET pair and computational modeling
and assessment. In: Stein V, ed. Synthetic Protein Switches. Vol 1596.
Synthetic Protein Switches. Springer; 2017:89-99. doi:10.1007/978-1-4939-6940-1_6'
apa: Mitchell, J., Zhang, W., Herde, M., Henneberger, C., Janovjak, H. L., O’Mara,
M., & Jackson, C. (2017). Method for developing optical sensors using a synthetic
dye fluorescent protein FRET pair and computational modeling and assessment. In
V. Stein (Ed.), Synthetic Protein Switches (Vol. 1596, pp. 89–99). Springer.
https://doi.org/10.1007/978-1-4939-6940-1_6
chicago: Mitchell, Joshua, William Zhang, Michel Herde, Christian Henneberger, Harald
L Janovjak, Megan O’Mara, and Colin Jackson. “Method for Developing Optical Sensors
Using a Synthetic Dye Fluorescent Protein FRET Pair and Computational Modeling
and Assessment.” In Synthetic Protein Switches, edited by Viktor Stein,
1596:89–99. Synthetic Protein Switches. Springer, 2017. https://doi.org/10.1007/978-1-4939-6940-1_6.
ieee: J. Mitchell et al., “Method for developing optical sensors using a
synthetic dye fluorescent protein FRET pair and computational modeling and assessment,”
in Synthetic Protein Switches, vol. 1596, V. Stein, Ed. Springer, 2017,
pp. 89–99.
ista: 'Mitchell J, Zhang W, Herde M, Henneberger C, Janovjak HL, O’Mara M, Jackson
C. 2017.Method for developing optical sensors using a synthetic dye fluorescent
protein FRET pair and computational modeling and assessment. In: Synthetic Protein
Switches. Methods in Molecular Biology, vol. 1596, 89–99.'
mla: Mitchell, Joshua, et al. “Method for Developing Optical Sensors Using a Synthetic
Dye Fluorescent Protein FRET Pair and Computational Modeling and Assessment.”
Synthetic Protein Switches, edited by Viktor Stein, vol. 1596, Springer,
2017, pp. 89–99, doi:10.1007/978-1-4939-6940-1_6.
short: J. Mitchell, W. Zhang, M. Herde, C. Henneberger, H.L. Janovjak, M. O’Mara,
C. Jackson, in:, V. Stein (Ed.), Synthetic Protein Switches, Springer, 2017, pp.
89–99.
date_created: 2018-12-11T11:49:24Z
date_published: 2017-05-15T00:00:00Z
date_updated: 2021-01-12T08:22:13Z
day: '15'
department:
- _id: HaJa
doi: 10.1007/978-1-4939-6940-1_6
editor:
- first_name: Viktor
full_name: Stein, Viktor
last_name: Stein
intvolume: ' 1596'
language:
- iso: eng
month: '05'
oa_version: None
page: 89 - 99
publication: Synthetic Protein Switches
publication_identifier:
issn:
- '10643745'
publication_status: published
publisher: Springer
publist_id: '6450'
quality_controlled: '1'
scopus_import: 1
series_title: Synthetic Protein Switches
status: public
title: Method for developing optical sensors using a synthetic dye fluorescent protein
FRET pair and computational modeling and assessment
type: book_chapter
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 1596
year: '2017'
...
---
_id: '9707'
abstract:
- lang: eng
text: Branching morphogenesis of the epithelial ureteric bud forms the renal collecting
duct system and is critical for normal nephron number, while low nephron number
is implicated in hypertension and renal disease. Ureteric bud growth and branching
requires GDNF signaling from the surrounding mesenchyme to cells at the ureteric
bud tips, via the Ret receptor tyrosine kinase and coreceptor Gfrα1; Ret signaling
up-regulates transcription factors Etv4 and Etv5, which are also critical for
branching. Despite extensive knowledge of the genetic control of these events,
it is not understood, at the cellular level, how renal branching morphogenesis
is achieved or how Ret signaling influences epithelial cell behaviors to promote
this process. Analysis of chimeric embryos previously suggested a role for Ret
signaling in promoting cell rearrangements in the nephric duct, but this method
was unsuited to study individual cell behaviors during ureteric bud branching.
Here, we use Mosaic Analysis with Double Markers (MADM), combined with organ culture
and time-lapse imaging, to trace the movements and divisions of individual ureteric
bud tip cells. We first examine wild-type clones and then Ret or Etv4 mutant/wild-type
clones in which the mutant and wild-type sister cells are differentially and heritably
marked by green and red fluorescent proteins. We find that, in normal kidneys,
most individual tip cells behave as self-renewing progenitors, some of whose progeny
remain at the tips while others populate the growing UB trunks. In Ret or Etv4
MADM clones, the wild-type cells generated at a UB tip are much more likely to
remain at, or move to, the new tips during branching and elongation, while their
Ret−/− or Etv4−/− sister cells tend to lag behind and contribute only to the trunks.
By tracking successive mitoses in a cell lineage, we find that Ret signaling has
little effect on proliferation, in contrast to its effects on cell movement. Our
results show that Ret/Etv4 signaling promotes directed cell movements in the ureteric
bud tips, and suggest a model in which these cell movements mediate branching
morphogenesis.
article_processing_charge: No
author:
- first_name: Paul
full_name: Riccio, Paul
last_name: Riccio
- first_name: Christina
full_name: Cebrián, Christina
last_name: Cebrián
- first_name: Hui
full_name: Zong, Hui
last_name: Zong
- first_name: Simon
full_name: Hippenmeyer, Simon
id: 37B36620-F248-11E8-B48F-1D18A9856A87
last_name: Hippenmeyer
orcid: 0000-0003-2279-1061
- first_name: Frank
full_name: Costantini, Frank
last_name: Costantini
citation:
ama: 'Riccio P, Cebrián C, Zong H, Hippenmeyer S, Costantini F. Data from: Ret and
Etv4 promote directed movements of progenitor cells during renal branching morphogenesis.
2017. doi:10.5061/dryad.pk16b'
apa: 'Riccio, P., Cebrián, C., Zong, H., Hippenmeyer, S., & Costantini, F. (2017).
Data from: Ret and Etv4 promote directed movements of progenitor cells during
renal branching morphogenesis. Dryad. https://doi.org/10.5061/dryad.pk16b'
chicago: 'Riccio, Paul, Christina Cebrián, Hui Zong, Simon Hippenmeyer, and Frank
Costantini. “Data from: Ret and Etv4 Promote Directed Movements of Progenitor
Cells during Renal Branching Morphogenesis.” Dryad, 2017. https://doi.org/10.5061/dryad.pk16b.'
ieee: 'P. Riccio, C. Cebrián, H. Zong, S. Hippenmeyer, and F. Costantini, “Data
from: Ret and Etv4 promote directed movements of progenitor cells during renal
branching morphogenesis.” Dryad, 2017.'
ista: 'Riccio P, Cebrián C, Zong H, Hippenmeyer S, Costantini F. 2017. Data from:
Ret and Etv4 promote directed movements of progenitor cells during renal branching
morphogenesis, Dryad, 10.5061/dryad.pk16b.'
mla: 'Riccio, Paul, et al. Data from: Ret and Etv4 Promote Directed Movements
of Progenitor Cells during Renal Branching Morphogenesis. Dryad, 2017, doi:10.5061/dryad.pk16b.'
short: P. Riccio, C. Cebrián, H. Zong, S. Hippenmeyer, F. Costantini, (2017).
date_created: 2021-07-23T09:39:34Z
date_published: 2017-01-14T00:00:00Z
date_updated: 2022-08-25T13:34:55Z
day: '14'
department:
- _id: SiHi
doi: 10.5061/dryad.pk16b
main_file_link:
- open_access: '1'
url: https://doi.org/10.5061/dryad.pk16b
month: '01'
oa: 1
oa_version: Published Version
publisher: Dryad
related_material:
record:
- id: '9702'
relation: used_in_publication
status: deleted
status: public
title: 'Data from: Ret and Etv4 promote directed movements of progenitor cells during
renal branching morphogenesis'
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2017'
...
---
_id: '9844'
article_processing_charge: No
author:
- first_name: Nela
full_name: Nikolic, Nela
id: 42D9CABC-F248-11E8-B48F-1D18A9856A87
last_name: Nikolic
orcid: 0000-0001-9068-6090
- first_name: Frank
full_name: Schreiber, Frank
last_name: Schreiber
- first_name: Alma
full_name: Dal Co, Alma
last_name: Dal Co
- first_name: Daniel
full_name: Kiviet, Daniel
last_name: Kiviet
- first_name: Tobias
full_name: Bergmiller, Tobias
id: 2C471CFA-F248-11E8-B48F-1D18A9856A87
last_name: Bergmiller
orcid: 0000-0001-5396-4346
- first_name: Sten
full_name: Littmann, Sten
last_name: Littmann
- first_name: Marcel
full_name: Kuypers, Marcel
last_name: Kuypers
- first_name: Martin
full_name: Ackermann, Martin
last_name: Ackermann
citation:
ama: Nikolic N, Schreiber F, Dal Co A, et al. Source data for figures and tables.
2017. doi:10.1371/journal.pgen.1007122.s018
apa: Nikolic, N., Schreiber, F., Dal Co, A., Kiviet, D., Bergmiller, T., Littmann,
S., … Ackermann, M. (2017). Source data for figures and tables. Public Library
of Science. https://doi.org/10.1371/journal.pgen.1007122.s018
chicago: Nikolic, Nela, Frank Schreiber, Alma Dal Co, Daniel Kiviet, Tobias Bergmiller,
Sten Littmann, Marcel Kuypers, and Martin Ackermann. “Source Data for Figures
and Tables.” Public Library of Science, 2017. https://doi.org/10.1371/journal.pgen.1007122.s018.
ieee: N. Nikolic et al., “Source data for figures and tables.” Public Library
of Science, 2017.
ista: Nikolic N, Schreiber F, Dal Co A, Kiviet D, Bergmiller T, Littmann S, Kuypers
M, Ackermann M. 2017. Source data for figures and tables, Public Library of Science,
10.1371/journal.pgen.1007122.s018.
mla: Nikolic, Nela, et al. Source Data for Figures and Tables. Public Library
of Science, 2017, doi:10.1371/journal.pgen.1007122.s018.
short: N. Nikolic, F. Schreiber, A. Dal Co, D. Kiviet, T. Bergmiller, S. Littmann,
M. Kuypers, M. Ackermann, (2017).
date_created: 2021-08-09T13:27:16Z
date_published: 2017-12-18T00:00:00Z
date_updated: 2023-02-23T12:25:04Z
day: '18'
department:
- _id: CaGu
doi: 10.1371/journal.pgen.1007122.s018
month: '12'
oa_version: Published Version
publisher: Public Library of Science
related_material:
record:
- id: '541'
relation: used_in_publication
status: public
status: public
title: Source data for figures and tables
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2017'
...
---
_id: '12905'
article_processing_charge: No
author:
- first_name: Alois
full_name: Schlögl, Alois
id: 45BF87EE-F248-11E8-B48F-1D18A9856A87
last_name: Schlögl
orcid: 0000-0002-5621-8100
- first_name: Janos
full_name: Kiss, Janos
id: 3D3A06F8-F248-11E8-B48F-1D18A9856A87
last_name: Kiss
citation:
ama: 'Schlögl A, Kiss J. Scientific Computing at IST Austria. In: AHPC17 – Austrian
HPC Meeting 2017. FSP Scientific Computing; 2017:28.'
apa: 'Schlögl, A., & Kiss, J. (2017). Scientific Computing at IST Austria. In
AHPC17 – Austrian HPC Meeting 2017 (p. 28). Grundlsee, Austria: FSP Scientific
Computing.'
chicago: Schlögl, Alois, and Janos Kiss. “Scientific Computing at IST Austria.”
In AHPC17 – Austrian HPC Meeting 2017, 28. FSP Scientific Computing, 2017.
ieee: A. Schlögl and J. Kiss, “Scientific Computing at IST Austria,” in AHPC17
– Austrian HPC Meeting 2017, Grundlsee, Austria, 2017, p. 28.
ista: 'Schlögl A, Kiss J. 2017. Scientific Computing at IST Austria. AHPC17 – Austrian
HPC Meeting 2017. AHPC: Austrian HPC Meeting, 28.'
mla: Schlögl, Alois, and Janos Kiss. “Scientific Computing at IST Austria.” AHPC17
– Austrian HPC Meeting 2017, FSP Scientific Computing, 2017, p. 28.
short: A. Schlögl, J. Kiss, in:, AHPC17 – Austrian HPC Meeting 2017, FSP Scientific
Computing, 2017, p. 28.
conference:
end_date: 2017-03-03
location: Grundlsee, Austria
name: 'AHPC: Austrian HPC Meeting'
start_date: 2017-03-01
date_created: 2023-05-05T12:58:53Z
date_published: 2017-03-03T00:00:00Z
date_updated: 2023-05-16T07:22:23Z
day: '03'
ddc:
- '000'
department:
- _id: ScienComp
file:
- access_level: open_access
checksum: 7bcc499479d4f4c5ce6c0071c24ca6c6
content_type: application/pdf
creator: dernst
date_created: 2023-05-16T07:20:50Z
date_updated: 2023-05-16T07:20:50Z
file_id: '12969'
file_name: 2017_AHPC_Schloegl.pdf
file_size: 1005486
relation: main_file
success: 1
file_date_updated: 2023-05-16T07:20:50Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://vsc.ac.at/fileadmin/user_upload/vsc/conferences/ahpc17/BOOKLET_AHPC17.pdf
month: '03'
oa: 1
oa_version: Published Version
page: '28'
publication: AHPC17 – Austrian HPC Meeting 2017
publication_status: published
publisher: FSP Scientific Computing
status: public
title: Scientific Computing at IST Austria
type: conference_abstract
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...
---
_id: '13160'
abstract:
- lang: eng
text: "Transforming deterministic ω\r\n-automata into deterministic parity automata
is traditionally done using variants of appearance records. We present a more
efficient variant of this approach, tailored to Rabin automata, and several optimizations
applicable to all appearance records. We compare the methods experimentally and
find out that our method produces smaller automata than previous approaches. Moreover,
the experiments demonstrate the potential of our method for LTL synthesis, using
LTL-to-Rabin translators. It leads to significantly smaller parity automata when
compared to state-of-the-art approaches on complex formulae."
acknowledgement: This work is partially funded by the DFG project “Verified Model
Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Clara
full_name: Waldmann, Clara
last_name: Waldmann
- first_name: Maximilian
full_name: Weininger, Maximilian
last_name: Weininger
citation:
ama: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
for transforming Rabin automata into parity automata. In: Tools and Algorithms
for the Construction and Analysis of Systems. Vol 10205. Springer; 2017:443-460.
doi:10.1007/978-3-662-54577-5_26'
apa: 'Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2017).
Index appearance record for transforming Rabin automata into parity automata.
In Tools and Algorithms for the Construction and Analysis of Systems (Vol.
10205, pp. 443–460). Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54577-5_26'
chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
“Index Appearance Record for Transforming Rabin Automata into Parity Automata.”
In Tools and Algorithms for the Construction and Analysis of Systems, 10205:443–60.
Springer, 2017. https://doi.org/10.1007/978-3-662-54577-5_26.
ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
record for transforming Rabin automata into parity automata,” in Tools and
Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden,
2017, vol. 10205, pp. 443–460.
ista: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance
record for transforming Rabin automata into parity automata. Tools and Algorithms
for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.'
mla: Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata
into Parity Automata.” Tools and Algorithms for the Construction and Analysis
of Systems, vol. 10205, Springer, 2017, pp. 443–60, doi:10.1007/978-3-662-54577-5_26.
short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and
Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2017-04-22
date_created: 2023-06-21T13:21:14Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2023-06-21T13:29:46Z
day: '31'
department:
- _id: KrCh
doi: 10.1007/978-3-662-54577-5_26
external_id:
arxiv:
- '1701.05738'
intvolume: ' 10205'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.1701.05738
month: '03'
oa: 1
oa_version: Preprint
page: 443-460
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783662545775'
eissn:
- 1611-3349
isbn:
- '9783662545768'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
status: public
title: Index appearance record for transforming Rabin automata into parity automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10205
year: '2017'
...
---
_id: '950'
abstract:
- lang: eng
text: "Two-player games on graphs are widely studied in formal methods as they model
the interaction between a system and its environment. The game is played by moving
a token throughout a graph to produce an infinite path. There are several common
modes to determine how the players move the token through the graph; e.g., in
turn-based games the players alternate turns in moving the token. We study the
bidding mode of moving the token, which, to the best of our knowledge, has never
been studied in infinite-duration games. Both players have separate budgets, which
sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously,
and a bid is legal if it does not exceed the available budget. The winner of the
bidding pays his bid to the other player and moves the token. For reachability
objectives, repeated bidding games have been studied and are called Richman games.
There, a central question is the existence and computation of threshold budgets;
namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win
the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity
games and mean-payoff games. We show the existence of threshold budgets in these
games, and reduce the problem of finding them to Richman games. We also determine
the strategy-complexity of an optimal strategy. Our most interesting result shows
that memoryless strategies suffice for mean-payoff bidding games. \r\n"
alternative_title:
- LIPIcs
article_number: '17'
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- 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: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
citation:
ama: 'Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol
85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.21'
apa: 'Avni, G., Henzinger, T. A., & Chonev, V. K. (2017). Infinite-duration
bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin,
Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21'
chicago: Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration
Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
https://doi.org/10.4230/LIPIcs.CONCUR.2017.21.
ieee: 'G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,”
presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.'
ista: 'Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR:
Concurrency Theory, LIPIcs, vol. 85, 17.'
mla: Avni, Guy, et al. Infinite-Duration Bidding Games. Vol. 85, 17, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.21.
short: G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2017.
conference:
end_date: 2017-09-07
location: Berlin, Germany
name: 'CONCUR: Concurrency Theory'
start_date: 2017-09-05
date_created: 2018-12-11T11:49:22Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-08-29T07:02:13Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2017.21
external_id:
arxiv:
- '1705.01433'
file:
- access_level: open_access
checksum: 6d5cccf755207b91ccbef95d8275b013
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:00Z
date_updated: 2020-07-14T12:48:16Z
file_id: '5318'
file_name: IST-2017-844-v1+1_concur-cr.pdf
file_size: 335170
relation: main_file
file_date_updated: 2020-07-14T12:48:16Z
has_accepted_license: '1'
intvolume: ' 85'
language:
- iso: eng
month: '09'
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6466'
pubrep_id: '844'
quality_controlled: '1'
related_material:
record:
- id: '6752'
relation: later_version
status: public
scopus_import: 1
status: public
title: Infinite-duration bidding games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 85
year: '2017'
...
---
_id: '683'
abstract:
- lang: eng
text: 'Given a triangulation of a point set in the plane, a flip deletes an edge
e whose removal leaves a convex quadrilateral, and replaces e by the opposite
diagonal of the quadrilateral. It is well known that any triangulation of a point
set can be reconfigured to any other triangulation by some sequence of flips.
We explore this question in the setting where each edge of a triangulation has
a label, and a flip transfers the label of the removed edge to the new edge. It
is not true that every labelled triangulation of a point set can be reconfigured
to every other labelled triangulation via a sequence of flips, but we characterize
when this is possible. There is an obvious necessary condition: for each label
l, if edge e has label l in the first triangulation and edge f has label l in
the second triangulation, then there must be some sequence of flips that moves
label l from e to f, ignoring all other labels. Bose, Lubiw, Pathak and Verdonschot
formulated the Orbit Conjecture, which states that this necessary condition is
also sufficient, i.e. that all labels can be simultaneously mapped to their destination
if and only if each label individually can be mapped to its destination. We prove
this conjecture. Furthermore, we give a polynomial-time algorithm to find a sequence
of flips to reconfigure one labelled triangulation to another, if such a sequence
exists, and we prove an upper bound of O(n7) on the length of the flip sequence.
Our proof uses the topological result that the sets of pairwise non-crossing edges
on a planar point set form a simplicial complex that is homeomorphic to a high-dimensional
ball (this follows from a result of Orden and Santos; we give a different proof
based on a shelling argument). The dual cell complex of this simplicial ball,
called the flip complex, has the usual flip graph as its 1-skeleton. We use properties
of the 2-skeleton of the flip complex to prove the Orbit Conjecture.'
alternative_title:
- LIPIcs
article_number: '49'
author:
- first_name: Anna
full_name: Lubiw, Anna
last_name: Lubiw
- first_name: Zuzana
full_name: Masárová, Zuzana
id: 45CFE238-F248-11E8-B48F-1D18A9856A87
last_name: Masárová
orcid: 0000-0002-6660-1322
- first_name: Uli
full_name: Wagner, Uli
id: 36690CA2-F248-11E8-B48F-1D18A9856A87
last_name: Wagner
orcid: 0000-0002-1494-0568
citation:
ama: 'Lubiw A, Masárová Z, Wagner U. A proof of the orbit conjecture for flipping
edge labelled triangulations. In: Vol 77. Schloss Dagstuhl - Leibniz-Zentrum für
Informatik; 2017. doi:10.4230/LIPIcs.SoCG.2017.49'
apa: 'Lubiw, A., Masárová, Z., & Wagner, U. (2017). A proof of the orbit conjecture
for flipping edge labelled triangulations (Vol. 77). Presented at the SoCG: Symposium
on Computational Geometry, Brisbane, Australia: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.SoCG.2017.49'
chicago: Lubiw, Anna, Zuzana Masárová, and Uli Wagner. “A Proof of the Orbit Conjecture
for Flipping Edge Labelled Triangulations,” Vol. 77. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2017. https://doi.org/10.4230/LIPIcs.SoCG.2017.49.
ieee: 'A. Lubiw, Z. Masárová, and U. Wagner, “A proof of the orbit conjecture for
flipping edge labelled triangulations,” presented at the SoCG: Symposium on Computational
Geometry, Brisbane, Australia, 2017, vol. 77.'
ista: 'Lubiw A, Masárová Z, Wagner U. 2017. A proof of the orbit conjecture for
flipping edge labelled triangulations. SoCG: Symposium on Computational Geometry,
LIPIcs, vol. 77, 49.'
mla: Lubiw, Anna, et al. A Proof of the Orbit Conjecture for Flipping Edge Labelled
Triangulations. Vol. 77, 49, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2017, doi:10.4230/LIPIcs.SoCG.2017.49.
short: A. Lubiw, Z. Masárová, U. Wagner, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2017.
conference:
end_date: 2017-07-07
location: Brisbane, Australia
name: 'SoCG: Symposium on Computational Geometry'
start_date: 2017-07-04
date_created: 2018-12-11T11:47:54Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-09-05T15:01:43Z
day: '01'
ddc:
- '514'
- '516'
department:
- _id: UlWa
doi: 10.4230/LIPIcs.SoCG.2017.49
file:
- access_level: open_access
checksum: 24fdde981cc513352a78dcf9b0660ae9
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:12Z
date_updated: 2020-07-14T12:47:41Z
file_id: '5265'
file_name: IST-2017-896-v1+1_LIPIcs-SoCG-2017-49.pdf
file_size: 710007
relation: main_file
file_date_updated: 2020-07-14T12:47:41Z
has_accepted_license: '1'
intvolume: ' 77'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7033'
pubrep_id: '896'
quality_controlled: '1'
related_material:
record:
- id: '5986'
relation: later_version
status: public
scopus_import: 1
status: public
title: A proof of the orbit conjecture for flipping edge labelled triangulations
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 77
year: '2017'
...
---
_id: '1155'
abstract:
- lang: eng
text: This dissertation concerns the automatic verification of probabilistic systems
and programs with arrays by statistical and logical methods. Although statistical
and logical methods are different in nature, we show that they can be successfully
combined for system analysis. In the first part of the dissertation we present
a new statistical algorithm for the verification of probabilistic systems with
respect to unbounded properties, including linear temporal logic. Our algorithm
often performs faster than the previous approaches, and at the same time requires
less information about the system. In addition, our method can be generalized
to unbounded quantitative properties such as mean-payoff bounds. In the second
part, we introduce two techniques for comparing probabilistic systems. Probabilistic
systems are typically compared using the notion of equivalence, which requires
the systems to have the equal probability of all behaviors. However, this notion
is often too strict, since probabilities are typically only empirically estimated,
and any imprecision may break the relation between processes. On the one hand,
we propose to replace the Boolean notion of equivalence by a quantitative distance
of similarity. For this purpose, we introduce a statistical framework for estimating
distances between Markov chains based on their simulation runs, and we investigate
which distances can be approximated in our framework. On the other hand, we propose
to compare systems with respect to a new qualitative logic, which expresses that
behaviors occur with probability one or a positive probability. This qualitative
analysis is robust with respect to modeling errors and applicable to many domains.
In the last part, we present a new quantifier-free logic for integer arrays, which
allows us to express counting. Counting properties are prevalent in array-manipulating
programs, however they cannot be expressed in the quantified fragments of the
theory of arrays. We present a decision procedure for our logic, and provide several
complexity results.
acknowledgement: ' First of all, I want to thank my advisor, prof. Thomas A. Henzinger,
for his guidance during my PhD program. I am grateful for the freedom I was given
to pursue my research interests, and his continuous support. Working with prof.
Henzinger was a truly inspiring experience and taught me what it means to be a scientist.
I want to express my gratitude to my collaborators: Nikola Beneš, Krishnendu Chatterjee,
Martin Chmelík, Ashutosh Gupta, Willibald Krenn, Jan Kˇretínský, Dejan Nickovic,
Andrey Kupriyanov, and Tatjana Petrov. I have learned a great deal from my collaborators,
and without their help this thesis would not be possible. In addition, I want to
thank the members of my thesis committee: Dirk Beyer, Dejan Nickovic, and Georg
Weissenbacher for their advice and reviewing this dissertation. I would especially
like to acknowledge the late Helmut Veith, who was a member of my committee. I will
remember Helmut for his kindness, enthusiasm, and wit, as well as for being an inspiring
scientist. Finally, I would like to thank my colleagues for making my stay at IST
such a pleasant experience: Guy Avni, Sergiy Bogomolov, Ventsislav Chonev, Rasmus
Ibsen-Jensen, Mirco Giacobbe, Bernhard Kragl, Hui Kong, Petr Novotný, Jan Otop,
Andreas Pavlogiannis, Tantjana Petrov, Arjun Radhakrishna, Jakob Ruess, Thorsten
Tarrach, as well as other members of groups Henzinger and Chatterjee. '
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
citation:
ama: Daca P. Statistical and logical methods for property checking. 2017. doi:10.15479/AT:ISTA:TH_730
apa: Daca, P. (2017). Statistical and logical methods for property checking.
Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:TH_730
chicago: Daca, Przemyslaw. “Statistical and Logical Methods for Property Checking.”
Institute of Science and Technology Austria, 2017. https://doi.org/10.15479/AT:ISTA:TH_730.
ieee: P. Daca, “Statistical and logical methods for property checking,” Institute
of Science and Technology Austria, 2017.
ista: Daca P. 2017. Statistical and logical methods for property checking. Institute
of Science and Technology Austria.
mla: Daca, Przemyslaw. Statistical and Logical Methods for Property Checking.
Institute of Science and Technology Austria, 2017, doi:10.15479/AT:ISTA:TH_730.
short: P. Daca, Statistical and Logical Methods for Property Checking, Institute
of Science and Technology Austria, 2017.
date_created: 2018-12-11T11:50:27Z
date_published: 2017-01-02T00:00:00Z
date_updated: 2023-09-07T11:58:34Z
day: '02'
ddc:
- '004'
- '005'
degree_awarded: PhD
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:TH_730
ec_funded: 1
file:
- access_level: open_access
checksum: 1406a681cb737508234fde34766be2c2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:26Z
date_updated: 2020-07-14T12:44:34Z
file_id: '4880'
file_name: IST-2017-730-v1+1_Statistical_and_Logical_Methods_for_Property_Checking.pdf
file_size: 1028586
relation: main_file
file_date_updated: 2020-07-14T12:44:34Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '163'
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '6203'
pubrep_id: '730'
related_material:
record:
- id: '1093'
relation: part_of_dissertation
status: public
- id: '1230'
relation: part_of_dissertation
status: public
- id: '1234'
relation: part_of_dissertation
status: public
- id: '1391'
relation: part_of_dissertation
status: public
- id: '1501'
relation: part_of_dissertation
status: public
- id: '1502'
relation: part_of_dissertation
status: public
- id: '2063'
relation: part_of_dissertation
status: public
- id: '2167'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
title: Statistical and logical methods for property checking
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2017'
...
---
_id: '6291'
abstract:
- lang: eng
text: Bacteria and their pathogens – phages – are the most abundant living entities
on Earth. Throughout their coevolution, bacteria have evolved multiple immune
systems to overcome the ubiquitous threat from the phages. Although the molecu-
lar details of these immune systems’ functions are relatively well understood,
their epidemiological consequences for the phage-bacterial communities have been
largely neglected. In this thesis we employed both experimental and theoretical
methods to explore whether herd and social immunity may arise in bacterial popu-
lations. Using our experimental system consisting of Escherichia coli strains
with a CRISPR based immunity to the T7 phage we show that herd immunity arises
in phage-bacterial communities and that it is accentuated when the populations
are spatially structured. By fitting a mathematical model, we inferred expressions
for the herd immunity threshold and the velocity of spread of a phage epidemic
in partially resistant bacterial populations, which both depend on the bacterial
growth rate, phage burst size and phage latent period. We also investigated the
poten- tial for social immunity in Streptococcus thermophilus and its phage 2972
using a bioinformatic analysis of potentially coding short open reading frames
with a signalling signature, encoded within the CRISPR associated genes. Subsequently,
we tested one identified potentially signalling peptide and found that its addition
to a phage-challenged culture increases probability of survival of bacteria two
fold, although the results were only marginally significant. Together, these results
demonstrate that the ubiquitous arms races between bacteria and phages have further
consequences at the level of the population.
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Pavel
full_name: Payne, Pavel
id: 35F78294-F248-11E8-B48F-1D18A9856A87
last_name: Payne
orcid: 0000-0002-2711-9453
citation:
ama: Payne P. Bacterial herd and social immunity to phages. 2017.
apa: Payne, P. (2017). Bacterial herd and social immunity to phages. Institute
of Science and Technology Austria.
chicago: Payne, Pavel. “Bacterial Herd and Social Immunity to Phages.” Institute
of Science and Technology Austria, 2017.
ieee: P. Payne, “Bacterial herd and social immunity to phages,” Institute of Science
and Technology Austria, 2017.
ista: Payne P. 2017. Bacterial herd and social immunity to phages. Institute of
Science and Technology Austria.
mla: Payne, Pavel. Bacterial Herd and Social Immunity to Phages. Institute
of Science and Technology Austria, 2017.
short: P. Payne, Bacterial Herd and Social Immunity to Phages, Institute of Science
and Technology Austria, 2017.
date_created: 2019-04-09T15:16:45Z
date_published: 2017-02-01T00:00:00Z
date_updated: 2023-09-07T12:00:00Z
day: '01'
ddc:
- '570'
degree_awarded: PhD
department:
- _id: NiBa
- _id: JoBo
file:
- access_level: closed
checksum: a0fc5c26a89c0ea759947ffba87d0d8f
content_type: application/pdf
creator: dernst
date_created: 2019-04-09T15:15:32Z
date_updated: 2020-07-14T12:47:27Z
file_id: '6292'
file_name: thesis_pavel_payne_final_w_signature_page.pdf
file_size: 3025175
relation: main_file
- access_level: open_access
checksum: af531e921a7f64a9e0af4cd8783b2226
content_type: application/pdf
creator: dernst
date_created: 2021-02-22T13:45:59Z
date_updated: 2021-02-22T13:45:59Z
file_id: '9187'
file_name: 2017_Payne_Thesis.pdf
file_size: 3111536
relation: main_file
success: 1
file_date_updated: 2021-02-22T13:45:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '83'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
status: public
supervisor:
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
title: Bacterial herd and social immunity to phages
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2017'
...
---
_id: '561'
abstract:
- lang: eng
text: Restriction–modification systems are widespread genetic elements that protect
bacteria from bacteriophage infections by recognizing and cleaving heterologous
DNA at short, well-defined sequences called restriction sites. Bioinformatic evidence
shows that restriction sites are significantly underrepresented in bacteriophage
genomes, presumably because bacteriophages with fewer restriction sites are more
likely to escape cleavage by restriction–modification systems. However, how mutations
in restriction sites affect the likelihood of bacteriophage escape is unknown.
Using the bacteriophage l and the restriction–modification system EcoRI, we show
that while mutation effects at different restriction sites are unequal, they are
independent. As a result, the probability of bacteriophage escape increases with
each mutated restriction site. Our results experimentally support the role of
restriction site avoidance as a response to selection imposed by restriction–modification
systems and offer an insight into the events underlying the process of bacteriophage
escape.
acknowledgement: This work was funded by an HFSP Young Investigators' grant RGY0079/2011
(C.C.G.). M.P. is a recipient of a DOC Fellowship of the Austrian Academy of Science
at the Institute of Science and Technology Austria.
article_number: '20170646'
article_processing_charge: No
article_type: original
author:
- first_name: Maros
full_name: Pleska, Maros
id: 4569785E-F248-11E8-B48F-1D18A9856A87
last_name: Pleska
orcid: 0000-0001-7460-7479
- first_name: Calin C
full_name: Guet, Calin C
id: 47F8433E-F248-11E8-B48F-1D18A9856A87
last_name: Guet
orcid: 0000-0001-6220-2052
citation:
ama: Pleska M, Guet CC. Effects of mutations in phage restriction sites during escape
from restriction–modification. Biology Letters. 2017;13(12). doi:10.1098/rsbl.2017.0646
apa: Pleska, M., & Guet, C. C. (2017). Effects of mutations in phage restriction
sites during escape from restriction–modification. Biology Letters. The
Royal Society. https://doi.org/10.1098/rsbl.2017.0646
chicago: Pleska, Maros, and Calin C Guet. “Effects of Mutations in Phage Restriction
Sites during Escape from Restriction–Modification.” Biology Letters. The
Royal Society, 2017. https://doi.org/10.1098/rsbl.2017.0646.
ieee: M. Pleska and C. C. Guet, “Effects of mutations in phage restriction sites
during escape from restriction–modification,” Biology Letters, vol. 13,
no. 12. The Royal Society, 2017.
ista: Pleska M, Guet CC. 2017. Effects of mutations in phage restriction sites during
escape from restriction–modification. Biology Letters. 13(12), 20170646.
mla: Pleska, Maros, and Calin C. Guet. “Effects of Mutations in Phage Restriction
Sites during Escape from Restriction–Modification.” Biology Letters, vol.
13, no. 12, 20170646, The Royal Society, 2017, doi:10.1098/rsbl.2017.0646.
short: M. Pleska, C.C. Guet, Biology Letters 13 (2017).
date_created: 2018-12-11T11:47:11Z
date_published: 2017-12-01T00:00:00Z
date_updated: 2023-09-07T11:59:32Z
day: '01'
department:
- _id: CaGu
doi: 10.1098/rsbl.2017.0646
external_id:
pmid:
- '29237814'
intvolume: ' 13'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1098/rsbl.2017.0646
month: '12'
oa: 1
oa_version: Published Version
pmid: 1
project:
- _id: 251BCBEC-B435-11E9-9278-68D0E5697425
grant_number: RGY0079/2011
name: Multi-Level Conflicts in Evolutionary Dynamics of Restriction-Modification
Systems (HFSP Young investigators' grant)
- _id: 251D65D8-B435-11E9-9278-68D0E5697425
grant_number: '24210'
name: Effects of Stochasticity on the Function of Restriction-Modi cation Systems
at the Single-Cell Level (DOC Fellowship)
publication: Biology Letters
publication_identifier:
issn:
- 1744-9561
publication_status: published
publisher: The Royal Society
publist_id: '7253'
quality_controlled: '1'
related_material:
record:
- id: '9847'
relation: research_data
status: public
- id: '202'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Effects of mutations in phage restriction sites during escape from restriction–modification
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2017'
...