---
_id: '1374'
abstract:
- lang: eng
  text: 'We study two-player zero-sum games over infinite-state graphs equipped with
    ωB and finitary conditions. Our first contribution is about the strategy complexity,
    i.e the memory required for winning strategies: we prove that over general infinite-state
    graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory
    suffices for finitary parity games. We then study pushdown games with boundedness
    conditions, with two contributions. First we prove a collapse result for pushdown
    games with ωB-conditions, implying the decidability of solving these games. Second
    we consider pushdown games with finitary parity along with stack boundedness conditions,
    and show that solving these games is EXPTIME-complete.'
alternative_title:
- LIPIcs
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Nathanaël
  full_name: Fijalkow, Nathanaël
  last_name: Fijalkow
citation:
  ama: 'Chatterjee K, Fijalkow N. Infinite-state games with finitary conditions. In:
    <i>22nd EACSL Annual Conference on Computer Science Logic</i>. Vol 23. Leibniz
    International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik; 2013:181-196. doi:<a href="https://doi.org/10.4230/LIPIcs.CSL.2013.181">10.4230/LIPIcs.CSL.2013.181</a>'
  apa: 'Chatterjee, K., &#38; Fijalkow, N. (2013). Infinite-state games with finitary
    conditions. In <i>22nd EACSL Annual Conference on Computer Science Logic</i> (Vol.
    23, pp. 181–196). Torino, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
    <a href="https://doi.org/10.4230/LIPIcs.CSL.2013.181">https://doi.org/10.4230/LIPIcs.CSL.2013.181</a>'
  chicago: Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with
    Finitary Conditions.” In <i>22nd EACSL Annual Conference on Computer Science Logic</i>,
    23:181–96. Leibniz International Proceedings in Informatics. Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik, 2013. <a href="https://doi.org/10.4230/LIPIcs.CSL.2013.181">https://doi.org/10.4230/LIPIcs.CSL.2013.181</a>.
  ieee: K. Chatterjee and N. Fijalkow, “Infinite-state games with finitary conditions,”
    in <i>22nd EACSL Annual Conference on Computer Science Logic</i>, Torino, Italy,
    2013, vol. 23, pp. 181–196.
  ista: 'Chatterjee K, Fijalkow N. 2013. Infinite-state games with finitary conditions.
    22nd EACSL Annual Conference on Computer Science Logic. CSL: Computer Science
    LogicLeibniz International Proceedings in Informatics, LIPIcs, vol. 23, 181–196.'
  mla: Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with
    Finitary Conditions.” <i>22nd EACSL Annual Conference on Computer Science Logic</i>,
    vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–96,
    doi:<a href="https://doi.org/10.4230/LIPIcs.CSL.2013.181">10.4230/LIPIcs.CSL.2013.181</a>.
  short: K. Chatterjee, N. Fijalkow, in:, 22nd EACSL Annual Conference on Computer
    Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–196.
conference:
  end_date: 2013-09-05
  location: Torino, Italy
  name: 'CSL: Computer Science Logic'
  start_date: 203-09-02
date_created: 2018-12-11T11:51:39Z
date_published: 2013-09-01T00:00:00Z
date_updated: 2021-01-12T06:50:14Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CSL.2013.181
ec_funded: 1
file:
- access_level: open_access
  checksum: b7091a3866db573c0db5ec486952255e
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:38Z
  date_updated: 2020-07-14T12:44:47Z
  file_id: '5023'
  file_name: IST-2016-624-v1+1_ChKr_Infinite-state_games_2013_17.pdf
  file_size: 547296
  relation: main_file
file_date_updated: 2020-07-14T12:44:47Z
has_accepted_license: '1'
intvolume: '        23'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '09'
oa: 1
oa_version: Published Version
page: 181 - 196
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 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: 22nd EACSL Annual Conference on Computer Science Logic
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5837'
pubrep_id: '624'
quality_controlled: '1'
scopus_import: 1
series_title: Leibniz International Proceedings in Informatics
status: public
title: Infinite-state games with finitary conditions
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: 23
year: '2013'
...
---
_id: '1376'
abstract:
- lang: eng
  text: 'We consider the distributed synthesis problem for temporal logic specifications.
    Traditionally, the problem has been studied for LTL, and the previous results
    show that the problem is decidable iff there is no information fork in the architecture.
    We consider the problem for fragments of LTL and our main results are as follows:
    (1) We show that the problem is undecidable for architectures with information
    forks even for the fragment of LTL with temporal operators restricted to next
    and eventually. (2) For specifications restricted to globally along with non-nested
    next operators, we establish decidability (in EXPSPACE) for star architectures
    where the processes receive disjoint inputs, whereas we establish undecidability
    for architectures containing an information fork-meet structure. (3) Finally,
    we consider LTL without the next operator, and establish decidability (NEXPTIME-complete)
    for all architectures for a fragment that consists of a set of safety assumptions,
    and a set of guarantees where each guarantee is a safety, reachability, or liveness
    condition.'
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
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
citation:
  ama: 'Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed synthesis
    for LTL fragments. In: <i>13th International Conference on Formal Methods in Computer-Aided
    Design</i>. IEEE; 2013:18-25. doi:<a href="https://doi.org/10.1109/FMCAD.2013.6679386">10.1109/FMCAD.2013.6679386</a>'
  apa: 'Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Pavlogiannis, A. (2013).
    Distributed synthesis for LTL fragments. In <i>13th International Conference on
    Formal Methods in Computer-Aided Design</i> (pp. 18–25). Portland, OR, United
    States: IEEE. <a href="https://doi.org/10.1109/FMCAD.2013.6679386">https://doi.org/10.1109/FMCAD.2013.6679386</a>'
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis.
    “Distributed Synthesis for LTL Fragments.” In <i>13th International Conference
    on Formal Methods in Computer-Aided Design</i>, 18–25. IEEE, 2013. <a href="https://doi.org/10.1109/FMCAD.2013.6679386">https://doi.org/10.1109/FMCAD.2013.6679386</a>.
  ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, “Distributed
    synthesis for LTL fragments,” in <i>13th International Conference on Formal Methods
    in Computer-Aided Design</i>, Portland, OR, United States, 2013, pp. 18–25.
  ista: 'Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis
    for LTL fragments. 13th International Conference on Formal Methods in Computer-Aided
    Design. FMCAD: Formal Methods in Computer-Aided Design, 18–25.'
  mla: Chatterjee, Krishnendu, et al. “Distributed Synthesis for LTL Fragments.” <i>13th
    International Conference on Formal Methods in Computer-Aided Design</i>, IEEE,
    2013, pp. 18–25, doi:<a href="https://doi.org/10.1109/FMCAD.2013.6679386">10.1109/FMCAD.2013.6679386</a>.
  short: K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, in:, 13th International
    Conference on Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 18–25.
conference:
  end_date: 2013-10-23
  location: Portland, OR, United States
  name: 'FMCAD: Formal Methods in Computer-Aided Design'
  start_date: 2013-10-20
date_created: 2018-12-11T11:51:40Z
date_published: 2013-12-11T00:00:00Z
date_updated: 2023-02-23T12:24:53Z
day: '11'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1109/FMCAD.2013.6679386
ec_funded: 1
language:
- iso: eng
month: '12'
oa_version: None
page: 18 - 25
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 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: 13th International Conference on Formal Methods in Computer-Aided Design
publication_status: published
publisher: IEEE
publist_id: '5835'
quality_controlled: '1'
related_material:
  record:
  - id: '5406'
    relation: earlier_version
    status: public
status: public
title: Distributed synthesis for LTL fragments
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '1385'
abstract:
- lang: eng
  text: It is often difficult to correctly implement a Boolean controller for a complex
    system, especially when concurrency is involved. Yet, it may be easy to formally
    specify a controller. For instance, for a pipelined processor it suffices to state
    that the visible behavior of the pipelined system should be identical to a non-pipelined
    reference system (Burch-Dill paradigm). We present a novel procedure to efficiently
    synthesize multiple Boolean control signals from a specification given as a quantified
    first-order formula (with a specific quantifier structure). Our approach uses
    uninterpreted functions to abstract details of the design. We construct an unsatisfiable
    SMT formula from the given specification. Then, from just one proof of unsatisfiability,
    we use a variant of Craig interpolation to compute multiple coordinated interpolants
    that implement the Boolean control signals. Our method avoids iterative learning
    and back-substitution of the control functions. We applied our approach to synthesize
    a controller for a simple two-stage pipelined processor, and present first experimental
    results.
acknowledgement: "This research was supported by the European Commission through project\r\nDIAMOND
  \ (FP7-2009-IST-4-248613), and  QUAINT  (I774-N23),  "
arxiv: 1
author:
- first_name: Georg
  full_name: Hofferek, Georg
  last_name: Hofferek
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Bettina
  full_name: Könighofer, Bettina
  last_name: Könighofer
- first_name: Jie
  full_name: Jiang, Jie
  last_name: Jiang
- first_name: Roderick
  full_name: Bloem, Roderick
  last_name: Bloem
citation:
  ama: 'Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. Synthesizing multiple
    boolean functions using interpolation on a single proof. In: <i>2013 Formal Methods
    in Computer-Aided Design</i>. IEEE; 2013:77-84. doi:<a href="https://doi.org/10.1109/FMCAD.2013.6679394">10.1109/FMCAD.2013.6679394</a>'
  apa: 'Hofferek, G., Gupta, A., Könighofer, B., Jiang, J., &#38; Bloem, R. (2013).
    Synthesizing multiple boolean functions using interpolation on a single proof.
    In <i>2013 Formal Methods in Computer-Aided Design</i> (pp. 77–84). Portland,
    OR, United States: IEEE. <a href="https://doi.org/10.1109/FMCAD.2013.6679394">https://doi.org/10.1109/FMCAD.2013.6679394</a>'
  chicago: Hofferek, Georg, Ashutosh Gupta, Bettina Könighofer, Jie Jiang, and Roderick
    Bloem. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single
    Proof.” In <i>2013 Formal Methods in Computer-Aided Design</i>, 77–84. IEEE, 2013.
    <a href="https://doi.org/10.1109/FMCAD.2013.6679394">https://doi.org/10.1109/FMCAD.2013.6679394</a>.
  ieee: G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, and R. Bloem, “Synthesizing
    multiple boolean functions using interpolation on a single proof,” in <i>2013
    Formal Methods in Computer-Aided Design</i>, Portland, OR, United States, 2013,
    pp. 77–84.
  ista: 'Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. 2013. Synthesizing multiple
    boolean functions using interpolation on a single proof. 2013 Formal Methods in
    Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 77–84.'
  mla: Hofferek, Georg, et al. “Synthesizing Multiple Boolean Functions Using Interpolation
    on a Single Proof.” <i>2013 Formal Methods in Computer-Aided Design</i>, IEEE,
    2013, pp. 77–84, doi:<a href="https://doi.org/10.1109/FMCAD.2013.6679394">10.1109/FMCAD.2013.6679394</a>.
  short: G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, R. Bloem, in:, 2013 Formal
    Methods in Computer-Aided Design, IEEE, 2013, pp. 77–84.
