---
_id: '5431'
abstract:
- lang: eng
text: "We consider finite-state concurrent stochastic games, played by k>=2 players
for an infinite number of rounds, where in every round, each player simultaneously
and independently of the other players chooses an action, whereafter the successor
state is determined by a probability distribution given by the current state and
the chosen actions. We consider reachability objectives that given a target set
of states require that some state in the target set is visited, and the dual safety
objectives that given a target set require that only states in the target set
are visited. We are interested in the complexity of stationary strategies measured
by their patience, which is defined as the inverse of the smallest non-zero probability
employed.\r\n\r\n Our main results are as follows: We show that in two-player
zero-sum concurrent stochastic games (with reachability objective for one player
and the complementary safety objective for the other player): (i) the optimal
bound on the patience of optimal and epsilon-optimal strategies, for both players
is doubly exponential; and (ii) even in games with a single non-absorbing state
exponential (in the number of actions) patience is necessary. In general we study
the class of non-zero-sum games admitting epsilon-Nash equilibria. We show that
if there is at least one player with reachability objective, then doubly-exponential
patience is needed in general for epsilon-Nash equilibrium strategies, whereas
in contrast if all players have safety objectives, then the optimal bound on patience
for epsilon-Nash equilibrium strategies is only exponential."
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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Kristoffer
full_name: Hansen, Kristoffer
last_name: Hansen
citation:
ama: Chatterjee K, Ibsen-Jensen R, Hansen K. The Patience of Concurrent Stochastic
Games with Safety and Reachability Objectives. IST Austria; 2015. doi:10.15479/AT:IST-2015-322-v1-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Hansen, K. (2015). The patience
of concurrent stochastic games with safety and reachability objectives. IST
Austria. https://doi.org/10.15479/AT:IST-2015-322-v1-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Kristoffer Hansen. The
Patience of Concurrent Stochastic Games with Safety and Reachability Objectives.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-322-v1-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and K. Hansen, The patience of concurrent
stochastic games with safety and reachability objectives. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Hansen K. 2015. The patience of concurrent stochastic
games with safety and reachability objectives, IST Austria, 25p.
mla: Chatterjee, Krishnendu, et al. The Patience of Concurrent Stochastic Games
with Safety and Reachability Objectives. IST Austria, 2015, doi:10.15479/AT:IST-2015-322-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, K. Hansen, The Patience of Concurrent Stochastic
Games with Safety and Reachability Objectives, IST Austria, 2015.
date_created: 2018-12-12T11:39:17Z
date_published: 2015-02-19T00:00:00Z
date_updated: 2021-01-12T08:02:13Z
day: '19'
ddc:
- '005'
- '519'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-322-v1-1
file:
- access_level: open_access
checksum: bfb858262c30445b8e472c40069178a2
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:31Z
date_updated: 2020-07-14T12:46:53Z
file_id: '5491'
file_name: IST-2015-322-v1+1_safetygames.pdf
file_size: 661015
relation: main_file
file_date_updated: 2020-07-14T12:46:53Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '25'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '322'
status: public
title: The patience of concurrent stochastic games with safety and reachability objectives
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5432'
abstract:
- lang: eng
text: "Evolution occurs in populations of reproducing individuals. The structure
of the population affects the outcome of the evolutionary process. Evolutionary
graph theory is a powerful approach to study this phenomenon. There are two graphs.
The interaction graph specifies who interacts with whom in the context of evolution.The
replacement graph specifies who competes with whom for reproduction. \r\nThe vertices
of the two graphs are the same, and each vertex corresponds to an individual of
the population. A key quantity is the fixation probability of a new mutant. It
is defined as the probability that a newly introduced mutant (on a single vertex)
generates a lineage of offspring which eventually takes over the entire population
of resident individuals. The basic computational questions are as follows: (i)
the qualitative question asks whether the fixation probability is positive; and
(ii) the quantitative approximation question asks for an approximation of the
fixation probability. \r\nOur main results are:\r\n(1) We show that the qualitative
question is NP-complete and the quantitative approximation question is #P-hard
in the special case when the interaction and the replacement graphs coincide and
even with the restriction that the resident individuals do not reproduce (which
corresponds to an invading population taking over an empty structure).\r\n(2)
We show that in general the qualitative question is PSPACE-complete and the quantitative
approximation question is PSPACE-hard and can be solved in exponential time.\r\n"
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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Chatterjee K, Ibsen-Jensen R, Nowak M. The Complexity of Evolutionary Games
on Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-323-v1-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2015). The complexity
of evolutionary games on graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-323-v1-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. The Complexity
of Evolutionary Games on Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-323-v1-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, The complexity of evolutionary
games on graphs. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Nowak M. 2015. The complexity of evolutionary
games on graphs, IST Austria, 29p.
mla: Chatterjee, Krishnendu, et al. The Complexity of Evolutionary Games on Graphs.
IST Austria, 2015, doi:10.15479/AT:IST-2015-323-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, M. Nowak, The Complexity of Evolutionary
Games on Graphs, IST Austria, 2015.
date_created: 2018-12-12T11:39:18Z
date_published: 2015-02-19T00:00:00Z
date_updated: 2023-02-23T12:26:33Z
day: '19'
ddc:
- '005'
- '576'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-323-v1-1
file:
- access_level: open_access
checksum: 546c1b291d545e7b24aaaf4199dac671
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:57Z
date_updated: 2020-07-14T12:46:53Z
file_id: '5519'
file_name: IST-2015-323-v1+1_main.pdf
file_size: 576347
relation: main_file
file_date_updated: 2020-07-14T12:46:53Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '29'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '323'
related_material:
record:
- id: '5421'
relation: earlier_version
status: public
- id: '5440'
relation: later_version
status: public
status: public
title: The complexity of evolutionary games on graphs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5435'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) with multiple limit-average
(or mean-payoff) objectives. \r\nThere have been two different views: (i) the
expectation semantics, where the goal is to optimize the expected mean-payoff
objective, and (ii) the satisfaction semantics, where the goal is to maximize
the probability of runs such that the mean-payoff value stays above a given vector.
\ \r\nWe consider the problem where the goal is to optimize the expectation under
the constraint that the satisfaction semantics is ensured, and thus consider a
generalization that unifies the existing semantics. Our problem captures the notion
of optimization with respect to strategies that are risk-averse (i.e., ensures
certain probabilistic guarantee).\r\nOur main results are algorithms for the decision
problem which are always polynomial in the size of the MDP.\r\nWe also show that
an approximation of the Pareto-curve can be computed in time polynomial in the
size of the MDP, and the approximation factor, but exponential in the number of
dimensions. Finally, we present a complete characterization of the strategy complexity
(in terms of memory bounds and randomization) required to solve our problem."
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: Zuzana
full_name: Komarkova, Zuzana
last_name: Komarkova
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Komarkova Z, Kretinsky J. Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes. IST Austria; 2015. doi:10.15479/AT:IST-2015-318-v2-1
apa: Chatterjee, K., Komarkova, Z., & Kretinsky, J. (2015). Unifying two
views on multiple mean-payoff objectives in Markov decision processes. IST
Austria. https://doi.org/10.15479/AT:IST-2015-318-v2-1
chicago: Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. Unifying
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-318-v2-1.
ieee: K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple
mean-payoff objectives in Markov decision processes. IST Austria, 2015.
ista: Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple
mean-payoff objectives in Markov decision processes, IST Austria, 51p.
mla: Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v2-1.
short: K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple
Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015.
date_created: 2018-12-12T11:39:19Z
date_published: 2015-02-23T00:00:00Z
date_updated: 2023-02-23T12:26:00Z
day: '23'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-318-v2-1
file:
- access_level: open_access
checksum: 75284adec80baabdfe71ff9ebbc27445
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:03Z
date_updated: 2020-07-14T12:46:53Z
file_id: '5525'
file_name: IST-2015-318-v2+1_main.pdf
file_size: 717630
relation: main_file
file_date_updated: 2020-07-14T12:46:53Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '51'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '327'
related_material:
record:
- id: '1657'
relation: later_version
status: public
- id: '466'
relation: later_version
status: public
- id: '5429'
relation: earlier_version
status: public
status: public
title: Unifying two views on multiple mean-payoff objectives in Markov decision processes
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5436'
abstract:
- lang: eng
text: "Recently there has been a significant effort to handle quantitative properties
in formal verification and synthesis. While weighted automata over finite and
infinite words provide a natural and flexible framework to express quantitative
properties, perhaps surprisingly, some basic system properties such as average
response time cannot be expressed using weighted automata, nor in any other know
decidable formalism. In this work, we introduce nested weighted automata as a
natural extension of weighted automata which makes it possible to express important
quantitative properties such as average response time.\r\nIn nested weighted automata,
a master automaton spins off and collects results from weighted slave automata,
each of which computes a quantity along a finite portion of an infinite word.
Nested weighted automata can be viewed as the quantitative analogue of monitor
automata, which are used in run-time verification. We establish an almost complete
decidability picture for the basic decision problems about nested weighted automata,
and illustrate their applicability in several domains. In particular, nested weighted
automata can be used to decide average response time properties."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Otop J. Nested Weighted Automata. IST Austria;
2015. doi:10.15479/AT:IST-2015-170-v2-2
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2015). Nested weighted
automata. IST Austria. https://doi.org/10.15479/AT:IST-2015-170-v2-2
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted
Automata. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-170-v2-2.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata.
IST Austria, 2015.
ista: Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata, IST Austria,
29p.
mla: Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria,
2015, doi:10.15479/AT:IST-2015-170-v2-2.
short: K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria,
2015.
date_created: 2018-12-12T11:39:19Z
date_published: 2015-04-24T00:00:00Z
date_updated: 2023-02-23T12:25:21Z
day: '24'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2015-170-v2-2
file:
- access_level: open_access
checksum: 3c402f47d3669c28d04d1af405a08e3f
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:19Z
date_updated: 2020-07-14T12:46:54Z
file_id: '5541'
file_name: IST-2015-170-v2+2_report.pdf
file_size: 569991
relation: main_file
file_date_updated: 2020-07-14T12:46:54Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '29'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '331'
related_material:
record:
- id: '1656'
relation: later_version
status: public
- id: '467'
relation: later_version
status: public
- id: '5415'
relation: earlier_version
status: public
status: public
title: Nested weighted automata
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5437'
abstract:
- lang: eng
text: "We consider the core algorithmic problems related to verification of systems
with respect to three classical quantitative properties, namely, the mean-payoff
property, the ratio property, and the minimum initial credit for energy property.
\r\nThe algorithmic problem given a graph and a quantitative property asks to
compute the optimal value (the infimum value over all traces) from every node
of the graph. We consider graphs with constant treewidth, and it is well-known
that the control-flow graphs of most programs have constant treewidth. Let $n$
denote the number of nodes of a graph, $m$ the number of edges (for constant treewidth
graphs $m=O(n)$) and $W$ the largest absolute value of the weights.\r\nOur main
theoretical results are as follows.\r\nFirst, for constant treewidth graphs we
present an algorithm that approximates the mean-payoff value within a multiplicative
factor of $\\epsilon$ in time $O(n \\cdot \\log (n/\\epsilon))$ and linear space,
as compared to the classical algorithms that require quadratic time. Second, for
the ratio property we present an algorithm that for constant treewidth graphs
works in time $O(n \\cdot \\log (|a\\cdot b|))=O(n\\cdot\\log (n\\cdot W))$, when
the output is $\\frac{a}{b}$, as compared to the previously best known algorithm
with running time $O(n^2 \\cdot \\log (n\\cdot W))$. Third, for the minimum initial
credit problem we show that (i)~for general graphs the problem can be solved in
$O(n^2\\cdot m)$ time and the associated decision problem can be solved in $O(n\\cdot
m)$ time, improving the previous known $O(n^3\\cdot m\\cdot \\log (n\\cdot W))$
and $O(n^2 \\cdot m)$ bounds, respectively; and (ii)~for constant treewidth graphs
we present an algorithm that requires $O(n\\cdot \\log n)$ time, improving the
previous known $O(n^4 \\cdot \\log (n \\cdot W))$ bound.\r\nWe have implemented
some of our algorithms and show that they present a significant speedup on standard
benchmarks. "
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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster Algorithms for Quantitative
Verification in Constant Treewidth Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-330-v2-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster
algorithms for quantitative verification in constant treewidth graphs. IST
Austria. https://doi.org/10.15479/AT:IST-2015-330-v2-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-330-v2-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Faster algorithms
for quantitative verification in constant treewidth graphs. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for
quantitative verification in constant treewidth graphs, IST Austria, 27p.
mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification
in Constant Treewidth Graphs. IST Austria, 2015, doi:10.15479/AT:IST-2015-330-v2-1.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative
Verification in Constant Treewidth Graphs, IST Austria, 2015.
date_created: 2018-12-12T11:39:19Z
date_published: 2015-04-27T00:00:00Z
date_updated: 2023-02-23T12:26:05Z
day: '27'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-330-v2-1
file:
- access_level: open_access
checksum: f5917c20f84018b362d385c000a2e123
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:12Z
date_updated: 2020-07-14T12:46:54Z
file_id: '5473'
file_name: IST-2015-330-v2+1_main.pdf
file_size: 1072137
relation: main_file
file_date_updated: 2020-07-14T12:46:54Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '27'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '333'
related_material:
record:
- id: '1607'
relation: later_version
status: public
- id: '5430'
relation: earlier_version
status: public
status: public
title: Faster algorithms for quantitative verification in constant treewidth graphs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5438'
abstract:
- lang: eng
text: "The edit distance between two words w1, w2 is the minimal number of word
operations (letter insertions, deletions, and substitutions) necessary to transform
w1 to w2. The edit distance generalizes to languages L1, L2, where the edit distance
is the minimal number k such that for every word from L1 there exists a word in
L2 with edit distance at most k. We study the edit distance computation problem
between pushdown automata and their subclasses.\r\nThe problem of computing edit
distance to a pushdown automaton is undecidable, and in practice, the interesting
question is to compute the edit distance from a pushdown automaton (the implementation,
a standard model for programs with recursion) to a regular language (the specification).
In this work, we present a complete picture of decidability and complexity for
deciding whether, for a given threshold k, the edit distance from a pushdown automaton
to a finite automaton is at most k. "
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit Distance for Pushdown
Automata. IST Austria; 2015. doi:10.15479/AT:IST-2015-334-v1-1
apa: Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., & Otop, J. (2015).
Edit distance for pushdown automata. IST Austria. https://doi.org/10.15479/AT:IST-2015-334-v1-1
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan
Otop. Edit Distance for Pushdown Automata. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-334-v1-1.
ieee: K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, Edit distance
for pushdown automata. IST Austria, 2015.
ista: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for
pushdown automata, IST Austria, 15p.
mla: Chatterjee, Krishnendu, et al. Edit Distance for Pushdown Automata.
IST Austria, 2015, doi:10.15479/AT:IST-2015-334-v1-1.
short: K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Edit Distance for
Pushdown Automata, IST Austria, 2015.
date_created: 2018-12-12T11:39:20Z
date_published: 2015-05-05T00:00:00Z
date_updated: 2023-02-23T12:20:08Z
day: '05'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-334-v1-1
file:
- access_level: open_access
checksum: 8a5f2d77560e552af87eb1982437a43b
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:56Z
date_updated: 2020-07-14T12:46:55Z
file_id: '5518'
file_name: IST-2015-334-v1+1_report.pdf
file_size: 422573
relation: main_file
file_date_updated: 2020-07-14T12:46:55Z
has_accepted_license: '1'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: '15'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '334'
related_material:
record:
- id: '1610'
relation: later_version
status: public
- id: '465'
relation: later_version
status: public
status: public
title: Edit distance for pushdown automata
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5439'
abstract:
- lang: eng
text: 'The target discounted-sum problem is the following: Given a rational discount
factor 0 < λ < 1 and three rational values a, b, and t, does there exist a finite
or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals
t? The problem turns out to relate to many fields of mathematics and computer
science, and its decidability question is surprisingly hard to solve. We solve
the finite version of the problem, and show the hardness of the infinite version,
linking it to various areas and open problems in mathematics and computer science:
β-expansions, discounted-sum automata, piecewise affine maps, and generalizations
of the Cantor set. We provide some partial results to the infinite version, among
which are solutions to its restriction to eventually-periodic sequences and to
the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving
some open problems on discounted-sum automata, among which are the exact-value
problem for nondeterministic automata over finite words and the universality and
inclusion problems for functional automata. '
alternative_title:
- IST Austria Technical Report
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Boker U, Henzinger TA, Otop J. The Target Discounted-Sum Problem. IST
Austria; 2015. doi:10.15479/AT:IST-2015-335-v1-1
apa: Boker, U., Henzinger, T. A., & Otop, J. (2015). The target discounted-sum
problem. IST Austria. https://doi.org/10.15479/AT:IST-2015-335-v1-1
chicago: Boker, Udi, Thomas A Henzinger, and Jan Otop. The Target Discounted-Sum
Problem. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-335-v1-1.
ieee: U. Boker, T. A. Henzinger, and J. Otop, The target discounted-sum problem.
IST Austria, 2015.
ista: Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem, IST
Austria, 20p.
mla: Boker, Udi, et al. The Target Discounted-Sum Problem. IST Austria, 2015,
doi:10.15479/AT:IST-2015-335-v1-1.
short: U. Boker, T.A. Henzinger, J. Otop, The Target Discounted-Sum Problem, IST
Austria, 2015.
date_created: 2018-12-12T11:39:20Z
date_published: 2015-05-18T00:00:00Z
date_updated: 2023-02-23T10:08:48Z
day: '18'
ddc:
- '004'
- '512'
- '513'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2015-335-v1-1
file:
- access_level: open_access
checksum: 40405907aa012acece1bc26cf0be554d
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:55Z
date_updated: 2020-07-14T12:46:55Z
file_id: '5517'
file_name: IST-2015-335-v1+1_report.pdf
file_size: 589619
relation: main_file
file_date_updated: 2020-07-14T12:46:55Z
has_accepted_license: '1'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '335'
related_material:
record:
- id: '1659'
relation: later_version
status: public
status: public
title: The target discounted-sum problem
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5440'
abstract:
- lang: eng
text: 'Evolution occurs in populations of reproducing individuals. The structure
of the population affects the outcome of the evolutionary process. Evolutionary
graph theory is a powerful approach to study this phenomenon. There are two graphs.
The interaction graph specifies who interacts with whom for payoff in the context
of evolution. The replacement graph specifies who competes with whom for reproduction.
The vertices of the two graphs are the same, and each vertex corresponds to an
individual of the population. The fitness (or the reproductive rate) is a non-negative
number, and depends on the payoff. A key quantity is the fixation probability
of a new mutant. It is defined as the probability that a newly introduced mutant
(on a single vertex) generates a lineage of offspring which eventually takes over
the entire population of resident individuals. The basic computational questions
are as follows: (i) the qualitative question asks whether the fixation probability
is positive; and (ii) the quantitative approximation question asks for an approximation
of the fixation probability. Our main results are as follows: First, we consider
a special case of the general problem, where the residents do not reproduce. We
show that the qualitative question is NP-complete, and the quantitative approximation
question is #P-complete, and the hardness results hold even in the special case
where the interaction and the replacement graphs coincide. Second, we show that
in general both the qualitative and the quantitative approximation questions are
PSPACE-complete. The PSPACE-hardness result for quantitative approximation holds
even when the fitness is always positive.'
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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Chatterjee K, Ibsen-Jensen R, Nowak M. The Complexity of Evolutionary Games
on Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-323-v2-2
apa: Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2015). The complexity
of evolutionary games on graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-323-v2-2
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. The Complexity
of Evolutionary Games on Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-323-v2-2.
ieee: K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, The complexity of evolutionary
games on graphs. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Nowak M. 2015. The complexity of evolutionary
games on graphs, IST Austria, 18p.
mla: Chatterjee, Krishnendu, et al. The Complexity of Evolutionary Games on Graphs.
IST Austria, 2015, doi:10.15479/AT:IST-2015-323-v2-2.
short: K. Chatterjee, R. Ibsen-Jensen, M. Nowak, The Complexity of Evolutionary
Games on Graphs, IST Austria, 2015.
date_created: 2018-12-12T11:39:21Z
date_published: 2015-06-16T00:00:00Z
date_updated: 2023-02-23T12:26:10Z
day: '16'
ddc:
- '005'
- '576'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-323-v2-2
file:
- access_level: open_access
checksum: 66aace7d367032af97c15e35c9be9636
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:23Z
date_updated: 2020-07-14T12:46:56Z
file_id: '5484'
file_name: IST-2015-323-v2+2_main.pdf
file_size: 466161
relation: main_file
file_date_updated: 2020-07-14T12:46:56Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: '18'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '338'
related_material:
record:
- id: '5421'
relation: earlier_version
status: public
- id: '5432'
relation: earlier_version
status: public
status: public
title: The complexity of evolutionary games on graphs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5441'
abstract:
- lang: eng
text: We study algorithmic questions for concurrent systems where the transitions
are labeled from a complete, closed semiring, and path properties are algebraic
with semiring operations. The algebraic path properties can model dataflow analysis
problems, the shortest path problem, and many other natural problems that arise
in program analysis. We consider that each component of the concurrent system
is a graph with constant treewidth, a property satisfied by the controlflow graphs
of most programs. We allow for multiple possible queries, which arise naturally
in demand driven dataflow analysis. The study of multiple queries allows us to
consider the tradeoff between the resource usage of the one-time preprocessing
and for each individual query. The traditional approach constructs the product
graph of all components and applies the best-known graph algorithm on the product.
In this approach, even the answer to a single query requires the transitive closure
(i.e., the results of all possible queries), which provides no room for tradeoff
between preprocessing and query time. Our main contributions are algorithms that
significantly improve the worst-case running time of the traditional approach,
and provide various tradeoffs depending on the number of queries. For example,
in a concurrent system of two components, the traditional approach requires hexic
time in the worst case for answering one query as well as computing the transitive
closure, whereas we show that with one-time preprocessing in almost cubic time,
each subsequent query can be answered in at most linear time, and even the transitive
closure can be computed in almost quartic time. Furthermore, we establish conditional
optimality results showing that the worst-case running time of our algorithms
cannot be improved without achieving major breakthroughs in graph algorithms (i.e.,
improving the worst-case bound for the shortest path problem in general graphs).
Preliminary experimental results show that our algorithms perform favorably on
several benchmarks.
alternative_title:
- 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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Amir
full_name: Goharshady, Amir
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms
for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.
IST Austria; 2015. doi:10.15479/AT:IST-2015-340-v1-1
apa: Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., & Pavlogiannis, A.
(2015). Algorithms for algebraic path properties in concurrent systems of constant
treewidth components. IST Austria. https://doi.org/10.15479/AT:IST-2015-340-v1-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady,
and Andreas Pavlogiannis. Algorithms for Algebraic Path Properties in Concurrent
Systems of Constant Treewidth Components. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-340-v1-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, Algorithms
for algebraic path properties in concurrent systems of constant treewidth components.
IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2015. Algorithms
for algebraic path properties in concurrent systems of constant treewidth components,
IST Austria, 24p.
mla: Chatterjee, Krishnendu, et al. Algorithms for Algebraic Path Properties
in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015,
doi:10.15479/AT:IST-2015-340-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, Algorithms
for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components,
IST Austria, 2015.
date_created: 2018-12-12T11:39:21Z
date_published: 2015-07-11T00:00:00Z
date_updated: 2023-09-19T14:36:19Z
day: '11'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-340-v1-1
file:
- access_level: open_access
checksum: df383dc62c94d7b2ea639aba088a76c6
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:09Z
date_updated: 2020-07-14T12:46:56Z
file_id: '5531'
file_name: IST-2015-340-v1+1_main.pdf
file_size: 861396
relation: main_file
file_date_updated: 2020-07-14T12:46:56Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '24'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '340'
related_material:
record:
- id: '1437'
relation: later_version
status: public
- id: '5442'
relation: earlier_version
status: public
- id: '6009'
relation: later_version
status: public
status: public
title: Algorithms for algebraic path properties in concurrent systems of constant
treewidth components
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5443'
abstract:
- lang: eng
text: POMDPs are standard models for probabilistic planning problems, where an agent
interacts with an uncertain environment. We study the problem of almost-sure reachability,
where given a set of target states, the question is to decide whether there is
a policy to ensure that the target set is reached with probability 1 (almost-surely).
While in general the problem is EXPTIME-complete, in many practical cases policies
with a small amount of memory suffice. Moreover, the existing solution to the
problem is explicit, which first requires to construct explicitly an exponential
reduction to a belief-support MDP. In this work, we first study the existence
of observation-stationary strategies, which is NP-complete, and then small-memory
strategies. We present a symbolic algorithm by an efficient encoding to SAT and
using a SAT solver for the problem. We report experimental results demonstrating
the scalability of our symbolic (SAT-based) approach.
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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Jessica
full_name: Davies, Jessica
id: 378E0060-F248-11E8-B48F-1D18A9856A87
last_name: Davies
citation:
ama: Chatterjee K, Chmelik M, Davies J. A Symbolic SAT-Based Algorithm for Almost-Sure
Reachability with Small Strategies in POMDPs. IST Austria; 2015. doi:10.15479/AT:IST-2015-325-v2-1
apa: Chatterjee, K., Chmelik, M., & Davies, J. (2015). A symbolic SAT-based
algorithm for almost-sure reachability with small strategies in POMDPs. IST
Austria. https://doi.org/10.15479/AT:IST-2015-325-v2-1
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. A Symbolic
SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-325-v2-1.
ieee: K. Chatterjee, M. Chmelik, and J. Davies, A symbolic SAT-based algorithm
for almost-sure reachability with small strategies in POMDPs. IST Austria,
2015.
ista: Chatterjee K, Chmelik M, Davies J. 2015. A symbolic SAT-based algorithm for
almost-sure reachability with small strategies in POMDPs, IST Austria, 23p.
mla: Chatterjee, Krishnendu, et al. A Symbolic SAT-Based Algorithm for Almost-Sure
Reachability with Small Strategies in POMDPs. IST Austria, 2015, doi:10.15479/AT:IST-2015-325-v2-1.
short: K. Chatterjee, M. Chmelik, J. Davies, A Symbolic SAT-Based Algorithm for
Almost-Sure Reachability with Small Strategies in POMDPs, IST Austria, 2015.
date_created: 2018-12-12T11:39:22Z
date_published: 2015-11-06T00:00:00Z
date_updated: 2023-02-21T16:24:05Z
day: '06'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-325-v2-1
file:
- access_level: open_access
checksum: f0fa31ad8161ed655137e94012123ef9
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:05Z
date_updated: 2020-07-14T12:46:57Z
file_id: '5466'
file_name: IST-2015-325-v2+1_main.pdf
file_size: 412379
relation: main_file
file_date_updated: 2020-07-14T12:46:57Z
has_accepted_license: '1'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: '23'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '362'
related_material:
record:
- id: '1166'
relation: later_version
status: public
status: public
title: A symbolic SAT-based algorithm for almost-sure reachability with small strategies
in POMDPs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5444'
abstract:
- lang: eng
text: A comprehensive understanding of the clonal evolution of cancer is critical
for understanding neoplasia. Genome-wide sequencing data enables evolutionary
studies at unprecedented depth. However, classical phylogenetic methods often
struggle with noisy sequencing data of impure DNA samples and fail to detect subclones
that have different evolutionary trajectories. We have developed a tool, called
Treeomics, that allows us to reconstruct the phylogeny of a cancer with commonly
available sequencing technologies. Using Bayesian inference and Integer Linear
Programming, robust phylogenies consistent with the biological processes underlying
cancer evolution were obtained for pancreatic, ovarian, and prostate cancers.
Furthermore, Treeomics correctly identified sequencing artifacts such as those
resulting from low statistical power; nearly 7% of variants were misclassified
by conventional statistical methods. These artifacts can skew phylogenies by creating
illusory tumor heterogeneity among distinct samples. Importantly, we show that
the evolutionary trees generated with Treeomics are mathematically optimal.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Johannes
full_name: Reiter, Johannes
id: 4A918E98-F248-11E8-B48F-1D18A9856A87
last_name: Reiter
orcid: 0000-0002-0170-7353
- first_name: Alvin
full_name: Makohon-Moore, Alvin
last_name: Makohon-Moore
- first_name: Jeffrey
full_name: Gerold, Jeffrey
last_name: Gerold
- first_name: Ivana
full_name: Bozic, Ivana
last_name: Bozic
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Christine
full_name: Iacobuzio-Donahue, Christine
last_name: Iacobuzio-Donahue
- first_name: Bert
full_name: Vogelstein, Bert
last_name: Vogelstein
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Reiter J, Makohon-Moore A, Gerold J, et al. Reconstructing Robust Phylogenies
of Metastatic Cancers. IST Austria; 2015. doi:10.15479/AT:IST-2015-399-v1-1
apa: Reiter, J., Makohon-Moore, A., Gerold, J., Bozic, I., Chatterjee, K., Iacobuzio-Donahue,
C., … Nowak, M. (2015). Reconstructing robust phylogenies of metastatic cancers.
IST Austria. https://doi.org/10.15479/AT:IST-2015-399-v1-1
chicago: Reiter, Johannes, Alvin Makohon-Moore, Jeffrey Gerold, Ivana Bozic, Krishnendu
Chatterjee, Christine Iacobuzio-Donahue, Bert Vogelstein, and Martin Nowak. Reconstructing
Robust Phylogenies of Metastatic Cancers. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-399-v1-1.
ieee: J. Reiter et al., Reconstructing robust phylogenies of metastatic
cancers. IST Austria, 2015.
ista: Reiter J, Makohon-Moore A, Gerold J, Bozic I, Chatterjee K, Iacobuzio-Donahue
C, Vogelstein B, Nowak M. 2015. Reconstructing robust phylogenies of metastatic
cancers, IST Austria, 25p.
mla: Reiter, Johannes, et al. Reconstructing Robust Phylogenies of Metastatic
Cancers. IST Austria, 2015, doi:10.15479/AT:IST-2015-399-v1-1.
short: J. Reiter, A. Makohon-Moore, J. Gerold, I. Bozic, K. Chatterjee, C. Iacobuzio-Donahue,
B. Vogelstein, M. Nowak, Reconstructing Robust Phylogenies of Metastatic Cancers,
IST Austria, 2015.
date_created: 2018-12-12T11:39:22Z
date_published: 2015-12-30T00:00:00Z
date_updated: 2020-07-14T23:05:07Z
day: '30'
ddc:
- '000'
- '576'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-399-v1-1
file:
- access_level: open_access
checksum: c47d33bdda06181753c0af36f16e7b5d
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:24Z
date_updated: 2020-07-14T12:46:58Z
file_id: '5485'
file_name: IST-2015-399-v1+1_treeomics.pdf
file_size: 3533200
relation: main_file
file_date_updated: 2020-07-14T12:46:58Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '25'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '399'
status: public
title: Reconstructing robust phylogenies of metastatic cancers
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5549'
abstract:
- lang: eng
text: "This repository contains the experimental part of the CAV 2015 publication
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe
extended the probabilistic model checker PRISM to represent strategies of Markov
Decision Processes as Decision Trees.\r\nThe archive contains a java executable
version of the extended tool (prism_dectree.jar) together with a few examples
of the PRISM benchmark library.\r\nTo execute the program, please have a look
at the README.txt, which provides instructions and further information on the
archive.\r\nThe archive contains scripts that (if run often enough) reproduces
the data presented in the publication."
article_processing_charge: No
author:
- first_name: Andreas
full_name: Fellner, Andreas
id: 42BABFB4-F248-11E8-B48F-1D18A9856A87
last_name: Fellner
citation:
ama: 'Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation
by Learning Small Strategies in Markov Decision Processes. 2015. doi:10.15479/AT:ISTA:28'
apa: 'Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample
Explanation by Learning Small Strategies in Markov Decision Processes. Institute
of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:28'
chicago: 'Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample
Explanation by Learning Small Strategies in Markov Decision Processes.” Institute
of Science and Technology Austria, 2015. https://doi.org/10.15479/AT:ISTA:28.'
ieee: 'A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation
by Learning Small Strategies in Markov Decision Processes.” Institute of Science
and Technology Austria, 2015.'
ista: 'Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample
Explanation by Learning Small Strategies in Markov Decision Processes, Institute
of Science and Technology Austria, 10.15479/AT:ISTA:28.'
mla: 'Fellner, Andreas. Experimental Part of CAV 2015 Publication: Counterexample
Explanation by Learning Small Strategies in Markov Decision Processes. Institute
of Science and Technology Austria, 2015, doi:10.15479/AT:ISTA:28.'
short: A. Fellner, (2015).
contributor:
- first_name: Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
datarep_id: '28'
date_created: 2018-12-12T12:31:29Z
date_published: 2015-08-13T00:00:00Z
date_updated: 2024-02-21T13:52:07Z
day: '13'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:ISTA:28
ec_funded: 1
file:
- access_level: open_access
checksum: b8bcb43c0893023cda66c1b69c16ac62
content_type: application/zip
creator: system
date_created: 2018-12-12T13:02:31Z
date_updated: 2020-07-14T12:47:00Z
file_id: '5597'
file_name: IST-2015-28-v1+2_Fellner_DataRep.zip
file_size: 49557109
relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
keyword:
- Markov Decision Process
- Decision Tree
- Probabilistic Verification
- Counterexample Explanation
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publisher: Institute of Science and Technology Austria
publist_id: '5564'
related_material:
record:
- id: '1603'
relation: popular_science
status: public
status: public
title: 'Experimental part of CAV 2015 publication: Counterexample Explanation by Learning
Small Strategies in Markov Decision Processes'
tmp:
image: /images/cc_0.png
legal_code_url: https://creativecommons.org/publicdomain/zero/1.0/legalcode
name: Creative Commons Public Domain Dedication (CC0 1.0)
short: CC0 (1.0)
type: research_data
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1474'
abstract:
- lang: eng
text: Cryptographic access control offers selective access to encrypted data via
a combination of key management and functionality-rich cryptographic schemes,
such as attribute-based encryption. Using this approach, publicly available meta-data
may inadvertently leak information on the access policy that is enforced by cryptography,
which renders cryptographic access control unusable in settings where this information
is highly sensitive. We begin to address this problem by presenting rigorous definitions
for policy privacy in cryptographic access control. For concreteness we set our
results in the model of Role-Based Access Control (RBAC), where we identify and
formalize several different flavors of privacy, however, our framework should
serve as inspiration for other models of access control. Based on our insights
we propose a new system which significantly improves on the privacy properties
of state-of-the-art constructions. Our design is based on a novel type of privacy-preserving
attribute-based encryption, which we introduce and show how to instantiate. We
present our results in the context of a cryptographic RBAC system by Ferrara et
al. (CSF'13), which uses cryptography to control read access to files, while write
access is still delegated to trusted monitors. We give an extension of the construction
that permits cryptographic control over write access. Our construction assumes
that key management uses out-of-band channels between the policy enforcer and
the users but eliminates completely the need for monitoring read/write access
to the data.
article_processing_charge: No
author:
- first_name: Anna
full_name: Ferrara, Anna
last_name: Ferrara
- first_name: Georg
full_name: Fuchsbauer, Georg
id: 46B4C3EE-F248-11E8-B48F-1D18A9856A87
last_name: Fuchsbauer
- first_name: Bin
full_name: Liu, Bin
last_name: Liu
- first_name: Bogdan
full_name: Warinschi, Bogdan
last_name: Warinschi
citation:
ama: 'Ferrara A, Fuchsbauer G, Liu B, Warinschi B. Policy privacy in cryptographic
access control. In: IEEE; 2015:46-60. doi:10.1109/CSF.2015.11'
apa: 'Ferrara, A., Fuchsbauer, G., Liu, B., & Warinschi, B. (2015). Policy privacy
in cryptographic access control (pp. 46–60). Presented at the CSF: Computer Security
Foundations, Verona, Italy: IEEE. https://doi.org/10.1109/CSF.2015.11'
chicago: Ferrara, Anna, Georg Fuchsbauer, Bin Liu, and Bogdan Warinschi. “Policy
Privacy in Cryptographic Access Control,” 46–60. IEEE, 2015. https://doi.org/10.1109/CSF.2015.11.
ieee: 'A. Ferrara, G. Fuchsbauer, B. Liu, and B. Warinschi, “Policy privacy in cryptographic
access control,” presented at the CSF: Computer Security Foundations, Verona,
Italy, 2015, pp. 46–60.'
ista: 'Ferrara A, Fuchsbauer G, Liu B, Warinschi B. 2015. Policy privacy in cryptographic
access control. CSF: Computer Security Foundations, 46–60.'
mla: Ferrara, Anna, et al. Policy Privacy in Cryptographic Access Control.
IEEE, 2015, pp. 46–60, doi:10.1109/CSF.2015.11.
short: A. Ferrara, G. Fuchsbauer, B. Liu, B. Warinschi, in:, IEEE, 2015, pp. 46–60.
conference:
end_date: 2015-07-17
location: Verona, Italy
name: 'CSF: Computer Security Foundations'
start_date: 2015-07-13
date_created: 2018-12-11T11:52:14Z
date_published: 2015-09-04T00:00:00Z
date_updated: 2021-01-12T06:50:59Z
day: '04'
department:
- _id: KrPi
doi: 10.1109/CSF.2015.11
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://epubs.surrey.ac.uk/808055/
month: '09'
oa: 1
oa_version: Submitted Version
page: 46-60
project:
- _id: 258C570E-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '259668'
name: Provable Security for Physical Cryptography
publication_status: published
publisher: IEEE
publist_id: '5722'
quality_controlled: '1'
status: public
title: Policy privacy in cryptographic access control
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1481'
abstract:
- lang: eng
text: 'Simple board games, like Tic-Tac-Toe and CONNECT-4, play an important role
not only in the development of mathematical and logical skills, but also in the
emotional and social development. In this paper, we address the problem of generating
targeted starting positions for such games. This can facilitate new approaches
for bringing novice players to mastery, and also leads to discovery of interesting
game variants. We present an approach that generates starting states of varying
hardness levels for player 1 in a two-player board game, given rules of the board
game, the desired number of steps required for player 1 to win, and the expertise
levels of the two players. Our approach leverages symbolic methods and iterative
simulation to efficiently search the extremely large state space. We present experimental
results that include discovery of states of varying hardness levels for several
simple grid-based board games. The presence of such states for standard game variants
like 4×4 Tic-Tac-Toe opens up new games to be played that have never been played
as the default start state is heavily biased. '
acknowledgement: "A Technical Report of this paper is available at: \r\nhttps://repository.ist.ac.at/id/eprint/146.\r\n"
article_processing_charge: No
author:
- first_name: Umair
full_name: Ahmed, Umair
last_name: Ahmed
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Sumit
full_name: Gulwani, Sumit
last_name: Gulwani
citation:
ama: 'Ahmed U, Chatterjee K, Gulwani S. Automatic generation of alternative starting
positions for simple traditional board games. In: Proceedings of the Twenty-Ninth
AAAI Conference on Artificial Intelligence. Vol 2. AAAI Press; 2015:745-752.'
apa: 'Ahmed, U., Chatterjee, K., & Gulwani, S. (2015). Automatic generation
of alternative starting positions for simple traditional board games. In Proceedings
of the Twenty-Ninth AAAI Conference on Artificial Intelligence (Vol. 2, pp.
745–752). Austin, TX, USA: AAAI Press.'
chicago: Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. “Automatic Generation
of Alternative Starting Positions for Simple Traditional Board Games.” In Proceedings
of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2:745–52.
AAAI Press, 2015.
ieee: U. Ahmed, K. Chatterjee, and S. Gulwani, “Automatic generation of alternative
starting positions for simple traditional board games,” in Proceedings of the
Twenty-Ninth AAAI Conference on Artificial Intelligence, Austin, TX, USA,
2015, vol. 2, pp. 745–752.
ista: 'Ahmed U, Chatterjee K, Gulwani S. 2015. Automatic generation of alternative
starting positions for simple traditional board games. Proceedings of the Twenty-Ninth
AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence
vol. 2, 745–752.'
mla: Ahmed, Umair, et al. “Automatic Generation of Alternative Starting Positions
for Simple Traditional Board Games.” Proceedings of the Twenty-Ninth AAAI Conference
on Artificial Intelligence, vol. 2, AAAI Press, 2015, pp. 745–52.
short: U. Ahmed, K. Chatterjee, S. Gulwani, in:, Proceedings of the Twenty-Ninth
AAAI Conference on Artificial Intelligence, AAAI Press, 2015, pp. 745–752.
conference:
end_date: 2015-01-30
location: Austin, TX, USA
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2015-01-25
date_created: 2018-12-11T11:52:16Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2023-02-23T12:25:07Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
intvolume: ' 2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/download/9523/9300
month: '01'
oa: 1
oa_version: None
page: 745 - 752
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence
publication_status: published
publisher: AAAI Press
publist_id: '5713'
quality_controlled: '1'
related_material:
record:
- id: '5410'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Automatic generation of alternative starting positions for simple traditional
board games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2015'
...
---
_id: '1483'
abstract:
- lang: eng
text: Topological data analysis offers a rich source of valuable information to
study vision problems. Yet, so far we lack a theoretically sound connection to
popular kernel-based learning techniques, such as kernel SVMs or kernel PCA. In
this work, we establish such a connection by designing a multi-scale kernel for
persistence diagrams, a stable summary representation of topological features
in data. We show that this kernel is positive definite and prove its stability
with respect to the 1-Wasserstein distance. Experiments on two benchmark datasets
for 3D shape classification/retrieval and texture recognition show considerable
performance gains of the proposed method compared to an alternative approach that
is based on the recently introduced persistence landscapes.
author:
- first_name: Jan
full_name: Reininghaus, Jan
id: 4505473A-F248-11E8-B48F-1D18A9856A87
last_name: Reininghaus
- first_name: Stefan
full_name: Huber, Stefan
id: 4700A070-F248-11E8-B48F-1D18A9856A87
last_name: Huber
orcid: 0000-0002-8871-5814
- first_name: Ulrich
full_name: Bauer, Ulrich
id: 2ADD483A-F248-11E8-B48F-1D18A9856A87
last_name: Bauer
orcid: 0000-0002-9683-0724
- first_name: Roland
full_name: Kwitt, Roland
last_name: Kwitt
citation:
ama: 'Reininghaus J, Huber S, Bauer U, Kwitt R. A stable multi-scale kernel for
topological machine learning. In: IEEE; 2015:4741-4748. doi:10.1109/CVPR.2015.7299106'
apa: 'Reininghaus, J., Huber, S., Bauer, U., & Kwitt, R. (2015). A stable multi-scale
kernel for topological machine learning (pp. 4741–4748). Presented at the CVPR:
Computer Vision and Pattern Recognition, Boston, MA, USA: IEEE. https://doi.org/10.1109/CVPR.2015.7299106'
chicago: Reininghaus, Jan, Stefan Huber, Ulrich Bauer, and Roland Kwitt. “A Stable
Multi-Scale Kernel for Topological Machine Learning,” 4741–48. IEEE, 2015. https://doi.org/10.1109/CVPR.2015.7299106.
ieee: 'J. Reininghaus, S. Huber, U. Bauer, and R. Kwitt, “A stable multi-scale kernel
for topological machine learning,” presented at the CVPR: Computer Vision and
Pattern Recognition, Boston, MA, USA, 2015, pp. 4741–4748.'
ista: 'Reininghaus J, Huber S, Bauer U, Kwitt R. 2015. A stable multi-scale kernel
for topological machine learning. CVPR: Computer Vision and Pattern Recognition,
4741–4748.'
mla: Reininghaus, Jan, et al. A Stable Multi-Scale Kernel for Topological Machine
Learning. IEEE, 2015, pp. 4741–48, doi:10.1109/CVPR.2015.7299106.
short: J. Reininghaus, S. Huber, U. Bauer, R. Kwitt, in:, IEEE, 2015, pp. 4741–4748.
conference:
end_date: 2015-06-12
location: Boston, MA, USA
name: 'CVPR: Computer Vision and Pattern Recognition'
start_date: 2015-06-07
date_created: 2018-12-11T11:52:17Z
date_published: 2015-10-14T00:00:00Z
date_updated: 2021-01-12T06:51:03Z
day: '14'
department:
- _id: HeEd
doi: 10.1109/CVPR.2015.7299106
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1412.6821
month: '10'
oa: 1
oa_version: Preprint
page: 4741 - 4748
publication_identifier:
eisbn:
- '978-1-4673-6964-0 '
publication_status: published
publisher: IEEE
publist_id: '5709'
scopus_import: 1
status: public
title: A stable multi-scale kernel for topological machine learning
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1495'
abstract:
- lang: eng
text: 'Motivated by biological questions, we study configurations of equal-sized
disks in the Euclidean plane that neither pack nor cover. Measuring the quality
by the probability that a random point lies in exactly one disk, we show that
the regular hexagonal grid gives the maximum among lattice configurations. '
author:
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Mabel
full_name: Iglesias Ham, Mabel
id: 41B58C0C-F248-11E8-B48F-1D18A9856A87
last_name: Iglesias Ham
- first_name: Vitaliy
full_name: Kurlin, Vitaliy
last_name: Kurlin
citation:
ama: 'Edelsbrunner H, Iglesias Ham M, Kurlin V. Relaxed disk packing. In: Proceedings
of the 27th Canadian Conference on Computational Geometry. Vol 2015-August.
Queen’s University; 2015:128-135.'
apa: 'Edelsbrunner, H., Iglesias Ham, M., & Kurlin, V. (2015). Relaxed disk
packing. In Proceedings of the 27th Canadian Conference on Computational Geometry
(Vol. 2015–August, pp. 128–135). Ontario, Canada: Queen’s University.'
chicago: Edelsbrunner, Herbert, Mabel Iglesias Ham, and Vitaliy Kurlin. “Relaxed
Disk Packing.” In Proceedings of the 27th Canadian Conference on Computational
Geometry, 2015–August:128–35. Queen’s University, 2015.
ieee: H. Edelsbrunner, M. Iglesias Ham, and V. Kurlin, “Relaxed disk packing,” in
Proceedings of the 27th Canadian Conference on Computational Geometry,
Ontario, Canada, 2015, vol. 2015–August, pp. 128–135.
ista: 'Edelsbrunner H, Iglesias Ham M, Kurlin V. 2015. Relaxed disk packing. Proceedings
of the 27th Canadian Conference on Computational Geometry. CCCG: Canadian Conference
on Computational Geometry vol. 2015–August, 128–135.'
mla: Edelsbrunner, Herbert, et al. “Relaxed Disk Packing.” Proceedings of the
27th Canadian Conference on Computational Geometry, vol. 2015–August, Queen’s
University, 2015, pp. 128–35.
short: H. Edelsbrunner, M. Iglesias Ham, V. Kurlin, in:, Proceedings of the 27th
Canadian Conference on Computational Geometry, Queen’s University, 2015, pp. 128–135.
conference:
end_date: 2015-08-12
location: Ontario, Canada
name: 'CCCG: Canadian Conference on Computational Geometry'
start_date: 2015-08-10
date_created: 2018-12-11T11:52:21Z
date_published: 2015-08-01T00:00:00Z
date_updated: 2021-01-12T06:51:09Z
day: '01'
department:
- _id: HeEd
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1505.03402
month: '08'
oa: 1
oa_version: Submitted Version
page: 128-135
project:
- _id: 255D761E-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '318493'
name: Topological Complex Systems
publication: Proceedings of the 27th Canadian Conference on Computational Geometry
publication_status: published
publisher: Queen's University
publist_id: '5684'
quality_controlled: '1'
scopus_import: 1
status: public
title: Relaxed disk packing
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 2015-August
year: '2015'
...
---
_id: '1497'
abstract:
- lang: eng
text: Detecting allelic biases from high-throughput sequencing data requires an
approach that maximises sensitivity while minimizing false positives. Here, we
present Allelome.PRO, an automated user-friendly bioinformatics pipeline, which
uses high-throughput sequencing data from reciprocal crosses of two genetically
distinct mouse strains to detect allele-specific expression and chromatin modifications.
Allelome.PRO extends approaches used in previous studies that exclusively analyzed
imprinted expression to give a complete picture of the ‘allelome’ by automatically
categorising the allelic expression of all genes in a given cell type into imprinted,
strain-biased, biallelic or non-informative. Allelome.PRO offers increased sensitivity
to analyze lowly expressed transcripts, together with a robust false discovery
rate empirically calculated from variation in the sequencing data. We used RNA-seq
data from mouse embryonic fibroblasts from F1 reciprocal crosses to determine
a biologically relevant allelic ratio cutoff, and define for the first time an
entire allelome. Furthermore, we show that Allelome.PRO detects differential enrichment
of H3K4me3 over promoters from ChIP-seq data validating the RNA-seq results. This
approach can be easily extended to analyze histone marks of active enhancers,
or transcription factor binding sites and therefore provides a powerful tool to
identify candidate cis regulatory elements genome wide.
acknowledgement: "Austrian Science Fund [FWF P25185-B22, FWF F4302- B09, FWFW1207-B09].
Funding for open access charge: Austrian Science Fund.\r\nWe thank Florian Breitwieser
for advice during the early stages of this project. High-throughput sequencing was
conducted by the Biomedical Sequencing Facility (BSF) at CeMM in Vienna."
article_number: e146
author:
- first_name: Daniel
full_name: Andergassen, Daniel
last_name: Andergassen
- first_name: Christoph
full_name: Dotter, Christoph
id: 4C66542E-F248-11E8-B48F-1D18A9856A87
last_name: Dotter
- first_name: Tomasz
full_name: Kulinski, Tomasz
last_name: Kulinski
- first_name: Philipp
full_name: Guenzl, Philipp
last_name: Guenzl
- first_name: Philipp
full_name: Bammer, Philipp
last_name: Bammer
- first_name: Denise
full_name: Barlow, Denise
last_name: Barlow
- first_name: Florian
full_name: Pauler, Florian
last_name: Pauler
- first_name: Quanah
full_name: Hudson, Quanah
last_name: Hudson
citation:
ama: Andergassen D, Dotter C, Kulinski T, et al. Allelome.PRO, a pipeline to define
allele-specific genomic features from high-throughput sequencing data. Nucleic
Acids Research. 2015;43(21). doi:10.1093/nar/gkv727
apa: Andergassen, D., Dotter, C., Kulinski, T., Guenzl, P., Bammer, P., Barlow,
D., … Hudson, Q. (2015). Allelome.PRO, a pipeline to define allele-specific genomic
features from high-throughput sequencing data. Nucleic Acids Research.
Oxford University Press. https://doi.org/10.1093/nar/gkv727
chicago: Andergassen, Daniel, Christoph Dotter, Tomasz Kulinski, Philipp Guenzl,
Philipp Bammer, Denise Barlow, Florian Pauler, and Quanah Hudson. “Allelome.PRO,
a Pipeline to Define Allele-Specific Genomic Features from High-Throughput Sequencing
Data.” Nucleic Acids Research. Oxford University Press, 2015. https://doi.org/10.1093/nar/gkv727.
ieee: D. Andergassen et al., “Allelome.PRO, a pipeline to define allele-specific
genomic features from high-throughput sequencing data,” Nucleic Acids Research,
vol. 43, no. 21. Oxford University Press, 2015.
ista: Andergassen D, Dotter C, Kulinski T, Guenzl P, Bammer P, Barlow D, Pauler
F, Hudson Q. 2015. Allelome.PRO, a pipeline to define allele-specific genomic
features from high-throughput sequencing data. Nucleic Acids Research. 43(21),
e146.
mla: Andergassen, Daniel, et al. “Allelome.PRO, a Pipeline to Define Allele-Specific
Genomic Features from High-Throughput Sequencing Data.” Nucleic Acids Research,
vol. 43, no. 21, e146, Oxford University Press, 2015, doi:10.1093/nar/gkv727.
short: D. Andergassen, C. Dotter, T. Kulinski, P. Guenzl, P. Bammer, D. Barlow,
F. Pauler, Q. Hudson, Nucleic Acids Research 43 (2015).
date_created: 2018-12-11T11:52:22Z
date_published: 2015-07-21T00:00:00Z
date_updated: 2021-01-12T06:51:09Z
day: '21'
ddc:
- '570'
department:
- _id: GaNo
doi: 10.1093/nar/gkv727
file:
- access_level: open_access
checksum: 385b83854fd0eb2e4f386867da2823e2
content_type: application/pdf
creator: dernst
date_created: 2018-12-20T14:18:57Z
date_updated: 2020-07-14T12:44:58Z
file_id: '5768'
file_name: 2015_NucleicAcidsRes_Andergassen.pdf
file_size: 6863297
relation: main_file
file_date_updated: 2020-07-14T12:44:58Z
has_accepted_license: '1'
intvolume: ' 43'
issue: '21'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
publication: Nucleic Acids Research
publication_status: published
publisher: Oxford University Press
publist_id: '5682'
quality_controlled: '1'
scopus_import: 1
status: public
title: Allelome.PRO, a pipeline to define allele-specific genomic features from high-throughput
sequencing data
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 43
year: '2015'
...
---
_id: '1498'
abstract:
- lang: eng
text: Fault-tolerant distributed algorithms play an important role in many critical/high-availability
applications. These algorithms are notoriously difficult to implement correctly,
due to asynchronous communication and the occurrence of faults, such as the network
dropping messages or computers crashing. Nonetheless there is surprisingly little
language and verification support to build distributed systems based on fault-tolerant
algorithms. In this paper, we present some of the challenges that a designer has
to overcome to implement a fault-tolerant distributed system. Then we review different
models that have been proposed to reason about distributed algorithms and sketch
how such a model can form the basis for a domain-specific programming language.
Adopting a high-level programming model can simplify the programmer's life and
make the code amenable to automated verification, while still compiling to efficiently
executable code. We conclude by summarizing the current status of an ongoing language
design and implementation project that is based on this idea.
alternative_title:
- LIPIcs
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: 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, Zufferey D. The need for language support for fault-tolerant
distributed systems. 2015;32:90-102. doi:10.4230/LIPIcs.SNAPL.2015.90
apa: 'Dragoi, C., Henzinger, T. A., & Zufferey, D. (2015). The need for language
support for fault-tolerant distributed systems. Presented at the SNAPL: Summit
oN Advances in Programming Languages, Asilomar, CA, United States: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SNAPL.2015.90'
chicago: Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “The Need for
Language Support for Fault-Tolerant Distributed Systems.” Leibniz International
Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2015. https://doi.org/10.4230/LIPIcs.SNAPL.2015.90.
ieee: C. Dragoi, T. A. Henzinger, and D. Zufferey, “The need for language support
for fault-tolerant distributed systems,” vol. 32. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, pp. 90–102, 2015.
ista: Dragoi C, Henzinger TA, Zufferey D. 2015. The need for language support for
fault-tolerant distributed systems. 32, 90–102.
mla: Dragoi, Cezara, et al. The Need for Language Support for Fault-Tolerant
Distributed Systems. Vol. 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2015, pp. 90–102, doi:10.4230/LIPIcs.SNAPL.2015.90.
short: C. Dragoi, T.A. Henzinger, D. Zufferey, 32 (2015) 90–102.
conference:
end_date: 2015-05-06
location: Asilomar, CA, United States
name: 'SNAPL: Summit oN Advances in Programming Languages'
start_date: 2015-05-03
date_created: 2018-12-11T11:52:22Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2020-08-11T10:09:14Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.SNAPL.2015.90
ec_funded: 1
file:
- access_level: open_access
checksum: cf5e94baa89a2dc4c5de01abc676eda8
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:02Z
date_updated: 2020-07-14T12:44:58Z
file_id: '5050'
file_name: IST-2016-499-v1+1_9.pdf
file_size: 489362
relation: main_file
file_date_updated: 2020-07-14T12:44:58Z
has_accepted_license: '1'
intvolume: ' 32'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 90 - 102
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
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
isbn:
- '978-3-939897-80-4 '
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5681'
pubrep_id: '499'
quality_controlled: '1'
scopus_import: 1
series_title: Leibniz International Proceedings in Informatics
status: public
title: The need for language support for fault-tolerant distributed systems
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 32
year: '2015'
...
---
_id: '1499'
abstract:
- lang: eng
text: "We consider weighted automata with both positive and negative integer weights
on edges and\r\nstudy the problem of synchronization using adaptive strategies
that may only observe whether\r\nthe current weight-level is negative or nonnegative.
We show that the synchronization problem is decidable in polynomial time for deterministic
weighted automata."
acknowledgement: "The research leading to these results has received funding from
the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement
601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center
IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM),
the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein
Award), the Czech Science Foundation under grant agreement P202/12/G061, and People
Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme
(FP7/2007-2013) REA Grant No 291734."
alternative_title:
- LIPIcs
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Kim
full_name: Larsen, Kim
last_name: Larsen
- first_name: Simon
full_name: Laursen, Simon
last_name: Laursen
- first_name: Jiří
full_name: Srba, Jiří
last_name: Srba
citation:
ama: 'Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of
weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2015:142-154. doi:10.4230/LIPIcs.CONCUR.2015.142'
apa: 'Kretinsky, J., Larsen, K., Laursen, S., & Srba, J. (2015). Polynomial
time decidability of weighted synchronization under partial observability (Vol.
42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142'
chicago: Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time
Decidability of Weighted Synchronization under Partial Observability,” 42:142–54.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142.
ieee: 'J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability
of weighted synchronization under partial observability,” presented at the CONCUR:
Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.'
ista: 'Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability
of weighted synchronization under partial observability. CONCUR: Concurrency Theory,
LIPIcs, vol. 42, 142–154.'
mla: Kretinsky, Jan, et al. Polynomial Time Decidability of Weighted Synchronization
under Partial Observability. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2015, pp. 142–54, doi:10.4230/LIPIcs.CONCUR.2015.142.
short: J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2015, pp. 142–154.
conference:
end_date: 2015-09-04
location: Madrid, Spain
name: 'CONCUR: Concurrency Theory'
start_date: 2015-09-01
date_created: 2018-12-11T11:52:22Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2021-01-12T06:51:10Z
day: '01'
ddc:
- '000'
- '003'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2015.142
ec_funded: 1
file:
- access_level: open_access
checksum: 49eb5021caafaabe5356c65b9c5f8c9c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:12Z
date_updated: 2020-07-14T12:44:58Z
file_id: '4672'
file_name: IST-2016-498-v1+1_32.pdf
file_size: 623563
relation: main_file
file_date_updated: 2020-07-14T12:44:58Z
has_accepted_license: '1'
intvolume: ' 42'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 142 - 154
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
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5680'
pubrep_id: '498'
quality_controlled: '1'
scopus_import: 1
status: public
title: Polynomial time decidability of weighted synchronization under partial observability
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 42
year: '2015'
...
---
_id: '1501'
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. We introduce a new simulation relation to capture
the refinement relation of MDPs with respect to qualitative properties, and present
discrete graph algorithms with quadratic complexity to compute the simulation
relation. We present an automated technique for assume-guarantee style reasoning
for compositional analysis of two-player games by giving a counterexample guided
abstraction-refinement approach to compute our new simulation relation. We show
a tight link between two-player games and MDPs, and as a consequence the results
for games are lifted to MDPs with qualitative properties. We have implemented
our algorithms and show that the compositional analysis leads to significant improvements. '
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE),
and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games),
Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive
Modeling).'
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 compositional analysis of qualitative
properties in Markov decision processes. Formal Methods in System Design.
2015;47(2):230-264. doi:10.1007/s10703-015-0235-2
apa: Chatterjee, K., Chmelik, M., & Daca, P. (2015). CEGAR for compositional
analysis of qualitative properties in Markov decision processes. Formal Methods
in System Design. Springer. https://doi.org/10.1007/s10703-015-0235-2
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for
Compositional Analysis of Qualitative Properties in Markov Decision Processes.”
Formal Methods in System Design. Springer, 2015. https://doi.org/10.1007/s10703-015-0235-2.
ieee: K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis
of qualitative properties in Markov decision processes,” Formal Methods in
System Design, vol. 47, no. 2. Springer, pp. 230–264, 2015.
ista: Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of
qualitative properties in Markov decision processes. Formal Methods in System
Design. 47(2), 230–264.
mla: Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative
Properties in Markov Decision Processes.” Formal Methods in System Design,
vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:10.1007/s10703-015-0235-2.
short: K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015)
230–264.
date_created: 2018-12-11T11:52:23Z
date_published: 2015-10-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10703-015-0235-2
ec_funded: 1
intvolume: ' 47'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1405.0835
month: '10'
oa: 1
oa_version: Preprint
page: 230 - 264
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 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: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '5677'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: CEGAR for compositional analysis of qualitative properties in Markov decision
processes
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 47
year: '2015'
...