---
_id: '2052'
abstract:
- lang: eng
  text: A standard technique for solving the parameterized model checking problem
    is to reduce it to the classic model checking problem of finitely many finite-state
    systems. This work considers some of the theoretical power and limitations of
    this technique. We focus on concurrent systems in which processes communicate
    via pairwise rendezvous, as well as the special cases of disjunctive guards and
    token passing; specifications are expressed in indexed temporal logic without
    the next operator; and the underlying network topologies are generated by suitable
    Monadic Second Order Logic formulas and graph operations. First, we settle the
    exact computational complexity of the parameterized model checking problem for
    some of our concurrent systems, and establish new decidability results for others.
    Second, we consider the cases that model checking the parameterized system can
    be reduced to model checking some fixed number of processes, the number is known
    as a cutoff. We provide many cases for when such cutoffs can be computed, establish
    lower bounds on the size of such cutoffs, and identify cases where no cutoff exists.
    Third, we consider cases for which the parameterized system is equivalent to a
    single finite-state system (more precisely a Büchi word automaton), and establish
    tight bounds on the sizes of such automata.
acknowledgement: The second, third, fourth and fifth authors were supported by the
  Austrian National Research Network S11403-N23 (RiSE) of the Austrian Science Fund
  (FWF) and by the Vienna Science and Technology Fund (WWTF) through grants PROSEED,
  ICT12-059, and VRG11-005.
alternative_title:
- LNCS
author:
- first_name: Benjamin
  full_name: Aminof, Benjamin
  id: 4A55BD00-F248-11E8-B48F-1D18A9856A87
  last_name: Aminof
- first_name: Tomer
  full_name: Kotek, Tomer
  last_name: Kotek
- first_name: Sacha
  full_name: Rubin, Sacha
  last_name: Rubin
- first_name: Francesco
  full_name: Spegni, Francesco
  last_name: Spegni
- first_name: Helmut
  full_name: Veith, Helmut
  last_name: Veith