conference:
  end_date: 2013-10-23
  location: Portland, OR, United States
  name: 'FMCAD: Formal Methods in Computer-Aided Design'
  start_date: 2013-10-20
date_created: 2018-12-11T11:51:43Z
date_published: 2013-12-11T00:00:00Z
date_updated: 2021-01-12T06:50:19Z
day: '11'
department:
- _id: ToHe
doi: 10.1109/FMCAD.2013.6679394
ec_funded: 1
external_id:
  arxiv:
  - '1308.4767'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1308.4767
month: '12'
oa: 1
oa_version: Preprint
page: 77 - 84
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: 2013 Formal Methods in Computer-Aided Design
publication_status: published
publisher: IEEE
publist_id: '5825'
quality_controlled: '1'
status: public
title: Synthesizing multiple boolean functions using interpolation on a single proof
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '1387'
abstract:
- lang: eng
  text: Choices made by nondeterministic word automata depend on both the past (the
    prefix of the word read so far) and the future (the suffix yet to be read). In
    several applications, most notably synthesis, the future is diverse or unknown,
    leading to algorithms that are based on deterministic automata. Hoping to retain
    some of the advantages of nondeterministic automata, researchers have studied
    restricted classes of nondeterministic automata. Three such classes are nondeterministic
    automata that are good for trees (GFT; i.e., ones that can be expanded to tree
    automata accepting the derived tree languages, thus whose choices should satisfy
    diverse futures), good for games (GFG; i.e., ones whose choices depend only on
    the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent
    deterministic automata). The theoretical properties and relative merits of the
    different classes are still open, having vagueness on whether they really differ
    from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known
    whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also
    open is the possible succinctness of GFG and GFT automata compared to deterministic
    automata. We study these problems for ω-regular automata with all common acceptance
    conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction
    for GFG automata.
acknowledgement: and ERC Grant QUALITY.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Udi
  full_name: Boker, Udi
  id: 31E297B6-F248-11E8-B48F-1D18A9856A87
  last_name: Boker
- first_name: Denis
  full_name: Kuperberg, Denis
  last_name: Kuperberg
- first_name: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
- first_name: Michał
  full_name: Skrzypczak, Michał
  last_name: Skrzypczak
citation:
  ama: Boker U, Kuperberg D, Kupferman O, Skrzypczak M. Nondeterminism in the presence
    of a diverse or unknown future. 2013;7966(PART 2):89-100. doi:<a href="https://doi.org/10.1007/978-3-642-39212-2_11">10.1007/978-3-642-39212-2_11</a>
  apa: 'Boker, U., Kuperberg, D., Kupferman, O., &#38; Skrzypczak, M. (2013). Nondeterminism
    in the presence of a diverse or unknown future. Presented at the ICALP: Automata,
    Languages and Programming, Riga, Latvia: Springer. <a href="https://doi.org/10.1007/978-3-642-39212-2_11">https://doi.org/10.1007/978-3-642-39212-2_11</a>'
  chicago: Boker, Udi, Denis Kuperberg, Orna Kupferman, and Michał Skrzypczak. “Nondeterminism
    in the Presence of a Diverse or Unknown Future.” Lecture Notes in Computer Science.
    Springer, 2013. <a href="https://doi.org/10.1007/978-3-642-39212-2_11">https://doi.org/10.1007/978-3-642-39212-2_11</a>.
  ieee: U. Boker, D. Kuperberg, O. Kupferman, and M. Skrzypczak, “Nondeterminism in
    the presence of a diverse or unknown future,” vol. 7966, no. PART 2. Springer,
    pp. 89–100, 2013.
  ista: Boker U, Kuperberg D, Kupferman O, Skrzypczak M. 2013. Nondeterminism in the
    presence of a diverse or unknown future. 7966(PART 2), 89–100.
  mla: Boker, Udi, et al. <i>Nondeterminism in the Presence of a Diverse or Unknown
    Future</i>. Vol. 7966, no. PART 2, Springer, 2013, pp. 89–100, doi:<a href="https://doi.org/10.1007/978-3-642-39212-2_11">10.1007/978-3-642-39212-2_11</a>.
  short: U. Boker, D. Kuperberg, O. Kupferman, M. Skrzypczak, 7966 (2013) 89–100.
conference:
  end_date: 2013-07-12
  location: Riga, Latvia
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 2013-07-08
date_created: 2018-12-11T11:51:44Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2020-08-11T10:09:09Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39212-2_11
ec_funded: 1
file:
- access_level: open_access
  checksum: 98bc02e3793072e279ec8d364b381ff3
  content_type: application/pdf
  creator: dernst
  date_created: 2020-05-15T11:05:50Z
  date_updated: 2020-07-14T12:44:48Z
  file_id: '7857'
  file_name: 2013_ICALP_Boker.pdf
  file_size: 276982
  relation: main_file
file_date_updated: 2020-07-14T12:44:48Z
has_accepted_license: '1'
intvolume: '      7966'
issue: PART 2
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 89 - 100
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_status: published
publisher: Springer
publist_id: '5823'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Nondeterminism in the presence of a diverse or unknown future
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7966
year: '2013'
...
---
_id: '1405'
abstract:
- lang: eng
  text: "Motivated by the analysis of highly dynamic message-passing systems, i.e.
    unbounded thread creation, mobility, etc. we present a framework for the analysis
    of depth-bounded systems. Depth-bounded systems are one of the most expressive
    known fragment of the π-calculus for which interesting verification problems are
    still decidable. Even though they are infinite state systems depth-bounded systems
    are well-structured, thus can be analyzed algorithmically. We give an interpretation
    of depth-bounded systems as graph-rewriting systems. This gives more flexibility
    and ease of use to apply depth-bounded systems to other type of systems like shared
    memory concurrency.\r\n\r\nFirst, we develop an adequate domain of limits for
    depth-bounded systems, a prerequisite for the effective representation of downward-closed
    sets. Downward-closed sets are needed by forward saturation-based algorithms to
    represent potentially infinite sets of states. Then, we present an abstract interpretation
    framework to compute the covering set of well-structured transition systems. Because,
    in general, the covering set is not computable, our abstraction over-approximates
    the actual covering set. Our abstraction captures the essence of acceleration
    based-algorithms while giving up enough precision to ensure convergence. We have
    implemented the analysis in the PICASSO tool and show that it is accurate in practice.
    Finally, we build some further analyses like termination using the covering set
    as starting point."
acknowledgement: "This work was supported in part by the Austrian Science Fund NFN
  RiSE (Rigorous Systems Engineering) and by the ERC Advanced Grant QUAREM (Quantitative
  Reactve Modeling).\r\nChapter 2, 3, and 4 are joint work with Thomas A. Henzinger
  and Thomas Wies. Chapter 2 was published in FoSSaCS 2010 as “Forward Analysis of
  Depth-Bounded Processes” [112]. Chapter 3 was published in VMCAI 2012 as “Ideal
  Abstractions for Well-Structured Transition Systems” [114]. Chap- ter 5.1 is joint
  work with Kshitij Bansal, Eric Koskinen, and Thomas Wies. It was published in TACAS
  2013 as “Structural Counter Abstraction” [13]. The author’s contribution in this
  part is mostly related to the implementation. The theory required to understand
  the method and its implementation is quickly recalled to make the thesis self-contained,
  but should not be considered as a contribution. For the details of the methods,
  we refer the reader to the orig- inal publication [13] and the corresponding technical
  report [14]. Chapter 5.2 is ongoing work with Shahram Esmaeilsabzali, Rupak Majumdar,
  and Thomas Wies. I also would like to thank the people who supported over the past
  4 years. My advisor Thomas A. Henzinger who gave me a lot of freedom to work on
  projects I was interested in. My collaborators, especially Thomas Wies with whom
  I worked since the beginning. The members of my thesis committee, Viktor Kun- cak
  and Rupak Majumdar, who also agreed to advise me. Simon Aeschbacher, Pavol Cerny,
  Cezara Dragoi, Arjun Radhakrishna, my family, friends and col- leagues who created
  an enjoyable environment. "
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Damien
  full_name: Zufferey, Damien
  id: 4397AC76-F248-11E8-B48F-1D18A9856A87
  last_name: Zufferey
  orcid: 0000-0002-3197-8736
citation:
  ama: Zufferey D. Analysis of dynamic message passing programs. 2013. doi:<a href="https://doi.org/10.15479/at:ista:1405">10.15479/at:ista:1405</a>
  apa: Zufferey, D. (2013). <i>Analysis of dynamic message passing programs</i>. Institute
    of Science and Technology Austria. <a href="https://doi.org/10.15479/at:ista:1405">https://doi.org/10.15479/at:ista:1405</a>
  chicago: Zufferey, Damien. “Analysis of Dynamic Message Passing Programs.” Institute
    of Science and Technology Austria, 2013. <a href="https://doi.org/10.15479/at:ista:1405">https://doi.org/10.15479/at:ista:1405</a>.
  ieee: D. Zufferey, “Analysis of dynamic message passing programs,” Institute of
    Science and Technology Austria, 2013.
  ista: Zufferey D. 2013. Analysis of dynamic message passing programs. Institute
    of Science and Technology Austria.
  mla: Zufferey, Damien. <i>Analysis of Dynamic Message Passing Programs</i>. Institute
    of Science and Technology Austria, 2013, doi:<a href="https://doi.org/10.15479/at:ista:1405">10.15479/at:ista:1405</a>.
  short: D. Zufferey, Analysis of Dynamic Message Passing Programs, Institute of Science
    and Technology Austria, 2013.
date_created: 2018-12-11T11:51:50Z
date_published: 2013-09-05T00:00:00Z
date_updated: 2023-09-07T11:36:37Z
day: '05'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: ToHe
- _id: GradSch
doi: 10.15479/at:ista:1405
ec_funded: 1
file:
- access_level: open_access
  checksum: ed2d7b52933d134e8dc69d569baa284e
  content_type: application/pdf
  creator: dernst
  date_created: 2021-02-22T11:28:36Z
  date_updated: 2021-02-22T11:28:36Z
  file_id: '9176'
  file_name: 2013_Zufferey_thesis_final.pdf
  file_size: 1514906
  relation: main_file
  success: 1
