---
_id: '5423'
abstract:
- lang: eng
text: 'We present a flexible framework for the automated competitive analysis of
on-line scheduling algorithms for firm- deadline real-time tasks based on multi-objective
graphs: Given a taskset and an on-line scheduling algorithm specified as a labeled
transition system, along with some optional safety, liveness, and/or limit-average
constraints for the adversary, we automatically compute the competitive ratio
of the algorithm w.r.t. a clairvoyant scheduler. We demonstrate the flexibility
and power of our approach by comparing the competitive ratio of several on-line
algorithms, including D(over), that have been proposed in the past, for various
tasksets. Our experimental results reveal that none of these algorithms is universally
optimal, in the sense that there are tasksets where other schedulers provide better
performance. Our framework is hence a very useful design tool for selecting optimal
algorithms for a given application. '
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: Alexander
full_name: Kössler, Alexander
last_name: Kössler
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Ulrich
full_name: Schmid, Ulrich
last_name: Schmid
citation:
ama: Chatterjee K, Kössler A, Pavlogiannis A, Schmid U. A Framework for Automated
Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks. IST Austria;
2014. doi:10.15479/AT:IST-2014-300-v1-1
apa: Chatterjee, K., Kössler, A., Pavlogiannis, A., & Schmid, U. (2014). A
framework for automated competitive analysis of on-line scheduling of firm-deadline
tasks. IST Austria. https://doi.org/10.15479/AT:IST-2014-300-v1-1
chicago: Chatterjee, Krishnendu, Alexander Kössler, Andreas Pavlogiannis, and Ulrich
Schmid. A Framework for Automated Competitive Analysis of On-Line Scheduling
of Firm-Deadline Tasks. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-300-v1-1.
ieee: K. Chatterjee, A. Kössler, A. Pavlogiannis, and U. Schmid, A framework
for automated competitive analysis of on-line scheduling of firm-deadline tasks.
IST Austria, 2014.
ista: Chatterjee K, Kössler A, Pavlogiannis A, Schmid U. 2014. A framework for automated
competitive analysis of on-line scheduling of firm-deadline tasks, IST Austria,
14p.
mla: Chatterjee, Krishnendu, et al. A Framework for Automated Competitive Analysis
of On-Line Scheduling of Firm-Deadline Tasks. IST Austria, 2014, doi:10.15479/AT:IST-2014-300-v1-1.
short: K. Chatterjee, A. Kössler, A. Pavlogiannis, U. Schmid, A Framework for Automated
Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks, IST Austria,
2014.
date_created: 2018-12-12T11:39:15Z
date_published: 2014-07-29T00:00:00Z
date_updated: 2023-02-23T10:11:15Z
day: '29'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-300-v1-1
file:
- access_level: open_access
checksum: 4b8fde4d9ef6653837f6803921d83032
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:53Z
date_updated: 2020-07-14T12:46:50Z
file_id: '5514'
file_name: IST-2014-300-v1+1_main.pdf
file_size: 1270021
relation: main_file
file_date_updated: 2020-07-14T12:46:50Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '14'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '300'
related_material:
record:
- id: '1714'
relation: later_version
status: public
status: public
title: A framework for automated competitive analysis of on-line scheduling of firm-deadline
tasks
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5424'
abstract:
- lang: eng
text: We consider partially observable Markov decision processes (POMDPs), that
are a standard framework for robotics applications to model uncertainties present
in the real world, with temporal logic specifications. All temporal logic specifications
in linear-time temporal logic (LTL) can be expressed as parity objectives. We
study the qualitative analysis problem for POMDPs with parity objectives that
asks whether there is a controller (policy) to ensure that the objective holds
with probability 1 (almost-surely). While the qualitative analysis of POMDPs with
parity objectives is undecidable, recent results show that when restricted to
finite-memory policies the problem is EXPTIME-complete. While the problem is intractable
in theory, we present a practical approach to solve the qualitative analysis problem.
We designed several heuristics to deal with the exponential complexity, and have
used our implementation on a number of well-known POMDP examples for robotics
applications. Our results provide the first practical approach to solve the qualitative
analysis of robot motion planning with LTL properties in the presence of uncertainty.
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: Raghav
full_name: Gupta, Raghav
last_name: Gupta
- first_name: Ayush
full_name: Kanodia, Ayush
last_name: Kanodia
citation:
ama: Chatterjee K, Chmelik M, Gupta R, Kanodia A. Qualitative Analysis of POMDPs
with Temporal Logic Specifications for Robotics Applications. IST Austria;
2014. doi:10.15479/AT:IST-2014-305-v1-1
apa: Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2014). Qualitative
analysis of POMDPs with temporal logic specifications for robotics applications.
IST Austria. https://doi.org/10.15479/AT:IST-2014-305-v1-1
chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia.
Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics
Applications. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-305-v1-1.
ieee: K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, Qualitative analysis
of POMDPs with temporal logic specifications for robotics applications. IST
Austria, 2014.
ista: Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2014. Qualitative analysis of
POMDPs with temporal logic specifications for robotics applications, IST Austria,
12p.
mla: Chatterjee, Krishnendu, et al. Qualitative Analysis of POMDPs with Temporal
Logic Specifications for Robotics Applications. IST Austria, 2014, doi:10.15479/AT:IST-2014-305-v1-1.
short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Qualitative Analysis of
POMDPs with Temporal Logic Specifications for Robotics Applications, IST Austria,
2014.
date_created: 2018-12-12T11:39:15Z
date_published: 2014-09-09T00:00:00Z
date_updated: 2023-02-23T12:25:52Z
day: '09'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-305-v1-1
file:
- access_level: open_access
checksum: 35009d5fad01198341e6c1a3353481b7
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:51Z
date_updated: 2020-07-14T12:46:51Z
file_id: '5512'
file_name: IST-2014-305-v1+1_main.pdf
file_size: 655774
relation: main_file
file_date_updated: 2020-07-14T12:46:51Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '12'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '305'
related_material:
record:
- id: '1732'
relation: later_version
status: public
- id: '5426'
relation: later_version
status: public
status: public
title: Qualitative analysis of POMDPs with temporal logic specifications for robotics
applications
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5425'
abstract:
- lang: eng
text: ' We consider partially observable Markov decision processes (POMDPs) with
a set of target states and every transition is associated with an integer cost.
The optimization objective we study asks to minimize the expected total cost till
the target set is reached, while ensuring that the target set is reached almost-surely
(with probability 1). We show that for integer costs approximating the optimal
cost is undecidable. For positive costs, our results are as follows: (i) we establish
matching lower and upper bounds for the optimal cost and the bound is double exponential;
(ii) we show that the problem of approximating the optimal cost is decidable and
present approximation algorithms developing on the existing algorithms for POMDPs
with finite-horizon objectives. While the worst-case running time of our algorithm
is double exponential, we also present efficient stopping criteria for the algorithm
and show experimentally that it performs well in many examples of interest.'
alternative_title:
- IST Austria Technical Report
author:
- first_name: '1'
full_name: Anonymous, 1
last_name: Anonymous
- first_name: '2'
full_name: Anonymous, 2
last_name: Anonymous
- first_name: '3'
full_name: Anonymous, 3
last_name: Anonymous
- first_name: '4'
full_name: Anonymous, 4
last_name: Anonymous
citation:
ama: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. Optimal Cost Almost-Sure
Reachability in POMDPs. IST Austria; 2014.
apa: Anonymous, 1, Anonymous, 2, Anonymous, 3, & Anonymous, 4. (2014). Optimal
cost almost-sure reachability in POMDPs. IST Austria.
chicago: Anonymous, 1, 2 Anonymous, 3 Anonymous, and 4 Anonymous. Optimal Cost
Almost-Sure Reachability in POMDPs. IST Austria, 2014.
ieee: 1 Anonymous, 2 Anonymous, 3 Anonymous, and 4 Anonymous, Optimal cost almost-sure
reachability in POMDPs. IST Austria, 2014.
ista: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. 2014. Optimal cost almost-sure
reachability in POMDPs, IST Austria, 22p.
mla: Anonymous, 1, et al. Optimal Cost Almost-Sure Reachability in POMDPs.
IST Austria, 2014.
short: 1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, Optimal Cost Almost-Sure
Reachability in POMDPs, IST Austria, 2014.
date_created: 2018-12-12T11:39:15Z
date_published: 2014-09-09T00:00:00Z
date_updated: 2023-02-23T10:02:57Z
day: '09'
ddc:
- '000'
file:
- access_level: open_access
checksum: b9668a70d53c550b3cd64f0c77451c3d
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:17Z
date_updated: 2020-07-14T12:46:51Z
file_id: '5478'
file_name: IST-2014-307-v1+1_main.pdf
file_size: 2725429
relation: main_file
- access_level: closed
checksum: 808ada1dddecc48ca041526fcc6a9efd
content_type: text/plain
creator: dernst
date_created: 2019-04-16T14:16:12Z
date_updated: 2020-07-14T12:46:51Z
file_id: '6322'
file_name: IST-2014-307-v1+2_authors.txt
file_size: 117
relation: main_file
file_date_updated: 2020-07-14T12:46:51Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '22'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '307'
related_material:
record:
- id: '1529'
relation: later_version
status: public
scopus_import: 1
status: public
title: Optimal cost almost-sure reachability in POMDPs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5426'
abstract:
- lang: eng
text: We consider partially observable Markov decision processes (POMDPs), that
are a standard framework for robotics applications to model uncertainties present
in the real world, with temporal logic specifications. All temporal logic specifications
in linear-time temporal logic (LTL) can be expressed as parity objectives. We
study the qualitative analysis problem for POMDPs with parity objectives that
asks whether there is a controller (policy) to ensure that the objective holds
with probability 1 (almost-surely). While the qualitative analysis of POMDPs with
parity objectives is undecidable, recent results show that when restricted to
finite-memory policies the problem is EXPTIME-complete. While the problem is intractable
in theory, we present a practical approach to solve the qualitative analysis problem.
We designed several heuristics to deal with the exponential complexity, and have
used our implementation on a number of well-known POMDP examples for robotics
applications. Our results provide the first practical approach to solve the qualitative
analysis of robot motion planning with LTL properties in the presence of uncertainty.
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: Raghav
full_name: Gupta, Raghav
last_name: Gupta
- first_name: Ayush
full_name: Kanodia, Ayush
last_name: Kanodia
citation:
ama: Chatterjee K, Chmelik M, Gupta R, Kanodia A. Qualitative Analysis of POMDPs
with Temporal Logic Specifications for Robotics Applications. IST Austria;
2014. doi:10.15479/AT:IST-2014-305-v2-1
apa: Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2014). Qualitative
analysis of POMDPs with temporal logic specifications for robotics applications.
IST Austria. https://doi.org/10.15479/AT:IST-2014-305-v2-1
chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia.
Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics
Applications. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-305-v2-1.
ieee: K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, Qualitative analysis
of POMDPs with temporal logic specifications for robotics applications. IST
Austria, 2014.
ista: Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2014. Qualitative analysis of
POMDPs with temporal logic specifications for robotics applications, IST Austria,
10p.
mla: Chatterjee, Krishnendu, et al. Qualitative Analysis of POMDPs with Temporal
Logic Specifications for Robotics Applications. IST Austria, 2014, doi:10.15479/AT:IST-2014-305-v2-1.
short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Qualitative Analysis of
POMDPs with Temporal Logic Specifications for Robotics Applications, IST Austria,
2014.
date_created: 2018-12-12T11:39:16Z
date_published: 2014-09-29T00:00:00Z
date_updated: 2023-02-23T12:25:47Z
day: '29'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-305-v2-1
file:
- access_level: open_access
checksum: 730c0a8e97cf2712a884b2cc423f3919
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:15Z
date_updated: 2020-07-14T12:46:51Z
file_id: '5537'
file_name: IST-2014-305-v2+1_main2.pdf
file_size: 656019
relation: main_file
file_date_updated: 2020-07-14T12:46:51Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '10'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '311'
related_material:
record:
- id: '1732'
relation: later_version
status: public
- id: '5424'
relation: earlier_version
status: public
status: public
title: Qualitative analysis of POMDPs with temporal logic specifications for robotics
applications
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5427'
abstract:
- lang: eng
text: 'We consider graphs with n nodes together with their tree-decomposition that
has b = O ( n ) bags and width t , on the standard RAM computational model with
wordsize W = Θ (log n ) . Our contributions are two-fold: Our first contribution
is an algorithm that given a graph and its tree-decomposition as input, computes
a binary and balanced tree-decomposition of width at most 4 · t + 3 of the graph
in O ( b ) time and space, improving a long-standing (from 1992) bound of O (
n · log n ) time for constant treewidth graphs. Our second contribution is on
reachability queries for low treewidth graphs. We build on our tree-balancing
algorithm and present a data-structure for graph reachability that requires O
( n · t 2 ) preprocessing time, O ( n · t ) space, and O ( d t/ log n e ) time
for pair queries, and O ( n · t · log t/ log n ) time for single-source queries.
For constant t our data-structure uses O ( n ) time for preprocessing, O (1) time
for pair queries, and O ( n/ log n ) time for single-source queries. This is (asymptotically)
optimal and is faster than DFS/BFS when answering more than a constant number
of single-source queries.'
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. Optimal Tree-Decomposition
Balancing and Reachability on Low Treewidth Graphs. IST Austria; 2014. doi:10.15479/AT:IST-2014-314-v1-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2014). Optimal
tree-decomposition balancing and reachability on low treewidth graphs. IST
Austria. https://doi.org/10.15479/AT:IST-2014-314-v1-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs.
IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-314-v1-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Optimal tree-decomposition
balancing and reachability on low treewidth graphs. IST Austria, 2014.
ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2014. Optimal tree-decomposition
balancing and reachability on low treewidth graphs, IST Austria, 24p.
mla: Chatterjee, Krishnendu, et al. Optimal Tree-Decomposition Balancing and
Reachability on Low Treewidth Graphs. IST Austria, 2014, doi:10.15479/AT:IST-2014-314-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Optimal Tree-Decomposition
Balancing and Reachability on Low Treewidth Graphs, IST Austria, 2014.
date_created: 2018-12-12T11:39:16Z
date_published: 2014-11-05T00:00:00Z
date_updated: 2021-01-12T08:02:09Z
day: '05'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-314-v1-1
file:
- access_level: open_access
checksum: 9d3b90bf4fff74664f182f2d95ef727a
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:10Z
date_updated: 2020-07-14T12:46:52Z
file_id: '5471'
file_name: IST-2014-314-v1+1_long.pdf
file_size: 405561
relation: main_file
file_date_updated: 2020-07-14T12:46:52Z
has_accepted_license: '1'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: '24'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '314'
status: public
title: Optimal tree-decomposition balancing and reachability on low treewidth graphs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5428'
abstract:
- lang: eng
text: "Simulation is an attractive alternative for language inclusion for automata
as it is an under-approximation of language inclusion, but usually has much lower
complexity. For non-deterministic automata, while language inclusion is PSPACE-complete,
simulation can be computed in polynomial time. Simulation has also been extended
in two orthogonal directions, namely, (1) fair simulation, for simulation over
specified set of infinite runs; and (2) quantitative simulation, for simulation
between weighted automata. Again, while fair trace inclusion is PSPACE-complete,
fair simulation can be computed in polynomial time. For weighted automata, the
(quantitative) language inclusion problem is undecidable for mean-payoff automata
and the decidability is open for discounted-sum automata, whereas the (quantitative)
simulation reduce to mean-payoff games and discounted-sum games, which admit pseudo-polynomial
time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted
automata with Büchi acceptance conditions, i.e., we generalize fair simulation
from non-weighted automata to weighted automata. We show that imposing Büchi acceptance
conditions on weighted automata changes many fundamental properties of the simulation
games. For example, whereas for mean-payoff and discounted-sum games, the players
do not need memory to play optimally; we show in contrast that for simulation
games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal
strategies for both players require infinite memory in general, and (ii) for discounted-sum
objectives, optimal strategies need not exist for both players. While the simulation
games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory
requirements for mean-payoff objectives) as compared to their counterpart without
Büchi acceptance conditions, we still present pseudo-polynomial time algorithms
to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff
and weighted discounted-sum automata."
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
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative Fair Simulation
Games. IST Austria; 2014. doi:10.15479/AT:IST-2014-315-v1-1
apa: Chatterjee, K., Henzinger, T. A., Otop, J., & Velner, Y. (2014). Quantitative
fair simulation games. IST Austria. https://doi.org/10.15479/AT:IST-2014-315-v1-1
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner.
Quantitative Fair Simulation Games. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-315-v1-1.
ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, Quantitative fair
simulation games. IST Austria, 2014.
ista: Chatterjee K, Henzinger TA, Otop J, Velner Y. 2014. Quantitative fair simulation
games, IST Austria, 26p.
mla: Chatterjee, Krishnendu, et al. Quantitative Fair Simulation Games. IST
Austria, 2014, doi:10.15479/AT:IST-2014-315-v1-1.
short: K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Quantitative Fair Simulation
Games, IST Austria, 2014.
date_created: 2018-12-12T11:39:16Z
date_published: 2014-12-05T00:00:00Z
date_updated: 2023-09-20T12:07:48Z
day: '05'
ddc:
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.15479/AT:IST-2014-315-v1-1
file:
- access_level: open_access
checksum: b1d573bc04365625ff9974880c0aa807
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:59Z
date_updated: 2020-07-14T12:46:52Z
file_id: '5521'
file_name: IST-2014-315-v1+1_report.pdf
file_size: 531046
relation: main_file
file_date_updated: 2020-07-14T12:46:52Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '26'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '315'
related_material:
record:
- id: '1066'
relation: later_version
status: public
status: public
title: Quantitative fair simulation games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5399'
abstract:
- lang: eng
text: In this work we present a flexible tool for tumor progression, which simulates
the evolutionary dynamics of cancer. Tumor progression implements a multi-type
branching process where the key parameters are the fitness landscape, the mutation
rate, and the average time of cell division. The fitness of a cancer cell depends
on the mutations it has accumulated. The input to our tool could be any fitness
landscape, mutation rate, and cell division time, and the tool produces the growth
dynamics and all relevant statistics.
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: 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: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: 'Reiter J, Bozic I, Chatterjee K, Nowak M. TTP: Tool for Tumor Progression.
IST Austria; 2013. doi:10.15479/AT:IST-2013-104-v1-1'
apa: 'Reiter, J., Bozic, I., Chatterjee, K., & Nowak, M. (2013). TTP: Tool
for Tumor Progression. IST Austria. https://doi.org/10.15479/AT:IST-2013-104-v1-1'
chicago: 'Reiter, Johannes, Ivana Bozic, Krishnendu Chatterjee, and Martin Nowak.
TTP: Tool for Tumor Progression. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-104-v1-1.'
ieee: 'J. Reiter, I. Bozic, K. Chatterjee, and M. Nowak, TTP: Tool for Tumor
Progression. IST Austria, 2013.'
ista: 'Reiter J, Bozic I, Chatterjee K, Nowak M. 2013. TTP: Tool for Tumor Progression,
IST Austria, 17p.'
mla: 'Reiter, Johannes, et al. TTP: Tool for Tumor Progression. IST Austria,
2013, doi:10.15479/AT:IST-2013-104-v1-1.'
short: 'J. Reiter, I. Bozic, K. Chatterjee, M. Nowak, TTP: Tool for Tumor Progression,
IST Austria, 2013.'
date_created: 2018-12-12T11:39:07Z
date_published: 2013-01-11T00:00:00Z
date_updated: 2023-02-23T10:23:57Z
day: '11'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2013-104-v1-1
file:
- access_level: open_access
checksum: 2cc8c6e157eca1271128db80bb3dec80
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:20Z
date_updated: 2020-07-14T12:46:44Z
file_id: '5542'
file_name: IST-2013-104-v1+1_tumortool.pdf
file_size: 1471954
relation: main_file
file_date_updated: 2020-07-14T12:46:44Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '17'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '104'
related_material:
record:
- id: '2000'
relation: later_version
status: public
status: public
title: 'TTP: Tool for Tumor Progression'
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5400'
abstract:
- lang: eng
text: We consider partially observable Markov decision processes (POMDPs) with ω-regular
conditions specified as parity objectives. The class of ω-regular languages extends
regular languages to infinite strings and provides a robust specification language
to express all properties used in verification, and parity objectives are canonical
forms to express ω-regular conditions. The qualitative analysis problem given
a POMDP and a parity objective asks whether there is a strategy to ensure that
the objective is satis- fied with probability 1 (resp. positive probability).
While the qualitative analysis problems are known to be undecidable even for very
special cases of parity objectives, we establish decidability (with optimal complexity)
of the qualitative analysis problems for POMDPs with all parity objectives under
finite- memory strategies. We establish asymptotically optimal (exponential) memory
bounds and EXPTIME- completeness of the qualitative analysis problems under finite-memory
strategies for POMDPs with parity objectives.
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: Mathieu
full_name: Tracol, Mathieu
id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
last_name: Tracol
citation:
ama: Chatterjee K, Chmelik M, Tracol M. What Is Decidable about Partially Observable
Markov Decision Processes with ω-Regular Objectives. IST Austria; 2013. doi:10.15479/AT:IST-2013-109-v1-1
apa: Chatterjee, K., Chmelik, M., & Tracol, M. (2013). What is decidable
about partially observable Markov decision processes with ω-regular objectives.
IST Austria. https://doi.org/10.15479/AT:IST-2013-109-v1-1
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. What Is
Decidable about Partially Observable Markov Decision Processes with ω-Regular
Objectives. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-109-v1-1.
ieee: K. Chatterjee, M. Chmelik, and M. Tracol, What is decidable about partially
observable Markov decision processes with ω-regular objectives. IST Austria,
2013.
ista: Chatterjee K, Chmelik M, Tracol M. 2013. What is decidable about partially
observable Markov decision processes with ω-regular objectives, IST Austria, 41p.
mla: Chatterjee, Krishnendu, et al. What Is Decidable about Partially Observable
Markov Decision Processes with ω-Regular Objectives. IST Austria, 2013, doi:10.15479/AT:IST-2013-109-v1-1.
short: K. Chatterjee, M. Chmelik, M. Tracol, What Is Decidable about Partially Observable
Markov Decision Processes with ω-Regular Objectives, IST Austria, 2013.
date_created: 2018-12-12T11:39:07Z
date_published: 2013-02-20T00:00:00Z
date_updated: 2023-02-23T10:36:45Z
day: '20'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2013-109-v1-1
file:
- access_level: open_access
checksum: cbba40210788a1b22c6cf06433b5ed6f
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:06Z
date_updated: 2020-07-14T12:46:44Z
file_id: '5467'
file_name: IST-2013-109-v1+1_What_is_Decidable_about_Partially_Observable_Markov_Decision_Processes_with_ω-Regular_Objectives.pdf
file_size: 483407
relation: main_file
file_date_updated: 2020-07-14T12:46:44Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '41'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '109'
related_material:
record:
- id: '1477'
relation: later_version
status: public
- id: '2295'
relation: later_version
status: public
status: public
title: What is decidable about partially observable Markov decision processes with
ω-regular objectives
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5402'
abstract:
- lang: eng
text: "Linearizability requires that the outcome of calls by competing threads to
a concurrent data structure is the same as some sequential execution where each
thread has exclusive access to the data structure. In an ordered data structure,
such as a queue or a stack, linearizability is ensured by requiring threads commit
in the order dictated by the sequential semantics of the data structure; e.g.,
in a concurrent queue implementation a dequeue can only remove the oldest element.
\r\nIn this paper, we investigate the impact of this strict ordering, by comparing
what linearizability allows to what existing implementations do. We first give
an operational definition for linearizability which allows us to build the most
general linearizable implementation as a transition system for any given sequential
specification. We then use this operational definition to categorize linearizable
implementations based on whether they are bound or free. In a bound implementation,
whenever all threads observe the same logical state, the updates to the logical
state and the temporal order of commits coincide. All existing queue implementations
we know of are bound. We then proceed to present, to the best of our knowledge,
the first ever free queue implementation. Our experiments show that free implementations
have the potential for better performance by suffering less from contention."
alternative_title:
- IST Austria Technical Report
author:
- 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: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
citation:
ama: Henzinger TA, Sezgin A. How Free Is Your Linearizable Concurrent Data Structure?
IST Austria; 2013. doi:10.15479/AT:IST-2013-123-v1-1
apa: Henzinger, T. A., & Sezgin, A. (2013). How free is your linearizable
concurrent data structure? IST Austria. https://doi.org/10.15479/AT:IST-2013-123-v1-1
chicago: Henzinger, Thomas A, and Ali Sezgin. How Free Is Your Linearizable Concurrent
Data Structure? IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-123-v1-1.
ieee: T. A. Henzinger and A. Sezgin, How free is your linearizable concurrent
data structure? IST Austria, 2013.
ista: Henzinger TA, Sezgin A. 2013. How free is your linearizable concurrent data
structure?, IST Austria, 16p.
mla: Henzinger, Thomas A., and Ali Sezgin. How Free Is Your Linearizable Concurrent
Data Structure? IST Austria, 2013, doi:10.15479/AT:IST-2013-123-v1-1.
short: T.A. Henzinger, A. Sezgin, How Free Is Your Linearizable Concurrent Data
Structure?, IST Austria, 2013.
date_created: 2018-12-12T11:39:07Z
date_published: 2013-06-12T00:00:00Z
date_updated: 2020-07-14T23:04:47Z
day: '12'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2013-123-v1-1
file:
- access_level: open_access
checksum: ce580605ae9756a8c99d7b403ebb8eed
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:19Z
date_updated: 2020-07-14T12:46:45Z
file_id: '5480'
file_name: IST-2013-123-v1+1_main-concur2013.pdf
file_size: 249790
relation: main_file
file_date_updated: 2020-07-14T12:46:45Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: '16'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '123'
status: public
title: How free is your linearizable concurrent data structure?
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5403'
abstract:
- lang: eng
text: 'We consider concurrent games played by two-players on a finite state graph,
where in every round the players simultaneously choose a move, and the current
state along with the joint moves determine the successor state. We study the most
fundamental objective for concurrent games, namely, mean-payoff or limit-average
objective, where a reward is associated to every transition, and the goal of player
1 is to maximize the long-run average of the rewards, and the objective of player
2 is strictly the opposite (i.e., the games are zero-sum). The path constraint
for player 1 could be qualitative, i.e., the mean-payoff is the maximal reward,
or arbitrarily close to it; or quantitative, i.e., a given threshold between the
minimal and maximal reward. We consider the computation of the almost-sure (resp.
positive) winning sets, where player 1 can ensure that the path constraint is
satisfied with probability 1 (resp. positive probability). Almost-sure winning
with qualitative constraint exactly corresponds to the question whether there
exists a strategy to ensure that the payoff is the maximal reward of the game.
Our main results for qualitative path constraints are as follows: (1) we establish
qualitative determinacy results that show for every state either player 1 has
a strategy to ensure almost-sure (resp. positive) winning against all player-2
strategies or player 2 has a spoiling strategy to falsify almost-sure (resp. positive)
winning against all player-1 strategies; (2) we present optimal strategy complexity
results that precisely characterize the classes of strategies required for almost-sure
and positive winning for both players; and (3) we present quadratic time algorithms
to compute the almost-sure and the positive winning sets, matching the best known
bound of the algorithms for much simpler problems (such as reachability objectives).
For quantitative constraints we show that a polynomial time solution for the almost-sure
or the positive winning set would imply a solution to a long-standing open problem
(of solving the value problem of mean-payoff games) that is not known to be in
polynomial time.'
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
citation:
ama: Chatterjee K, Ibsen-Jensen R. Qualitative Analysis of Concurrent Mean-Payoff
Games. IST Austria; 2013. doi:10.15479/AT:IST-2013-126-v1-1
apa: Chatterjee, K., & Ibsen-Jensen, R. (2013). Qualitative analysis of concurrent
mean-payoff games. IST Austria. https://doi.org/10.15479/AT:IST-2013-126-v1-1
chicago: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. Qualitative Analysis
of Concurrent Mean-Payoff Games. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-126-v1-1.
ieee: K. Chatterjee and R. Ibsen-Jensen, Qualitative analysis of concurrent mean-payoff
games. IST Austria, 2013.
ista: Chatterjee K, Ibsen-Jensen R. 2013. Qualitative analysis of concurrent mean-payoff
games, IST Austria, 33p.
mla: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. Qualitative Analysis of
Concurrent Mean-Payoff Games. IST Austria, 2013, doi:10.15479/AT:IST-2013-126-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, Qualitative Analysis of Concurrent Mean-Payoff
Games, IST Austria, 2013.
date_created: 2018-12-12T11:39:08Z
date_published: 2013-07-03T00:00:00Z
date_updated: 2023-02-23T12:22:53Z
day: '03'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2013-126-v1-1
file:
- access_level: open_access
checksum: 063868c665beec37bf28160e2a695746
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:49Z
date_updated: 2020-07-14T12:46:45Z
file_id: '5510'
file_name: IST-2013-126-v1+1_soda_full.pdf
file_size: 434523
relation: main_file
file_date_updated: 2020-07-14T12:46:45Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '126'
related_material:
record:
- id: '524'
relation: later_version
status: public
status: public
title: Qualitative analysis of concurrent mean-payoff games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5404'
abstract:
- lang: eng
text: 'We study finite-state two-player (zero-sum) concurrent mean-payoff games
played on a graph. We focus on the important sub-class of ergodic games where
all states are visited infinitely often with probability 1. The algorithmic study
of ergodic games was initiated in a seminal work of Hoffman and Karp in 1966,
but all basic complexity questions have remained unresolved. Our main results
for ergodic games are as follows: We establish (1) an optimal exponential bound
on the patience of stationary strategies (where patience of a distribution is
the inverse of the smallest positive probability and represents a complexity measure
of a stationary strategy); (2) the approximation problem lie in FNP; (3) the approximation
problem is at least as hard as the decision problem for simple stochastic games
(for which NP and coNP is the long-standing best known bound). We show that the
exact value can be expressed in the existential theory of the reals, and also
establish square-root sum hardness for a related class of games.'
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
citation:
ama: Chatterjee K, Ibsen-Jensen R. The Complexity of Ergodic Games. IST Austria;
2013. doi:10.15479/AT:IST-2013-127-v1-1
apa: Chatterjee, K., & Ibsen-Jensen, R. (2013). The complexity of ergodic
games. IST Austria. https://doi.org/10.15479/AT:IST-2013-127-v1-1
chicago: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Complexity of Ergodic
Games. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-127-v1-1.
ieee: K. Chatterjee and R. Ibsen-Jensen, The complexity of ergodic games.
IST Austria, 2013.
ista: Chatterjee K, Ibsen-Jensen R. 2013. The complexity of ergodic games, IST Austria,
29p.
mla: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Complexity of Ergodic
Games. IST Austria, 2013, doi:10.15479/AT:IST-2013-127-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, The Complexity of Ergodic Games, IST Austria,
2013.
date_created: 2018-12-12T11:39:08Z
date_published: 2013-07-03T00:00:00Z
date_updated: 2023-02-23T10:30:55Z
day: '03'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2013-127-v1-1
file:
- access_level: open_access
checksum: 79ee5e677a82611ce06e0360c69d494a
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:35Z
date_updated: 2020-07-14T12:46:45Z
file_id: '5496'
file_name: IST-2013-127-v1+1_ergodic.pdf
file_size: 517275
relation: main_file
file_date_updated: 2020-07-14T12:46:45Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '29'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '127'
related_material:
record:
- id: '2162'
relation: later_version
status: public
status: public
title: The complexity of ergodic games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5405'
abstract:
- lang: eng
text: "The theory of graph games is the foundation for modeling and synthesizing
reactive processes. In the synthesis of stochastic processes, we use 2-1/2-player
games where some transitions of the game graph are controlled by two adversarial
players, the System and the Environment, and the other transitions are determined
probabilistically. We consider 2-1/2-player games where the objective of the System
is the conjunction of a qualitative objective (specified as a parity condition)
and a quantitative objective (specified as a mean-payoff condition). We establish
that the problem of deciding whether the System can ensure that the probability
to satisfy the mean-payoff parity objective is at least a given threshold is in
NP ∩ coNP, matching the best known bound in the special case of 2-player games
(where all transitions are deterministic) with only parity objectives, or with
only mean-payoff objectives. We present an algorithm running\r\nin time O(d ·
n^{2d}·MeanGame) to compute the set of almost-sure winning states from which the
objective\r\ncan be ensured with probability 1, where n is the number of states
of the game, d the number of priorities\r\nof the parity objective, and MeanGame
is the complexity to compute the set of almost-sure winning states\r\nin 2-1/2-player
mean-payoff games. Our results are useful in the synthesis of stochastic reactive
systems\r\nwith both functional requirement (given as a qualitative objective)
and performance requirement (given\r\nas a quantitative objective)."
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: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Hugo
full_name: Gimbert, Hugo
last_name: Gimbert
- first_name: Youssouf
full_name: Oualhadj, Youssouf
last_name: Oualhadj
citation:
ama: Chatterjee K, Doyen L, Gimbert H, Oualhadj Y. Perfect-Information Stochastic
Mean-Payoff Parity Games. IST Austria; 2013. doi:10.15479/AT:IST-2013-128-v1-1
apa: Chatterjee, K., Doyen, L., Gimbert, H., & Oualhadj, Y. (2013). Perfect-information
stochastic mean-payoff parity games. IST Austria. https://doi.org/10.15479/AT:IST-2013-128-v1-1
chicago: Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Youssouf Oualhadj.
Perfect-Information Stochastic Mean-Payoff Parity Games. IST Austria, 2013.
https://doi.org/10.15479/AT:IST-2013-128-v1-1.
ieee: K. Chatterjee, L. Doyen, H. Gimbert, and Y. Oualhadj, Perfect-information
stochastic mean-payoff parity games. IST Austria, 2013.
ista: Chatterjee K, Doyen L, Gimbert H, Oualhadj Y. 2013. Perfect-information stochastic
mean-payoff parity games, IST Austria, 22p.
mla: Chatterjee, Krishnendu, et al. Perfect-Information Stochastic Mean-Payoff
Parity Games. IST Austria, 2013, doi:10.15479/AT:IST-2013-128-v1-1.
short: K. Chatterjee, L. Doyen, H. Gimbert, Y. Oualhadj, Perfect-Information Stochastic
Mean-Payoff Parity Games, IST Austria, 2013.
date_created: 2018-12-12T11:39:09Z
date_published: 2013-07-08T00:00:00Z
date_updated: 2023-02-23T10:33:08Z
day: '08'
ddc:
- '000'
- '005'
- '510'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2013-128-v1-1
file:
- access_level: open_access
checksum: ede787a10e74e4f7db302fab8f12f3ca
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:54Z
date_updated: 2020-07-14T12:46:45Z
file_id: '5516'
file_name: IST-2013-128-v1+1_full_stoch_mpp.pdf
file_size: 387467
relation: main_file
file_date_updated: 2020-07-14T12:46:45Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '22'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '128'
related_material:
record:
- id: '2212'
relation: later_version
status: public
status: public
title: Perfect-information stochastic mean-payoff parity games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5406'
abstract:
- lang: eng
text: 'We consider the distributed synthesis problem fortemporal logic specifications.
Traditionally, the problem has been studied for LTL, and the previous results
show that the problem is decidable iff there is no information fork in the architecture.
We consider the problem for fragments of LTLand our main results are as follows:
(1) We show that the problem is undecidable for architectures with information
forks even for the fragment of LTL with temporal operators restricted to next
and eventually. (2) For specifications restricted to globally along with non-nested
next operators, we establish decidability (in EXPSPACE) for star architectures
where the processes receive disjoint inputs, whereas we establish undecidability
for architectures containing an information fork-meet structure. (3)Finally, we
consider LTL without the next operator, and establish decidability (NEXPTIME-complete)
for all architectures for a fragment that consists of a set of safety assumptions,
and a set of guarantees where each guarantee is a safety, reachability, or liveness
condition.'
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
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed Synthesis
for LTL Fragments. IST Austria; 2013. doi:10.15479/AT:IST-2013-130-v1-1
apa: Chatterjee, K., Henzinger, T. A., Otop, J., & Pavlogiannis, A. (2013).
Distributed synthesis for LTL Fragments. IST Austria. https://doi.org/10.15479/AT:IST-2013-130-v1-1
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis.
Distributed Synthesis for LTL Fragments. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-130-v1-1.
ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, Distributed
synthesis for LTL Fragments. IST Austria, 2013.
ista: Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis
for LTL Fragments, IST Austria, 11p.
mla: Chatterjee, Krishnendu, et al. Distributed Synthesis for LTL Fragments.
IST Austria, 2013, doi:10.15479/AT:IST-2013-130-v1-1.
short: K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, Distributed Synthesis
for LTL Fragments, IST Austria, 2013.
date_created: 2018-12-12T11:39:09Z
date_published: 2013-07-08T00:00:00Z
date_updated: 2023-02-21T17:01:26Z
day: '08'
ddc:
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2013-130-v1-1
file:
- access_level: open_access
checksum: 855513ebaf6f72228800c5fdb522f93c
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:18Z
date_updated: 2020-07-14T12:46:45Z
file_id: '5540'
file_name: IST-2013-130-v1+1_Distributed_Synthesis.pdf
file_size: 467895
relation: main_file
file_date_updated: 2020-07-14T12:46:45Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '11'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '130'
related_material:
record:
- id: '1376'
relation: later_version
status: public
status: public
title: Distributed synthesis for LTL Fragments
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5408'
abstract:
- lang: eng
text: "We consider two-player partial-observation stochastic games where player
1 has partial observation and player 2 has perfect observation. The winning condition
we study are omega-regular conditions specified as parity objectives. The qualitative
analysis problem given a partial-observation stochastic game and a parity objective
asks whether there is a strategy to ensure that the objective is satisfied with
probability 1 (resp. positive probability). While the qualitative analysis problems
are known to be undecidable even for very special cases of parity objectives,
they were shown to be decidable in 2EXPTIME under finite-memory strategies. We
improve the complexity and show that the qualitative analysis problems for partial-observation
stochastic parity games under finite-memory strategies are \r\nEXPTIME-complete;
and also establish optimal (exponential) memory bounds for finite-memory strategies
required for qualitative analysis. "
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: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Sumit
full_name: Nain, Sumit
last_name: Nain
- first_name: Moshe
full_name: Vardi, Moshe
last_name: Vardi
citation:
ama: Chatterjee K, Doyen L, Nain S, Vardi M. The Complexity of Partial-Observation
Stochastic Parity Games with Finite-Memory Strategies. IST Austria; 2013.
doi:10.15479/AT:IST-2013-141-v1-1
apa: Chatterjee, K., Doyen, L., Nain, S., & Vardi, M. (2013). The complexity
of partial-observation stochastic parity games with finite-memory strategies.
IST Austria. https://doi.org/10.15479/AT:IST-2013-141-v1-1
chicago: Chatterjee, Krishnendu, Laurent Doyen, Sumit Nain, and Moshe Vardi. The
Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies.
IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-141-v1-1.
ieee: K. Chatterjee, L. Doyen, S. Nain, and M. Vardi, The complexity of partial-observation
stochastic parity games with finite-memory strategies. IST Austria, 2013.
ista: Chatterjee K, Doyen L, Nain S, Vardi M. 2013. The complexity of partial-observation
stochastic parity games with finite-memory strategies, IST Austria, 17p.
mla: Chatterjee, Krishnendu, et al. The Complexity of Partial-Observation Stochastic
Parity Games with Finite-Memory Strategies. IST Austria, 2013, doi:10.15479/AT:IST-2013-141-v1-1.
short: K. Chatterjee, L. Doyen, S. Nain, M. Vardi, The Complexity of Partial-Observation
Stochastic Parity Games with Finite-Memory Strategies, IST Austria, 2013.
date_created: 2018-12-12T11:39:10Z
date_published: 2013-09-12T00:00:00Z
date_updated: 2023-02-23T10:33:11Z
day: '12'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2013-141-v1-1
file:
- access_level: open_access
checksum: 226bc791124f8d3138379778ce834e86
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:16Z
date_updated: 2020-07-14T12:46:46Z
file_id: '5477'
file_name: IST-2013-141-v1+1_main-tech-rpt.pdf
file_size: 300481
relation: main_file
file_date_updated: 2020-07-14T12:46:46Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '17'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '141'
related_material:
record:
- id: '2213'
relation: later_version
status: public
status: public
title: The complexity of partial-observation stochastic parity games with finite-memory
strategies
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5409'
abstract:
- lang: eng
text: "The edit distance between two (untimed) traces is the minimum cost of a sequence
of edit operations (insertion, deletion, or substitution) needed to transform
one trace to the other. Edit distances have been extensively studied in the untimed
setting, and form the basis for approximate matching of sequences in different
domains such as coding theory, parsing, and speech recognition. \r\nIn this paper,
we lift the study of edit distances from untimed languages to the timed setting.
We define an edit distance between timed words which incorporates both the edit
distance between the untimed words and the absolute difference in timestamps.
Our edit distance between two timed words is computable in polynomial time. Further,
we show that the edit distance between a timed word and a timed language generated
by a timed automaton, defined as the edit distance between the word and the closest
word in the language, is PSPACE-complete. While computing the edit distance between
two timed automata is undecidable, we show that the approximate version, where
we decide if the edit distance between two timed automata is either less than
a given parameter or more than delta away from the parameter, for delta>0, can
be solved in exponential space and is EXPSPACE-hard. Our definitions and techniques
can be generalized to the setting of hybrid systems, and we show analogous decidability
results for rectangular automata."
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: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
citation:
ama: Chatterjee K, Ibsen-Jensen R, Majumdar R. Edit Distance for Timed Automata.
IST Austria; 2013. doi:10.15479/AT:IST-2013-144-v1-1
apa: Chatterjee, K., Ibsen-Jensen, R., & Majumdar, R. (2013). Edit distance
for timed automata. IST Austria. https://doi.org/10.15479/AT:IST-2013-144-v1-1
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Rupak Majumdar. Edit
Distance for Timed Automata. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-144-v1-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and R. Majumdar, Edit distance for timed
automata. IST Austria, 2013.
ista: Chatterjee K, Ibsen-Jensen R, Majumdar R. 2013. Edit distance for timed automata,
IST Austria, 12p.
mla: Chatterjee, Krishnendu, et al. Edit Distance for Timed Automata. IST
Austria, 2013, doi:10.15479/AT:IST-2013-144-v1-1.
short: K. Chatterjee, R. Ibsen-Jensen, R. Majumdar, Edit Distance for Timed Automata,
IST Austria, 2013.
date_created: 2018-12-12T11:39:10Z
date_published: 2013-10-30T00:00:00Z
date_updated: 2023-02-23T10:33:18Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2013-144-v1-1
file:
- access_level: open_access
checksum: 0f7633081ba8299c543322f0ad08571f
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:08Z
date_updated: 2020-07-14T12:46:46Z
file_id: '5469'
file_name: IST-2013-144-v1+1_main.pdf
file_size: 336377
relation: main_file
file_date_updated: 2020-07-14T12:46:46Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '12'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '144'
related_material:
record:
- id: '2216'
relation: later_version
status: public
status: public
title: Edit distance for timed automata
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5410'
abstract:
- lang: eng
text: "Board games, like Tic-Tac-Toe and CONNECT-4, play an important role not only
in development of mathematical and logical skills, but also in 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.
\r\nOur approach 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. Also, the presence of such states for standard game variants like Tic-Tac-Toe
on board size 4x4 opens up new games to be played that have not been played for
ages since the default start state is heavily biased. "
alternative_title:
- IST Austria Technical Report
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 Traditional Board Games. IST Austria; 2013. doi:10.15479/AT:IST-2013-146-v1-1
apa: Ahmed, U., Chatterjee, K., & Gulwani, S. (2013). Automatic generation
of alternative starting positions for traditional board games. IST Austria.
https://doi.org/10.15479/AT:IST-2013-146-v1-1
chicago: Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. Automatic Generation
of Alternative Starting Positions for Traditional Board Games. IST Austria,
2013. https://doi.org/10.15479/AT:IST-2013-146-v1-1.
ieee: U. Ahmed, K. Chatterjee, and S. Gulwani, Automatic generation of alternative
starting positions for traditional board games. IST Austria, 2013.
ista: Ahmed U, Chatterjee K, Gulwani S. 2013. Automatic generation of alternative
starting positions for traditional board games, IST Austria, 13p.
mla: Ahmed, Umair, et al. Automatic Generation of Alternative Starting Positions
for Traditional Board Games. IST Austria, 2013, doi:10.15479/AT:IST-2013-146-v1-1.
short: U. Ahmed, K. Chatterjee, S. Gulwani, Automatic Generation of Alternative
Starting Positions for Traditional Board Games, IST Austria, 2013.
date_created: 2018-12-12T11:39:10Z
date_published: 2013-12-03T00:00:00Z
date_updated: 2023-02-23T10:00:50Z
day: '03'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2013-146-v1-1
file:
- access_level: open_access
checksum: 409f3aaaf1184e4057b89cbb449dac80
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:06Z
date_updated: 2020-07-14T12:46:46Z
file_id: '5528'
file_name: IST-2013-146-v1+1_main.pdf
file_size: 818189
relation: main_file
file_date_updated: 2020-07-14T12:46:46Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '13'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '146'
related_material:
record:
- id: '1481'
relation: later_version
status: public
status: public
title: Automatic generation of alternative starting positions for traditional board
games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '6440'
abstract:
- lang: eng
text: In order to guarantee that each method of a data structure updates the logical
state exactly once, al-most all non-blocking implementations employ Compare-And-Swap
(CAS) based synchronization. For FIFO queue implementations this translates into concurrent enqueue or dequeue methods
competing among themselves to update the same variable, the tail or the head,
respectively, leading to high contention and poor scalability. Recent non-blocking
queue implementations try to alleviate high contentionby increasing the number
of contention points, all the while using CAS-based synchronization. Furthermore,
obtaining a wait-free implementation with competition is achieved by additional
synchronization which leads to further degradation of performance.In this paper
we formalize the notion of competitiveness of a synchronizing statement which
can beused as a measure for the scalability of concurrent implementations. We
present a new queue implementation, the Speculative Pairing (SP) queue, which,
as we show, decreases competitiveness by using Fetch-And-Increment (FAI) instead
of CAS. We prove that the SP queue is linearizable and lock-free.We also show
that replacing CAS with FAI leads to wait-freedom for dequeue methods without
an adverse effect on performance. In fact, our experiments suggest that the SP
queue can perform and scale better than the state-of-the-art queue implementations.
alternative_title:
- IST Austria Technical Report
author:
- 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: Hannes
full_name: Payer, Hannes
last_name: Payer
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
citation:
ama: Henzinger TA, Payer H, Sezgin A. Replacing Competition with Cooperation
to Achieve Scalable Lock-Free FIFO Queues . IST Austria; 2013. doi:10.15479/AT:IST-2013-124-v1-1
apa: Henzinger, T. A., Payer, H., & Sezgin, A. (2013). Replacing competition
with cooperation to achieve scalable lock-free FIFO queues . IST Austria.
https://doi.org/10.15479/AT:IST-2013-124-v1-1
chicago: Henzinger, Thomas A, Hannes Payer, and Ali Sezgin. Replacing Competition
with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria,
2013. https://doi.org/10.15479/AT:IST-2013-124-v1-1.
ieee: T. A. Henzinger, H. Payer, and A. Sezgin, Replacing competition with cooperation
to achieve scalable lock-free FIFO queues . IST Austria, 2013.
ista: Henzinger TA, Payer H, Sezgin A. 2013. Replacing competition with cooperation
to achieve scalable lock-free FIFO queues , IST Austria, 23p.
mla: Henzinger, Thomas A., et al. Replacing Competition with Cooperation to Achieve
Scalable Lock-Free FIFO Queues . IST Austria, 2013, doi:10.15479/AT:IST-2013-124-v1-1.
short: T.A. Henzinger, H. Payer, A. Sezgin, Replacing Competition with Cooperation
to Achieve Scalable Lock-Free FIFO Queues , IST Austria, 2013.
date_created: 2019-05-13T14:13:27Z
date_published: 2013-06-13T00:00:00Z
date_updated: 2020-07-14T23:06:19Z
day: '13'
ddc:
- '000'
- '005'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2013-124-v1-1
file:
- access_level: open_access
checksum: a219ba4eada6cd62befed52262ee15d4
content_type: application/pdf
creator: dernst
date_created: 2019-05-13T14:11:39Z
date_updated: 2020-07-14T12:47:30Z
file_id: '6441'
file_name: 2013_TechRep_Henzinger.pdf
file_size: 549684
relation: main_file
file_date_updated: 2020-07-14T12:47:30Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: '23'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '124'
status: public
title: 'Replacing competition with cooperation to achieve scalable lock-free FIFO
queues '
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5396'
abstract:
- lang: eng
text: We consider the problem of inference in agraphical model with binary variables.
While in theory it is arguably preferable to compute marginal probabilities, in
practice researchers often use MAP inference due to the availability of efficient
discrete optimization algorithms. We bridge the gap between the two approaches
by introducing the Discrete Marginals technique in which approximate marginals
are obtained by minimizing an objective function with unary and pair-wise terms
over a discretized domain. This allows the use of techniques originally devel-oped
for MAP-MRF inference and learning. We explore two ways to set up the objective
function - by discretizing the Bethe free energy and by learning it from training
data. Experimental results show that for certain types of graphs a learned function
can out-perform the Bethe approximation. We also establish a link between the
Bethe free energy and submodular functions.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Filip
full_name: Korc, Filip
id: 476A2FD6-F248-11E8-B48F-1D18A9856A87
last_name: Korc
- first_name: Vladimir
full_name: Kolmogorov, Vladimir
id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
last_name: Kolmogorov
- first_name: Christoph
full_name: Lampert, Christoph
id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
last_name: Lampert
orcid: 0000-0001-8622-7887
citation:
ama: Korc F, Kolmogorov V, Lampert C. Approximating Marginals Using Discrete
Energy Minimization. IST Austria; 2012. doi:10.15479/AT:IST-2012-0003
apa: Korc, F., Kolmogorov, V., & Lampert, C. (2012). Approximating marginals
using discrete energy minimization. IST Austria. https://doi.org/10.15479/AT:IST-2012-0003
chicago: Korc, Filip, Vladimir Kolmogorov, and Christoph Lampert. Approximating
Marginals Using Discrete Energy Minimization. IST Austria, 2012. https://doi.org/10.15479/AT:IST-2012-0003.
ieee: F. Korc, V. Kolmogorov, and C. Lampert, Approximating marginals using discrete
energy minimization. IST Austria, 2012.
ista: Korc F, Kolmogorov V, Lampert C. 2012. Approximating marginals using discrete
energy minimization, IST Austria, 13p.
mla: Korc, Filip, et al. Approximating Marginals Using Discrete Energy Minimization.
IST Austria, 2012, doi:10.15479/AT:IST-2012-0003.
short: F. Korc, V. Kolmogorov, C. Lampert, Approximating Marginals Using Discrete
Energy Minimization, IST Austria, 2012.
date_created: 2018-12-12T11:39:06Z
date_published: 2012-07-23T00:00:00Z
date_updated: 2023-02-23T11:13:22Z
day: '23'
ddc:
- '000'
department:
- _id: VlKo
- _id: ChLa
doi: 10.15479/AT:IST-2012-0003
file:
- access_level: open_access
checksum: 7e0ba85ad123b13223aaf6cdde2d288c
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:29Z
date_updated: 2020-07-14T12:46:44Z
file_id: '5490'
file_name: IST-2012-0003_IST-2012-0003.pdf
file_size: 618744
relation: main_file
file_date_updated: 2020-07-14T12:46:44Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '13'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '36'
related_material:
record:
- id: '3124'
relation: earlier_version
status: public
status: public
title: Approximating marginals using discrete energy minimization
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '5377'
abstract:
- lang: eng
text: 'Two-player games on graphs are central in many problems in formal verification
and program analysis such as synthesis and verification of open systems. In this
work we consider solving recursive game graphs (or pushdown game graphs) that
can model the control flow of sequential programs with recursion. While pushdown
games have been studied before with qualitative objectives, such as reachability
and ω-regular objectives, in this work we study for the first time such games
with the most well-studied quantitative objective, namely, mean-payoff objectives.
In pushdown games two types of strategies are relevant: (1) global strategies,
that depend on the entire global history; and (2) modular strategies, that have
only local memory and thus do not depend on the context of invocation, but only
on the history of the current invocation of the module. Our main results are as
follows: (1) One-player pushdown games with mean-payoff objectives under global
strategies are decidable in polynomial time. (2) Two- player pushdown games with
mean-payoff objectives under global strategies are undecidable. (3) One-player
pushdown games with mean-payoff objectives under modular strategies are NP- hard.
(4) Two-player pushdown games with mean-payoff objectives under modular strategies
can be solved in NP (i.e., both one-player and two-player pushdown games with
mean-payoff objectives under modular strategies are NP-complete). We also establish
the optimal strategy complexity showing that global strategies for mean-payoff
objectives require infinite memory even in one-player pushdown games; and memoryless
modular strategies are sufficient in two- player pushdown games. Finally we also
show that all the problems have the same complexity if the stack boundedness condition
is added, where along with the mean-payoff objective the player must also ensure
that the stack height is bounded.'
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: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Velner Y. Mean-Payoff Pushdown Games. IST Austria; 2012.
doi:10.15479/AT:IST-2012-0002
apa: Chatterjee, K., & Velner, Y. (2012). Mean-payoff pushdown games.
IST Austria. https://doi.org/10.15479/AT:IST-2012-0002
chicago: Chatterjee, Krishnendu, and Yaron Velner. Mean-Payoff Pushdown Games.
IST Austria, 2012. https://doi.org/10.15479/AT:IST-2012-0002.
ieee: K. Chatterjee and Y. Velner, Mean-payoff pushdown games. IST Austria,
2012.
ista: Chatterjee K, Velner Y. 2012. Mean-payoff pushdown games, IST Austria, 33p.
mla: Chatterjee, Krishnendu, and Yaron Velner. Mean-Payoff Pushdown Games.
IST Austria, 2012, doi:10.15479/AT:IST-2012-0002.
short: K. Chatterjee, Y. Velner, Mean-Payoff Pushdown Games, IST Austria, 2012.
date_created: 2018-12-12T11:38:59Z
date_published: 2012-07-02T00:00:00Z
date_updated: 2023-02-23T11:05:50Z
day: '02'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2012-0002
file:
- access_level: open_access
checksum: a03c08c1589dbb0c96183a8bcf3ab240
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:00Z
date_updated: 2020-07-14T12:46:38Z
file_id: '5522'
file_name: IST-2012-002_IST-2012-0002.pdf
file_size: 592098
relation: main_file
file_date_updated: 2020-07-14T12:46:38Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '10'
related_material:
record:
- id: '2956'
relation: later_version
status: public
status: public
title: Mean-payoff pushdown games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '5378'
abstract:
- lang: eng
text: 'One central issue in the formal design and analysis of reactive systems is
the notion of refinement that asks whether all behaviors of the implementation
is allowed by the specification. The local interpretation of behavior leads to
the notion of simulation. Alternating transition systems (ATSs) provide a general
model for composite reactive systems, and the simulation relation for ATSs is
known as alternating simulation. The simulation relation for fair transition systems
is called fair simulation. In this work our main contributions are as follows:
(1) We present an improved algorithm for fair simulation with Büchi fairness constraints;
our algorithm requires O(n3 · m) time as compared to the previous known O(n6)-time
algorithm, where n is the number of states and m is the number of transitions.
(2) We present a game based algorithm for alternating simulation that requires
O(m2)-time as compared to the previous known O((n · m)2)-time algorithm, where
n is the number of states and m is the size of transition relation. (3) We present
an iterative algorithm for alternating simulation that matches the time complexity
of the game based algorithm, but is more space efficient than the game based algorithm.'
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: Siddhesh
full_name: Chaubal, Siddhesh
last_name: Chaubal
- first_name: Pritish
full_name: Kamath, Pritish
last_name: Kamath
citation:
ama: Chatterjee K, Chaubal S, Kamath P. Faster Algorithms for Alternating Refinement
Relations. IST Austria; 2012. doi:10.15479/AT:IST-2012-0001
apa: Chatterjee, K., Chaubal, S., & Kamath, P. (2012). Faster algorithms
for alternating refinement relations. IST Austria. https://doi.org/10.15479/AT:IST-2012-0001
chicago: Chatterjee, Krishnendu, Siddhesh Chaubal, and Pritish Kamath. Faster
Algorithms for Alternating Refinement Relations. IST Austria, 2012. https://doi.org/10.15479/AT:IST-2012-0001.
ieee: K. Chatterjee, S. Chaubal, and P. Kamath, Faster algorithms for alternating
refinement relations. IST Austria, 2012.
ista: Chatterjee K, Chaubal S, Kamath P. 2012. Faster algorithms for alternating
refinement relations, IST Austria, 21p.
mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Alternating Refinement
Relations. IST Austria, 2012, doi:10.15479/AT:IST-2012-0001.
short: K. Chatterjee, S. Chaubal, P. Kamath, Faster Algorithms for Alternating Refinement
Relations, IST Austria, 2012.
date_created: 2018-12-12T11:38:59Z
date_published: 2012-07-04T00:00:00Z
date_updated: 2023-02-23T12:21:38Z
day: '04'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2012-0001
file:
- access_level: open_access
checksum: ec8d1857cc7095d3de5107a0162ced37
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:28Z
date_updated: 2020-07-14T12:46:39Z
file_id: '5489'
file_name: IST-2012-0001_IST-2012-0001.pdf
file_size: 394256
relation: main_file
file_date_updated: 2020-07-14T12:46:39Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '21'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '14'
related_material:
record:
- id: '497'
relation: later_version
status: public
status: public
title: Faster algorithms for alternating refinement relations
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2012'
...