---
_id: '653'
abstract:
- lang: eng
text: The extent of heterogeneity among driver gene mutations present in naturally
occurring metastases - that is, treatment-naive metastatic disease - is largely
unknown. To address this issue, we carried out 60× whole-genome sequencing of
26 metastases from four patients with pancreatic cancer. We found that identical
mutations in known driver genes were present in every metastatic lesion for each
patient studied. Passenger gene mutations, which do not have known or predicted
functional consequences, accounted for all intratumoral heterogeneity. Even with
respect to these passenger mutations, our analysis suggests that the genetic similarity
among the founding cells of metastases was higher than that expected for any two
cells randomly taken from a normal tissue. The uniformity of known driver gene
mutations among metastases in the same patient has critical and encouraging implications
for the success of future targeted therapies in advanced-stage disease.
acknowledgement: 'We thank the Memorial Sloan Kettering Cancer Center Molecular Cytology
core facility for immunohistochemistry staining. This work was supported by Office
of Naval Research grant N00014-16-1-2914, the Bill and Melinda Gates Foundation
(OPP1148627), and a gift from B. Wu and E. Larson (M.A.N.), National Institutes
of Health grants CA179991 (C.A.I.-D. and I.B.), F31 CA180682 (A.P.M.-M.), CA43460
(B.V.), and P50 CA62924, the Monastra Foundation, the Virginia and D.K. Ludwig Fund
for Cancer Research, the Lustgarten Foundation for Pancreatic Cancer Research, the
Sol Goldman Center for Pancreatic Cancer Research, the Sol Goldman Sequencing Center,
ERC Start grant 279307: Graph Games (J.G.R., D.K., and C.K.), Austrian Science Fund
(FWF) grant P23499-N23 (J.G.R., D.K., and C.K.), and FWF NFN grant S11407-N23 RiSE/SHiNE
(J.G.R., D.K., and C.K.).'
article_processing_charge: No
article_type: original
author:
- first_name: Alvin
full_name: Makohon Moore, Alvin
last_name: Makohon Moore
- first_name: Ming
full_name: Zhang, Ming
last_name: Zhang
- 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: Božić, Ivana
last_name: Božić
- first_name: Benjamin
full_name: Allen, Benjamin
last_name: Allen
- first_name: Deepanjan
full_name: Kundu, Deepanjan
id: 1d4c0f4f-e8a3-11ec-a351-e36772758c45
last_name: Kundu
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Fay
full_name: Wong, Fay
last_name: Wong
- first_name: Yuchen
full_name: Jiao, Yuchen
last_name: Jiao
- first_name: Zachary
full_name: Kohutek, Zachary
last_name: Kohutek
- first_name: Jungeui
full_name: Hong, Jungeui
last_name: Hong
- first_name: Marc
full_name: Attiyeh, Marc
last_name: Attiyeh
- first_name: Breanna
full_name: Javier, Breanna
last_name: Javier
- first_name: Laura
full_name: Wood, Laura
last_name: Wood
- first_name: Ralph
full_name: Hruban, Ralph
last_name: Hruban
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
- first_name: Nickolas
full_name: Papadopoulos, Nickolas
last_name: Papadopoulos
- first_name: Kenneth
full_name: Kinzler, Kenneth
last_name: Kinzler
- first_name: Bert
full_name: Vogelstein, Bert
last_name: Vogelstein
- first_name: Christine
full_name: Iacobuzio Donahue, Christine
last_name: Iacobuzio Donahue
citation:
ama: Makohon Moore A, Zhang M, Reiter J, et al. Limited heterogeneity of known driver
gene mutations among the metastases of individual patients with pancreatic cancer.
Nature Genetics. 2017;49(3):358-366. doi:10.1038/ng.3764
apa: Makohon Moore, A., Zhang, M., Reiter, J., Božić, I., Allen, B., Kundu, D.,
… Iacobuzio Donahue, C. (2017). Limited heterogeneity of known driver gene mutations
among the metastases of individual patients with pancreatic cancer. Nature
Genetics. Nature Publishing Group. https://doi.org/10.1038/ng.3764
chicago: Makohon Moore, Alvin, Ming Zhang, Johannes Reiter, Ivana Božić, Benjamin
Allen, Deepanjan Kundu, Krishnendu Chatterjee, et al. “Limited Heterogeneity of
Known Driver Gene Mutations among the Metastases of Individual Patients with Pancreatic
Cancer.” Nature Genetics. Nature Publishing Group, 2017. https://doi.org/10.1038/ng.3764.
ieee: A. Makohon Moore et al., “Limited heterogeneity of known driver gene
mutations among the metastases of individual patients with pancreatic cancer,”
Nature Genetics, vol. 49, no. 3. Nature Publishing Group, pp. 358–366,
2017.
ista: Makohon Moore A, Zhang M, Reiter J, Božić I, Allen B, Kundu D, Chatterjee
K, Wong F, Jiao Y, Kohutek Z, Hong J, Attiyeh M, Javier B, Wood L, Hruban R, Nowak
M, Papadopoulos N, Kinzler K, Vogelstein B, Iacobuzio Donahue C. 2017. Limited
heterogeneity of known driver gene mutations among the metastases of individual
patients with pancreatic cancer. Nature Genetics. 49(3), 358–366.
mla: Makohon Moore, Alvin, et al. “Limited Heterogeneity of Known Driver Gene Mutations
among the Metastases of Individual Patients with Pancreatic Cancer.” Nature
Genetics, vol. 49, no. 3, Nature Publishing Group, 2017, pp. 358–66, doi:10.1038/ng.3764.
short: A. Makohon Moore, M. Zhang, J. Reiter, I. Božić, B. Allen, D. Kundu, K. Chatterjee,
F. Wong, Y. Jiao, Z. Kohutek, J. Hong, M. Attiyeh, B. Javier, L. Wood, R. Hruban,
M. Nowak, N. Papadopoulos, K. Kinzler, B. Vogelstein, C. Iacobuzio Donahue, Nature
Genetics 49 (2017) 358–366.
date_created: 2018-12-11T11:47:43Z
date_published: 2017-03-01T00:00:00Z
date_updated: 2022-06-10T09:55:08Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/ng.3764
ec_funded: 1
external_id:
pmid:
- '28092682'
file:
- access_level: open_access
checksum: e442dc3b7420a36ec805e9bb45cc1a2e
content_type: application/pdf
creator: dernst
date_created: 2019-11-19T08:13:50Z
date_updated: 2020-07-14T12:47:33Z
file_id: '7050'
file_name: 2017_NatureGenetics_Makohon.pdf
file_size: 908099
relation: main_file
file_date_updated: 2020-07-14T12:47:33Z
has_accepted_license: '1'
intvolume: ' 49'
issue: '3'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
page: 358 - 366
pmid: 1
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: Nature Genetics
publication_identifier:
issn:
- '10614036'
publication_status: published
publisher: Nature Publishing Group
publist_id: '7092'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Limited heterogeneity of known driver gene mutations among the metastases of
individual patients with pancreatic cancer
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 49
year: '2017'
...
---
_id: '13160'
abstract:
- lang: eng
text: "Transforming deterministic ω\r\n-automata into deterministic parity automata
is traditionally done using variants of appearance records. We present a more
efficient variant of this approach, tailored to Rabin automata, and several optimizations
applicable to all appearance records. We compare the methods experimentally and
find out that our method produces smaller automata than previous approaches. Moreover,
the experiments demonstrate the potential of our method for LTL synthesis, using
LTL-to-Rabin translators. It leads to significantly smaller parity automata when
compared to state-of-the-art approaches on complex formulae."
acknowledgement: This work is partially funded by the DFG project “Verified Model
Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Clara
full_name: Waldmann, Clara
last_name: Waldmann
- first_name: Maximilian
full_name: Weininger, Maximilian
last_name: Weininger
citation:
ama: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
for transforming Rabin automata into parity automata. In: Tools and Algorithms
for the Construction and Analysis of Systems. Vol 10205. Springer; 2017:443-460.
doi:10.1007/978-3-662-54577-5_26'
apa: 'Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2017).
Index appearance record for transforming Rabin automata into parity automata.
In Tools and Algorithms for the Construction and Analysis of Systems (Vol.
10205, pp. 443–460). Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54577-5_26'
chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
“Index Appearance Record for Transforming Rabin Automata into Parity Automata.”
In Tools and Algorithms for the Construction and Analysis of Systems, 10205:443–60.
Springer, 2017. https://doi.org/10.1007/978-3-662-54577-5_26.
ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
record for transforming Rabin automata into parity automata,” in Tools and
Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden,
2017, vol. 10205, pp. 443–460.
ista: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance
record for transforming Rabin automata into parity automata. Tools and Algorithms
for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.'
mla: Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata
into Parity Automata.” Tools and Algorithms for the Construction and Analysis
of Systems, vol. 10205, Springer, 2017, pp. 443–60, doi:10.1007/978-3-662-54577-5_26.
short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and
Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2017-04-22
date_created: 2023-06-21T13:21:14Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2023-06-21T13:29:46Z
day: '31'
department:
- _id: KrCh
doi: 10.1007/978-3-662-54577-5_26
external_id:
arxiv:
- '1701.05738'
intvolume: ' 10205'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.1701.05738
month: '03'
oa: 1
oa_version: Preprint
page: 443-460
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783662545775'
eissn:
- 1611-3349
isbn:
- '9783662545768'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
status: public
title: Index appearance record for transforming Rabin automata into parity automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10205
year: '2017'
...
---
_id: '1407'
abstract:
- lang: eng
text: We consider the problem of computing the set of initial states of a dynamical
system such that there exists a control strategy to ensure that the trajectories
satisfy a temporal logic specification with probability 1 (almost-surely). We
focus on discrete-time, stochastic linear dynamics and specifications given as
formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over
linear predicates in the states of the system. We propose a solution based on
iterative abstraction-refinement, and turn-based 2-player probabilistic games.
While the theoretical guarantee of our algorithm after any finite number of iterations
is only a partial solution, we show that if our algorithm terminates, then the
result is the set of all satisfying initial states. Moreover, for any (partial)
solution our algorithm synthesizes witness control strategies to ensure almost-sure
satisfaction of the temporal logic specification. While the proposed algorithm
guarantees progress and soundness in every iteration, it is computationally demanding.
We offer an alternative, more efficient solution for the reachability properties
that decomposes the problem into a series of smaller problems of the same type.
All algorithms are demonstrated on an illustrative case study.
article_processing_charge: No
arxiv: 1
author:
- first_name: Mária
full_name: Svoreňová, Mária
last_name: Svoreňová
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ivana
full_name: Cěrná, Ivana
last_name: Cěrná
- first_name: Cǎlin
full_name: Belta, Cǎlin
last_name: Belta
citation:
ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal
logic control for stochastic linear systems using abstraction refinement of probabilistic
games. Nonlinear Analysis: Hybrid Systems. 2017;23(2):230-253. doi:10.1016/j.nahs.2016.04.006'
apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &
Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction
refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems.
Elsevier. https://doi.org/10.1016/j.nahs.2016.04.006'
chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee,
Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid
Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.04.006.'
ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta,
“Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games,” Nonlinear Analysis: Hybrid Systems, vol. 23, no.
2. Elsevier, pp. 230–253, 2017.'
ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017.
Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253.'
mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid
Systems, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:10.1016/j.nahs.2016.04.006.'
short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta,
Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.'
date_created: 2018-12-11T11:51:50Z
date_published: 2017-02-01T00:00:00Z
date_updated: 2023-09-20T09:43:09Z
day: '01'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1016/j.nahs.2016.04.006
ec_funded: 1
external_id:
arxiv:
- '1410.5387'
isi:
- '000390637000014'
intvolume: ' 23'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1410.5387
month: '02'
oa: 1
oa_version: Preprint
page: 230 - 253
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_status: published
publisher: Elsevier
publist_id: '5800'
quality_controlled: '1'
related_material:
record:
- id: '1689'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 23
year: '2017'
...
---
_id: '949'
abstract:
- lang: eng
text: The notion of treewidth of graphs has been exploited for faster algorithms
for several problems arising in verification and program analysis. Moreover, various
notions of balanced tree decompositions have been used for improved algorithms
supporting dynamic updates and analysis of concurrent programs. In this work,
we present a tool for constructing tree-decompositions of CFGs obtained from Java
methods, which is implemented as an extension to the widely used Soot framework.
The experimental results show that our implementation on real-world Java benchmarks
is very efficient. Our tool also provides the first implementation for balancing
tree-decompositions. In summary, we present the first tool support for exploiting
treewidth in the static analysis problems on Java programs.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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, Goharshady AK, Pavlogiannis A. JTDec: A tool for tree decompositions
in soot. In: D’Souza D, ed. Vol 10482. Springer; 2017:59-66. doi:10.1007/978-3-319-68167-2_4'
apa: 'Chatterjee, K., Goharshady, A. K., & Pavlogiannis, A. (2017). JTDec: A
tool for tree decompositions in soot. In D. D’Souza (Ed.) (Vol. 10482, pp. 59–66).
Presented at the ATVA: Automated Technology for Verification and Analysis, Pune,
India: Springer. https://doi.org/10.1007/978-3-319-68167-2_4'
chicago: 'Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Andreas Pavlogiannis.
“JTDec: A Tool for Tree Decompositions in Soot.” edited by Deepak D’Souza, 10482:59–66.
Springer, 2017. https://doi.org/10.1007/978-3-319-68167-2_4.'
ieee: 'K. Chatterjee, A. K. Goharshady, and A. Pavlogiannis, “JTDec: A tool for
tree decompositions in soot,” presented at the ATVA: Automated Technology for
Verification and Analysis, Pune, India, 2017, vol. 10482, pp. 59–66.'
ista: 'Chatterjee K, Goharshady AK, Pavlogiannis A. 2017. JTDec: A tool for tree
decompositions in soot. ATVA: Automated Technology for Verification and Analysis,
LNCS, vol. 10482, 59–66.'
mla: 'Chatterjee, Krishnendu, et al. JTDec: A Tool for Tree Decompositions in
Soot. Edited by Deepak D’Souza, vol. 10482, Springer, 2017, pp. 59–66, doi:10.1007/978-3-319-68167-2_4.'
short: K. Chatterjee, A.K. Goharshady, A. Pavlogiannis, in:, D. D’Souza (Ed.), Springer,
2017, pp. 59–66.
conference:
end_date: 2017-10-06
location: Pune, India
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2017-10-03
date_created: 2018-12-11T11:49:22Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2024-03-25T23:30:19Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.1007/978-3-319-68167-2_4
ec_funded: 1
editor:
- first_name: Deepak
full_name: D'Souza, Deepak
last_name: D'Souza
external_id:
isi:
- '000723567800004'
file:
- access_level: open_access
checksum: a0d9f5f94dc594c4e71e78525c9942f1
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:45Z
date_updated: 2020-07-14T12:48:16Z
file_id: '4835'
file_name: IST-2017-845-v1+1_2017_Chatterjee_JTDec.pdf
file_size: 948514
relation: main_file
file_date_updated: 2020-07-14T12:48:16Z
has_accepted_license: '1'
intvolume: ' 10482'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 59 - 66
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6468'
pubrep_id: '845'
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: 'JTDec: A tool for tree decompositions in soot'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10482
year: '2017'
...
---
_id: '950'
abstract:
- lang: eng
text: "Two-player games on graphs are widely studied in formal methods as they model
the interaction between a system and its environment. The game is played by moving
a token throughout a graph to produce an infinite path. There are several common
modes to determine how the players move the token through the graph; e.g., in
turn-based games the players alternate turns in moving the token. We study the
bidding mode of moving the token, which, to the best of our knowledge, has never
been studied in infinite-duration games. Both players have separate budgets, which
sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously,
and a bid is legal if it does not exceed the available budget. The winner of the
bidding pays his bid to the other player and moves the token. For reachability
objectives, repeated bidding games have been studied and are called Richman games.
There, a central question is the existence and computation of threshold budgets;
namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win
the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity
games and mean-payoff games. We show the existence of threshold budgets in these
games, and reduce the problem of finding them to Richman games. We also determine
the strategy-complexity of an optimal strategy. Our most interesting result shows
that memoryless strategies suffice for mean-payoff bidding games. \r\n"
alternative_title:
- LIPIcs
article_number: '17'
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
citation:
ama: 'Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol
85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.21'
apa: 'Avni, G., Henzinger, T. A., & Chonev, V. K. (2017). Infinite-duration
bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin,
Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21'
chicago: Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration
Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
https://doi.org/10.4230/LIPIcs.CONCUR.2017.21.
ieee: 'G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,”
presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.'
ista: 'Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR:
Concurrency Theory, LIPIcs, vol. 85, 17.'
mla: Avni, Guy, et al. Infinite-Duration Bidding Games. Vol. 85, 17, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.21.
short: G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2017.
conference:
end_date: 2017-09-07
location: Berlin, Germany
name: 'CONCUR: Concurrency Theory'
start_date: 2017-09-05
date_created: 2018-12-11T11:49:22Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-08-29T07:02:13Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2017.21
external_id:
arxiv:
- '1705.01433'
file:
- access_level: open_access
checksum: 6d5cccf755207b91ccbef95d8275b013
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:00Z
date_updated: 2020-07-14T12:48:16Z
file_id: '5318'
file_name: IST-2017-844-v1+1_concur-cr.pdf
file_size: 335170
relation: main_file
file_date_updated: 2020-07-14T12:48:16Z
has_accepted_license: '1'
intvolume: ' 85'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6466'
pubrep_id: '844'
quality_controlled: '1'
related_material:
record:
- id: '6752'
relation: later_version
status: public
scopus_import: 1
status: public
title: Infinite-duration bidding games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 85
year: '2017'
...
---
_id: '1009'
abstract:
- lang: eng
text: A standard objective in partially-observable Markov decision processes (POMDPs)
is to find a policy that maximizes the expected discounted-sum payoff. However,
such policies may still permit unlikely but highly undesirable outcomes, which
is problematic especially in safety-critical applications. Recently, there has
been a surge of interest in POMDPs where the goal is to maximize the probability
to ensure that the payoff is at least a given threshold, but these approaches
do not consider any optimization beyond satisfying this threshold constraint.
In this work we go beyond both the “expectation” and “threshold” approaches and
consider a “guaranteed payoff optimization (GPO)” problem for POMDPs, where we
are given a threshold t and the objective is to find a policy σ such that a) each
possible outcome of σ yields a discounted-sum payoff of at least t, and b) the
expected discounted-sum payoff of σ is optimal (or near-optimal) among all policies
satisfying a). We present a practical approach to tackle the GPO problem and evaluate
it on standard POMDP benchmarks.
acknowledgement: 'he research leading to these results was supported by the Austrian
Science Fund (FWF) NFN Grant no. S11407-N23 (RiSE/SHiNE); two ERC Starting grants
(279307: Graph Games, 279499: inVEST); the Vienna Science and Tech- nology Fund
(WWTF) through project ICT15-003; and the People Programme (Marie Curie Actions)
of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant
agreement no. [291734].'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Guillermo
full_name: Pérez, Guillermo
last_name: Pérez
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
- first_name: Djordje
full_name: Zikelic, Djordje
last_name: Zikelic
citation:
ama: 'Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. Optimizing expectation
with guarantees in POMDPs. In: Proceedings of the 31st AAAI Conference on Artificial
Intelligence. Vol 5. AAAI Press; 2017:3725-3732.'
apa: 'Chatterjee, K., Novotný, P., Pérez, G., Raskin, J., & Zikelic, D. (2017).
Optimizing expectation with guarantees in POMDPs. In Proceedings of the 31st
AAAI Conference on Artificial Intelligence (Vol. 5, pp. 3725–3732). San Francisco,
CA, United States: AAAI Press.'
chicago: Chatterjee, Krishnendu, Petr Novotný, Guillermo Pérez, Jean Raskin, and
Djordje Zikelic. “Optimizing Expectation with Guarantees in POMDPs.” In Proceedings
of the 31st AAAI Conference on Artificial Intelligence, 5:3725–32. AAAI Press,
2017.
ieee: K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, and D. Zikelic, “Optimizing
expectation with guarantees in POMDPs,” in Proceedings of the 31st AAAI Conference
on Artificial Intelligence, San Francisco, CA, United States, 2017, vol. 5,
pp. 3725–3732.
ista: 'Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. 2017. Optimizing expectation
with guarantees in POMDPs. Proceedings of the 31st AAAI Conference on Artificial
Intelligence. AAAI: Conference on Artificial Intelligence vol. 5, 3725–3732.'
mla: Chatterjee, Krishnendu, et al. “Optimizing Expectation with Guarantees in POMDPs.”
Proceedings of the 31st AAAI Conference on Artificial Intelligence, vol.
5, AAAI Press, 2017, pp. 3725–32.
short: K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, D. Zikelic, in:, Proceedings
of the 31st AAAI Conference on Artificial Intelligence, AAAI Press, 2017, pp.
3725–3732.
conference:
end_date: 2017-02-10
location: San Francisco, CA, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2017-02-04
date_created: 2018-12-11T11:49:40Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2025-06-02T08:53:49Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
external_id:
isi:
- '000485630703107'
intvolume: ' 5'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://www.aaai.org/ocs/index.php/AAAI/AAAI17/paper/download/14354/14092
month: '01'
oa: 1
oa_version: Submitted Version
page: 3725 - 3732
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the 31st AAAI Conference on Artificial Intelligence
publication_status: published
publisher: AAAI Press
publist_id: '6387'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Optimizing expectation with guarantees in POMDPs
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 5
year: '2017'
...
---
_id: '1011'
abstract:
- lang: eng
text: Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly
equivalent, are standard models for interprocedural analysis. Yet RSMs are more
convenient as they (a) explicitly model function calls and returns, and (b) specify
many natural parameters for algorithmic analysis, e.g., the number of entries
and exits. We consider a general framework where RSM transitions are labeled from
a semiring and path properties are algebraic with semiring operations, which can
model, e.g., interprocedural reachability and dataflow analysis problems. Our
main contributions are new algorithms for several fundamental problems. As compared
to a direct translation of RSMs to PDSs and the best-known existing bounds of
PDSs, our analysis algorithm improves the complexity for finite-height semirings
(that subsumes reachability and standard dataflow properties). We further consider
the problem of extracting distance values from the representation structures computed
by our algorithm, and give efficient algorithms that distinguish the complexity
of a one-time preprocessing from the complexity of each individual query. Another
advantage of our algorithm is that our improvements carry over to the concurrent
setting, where we improve the bestknown complexity for the context-bounded analysis
of concurrent RSMs. Finally, we provide a prototype implementation that gives
a significant speed-up on several benchmarks from the SLAM/SDV project.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
orcid: 0000-0001-7745-9117
- first_name: Samarth
full_name: Mishra, Samarth
last_name: Mishra
- 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, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted
recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:10.1007/978-3-662-54434-1_11'
apa: 'Chatterjee, K., Kragl, B., Mishra, S., & Pavlogiannis, A. (2017). Faster
algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201,
pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala,
Sweden: Springer. https://doi.org/10.1007/978-3-662-54434-1_11'
chicago: Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis.
“Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok
Yang, 10201:287–313. Springer, 2017. https://doi.org/10.1007/978-3-662-54434-1_11.
ieee: 'K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms
for weighted recursive state machines,” presented at the ESOP: European Symposium
on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.'
ista: 'Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms
for weighted recursive state machines. ESOP: European Symposium on Programming,
LNCS, vol. 10201, 287–313.'
mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Weighted Recursive
State Machines. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313,
doi:10.1007/978-3-662-54434-1_11.
short: K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.),
Springer, 2017, pp. 287–313.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'ESOP: European Symposium on Programming'
start_date: 2017-04-22
date_created: 2018-12-11T11:49:41Z
date_published: 2017-03-19T00:00:00Z
date_updated: 2023-09-22T09:44:50Z
day: '19'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-54434-1_11
ec_funded: 1
editor:
- first_name: Hongseok
full_name: Yang, Hongseok
last_name: Yang
external_id:
isi:
- '000681702400011'
intvolume: ' 10201'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1701.04914
month: '03'
oa: 1
oa_version: Submitted Version
page: 287 - 313
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6384'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for weighted recursive state machines
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10201
year: '2017'
...
---
_id: '10416'
abstract:
- lang: eng
text: 'A fundamental algorithmic problem at the heart of static analysis is Dyck
reachability. The input is a graph where the edges are labeled with different
types of opening and closing parentheses, and the reachability information is
computed via paths whose parentheses are properly matched. We present new results
for Dyck reachability problems with applications to alias analysis and data-dependence
analysis. Our main contributions, that include improved upper bounds as well as
lower bounds that establish optimality guarantees, are as follows: First, we consider
Dyck reachability on bidirected graphs, which is the standard way of performing
field-sensitive points-to analysis. Given a bidirected graph with n nodes and
m edges, we present: (i) an algorithm with worst-case running time O(m + n · α(n)),
where α(n) is the inverse Ackermann function, improving the previously known O(n2)
time bound; (ii) a matching lower bound that shows that our algorithm is optimal
wrt to worst-case complexity; and (iii) an optimal average-case upper bound of
O(m) time, improving the previously known O(m · logn) bound. Second, we consider
the problem of context-sensitive data-dependence analysis, where the task is to
obtain analysis summaries of library code in the presence of callbacks. Our algorithm
preprocesses libraries in almost linear time, after which the contribution of
the library in the complexity of the client analysis is only linear, and only
wrt the number of call sites. Third, we prove that combinatorial algorithms for
Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained
without obtaining sub-cubic combinatorial algorithms for Boolean Matrix Multiplication,
which is a long-standing open problem. Thus we establish that the existing combinatorial
algorithms for Dyck reachability are (conditionally) optimal for general graphs.
We also show that the same hardness holds for graphs of constant treewidth. Finally,
we provide a prototype implementation of our algorithms for both alias analysis
and data-dependence analysis. Our experimental evaluation demonstrates that the
new algorithms significantly outperform all existing methods on the two problems,
over real-world benchmarks.'
acknowledgement: "The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Start grant
(279307: Graph Games).\r\n"
article_number: '30'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Bhavya
full_name: Choudhary, Bhavya
last_name: Choudhary
- 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, Choudhary B, Pavlogiannis A. Optimal Dyck reachability for data-dependence
and Alias analysis. Proceedings of the ACM on Programming Languages. 2017;2(POPL).
doi:10.1145/3158118
apa: 'Chatterjee, K., Choudhary, B., & Pavlogiannis, A. (2017). Optimal Dyck
reachability for data-dependence and Alias analysis. Proceedings of the ACM
on Programming Languages. Los Angeles, CA, United States: Association for
Computing Machinery. https://doi.org/10.1145/3158118'
chicago: Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. “Optimal
Dyck Reachability for Data-Dependence and Alias Analysis.” Proceedings of the
ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158118.
ieee: K. Chatterjee, B. Choudhary, and A. Pavlogiannis, “Optimal Dyck reachability
for data-dependence and Alias analysis,” Proceedings of the ACM on Programming
Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.
ista: Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability
for data-dependence and Alias analysis. Proceedings of the ACM on Programming
Languages. 2(POPL), 30.
mla: Chatterjee, Krishnendu, et al. “Optimal Dyck Reachability for Data-Dependence
and Alias Analysis.” Proceedings of the ACM on Programming Languages, vol.
2, no. POPL, 30, Association for Computing Machinery, 2017, doi:10.1145/3158118.
short: K. Chatterjee, B. Choudhary, A. Pavlogiannis, Proceedings of the ACM on Programming
Languages 2 (2017).
conference:
end_date: 2018-01-13
location: Los Angeles, CA, United States
name: 'POPL: Programming Languages'
start_date: 2018-01-07
date_created: 2021-12-05T23:01:48Z
date_published: 2017-12-27T00:00:00Z
date_updated: 2023-02-23T12:27:13Z
day: '27'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3158118
ec_funded: 1
external_id:
arxiv:
- '1910.00241'
file:
- access_level: open_access
checksum: faa3f7b3fe8aab84b50ed805c26a0ee5
content_type: application/pdf
creator: cchlebak
date_created: 2021-12-07T08:06:28Z
date_updated: 2021-12-07T08:06:28Z
file_id: '10421'
file_name: 2017_ACMProgLang_Chatterjee.pdf
file_size: 460188
relation: main_file
success: 1
file_date_updated: 2021-12-07T08:06:28Z
has_accepted_license: '1'
intvolume: ' 2'
issue: POPL
language:
- iso: eng
month: '12'
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: 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
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '5455'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Optimal Dyck reachability for data-dependence and Alias analysis
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: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
---
_id: '10417'
abstract:
- lang: eng
text: "We present a new dynamic partial-order reduction method for stateless model
checking of concurrent programs. A common approach for exploring program behaviors
relies on enumerating the traces of the program, without storing the visited states
(aka stateless exploration). As the number of distinct traces grows exponentially,
dynamic partial-order reduction (DPOR) techniques have been successfully used
to partition the space of traces into equivalence classes (Mazurkiewicz partitioning),
with the goal of exploring only few representative traces from each class.\r\n\r\nWe
introduce a new equivalence on traces under sequential consistency semantics,
which we call the observation equivalence. Two traces are observationally equivalent
if every read event observes the same write event in both traces. While the traditional
Mazurkiewicz equivalence is control-centric, our new definition is data-centric.
We show that our observation equivalence is coarser than the Mazurkiewicz equivalence,
and in many cases even exponentially coarser. We devise a DPOR exploration of
the trace space, called data-centric DPOR, based on the observation equivalence."
acknowledgement: "The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499- N23, FWF\r\nNFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant
(279307: Graph Games), and Czech\r\nScience Foundation grant GBP202/12/G061."
article_number: '31'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
last_name: Chalupa
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Nishant
full_name: Sinha, Nishant
last_name: Sinha
- first_name: Kapil
full_name: Vaidya, Kapil
last_name: Vaidya
citation:
ama: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-centric dynamic
partial order reduction. Proceedings of the ACM on Programming Languages.
2017;2(POPL). doi:10.1145/3158119
apa: 'Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., & Vaidya, K.
(2017). Data-centric dynamic partial order reduction. Proceedings of the ACM
on Programming Languages. Los Angeles, CA, United States: Association for
Computing Machinery. https://doi.org/10.1145/3158119'
chicago: Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha,
and Kapil Vaidya. “Data-Centric Dynamic Partial Order Reduction.” Proceedings
of the ACM on Programming Languages. Association for Computing Machinery,
2017. https://doi.org/10.1145/3158119.
ieee: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, “Data-centric
dynamic partial order reduction,” Proceedings of the ACM on Programming Languages,
vol. 2, no. POPL. Association for Computing Machinery, 2017.
ista: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric
dynamic partial order reduction. Proceedings of the ACM on Programming Languages.
2(POPL), 31.
mla: Chalupa, Marek, et al. “Data-Centric Dynamic Partial Order Reduction.” Proceedings
of the ACM on Programming Languages, vol. 2, no. POPL, 31, Association for
Computing Machinery, 2017, doi:10.1145/3158119.
short: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings
of the ACM on Programming Languages 2 (2017).
conference:
end_date: 2018-01-13
location: Los Angeles, CA, United States
name: 'POPL: Programming Languages'
start_date: 2018-01-07
date_created: 2021-12-05T23:01:49Z
date_published: 2017-12-27T00:00:00Z
date_updated: 2023-02-23T12:27:16Z
day: '27'
department:
- _id: KrCh
doi: 10.1145/3158119
ec_funded: 1
external_id:
arxiv:
- '1610.01188'
intvolume: ' 2'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://dl.acm.org/doi/10.1145/3158119
month: '12'
oa: 1
oa_version: Published Version
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'
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '5448'
relation: earlier_version
status: public
- id: '5456'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Data-centric dynamic partial order reduction
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
---
_id: '10418'
abstract:
- lang: eng
text: We present a new proof rule for proving almost-sure termination of probabilistic
programs, including those that contain demonic non-determinism. An important question
for a probabilistic program is whether the probability mass of all its diverging
runs is zero, that is that it terminates "almost surely". Proving that can be
hard, and this paper presents a new method for doing so. It applies directly to
the program's source code, even if the program contains demonic choice. Like others,
we use variant functions (a.k.a. "super-martingales") that are real-valued and
decrease randomly on each loop iteration; but our key innovation is that the amount
as well as the probability of the decrease are parametric. We prove the soundness
of the new rule, indicate where its applicability goes beyond existing rules,
and explain its connection to classical results on denumerable (non-demonic) Markov
chains.
acknowledgement: "McIver and Morgan are grateful to David Basin and the Information
Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during
part of which this work began. And thanks particularly to Andreas Lochbihler, who
shared with us the probabilistic termination problem that led to it. They acknowledge
the support of ARC grant DP140101119. Part of this work was carried out during the
Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs
Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden.
Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4."
article_number: '33'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Annabelle
full_name: Mciver, Annabelle
last_name: Mciver
- first_name: Carroll
full_name: Morgan, Carroll
last_name: Morgan
- first_name: Benjamin Lucien
full_name: Kaminski, Benjamin Lucien
last_name: Kaminski
- first_name: Joost P
full_name: Katoen, Joost P
id: 4524F760-F248-11E8-B48F-1D18A9856A87
last_name: Katoen
citation:
ama: Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure
termination. Proceedings of the ACM on Programming Languages. 2017;2(POPL).
doi:10.1145/3158121
apa: 'Mciver, A., Morgan, C., Kaminski, B. L., & Katoen, J. P. (2017). A new
proof rule for almost-sure termination. Proceedings of the ACM on Programming
Languages. Los Angeles, CA, United States: Association for Computing Machinery.
https://doi.org/10.1145/3158121'
chicago: Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost
P Katoen. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the
ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158121.
ieee: A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule
for almost-sure termination,” Proceedings of the ACM on Programming Languages,
vol. 2, no. POPL. Association for Computing Machinery, 2017.
ista: Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure
termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.
mla: Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” Proceedings
of the ACM on Programming Languages, vol. 2, no. POPL, 33, Association for
Computing Machinery, 2017, doi:10.1145/3158121.
short: A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM
on Programming Languages 2 (2017).
conference:
end_date: 2018-01-13
location: Los Angeles, CA, United States
name: 'POPL: Programming Languages'
start_date: 2018-01-07
date_created: 2021-12-05T23:01:49Z
date_published: 2017-12-07T00:00:00Z
date_updated: 2021-12-07T08:04:14Z
day: '07'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/3158121
external_id:
arxiv:
- '1711.03588'
intvolume: ' 2'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://dl.acm.org/doi/10.1145/3158121
month: '12'
oa: 1
oa_version: Published Version
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: A new proof rule for almost-sure termination
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
---
_id: '1065'
abstract:
- lang: eng
text: 'We consider the problem of reachability in pushdown graphs. We study the
problem for pushdown graphs with constant treewidth. Even for pushdown graphs
with treewidth 1, for the reachability problem we establish the following: (i)
the problem is PTIME-complete, and (ii) any subcubic algorithm for the problem
would contradict the k-clique conjecture and imply faster combinatorial algorithms
for cliques in graphs.'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Georg F
full_name: Osang, Georg F
id: 464B40D6-F248-11E8-B48F-1D18A9856A87
last_name: Osang
orcid: 0000-0002-8882-5116
citation:
ama: Chatterjee K, Osang GF. Pushdown reachability with constant treewidth. Information
Processing Letters. 2017;122:25-29. doi:10.1016/j.ipl.2017.02.003
apa: Chatterjee, K., & Osang, G. F. (2017). Pushdown reachability with constant
treewidth. Information Processing Letters. Elsevier. https://doi.org/10.1016/j.ipl.2017.02.003
chicago: Chatterjee, Krishnendu, and Georg F Osang. “Pushdown Reachability with
Constant Treewidth.” Information Processing Letters. Elsevier, 2017. https://doi.org/10.1016/j.ipl.2017.02.003.
ieee: K. Chatterjee and G. F. Osang, “Pushdown reachability with constant treewidth,”
Information Processing Letters, vol. 122. Elsevier, pp. 25–29, 2017.
ista: Chatterjee K, Osang GF. 2017. Pushdown reachability with constant treewidth.
Information Processing Letters. 122, 25–29.
mla: Chatterjee, Krishnendu, and Georg F. Osang. “Pushdown Reachability with Constant
Treewidth.” Information Processing Letters, vol. 122, Elsevier, 2017, pp.
25–29, doi:10.1016/j.ipl.2017.02.003.
short: K. Chatterjee, G.F. Osang, Information Processing Letters 122 (2017) 25–29.
date_created: 2018-12-11T11:49:57Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-09-20T12:08:18Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: HeEd
doi: 10.1016/j.ipl.2017.02.003
ec_funded: 1
external_id:
isi:
- '000399506600005'
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:17Z
date_updated: 2019-10-15T07:44:51Z
file_id: '4998'
file_name: IST-2018-991-v1+2_2018_Chatterjee_Pushdown_PREPRINT.pdf
file_size: 247657
relation: main_file
file_date_updated: 2019-10-15T07:44:51Z
has_accepted_license: '1'
intvolume: ' 122'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 25 - 29
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Information Processing Letters
publication_identifier:
issn:
- '00200190'
publication_status: published
publisher: Elsevier
publist_id: '6323'
pubrep_id: '991'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Pushdown reachability with constant treewidth
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 122
year: '2017'
...
---
_id: '1194'
abstract:
- lang: eng
text: 'Termination is one of the basic liveness properties, and we study the termination
problem for probabilistic programs with real-valued variables. Previous works
focused on the qualitative problem that asks whether an input program terminates
with probability~1 (almost-sure termination). A powerful approach for this qualitative
problem is the notion of ranking supermartingales with respect to a given set
of invariants. The quantitative problem (probabilistic termination) asks for bounds
on the termination probability. A fundamental and conceptual drawback of the existing
approaches to address probabilistic termination is that even though the supermartingales
consider the probabilistic behavior of the programs, the invariants are obtained
completely ignoring the probabilistic aspect. In this work we address the probabilistic
termination problem for linear-arithmetic probabilistic programs with nondeterminism.
We define the notion of {\em stochastic invariants}, which are constraints along
with a probability bound that the constraints hold. We introduce a concept of
{\em repulsing supermartingales}. First, we show that repulsing supermartingales
can be used to obtain bounds on the probability of the stochastic invariants.
Second, we show the effectiveness of repulsing supermartingales in the following
three ways: (1)~With a combination of ranking and repulsing supermartingales we
can compute lower bounds on the probability of termination; (2)~repulsing supermartingales
provide witnesses for refutation of almost-sure termination; and (3)~with a combination
of ranking and repulsing supermartingales we can establish persistence properties
of probabilistic programs. We also present results on related computational problems
and an experimental evaluation of our approach on academic examples. '
alternative_title:
- ACM SIGPLAN Notices
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Djordje
full_name: Zikelic, Djordje
last_name: Zikelic
citation:
ama: 'Chatterjee K, Novotný P, Zikelic D. Stochastic invariants for probabilistic
termination. In: Vol 52. ACM; 2017:145-160. doi:10.1145/3009837.3009873'
apa: 'Chatterjee, K., Novotný, P., & Zikelic, D. (2017). Stochastic invariants
for probabilistic termination (Vol. 52, pp. 145–160). Presented at the POPL: Principles
of Programming Languages, Paris, France: ACM. https://doi.org/10.1145/3009837.3009873'
chicago: Chatterjee, Krishnendu, Petr Novotný, and Djordje Zikelic. “Stochastic
Invariants for Probabilistic Termination,” 52:145–60. ACM, 2017. https://doi.org/10.1145/3009837.3009873.
ieee: 'K. Chatterjee, P. Novotný, and D. Zikelic, “Stochastic invariants for probabilistic
termination,” presented at the POPL: Principles of Programming Languages, Paris,
France, 2017, vol. 52, no. 1, pp. 145–160.'
ista: 'Chatterjee K, Novotný P, Zikelic D. 2017. Stochastic invariants for probabilistic
termination. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol.
52, 145–160.'
mla: Chatterjee, Krishnendu, et al. Stochastic Invariants for Probabilistic Termination.
Vol. 52, no. 1, ACM, 2017, pp. 145–60, doi:10.1145/3009837.3009873.
short: K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.
conference:
end_date: 2017-01-21
location: Paris, France
name: 'POPL: Principles of Programming Languages'
start_date: 2017-01-15
date_created: 2018-12-11T11:50:39Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2025-07-14T09:09:58Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3009837.3009873
ec_funded: 1
external_id:
isi:
- '000408311200013'
intvolume: ' 52'
isi: 1
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1611.01063
month: '01'
oa: 1
oa_version: Submitted Version
page: 145 - 160
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_identifier:
issn:
- '07308566'
publication_status: published
publisher: ACM
publist_id: '6157'
quality_controlled: '1'
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Stochastic invariants for probabilistic termination
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 52
year: '2017'
...
---
_id: '1294'
abstract:
- lang: eng
text: We study controller synthesis problems for finite-state Markov decision processes,
where the objective is to optimize the expected mean-payoff performance and stability
(also known as variability in the literature). We argue that the basic notion
of expressing the stability using the statistical variance of the mean payoff
is sometimes insufficient, and propose an alternative definition. We show that
a strategy ensuring both the expected mean payoff and the variance below given
bounds requires randomization and memory, under both the above definitions. We
then show that the problem of finding such a strategy can be expressed as a set
of constraints.
article_processing_charge: No
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
citation:
ama: Brázdil T, Chatterjee K, Forejt V, Kučera A. Trading performance for stability
in Markov decision processes. Journal of Computer and System Sciences.
2017;84:144-170. doi:10.1016/j.jcss.2016.09.009
apa: Brázdil, T., Chatterjee, K., Forejt, V., & Kučera, A. (2017). Trading performance
for stability in Markov decision processes. Journal of Computer and System
Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2016.09.009
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera.
“Trading Performance for Stability in Markov Decision Processes.” Journal of
Computer and System Sciences. Elsevier, 2017. https://doi.org/10.1016/j.jcss.2016.09.009.
ieee: T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Trading performance
for stability in Markov decision processes,” Journal of Computer and System
Sciences, vol. 84. Elsevier, pp. 144–170, 2017.
ista: Brázdil T, Chatterjee K, Forejt V, Kučera A. 2017. Trading performance for
stability in Markov decision processes. Journal of Computer and System Sciences.
84, 144–170.
mla: Brázdil, Tomáš, et al. “Trading Performance for Stability in Markov Decision
Processes.” Journal of Computer and System Sciences, vol. 84, Elsevier,
2017, pp. 144–70, doi:10.1016/j.jcss.2016.09.009.
short: T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, Journal of Computer and
System Sciences 84 (2017) 144–170.
date_created: 2018-12-11T11:51:12Z
date_published: 2017-03-01T00:00:00Z
date_updated: 2023-09-20T11:15:31Z
day: '01'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.1016/j.jcss.2016.09.009
ec_funded: 1
external_id:
isi:
- '000388430000011'
file:
- access_level: open_access
checksum: 91271b23cf884d7c06d33bef0cd623b1
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:30Z
date_updated: 2020-07-14T12:44:42Z
file_id: '4885'
file_name: IST-2016-717-v1+1_1-s2.0-S0022000016300897-main.pdf
file_size: 708657
relation: main_file
file_date_updated: 2020-07-14T12:44:42Z
has_accepted_license: '1'
intvolume: ' 84'
isi: 1
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: 144 - 170
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Elsevier
publist_id: '6009'
pubrep_id: '717'
quality_controlled: '1'
related_material:
record:
- id: '2305'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Trading performance for stability in Markov decision processes
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 84
year: '2017'
...
---
_id: '1068'
abstract:
- lang: eng
text: 'Games on graphs provide the appropriate framework to study several central
problems in computer science, such as verification and synthesis of reactive systems.
One of the most basic objectives for games on graphs is the liveness (or Büchi)
objective that given a target set of vertices requires that some vertex in the
target set is visited infinitely often. We study generalized Büchi objectives
(i.e., conjunction of liveness objectives), and implications between two generalized
Büchi objectives (known as GR(1) objectives), that arise in numerous applications
in computer-aided verification. We present improved algorithms and conditional
super-linear lower bounds based on widely believed assumptions about the complexity
of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider
graph games with n vertices, m edges, and generalized Büchi objectives with k
conjunctions. First, we present an algorithm with running time O(k*n^2), improving
the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm
is optimal for dense graphs under (A1). Second, we show that the basic algorithm
for the problem is optimal for sparse graphs when the target sets have constant
size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions
in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1
k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time
algorithm for m > n^{1.5}. '
acknowledgement: K. C., M. H., and W. D. are partially supported by the Vienna Science
and Technology Fund (WWTF) through project ICT15-003. K. C. is partially supported
by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC
Start grant (279307
alternative_title:
- LIPIcs
article_number: '25'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Wolfgang
full_name: Dvorák, Wolfgang
last_name: Dvorák
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Veronika
full_name: Loitzenbauer, Veronika
last_name: Loitzenbauer
citation:
ama: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. Conditionally optimal
algorithms for generalized Büchi Games. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2016. doi:10.4230/LIPIcs.MFCS.2016.25'
apa: 'Chatterjee, K., Dvorák, W., Henzinger, M. H., & Loitzenbauer, V. (2016).
Conditionally optimal algorithms for generalized Büchi Games (Vol. 58). Presented
at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow, Poland:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2016.25'
chicago: Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Veronika
Loitzenbauer. “Conditionally Optimal Algorithms for Generalized Büchi Games,”
Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.MFCS.2016.25.
ieee: 'K. Chatterjee, W. Dvorák, M. H. Henzinger, and V. Loitzenbauer, “Conditionally
optimal algorithms for generalized Büchi Games,” presented at the MFCS: Mathematical
Foundations of Computer Science (SG), Krakow, Poland, 2016, vol. 58.'
ista: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. 2016. Conditionally
optimal algorithms for generalized Büchi Games. MFCS: Mathematical Foundations
of Computer Science (SG), LIPIcs, vol. 58, 25.'
mla: Chatterjee, Krishnendu, et al. Conditionally Optimal Algorithms for Generalized
Büchi Games. Vol. 58, 25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016, doi:10.4230/LIPIcs.MFCS.2016.25.
short: K. Chatterjee, W. Dvorák, M.H. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Krakow, Poland
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2016-08-22
date_created: 2018-12-11T11:49:58Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2025-06-02T08:53:50Z
day: '01'
ddc:
- '000'
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.MFCS.2016.25
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:02Z
date_updated: 2018-12-12T10:16:02Z
file_id: '5187'
file_name: IST-2017-779-v1+1_LIPIcs-MFCS-2016-25.pdf
file_size: 632786
relation: main_file
file_date_updated: 2018-12-12T10:16:02Z
has_accepted_license: '1'
intvolume: ' 58'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/3.0/
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided 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'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6317'
pubrep_id: '779'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Conditionally optimal algorithms for generalized Büchi Games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 58
year: '2016'
...
---
_id: '1069'
abstract:
- lang: eng
text: "The Continuous Skolem Problem asks whether a real-valued function satisfying
a linear differen-\r\ntial equation has a zero in a given interval of real numbers.
This is a fundamental reachability\r\nproblem for continuous linear dynamical
systems, such as linear hybrid automata and continuous-\r\ntime Markov chains.
Decidability of the problem is currently open – indeed decidability is open\r\neven
for the sub-problem in which a zero is sought in a bounded interval. In this paper
we show\r\ndecidability of the bounded problem subject to Schanuel’s Conjecture,
a unifying conjecture in\r\ntranscendental number theory. We furthermore analyse
the unbounded problem in terms of the\r\nfrequencies of the differential equation,
that is, the imaginary parts of the characteristic roots.\r\nWe show that the
unbounded problem can be reduced to the bounded problem if there is at most\r\none
rationally linearly independent frequency, or if there are two rationally linearly
independent\r\nfrequencies and all characteristic roots are simple. We complete
the picture by showing that de-\r\ncidability of the unbounded problem in the
case of two (or more) rationally linearly independent\r\nfrequencies would entail
a major new effectiveness result in Diophantine approximation, namely\r\ncomputability
of the Diophantine-approximation types of all real algebraic numbers."
acknowledgement: 'Ventsislav Chonev is supported by Austrian Science Fund (FWF) NFN
Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and ERC
Advanced Grant (267989: QUAREM).'
alternative_title:
- LIPIcs
article_number: '100'
author:
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
- first_name: Joël
full_name: Ouaknine, Joël
last_name: Ouaknine
- first_name: James
full_name: Worrell, James
last_name: Worrell
citation:
ama: 'Chonev VK, Ouaknine J, Worrell J. On the skolem problem for continuous linear
dynamical systems. In: Vol 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik;
2016. doi:10.4230/LIPIcs.ICALP.2016.100'
apa: 'Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the skolem problem
for continuous linear dynamical systems (Vol. 55). Presented at the ICALP: Automata,
Languages and Programming, Rome, Italy: Schloss Dagstuhl- Leibniz-Zentrum fur
Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2016.100'
chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Skolem
Problem for Continuous Linear Dynamical Systems,” Vol. 55. Schloss Dagstuhl- Leibniz-Zentrum
fur Informatik, 2016. https://doi.org/10.4230/LIPIcs.ICALP.2016.100.
ieee: 'V. K. Chonev, J. Ouaknine, and J. Worrell, “On the skolem problem for continuous
linear dynamical systems,” presented at the ICALP: Automata, Languages and Programming,
Rome, Italy, 2016, vol. 55.'
ista: 'Chonev VK, Ouaknine J, Worrell J. 2016. On the skolem problem for continuous
linear dynamical systems. ICALP: Automata, Languages and Programming, LIPIcs,
vol. 55, 100.'
mla: Chonev, Ventsislav K., et al. On the Skolem Problem for Continuous Linear
Dynamical Systems. Vol. 55, 100, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016, doi:10.4230/LIPIcs.ICALP.2016.100.
short: V.K. Chonev, J. Ouaknine, J. Worrell, in:, Schloss Dagstuhl- Leibniz-Zentrum
fur Informatik, 2016.
conference:
end_date: 2016-07-15
location: Rome, Italy
name: 'ICALP: Automata, Languages and Programming'
start_date: 2016-07-12
date_created: 2018-12-11T11:49:59Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:48:03Z
day: '01'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ICALP.2016.100
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:26Z
date_updated: 2018-12-12T10:16:26Z
file_id: '5213'
file_name: IST-2017-778-v1+1_LIPIcs-ICALP-2016-100.pdf
file_size: 521415
relation: main_file
file_date_updated: 2018-12-12T10:16:26Z
has_accepted_license: '1'
intvolume: ' 55'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik
publist_id: '6314'
pubrep_id: '778'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the skolem problem for continuous linear dynamical 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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 55
year: '2016'
...
---
_id: '1070'
abstract:
- lang: eng
text: 'We present a logic that extends CTL (Computation Tree Logic) with operators
that express synchronization properties. A property is synchronized in a system
if it holds in all paths of a certain length. The new logic is obtained by using
the same path quantifiers and temporal operators as in CTL, but allowing a different
order of the quantifiers. This small syntactic variation induces a logic that
can express non-regular properties for which known extensions of MSO with equality
of path length are undecidable. We show that our variant of CTL is decidable and
that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We
analogously consider quantifier exchange in extensions of CTL, and we present
operators defined using basic operators of CTL* that express the occurrence of
infinitely many synchronization points. We show that the model-checking problem
remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide
if the Next operator is allowed in the logics, thus the classical bisimulation
quotient can be used for state-space reduction before model checking. '
acknowledgement: "This research was partially supported by Austrian Science Fund (FWF)
NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), Vienna
Science and Technology Fund (WWTF) through project ICT15-003, and European project
Cassting (FP7-601148).\r\n\r\nWe thank Stefan Göller and anonymous reviewers for
their insightful\r\ncomments and suggestions.\r\n"
alternative_title:
- LIPIcs
article_number: '98'
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
citation:
ama: 'Chatterjee K, Doyen L. Computation tree logic for synchronization properties.
In: Vol 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:10.4230/LIPIcs.ICALP.2016.98'
apa: 'Chatterjee, K., & Doyen, L. (2016). Computation tree logic for synchronization
properties (Vol. 55). Presented at the ICALP: Automata, Languages and Programming,
Rome, Italy: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2016.98'
chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Computation Tree Logic for
Synchronization Properties,” Vol. 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016. https://doi.org/10.4230/LIPIcs.ICALP.2016.98.
ieee: 'K. Chatterjee and L. Doyen, “Computation tree logic for synchronization properties,”
presented at the ICALP: Automata, Languages and Programming, Rome, Italy, 2016,
vol. 55.'
ista: 'Chatterjee K, Doyen L. 2016. Computation tree logic for synchronization properties.
ICALP: Automata, Languages and Programming, LIPIcs, vol. 55, 98.'
mla: Chatterjee, Krishnendu, and Laurent Doyen. Computation Tree Logic for Synchronization
Properties. Vol. 55, 98, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016, doi:10.4230/LIPIcs.ICALP.2016.98.
short: K. Chatterjee, L. Doyen, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016.
conference:
end_date: 2016-07-15
location: Rome, Italy
name: 'ICALP: Automata, Languages and Programming'
start_date: 2016-07-12
date_created: 2018-12-11T11:49:59Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:48:03Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ICALP.2016.98
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:52Z
date_updated: 2018-12-12T10:08:52Z
file_id: '4714'
file_name: IST-2017-812-v1+1_LIPIcs-ICALP-2016-98.pdf
file_size: 546133
relation: main_file
file_date_updated: 2018-12-12T10:08:52Z
has_accepted_license: '1'
intvolume: ' 55'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik
publist_id: '6313'
pubrep_id: '812'
quality_controlled: '1'
scopus_import: 1
status: public
title: Computation tree logic for synchronization properties
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 55
year: '2016'
...
---
_id: '1071'
abstract:
- lang: eng
text: 'We consider data-structures for answering reachability and distance queries
on constant-treewidth graphs with n nodes, on the standard RAM computational model
with wordsize W=Theta(log n). Our first contribution is a data-structure that
after O(n) preprocessing time, allows (1) pair reachability queries in O(1) time;
and (2) single-source reachability queries in O(n/log n) time. This is (asymptotically)
optimal and is faster than DFS/BFS when answering more than a constant number
of single-source queries. The data-structure uses at all times O(n) space. Our
second contribution is a space-time tradeoff data-structure for distance queries.
For any epsilon in [1/2,1], we provide a data-structure with polynomial preprocessing
time that allows pair queries in O(n^{1-\epsilon} alpha(n)) time, where alpha
is the inverse of the Ackermann function, and at all times uses O(n^epsilon) space.
The input graph G is not considered in the space complexity. '
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE) and ERC Start grant
(279307: Graph Games).'
alternative_title:
- LIPIcs
article_number: '28'
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 reachability and a space
time tradeoff for distance queries in constant treewidth graphs. In: Vol 57. Schloss
Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:10.4230/LIPIcs.ESA.2016.28'
apa: 'Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2016). Optimal reachability
and a space time tradeoff for distance queries in constant treewidth graphs (Vol.
57). Presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark:
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. https://doi.org/10.4230/LIPIcs.ESA.2016.28'
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
“Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant
Treewidth Graphs,” Vol. 57. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016. https://doi.org/10.4230/LIPIcs.ESA.2016.28.
ieee: 'K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal reachability
and a space time tradeoff for distance queries in constant treewidth graphs,”
presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark, 2016,
vol. 57.'
ista: 'Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2016. Optimal reachability
and a space time tradeoff for distance queries in constant treewidth graphs. ESA:
European Symposium on Algorithms, LIPIcs, vol. 57, 28.'
mla: Chatterjee, Krishnendu, et al. Optimal Reachability and a Space Time Tradeoff
for Distance Queries in Constant Treewidth Graphs. Vol. 57, 28, Schloss Dagstuhl-
Leibniz-Zentrum fur Informatik, 2016, doi:10.4230/LIPIcs.ESA.2016.28.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Schloss Dagstuhl- Leibniz-Zentrum
fur Informatik, 2016.
conference:
end_date: 2016-08-24
location: Aarhus, Denmark
name: 'ESA: European Symposium on Algorithms'
start_date: 2016-08-22
date_created: 2018-12-11T11:49:59Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-09-07T12:01:58Z
day: '01'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ESA.2016.28
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:31Z
date_updated: 2018-12-12T10:14:31Z
file_id: '5084'
file_name: IST-2017-777-v1+1_LIPIcs-ESA-2016-28.pdf
file_size: 579225
relation: main_file
file_date_updated: 2018-12-12T10:14:31Z
has_accepted_license: '1'
intvolume: ' 57'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
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'
publication_status: published
publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik
publist_id: '6312'
pubrep_id: '777'
quality_controlled: '1'
related_material:
record:
- id: '821'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Optimal reachability and a space time tradeoff for distance queries in constant
treewidth graphs
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 57
year: '2016'
...
---
_id: '1090'
abstract:
- lang: eng
text: ' While weighted automata provide a natural framework to express quantitative
properties, many basic properties like average response time cannot be expressed
with weighted automata. Nested weighted automata extend weighted automata and
consist of a master automaton and a set of slave automata that are invoked by
the master automaton. Nested weighted automata are strictly more expressive than
weighted automata (e.g., average response time can be expressed with nested weighted
automata), but the basic decision questions have higher complexity (e.g., for
deterministic automata, the emptiness question for nested weighted automata is
PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME).
We consider a natural subclass of nested weighted automata where at any point
at most a bounded number k of slave automata can be active. We focus on automata
whose master value function is the limit average. We show that these nested weighted
automata with bounded width are strictly more expressive than weighted automata
(e.g., average response time with no overlapping requests can be expressed with
bound k=1, but not with non-nested weighted automata). We show that the complexity
of the basic decision problems (i.e., emptiness and universality) for the subclass
with k constant matches the complexity for weighted automata. Moreover, when k
is part of the input given in unary we establish PSPACE-completeness.'
acknowledgement: "This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award),
ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF)
through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under
grant 2014/15/D/ST6/04543."
alternative_title:
- LIPIcs
article_number: '24'
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 limit-average automata
of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2016. doi:10.4230/LIPIcs.MFCS.2016.24'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Nested weighted limit-average
automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations
of Computer Science (SG), Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2016.24'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted
Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016. https://doi.org/10.4230/LIPIcs.MFCS.2016.24.
ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average
automata of bounded width,” presented at the MFCS: Mathematical Foundations of
Computer Science (SG), Krakow; Poland, 2016, vol. 58.'
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata
of bounded width. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs,
vol. 58, 24.'
mla: Chatterjee, Krishnendu, et al. Nested Weighted Limit-Average Automata of
Bounded Width. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016, doi:10.4230/LIPIcs.MFCS.2016.24.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Krakow; Poland
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2016-08-22
date_created: 2018-12-11T11:50:05Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:48:12Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2016.24
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:31Z
date_updated: 2018-12-12T10:17:31Z
file_id: '5286'
file_name: IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf
file_size: 564560
relation: main_file
file_date_updated: 2018-12-12T10:17:31Z
has_accepted_license: '1'
intvolume: ' 58'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6286'
pubrep_id: '795'
quality_controlled: '1'
scopus_import: 1
status: public
title: Nested weighted limit-average automata of bounded width
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 58
year: '2016'
...
---
_id: '1093'
abstract:
- lang: eng
text: 'We introduce a general class of distances (metrics) between Markov chains,
which are based on linear behaviour. This class encompasses distances given topologically
(such as the total variation distance or trace distance) as well as by temporal
logics or automata. We investigate which of the distances can be approximated
by observing the systems, i.e. by black-box testing or simulation, and we provide
both negative and positive results. '
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF)
under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award),
by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced
Postdoc. Mobility Fellowship – grant number P300P2_161067."
alternative_title:
- LIPIcs
article_number: '20'
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov
chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.20'
apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Linear
distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency
Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.CONCUR.2016.20'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20.
ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances
between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City;
Canada, 2016, vol. 59.'
ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between
Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.'
mla: Daca, Przemyslaw, et al. Linear Distances between Markov Chains. Vol.
59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.20.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Quebec City; Canada
name: 'CONCUR: Concurrency Theory'
start_date: 2016-08-23
date_created: 2018-12-11T11:50:06Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
- _id: KrCh
- _id: CaGu
doi: 10.4230/LIPIcs.CONCUR.2016.20
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:39Z
date_updated: 2018-12-12T10:11:39Z
file_id: '4895'
file_name: IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf
file_size: 501827
relation: main_file
file_date_updated: 2018-12-12T10:11:39Z
has_accepted_license: '1'
intvolume: ' 59'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
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
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6283'
pubrep_id: '794'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Linear distances between Markov chains
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1138'
abstract:
- lang: eng
text: Automata with monitor counters, where the transitions do not depend on counter
values, and nested weighted automata are two expressive automata-theoretic frameworks
for quantitative properties. For a well-studied and wide class of quantitative
functions, we establish that automata with monitor counters and nested weighted
automata are equivalent. We study for the first time such quantitative automata
under probabilistic semantics. We show that several problems that are undecidable
for the classical questions of emptiness and universality become decidable under
the probabilistic semantics. We present a complete picture of decidability for
such automata, and even an almost-complete picture of computational complexity,
for the probabilistic questions we consider. © 2016 ACM.
acknowledgement: This research was funded in part by the European Research Council
(ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF)
projects S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499-
N23, FWF NFN Grant No S114
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: 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. Quantitative automata under probabilistic
semantics. In: Proceedings of the 31st Annual ACM/IEEE Symposium. IEEE;
2016:76-85. doi:10.1145/2933575.2933588'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative automata
under probabilistic semantics. In Proceedings of the 31st Annual ACM/IEEE Symposium
(pp. 76–85). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2933588'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative
Automata under Probabilistic Semantics.” In Proceedings of the 31st Annual
ACM/IEEE Symposium, 76–85. IEEE, 2016. https://doi.org/10.1145/2933575.2933588.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under
probabilistic semantics,” in Proceedings of the 31st Annual ACM/IEEE Symposium,
New York, NY, USA, 2016, pp. 76–85.
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic
semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer
Science, 76–85.'
mla: Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.”
Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85,
doi:10.1145/2933575.2933588.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual
ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.
conference:
end_date: 2016-07-08
location: New York, NY, USA
name: 'LICS: Logic in Computer Science'
start_date: 2016-07-05
date_created: 2018-12-11T11:50:21Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2021-01-12T06:48:34Z
day: '05'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/2933575.2933588
ec_funded: 1
external_id:
arxiv:
- '1604.06764'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.06764
month: '07'
oa: 1
oa_version: Preprint
page: 76 - 85
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: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the 31st Annual ACM/IEEE Symposium
publication_status: published
publisher: IEEE
publist_id: '6220'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative automata under probabilistic semantics
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...