- access_level: closed
  checksum: cecc4c4b14225bee973d32e3dba91a55
  content_type: application/pdf
  creator: cchlebak
  date_created: 2021-11-16T14:42:52Z
  date_updated: 2021-11-17T13:47:58Z
  file_id: '10298'
  file_name: 2013_Zufferey_thesis_final_pdfa.pdf
  file_size: 1378313
  relation: main_file
file_date_updated: 2021-11-17T13:47:58Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- url: http://dzufferey.github.io/files/2013_thesis.pdf
month: '09'
oa: 1
oa_version: Published Version
page: '134'
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_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5802'
related_material:
  record:
  - id: '2847'
    relation: part_of_dissertation
    status: public
  - id: '3251'
    relation: part_of_dissertation
    status: public
  - id: '4361'
    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: Analysis of dynamic message passing programs
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2013'
...
---
_id: '1406'
abstract:
- lang: eng
  text: Epithelial spreading is a critical part of various developmental and wound
    repair processes. Here we use zebrafish epiboly as a model system to study the
    cellular and molecular mechanisms underlying the spreading of epithelial sheets.
    During zebrafish epiboly the enveloping cell layer (EVL), a simple squamous epithelium,
    spreads over the embryo to eventually cover the entire yolk cell by the end of
    gastrulation. The EVL leading edge is anchored through tight junctions to the
    yolk syncytial layer (YSL), where directly adjacent to the EVL margin a contractile
    actomyosin ring is formed that is thought to drive EVL epiboly. The prevalent
    view in the field was that the contractile ring exerts a pulling force on the
    EVL margin, which pulls the EVL towards the vegetal pole. However, how this force
    is generated and how it affects EVL morphology still remains elusive. Moreover,
    the cellular mechanisms mediating the increase in EVL surface area, while maintaining
    tissue integrity and function are still unclear. Here we show that the YSL actomyosin
    ring pulls on the EVL margin by two distinct force-generating mechanisms. One
    mechanism is based on contraction of the ring around its circumference, as previously
    proposed. The second mechanism is based on actomyosin retrogade flows, generating
    force through resistance against the substrate. The latter can function at any
    epiboly stage even in situations where the contraction-based mechanism is unproductive.
    Additionally, we demonstrate that during epiboly the EVL is subjected to anisotropic
    tension, which guides the orientation of EVL cell division along the main axis
    (animal-vegetal) of tension. The influence of tension in cell division orientation
    involves cell elongation and requires myosin-2 activity for proper spindle alignment.
    Strikingly, we reveal that tension-oriented cell divisions release anisotropic
    tension within the EVL and that in the absence of such divisions, EVL cells undergo
    ectopic fusions. We conclude that forces applied to the EVL by the action of the
    YSL actomyosin ring generate a tension anisotropy in the EVL that orients cell
    divisions, which in turn limit tissue tension increase thereby facilitating tissue
    spreading.
acknowledged_ssus:
- _id: Bio
- _id: PreCl
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Pedro
  full_name: Campinho, Pedro
  id: 3AFBBC42-F248-11E8-B48F-1D18A9856A87
  last_name: Campinho
  orcid: 0000-0002-8526-5416
citation:
  ama: 'Campinho P. Mechanics of zebrafish epiboly: Tension-oriented cell divisions
    limit anisotropic tissue tension in epithelial spreading. 2013.'
  apa: 'Campinho, P. (2013). <i>Mechanics of zebrafish epiboly: Tension-oriented cell
    divisions limit anisotropic tissue tension in epithelial spreading</i>. Institute
    of Science and Technology Austria.'
  chicago: 'Campinho, Pedro. “Mechanics of Zebrafish Epiboly: Tension-Oriented Cell
    Divisions Limit Anisotropic Tissue Tension in Epithelial Spreading.” Institute
    of Science and Technology Austria, 2013.'
  ieee: 'P. Campinho, “Mechanics of zebrafish epiboly: Tension-oriented cell divisions
    limit anisotropic tissue tension in epithelial spreading,” Institute of Science
    and Technology Austria, 2013.'
  ista: 'Campinho P. 2013. Mechanics of zebrafish epiboly: Tension-oriented cell divisions
    limit anisotropic tissue tension in epithelial spreading. Institute of Science
    and Technology Austria.'
  mla: 'Campinho, Pedro. <i>Mechanics of Zebrafish Epiboly: Tension-Oriented Cell
    Divisions Limit Anisotropic Tissue Tension in Epithelial Spreading</i>. Institute
    of Science and Technology Austria, 2013.'
  short: 'P. Campinho, Mechanics of Zebrafish Epiboly: Tension-Oriented Cell Divisions
    Limit Anisotropic Tissue Tension in Epithelial Spreading, Institute of Science
    and Technology Austria, 2013.'
date_created: 2018-12-11T11:51:50Z
date_published: 2013-10-01T00:00:00Z
date_updated: 2023-09-07T11:36:07Z
day: '01'
degree_awarded: PhD
department:
- _id: CaHe
language:
- iso: eng
month: '10'
oa_version: None
page: '123'
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5801'
status: public
supervisor:
- first_name: Carl-Philipp J
  full_name: Heisenberg, Carl-Philipp J
  id: 39427864-F248-11E8-B48F-1D18A9856A87
  last_name: Heisenberg
  orcid: 0000-0002-0912-4566
title: 'Mechanics of zebrafish epiboly: Tension-oriented cell divisions limit anisotropic
  tissue tension in epithelial spreading'
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2013'
...
---
_id: '9459'
abstract:
- lang: eng
  text: Nucleosome remodelers of the DDM1/Lsh family are required for DNA methylation
    of transposable elements, but the reason for this is unknown. How DDM1 interacts
    with other methylation pathways, such as small-RNA-directed DNA methylation (RdDM),
    which is thought to mediate plant asymmetric methylation through DRM enzymes,
    is also unclear. Here, we show that most asymmetric methylation is facilitated
    by DDM1 and mediated by the methyltransferase CMT2 separately from RdDM. We find
    that heterochromatic sequences preferentially require DDM1 for DNA methylation
    and that this preference depends on linker histone H1. RdDM is instead inhibited
    by heterochromatin and absolutely requires the nucleosome remodeler DRD1. Together,
    DDM1 and RdDM mediate nearly all transposon methylation and collaborate to repress
    transposition and regulate the methylation and expression of genes. Our results
    indicate that DDM1 provides DNA methyltransferases access to H1-containing heterochromatin
    to allow stable silencing of transposable elements in cooperation with the RdDM
    pathway.
article_processing_charge: No
article_type: original
author:
- first_name: Assaf
  full_name: Zemach, Assaf
  last_name: Zemach
- first_name: M. Yvonne
  full_name: Kim, M. Yvonne
  last_name: Kim
- first_name: Ping-Hung
  full_name: Hsieh, Ping-Hung
  last_name: Hsieh
- first_name: Devin
  full_name: Coleman-Derr, Devin
  last_name: Coleman-Derr
- first_name: Leor
  full_name: Eshed-Williams, Leor
  last_name: Eshed-Williams
- first_name: Ka
  full_name: Thao, Ka
  last_name: Thao
- first_name: Stacey L.
  full_name: Harmer, Stacey L.
  last_name: Harmer
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
citation:
  ama: Zemach A, Kim MY, Hsieh P-H, et al. The Arabidopsis nucleosome remodeler DDM1
    allows DNA methyltransferases to access H1-containing heterochromatin. <i>Cell</i>.
    2013;153(1):193-205. doi:<a href="https://doi.org/10.1016/j.cell.2013.02.033">10.1016/j.cell.2013.02.033</a>
  apa: Zemach, A., Kim, M. Y., Hsieh, P.-H., Coleman-Derr, D., Eshed-Williams, L.,
    Thao, K., … Zilberman, D. (2013). The Arabidopsis nucleosome remodeler DDM1 allows
    DNA methyltransferases to access H1-containing heterochromatin. <i>Cell</i>. Elsevier.
    <a href="https://doi.org/10.1016/j.cell.2013.02.033">https://doi.org/10.1016/j.cell.2013.02.033</a>
  chicago: Zemach, Assaf, M. Yvonne Kim, Ping-Hung Hsieh, Devin Coleman-Derr, Leor
    Eshed-Williams, Ka Thao, Stacey L. Harmer, and Daniel Zilberman. “The Arabidopsis
    Nucleosome Remodeler DDM1 Allows DNA Methyltransferases to Access H1-Containing
    Heterochromatin.” <i>Cell</i>. Elsevier, 2013. <a href="https://doi.org/10.1016/j.cell.2013.02.033">https://doi.org/10.1016/j.cell.2013.02.033</a>.
  ieee: A. Zemach <i>et al.</i>, “The Arabidopsis nucleosome remodeler DDM1 allows
    DNA methyltransferases to access H1-containing heterochromatin,” <i>Cell</i>,
    vol. 153, no. 1. Elsevier, pp. 193–205, 2013.
  ista: Zemach A, Kim MY, Hsieh P-H, Coleman-Derr D, Eshed-Williams L, Thao K, Harmer
    SL, Zilberman D. 2013. The Arabidopsis nucleosome remodeler DDM1 allows DNA methyltransferases
    to access H1-containing heterochromatin. Cell. 153(1), 193–205.
  mla: Zemach, Assaf, et al. “The Arabidopsis Nucleosome Remodeler DDM1 Allows DNA
    Methyltransferases to Access H1-Containing Heterochromatin.” <i>Cell</i>, vol.
    153, no. 1, Elsevier, 2013, pp. 193–205, doi:<a href="https://doi.org/10.1016/j.cell.2013.02.033">10.1016/j.cell.2013.02.033</a>.
  short: A. Zemach, M.Y. Kim, P.-H. Hsieh, D. Coleman-Derr, L. Eshed-Williams, K.
    Thao, S.L. Harmer, D. Zilberman, Cell 153 (2013) 193–205.
date_created: 2021-06-04T12:23:28Z
date_published: 2013-03-28T00:00:00Z
date_updated: 2021-12-14T08:25:35Z
day: '28'
department:
- _id: DaZi
doi: 10.1016/j.cell.2013.02.033
extern: '1'
external_id:
  pmid:
  - '23540698'