citation:
  ama: 'Aminof B, Kotek T, Rubin S, Spegni F, Veith H. Parameterized model checking
    of rendezvous systems. In: Baldan P, Gorla D, eds. <i>Lecture Notes in Computer
    Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
    Notes in Bioinformatics)</i>. Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik; 2014:109-124. doi:<a href="https://doi.org/10.1007/978-3-662-44584-6_9">10.1007/978-3-662-44584-6_9</a>'
  apa: 'Aminof, B., Kotek, T., Rubin, S., Spegni, F., &#38; Veith, H. (2014). Parameterized
    model checking of rendezvous systems. In P. Baldan &#38; D. Gorla (Eds.), <i>Lecture
    Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence
    and Lecture Notes in Bioinformatics)</i> (Vol. 8704, pp. 109–124). Rome, Italy:
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.1007/978-3-662-44584-6_9">https://doi.org/10.1007/978-3-662-44584-6_9</a>'
  chicago: Aminof, Benjamin, Tomer Kotek, Sacha Rubin, Francesco Spegni, and Helmut
    Veith. “Parameterized Model Checking of Rendezvous Systems.” In <i>Lecture Notes
    in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
    and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan and Daniele Gorla,
    8704:109–24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. <a href="https://doi.org/10.1007/978-3-662-44584-6_9">https://doi.org/10.1007/978-3-662-44584-6_9</a>.
  ieee: B. Aminof, T. Kotek, S. Rubin, F. Spegni, and H. Veith, “Parameterized model
    checking of rendezvous systems,” in <i>Lecture Notes in Computer Science (including
    subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>,
    Rome, Italy, 2014, vol. 8704, pp. 109–124.
  ista: 'Aminof B, Kotek T, Rubin S, Spegni F, Veith H. 2014. Parameterized model
    checking of rendezvous systems. Lecture Notes in Computer Science (including subseries
    Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
    CONCUR: Concurrency Theory, LNCS, vol. 8704, 109–124.'
  mla: Aminof, Benjamin, et al. “Parameterized Model Checking of Rendezvous Systems.”
    <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
    Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan
    and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2014, pp. 109–24, doi:<a href="https://doi.org/10.1007/978-3-662-44584-6_9">10.1007/978-3-662-44584-6_9</a>.
  short: B. Aminof, T. Kotek, S. Rubin, F. Spegni, H. Veith, in:, P. Baldan, D. Gorla
    (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in
    Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik, 2014, pp. 109–124.
conference:
  end_date: 2014-09-05
  location: Rome, Italy
  name: 'CONCUR: Concurrency Theory'
  start_date: 2014-09-02
date_created: 2018-12-11T11:55:26Z
date_published: 2014-09-01T00:00:00Z
date_updated: 2021-01-12T06:54:59Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-44584-6_9
editor:
- first_name: Paolo
  full_name: Baldan, Paolo
  last_name: Baldan
- first_name: Daniele
  full_name: Gorla, Daniele
  last_name: Gorla
intvolume: '      8704'
language:
- iso: eng
month: '09'
oa_version: None
page: 109 - 124
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
  in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4994'
quality_controlled: '1'
status: public
title: Parameterized model checking of rendezvous systems
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 8704
year: '2014'
...
---
_id: '2053'
abstract:
- lang: eng
  text: In contrast to the usual understanding of probabilistic systems as stochastic
    processes, recently these systems have also been regarded as transformers of probabilities.
    In this paper, we give a natural definition of strong bisimulation for probabilistic
    systems corresponding to this view that treats probability distributions as first-class
    citizens. Our definition applies in the same way to discrete systems as well as
    to systems with uncountable state and action spaces. Several examples demonstrate
    that our definition refines the understanding of behavioural equivalences of probabilistic
    systems. In particular, it solves a longstanding open problem concerning the representation
    of memoryless continuous time by memoryfull continuous time. Finally, we give
    algorithms for computing this bisimulation not only for finite but also for classes
    of uncountably infinite systems.
acknowledgement: This work is supported by the EU 7th Framework Programme under grant
  agreements 295261 (MEALS) and 318490 (SENSATION), Czech Science Foundation under
  grant agreement P202/12/G061, the DFG Transregional Collaborative Research Centre
  SFB/TR 14 AVACS, and by the CAS/SAFEA International Partnership Program for Creative
  Research Teams.
alternative_title:
- LNCS
author:
- first_name: Holger
  full_name: Hermanns, Holger
  last_name: Hermanns
- first_name: Jan
  full_name: Krčál, Jan
  last_name: Krčál
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
citation:
  ama: 'Hermanns H, Krčál J, Kretinsky J. Probabilistic bisimulation: Naturally on
    distributions. In: Baldan P, Gorla D, eds. <i>Lecture Notes in Computer Science
    (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes
    in Bioinformatics)</i>. Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
    2014:249-265. doi:<a href="https://doi.org/10.1007/978-3-662-44584-6_18">10.1007/978-3-662-44584-6_18</a>'
  apa: 'Hermanns, H., Krčál, J., &#38; Kretinsky, J. (2014). Probabilistic bisimulation:
    Naturally on distributions. In P. Baldan &#38; D. Gorla (Eds.), <i>Lecture Notes
    in Computer Science (including subseries Lecture Notes in Artificial Intelligence
    and Lecture Notes in Bioinformatics)</i> (Vol. 8704, pp. 249–265). Rome, Italy:
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.1007/978-3-662-44584-6_18">https://doi.org/10.1007/978-3-662-44584-6_18</a>'
  chicago: 'Hermanns, Holger, Jan Krčál, and Jan Kretinsky. “Probabilistic Bisimulation:
    Naturally on Distributions.” In <i>Lecture Notes in Computer Science (Including
    Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>,
    edited by Paolo Baldan and Daniele Gorla, 8704:249–65. Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2014. <a href="https://doi.org/10.1007/978-3-662-44584-6_18">https://doi.org/10.1007/978-3-662-44584-6_18</a>.'
  ieee: 'H. Hermanns, J. Krčál, and J. Kretinsky, “Probabilistic bisimulation: Naturally
    on distributions,” in <i>Lecture Notes in Computer Science (including subseries
    Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>,
    Rome, Italy, 2014, vol. 8704, pp. 249–265.'
  ista: 'Hermanns H, Krčál J, Kretinsky J. 2014. Probabilistic bisimulation: Naturally
    on distributions. Lecture Notes in Computer Science (including subseries Lecture
    Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR:
    Concurrency Theory, LNCS, vol. 8704, 249–265.'
  mla: 'Hermanns, Holger, et al. “Probabilistic Bisimulation: Naturally on Distributions.”
    <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
    Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan
    and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2014, pp. 249–65, doi:<a href="https://doi.org/10.1007/978-3-662-44584-6_18">10.1007/978-3-662-44584-6_18</a>.'
  short: H. Hermanns, J. Krčál, J. Kretinsky, in:, P. Baldan, D. Gorla (Eds.), Lecture
    Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
    and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2014, pp. 249–265.
conference:
  end_date: 2014-09-05
  location: Rome, Italy
  name: 'CONCUR: Concurrency Theory'
  start_date: 2014-09-02
date_created: 2018-12-11T11:55:27Z
date_published: 2014-09-01T00:00:00Z
date_updated: 2021-01-12T06:55:00Z
day: '01'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-662-44584-6_18
ec_funded: 1
editor:
- first_name: Paolo
  full_name: Baldan, Paolo
  last_name: Baldan
- first_name: Daniele
  full_name: Gorla, Daniele
  last_name: Gorla
intvolume: '      8704'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1404.5084
month: '09'
oa: 1
oa_version: Submitted Version
page: 249 - 265
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
  in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4993'
status: public
title: 'Probabilistic bisimulation: Naturally on distributions'
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 8704
year: '2014'
...
---
_id: '2054'
abstract:
- lang: eng
  text: 'We study two-player concurrent games on finite-state graphs played for an
    infinite number of rounds, where in each round, the two players (player 1 and
    player 2) choose their moves independently and simultaneously; the current state
    and the two moves determine the successor state. The objectives are ω-regular
    winning conditions specified as parity objectives. We consider the qualitative
    analysis problems: the computation of the almost-sure and limit-sure winning set
    of states, where player 1 can ensure to win with probability 1 and with probability
    arbitrarily close to 1, respectively. In general the almost-sure and limit-sure
    winning strategies require both infinite-memory as well as infinite-precision
    (to describe probabilities). While the qualitative analysis problem for concurrent
    parity games with infinite-memory, infinite-precision randomized strategies was
    studied before, we study the bounded-rationality problem for qualitative analysis
    of concurrent parity games, where the strategy set for player 1 is restricted
    to bounded-resource strategies. In terms of precision, strategies can be deterministic,
    uniform, finite-precision, or infinite-precision; and in terms of memory, strategies
    can be memoryless, finite-memory, or infinite-memory. We present a precise and
    complete characterization of the qualitative winning sets for all combinations
    of classes of strategies. In particular, we show that uniform memoryless strategies
    are as powerful as finite-precision infinite-memory strategies, and infinite-precision
    memoryless strategies are as powerful as infinite-precision finite-memory strategies.
    We show that the winning sets can be computed in (n2d+3) time, where n is the
    size of the game structure and 2d is the number of priorities (or colors), and
    our algorithms are symbolic. The membership problem of whether a state belongs
    to a winning set can be decided in NP ∩ coNP. Our symbolic algorithms are based
    on a characterization of the winning sets as μ-calculus formulas, however, our
    μ-calculus formulas are crucially different from the ones for concurrent parity
    games (without bounded rationality); and our memoryless witness strategy constructions
    are significantly different from the infinite-memory witness strategy constructions
    for concurrent parity games.'
alternative_title:
- LNCS
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
citation:
  ama: 'Chatterjee K. Qualitative concurrent parity games: Bounded rationality. In:
    Baldan P, Gorla D, eds. <i>Lecture Notes in Computer Science (Including Subseries
    Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>.
    Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:544-559. doi:<a
    href="https://doi.org/10.1007/978-3-662-44584-6_37">10.1007/978-3-662-44584-6_37</a>'
  apa: 'Chatterjee, K. (2014). Qualitative concurrent parity games: Bounded rationality.
    In P. Baldan &#38; D. Gorla (Eds.), <i>Lecture Notes in Computer Science (including
    subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>
    (Vol. 8704, pp. 544–559). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik. <a href="https://doi.org/10.1007/978-3-662-44584-6_37">https://doi.org/10.1007/978-3-662-44584-6_37</a>'
  chicago: 'Chatterjee, Krishnendu. “Qualitative Concurrent Parity Games: Bounded
    Rationality.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture
    Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited
    by Paolo Baldan and Daniele Gorla, 8704:544–59. Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2014. <a href="https://doi.org/10.1007/978-3-662-44584-6_37">https://doi.org/10.1007/978-3-662-44584-6_37</a>.'
  ieee: 'K. Chatterjee, “Qualitative concurrent parity games: Bounded rationality,”
    in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in
    Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Rome, Italy,
    2014, vol. 8704, pp. 544–559.'
  ista: 'Chatterjee K. 2014. Qualitative concurrent parity games: Bounded rationality.
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial
    Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory,
    LNCS, vol. 8704, 544–559.'
  mla: 'Chatterjee, Krishnendu. “Qualitative Concurrent Parity Games: Bounded Rationality.”
    <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
    Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan
    and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2014, pp. 544–59, doi:<a href="https://doi.org/10.1007/978-3-662-44584-6_37">10.1007/978-3-662-44584-6_37</a>.'
  short: K. Chatterjee, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer
    Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
    Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014,
    pp. 544–559.
conference:
  end_date: 2014-09-05
  location: Rome, Italy
  name: 'CONCUR: Concurrency Theory'
  start_date: 2014-09-02
date_created: 2018-12-11T11:55:27Z
date_published: 2014-09-01T00:00:00Z
date_updated: 2023-02-23T11:23:36Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-44584-6_37
ec_funded: 1
editor:
- first_name: Paolo
  full_name: Baldan, Paolo
  last_name: Baldan
- first_name: Daniele
  full_name: Gorla, Daniele
  last_name: Gorla
intvolume: '      8704'
language:
- iso: eng
month: '09'
oa_version: None
page: 544 - 559
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
  in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4992'
quality_controlled: '1'
related_material:
  record:
  - id: '3354'
    relation: earlier_version
    status: public
status: public
title: 'Qualitative concurrent parity games: Bounded rationality'
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 8704
year: '2014'
...
---
_id: '2056'
abstract:
- lang: eng
  text: 'We consider a continuous-time Markov chain (CTMC) whose state space is partitioned
    into aggregates, and each aggregate is assigned a probability measure. A sufficient
    condition for defining a CTMC over the aggregates is presented as a variant of
    weak lumpability, which also characterizes that the measure over the original
    process can be recovered from that of the aggregated one. We show how the applicability
    of de-aggregation depends on the initial distribution. The application section
    is devoted to illustrate how the developed theory aids in reducing CTMC models
    of biochemical systems particularly in connection to protein-protein interactions.
    We assume that the model is written by a biologist in form of site-graph-rewrite
    rules. Site-graph-rewrite rules compactly express that, often, only a local context
    of a protein (instead of a full molecular species) needs to be in a certain configuration
    in order to trigger a reaction event. This observation leads to suitable aggregate
    Markov chains with smaller state spaces, thereby providing sufficient reduction
    in computational complexity. This is further exemplified in two case studies:
    simple unbounded polymerization and early EGFR/insulin crosstalk.'
acknowledgement: T. Petrov is supported by SystemsX.ch—the Swiss Inititative for Systems
  Biology.
author:
- first_name: Arnab
  full_name: Ganguly, Arnab
  last_name: Ganguly
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
- first_name: Heinz
  full_name: Koeppl, Heinz
  last_name: Koeppl
citation:
  ama: Ganguly A, Petrov T, Koeppl H. Markov chain aggregation and its applications
    to combinatorial reaction networks. <i>Journal of Mathematical Biology</i>. 2014;69(3):767-797.
    doi:<a href="https://doi.org/10.1007/s00285-013-0738-7">10.1007/s00285-013-0738-7</a>
  apa: Ganguly, A., Petrov, T., &#38; Koeppl, H. (2014). Markov chain aggregation
    and its applications to combinatorial reaction networks. <i>Journal of Mathematical
    Biology</i>. Springer. <a href="https://doi.org/10.1007/s00285-013-0738-7">https://doi.org/10.1007/s00285-013-0738-7</a>
  chicago: Ganguly, Arnab, Tatjana Petrov, and Heinz Koeppl. “Markov Chain Aggregation
    and Its Applications to Combinatorial Reaction Networks.” <i>Journal of Mathematical
    Biology</i>. Springer, 2014. <a href="https://doi.org/10.1007/s00285-013-0738-7">https://doi.org/10.1007/s00285-013-0738-7</a>.
  ieee: A. Ganguly, T. Petrov, and H. Koeppl, “Markov chain aggregation and its applications
    to combinatorial reaction networks,” <i>Journal of Mathematical Biology</i>, vol.
    69, no. 3. Springer, pp. 767–797, 2014.
  ista: Ganguly A, Petrov T, Koeppl H. 2014. Markov chain aggregation and its applications
    to combinatorial reaction networks. Journal of Mathematical Biology. 69(3), 767–797.
  mla: Ganguly, Arnab, et al. “Markov Chain Aggregation and Its Applications to Combinatorial
    Reaction Networks.” <i>Journal of Mathematical Biology</i>, vol. 69, no. 3, Springer,
    2014, pp. 767–97, doi:<a href="https://doi.org/10.1007/s00285-013-0738-7">10.1007/s00285-013-0738-7</a>.
  short: A. Ganguly, T. Petrov, H. Koeppl, Journal of Mathematical Biology 69 (2014)
    767–797.
date_created: 2018-12-11T11:55:28Z
date_published: 2014-11-20T00:00:00Z
date_updated: 2021-01-12T06:55:01Z
day: '20'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1007/s00285-013-0738-7
intvolume: '        69'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1303.4532
month: '11'
oa: 1
oa_version: Submitted Version
page: 767 - 797
publication: Journal of Mathematical Biology
publication_status: published
publisher: Springer
publist_id: '4990'
quality_controlled: '1'
scopus_import: 1
status: public
title: Markov chain aggregation and its applications to combinatorial reaction networks
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 69
year: '2014'
...
---
_id: '2057'
abstract:
- lang: eng
  text: 'In the past few years, a lot of attention has been devoted to multimedia
    indexing by fusing multimodal informations. Two kinds of fusion schemes are generally
    considered: The early fusion and the late fusion. We focus on late classifier
    fusion, where one combines the scores of each modality at the decision level.
    To tackle this problem, we investigate a recent and elegant well-founded quadratic
    program named MinCq coming from the machine learning PAC-Bayesian theory. MinCq
    looks for the weighted combination, over a set of real-valued functions seen as
    voters, leading to the lowest misclassification rate, while maximizing the voters’
    diversity. We propose an extension of MinCq tailored to multimedia indexing. Our
    method is based on an order-preserving pairwise loss adapted to ranking that allows
    us to improve Mean Averaged Precision measure while taking into account the diversity
    of the voters that we want to fuse. We provide evidence that this method is naturally
    adapted to late fusion procedures and confirm the good behavior of our approach
    on the challenging PASCAL VOC’07 benchmark.'
alternative_title:
- LNCS
arxiv: 1
author:
- first_name: Emilie
  full_name: Morvant, Emilie
  id: 4BAC2A72-F248-11E8-B48F-1D18A9856A87
  last_name: Morvant
  orcid: 0000-0002-8301-7240
- first_name: Amaury
  full_name: Habrard, Amaury
  last_name: Habrard
- first_name: Stéphane
  full_name: Ayache, Stéphane
  last_name: Ayache
citation:
  ama: 'Morvant E, Habrard A, Ayache S. Majority vote of diverse classifiers for late
    fusion. In: <i>Lecture Notes in Computer Science (Including Subseries Lecture
    Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol
    8621. Springer; 2014:153-162. doi:<a href="https://doi.org/10.1007/978-3-662-44415-3_16">10.1007/978-3-662-44415-3_16</a>'
  apa: 'Morvant, E., Habrard, A., &#38; Ayache, S. (2014). Majority vote of diverse
    classifiers for late fusion. In <i>Lecture Notes in Computer Science (including
    subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>
    (Vol. 8621, pp. 153–162). Joensuu, Finland: Springer. <a href="https://doi.org/10.1007/978-3-662-44415-3_16">https://doi.org/10.1007/978-3-662-44415-3_16</a>'
  chicago: Morvant, Emilie, Amaury Habrard, and Stéphane Ayache. “Majority Vote of
    Diverse Classifiers for Late Fusion.” In <i>Lecture Notes in Computer Science
    (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes
    in Bioinformatics)</i>, 8621:153–62. Springer, 2014. <a href="https://doi.org/10.1007/978-3-662-44415-3_16">https://doi.org/10.1007/978-3-662-44415-3_16</a>.
  ieee: E. Morvant, A. Habrard, and S. Ayache, “Majority vote of diverse classifiers
    for late fusion,” in <i>Lecture Notes in Computer Science (including subseries
    Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>,
    Joensuu, Finland, 2014, vol. 8621, pp. 153–162.
  ista: 'Morvant E, Habrard A, Ayache S. 2014. Majority vote of diverse classifiers
    for late fusion. Lecture Notes in Computer Science (including subseries Lecture
    Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). IAPR: International
    Workshop on Structural, Syntactic, and Statistical Pattern Recognition, LNCS,
    vol. 8621, 153–162.'
  mla: Morvant, Emilie, et al. “Majority Vote of Diverse Classifiers for Late Fusion.”
    <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
    Intelligence and Lecture Notes in Bioinformatics)</i>, vol. 8621, Springer, 2014,
    pp. 153–62, doi:<a href="https://doi.org/10.1007/978-3-662-44415-3_16">10.1007/978-3-662-44415-3_16</a>.
  short: E. Morvant, A. Habrard, S. Ayache, in:, Lecture Notes in Computer Science
    (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes
    in Bioinformatics), Springer, 2014, pp. 153–162.
conference:
  end_date: 2014-08-22
  location: Joensuu, Finland
  name: 'IAPR: International Workshop on Structural, Syntactic, and Statistical Pattern
    Recognition'
  start_date: 2014-08-20
date_created: 2018-12-11T11:55:28Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2021-01-12T06:55:01Z
day: '01'
department:
- _id: ChLa
doi: 10.1007/978-3-662-44415-3_16
ec_funded: 1
external_id:
  arxiv:
  - '1404.7796'
intvolume: '      8621'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1404.7796
month: '01'
oa: 1
oa_version: Preprint
page: 153 - 162
project:
- _id: 2532554C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '308036'
  name: Lifelong Learning of Visual Scene Understanding
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
  in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_status: published
publisher: Springer
publist_id: '4989'
quality_controlled: '1'
scopus_import: 1
status: public
title: Majority vote of diverse classifiers for late fusion
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8621
year: '2014'
...
---
_id: '2058'
abstract:
- lang: eng
  text: We present a method for smoothly blending between existing liquid animations.
    We introduce a semi-automatic method for matching two existing liquid animations,
    which we use to create new fluid motion that plausibly interpolates the input.
    Our contributions include a new space-time non-rigid iterative closest point algorithm
    that incorporates user guidance, a subsampling technique for efficient registration
    of meshes with millions of vertices, and a fast surface extraction algorithm that
    produces 3D triangle meshes from a 4D space-time surface. Our technique can be
    used to instantly create hundreds of new simulations, or to interactively explore
    complex parameter spaces. Our method is guaranteed to produce output that does
    not deviate from the input animations, and it generalizes to multiple dimensions.
    Because our method runs at interactive rates after the initial precomputation
    step, it has potential applications in games and training simulations.
article_number: '137'
article_processing_charge: No
author:
- first_name: Karthik
  full_name: Raveendran, Karthik
  last_name: Raveendran
- first_name: Christopher J
  full_name: Wojtan, Christopher J
  id: 3C61F1D2-F248-11E8-B48F-1D18A9856A87
  last_name: Wojtan
  orcid: 0000-0001-6646-5546
- first_name: Nils
  full_name: Thuerey, Nils
  last_name: Thuerey
- first_name: Greg
  full_name: Türk, Greg
  last_name: Türk
citation:
  ama: 'Raveendran K, Wojtan C, Thuerey N, Türk G. Blending liquids. In: <i>ACM Transactions
    on Graphics</i>. Vol 33. ACM; 2014. doi:<a href="https://doi.org/10.1145/2601097.2601126">10.1145/2601097.2601126</a>'
  apa: 'Raveendran, K., Wojtan, C., Thuerey, N., &#38; Türk, G. (2014). Blending liquids.
    In <i>ACM Transactions on Graphics</i> (Vol. 33). Vancouver, Canada: ACM. <a href="https://doi.org/10.1145/2601097.2601126">https://doi.org/10.1145/2601097.2601126</a>'
  chicago: Raveendran, Karthik, Chris Wojtan, Nils Thuerey, and Greg Türk. “Blending
    Liquids.” In <i>ACM Transactions on Graphics</i>, Vol. 33. ACM, 2014. <a href="https://doi.org/10.1145/2601097.2601126">https://doi.org/10.1145/2601097.2601126</a>.
  ieee: K. Raveendran, C. Wojtan, N. Thuerey, and G. Türk, “Blending liquids,” in
    <i>ACM Transactions on Graphics</i>, Vancouver, Canada, 2014, vol. 33, no. 4.
  ista: 'Raveendran K, Wojtan C, Thuerey N, Türk G. 2014. Blending liquids. ACM Transactions
    on Graphics. SIGGRAPH: International Conference and Exhibition on Computer Graphics
    and Interactive Techniques vol. 33, 137.'
  mla: Raveendran, Karthik, et al. “Blending Liquids.” <i>ACM Transactions on Graphics</i>,
    vol. 33, no. 4, 137, ACM, 2014, doi:<a href="https://doi.org/10.1145/2601097.2601126">10.1145/2601097.2601126</a>.
  short: K. Raveendran, C. Wojtan, N. Thuerey, G. Türk, in:, ACM Transactions on Graphics,
    ACM, 2014.
conference:
  end_date: 2014-08-14
  location: Vancouver, Canada
  name: 'SIGGRAPH: International Conference and Exhibition on Computer Graphics and
    Interactive Techniques'
  start_date: 2014-08-10
date_created: 2018-12-11T11:55:28Z
date_published: 2014-07-01T00:00:00Z
date_updated: 2022-08-25T14:02:46Z
day: '01'
ddc:
- '000'
department:
- _id: ChWo
doi: 10.1145/2601097.2601126
file:
- access_level: open_access
  checksum: 1752760a2e71e254537f31c0d10d9c6c
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:08:27Z
  date_updated: 2020-07-14T12:45:27Z
  file_id: '4688'
  file_name: IST-2016-606-v1+1_BlendingLiquids-Preprint.pdf
  file_size: 8387384
  relation: main_file
file_date_updated: 2020-07-14T12:45:27Z
has_accepted_license: '1'
intvolume: '        33'
issue: '4'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
project:
- _id: 25636330-B435-11E9-9278-68D0E5697425
  grant_number: 11-NSF-1070
  name: ROOTS Genome-wide Analysis of Root Traits
publication: ACM Transactions on Graphics
publication_status: published
publisher: ACM
publist_id: '4988'
pubrep_id: '606'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Blending liquids
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 33
year: '2014'
...
---
_id: '2059'
abstract:
- lang: eng
  text: Plant embryogenesis is regulated by differential distribution of the plant
    hormone auxin. However, the cells establishing these gradients during microspore
    embryogenesis remain to be identified. For the first time, we describe, using
    the DR5 or DR5rev reporter gene systems, the GFP- and GUS-based auxin biosensors
    to monitor auxin during Brassica napus androgenesis at cellular resolution in
    the initial stages. Our study provides evidence that the distribution of auxin
    changes during embryo development and depends on the temperature-inducible in
    vitro culture conditions. For this, microspores (mcs) were induced to embryogenesis
    by heat treatment and then subjected to genetic modification via Agrobacterium
    tumefaciens. The duration of high temperature treatment had a significant influence
    on auxin distribution in isolated and in vitro-cultured microspores and on microspore-derived
    embryo development. In the “mild” heat-treated (1 day at 32 °C) mcs, auxin localized
    in a polar way already at the uni-nucleate microspore, which was critical for
    the initiation of embryos with suspensor-like structure. Assuming a mean mcs radius
    of 20 μm, endogenous auxin content in a single cell corresponded to concentration
    of 1.01 μM. In mcs subjected to a prolonged heat (5 days at 32 °C), although auxin
    concentration increased dozen times, auxin polarization was set up at a few-celled
    pro-embryos without suspensor. Those embryos were enclosed in the outer wall called
    the exine. The exine rupture was accompanied by the auxin gradient polarization.
    Relative quantitative estimation of auxin, using time-lapse imaging, revealed
    that primordia possess up to 1.3-fold higher amounts than those found in the root
    apices of transgenic MDEs in the presence of exogenous auxin. Our results show,
    for the first time, which concentration of endogenous auxin coincides with the
    first cell division and how the high temperature interplays with auxin, by what
    affects delay early establishing microspore polarity. Moreover, we present how
    the local auxin accumulation demonstrates the apical–basal axis formation of the
    androgenic embryo and directs the axiality of the adult haploid plant.
acknowledgement: The research was supported by the IPP PAS-IPGB SAS bilateral project
  (“Molecular analysis of auxin distribution in oilseed androgenic embryos”), IPP
  PAS-FWO VIB bilateral project (“Auxin as signaling molecule in doubled haploid production
  of rape (B. napus var. oleifera)”), individual national research project 2011/01/D/NZ9/02547,
  and VEGA 2-0090-14.
author:
- first_name: Ewa
  full_name: Dubas, Ewa
  last_name: Dubas
- first_name: Jana
  full_name: Moravčíková, Jana
  last_name: Moravčíková
- first_name: Jana
  full_name: Libantová, Jana
  last_name: Libantová
- first_name: Ildikó
  full_name: Matušíková, Ildikó
  last_name: Matušíková
- first_name: Eva
  full_name: Benková, Eva
  id: 38F4F166-F248-11E8-B48F-1D18A9856A87
  last_name: Benková
  orcid: 0000-0002-8510-9739
- first_name: Iwona
  full_name: Zur, Iwona
  last_name: Zur
- first_name: Monika
  full_name: Krzewska, Monika
  last_name: Krzewska
citation:
  ama: Dubas E, Moravčíková J, Libantová J, et al. The influence of heat stress on
    auxin distribution in transgenic B napus microspores and microspore derived embryos.
    <i>Protoplasma</i>. 2014;251(5):1077-1087. doi:<a href="https://doi.org/10.1007/s00709-014-0616-1">10.1007/s00709-014-0616-1</a>
  apa: Dubas, E., Moravčíková, J., Libantová, J., Matušíková, I., Benková, E., Zur,
    I., &#38; Krzewska, M. (2014). The influence of heat stress on auxin distribution
    in transgenic B napus microspores and microspore derived embryos. <i>Protoplasma</i>.
    Springer. <a href="https://doi.org/10.1007/s00709-014-0616-1">https://doi.org/10.1007/s00709-014-0616-1</a>
  chicago: Dubas, Ewa, Jana Moravčíková, Jana Libantová, Ildikó Matušíková, Eva Benková,
    Iwona Zur, and Monika Krzewska. “The Influence of Heat Stress on Auxin Distribution
    in Transgenic B Napus Microspores and Microspore Derived Embryos.” <i>Protoplasma</i>.
    Springer, 2014. <a href="https://doi.org/10.1007/s00709-014-0616-1">https://doi.org/10.1007/s00709-014-0616-1</a>.
  ieee: E. Dubas <i>et al.</i>, “The influence of heat stress on auxin distribution
    in transgenic B napus microspores and microspore derived embryos,” <i>Protoplasma</i>,
    vol. 251, no. 5. Springer, pp. 1077–1087, 2014.
  ista: Dubas E, Moravčíková J, Libantová J, Matušíková I, Benková E, Zur I, Krzewska
    M. 2014. The influence of heat stress on auxin distribution in transgenic B napus
    microspores and microspore derived embryos. Protoplasma. 251(5), 1077–1087.
  mla: Dubas, Ewa, et al. “The Influence of Heat Stress on Auxin Distribution in Transgenic
    B Napus Microspores and Microspore Derived Embryos.” <i>Protoplasma</i>, vol.
    251, no. 5, Springer, 2014, pp. 1077–87, doi:<a href="https://doi.org/10.1007/s00709-014-0616-1">10.1007/s00709-014-0616-1</a>.
  short: E. Dubas, J. Moravčíková, J. Libantová, I. Matušíková, E. Benková, I. Zur,
    M. Krzewska, Protoplasma 251 (2014) 1077–1087.
date_created: 2018-12-11T11:55:29Z
date_published: 2014-02-20T00:00:00Z
date_updated: 2021-01-12T06:55:02Z
day: '20'
ddc:
- '580'
department:
- _id: EvBe
doi: 10.1007/s00709-014-0616-1
file:
- access_level: open_access
  checksum: d570a6073765118fc0bb83c31d96fa53
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:18:31Z
  date_updated: 2020-07-14T12:45:27Z
  file_id: '5353'
  file_name: IST-2015-394-v1+1_s00709-014-0616-1.pdf
  file_size: 6377990
  relation: main_file
file_date_updated: 2020-07-14T12:45:27Z
has_accepted_license: '1'
intvolume: '       251'
issue: '5'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: 1077 - 1087
publication: Protoplasma
publication_status: published
publisher: Springer
publist_id: '4987'
pubrep_id: '394'
quality_controlled: '1'
scopus_import: 1
status: public
title: The influence of heat stress on auxin distribution in transgenic B napus microspores
  and microspore derived embryos
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 251
year: '2014'
...
---
_id: '2061'
abstract:
- lang: eng
  text: 'Development of cambium and its activity is important for our knowledge of
    the mechanism of secondary growth. Arabidopsis thaliana emerges as a good model
    plant for such a kind of study. Thus, this paper reports on cellular events taking
    place in the interfascicular regions of inflorescence stems of A. thaliana, leading
    to the development of interfascicular cambium from differentiated interfascicular
    parenchyma cells (IPC). These events are as follows: appearance of auxin accumulation,
    PIN1 gene expression, polar PIN1 protein localization in the basal plasma membrane
    and periclinal divisions. Distribution of auxin was observed to be higher in differentiating
    into cambium parenchyma cells compared to cells within the pith and cortex. Expression
    of PIN1 in IPC was always preceded by auxin accumulation. Basal localization of
    PIN1 was already established in the cells prior to their periclinal division.
    These cellular events initiated within parenchyma cells adjacent to the vascular
    bundles and successively extended from that point towards the middle region of
    the interfascicular area, located between neighboring vascular bundles. The final
    consequence of which was the closure of the cambial ring within the stem. Changes
    in the chemical composition of IPC walls were also detected and included changes
    of pectic epitopes, xyloglucans (XG) and extensins rich in hydroxyproline (HRGPs).
    In summary, results presented in this paper describe interfascicular cambium ontogenesis
    in terms of successive cellular events in the interfascicular regions of inflorescence
    stems of Arabidopsis.'
author:
- first_name: Ewa
  full_name: Mazur, Ewa
  last_name: Mazur
- first_name: Ewa
  full_name: Kurczyñska, Ewa
  last_name: Kurczyñska
- first_name: Jiří
  full_name: Friml, Jiří
  id: 4159519E-F248-11E8-B48F-1D18A9856A87
  last_name: Friml
  orcid: 0000-0002-8302-7596
citation:
  ama: Mazur E, Kurczyñska E, Friml J. Cellular events during interfascicular cambium
    ontogenesis in inflorescence stems of Arabidopsis. <i>Protoplasma</i>. 2014;251(5):1125-1139.
    doi:<a href="https://doi.org/10.1007/s00709-014-0620-5">10.1007/s00709-014-0620-5</a>
  apa: Mazur, E., Kurczyñska, E., &#38; Friml, J. (2014). Cellular events during interfascicular
    cambium ontogenesis in inflorescence stems of Arabidopsis. <i>Protoplasma</i>.
    Springer. <a href="https://doi.org/10.1007/s00709-014-0620-5">https://doi.org/10.1007/s00709-014-0620-5</a>
  chicago: Mazur, Ewa, Ewa Kurczyñska, and Jiří Friml. “Cellular Events during Interfascicular
    Cambium Ontogenesis in Inflorescence Stems of Arabidopsis.” <i>Protoplasma</i>.
    Springer, 2014. <a href="https://doi.org/10.1007/s00709-014-0620-5">https://doi.org/10.1007/s00709-014-0620-5</a>.
  ieee: E. Mazur, E. Kurczyñska, and J. Friml, “Cellular events during interfascicular
    cambium ontogenesis in inflorescence stems of Arabidopsis,” <i>Protoplasma</i>,
    vol. 251, no. 5. Springer, pp. 1125–1139, 2014.
  ista: Mazur E, Kurczyñska E, Friml J. 2014. Cellular events during interfascicular
    cambium ontogenesis in inflorescence stems of Arabidopsis. Protoplasma. 251(5),
    1125–1139.
  mla: Mazur, Ewa, et al. “Cellular Events during Interfascicular Cambium Ontogenesis
    in Inflorescence Stems of Arabidopsis.” <i>Protoplasma</i>, vol. 251, no. 5, Springer,
    2014, pp. 1125–39, doi:<a href="https://doi.org/10.1007/s00709-014-0620-5">10.1007/s00709-014-0620-5</a>.
  short: E. Mazur, E. Kurczyñska, J. Friml, Protoplasma 251 (2014) 1125–1139.
date_created: 2018-12-11T11:55:29Z
date_published: 2014-02-14T00:00:00Z
date_updated: 2021-01-12T06:55:03Z
day: '14'
department:
- _id: JiFr
doi: 10.1007/s00709-014-0620-5
intvolume: '       251'
issue: '5'
language:
- iso: eng
month: '02'
oa_version: None
page: 1125 - 1139
publication: Protoplasma
publication_status: published
publisher: Springer
publist_id: '4985'
quality_controlled: '1'
scopus_import: 1
status: public
title: Cellular events during interfascicular cambium ontogenesis in inflorescence
  stems of Arabidopsis
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 251
year: '2014'
...
---
_id: '2062'
abstract:
- lang: eng
  text: The success story of fast-spiking, parvalbumin-positive (PV+) GABAergic interneurons
    (GABA, γ-aminobutyric acid) in the mammalian central nervous system is noteworthy.
    In 1995, the properties of these interneurons were completely unknown. Twenty
    years later, thanks to the massive use of subcellular patch-clamp techniques,
    simultaneous multiple-cell recording, optogenetics, in vivo measurements, and
    computational approaches, our knowledge about PV+ interneurons became more extensive
    than for several types of pyramidal neurons. These findings have implications
    beyond the “small world” of basic research on GABAergic cells. For example, the
    results provide a first proof of principle that neuroscientists might be able
    to close the gaps between the molecular, cellular, network, and behavioral levels,
    representing one of the main challenges at the present time. Furthermore, the
    results may form the basis for PV+ interneurons as therapeutic targets for brain
    disease in the future. However, much needs to be learned about the basic function
    of these interneurons before clinical neuroscientists will be able to use PV+
    interneurons for therapeutic purposes.
article_number: '1255263'
author:
- first_name: Hua
  full_name: Hu, Hua
  id: 4AC0145C-F248-11E8-B48F-1D18A9856A87
  last_name: Hu
- first_name: Jian
  full_name: Gan, Jian
  id: 3614E438-F248-11E8-B48F-1D18A9856A87
  last_name: Gan
- first_name: Peter M
  full_name: Jonas, Peter M
  id: 353C1B58-F248-11E8-B48F-1D18A9856A87
  last_name: Jonas
  orcid: 0000-0001-5001-4804
citation:
  ama: 'Hu H, Gan J, Jonas PM. Fast-spiking parvalbumin^+ GABAergic interneurons:
    From cellular design to microcircuit function. <i>Science</i>. 2014;345(6196).
    doi:<a href="https://doi.org/10.1126/science.1255263">10.1126/science.1255263</a>'
  apa: 'Hu, H., Gan, J., &#38; Jonas, P. M. (2014). Fast-spiking parvalbumin^+ GABAergic
    interneurons: From cellular design to microcircuit function. <i>Science</i>. American
    Association for the Advancement of Science. <a href="https://doi.org/10.1126/science.1255263">https://doi.org/10.1126/science.1255263</a>'
  chicago: 'Hu, Hua, Jian Gan, and Peter M Jonas. “Fast-Spiking Parvalbumin^+ GABAergic
    Interneurons: From Cellular Design to Microcircuit Function.” <i>Science</i>.
    American Association for the Advancement of Science, 2014. <a href="https://doi.org/10.1126/science.1255263">https://doi.org/10.1126/science.1255263</a>.'
  ieee: 'H. Hu, J. Gan, and P. M. Jonas, “Fast-spiking parvalbumin^+ GABAergic interneurons:
    From cellular design to microcircuit function,” <i>Science</i>, vol. 345, no.
    6196. American Association for the Advancement of Science, 2014.'
  ista: 'Hu H, Gan J, Jonas PM. 2014. Fast-spiking parvalbumin^+ GABAergic interneurons:
    From cellular design to microcircuit function. Science. 345(6196), 1255263.'
  mla: 'Hu, Hua, et al. “Fast-Spiking Parvalbumin^+ GABAergic Interneurons: From Cellular
    Design to Microcircuit Function.” <i>Science</i>, vol. 345, no. 6196, 1255263,
    American Association for the Advancement of Science, 2014, doi:<a href="https://doi.org/10.1126/science.1255263">10.1126/science.1255263</a>.'
  short: H. Hu, J. Gan, P.M. Jonas, Science 345 (2014).
date_created: 2018-12-11T11:55:29Z
date_published: 2014-08-01T00:00:00Z
date_updated: 2021-01-12T06:55:03Z
day: '01'
ddc:
- '570'
department:
- _id: PeJo
doi: 10.1126/science.1255263
ec_funded: 1
file:
- access_level: open_access
  checksum: a0036a589037d37e86364fa25cc0a82f
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:16:00Z
  date_updated: 2020-07-14T12:45:27Z
  file_id: '5185'
  file_name: IST-2017-821-v1+1_1255263JonasPVReviewTextR_Final.pdf
  file_size: 215514
  relation: main_file
- access_level: open_access
  checksum: e1f57d2713725449cb898fdcb8ef47b8
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:16:01Z
  date_updated: 2020-07-14T12:45:27Z
  file_id: '5186'
  file_name: IST-2017-821-v1+2_1255263JonasPVReviewFigures_Final.pdf
  file_size: 1732723
  relation: main_file
file_date_updated: 2020-07-14T12:45:27Z
has_accepted_license: '1'
intvolume: '       345'
issue: '6196'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
project:
- _id: 25C26B1E-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P24909-B24
  name: Mechanisms of transmitter release at GABAergic synapses
- _id: 25C0F108-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '268548'
  name: Nanophysiology of fast-spiking, parvalbumin-expressing GABAergic interneurons
publication: Science
publication_status: published
publisher: American Association for the Advancement of Science
publist_id: '4984'
pubrep_id: '821'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Fast-spiking parvalbumin^+ GABAergic interneurons: From cellular design to
  microcircuit function'
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 345
year: '2014'
...
---
_id: '2063'
abstract:
- lang: eng
  text: We consider Markov decision processes (MDPs) which are a standard model for
    probabilistic systems.We focus on qualitative properties forMDPs that can express
    that desired behaviors of the system arise almost-surely (with probability 1)
    or with positive probability. We introduce a new simulation relation to capture
    the refinement relation ofMDPs with respect to qualitative properties, and present
    discrete graph theoretic algorithms with quadratic complexity to compute the simulation
    relation.We present an automated technique for assume-guarantee style reasoning
    for compositional analysis ofMDPs with qualitative properties by giving a counterexample
    guided abstraction-refinement approach to compute our new simulation relation.
    We have implemented our algorithms and show that the compositional analysis leads
    to significant improvements.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Martin
  full_name: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
- first_name: Przemyslaw
  full_name: Daca, Przemyslaw
  id: 49351290-F248-11E8-B48F-1D18A9856A87
  last_name: Daca
citation:
  ama: 'Chatterjee K, Chmelik M, Daca P. CEGAR for qualitative analysis of probabilistic
    systems. In: Vol 8559. Springer; 2014:473-490. doi:<a href="https://doi.org/10.1007/978-3-319-08867-9_31">10.1007/978-3-319-08867-9_31</a>'
  apa: 'Chatterjee, K., Chmelik, M., &#38; Daca, P. (2014). CEGAR for qualitative
    analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV:
    Computer Aided Verification, Vienna, Austria: Springer. <a href="https://doi.org/10.1007/978-3-319-08867-9_31">https://doi.org/10.1007/978-3-319-08867-9_31</a>'
  chicago: Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for
    Qualitative Analysis of Probabilistic Systems,” 8559:473–90. Springer, 2014. <a
    href="https://doi.org/10.1007/978-3-319-08867-9_31">https://doi.org/10.1007/978-3-319-08867-9_31</a>.
  ieee: 'K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for qualitative analysis of
    probabilistic systems,” presented at the CAV: Computer Aided Verification, Vienna,
    Austria, 2014, vol. 8559, pp. 473–490.'
  ista: 'Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of
    probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490.'
  mla: Chatterjee, Krishnendu, et al. <i>CEGAR for Qualitative Analysis of Probabilistic
    Systems</i>. Vol. 8559, Springer, 2014, pp. 473–90, doi:<a href="https://doi.org/10.1007/978-3-319-08867-9_31">10.1007/978-3-319-08867-9_31</a>.
  short: K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490.
conference:
  end_date: 2014-07-22
  location: Vienna, Austria
  name: 'CAV: Computer Aided Verification'
  start_date: 2014-07-18
date_created: 2018-12-11T11:55:30Z
date_published: 2014-07-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-08867-9_31
ec_funded: 1
intvolume: '      8559'
language:
- iso: eng
month: '07'
oa_version: None
page: 473 - 490
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: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '4978'
quality_controlled: '1'
related_material:
  record:
  - id: '5412'
    relation: earlier_version
    status: public
  - id: '5413'
    relation: earlier_version
    status: public
  - id: '5414'
    relation: earlier_version
    status: public
  - id: '1155'
    relation: dissertation_contains
    status: public
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8559
year: '2014'
...
---
_id: '2064'
abstract:
- lang: eng
  text: We examined the synaptic structure, quantity, and distribution of α-amino-3-hydroxy-5-methylisoxazole-4-propionic
    acid (AMPA)- and N-methyl-D-aspartate (NMDA)-type glutamate receptors (AMPARs
    and NMDARs, respectively) in rat cochlear nuclei by a highly sensitive freeze-fracture
    replica labeling technique. Four excitatory synapses formed by two distinct inputs,
    auditory nerve (AN) and parallel fibers (PF), on different cell types were analyzed.
    These excitatory synapse types included AN synapses on bushy cells (AN-BC synapses)
    and fusiform cells (AN-FC synapses) and PF synapses on FC (PF-FC synapses) and
    cartwheel cell spines (PF-CwC synapses). Immunogold labeling revealed differences
    in synaptic structure as well as AMPAR and NMDAR number and/or density in both
    AN and PF synapses, indicating a target-dependent organization. The immunogold
    receptor labeling also identified differences in the synaptic organization of
    FCs based on AN or PF connections, indicating an input-dependent organization
    in FCs. Among the four excitatory synapse types, the AN-BC synapses were the smallest
    and had the most densely packed intramembrane particles (IMPs), whereas the PF-CwC
    synapses were the largest and had sparsely packed IMPs. All four synapse types
    showed positive correlations between the IMP-cluster area and the AMPAR number,
    indicating a common intrasynapse-type relationship for glutamatergic synapses.
    Immunogold particles for AMPARs were distributed over the entire area of individual
    AN synapses; PF synapses often showed synaptic areas devoid of labeling. The gold-labeling
    for NMDARs occurred in a mosaic fashion, with less positive correlations between
    the IMP-cluster area and the NMDAR number. Our observations reveal target- and
    input-dependent features in the structure, number, and organization of AMPARs
    and NMDARs in AN and PF synapses.
acknowledgement: "National Institutes of Health (NIH) Grant Number: 1R01DC013048‐0;
  Biotechnology and Biological Sciences Research Council, UK Grant Number: BB/J015938/1\r\n"
author:
- first_name: Maía
  full_name: Rubio, Maía
  last_name: Rubio
- first_name: Yugo
  full_name: Fukazawa, Yugo
  last_name: Fukazawa
- first_name: Naomi
  full_name: Kamasawa, Naomi
  last_name: Kamasawa
- first_name: Cheryl
  full_name: Clarkson, Cheryl
  last_name: Clarkson
- first_name: Elek
  full_name: Molnár, Elek
  last_name: Molnár
- first_name: Ryuichi
  full_name: Shigemoto, Ryuichi
  id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
  last_name: Shigemoto
  orcid: 0000-0001-8761-9444
citation:
  ama: Rubio M, Fukazawa Y, Kamasawa N, Clarkson C, Molnár E, Shigemoto R. Target-
    and input-dependent organization of AMPA and NMDA receptors in synaptic connections
    of the cochlear nucleus. <i>Journal of Comparative Neurology</i>. 2014;522(18):4023-4042.
    doi:<a href="https://doi.org/10.1002/cne.23654">10.1002/cne.23654</a>
  apa: Rubio, M., Fukazawa, Y., Kamasawa, N., Clarkson, C., Molnár, E., &#38; Shigemoto,
    R. (2014). Target- and input-dependent organization of AMPA and NMDA receptors
    in synaptic connections of the cochlear nucleus. <i>Journal of Comparative Neurology</i>.
    Wiley-Blackwell. <a href="https://doi.org/10.1002/cne.23654">https://doi.org/10.1002/cne.23654</a>
  chicago: Rubio, Maía, Yugo Fukazawa, Naomi Kamasawa, Cheryl Clarkson, Elek Molnár,
    and Ryuichi Shigemoto. “Target- and Input-Dependent Organization of AMPA and NMDA
    Receptors in Synaptic Connections of the Cochlear Nucleus.” <i>Journal of Comparative
    Neurology</i>. Wiley-Blackwell, 2014. <a href="https://doi.org/10.1002/cne.23654">https://doi.org/10.1002/cne.23654</a>.
  ieee: M. Rubio, Y. Fukazawa, N. Kamasawa, C. Clarkson, E. Molnár, and R. Shigemoto,
    “Target- and input-dependent organization of AMPA and NMDA receptors in synaptic
    connections of the cochlear nucleus,” <i>Journal of Comparative Neurology</i>,
    vol. 522, no. 18. Wiley-Blackwell, pp. 4023–4042, 2014.
  ista: Rubio M, Fukazawa Y, Kamasawa N, Clarkson C, Molnár E, Shigemoto R. 2014.
    Target- and input-dependent organization of AMPA and NMDA receptors in synaptic
    connections of the cochlear nucleus. Journal of Comparative Neurology. 522(18),
    4023–4042.
  mla: Rubio, Maía, et al. “Target- and Input-Dependent Organization of AMPA and NMDA
    Receptors in Synaptic Connections of the Cochlear Nucleus.” <i>Journal of Comparative
    Neurology</i>, vol. 522, no. 18, Wiley-Blackwell, 2014, pp. 4023–42, doi:<a href="https://doi.org/10.1002/cne.23654">10.1002/cne.23654</a>.
  short: M. Rubio, Y. Fukazawa, N. Kamasawa, C. Clarkson, E. Molnár, R. Shigemoto,
    Journal of Comparative Neurology 522 (2014) 4023–4042.
date_created: 2018-12-11T11:55:30Z
date_published: 2014-07-29T00:00:00Z
date_updated: 2021-01-12T06:55:05Z
day: '29'
department:
- _id: RySh
doi: 10.1002/cne.23654
intvolume: '       522'
issue: '18'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4198489/
month: '07'
oa: 1
oa_version: Submitted Version
page: 4023 - 4042
publication: Journal of Comparative Neurology
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4974'
quality_controlled: '1'
scopus_import: 1
status: public
title: Target- and input-dependent organization of AMPA and NMDA receptors in synaptic
  connections of the cochlear nucleus
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 522
year: '2014'
...
---
_id: '1375'
abstract:
- lang: eng
  text: 'We consider directed graphs where each edge is labeled with an integer weight
    and study the fundamental algorithmic question of computing the value of a cycle
    with minimum mean weight. Our contributions are twofold: (1) First we show that
    the algorithmic question is reducible to the problem of a logarithmic number of
    min-plus matrix multiplications of n×n-matrices, where n is the number of vertices
    of the graph. (2) Second, when the weights are nonnegative, we present the first
    (1+ε)-approximation algorithm for the problem and the running time of our algorithm
    is Õ(nωlog3(nW/ε)/ε),1 where O(nω) is the time required for the classic n×n-matrix
    multiplication and W is the maximum value of the weights. With an additional O(log(nW/ε))
    factor in space a cycle with approximately optimal weight can be computed within
    the same time bound.'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Sebastian
  full_name: Krinninger, Sebastian
  last_name: Krinninger
- first_name: Veronika
  full_name: Loitzenbauer, Veronika
  last_name: Loitzenbauer
- first_name: Michael
  full_name: Raskin, Michael
  last_name: Raskin
citation:
  ama: Chatterjee K, Henzinger MH, Krinninger S, Loitzenbauer V, Raskin M. Approximating
    the minimum cycle mean. <i>Theoretical Computer Science</i>. 2014;547(C):104-116.
    doi:<a href="https://doi.org/10.1016/j.tcs.2014.06.031">10.1016/j.tcs.2014.06.031</a>
  apa: Chatterjee, K., Henzinger, M. H., Krinninger, S., Loitzenbauer, V., &#38; Raskin,
    M. (2014). Approximating the minimum cycle mean. <i>Theoretical Computer Science</i>.
    Elsevier. <a href="https://doi.org/10.1016/j.tcs.2014.06.031">https://doi.org/10.1016/j.tcs.2014.06.031</a>
  chicago: Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, Veronika
    Loitzenbauer, and Michael Raskin. “Approximating the Minimum Cycle Mean.” <i>Theoretical
    Computer Science</i>. Elsevier, 2014. <a href="https://doi.org/10.1016/j.tcs.2014.06.031">https://doi.org/10.1016/j.tcs.2014.06.031</a>.
  ieee: K. Chatterjee, M. H. Henzinger, S. Krinninger, V. Loitzenbauer, and M. Raskin,
    “Approximating the minimum cycle mean,” <i>Theoretical Computer Science</i>, vol.
    547, no. C. Elsevier, pp. 104–116, 2014.
  ista: Chatterjee K, Henzinger MH, Krinninger S, Loitzenbauer V, Raskin M. 2014.
    Approximating the minimum cycle mean. Theoretical Computer Science. 547(C), 104–116.
  mla: Chatterjee, Krishnendu, et al. “Approximating the Minimum Cycle Mean.” <i>Theoretical
    Computer Science</i>, vol. 547, no. C, Elsevier, 2014, pp. 104–16, doi:<a href="https://doi.org/10.1016/j.tcs.2014.06.031">10.1016/j.tcs.2014.06.031</a>.
  short: K. Chatterjee, M.H. Henzinger, S. Krinninger, V. Loitzenbauer, M. Raskin,
    Theoretical Computer Science 547 (2014) 104–116.
date_created: 2018-12-11T11:51:40Z
date_published: 2014-08-28T00:00:00Z
date_updated: 2022-09-09T11:50:58Z
day: '28'
department:
- _id: KrCh
doi: 10.1016/j.tcs.2014.06.031
ec_funded: 1
external_id:
  arxiv:
  - '1307.4473'
intvolume: '       547'
issue: C
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1307.4473
month: '08'
oa: 1
oa_version: Preprint
page: 104 - 116
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: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '5836'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Approximating the minimum cycle mean
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 547
year: '2014'
...
---
_id: '1392'
abstract:
- lang: eng
  text: Fault-tolerant distributed algorithms play an important role in ensuring the
    reliability of many software applications. In this paper we consider distributed
    algorithms whose computations are organized in rounds. To verify the correctness
    of such algorithms, we reason about (i) properties (such as invariants) of the
    state, (ii) the transitions controlled by the algorithm, and (iii) the communication
    graph. We introduce a logic that addresses these points, and contains set comprehensions
    with cardinality constraints, function symbols to describe the local states of
    each process, and a limited form of quantifier alternation to express the verification
    conditions. We show its use in automating the verification of consensus algorithms.
    In particular, we give a semi-decision procedure for the unsatisfiability problem
    of the logic and identify a decidable fragment. We successfully applied our framework
    to verify the correctness of a variety of consensus algorithms tolerant to both
    benign faults (message loss, process crashes) and value faults (message corruption).
acknowledgement: Supported by the Vienna Science and Technology Fund (WWTF) through
  grant PROSEED.
alternative_title:
- LNCS
author:
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- 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: Helmut
  full_name: Veith, Helmut
  last_name: Veith
- first_name: Josef
  full_name: Widder, Josef
  last_name: Widder
- first_name: Damien
  full_name: Zufferey, Damien
  id: 4397AC76-F248-11E8-B48F-1D18A9856A87
  last_name: Zufferey
  orcid: 0000-0002-3197-8736
citation:
  ama: 'Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. A logic-based framework
    for verifying consensus algorithms. In: Vol 8318. Springer; 2014:161-181. doi:<a
    href="https://doi.org/10.1007/978-3-642-54013-4_10">10.1007/978-3-642-54013-4_10</a>'
  apa: 'Dragoi, C., Henzinger, T. A., Veith, H., Widder, J., &#38; Zufferey, D. (2014).
    A logic-based framework for verifying consensus algorithms (Vol. 8318, pp. 161–181).
    Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
    San Diego, USA: Springer. <a href="https://doi.org/10.1007/978-3-642-54013-4_10">https://doi.org/10.1007/978-3-642-54013-4_10</a>'
  chicago: Dragoi, Cezara, Thomas A Henzinger, Helmut Veith, Josef Widder, and Damien
    Zufferey. “A Logic-Based Framework for Verifying Consensus Algorithms,” 8318:161–81.
    Springer, 2014. <a href="https://doi.org/10.1007/978-3-642-54013-4_10">https://doi.org/10.1007/978-3-642-54013-4_10</a>.
  ieee: 'C. Dragoi, T. A. Henzinger, H. Veith, J. Widder, and D. Zufferey, “A logic-based
    framework for verifying consensus algorithms,” presented at the VMCAI: Verification,
    Model Checking and Abstract Interpretation, San Diego, USA, 2014, vol. 8318, pp.
    161–181.'
  ista: 'Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. 2014. A logic-based
    framework for verifying consensus algorithms. VMCAI: Verification, Model Checking
    and Abstract Interpretation, LNCS, vol. 8318, 161–181.'
  mla: Dragoi, Cezara, et al. <i>A Logic-Based Framework for Verifying Consensus Algorithms</i>.
    Vol. 8318, Springer, 2014, pp. 161–81, doi:<a href="https://doi.org/10.1007/978-3-642-54013-4_10">10.1007/978-3-642-54013-4_10</a>.
  short: C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer,
    2014, pp. 161–181.
conference:
  end_date: 2014-01-21
  location: San Diego, USA
  name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
  start_date: 2014-01-19
date_created: 2018-12-11T11:51:45Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2021-01-12T06:50:22Z
day: '01'
ddc:
- '000'
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-54013-4_10
ec_funded: 1
file:
- access_level: open_access
  checksum: bffa33d39be77df0da39defe97eabf84
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:11:06Z
  date_updated: 2020-07-14T12:44:48Z
  file_id: '4859'
  file_name: IST-2014-179-v1+1_vmcai14.pdf
  file_size: 444138
  relation: main_file
file_date_updated: 2020-07-14T12:44:48Z
has_accepted_license: '1'
intvolume: '      8318'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 161 - 181
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: '5817'
pubrep_id: '179'
quality_controlled: '1'
scopus_import: 1
status: public
title: A logic-based framework for verifying consensus algorithms
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8318
year: '2014'
...
---
_id: '1393'
abstract:
- lang: eng
  text: 'Probabilistic programs are usual functional or imperative programs with two
    added constructs: (1) the ability to draw values at random from distributions,
    and (2) the ability to condition values of variables in a program via observations.
    Models from diverse application areas such as computer vision, coding theory,
    cryptographic protocols, biology and reliability analysis can be written as probabilistic
    programs. Probabilistic inference is the problem of computing an explicit representation
    of the probability distribution implicitly specified by a probabilistic program.
    Depending on the application, the desired output from inference may vary-we may
    want to estimate the expected value of some function f with respect to the distribution,
    or the mode of the distribution, or simply a set of samples drawn from the distribution.
    In this paper, we describe connections this research area called \Probabilistic
    Programming&quot; has with programming languages and software engineering, and
    this includes language design, and the static and dynamic analysis of programs.
    We survey current state of the art and speculate on promising directions for future
    research.'
article_processing_charge: No
author:
- first_name: Andrew
  full_name: Gordon, Andrew
  last_name: Gordon
- 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: Aditya
  full_name: Nori, Aditya
  last_name: Nori
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
citation:
  ama: 'Gordon A, Henzinger TA, Nori A, Rajamani S. Probabilistic programming. In:
    <i>Proceedings of the on Future of Software Engineering</i>. ACM; 2014:167-181.
    doi:<a href="https://doi.org/10.1145/2593882.2593900">10.1145/2593882.2593900</a>'
  apa: 'Gordon, A., Henzinger, T. A., Nori, A., &#38; Rajamani, S. (2014). Probabilistic
    programming. In <i>Proceedings of the on Future of Software Engineering</i> (pp.
    167–181). Hyderabad, India: ACM. <a href="https://doi.org/10.1145/2593882.2593900">https://doi.org/10.1145/2593882.2593900</a>'
  chicago: Gordon, Andrew, Thomas A Henzinger, Aditya Nori, and Sriram Rajamani. “Probabilistic
    Programming.” In <i>Proceedings of the on Future of Software Engineering</i>,
    167–81. ACM, 2014. <a href="https://doi.org/10.1145/2593882.2593900">https://doi.org/10.1145/2593882.2593900</a>.
  ieee: A. Gordon, T. A. Henzinger, A. Nori, and S. Rajamani, “Probabilistic programming,”
    in <i>Proceedings of the on Future of Software Engineering</i>, Hyderabad, India,
    2014, pp. 167–181.
  ista: 'Gordon A, Henzinger TA, Nori A, Rajamani S. 2014. Probabilistic programming.
    Proceedings of the on Future of Software Engineering. FOSE: Future of Software
    Engineering, 167–181.'
  mla: Gordon, Andrew, et al. “Probabilistic Programming.” <i>Proceedings of the on
    Future of Software Engineering</i>, ACM, 2014, pp. 167–81, doi:<a href="https://doi.org/10.1145/2593882.2593900">10.1145/2593882.2593900</a>.
  short: A. Gordon, T.A. Henzinger, A. Nori, S. Rajamani, in:, Proceedings of the
    on Future of Software Engineering, ACM, 2014, pp. 167–181.
conference:
  end_date: 2014-06-07
  location: Hyderabad, India
  name: 'FOSE: Future of Software Engineering'
  start_date: 2014-05-31
date_created: 2018-12-11T11:51:45Z
date_published: 2014-05-31T00:00:00Z
date_updated: 2021-01-12T06:50:22Z
day: '31'
department:
- _id: ToHe
doi: 10.1145/2593882.2593900
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1145/2593882.2593900
month: '05'
oa: 1
oa_version: Published Version
page: 167 - 181
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 on Future of Software Engineering
publication_status: published
publisher: ACM
publist_id: '5816'
quality_controlled: '1'
scopus_import: 1
status: public
title: Probabilistic programming
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '1395'
abstract:
- lang: eng
  text: In this thesis I studied various individual and social immune defences employed
    by the invasive garden ant Lasius neglectus mostly against entomopathogenic fungi.  The
    first two chapters of this thesis address the phenomenon of 'social immunisation'.
    Social immunisation, that is the immunological protection of group members due
    to social contact to a pathogen-exposed nestmate, has been described in various
    social insect species against different types of pathogens. However, in the case
    of entomopathogenic fungi it has, so far, only been demonstrated that social immunisation
    exists at all. Its underlying mechanisms r any other properties were, however,
    unknown. In the first chapter of this thesis I identified the mechanistic basis
    of social immunisation in L. neglectus against the entomopathogenous fungus Metarhizium.
    I could show that nestmates of a pathogen-exposed individual contract low-level
    infections due to social interactions. These low-level infections are, however,
    non-lethal and cause an active stimulation of the immune system, which protects
    the nestmates upon subsequent pathogen encounters. In the second chapter of this
    thesis I investigated the specificity and colony level effects of social immunisation.
    I demonstrated that the protection conferred by social immunisation is highly
    specific, protecting ants only against the same pathogen strain. In addition,
    depending on the respective context, social immunisation may even cause fitness
    costs. I further showed that social immunisation crucially affects sanitary behaviour
    and disease dynamics within ant groups. In the third chapter of this thesis I
    studied the effects of the ectosymbiotic fungus Laboulbenia formicarum on its
    host L. neglectus. Although Laboulbeniales are the largest order of insect-parasitic
    fungi, research concerning host fitness consequence is sparse. I showed that highly
    Laboulbenia-infected ants sustain fitness costs under resource limitation, however,
    gain fitness benefits when exposed to an entomopathogenus fungus. These effects
    are probably cause by a prophylactic upregulation of behavioural as well as physiological
    immune defences in highly infected ants.
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Matthias
  full_name: Konrad, Matthias
  id: 46528076-F248-11E8-B48F-1D18A9856A87
  last_name: Konrad
citation:
  ama: 'Konrad M. Immune defences in ants: Effects of social immunisation and a fungal
    ectosymbiont in the ant Lasius neglectus. 2014.'
  apa: 'Konrad, M. (2014). <i>Immune defences in ants: Effects of social immunisation
    and a fungal ectosymbiont in the ant Lasius neglectus</i>. Institute of Science
    and Technology Austria.'
  chicago: 'Konrad, Matthias. “Immune Defences in Ants: Effects of Social Immunisation
    and a Fungal Ectosymbiont in the Ant Lasius Neglectus.” Institute of Science and
    Technology Austria, 2014.'
  ieee: 'M. Konrad, “Immune defences in ants: Effects of social immunisation and a
    fungal ectosymbiont in the ant Lasius neglectus,” Institute of Science and Technology
    Austria, 2014.'
  ista: 'Konrad M. 2014. Immune defences in ants: Effects of social immunisation and
    a fungal ectosymbiont in the ant Lasius neglectus. Institute of Science and Technology
    Austria.'
  mla: 'Konrad, Matthias. <i>Immune Defences in Ants: Effects of Social Immunisation
    and a Fungal Ectosymbiont in the Ant Lasius Neglectus</i>. Institute of Science
    and Technology Austria, 2014.'
  short: 'M. Konrad, Immune Defences in Ants: Effects of Social Immunisation and a
    Fungal Ectosymbiont in the Ant Lasius Neglectus, Institute of Science and Technology
    Austria, 2014.'
date_created: 2018-12-11T11:51:46Z
date_published: 2014-02-01T00:00:00Z
date_updated: 2023-09-07T11:38:56Z
day: '01'
degree_awarded: PhD
department:
- _id: SyCr
language:
- iso: eng
month: '02'
oa_version: None
page: '131'
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5814'
status: public
supervisor:
- first_name: Sylvia M
  full_name: Cremer, Sylvia M
  id: 2F64EC8C-F248-11E8-B48F-1D18A9856A87
  last_name: Cremer
  orcid: 0000-0002-2193-3868
title: 'Immune defences in ants: Effects of social immunisation and a fungal ectosymbiont
  in the ant Lasius neglectus'
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2014'
...
---
_id: '1402'
abstract:
- lang: eng
  text: Phosphatidylinositol (Ptdlns) is a structural phospholipid that can be phosphorylated
    into various lipid signaling molecules, designated polyphosphoinositides (PPIs).
    The reversible phosphorylation of PPIs on the 3, 4, or 5 position of inositol
    is performed by a set of organelle-specific kinases and phosphatases, and the
    characteristic head groups make these molecules ideal for regulating biological
    processes in time and space. In yeast and mammals, Ptdlns3P and Ptdlns(3,5)P2
    play crucial roles in trafficking toward the lytic compartments, whereas the role
    in plants is not yet fully understood. Here we identified the role of a land plant-specific
    subgroup of PPI phosphatases, the suppressor of actin 2 (SAC2) to SAC5, during
    vauolar trafficking and morphogenesis in Arabidopsis thaliana. SAC2-SAC5 localize
    to the tonoplast along with Ptdlns3P, the presumable product of their activity.
    in SAC gain- and loss-of-function mutants, the levels of Ptdlns monophosphates
    and bisphosphates were changed, with opposite effects on the morphology of storage
    and lytic vacuoles, and the trafficking toward the vacuoles was defective. Moreover,
    multiple sac knockout mutants had an increased number of smaller storage and lytic
    vacuoles, whereas extralarge vacuoles were observed in the overexpression lines,
    correlating with various growth and developmental defects. The fragmented vacuolar
    phenotype of sac mutants could be mimicked by treating wild-type seedlings with
    Ptdlns(3,5)P2, corroborating that this PPI is important for vacuole morphology.
    Taken together, these results provide evidence that PPIs, together with their
    metabolic enzymes SAC2-SAC5, are crucial for vacuolar trafficking and for vacuolar
    morphology and function in plants.
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Petra
  full_name: Marhavá, Petra
  id: 44E59624-F248-11E8-B48F-1D18A9856A87
  last_name: Marhavá
citation:
  ama: Marhavá P. Molecular mechanisms of patterning and subcellular trafficking in
    Arabidopsis thaliana. 2014.
  apa: Marhavá, P. (2014). <i>Molecular mechanisms of patterning and subcellular trafficking
    in Arabidopsis thaliana</i>. Institute of Science and Technology Austria.
  chicago: Marhavá, Petra. “Molecular Mechanisms of Patterning and Subcellular Trafficking
    in Arabidopsis Thaliana.” Institute of Science and Technology Austria, 2014.
  ieee: P. Marhavá, “Molecular mechanisms of patterning and subcellular trafficking
    in Arabidopsis thaliana,” Institute of Science and Technology Austria, 2014.
  ista: Marhavá P. 2014. Molecular mechanisms of patterning and subcellular trafficking
    in Arabidopsis thaliana. Institute of Science and Technology Austria.
  mla: Marhavá, Petra. <i>Molecular Mechanisms of Patterning and Subcellular Trafficking
    in Arabidopsis Thaliana</i>. Institute of Science and Technology Austria, 2014.
  short: P. Marhavá, Molecular Mechanisms of Patterning and Subcellular Trafficking
    in Arabidopsis Thaliana, Institute of Science and Technology Austria, 2014.
date_created: 2018-12-11T11:51:49Z
date_published: 2014-12-01T00:00:00Z
date_updated: 2023-09-07T11:39:38Z
day: '01'
degree_awarded: PhD
department:
- _id: JiFr
language:
- iso: eng
month: '12'
oa_version: None
page: '90'
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5805'
status: public
supervisor:
- first_name: Jiří
  full_name: Friml, Jiří
  id: 4159519E-F248-11E8-B48F-1D18A9856A87
  last_name: Friml
  orcid: 0000-0002-8302-7596
title: Molecular mechanisms of patterning and subcellular trafficking in Arabidopsis
  thaliana
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2014'
...
---
_id: '1403'
abstract:
- lang: eng
  text: A variety of developmental and disease related processes depend on epithelial
    cell sheet spreading. In order to gain insight into the biophysical mechanism(s)
    underlying the tissue morphogenesis we studied the spreading of an epithelium
    during the early development of the zebrafish embryo. In zebrafish epiboly the
    enveloping cell layer (EVL), a simple squamous epithelium, spreads over the yolk
    cell to completely engulf it at the end of gastrulation. Previous studies have
    proposed that an actomyosin ring forming within the yolk syncytial layer (YSL)
    acts as purse string that through constriction along its circumference pulls on
    the margin of the EVL. Direct biophysical evidence for this hypothesis has however
    been missing. The aim of the thesis was to understand how the actomyosin ring
    may generate pulling forces onto the EVL and what cellular mechanism(s) may facilitate
    the spreading of the epithelium. Using laser ablation to measure cortical tension
    within the actomyosin ring we found an anisotropic tension distribution, which
    was highest along the circumference of the ring. However the low degree of anisotropy
    was incompatible with the actomyosin ring functioning as a purse string only.
    Additionally, we observed retrograde cortical flow from vegetal parts of the ring
    into the EVL margin. Interpreting the experimental data using a theoretical distribution
    that models  the tissues as active viscous gels led us to proposen that the actomyosin
    ring has a twofold contribution to EVL epiboly. It not only acts as a purse string
    through constriction along its circumference, but in addition constriction along
    the width of the ring generates pulling forces through friction-resisted cortical
    flow. Moreover, when rendering the purse string mechanism unproductive EVL epiboly
    proceeded normally indicating that the flow-friction mechanism is sufficient to
    drive the process. Aiming to understand what cellular mechanism(s) may facilitate
    the spreading of the epithelium we found that tension-oriented EVL cell divisions
    limit tissue anisotropy by releasing tension along the division axis and promote
    epithelial spreading. Notably, EVL cells undergo ectopic cell fusion in conditions
    in which oriented-cell division is impaired or the epithelium is mechanically
    challenged. Taken together our study of EVL epiboly suggests a novel mechanism
    of force generation for actomyosin rings through friction-resisted cortical flow
    and highlights the importance of tension-oriented cell divisions in epithelial
    morphogenesis.
acknowledged_ssus:
- _id: SSU
alternative_title:
- IST Austria Thesis
author:
- first_name: Martin
  full_name: Behrndt, Martin
  id: 3ECECA3A-F248-11E8-B48F-1D18A9856A87
  last_name: Behrndt
citation:
  ama: Behrndt M. Forces driving epithelial spreading in zebrafish epiboly. 2014.
  apa: Behrndt, M. (2014). <i>Forces driving epithelial spreading in zebrafish epiboly</i>.
    IST Austria.
  chicago: Behrndt, Martin. “Forces Driving Epithelial Spreading in Zebrafish Epiboly.”
    IST Austria, 2014.
  ieee: M. Behrndt, “Forces driving epithelial spreading in zebrafish epiboly,” IST
    Austria, 2014.
  ista: Behrndt M. 2014. Forces driving epithelial spreading in zebrafish epiboly.
    IST Austria.
  mla: Behrndt, Martin. <i>Forces Driving Epithelial Spreading in Zebrafish Epiboly</i>.
    IST Austria, 2014.
  short: M. Behrndt, Forces Driving Epithelial Spreading in Zebrafish Epiboly, IST
    Austria, 2014.
date_created: 2018-12-11T11:51:49Z
date_published: 2014-08-01T00:00:00Z
date_updated: 2023-10-17T12:16:58Z
day: '01'
department:
- _id: CaHe
language:
- iso: eng
month: '08'
oa_version: None
page: '91'
publication_status: published
publisher: IST Austria
publist_id: '5804'
related_material:
  record:
  - id: '2282'
    relation: part_of_dissertation
    status: public
  - id: '2950'
    relation: part_of_dissertation
    status: public
  - id: '3373'
    relation: part_of_dissertation
    status: public
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: Forces driving epithelial spreading in zebrafish epiboly
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '1404'
abstract:
- lang: eng
  text: "The co-evolution of hosts and pathogens is characterized by continuous adaptations
    of both parties. Pathogens of social insects need to adapt towards disease defences
    at two levels: 1) individual immunity of each colony member consisting of behavioural
    defence strategies as well as humoral and cellular immune responses and 2) social
    immunity that is collectively performed by all group members comprising behavioural,
    physiological and organisational defence strategies.\r\n\r\nTo disentangle the
    selection pressure on pathogens by the collective versus individual level of disease
    defence in social insects, we performed an evolution experiment using the Argentine
    Ant, Linepithema humile, as a host and a mixture of the general insect pathogenic
    fungus Metarhizium spp. (6 strains) as a pathogen. We allowed pathogen evolution
    over 10 serial host passages to two different evolution host treatments: (1) only
    individual host immunity in a single host treatment, and (2) simultaneously acting
    individual and social immunity in a social host treatment, in which an exposed
    ant was accompanied by two untreated nestmates.\r\n\r\nBefore starting the pathogen
    evolution experiment, the 6 Metarhizium spp. strains were characterised concerning
    conidiospore size killing rates in singly and socially reared ants, their competitiveness
    under coinfecting conditions and their influence on ant behaviour. We analysed
    how the ancestral atrain mixture changed in conidiospere size, killing rate and
    strain composition dependent on host treatment (single or social hosts) during
    10 passages and found that killing rate and conidiospere size of the pathogen
    increased under both evolution regimes, but different depending on host treatment.\r\n\r\nTesting
    the evolved strain mixtures that evolved under either the single or social host
    treatment under both single and social current rearing conditions in a full factorial
    design experiment revealed that the additional collective defences in insect societies
    add new selection pressure for their coevolving pathogens that compromise their
    ability to adapt to its host at the group level. To our knowledge, this is the
    first study directly measuring the influence of social immunity on pathogen evolution."
acknowledgement: This work was funded by the DFG and the ERC.
alternative_title:
- IST Austria Thesis
author:
- first_name: Miriam
  full_name: Stock, Miriam
  id: 42462816-F248-11E8-B48F-1D18A9856A87
  last_name: Stock
citation:
  ama: Stock M. Evolution of a fungal pathogen towards individual versus social immunity
    in ants. 2014.
  apa: Stock, M. (2014). <i>Evolution of a fungal pathogen towards individual versus
    social immunity in ants</i>. IST Austria.
  chicago: Stock, Miriam. “Evolution of a Fungal Pathogen towards Individual versus
    Social Immunity in Ants.” IST Austria, 2014.
  ieee: M. Stock, “Evolution of a fungal pathogen towards individual versus social
    immunity in ants,” IST Austria, 2014.
  ista: Stock M. 2014. Evolution of a fungal pathogen towards individual versus social
    immunity in ants. IST Austria.
  mla: Stock, Miriam. <i>Evolution of a Fungal Pathogen towards Individual versus
    Social Immunity in Ants</i>. IST Austria, 2014.
  short: M. Stock, Evolution of a Fungal Pathogen towards Individual versus Social
    Immunity in Ants, IST Austria, 2014.
date_created: 2018-12-11T11:51:49Z
date_published: 2014-04-01T00:00:00Z
date_updated: 2021-01-12T06:50:30Z
day: '01'
department:
- _id: SyCr
language:
- iso: eng
month: '04'
oa_version: None
page: '101'
publication_status: published
publisher: IST Austria
publist_id: '5803'
status: public
supervisor:
- first_name: Sylvia M
  full_name: Cremer, Sylvia M
  id: 2F64EC8C-F248-11E8-B48F-1D18A9856A87
  last_name: Cremer
  orcid: 0000-0002-2193-3868
title: Evolution of a fungal pathogen towards individual versus social immunity in
  ants
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5411'
abstract:
- lang: eng
  text: "Model-based testing is a promising technology for black-box software and
    hardware testing, in which test cases are generated automatically from high-level
    specifications. Nowadays, systems typically consist of multiple interacting components
    and, due to their complexity, testing presents a considerable portion of the effort
    and cost in the design process. Exploiting the compositional structure of system
    specifications can considerably reduce the effort in model-based testing. Moreover,
    inferring properties about the system from testing its individual components allows
    the designer to reduce the amount of integration testing.\r\nIn this paper, we
    study compositional properties of the IOCO-testing theory. We propose a new approach
    to composition and hiding operations, inspired by contract-based design and interface
    theories. These operations preserve behaviors that are compatible under composition
    and hiding, and prune away incompatible ones. The resulting specification characterizes
    the input sequences for which the unit testing of components is sufficient to
    infer the correctness of component integration without the need for further tests.
    We provide a methodology that uses these results to minimize integration testing
    effort, but also to detect potential weaknesses in specifications. While we focus
    on asynchronous models and the IOCO conformance relation, the resulting methodology
    can be applied to a broader class of systems."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Przemyslaw
  full_name: Daca, Przemyslaw
  id: 49351290-F248-11E8-B48F-1D18A9856A87
  last_name: Daca
- 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: Willibald
  full_name: Krenn, Willibald
  last_name: Krenn
- first_name: Dejan
  full_name: Nickovic, Dejan
  id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
  last_name: Nickovic
citation:
  ama: Daca P, Henzinger TA, Krenn W, Nickovic D. <i>Compositional Specifications
    for IOCO Testing</i>. IST Austria; 2014. doi:<a href="https://doi.org/10.15479/AT:IST-2014-148-v2-1">10.15479/AT:IST-2014-148-v2-1</a>
  apa: Daca, P., Henzinger, T. A., Krenn, W., &#38; Nickovic, D. (2014). <i>Compositional
    specifications for IOCO testing</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2014-148-v2-1">https://doi.org/10.15479/AT:IST-2014-148-v2-1</a>
  chicago: Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic.
    <i>Compositional Specifications for IOCO Testing</i>. IST Austria, 2014. <a href="https://doi.org/10.15479/AT:IST-2014-148-v2-1">https://doi.org/10.15479/AT:IST-2014-148-v2-1</a>.
  ieee: P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, <i>Compositional specifications
    for IOCO testing</i>. IST Austria, 2014.
  ista: Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications
    for IOCO testing, IST Austria, 20p.
  mla: Daca, Przemyslaw, et al. <i>Compositional Specifications for IOCO Testing</i>.
    IST Austria, 2014, doi:<a href="https://doi.org/10.15479/AT:IST-2014-148-v2-1">10.15479/AT:IST-2014-148-v2-1</a>.
  short: P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications
    for IOCO Testing, IST Austria, 2014.
date_created: 2018-12-12T11:39:11Z
date_published: 2014-01-28T00:00:00Z
date_updated: 2023-02-23T10:31:07Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2014-148-v2-1
file:
- access_level: open_access
  checksum: 0e03aba625cc334141a3148432aa5760
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:54:21Z
  date_updated: 2020-07-14T12:46:46Z
  file_id: '5543'
  file_name: IST-2014-148-v2+1_main_tr.pdf
  file_size: 534732
  relation: main_file
file_date_updated: 2020-07-14T12:46:46Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '152'
related_material:
  record:
  - id: '2167'
    relation: later_version
    status: public
status: public
title: Compositional specifications for IOCO testing
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5412'
abstract:
- lang: eng
  text: "We consider Markov decision processes (MDPs) which are a standard model for
    probabilistic systems. We focus on qualitative properties for MDPs that can express
    that desired behaviors of the system arise almost-surely (with probability 1)
    or with positive probability.\r\nWe introduce a new simulation relation to capture
    the refinement relation of MDPs with respect to qualitative properties, and present
    discrete graph theoretic algorithms with quadratic complexity to compute the simulation
    relation.\r\nWe present an automated technique for assume-guarantee style reasoning
    for compositional analysis of MDPs with qualitative properties by giving a counter-example
    guided abstraction-refinement approach to compute our new simulation relation.
    We have implemented our algorithms and show that the compositional analysis leads
    to significant improvements. "
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Przemyslaw
  full_name: Daca, Przemyslaw
  id: 49351290-F248-11E8-B48F-1D18A9856A87
  last_name: Daca
- first_name: Martin
  full_name: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
citation:
  ama: Chatterjee K, Daca P, Chmelik M. <i>CEGAR for Qualitative Analysis of Probabilistic
    Systems</i>. IST Austria; 2014. doi:<a href="https://doi.org/10.15479/AT:IST-2014-153-v1-1">10.15479/AT:IST-2014-153-v1-1</a>
  apa: Chatterjee, K., Daca, P., &#38; Chmelik, M. (2014). <i>CEGAR for qualitative
    analysis of probabilistic systems</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2014-153-v1-1">https://doi.org/10.15479/AT:IST-2014-153-v1-1</a>
  chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. <i>CEGAR for
    Qualitative Analysis of Probabilistic Systems</i>. IST Austria, 2014. <a href="https://doi.org/10.15479/AT:IST-2014-153-v1-1">https://doi.org/10.15479/AT:IST-2014-153-v1-1</a>.
  ieee: K. Chatterjee, P. Daca, and M. Chmelik, <i>CEGAR for qualitative analysis
    of probabilistic systems</i>. IST Austria, 2014.
  ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic
    systems, IST Austria, 31p.
  mla: Chatterjee, Krishnendu, et al. <i>CEGAR for Qualitative Analysis of Probabilistic
    Systems</i>. IST Austria, 2014, doi:<a href="https://doi.org/10.15479/AT:IST-2014-153-v1-1">10.15479/AT:IST-2014-153-v1-1</a>.
  short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic
    Systems, IST Austria, 2014.
date_created: 2018-12-12T11:39:11Z
date_published: 2014-01-29T00:00:00Z
date_updated: 2023-02-23T12:25:18Z
day: '29'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-153-v1-1
file:
- access_level: open_access
  checksum: 4d6cda4bebed970926403ad6ad8c745f
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:39Z
  date_updated: 2020-07-14T12:46:47Z
  file_id: '5500'
  file_name: IST-2014-153-v1+1_main.pdf
  file_size: 423322
  relation: main_file
file_date_updated: 2020-07-14T12:46:47Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '31'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '153'
related_material:
  record:
  - id: '2063'
    relation: later_version
    status: public
  - id: '5413'
    relation: later_version
    status: public
  - id: '5414'
    relation: later_version
    status: public
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