intvolume: '       153'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1016/j.cell.2013.02.033
month: '03'
oa: 1
oa_version: Published Version
page: 193-205
pmid: 1
publication: Cell
publication_identifier:
  eissn:
  - 1097-4172
  issn:
  - 0092-8674
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: The Arabidopsis nucleosome remodeler DDM1 allows DNA methyltransferases to
  access H1-containing heterochromatin
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 153
year: '2013'
...
---
_id: '9481'
abstract:
- lang: eng
  text: Arabidopsis thaliana endosperm, a transient tissue that nourishes the embryo,
    exhibits extensive localized DNA demethylation on maternally inherited chromosomes.
    Demethylation mediates parent-of-origin–specific (imprinted) gene expression but
    is apparently unnecessary for the extensive accumulation of maternally biased
    small RNA (sRNA) molecules detected in seeds. Endosperm DNA in the distantly related
    monocots rice and maize is likewise locally hypomethylated, but whether this hypomethylation
    is generally parent-of-origin specific is unknown. Imprinted expression of sRNA
    also remains uninvestigated in monocot seeds. Here, we report high-coverage sequencing
    of the Kitaake rice cultivar that enabled us to show that localized hypomethylation
    in rice endosperm occurs solely on the maternal genome, preferring regions of
    high DNA accessibility. Maternally expressed imprinted genes are enriched for
    hypomethylation at putative promoter regions and transcriptional termini and paternally
    expressed genes at promoters and gene bodies, mirroring our recent results in
    A. thaliana. However, unlike in A. thaliana, rice endosperm sRNA populations are
    dominated by specific strong sRNA-producing loci, and imprinted 24-nt sRNAs are
    expressed from both parental genomes and correlate with hypomethylation. Overlaps
    between imprinted sRNA loci and imprinted genes expressed from opposite alleles
    suggest that sRNAs may regulate genomic imprinting. Whereas sRNAs in seedling
    tissues primarily originate from small class II (cut-and-paste) transposable elements,
    those in endosperm are more uniformly derived, including sequences from other
    transposon classes, as well as genic and intergenic regions. Our data indicate
    that the endosperm exhibits a unique pattern of sRNA expression and suggest that
    localized hypomethylation of maternal endosperm DNA is conserved in flowering
    plants.
article_processing_charge: No
article_type: original
author:
- first_name: Jessica A.
  full_name: Rodrigues, Jessica A.
  last_name: Rodrigues
- first_name: Randy
  full_name: Ruan, Randy
  last_name: Ruan
- first_name: Toshiro
  full_name: Nishimura, Toshiro
  last_name: Nishimura
- first_name: Manoj K.
  full_name: Sharma, Manoj K.
  last_name: Sharma
- first_name: Rita
  full_name: Sharma, Rita
  last_name: Sharma
- first_name: Pamela C
  full_name: Ronald, Pamela C
  last_name: Ronald
- first_name: Robert L.
  full_name: Fischer, Robert L.
  last_name: Fischer
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
citation:
  ama: Rodrigues JA, Ruan R, Nishimura T, et al. Imprinted expression of genes and
    small RNA is associated with localized hypomethylation of the maternal genome
    in rice endosperm. <i>Proceedings of the National Academy of Sciences</i>. 2013;110(19):7934-7939.
    doi:<a href="https://doi.org/10.1073/pnas.1306164110">10.1073/pnas.1306164110</a>
  apa: Rodrigues, J. A., Ruan, R., Nishimura, T., Sharma, M. K., Sharma, R., Ronald,
    P. C., … Zilberman, D. (2013). Imprinted expression of genes and small RNA is
    associated with localized hypomethylation of the maternal genome in rice endosperm.
    <i>Proceedings of the National Academy of Sciences</i>. National Academy of Sciences.
    <a href="https://doi.org/10.1073/pnas.1306164110">https://doi.org/10.1073/pnas.1306164110</a>
  chicago: Rodrigues, Jessica A., Randy Ruan, Toshiro Nishimura, Manoj K. Sharma,
    Rita Sharma, Pamela C Ronald, Robert L. Fischer, and Daniel Zilberman. “Imprinted
    Expression of Genes and Small RNA Is Associated with Localized Hypomethylation
    of the Maternal Genome in Rice Endosperm.” <i>Proceedings of the National Academy
    of Sciences</i>. National Academy of Sciences, 2013. <a href="https://doi.org/10.1073/pnas.1306164110">https://doi.org/10.1073/pnas.1306164110</a>.
  ieee: J. A. Rodrigues <i>et al.</i>, “Imprinted expression of genes and small RNA
    is associated with localized hypomethylation of the maternal genome in rice endosperm,”
    <i>Proceedings of the National Academy of Sciences</i>, vol. 110, no. 19. National
    Academy of Sciences, pp. 7934–7939, 2013.
  ista: Rodrigues JA, Ruan R, Nishimura T, Sharma MK, Sharma R, Ronald PC, Fischer
    RL, Zilberman D. 2013. Imprinted expression of genes and small RNA is associated
    with localized hypomethylation of the maternal genome in rice endosperm. Proceedings
    of the National Academy of Sciences. 110(19), 7934–7939.
  mla: Rodrigues, Jessica A., et al. “Imprinted Expression of Genes and Small RNA
    Is Associated with Localized Hypomethylation of the Maternal Genome in Rice Endosperm.”
    <i>Proceedings of the National Academy of Sciences</i>, vol. 110, no. 19, National
    Academy of Sciences, 2013, pp. 7934–39, doi:<a href="https://doi.org/10.1073/pnas.1306164110">10.1073/pnas.1306164110</a>.
  short: J.A. Rodrigues, R. Ruan, T. Nishimura, M.K. Sharma, R. Sharma, P.C. Ronald,
    R.L. Fischer, D. Zilberman, Proceedings of the National Academy of Sciences 110
    (2013) 7934–7939.
date_created: 2021-06-07T07:31:02Z
date_published: 2013-05-07T00:00:00Z
date_updated: 2021-12-14T08:26:44Z
day: '07'
department:
- _id: DaZi
doi: 10.1073/pnas.1306164110
extern: '1'
external_id:
  pmid:
  - '23613580'
intvolume: '       110'
issue: '19'
keyword:
- Multidisciplinary
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1073/pnas.1306164110
month: '05'
oa: 1
oa_version: Published Version
page: 7934-7939
pmid: 1
publication: Proceedings of the National Academy of Sciences
publication_identifier:
  eissn:
  - 1091-6490
  issn:
  - 0027-8424
publication_status: published
publisher: National Academy of Sciences
quality_controlled: '1'
scopus_import: '1'
status: public
title: Imprinted expression of genes and small RNA is associated with localized hypomethylation
  of the maternal genome in rice endosperm
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 110
year: '2013'
...
---
_id: '9520'
abstract:
- lang: eng
  text: Plants undergo alternation of generation in which reproductive cells develop
    in the plant body ("sporophytic generation") and then differentiate into a multicellular
    gamete-forming "gametophytic generation." Different populations of helper cells
    assist in this transgenerational journey, with somatic tissues supporting early
    development and single nurse cells supporting gametogenesis. New data reveal a
    two-way relationship between early reproductive cells and their helpers involving
    complex epigenetic and signaling networks determining cell number and fate. Later,
    the egg cell plays a central role in specifying accessory cells, whereas in both
    gametophytes, companion cells contribute non-cell-autonomously to the epigenetic
    landscape of the gamete genomes.
article_processing_charge: No
article_type: review
author:
- first_name: Xiaoqi
  full_name: Feng, Xiaoqi
  id: e0164712-22ee-11ed-b12a-d80fcdf35958
  last_name: Feng
  orcid: 0000-0002-4008-1234
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
- first_name: Hugh
  full_name: Dickinson, Hugh
  last_name: Dickinson
citation:
  ama: 'Feng X, Zilberman D, Dickinson H. A conversation across generations: Soma-germ
    cell crosstalk in plants. <i>Developmental Cell</i>. 2013;24(3):215-225. doi:<a
    href="https://doi.org/10.1016/j.devcel.2013.01.014">10.1016/j.devcel.2013.01.014</a>'
  apa: 'Feng, X., Zilberman, D., &#38; Dickinson, H. (2013). A conversation across
    generations: Soma-germ cell crosstalk in plants. <i>Developmental Cell</i>. Elsevier.
    <a href="https://doi.org/10.1016/j.devcel.2013.01.014">https://doi.org/10.1016/j.devcel.2013.01.014</a>'
  chicago: 'Feng, Xiaoqi, Daniel Zilberman, and Hugh Dickinson. “A Conversation across
    Generations: Soma-Germ Cell Crosstalk in Plants.” <i>Developmental Cell</i>. Elsevier,
    2013. <a href="https://doi.org/10.1016/j.devcel.2013.01.014">https://doi.org/10.1016/j.devcel.2013.01.014</a>.'
  ieee: 'X. Feng, D. Zilberman, and H. Dickinson, “A conversation across generations:
    Soma-germ cell crosstalk in plants,” <i>Developmental Cell</i>, vol. 24, no. 3.
    Elsevier, pp. 215–225, 2013.'
  ista: 'Feng X, Zilberman D, Dickinson H. 2013. A conversation across generations:
    Soma-germ cell crosstalk in plants. Developmental Cell. 24(3), 215–225.'
  mla: 'Feng, Xiaoqi, et al. “A Conversation across Generations: Soma-Germ Cell Crosstalk
    in Plants.” <i>Developmental Cell</i>, vol. 24, no. 3, Elsevier, 2013, pp. 215–25,
    doi:<a href="https://doi.org/10.1016/j.devcel.2013.01.014">10.1016/j.devcel.2013.01.014</a>.'
  short: X. Feng, D. Zilberman, H. Dickinson, Developmental Cell 24 (2013) 215–225.
date_created: 2021-06-08T06:14:50Z
date_published: 2013-02-11T00:00:00Z
date_updated: 2023-05-08T11:00:59Z
day: '11'
department:
- _id: DaZi
- _id: XiFe
doi: 10.1016/j.devcel.2013.01.014
extern: '1'
external_id:
  pmid:
  - '23410937'
intvolume: '        24'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1016/j.devcel.2013.01.014
month: '02'
oa: 1
oa_version: Published Version
page: 215-225
pmid: 1
publication: Developmental Cell
publication_identifier:
  eissn:
  - 1878-1551
  issn:
  - 1534-5807
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'A conversation across generations: Soma-germ cell crosstalk in plants'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 24
year: '2013'
...
---
_id: '10396'
abstract:
- lang: eng
  text: Stimfit is a free cross-platform software package for viewing and analyzing
    electrophysiological data. It supports most standard file types for cellular neurophysiology
    and other biomedical formats. Its analysis algorithms have been used and validated
    in several experimental laboratories. Its embedded Python scripting interface
    makes Stimfit highly extensible and customizable.
article_number: '000010151520134181'
article_processing_charge: No
article_type: original
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: Peter M
  full_name: Jonas, Peter M
  id: 353C1B58-F248-11E8-B48F-1D18A9856A87
  last_name: Jonas
  orcid: 0000-0001-5001-4804
- first_name: C.
  full_name: Schmidt-Hieber, C.
  last_name: Schmidt-Hieber
- first_name: S. J.
  full_name: Guzman, S. J.
  last_name: Guzman
citation:
  ama: 'Schlögl A, Jonas PM, Schmidt-Hieber C, Guzman SJ. Stimfit: A fast visualization
    and analysis environment for cellular neurophysiology. <i>Biomedical Engineering
    / Biomedizinische Technik</i>. 2013;58(SI-1-Track-G). doi:<a href="https://doi.org/10.1515/bmt-2013-4181">10.1515/bmt-2013-4181</a>'
  apa: 'Schlögl, A., Jonas, P. M., Schmidt-Hieber, C., &#38; Guzman, S. J. (2013).
    Stimfit: A fast visualization and analysis environment for cellular neurophysiology.
    <i>Biomedical Engineering / Biomedizinische Technik</i>. Graz, Austria: De Gruyter.
    <a href="https://doi.org/10.1515/bmt-2013-4181">https://doi.org/10.1515/bmt-2013-4181</a>'
  chicago: 'Schlögl, Alois, Peter M Jonas, C. Schmidt-Hieber, and S. J. Guzman. “Stimfit:
    A Fast Visualization and Analysis Environment for Cellular Neurophysiology.” <i>Biomedical
    Engineering / Biomedizinische Technik</i>. De Gruyter, 2013. <a href="https://doi.org/10.1515/bmt-2013-4181">https://doi.org/10.1515/bmt-2013-4181</a>.'
  ieee: 'A. Schlögl, P. M. Jonas, C. Schmidt-Hieber, and S. J. Guzman, “Stimfit: A
    fast visualization and analysis environment for cellular neurophysiology,” <i>Biomedical
    Engineering / Biomedizinische Technik</i>, vol. 58, no. SI-1-Track-G. De Gruyter,
    2013.'
  ista: 'Schlögl A, Jonas PM, Schmidt-Hieber C, Guzman SJ. 2013. Stimfit: A fast visualization
    and analysis environment for cellular neurophysiology. Biomedical Engineering
    / Biomedizinische Technik. 58(SI-1-Track-G), 000010151520134181.'
  mla: 'Schlögl, Alois, et al. “Stimfit: A Fast Visualization and Analysis Environment
    for Cellular Neurophysiology.” <i>Biomedical Engineering / Biomedizinische Technik</i>,
    vol. 58, no. SI-1-Track-G, 000010151520134181, De Gruyter, 2013, doi:<a href="https://doi.org/10.1515/bmt-2013-4181">10.1515/bmt-2013-4181</a>.'
  short: A. Schlögl, P.M. Jonas, C. Schmidt-Hieber, S.J. Guzman, Biomedical Engineering
    / Biomedizinische Technik 58 (2013).
conference:
  end_date: 2013-09-21
  location: Graz, Austria
  name: 'BMT: Biomedizinische Technik '
  start_date: 2013-09-19
date_created: 2021-12-01T14:35:35Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2021-12-02T12:51:12Z
day: '01'
ddc:
- '005'
- '610'
department:
- _id: PeJo
doi: 10.1515/bmt-2013-4181
external_id:
  pmid:
  - '24042795'
file:
- access_level: open_access
  checksum: cdfc5339b530a25d6079f7223f0b1f16
  content_type: application/pdf
  creator: schloegl
  date_created: 2021-12-01T14:38:08Z
  date_updated: 2021-12-01T14:38:08Z
  file_id: '10397'
  file_name: Schloegl_Abstract-BMT2013.pdf
  file_size: 149825
  relation: main_file
  success: 1
file_date_updated: 2021-12-01T14:38:08Z
has_accepted_license: '1'
intvolume: '        58'
issue: SI-1-Track-G
keyword:
- biomedical engineering
- data analysis
- free software
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
pmid: 1
publication: Biomedical Engineering / Biomedizinische Technik
publication_identifier:
  eissn:
  - 1862-278X
  issn:
  - 0013-5585
publication_status: published
publisher: De Gruyter
quality_controlled: '1'
status: public
title: 'Stimfit: A fast visualization and analysis environment for cellular neurophysiology'
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 58
year: '2013'
...
---
_id: '9749'
abstract:
- lang: eng
  text: Cooperative behavior, where one individual incurs a cost to help another,
    is a wide spread phenomenon. Here we study direct reciprocity in the context of
    the alternating Prisoner's Dilemma. We consider all strategies that can be implemented
    by one and two-state automata. We calculate the payoff matrix of all pairwise
    encounters in the presence of noise. We explore deterministic selection dynamics
    with and without mutation. Using different error rates and payoff values, we observe
    convergence to a small number of distinct equilibria. Two of them are uncooperative
    strict Nash equilibria representing always-defect (ALLD) and Grim. The third equilibrium
    is mixed and represents a cooperative alliance of several strategies, dominated
    by a strategy which we call Forgiver. Forgiver cooperates whenever the opponent
    has cooperated; it defects once when the opponent has defected, but subsequently
    Forgiver attempts to re-establish cooperation even if the opponent has defected
    again. Forgiver is not an evolutionarily stable strategy, but the alliance, which
    it rules, is asymptotically stable. For a wide range of parameter values the most
    commonly observed outcome is convergence to the mixed equilibrium, dominated by
    Forgiver. Our results show that although forgiving might incur a short-term loss
    it can lead to a long-term gain. Forgiveness facilitates stable cooperation in
    the presence of exploitation and noise.
article_processing_charge: No
author:
- first_name: Benjamin
  full_name: Zagorsky, Benjamin
  last_name: Zagorsky
- first_name: Johannes
  full_name: Reiter, Johannes
  id: 4A918E98-F248-11E8-B48F-1D18A9856A87
  last_name: Reiter
  orcid: 0000-0002-0170-7353
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Martin
  full_name: Nowak, Martin
  last_name: Nowak
citation:
  ama: Zagorsky B, Reiter J, Chatterjee K, Nowak M. Forgiver triumphs in alternating
    prisoner’s dilemma . 2013. doi:<a href="https://doi.org/10.1371/journal.pone.0080814.s001">10.1371/journal.pone.0080814.s001</a>
  apa: Zagorsky, B., Reiter, J., Chatterjee, K., &#38; Nowak, M. (2013). Forgiver
    triumphs in alternating prisoner’s dilemma . Public Library of Science. <a href="https://doi.org/10.1371/journal.pone.0080814.s001">https://doi.org/10.1371/journal.pone.0080814.s001</a>
  chicago: Zagorsky, Benjamin, Johannes Reiter, Krishnendu Chatterjee, and Martin
    Nowak. “Forgiver Triumphs in Alternating Prisoner’s Dilemma .” Public Library
    of Science, 2013. <a href="https://doi.org/10.1371/journal.pone.0080814.s001">https://doi.org/10.1371/journal.pone.0080814.s001</a>.
  ieee: B. Zagorsky, J. Reiter, K. Chatterjee, and M. Nowak, “Forgiver triumphs in
    alternating prisoner’s dilemma .” Public Library of Science, 2013.
  ista: Zagorsky B, Reiter J, Chatterjee K, Nowak M. 2013. Forgiver triumphs in alternating
    prisoner’s dilemma , Public Library of Science, <a href="https://doi.org/10.1371/journal.pone.0080814.s001">10.1371/journal.pone.0080814.s001</a>.
  mla: Zagorsky, Benjamin, et al. <i>Forgiver Triumphs in Alternating Prisoner’s Dilemma
    </i>. Public Library of Science, 2013, doi:<a href="https://doi.org/10.1371/journal.pone.0080814.s001">10.1371/journal.pone.0080814.s001</a>.
  short: B. Zagorsky, J. Reiter, K. Chatterjee, M. Nowak, (2013).
date_created: 2021-07-28T15:45:07Z
date_published: 2013-12-12T00:00:00Z
date_updated: 2023-02-23T10:34:39Z
day: '12'
department:
- _id: KrCh
doi: 10.1371/journal.pone.0080814.s001
month: '12'
oa_version: Published Version
publisher: Public Library of Science
related_material:
  record:
  - id: '2247'
    relation: used_in_publication
    status: public
status: public
title: 'Forgiver triumphs in alternating prisoner''s dilemma '
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2013'
...
---
_id: '9751'
abstract:
- lang: eng
  text: High relatedness among interacting individuals has generally been considered
    a precondition for the evolution of altruism. However, kin-selection theory also
    predicts the evolution of altruism when relatedness is low, as long as the cost
    of the altruistic act is minor compared to its benefit. Here, we demonstrate evidence
    for a low-cost altruistic act in bacteria. We investigated Escherichia coli responding
    to the attack of an obligately lytic phage by committing suicide in order to prevent
    parasite transmission to nearby relatives. We found that bacterial suicide provides
    large benefits to survivors at marginal costs to committers. The cost of suicide
    was low because infected cells are moribund, rapidly dying upon phage infection,
    such that no more opportunity for reproduction remains. As a consequence of its
    marginal cost, host suicide was selectively favoured even when relatedness between
    committers and survivors approached zero. Altogether, our findings demonstrate
    that low-cost suicide can evolve with ease, represents an effective host-defence
    strategy, and seems to be widespread among microbes. Moreover, low-cost suicide
    might also occur in higher organisms as exemplified by infected social insect
    workers leaving the colony to die in isolation.
article_processing_charge: No
author:
- first_name: Dominik
  full_name: Refardt, Dominik
  last_name: Refardt
- first_name: Tobias
  full_name: Bergmiller, Tobias
  id: 2C471CFA-F248-11E8-B48F-1D18A9856A87
  last_name: Bergmiller
  orcid: 0000-0001-5396-4346
- first_name: Rolf
  full_name: Kümmerli, Rolf
  last_name: Kümmerli
citation:
  ama: 'Refardt D, Bergmiller T, Kümmerli R. Data from: Altruism can evolve when relatedness
    is low: evidence from bacteria committing suicide upon phage infection. 2013.
    doi:<a href="https://doi.org/10.5061/dryad.b1q2n">10.5061/dryad.b1q2n</a>'
  apa: 'Refardt, D., Bergmiller, T., &#38; Kümmerli, R. (2013). Data from: Altruism
    can evolve when relatedness is low: evidence from bacteria committing suicide
    upon phage infection. Dryad. <a href="https://doi.org/10.5061/dryad.b1q2n">https://doi.org/10.5061/dryad.b1q2n</a>'
  chicago: 'Refardt, Dominik, Tobias Bergmiller, and Rolf Kümmerli. “Data from: Altruism
    Can Evolve When Relatedness Is Low: Evidence from Bacteria Committing Suicide
    upon Phage Infection.” Dryad, 2013. <a href="https://doi.org/10.5061/dryad.b1q2n">https://doi.org/10.5061/dryad.b1q2n</a>.'
  ieee: 'D. Refardt, T. Bergmiller, and R. Kümmerli, “Data from: Altruism can evolve
    when relatedness is low: evidence from bacteria committing suicide upon phage
    infection.” Dryad, 2013.'
  ista: 'Refardt D, Bergmiller T, Kümmerli R. 2013. Data from: Altruism can evolve
    when relatedness is low: evidence from bacteria committing suicide upon phage
    infection, Dryad, <a href="https://doi.org/10.5061/dryad.b1q2n">10.5061/dryad.b1q2n</a>.'
  mla: 'Refardt, Dominik, et al. <i>Data from: Altruism Can Evolve When Relatedness
    Is Low: Evidence from Bacteria Committing Suicide upon Phage Infection</i>. Dryad,
    2013, doi:<a href="https://doi.org/10.5061/dryad.b1q2n">10.5061/dryad.b1q2n</a>.'
  short: D. Refardt, T. Bergmiller, R. Kümmerli, (2013).
date_created: 2021-07-30T08:08:09Z
date_published: 2013-03-21T00:00:00Z
date_updated: 2023-10-18T06:43:22Z
day: '21'
department:
- _id: CaGu
doi: 10.5061/dryad.b1q2n
main_file_link:
- open_access: '1'
  url: https://doi.org/10.5061/dryad.b1q2n
month: '03'
oa: 1
oa_version: Published Version
publisher: Dryad
related_material:
  record:
  - id: '2853'
    relation: used_in_publication
    status: public
status: public
title: 'Data from: Altruism can evolve when relatedness is low: evidence from bacteria
  committing suicide upon phage infection'
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2013'
...
---
_id: '9754'
abstract:
- lang: eng
  text: Short-read sequencing technologies have in principle made it feasible to draw
    detailed inferences about the recent history of any organism. In practice, however,
    this remains challenging due to the difficulty of genome assembly in most organisms
    and the lack of statistical methods powerful enough to discriminate among recent,
    non-equilibrium histories. We address both the assembly and inference challenges.
    We develop a bioinformatic pipeline for generating outgroup-rooted alignments
    of orthologous sequence blocks from de novo low-coverage short-read data for a
    small number of genomes, and show how such sequence blocks can be used to fit
    explicit models of population divergence and admixture in a likelihood framework.
    To illustrate our approach, we reconstruct the Pleistocene history of an oak-feeding
    insect (the oak gallwasp Biorhiza pallida) which, in common with many other taxa,
    was restricted during Pleistocene ice ages to a longitudinal series of southern
    refugia spanning theWestern Palaearctic. Our analysis of sequence blocks sampled
    from a single genome from each of three major glacial refugia reveals support
    for an unexpected history dominated by recent admixture. Despite the fact that
    80% of the genome is affected by admixture during the last glacial cycle, we are
    able to infer the deeper divergence history of these populations. These inferences
    are robust to variation in block length, mutation model, and the sampling location
    of individual genomes within refugia. This combination of de novo assembly and
    numerical likelihood calculation provides a powerful framework for estimating
    recent population history that can be applied to any organism without the need
    for prior genetic resources.
article_processing_charge: No
author:
- first_name: Jack
  full_name: Hearn, Jack
  last_name: Hearn
- first_name: Graham
  full_name: Stone, Graham
  last_name: Stone
- first_name: Nicholas H
  full_name: Barton, Nicholas H
  id: 4880FE40-F248-11E8-B48F-1D18A9856A87
  last_name: Barton
  orcid: 0000-0002-8548-5240
- first_name: Konrad
  full_name: Lohse, Konrad
  last_name: Lohse
- first_name: Lynsey
  full_name: Bunnefeld, Lynsey
  last_name: Bunnefeld
citation:
  ama: 'Hearn J, Stone G, Barton NH, Lohse K, Bunnefeld L. Data from: Likelihood-based
    inference of population history from low coverage de novo genome assemblies. 2013.
    doi:<a href="https://doi.org/10.5061/dryad.r3r60">10.5061/dryad.r3r60</a>'
  apa: 'Hearn, J., Stone, G., Barton, N. H., Lohse, K., &#38; Bunnefeld, L. (2013).
    Data from: Likelihood-based inference of population history from low coverage
    de novo genome assemblies. Dryad. <a href="https://doi.org/10.5061/dryad.r3r60">https://doi.org/10.5061/dryad.r3r60</a>'
  chicago: 'Hearn, Jack, Graham Stone, Nicholas H Barton, Konrad Lohse, and Lynsey
    Bunnefeld. “Data from: Likelihood-Based Inference of Population History from Low
    Coverage de Novo Genome Assemblies.” Dryad, 2013. <a href="https://doi.org/10.5061/dryad.r3r60">https://doi.org/10.5061/dryad.r3r60</a>.'
  ieee: 'J. Hearn, G. Stone, N. H. Barton, K. Lohse, and L. Bunnefeld, “Data from:
    Likelihood-based inference of population history from low coverage de novo genome
    assemblies.” Dryad, 2013.'
  ista: 'Hearn J, Stone G, Barton NH, Lohse K, Bunnefeld L. 2013. Data from: Likelihood-based
    inference of population history from low coverage de novo genome assemblies, Dryad,
    <a href="https://doi.org/10.5061/dryad.r3r60">10.5061/dryad.r3r60</a>.'
  mla: 'Hearn, Jack, et al. <i>Data from: Likelihood-Based Inference of Population
    History from Low Coverage de Novo Genome Assemblies</i>. Dryad, 2013, doi:<a href="https://doi.org/10.5061/dryad.r3r60">10.5061/dryad.r3r60</a>.'
  short: J. Hearn, G. Stone, N.H. Barton, K. Lohse, L. Bunnefeld, (2013).
date_created: 2021-07-30T08:31:22Z
date_published: 2013-10-01T00:00:00Z
date_updated: 2023-02-23T10:31:17Z
day: '01'
department:
- _id: NiBa
doi: 10.5061/dryad.r3r60
main_file_link:
- open_access: '1'
  url: https://doi.org/10.5061/dryad.r3r60
month: '10'
oa: 1
oa_version: Published Version
publisher: Dryad
related_material:
  record:
  - id: '2170'
    relation: used_in_publication
    status: public
status: public
title: 'Data from: Likelihood-based inference of population history from low coverage
  de novo genome assemblies'
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2013'
...
---
_id: '450'
abstract:
- lang: eng
  text: Understanding the relative importance of heterosis and outbreeding depression
    over multiple generations is a key question in evolutionary biology and is essential
    for identifying appropriate genetic sources for population and ecosystem restoration.
    Here we use 2455 experimental crosses between 12 population pairs of the rare
    perennial plant Rutidosis leptorrhynchoides (Asteraceae) to investigate the multi-generational
    (F1, F2, F3) fitness outcomes of inter-population hybridization. We detected no
    evidence of outbreeding depression, with inter-population hybrids and backcrosses
    showing either similar fitness or significant heterosis for fitness components
    across the three generations. Variation in heterosis among population pairs was
    best explained by characteristics of the foreign source or home population, and
    was greatest when the source population was large, with high genetic diversity
    and low inbreeding, and the home population was small and inbred. Our results
    indicate that the primary consideration for maximizing progeny fitness following
    population augmentation or restoration is the use of seed from large, genetically
    diverse populations.
article_number: '2058'
author:
- first_name: Melinda
  full_name: Pickup, Melinda
  id: 2C78037E-F248-11E8-B48F-1D18A9856A87
  last_name: Pickup
  orcid: 0000-0001-6118-0541
- first_name: David
  full_name: Field, David
  id: 419049E2-F248-11E8-B48F-1D18A9856A87
  last_name: Field
  orcid: 0000-0002-4014-8478
- first_name: David
  full_name: Rowell, David
  last_name: Rowell
- first_name: Andrew
  full_name: Young, Andrew
  last_name: Young
citation:
  ama: Pickup M, Field D, Rowell D, Young A. Source population characteristics affect
    heterosis following genetic rescue of fragmented plant populations. <i>Proceedings
    of the Royal Society of London Series B Biological Sciences</i>. 2013;280(1750).
    doi:<a href="https://doi.org/10.1098/rspb.2012.2058">10.1098/rspb.2012.2058</a>
  apa: Pickup, M., Field, D., Rowell, D., &#38; Young, A. (2013). Source population
    characteristics affect heterosis following genetic rescue of fragmented plant
    populations. <i>Proceedings of the Royal Society of London Series B Biological
    Sciences</i>. Royal Society, The. <a href="https://doi.org/10.1098/rspb.2012.2058">https://doi.org/10.1098/rspb.2012.2058</a>
  chicago: Pickup, Melinda, David Field, David Rowell, and Andrew Young. “Source Population
    Characteristics Affect Heterosis Following Genetic Rescue of Fragmented Plant
    Populations.” <i>Proceedings of the Royal Society of London Series B Biological
    Sciences</i>. Royal Society, The, 2013. <a href="https://doi.org/10.1098/rspb.2012.2058">https://doi.org/10.1098/rspb.2012.2058</a>.
  ieee: M. Pickup, D. Field, D. Rowell, and A. Young, “Source population characteristics
    affect heterosis following genetic rescue of fragmented plant populations,” <i>Proceedings
    of the Royal Society of London Series B Biological Sciences</i>, vol. 280, no.
    1750. Royal Society, The, 2013.
  ista: Pickup M, Field D, Rowell D, Young A. 2013. Source population characteristics
    affect heterosis following genetic rescue of fragmented plant populations. Proceedings
    of the Royal Society of London Series B Biological Sciences. 280(1750), 2058.
  mla: Pickup, Melinda, et al. “Source Population Characteristics Affect Heterosis
    Following Genetic Rescue of Fragmented Plant Populations.” <i>Proceedings of the
    Royal Society of London Series B Biological Sciences</i>, vol. 280, no. 1750,
    2058, Royal Society, The, 2013, doi:<a href="https://doi.org/10.1098/rspb.2012.2058">10.1098/rspb.2012.2058</a>.
  short: M. Pickup, D. Field, D. Rowell, A. Young, Proceedings of the Royal Society
    of London Series B Biological Sciences 280 (2013).
date_created: 2018-12-11T11:46:32Z
date_published: 2013-01-07T00:00:00Z
date_updated: 2021-01-12T07:57:25Z
day: '07'
department:
- _id: NiBa
doi: 10.1098/rspb.2012.2058
external_id:
  pmid:
  - '23173202'
intvolume: '       280'
issue: '1750'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC3574427/
month: '01'
oa: 1
oa_version: Submitted Version
pmid: 1
publication: Proceedings of the Royal Society of London Series B Biological Sciences
publication_status: published
publisher: Royal Society, The
publist_id: '7372'
quality_controlled: '1'
status: public
title: Source population characteristics affect heterosis following genetic rescue
  of fragmented plant populations
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 280
year: '2013'
...
---
_id: '2715'
abstract:
- lang: eng
  text: 'We consider Markov decision processes (MDPs) with specifications given as
    Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure
    winning vertices from where the objective can be ensured with probability 1. We
    study for the first time the average case complexity of the classical algorithm
    for computing the set of almost-sure winning vertices for MDPs with Büchi objectives.
    Our contributions are as follows: First, we show that for MDPs with constant out-degree
    the expected number of iterations is at most logarithmic and the average case
    running time is linear (as compared to the worst case linear number of iterations
    and quadratic time complexity). Second, for the average case analysis over all
    MDPs we show that the expected number of iterations is constant and the average
    case running time is linear (again as compared to the worst case linear number
    of iterations and quadratic time complexity). Finally we also show that given
    that all MDPs are equally likely, the probability that the classical algorithm
    requires more than constant number of iterations is exponentially small.'
alternative_title:
- LIPIcs
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Manas
  full_name: Joglekar, Manas
  last_name: Joglekar
- first_name: Nisarg
  full_name: Shah, Nisarg
  last_name: Shah
citation:
  ama: 'Chatterjee K, Joglekar M, Shah N. Average case analysis of the classical algorithm
    for Markov decision processes with Büchi objectives. In: Vol 18. Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik; 2012:461-473. doi:<a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461">10.4230/LIPIcs.FSTTCS.2012.461</a>'
  apa: 'Chatterjee, K., Joglekar, M., &#38; Shah, N. (2012). Average case analysis
    of the classical algorithm for Markov decision processes with Büchi objectives
    (Vol. 18, pp. 461–473). Presented at the FSTTCS: Foundations of Software Technology
    and Theoretical Computer Science, Hyderabad, India: Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik. <a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461">https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461</a>'
  chicago: Chatterjee, Krishnendu, Manas Joglekar, and Nisarg Shah. “Average Case
    Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives,”
    18:461–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. <a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461">https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461</a>.
  ieee: 'K. Chatterjee, M. Joglekar, and N. Shah, “Average case analysis of the classical
    algorithm for Markov decision processes with Büchi objectives,” presented at the
    FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Hyderabad,
    India, 2012, vol. 18, pp. 461–473.'
  ista: 'Chatterjee K, Joglekar M, Shah N. 2012. Average case analysis of the classical
    algorithm for Markov decision processes with Büchi objectives. FSTTCS: Foundations
    of Software Technology and Theoretical Computer Science, LIPIcs, vol. 18, 461–473.'
  mla: Chatterjee, Krishnendu, et al. <i>Average Case Analysis of the Classical Algorithm
    for Markov Decision Processes with Büchi Objectives</i>. Vol. 18, Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik, 2012, pp. 461–73, doi:<a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461">10.4230/LIPIcs.FSTTCS.2012.461</a>.
  short: K. Chatterjee, M. Joglekar, N. Shah, in:, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2012, pp. 461–473.
conference:
  end_date: 2012-12-17
  location: Hyderabad, India
  name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
  start_date: 2012-12-15
date_created: 2018-12-11T11:59:13Z
date_published: 2012-12-10T00:00:00Z
date_updated: 2023-02-23T10:06:04Z
day: '10'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.FSTTCS.2012.461
ec_funded: 1
file:
- access_level: open_access
  checksum: d4d644ed1a885dbfc4fa1ef4c5724dab
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:53Z
  date_updated: 2020-07-14T12:45:45Z
  file_id: '5040'
  file_name: IST-2016-525-v1+1_42_1_.pdf
  file_size: 519040
  relation: main_file
file_date_updated: 2020-07-14T12:45:45Z
has_accepted_license: '1'
intvolume: '        18'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: 461 - 473
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: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4180'
pubrep_id: '525'
quality_controlled: '1'
related_material:
  record:
  - id: '1598'
    relation: later_version
    status: public
scopus_import: 1
status: public
title: Average case analysis of the classical algorithm for Markov decision processes
  with Büchi objectives
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: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2012'
...
---
_id: '2825'
abstract:
- lang: eng
  text: 'We study the problem of maximum marginal prediction (MMP) in probabilistic
    graphical models, a task that occurs, for example, as the Bayes optimal decision
    rule under a Hamming loss. MMP is typically performed as a two-stage procedure:
    one estimates each variable''s marginal probability and then forms a prediction
    from the states of maximal probability. In this work we propose a simple yet effective
    technique for accelerating MMP when inference is sampling-based: instead of the
    above two-stage procedure we directly estimate the posterior probability of each
    decision variable. This allows us to identify the point of time when we are sufficiently
    certain about any individual decision. Whenever this is the case, we dynamically
    prune the variables we are confident about from the underlying factor graph. Consequently,
    at any time only samples of variables whose decision is still uncertain need to
    be created. Experiments in two prototypical scenarios, multi-label classification
    and image inpainting, show that adaptive sampling can drastically accelerate MMP
    without sacrificing prediction accuracy.'
author:
- first_name: Christoph
  full_name: Lampert, Christoph
  id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
  last_name: Lampert
  orcid: 0000-0001-8622-7887
citation:
  ama: 'Lampert C. Dynamic pruning of factor graphs for maximum marginal prediction.
    In: Vol 1. Neural Information Processing Systems; 2012:82-90.'
  apa: 'Lampert, C. (2012). Dynamic pruning of factor graphs for maximum marginal
    prediction (Vol. 1, pp. 82–90). Presented at the NIPS: Neural Information Processing
    Systems, Lake Tahoe, NV, United States: Neural Information Processing Systems.'
  chicago: Lampert, Christoph. “Dynamic Pruning of Factor Graphs for Maximum Marginal
    Prediction,” 1:82–90. Neural Information Processing Systems, 2012.
  ieee: 'C. Lampert, “Dynamic pruning of factor graphs for maximum marginal prediction,”
    presented at the NIPS: Neural Information Processing Systems, Lake Tahoe, NV,
    United States, 2012, vol. 1, pp. 82–90.'
  ista: 'Lampert C. 2012. Dynamic pruning of factor graphs for maximum marginal prediction.
    NIPS: Neural Information Processing Systems vol. 1, 82–90.'
  mla: Lampert, Christoph. <i>Dynamic Pruning of Factor Graphs for Maximum Marginal
    Prediction</i>. Vol. 1, Neural Information Processing Systems, 2012, pp. 82–90.
  short: C. Lampert, in:, Neural Information Processing Systems, 2012, pp. 82–90.
conference:
  end_date: 2012-12-06
  location: Lake Tahoe, NV, United States
  name: 'NIPS: Neural Information Processing Systems'
  start_date: 2012-12-03
date_created: 2018-12-11T11:59:48Z
date_published: 2012-12-01T00:00:00Z
date_updated: 2021-01-12T06:59:59Z
day: '01'
department:
- _id: ChLa
intvolume: '         1'
language:
- iso: eng
month: '12'
oa_version: None
page: 82 - 90
publication_status: published
publisher: Neural Information Processing Systems
publist_id: '3975'
quality_controlled: '1'
scopus_import: 1
status: public
title: Dynamic pruning of factor graphs for maximum marginal prediction
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 1
year: '2012'
...
---
_id: '2848'
abstract:
- lang: eng
  text: We study evolutionary game theory in a setting where individuals learn from
    each other. We extend the traditional approach by assuming that a population contains
    individuals with different learning abilities. In particular, we explore the situation
    where individuals have different search spaces, when attempting to learn the strategies
    of others. The search space of an individual specifies the set of strategies learnable
    by that individual. The search space is genetically given and does not change
    under social evolutionary dynamics. We introduce a general framework and study
    a specific example in the context of direct reciprocity. For this example, we
    obtain the counter intuitive result that cooperation can only evolve for intermediate
    benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection.
    Our paper is a step toward making a connection between computational learning
    theory and evolutionary game dynamics.
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Damien
  full_name: Zufferey, Damien
  id: 4397AC76-F248-11E8-B48F-1D18A9856A87
  last_name: Zufferey
  orcid: 0000-0002-3197-8736
- first_name: Martin
  full_name: Nowak, Martin
  last_name: Nowak
citation:
  ama: Chatterjee K, Zufferey D, Nowak M. Evolutionary game dynamics in populations
    with different learners. <i>Journal of Theoretical Biology</i>. 2012;301:161-173.
    doi:<a href="https://doi.org/10.1016/j.jtbi.2012.02.021">10.1016/j.jtbi.2012.02.021</a>
  apa: Chatterjee, K., Zufferey, D., &#38; Nowak, M. (2012). Evolutionary game dynamics
    in populations with different learners. <i>Journal of Theoretical Biology</i>.
    Elsevier. <a href="https://doi.org/10.1016/j.jtbi.2012.02.021">https://doi.org/10.1016/j.jtbi.2012.02.021</a>
  chicago: Chatterjee, Krishnendu, Damien Zufferey, and Martin Nowak. “Evolutionary
    Game Dynamics in Populations with Different Learners.” <i>Journal of Theoretical
    Biology</i>. Elsevier, 2012. <a href="https://doi.org/10.1016/j.jtbi.2012.02.021">https://doi.org/10.1016/j.jtbi.2012.02.021</a>.
  ieee: K. Chatterjee, D. Zufferey, and M. Nowak, “Evolutionary game dynamics in populations
    with different learners,” <i>Journal of Theoretical Biology</i>, vol. 301. Elsevier,
    pp. 161–173, 2012.
  ista: Chatterjee K, Zufferey D, Nowak M. 2012. Evolutionary game dynamics in populations
    with different learners. Journal of Theoretical Biology. 301, 161–173.
  mla: Chatterjee, Krishnendu, et al. “Evolutionary Game Dynamics in Populations with
    Different Learners.” <i>Journal of Theoretical Biology</i>, vol. 301, Elsevier,
    2012, pp. 161–73, doi:<a href="https://doi.org/10.1016/j.jtbi.2012.02.021">10.1016/j.jtbi.2012.02.021</a>.
  short: K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301
    (2012) 161–173.
date_created: 2018-12-11T11:59:55Z
date_published: 2012-05-21T00:00:00Z
date_updated: 2021-01-12T07:00:12Z
day: '21'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.jtbi.2012.02.021
ec_funded: 1
external_id:
  pmid:
  - '22394652'
intvolume: '       301'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3322297/
month: '05'
oa: 1
oa_version: Submitted Version
page: 161 - 173
pmid: 1
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 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: Journal of Theoretical Biology
publication_status: published
publisher: Elsevier
publist_id: '3946'
quality_controlled: '1'
scopus_import: 1
status: public
title: Evolutionary game dynamics in populations with different learners
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 301
year: '2012'
...
---
_id: '2849'
author:
- first_name: Herbert
  full_name: Edelsbrunner, Herbert
  id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
  last_name: Edelsbrunner
  orcid: 0000-0002-9823-6833
- first_name: Nataliya
  full_name: Strelkova, Nataliya
  last_name: Strelkova
citation:
  ama: Edelsbrunner H, Strelkova N. On the configuration space of Steiner minimal
    trees. <i>Russian Mathematical Surveys</i>. 2012;67(6):1167-1168. doi:<a href="https://doi.org/10.1070/RM2012v067n06ABEH004820">10.1070/RM2012v067n06ABEH004820</a>
  apa: Edelsbrunner, H., &#38; Strelkova, N. (2012). On the configuration space of
    Steiner minimal trees. <i>Russian Mathematical Surveys</i>. IOP Publishing Ltd.
    <a href="https://doi.org/10.1070/RM2012v067n06ABEH004820">https://doi.org/10.1070/RM2012v067n06ABEH004820</a>
  chicago: Edelsbrunner, Herbert, and Nataliya Strelkova. “On the Configuration Space
    of Steiner Minimal Trees.” <i>Russian Mathematical Surveys</i>. IOP Publishing
    Ltd., 2012. <a href="https://doi.org/10.1070/RM2012v067n06ABEH004820">https://doi.org/10.1070/RM2012v067n06ABEH004820</a>.
  ieee: H. Edelsbrunner and N. Strelkova, “On the configuration space of Steiner minimal
    trees,” <i>Russian Mathematical Surveys</i>, vol. 67, no. 6. IOP Publishing Ltd.,
    pp. 1167–1168, 2012.
  ista: Edelsbrunner H, Strelkova N. 2012. On the configuration space of Steiner minimal
    trees. Russian Mathematical Surveys. 67(6), 1167–1168.
  mla: Edelsbrunner, Herbert, and Nataliya Strelkova. “On the Configuration Space
    of Steiner Minimal Trees.” <i>Russian Mathematical Surveys</i>, vol. 67, no. 6,
    IOP Publishing Ltd., 2012, pp. 1167–68, doi:<a href="https://doi.org/10.1070/RM2012v067n06ABEH004820">10.1070/RM2012v067n06ABEH004820</a>.
  short: H. Edelsbrunner, N. Strelkova, Russian Mathematical Surveys 67 (2012) 1167–1168.
date_created: 2018-12-11T11:59:55Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2021-01-12T07:00:13Z
day: '01'
ddc:
- '000'
department:
- _id: HeEd
doi: 10.1070/RM2012v067n06ABEH004820
file:
- access_level: open_access
  checksum: 44ee8d173487e8ed41a51136816bbeb4
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:14:26Z
  date_updated: 2020-07-14T12:45:51Z
  file_id: '5078'
  file_name: IST-2016-546-v1+1_2014-J-05-SteinerMinTrees.pdf
  file_size: 392021
  relation: main_file
file_date_updated: 2020-07-14T12:45:51Z
has_accepted_license: '1'
intvolume: '        67'
issue: '6'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 1167 - 1168
publication: Russian Mathematical Surveys
publication_status: published
publisher: IOP Publishing Ltd.
publist_id: '3943'
pubrep_id: '546'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the configuration space of Steiner minimal trees
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 67
year: '2012'
...
---
_id: '2888'
abstract:
- lang: eng
  text: Formal verification aims to improve the quality of hardware and software by
    detecting errors before they do harm. At the basis of formal verification lies
    the logical notion of correctness, which purports to capture whether or not a
    circuit or program behaves as desired. We suggest that the boolean partition into
    correct and incorrect systems falls short of the practical need to assess the
    behavior of hardware and software in a more nuanced fashion against multiple criteria.
alternative_title:
- LNCS
author:
- 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: 'Henzinger TA. Quantitative reactive models. In: <i>Conference Proceedings
    MODELS 2012</i>. Vol 7590. Springer; 2012:1-2. doi:<a href="https://doi.org/10.1007/978-3-642-33666-9_1">10.1007/978-3-642-33666-9_1</a>'
  apa: 'Henzinger, T. A. (2012). Quantitative reactive models. In <i>Conference proceedings
    MODELS 2012</i> (Vol. 7590, pp. 1–2). Innsbruck, Austria: Springer. <a href="https://doi.org/10.1007/978-3-642-33666-9_1">https://doi.org/10.1007/978-3-642-33666-9_1</a>'
  chicago: Henzinger, Thomas A. “Quantitative Reactive Models.” In <i>Conference Proceedings
    MODELS 2012</i>, 7590:1–2. Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-33666-9_1">https://doi.org/10.1007/978-3-642-33666-9_1</a>.
  ieee: T. A. Henzinger, “Quantitative reactive models,” in <i>Conference proceedings
    MODELS 2012</i>, Innsbruck, Austria, 2012, vol. 7590, pp. 1–2.
  ista: 'Henzinger TA. 2012. Quantitative reactive models. Conference proceedings
    MODELS 2012. MODELS: Model-driven Engineering Languages and Systems, LNCS, vol.
    7590, 1–2.'
  mla: Henzinger, Thomas A. “Quantitative Reactive Models.” <i>Conference Proceedings
    MODELS 2012</i>, vol. 7590, Springer, 2012, pp. 1–2, doi:<a href="https://doi.org/10.1007/978-3-642-33666-9_1">10.1007/978-3-642-33666-9_1</a>.
  short: T.A. Henzinger, in:, Conference Proceedings MODELS 2012, Springer, 2012,
    pp. 1–2.
conference:
  end_date: 2012-10-05
  location: Innsbruck, Austria
  name: 'MODELS: Model-driven Engineering Languages and Systems'
  start_date: 2012-09-30
date_created: 2018-12-11T12:00:09Z
date_published: 2012-09-01T00:00:00Z
date_updated: 2021-01-12T07:00:29Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33666-9_1
ec_funded: 1
intvolume: '      7590'
language:
- iso: eng
month: '09'
oa_version: None
page: 1 - 2
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication: Conference proceedings MODELS 2012
publication_status: published
publisher: Springer
publist_id: '3870'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative reactive models
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7590
year: '2012'
...
---
_id: '2890'
abstract:
- lang: eng
  text: 'Systems are often specified using multiple requirements on their behavior.
    In practice, these requirements can be contradictory. The classical approach to
    specification, verification, and synthesis demands more detailed specifications
    that resolve any contradictions in the requirements. These detailed specifications
    are usually large, cumbersome, and hard to maintain or modify. In contrast, quantitative
    frameworks allow the formalization of the intuitive idea that what is desired
    is an implementation that comes &quot;closest&quot; to satisfying the mutually
    incompatible requirements, according to a measure of fit that can be defined by
    the requirements engineer. One flexible framework for quantifying how &quot;well&quot;
    an implementation satisfies a specification is offered by simulation distances
    that are parameterized by an error model. We introduce this framework, study its
    properties, and provide an algorithmic solution for the following quantitative
    synthesis question: given two (or more) behavioral requirements specified by possibly
    incompatible finite-state machines, and an error model, find the finite-state
    implementation that minimizes the maximal simulation distance to the given requirements.
    Furthermore, we generalize the framework to handle infinite alphabets (for example,
    realvalued domains). We also demonstrate how quantitative specifications based
    on simulation distances might lead to smaller and easier to modify specifications.
    Finally, we illustrate our approach using case studies on error correcting codes
    and scheduler synthesis.'
author:
- first_name: Pavol
  full_name: Cerny, Pavol
  id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
  last_name: Cerny
- first_name: Sivakanth
  full_name: Gopi, Sivakanth
  last_name: Gopi
- 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: Arjun
  full_name: Radhakrishna, Arjun
  id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
  last_name: Radhakrishna
- first_name: Nishant
  full_name: Totla, Nishant
  last_name: Totla
citation:
  ama: 'Cerny P, Gopi S, Henzinger TA, Radhakrishna A, Totla N. Synthesis from incompatible
    specifications. In: <i>Proceedings of the Tenth ACM International Conference on
    Embedded Software</i>. ACM; 2012:53-62. doi:<a href="https://doi.org/10.1145/2380356.2380371">10.1145/2380356.2380371</a>'
  apa: 'Cerny, P., Gopi, S., Henzinger, T. A., Radhakrishna, A., &#38; Totla, N. (2012).
    Synthesis from incompatible specifications. In <i>Proceedings of the tenth ACM
    international conference on Embedded software</i> (pp. 53–62). Tampere, Finland:
    ACM. <a href="https://doi.org/10.1145/2380356.2380371">https://doi.org/10.1145/2380356.2380371</a>'
  chicago: Cerny, Pavol, Sivakanth Gopi, Thomas A Henzinger, Arjun Radhakrishna, and
    Nishant Totla. “Synthesis from Incompatible Specifications.” In <i>Proceedings
    of the Tenth ACM International Conference on Embedded Software</i>, 53–62. ACM,
    2012. <a href="https://doi.org/10.1145/2380356.2380371">https://doi.org/10.1145/2380356.2380371</a>.
  ieee: P. Cerny, S. Gopi, T. A. Henzinger, A. Radhakrishna, and N. Totla, “Synthesis
    from incompatible specifications,” in <i>Proceedings of the tenth ACM international
    conference on Embedded software</i>, Tampere, Finland, 2012, pp. 53–62.
  ista: 'Cerny P, Gopi S, Henzinger TA, Radhakrishna A, Totla N. 2012. Synthesis from
    incompatible specifications. Proceedings of the tenth ACM international conference
    on Embedded software. EMSOFT: Embedded Software , 53–62.'
  mla: Cerny, Pavol, et al. “Synthesis from Incompatible Specifications.” <i>Proceedings
    of the Tenth ACM International Conference on Embedded Software</i>, ACM, 2012,
    pp. 53–62, doi:<a href="https://doi.org/10.1145/2380356.2380371">10.1145/2380356.2380371</a>.
  short: P. Cerny, S. Gopi, T.A. Henzinger, A. Radhakrishna, N. Totla, in:, Proceedings
    of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp.
    53–62.
conference:
  end_date: 2012-10-12
  location: Tampere, Finland
  name: 'EMSOFT: Embedded Software '
  start_date: 2012-10-07
date_created: 2018-12-11T12:00:10Z
date_published: 2012-10-01T00:00:00Z
date_updated: 2021-01-12T07:00:30Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2380356.2380371
ec_funded: 1
language:
- iso: eng
month: '10'
oa_version: None
page: 53 - 62
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication: Proceedings of the tenth ACM international conference on Embedded software
publication_status: published
publisher: ACM
publist_id: '3868'
quality_controlled: '1'
scopus_import: 1
status: public
title: Synthesis from incompatible specifications
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
