---
_id: '14778'
abstract:
- lang: eng
text: 'We consider the almost-sure (a.s.) termination problem for probabilistic
programs, which are a stochastic extension of classical imperative programs. Lexicographic
ranking functions provide a sound and practical approach for termination of non-probabilistic
programs, and their extension to probabilistic programs is achieved via lexicographic
ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous
work have a limitation that impedes their automation: all of their components
have to be non-negative in all reachable states. This might result in a LexRSM
not existing even for simple terminating programs. Our contributions are twofold.
First, we introduce a generalization of LexRSMs that allows for some components
to be negative. This standard feature of non-probabilistic termination proofs
was hitherto not known to be sound in the probabilistic setting, as the soundness
proof requires a careful analysis of the underlying stochastic process. Second,
we present polynomial-time algorithms using our generalized LexRSMs for proving
a.s. termination in broad classes of linear-arithmetic programs.'
acknowledgement: This research was partially supported by the ERC CoG (grant no. 863818;
ForM-SMArt), the Czech Science Foundation (grant no. GA21-24711S), and the European
Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie
Grant Agreement No. 665385.
article_number: '11'
article_processing_charge: Yes (via OA deal)
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: Ehsan
full_name: Kafshdar Goharshady, Ehsan
last_name: Kafshdar Goharshady
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Jiří
full_name: Zárevúcky, Jiří
last_name: Zárevúcky
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. On
lexicographic proof rules for probabilistic termination. Formal Aspects of
Computing. 2023;35(2). doi:10.1145/3585391
apa: Chatterjee, K., Kafshdar Goharshady, E., Novotný, P., Zárevúcky, J., &
Zikelic, D. (2023). On lexicographic proof rules for probabilistic termination.
Formal Aspects of Computing. Association for Computing Machinery. https://doi.org/10.1145/3585391
chicago: Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky,
and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.”
Formal Aspects of Computing. Association for Computing Machinery, 2023.
https://doi.org/10.1145/3585391.
ieee: K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic,
“On lexicographic proof rules for probabilistic termination,” Formal Aspects
of Computing, vol. 35, no. 2. Association for Computing Machinery, 2023.
ista: Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2023.
On lexicographic proof rules for probabilistic termination. Formal Aspects of
Computing. 35(2), 11.
mla: Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic
Termination.” Formal Aspects of Computing, vol. 35, no. 2, 11, Association
for Computing Machinery, 2023, doi:10.1145/3585391.
short: K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic,
Formal Aspects of Computing 35 (2023).
date_created: 2024-01-10T09:27:43Z
date_published: 2023-06-23T00:00:00Z
date_updated: 2025-07-14T09:10:10Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3585391
ec_funded: 1
external_id:
arxiv:
- '2108.02188'
file:
- access_level: open_access
checksum: 3bb133eeb27ec01649a9a36445d952d9
content_type: application/pdf
creator: dernst
date_created: 2024-01-16T08:11:24Z
date_updated: 2024-01-16T08:11:24Z
file_id: '14804'
file_name: 2023_FormalAspectsComputing_Chatterjee.pdf
file_size: 502522
relation: main_file
success: 1
file_date_updated: 2024-01-16T08:11:24Z
has_accepted_license: '1'
intvolume: ' 35'
issue: '2'
keyword:
- Theoretical Computer Science
- Software
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Formal Aspects of Computing
publication_identifier:
eissn:
- 1433-299X
issn:
- 0934-5043
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '10414'
relation: earlier_version
status: public
status: public
title: On lexicographic proof rules for probabilistic termination
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 35
year: '2023'
...
---
_id: '9644'
abstract:
- lang: eng
text: 'We present a new approach to proving non-termination of non-deterministic
integer programs. Our technique is rather simple but efficient. It relies on a
purely syntactic reversal of the program''s transition system followed by a constraint-based
invariant synthesis with constraints coming from both the original and the reversed
transition system. The latter task is performed by a simple call to an off-the-shelf
SMT-solver, which allows us to leverage the latest advances in SMT-solving. Moreover,
our method offers a combination of features not present (as a whole) in previous
approaches: it handles programs with non-determinism, provides relative completeness
guarantees and supports programs with polynomial arithmetic. The experiments performed
with our prototype tool RevTerm show that our approach, despite its simplicity
and stronger theoretical guarantees, is at least on par with the state-of-the-art
tools, often achieving a non-trivial improvement under a proper configuration
of its parameters.'
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
research was partially supported by the ERCCoG 863818 (ForM-SMArt) and the Czech
Science Foundation grant No. GJ19-15134Y.
article_processing_charge: No
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: Ehsan Kafshdar
full_name: Goharshady, Ehsan Kafshdar
last_name: Goharshady
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady EK, Novotný P, Zikelic D. Proving non-termination
by program reversal. In: Proceedings of the 42nd ACM SIGPLAN International
Conference on Programming Language Design and Implementation. Association
for Computing Machinery; 2021:1033-1048. doi:10.1145/3453483.3454093'
apa: 'Chatterjee, K., Goharshady, E. K., Novotný, P., & Zikelic, D. (2021).
Proving non-termination by program reversal. In Proceedings of the 42nd ACM
SIGPLAN International Conference on Programming Language Design and Implementation
(pp. 1033–1048). Online: Association for Computing Machinery. https://doi.org/10.1145/3453483.3454093'
chicago: Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde
Zikelic. “Proving Non-Termination by Program Reversal.” In Proceedings of the
42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation,
1033–48. Association for Computing Machinery, 2021. https://doi.org/10.1145/3453483.3454093.
ieee: K. Chatterjee, E. K. Goharshady, P. Novotný, and D. Zikelic, “Proving non-termination
by program reversal,” in Proceedings of the 42nd ACM SIGPLAN International
Conference on Programming Language Design and Implementation, Online, 2021,
pp. 1033–1048.
ista: 'Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. Proving non-termination
by program reversal. Proceedings of the 42nd ACM SIGPLAN International Conference
on Programming Language Design and Implementation. PLDI: Programming Language
Design and Implementation, 1033–1048.'
mla: Chatterjee, Krishnendu, et al. “Proving Non-Termination by Program Reversal.”
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
Language Design and Implementation, Association for Computing Machinery, 2021,
pp. 1033–48, doi:10.1145/3453483.3454093.
short: K. Chatterjee, E.K. Goharshady, P. Novotný, D. Zikelic, in:, Proceedings
of the 42nd ACM SIGPLAN International Conference on Programming Language Design
and Implementation, Association for Computing Machinery, 2021, pp. 1033–1048.
conference:
end_date: 2021-06-26
location: Online
name: 'PLDI: Programming Language Design and Implementation'
start_date: 2021-06-20
date_created: 2021-07-11T22:01:17Z
date_published: 2021-06-01T00:00:00Z
date_updated: 2025-07-14T09:10:06Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3453483.3454093
ec_funded: 1
external_id:
arxiv:
- '2104.01189'
isi:
- '000723661700067'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2104.01189
month: '06'
oa: 1
oa_version: Preprint
page: 1033-1048
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
Language Design and Implementation
publication_identifier:
isbn:
- '9781450383912'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Proving non-termination by program reversal
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '10414'
abstract:
- lang: eng
text: 'We consider the almost-sure (a.s.) termination problem for probabilistic
programs, which are a stochastic extension of classical imperative programs. Lexicographic
ranking functions provide a sound and practical approach for termination of non-probabilistic
programs, and their extension to probabilistic programs is achieved via lexicographic
ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous
work have a limitation that impedes their automation: all of their components
have to be non-negative in all reachable states. This might result in LexRSM not
existing even for simple terminating programs. Our contributions are twofold:
First, we introduce a generalization of LexRSMs which allows for some components
to be negative. This standard feature of non-probabilistic termination proofs
was hitherto not known to be sound in the probabilistic setting, as the soundness
proof requires a careful analysis of the underlying stochastic process. Second,
we present polynomial-time algorithms using our generalized LexRSMs for proving
a.s. termination in broad classes of linear-arithmetic programs.'
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt),
the Czech Science Foundation grant No. GJ19-15134Y, and the European Union’s Horizon
2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement
No. 665385.
alternative_title:
- LNCS
article_processing_charge: No
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: Ehsan Kafshdar
full_name: Goharshady, Ehsan Kafshdar
last_name: Goharshady
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Jiří
full_name: Zárevúcky, Jiří
last_name: Zárevúcky
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady EK, Novotný P, Zárevúcky J, Zikelic D. On lexicographic
proof rules for probabilistic termination. In: 24th International Symposium
on Formal Methods. Vol 13047. Springer Nature; 2021:619-639. doi:10.1007/978-3-030-90870-6_33'
apa: 'Chatterjee, K., Goharshady, E. K., Novotný, P., Zárevúcky, J., & Zikelic,
D. (2021). On lexicographic proof rules for probabilistic termination. In 24th
International Symposium on Formal Methods (Vol. 13047, pp. 619–639). Virtual:
Springer Nature. https://doi.org/10.1007/978-3-030-90870-6_33'
chicago: Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky,
and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.”
In 24th International Symposium on Formal Methods, 13047:619–39. Springer
Nature, 2021. https://doi.org/10.1007/978-3-030-90870-6_33.
ieee: K. Chatterjee, E. K. Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic,
“On lexicographic proof rules for probabilistic termination,” in 24th International
Symposium on Formal Methods, Virtual, 2021, vol. 13047, pp. 619–639.
ista: 'Chatterjee K, Goharshady EK, Novotný P, Zárevúcky J, Zikelic D. 2021. On
lexicographic proof rules for probabilistic termination. 24th International Symposium
on Formal Methods. FM: Formal Methods, LNCS, vol. 13047, 619–639.'
mla: Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic
Termination.” 24th International Symposium on Formal Methods, vol. 13047,
Springer Nature, 2021, pp. 619–39, doi:10.1007/978-3-030-90870-6_33.
short: K. Chatterjee, E.K. Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, in:,
24th International Symposium on Formal Methods, Springer Nature, 2021, pp. 619–639.
conference:
end_date: 2021-11-26
location: Virtual
name: 'FM: Formal Methods'
start_date: 2021-11-20
date_created: 2021-12-05T23:01:45Z
date_published: 2021-11-10T00:00:00Z
date_updated: 2025-07-14T09:10:11Z
day: '10'
department:
- _id: KrCh
doi: 10.1007/978-3-030-90870-6_33
ec_funded: 1
external_id:
arxiv:
- '2108.02188'
isi:
- '000758218600033'
intvolume: ' 13047'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2108.02188
month: '11'
oa: 1
oa_version: Preprint
page: 619-639
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: 24th International Symposium on Formal Methods
publication_identifier:
eisbn:
- 978-3-030-90870-6
eissn:
- 1611-3349
isbn:
- 9-783-0309-0869-0
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
- id: '14778'
relation: later_version
status: public
scopus_import: '1'
status: public
title: On lexicographic proof rules for probabilistic termination
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13047
year: '2021'
...
---
_id: '8193'
abstract:
- lang: eng
text: 'Multiple-environment Markov decision processes (MEMDPs) are MDPs equipped
with not one, but multiple probabilistic transition functions, which represent
the various possible unknown environments. While the previous research on MEMDPs
focused on theoretical properties for long-run average payoff, we study them with
discounted-sum payoff and focus on their practical advantages and applications.
MEMDPs can be viewed as a special case of Partially observable and Mixed observability
MDPs: the state of the system is perfectly observable, but not the environment.
We show that the specific structure of MEMDPs allows for more efficient algorithmic
analysis, in particular for faster belief updates. We demonstrate the applicability
of MEMDPs in several domains. In particular, we formalize the sequential decision-making
approach to contextual recommendation systems as MEMDPs and substantially improve
over the previous MDP approach.'
acknowledgement: Krishnendu Chatterjee is supported by the Austrian ScienceFund (FWF)
NFN Grant No. S11407-N23 (RiSE/SHiNE),and COST Action GAMENET. Petr Novotn ́y is
supported bythe Czech Science Foundation grant No. GJ19-15134Y.
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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Deep
full_name: Karkhanis, Deep
last_name: Karkhanis
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Amélie
full_name: Royer, Amélie
id: 3811D890-F248-11E8-B48F-1D18A9856A87
last_name: Royer
orcid: 0000-0002-8407-0705
citation:
ama: 'Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. Multiple-environment
Markov decision processes: Efficient analysis and applications. In: Proceedings
of the 30th International Conference on Automated Planning and Scheduling.
Vol 30. Association for the Advancement of Artificial Intelligence; 2020:48-56.'
apa: 'Chatterjee, K., Chmelik, M., Karkhanis, D., Novotný, P., & Royer, A. (2020).
Multiple-environment Markov decision processes: Efficient analysis and applications.
In Proceedings of the 30th International Conference on Automated Planning and
Scheduling (Vol. 30, pp. 48–56). Nancy, France: Association for the Advancement
of Artificial Intelligence.'
chicago: 'Chatterjee, Krishnendu, Martin Chmelik, Deep Karkhanis, Petr Novotný,
and Amélie Royer. “Multiple-Environment Markov Decision Processes: Efficient Analysis
and Applications.” In Proceedings of the 30th International Conference on Automated
Planning and Scheduling, 30:48–56. Association for the Advancement of Artificial
Intelligence, 2020.'
ieee: 'K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, and A. Royer, “Multiple-environment
Markov decision processes: Efficient analysis and applications,” in Proceedings
of the 30th International Conference on Automated Planning and Scheduling,
Nancy, France, 2020, vol. 30, pp. 48–56.'
ista: 'Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. 2020. Multiple-environment
Markov decision processes: Efficient analysis and applications. Proceedings of
the 30th International Conference on Automated Planning and Scheduling. ICAPS:
International Conference on Automated Planning and Scheduling vol. 30, 48–56.'
mla: 'Chatterjee, Krishnendu, et al. “Multiple-Environment Markov Decision Processes:
Efficient Analysis and Applications.” Proceedings of the 30th International
Conference on Automated Planning and Scheduling, vol. 30, Association for
the Advancement of Artificial Intelligence, 2020, pp. 48–56.'
short: K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, A. Royer, in:, Proceedings
of the 30th International Conference on Automated Planning and Scheduling, Association
for the Advancement of Artificial Intelligence, 2020, pp. 48–56.
conference:
end_date: 2020-10-30
location: Nancy, France
name: 'ICAPS: International Conference on Automated Planning and Scheduling'
start_date: 2020-10-26
date_created: 2020-08-02T22:00:58Z
date_published: 2020-06-01T00:00:00Z
date_updated: 2023-09-07T13:16:18Z
day: '01'
department:
- _id: KrCh
intvolume: ' 30'
language:
- iso: eng
month: '06'
oa_version: None
page: 48-56
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: Proceedings of the 30th International Conference on Automated Planning
and Scheduling
publication_identifier:
eissn:
- '23340843'
issn:
- '23340835'
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
related_material:
record:
- id: '8390'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: 'Multiple-environment Markov decision processes: Efficient analysis and applications'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 30
year: '2020'
...
---
_id: '7183'
abstract:
- lang: eng
text: 'A probabilistic vector addition system with states (pVASS) is a finite state
Markov process augmented with non-negative integer counters that can be incremented
or decremented during each state transition, blocking any behaviour that would
cause a counter to decrease below zero. The pVASS can be used as abstractions
of probabilistic programs with many decidable properties. The use of pVASS as
abstractions requires the presence of nondeterminism in the model. In this paper,
we develop techniques for checking fast termination of pVASS with nondeterminism.
That is, for every initial configuration of size n, we consider the worst expected
number of transitions needed to reach a configuration with some counter negative
(the expected termination time). We show that the problem whether the asymptotic
expected termination time is linear is decidable in polynomial time for a certain
natural class of pVASS with nondeterminism. Furthermore, we show the following
dichotomy: if the asymptotic expected termination time is not linear, then it
is at least quadratic, i.e., in Ω(n2).'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Tomás
full_name: Brázdil, Tomás
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: Antonín
full_name: Kucera, Antonín
last_name: Kucera
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Dominik
full_name: Velan, Dominik
last_name: Velan
citation:
ama: 'Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. Deciding fast termination
for probabilistic VASS with nondeterminism. In: International Symposium on
Automated Technology for Verification and Analysis. Vol 11781. Springer Nature;
2019:462-478. doi:10.1007/978-3-030-31784-3_27'
apa: 'Brázdil, T., Chatterjee, K., Kucera, A., Novotný, P., & Velan, D. (2019).
Deciding fast termination for probabilistic VASS with nondeterminism. In International
Symposium on Automated Technology for Verification and Analysis (Vol. 11781,
pp. 462–478). Taipei, Taiwan: Springer Nature. https://doi.org/10.1007/978-3-030-31784-3_27'
chicago: Brázdil, Tomás, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, and
Dominik Velan. “Deciding Fast Termination for Probabilistic VASS with Nondeterminism.”
In International Symposium on Automated Technology for Verification and Analysis,
11781:462–78. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-31784-3_27.
ieee: T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, and D. Velan, “Deciding
fast termination for probabilistic VASS with nondeterminism,” in International
Symposium on Automated Technology for Verification and Analysis, Taipei, Taiwan,
2019, vol. 11781, pp. 462–478.
ista: 'Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. 2019. Deciding fast
termination for probabilistic VASS with nondeterminism. International Symposium
on Automated Technology for Verification and Analysis. ATVA: Automated TEchnology
for Verification and Analysis, LNCS, vol. 11781, 462–478.'
mla: Brázdil, Tomás, et al. “Deciding Fast Termination for Probabilistic VASS with
Nondeterminism.” International Symposium on Automated Technology for Verification
and Analysis, vol. 11781, Springer Nature, 2019, pp. 462–78, doi:10.1007/978-3-030-31784-3_27.
short: T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, D. Velan, in:, International
Symposium on Automated Technology for Verification and Analysis, Springer Nature,
2019, pp. 462–478.
conference:
end_date: 2019-10-31
location: Taipei, Taiwan
name: 'ATVA: Automated TEchnology for Verification and Analysis'
start_date: 2019-10-28
date_created: 2019-12-15T23:00:44Z
date_published: 2019-10-21T00:00:00Z
date_updated: 2023-09-06T12:40:58Z
day: '21'
department:
- _id: KrCh
doi: 10.1007/978-3-030-31784-3_27
external_id:
arxiv:
- '1907.11010'
isi:
- '000723515700027'
intvolume: ' 11781'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1907.11010
month: '10'
oa: 1
oa_version: Preprint
page: 462-478
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: International Symposium on Automated Technology for Verification and
Analysis
publication_identifier:
eissn:
- '16113349'
isbn:
- '9783030317836'
issn:
- '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Deciding fast termination for probabilistic VASS with nondeterminism
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11781
year: '2019'
...
---
_id: '325'
abstract:
- lang: eng
text: Probabilistic programs extend classical imperative programs with real-valued
random variables and random branching. The most basic liveness property for such
programs is the termination property. The qualitative (aka almost-sure) termination
problem asks whether a given program program terminates with probability 1. While
ranking functions provide a sound and complete method for non-probabilistic programs,
the extension of them to probabilistic programs is achieved via ranking supermartingales
(RSMs). Although deep theoretical results have been established about RSMs, their
application to probabilistic programs with nondeterminism has been limited only
to programs of restricted control-flow structure. For non-probabilistic programs,
lexicographic ranking functions provide a compositional and practical approach
for termination analysis of real-world programs. In this work we introduce lexicographic
RSMs and show that they present a sound method for almost-sure termination of
probabilistic programs with nondeterminism. We show that lexicographic RSMs provide
a tool for compositional reasoning about almost-sure termination, and for probabilistic
programs with linear arithmetic they can be synthesized efficiently (in polynomial
time). We also show that with additional restrictions even asymptotic bounds on
expected termination time can be obtained through lexicographic RSMs. Finally,
we present experimental results on benchmarks adapted from previous work to demonstrate
the effectiveness of our approach.
article_number: '34'
arxiv: 1
author:
- first_name: Sheshansh
full_name: Agrawal, Sheshansh
last_name: Agrawal
- 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
citation:
ama: 'Agrawal S, Chatterjee K, Novotný P. Lexicographic ranking supermartingales:
an efficient approach to termination of probabilistic programs. In: Vol 2. ACM;
2018. doi:10.1145/3158122'
apa: 'Agrawal, S., Chatterjee, K., & Novotný, P. (2018). Lexicographic ranking
supermartingales: an efficient approach to termination of probabilistic programs
(Vol. 2). Presented at the POPL: Principles of Programming Languages, Los Angeles,
CA, USA: ACM. https://doi.org/10.1145/3158122'
chicago: 'Agrawal, Sheshansh, Krishnendu Chatterjee, and Petr Novotný. “Lexicographic
Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic
Programs,” Vol. 2. ACM, 2018. https://doi.org/10.1145/3158122.'
ieee: 'S. Agrawal, K. Chatterjee, and P. Novotný, “Lexicographic ranking supermartingales:
an efficient approach to termination of probabilistic programs,” presented at
the POPL: Principles of Programming Languages, Los Angeles, CA, USA, 2018, vol.
2, no. POPL.'
ista: 'Agrawal S, Chatterjee K, Novotný P. 2018. Lexicographic ranking supermartingales:
an efficient approach to termination of probabilistic programs. POPL: Principles
of Programming Languages vol. 2, 34.'
mla: 'Agrawal, Sheshansh, et al. Lexicographic Ranking Supermartingales: An Efficient
Approach to Termination of Probabilistic Programs. Vol. 2, no. POPL, 34, ACM,
2018, doi:10.1145/3158122.'
short: S. Agrawal, K. Chatterjee, P. Novotný, in:, ACM, 2018.
conference:
end_date: 2018-01-13
location: Los Angeles, CA, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2018-01-07
date_created: 2018-12-11T11:45:50Z
date_published: 2018-01-01T00:00:00Z
date_updated: 2021-01-12T07:42:07Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3158122
external_id:
arxiv:
- '1709.04037'
intvolume: ' 2'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1709.04037
month: '01'
oa: 1
oa_version: Preprint
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: ACM
publist_id: '7540'
quality_controlled: '1'
status: public
title: 'Lexicographic ranking supermartingales: an efficient approach to termination
of probabilistic programs'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2018'
...
---
_id: '24'
abstract:
- lang: eng
text: Partially-observable Markov decision processes (POMDPs) with discounted-sum
payoff are a standard framework to model a wide range of problems related to decision
making under uncertainty. Traditionally, the goal has been to obtain policies
that optimize the expectation of the discounted-sum payoff. A key drawback of
the expectation measure is that even low probability events with extreme payoff
can significantly affect the expectation, and thus the obtained policies are not
necessarily risk-averse. An alternate approach is to optimize the probability
that the payoff is above a certain threshold, which allows obtaining risk-averse
policies, but ignores optimization of the expectation. We consider the expectation
optimization with probabilistic guarantee (EOPG) problem, where the goal is to
optimize the expectation ensuring that the payoff is above a given threshold with
at least a specified probability. We present several results on the EOPG problem,
including the first algorithm to solve it.
acknowledgement: "This research was supported by the Vienna Science and Technology
Fund (WWTF) grant ICT15-003; Austrian Science Fund (FWF): S11407-N23(RiSE/SHiNE);and
an ERC Start Grant (279307:Graph Games).\r\n"
article_processing_charge: No
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: Adrian
full_name: Elgyütt, Adrian
id: 4A2E9DBA-F248-11E8-B48F-1D18A9856A87
last_name: Elgyütt
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Owen
full_name: Rouillé, Owen
last_name: Rouillé
citation:
ama: 'Chatterjee K, Elgyütt A, Novotný P, Rouillé O. Expectation optimization with
probabilistic guarantees in POMDPs with discounted-sum objectives. In: Vol 2018.
IJCAI; 2018:4692-4699. doi:10.24963/ijcai.2018/652'
apa: 'Chatterjee, K., Elgyütt, A., Novotný, P., & Rouillé, O. (2018). Expectation
optimization with probabilistic guarantees in POMDPs with discounted-sum objectives
(Vol. 2018, pp. 4692–4699). Presented at the IJCAI: International Joint Conference
on Artificial Intelligence, Stockholm, Sweden: IJCAI. https://doi.org/10.24963/ijcai.2018/652'
chicago: Chatterjee, Krishnendu, Adrian Elgyütt, Petr Novotný, and Owen Rouillé.
“Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum
Objectives,” 2018:4692–99. IJCAI, 2018. https://doi.org/10.24963/ijcai.2018/652.
ieee: 'K. Chatterjee, A. Elgyütt, P. Novotný, and O. Rouillé, “Expectation optimization
with probabilistic guarantees in POMDPs with discounted-sum objectives,” presented
at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm,
Sweden, 2018, vol. 2018, pp. 4692–4699.'
ista: 'Chatterjee K, Elgyütt A, Novotný P, Rouillé O. 2018. Expectation optimization
with probabilistic guarantees in POMDPs with discounted-sum objectives. IJCAI:
International Joint Conference on Artificial Intelligence vol. 2018, 4692–4699.'
mla: Chatterjee, Krishnendu, et al. Expectation Optimization with Probabilistic
Guarantees in POMDPs with Discounted-Sum Objectives. Vol. 2018, IJCAI, 2018,
pp. 4692–99, doi:10.24963/ijcai.2018/652.
short: K. Chatterjee, A. Elgyütt, P. Novotný, O. Rouillé, in:, IJCAI, 2018, pp.
4692–4699.
conference:
end_date: 2018-07-19
location: Stockholm, Sweden
name: 'IJCAI: International Joint Conference on Artificial Intelligence'
start_date: 2018-07-13
date_created: 2018-12-11T11:44:13Z
date_published: 2018-07-01T00:00:00Z
date_updated: 2025-06-02T08:53:48Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.24963/ijcai.2018/652
ec_funded: 1
external_id:
arxiv:
- '1804.10601'
isi:
- '000764175404117'
intvolume: ' 2018'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1804.10601
month: '07'
oa: 1
oa_version: Preprint
page: 4692 - 4699
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: IJCAI
publist_id: '8031'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum
objectives
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 2018
year: '2018'
...
---
_id: '5993'
abstract:
- lang: eng
text: 'In this article, we consider the termination problem of probabilistic programs
with real-valued variables. Thequestions concerned are: qualitative ones that
ask (i) whether the program terminates with probability 1(almost-sure termination)
and (ii) whether the expected termination time is finite (finite termination);
andquantitative ones that ask (i) to approximate the expected termination time
(expectation problem) and (ii) tocompute a boundBsuch that the probability not
to terminate afterBsteps decreases exponentially (con-centration problem). To
solve these questions, we utilize the notion of ranking supermartingales, which
isa powerful approach for proving termination of probabilistic programs. In detail,
we focus on algorithmicsynthesis of linear ranking-supermartingales over affine
probabilistic programs (Apps) with both angelic anddemonic non-determinism. An
important subclass of Apps is LRApp which is defined as the class of all Appsover
which a linear ranking-supermartingale exists.Our main contributions are as follows.
Firstly, we show that the membership problem of LRApp (i) canbe decided in polynomial
time for Apps with at most demonic non-determinism, and (ii) isNP-hard and inPSPACEfor
Apps with angelic non-determinism. Moreover, theNP-hardness result holds already
for Appswithout probability and demonic non-determinism. Secondly, we show that
the concentration problem overLRApp can be solved in the same complexity as for
the membership problem of LRApp. Finally, we show thatthe expectation problem
over LRApp can be solved in2EXPTIMEand isPSPACE-hard even for Apps withoutprobability
and non-determinism (i.e., deterministic programs). Our experimental results demonstrate
theeffectiveness of our approach to answer the qualitative and quantitative questions
over Apps with at mostdemonic non-determinism.'
article_number: '7'
article_processing_charge: No
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: Hongfei
full_name: Fu, Hongfei
id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
last_name: Fu
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Rouzbeh
full_name: Hasheminezhad, Rouzbeh
last_name: Hasheminezhad
citation:
ama: Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative
and quantitative termination problems for affine probabilistic programs. ACM
Transactions on Programming Languages and Systems. 2018;40(2). doi:10.1145/3174800
apa: Chatterjee, K., Fu, H., Novotný, P., & Hasheminezhad, R. (2018). Algorithmic
analysis of qualitative and quantitative termination problems for affine probabilistic
programs. ACM Transactions on Programming Languages and Systems. Association
for Computing Machinery (ACM). https://doi.org/10.1145/3174800
chicago: Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad.
“Algorithmic Analysis of Qualitative and Quantitative Termination Problems for
Affine Probabilistic Programs.” ACM Transactions on Programming Languages and
Systems. Association for Computing Machinery (ACM), 2018. https://doi.org/10.1145/3174800.
ieee: K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic
programs,” ACM Transactions on Programming Languages and Systems, vol.
40, no. 2. Association for Computing Machinery (ACM), 2018.
ista: Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2018. Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic
programs. ACM Transactions on Programming Languages and Systems. 40(2), 7.
mla: Chatterjee, Krishnendu, et al. “Algorithmic Analysis of Qualitative and Quantitative
Termination Problems for Affine Probabilistic Programs.” ACM Transactions on
Programming Languages and Systems, vol. 40, no. 2, 7, Association for Computing
Machinery (ACM), 2018, doi:10.1145/3174800.
short: K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming
Languages and Systems 40 (2018).
date_created: 2019-02-14T12:29:10Z
date_published: 2018-06-01T00:00:00Z
date_updated: 2023-09-19T14:38:42Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3174800
ec_funded: 1
external_id:
arxiv:
- '1510.08517'
isi:
- '000434634500003'
intvolume: ' 40'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1510.08517
month: '06'
oa: 1
oa_version: Submitted 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'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: ACM Transactions on Programming Languages and Systems
publication_identifier:
issn:
- 0164-0925
publication_status: published
publisher: Association for Computing Machinery (ACM)
quality_controlled: '1'
related_material:
record:
- id: '1438'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Algorithmic analysis of qualitative and quantitative termination problems for
affine probabilistic programs
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 40
year: '2018'
...
---
_id: '143'
abstract:
- lang: eng
text: 'Vector Addition Systems with States (VASS) provide a well-known and fundamental
model for the analysis of concurrent processes, parameterized systems, and are
also used as abstract models of programs in resource bound analysis. In this paper
we study the problem of obtaining asymptotic bounds on the termination time of
a given VASS. In particular, we focus on the practically important case of obtaining
polynomial bounds on termination time. Our main contributions are as follows:
First, we present a polynomial-time algorithm for deciding whether a given VASS
has a linear asymptotic complexity. We also show that if the complexity of a VASS
is not linear, it is at least quadratic. Second, we classify VASS according to
quantitative properties of their cycles. We show that certain singularities in
these properties are the key reason for non-polynomial asymptotic complexity of
VASS. In absence of singularities, we show that the asymptotic complexity is always
polynomial and of the form Θ(nk), for some integer k d, where d is the dimension
of the VASS. We present a polynomial-time algorithm computing the optimal k. For
general VASS, the same algorithm, which is based on a complete technique for the
construction of ranking functions in VASS, produces a valid lower bound, i.e.,
a k such that the termination complexity is (nk). Our results are based on new
insights into the geometry of VASS dynamics, which hold the potential for further
applicability to VASS analysis.'
alternative_title:
- ACM/IEEE Symposium on Logic in Computer Science
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: Antonín
full_name: Kučera, Antonín
last_name: Kučera
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Dominik
full_name: Velan, Dominik
last_name: Velan
- first_name: Florian
full_name: Zuleger, Florian
last_name: Zuleger
citation:
ama: 'Brázdil T, Chatterjee K, Kučera A, Novotný P, Velan D, Zuleger F. Efficient
algorithms for asymptotic bounds on termination time in VASS. In: Vol F138033.
IEEE; 2018:185-194. doi:10.1145/3209108.3209191'
apa: 'Brázdil, T., Chatterjee, K., Kučera, A., Novotný, P., Velan, D., & Zuleger,
F. (2018). Efficient algorithms for asymptotic bounds on termination time in VASS
(Vol. F138033, pp. 185–194). Presented at the LICS: Logic in Computer Science,
Oxford, United Kingdom: IEEE. https://doi.org/10.1145/3209108.3209191'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Antonín Kučera, Petr Novotný, Dominik
Velan, and Florian Zuleger. “Efficient Algorithms for Asymptotic Bounds on Termination
Time in VASS,” F138033:185–94. IEEE, 2018. https://doi.org/10.1145/3209108.3209191.
ieee: 'T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, and F. Zuleger,
“Efficient algorithms for asymptotic bounds on termination time in VASS,” presented
at the LICS: Logic in Computer Science, Oxford, United Kingdom, 2018, vol. F138033,
pp. 185–194.'
ista: 'Brázdil T, Chatterjee K, Kučera A, Novotný P, Velan D, Zuleger F. 2018. Efficient
algorithms for asymptotic bounds on termination time in VASS. LICS: Logic in Computer
Science, ACM/IEEE Symposium on Logic in Computer Science, vol. F138033, 185–194.'
mla: Brázdil, Tomáš, et al. Efficient Algorithms for Asymptotic Bounds on Termination
Time in VASS. Vol. F138033, IEEE, 2018, pp. 185–94, doi:10.1145/3209108.3209191.
short: T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, F. Zuleger, in:,
IEEE, 2018, pp. 185–194.
conference:
end_date: 2018-07-12
location: Oxford, United Kingdom
name: 'LICS: Logic in Computer Science'
start_date: 2018-07-09
date_created: 2018-12-11T11:44:51Z
date_published: 2018-07-09T00:00:00Z
date_updated: 2025-06-02T08:53:48Z
day: '09'
department:
- _id: KrCh
doi: 10.1145/3209108.3209191
ec_funded: 1
external_id:
isi:
- '000545262800020'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1804.10985
month: '07'
oa: 1
oa_version: Preprint
page: 185 - 194
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _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
publication_identifier:
isbn:
- 978-1-4503-5583-4
publication_status: published
publisher: IEEE
publist_id: '7780'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Efficient algorithms for asymptotic bounds on termination time in VASS
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: F138033
year: '2018'
...
---
_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: '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: '1438'
abstract:
- lang: eng
text: 'In this paper, we consider termination of probabilistic programs with real-valued
variables. The questions concerned are: (a) qualitative ones that ask (i) whether
the program terminates with probability 1 (almost-sure termination) and (ii) whether
the expected termination time is finite (finite termination); (b) quantitative
ones that ask (i) to approximate the expected termination time (expectation problem)
and (ii) to compute a bound B such that the probability to terminate after B steps
decreases exponentially (concentration problem). To solve these questions, we
utilize the notion of ranking supermartingales which is a powerful approach for
proving termination of probabilistic programs. In detail, we focus on algorithmic
synthesis of linear ranking-supermartingales over affine probabilistic programs
(APP''s) with both angelic and demonic non-determinism. An important subclass
of APP''s is LRAPP which is defined as the class of all APP''s over which a linear
ranking-supermartingale exists. Our main contributions are as follows. Firstly,
we show that the membership problem of LRAPP (i) can be decided in polynomial
time for APP''s with at most demonic non-determinism, and (ii) is NP-hard and
in PSPACE for APP''s with angelic non-determinism; moreover, the NP-hardness result
holds already for APP''s without probability and demonic non-determinism. Secondly,
we show that the concentration problem over LRAPP can be solved in the same complexity
as for the membership problem of LRAPP. Finally, we show that the expectation
problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP''s
without probability and non-determinism (i.e., deterministic programs). Our experimental
results demonstrate the effectiveness of our approach to answer the qualitative
and quantitative questions over APP''s with at most demonic non-determinism.'
acknowledgement: 'Supported by the Natural Science Foundation of China (NSFC) under
Grant No. 61532019 '
alternative_title:
- POPL
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: Hongfei
full_name: Fu, Hongfei
id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
last_name: Fu
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Rouzbeh
full_name: Hasheminezhad, Rouzbeh
last_name: Hasheminezhad
citation:
ama: 'Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative
and quantitative termination problems for affine probabilistic programs. In: Vol
20-22. ACM; 2016:327-342. doi:10.1145/2837614.2837639'
apa: 'Chatterjee, K., Fu, H., Novotný, P., & Hasheminezhad, R. (2016). Algorithmic
analysis of qualitative and quantitative termination problems for affine probabilistic
programs (Vol. 20–22, pp. 327–342). Presented at the POPL: Principles of Programming
Languages, St. Petersburg, FL, USA: ACM. https://doi.org/10.1145/2837614.2837639'
chicago: Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad.
“Algorithmic Analysis of Qualitative and Quantitative Termination Problems for
Affine Probabilistic Programs,” 20–22:327–42. ACM, 2016. https://doi.org/10.1145/2837614.2837639.
ieee: 'K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic
programs,” presented at the POPL: Principles of Programming Languages, St. Petersburg,
FL, USA, 2016, vol. 20–22, pp. 327–342.'
ista: 'Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2016. Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic
programs. POPL: Principles of Programming Languages, POPL, vol. 20–22, 327–342.'
mla: Chatterjee, Krishnendu, et al. Algorithmic Analysis of Qualitative and Quantitative
Termination Problems for Affine Probabilistic Programs. Vol. 20–22, ACM, 2016,
pp. 327–42, doi:10.1145/2837614.2837639.
short: K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, in:, ACM, 2016, pp. 327–342.
conference:
end_date: 2016-01-22
location: St. Petersburg, FL, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2016-01-20
date_created: 2018-12-11T11:52:01Z
date_published: 2016-01-11T00:00:00Z
date_updated: 2023-09-19T14:38:41Z
day: '11'
department:
- _id: KrCh
doi: 10.1145/2837614.2837639
ec_funded: 1
external_id:
arxiv:
- '1510.08517'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1510.08517
month: '01'
oa: 1
oa_version: Preprint
page: 327 - 342
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: ACM
publist_id: '5760'
quality_controlled: '1'
related_material:
record:
- id: '5993'
relation: later_version
status: public
scopus_import: 1
status: public
title: Algorithmic analysis of qualitative and quantitative termination problems for
affine probabilistic programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 20-22
year: '2016'
...
---
_id: '1325'
abstract:
- lang: eng
text: We study graphs and two-player games in which rewards are assigned to states,
and the goal of the players is to satisfy or dissatisfy certain property of the
generated outcome, given as a mean payoff property. Since the notion of mean-payoff
does not reflect possible fluctuations from the mean-payoff along a run, we propose
definitions and algorithms for capturing the stability of the system, and give
algorithms for deciding if a given mean payoff and stability objective can be
ensured in the system.
acknowledgement: "The work has been supported by the Czech Science Foundation, grant
No. 15-17564S, by EPSRC grant\r\nEP/M023656/1, and by the People Programme (Marie
Curie Actions) of the European Union’s Seventh\r\nFramework Programme (FP7/2007-2013)
under REA grant agreement no [291734]"
alternative_title:
- LIPIcs
article_number: '10'
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- 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
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Forejt V, Kučera A, Novotný P. Stability in graphs and games. In:
Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.10'
apa: 'Brázdil, T., Forejt, V., Kučera, A., & Novotný, P. (2016). Stability in
graphs and games (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.10'
chicago: Brázdil, Tomáš, Vojtěch Forejt, Antonín Kučera, and Petr Novotný. “Stability
in Graphs and Games,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.10.
ieee: 'T. Brázdil, V. Forejt, A. Kučera, and P. Novotný, “Stability in graphs and
games,” presented at the CONCUR: Concurrency Theory, Quebec City, Canada, 2016,
vol. 59.'
ista: 'Brázdil T, Forejt V, Kučera A, Novotný P. 2016. Stability in graphs and games.
CONCUR: Concurrency Theory, LIPIcs, vol. 59, 10.'
mla: Brázdil, Tomáš, et al. Stability in Graphs and Games. Vol. 59, 10, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.10.
short: T. Brázdil, V. Forejt, A. Kučera, P. Novotný, 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:51:23Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2016.10
ec_funded: 1
file:
- access_level: open_access
checksum: 3c2dc6ab0358f8aa8f7aa7d6c1293159
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:40Z
date_updated: 2020-07-14T12:44:44Z
file_id: '5229'
file_name: IST-2016-665-v1+1_Forejt_et_al__Stability_in_graphs_and_games.pdf
file_size: 553648
relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: ' 59'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5944'
pubrep_id: '665'
quality_controlled: '1'
scopus_import: 1
status: public
title: Stability in graphs and 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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1326'
abstract:
- lang: eng
text: 'Energy Markov Decision Processes (EMDPs) are finite-state Markov decision
processes where each transition is assigned an integer counter update and a rational
payoff. An EMDP configuration is a pair s(n), where s is a control state and n
is the current counter value. The configurations are changed by performing transitions
in the standard way. We consider the problem of computing a safe strategy (i.e.,
a strategy that keeps the counter non-negative) which maximizes the expected mean
payoff. '
acknowledgement: The research was funded by the Czech Science Foundation Grant No.
P202/12/G061 and by the People Programme (Marie Curie Actions) of the European Union’s
Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no [291734].
alternative_title:
- LNCS
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Kučera A, Novotný P. Optimizing the expected mean payoff in Energy
Markov Decision Processes. In: Vol 9938. Springer; 2016:32-49. doi:10.1007/978-3-319-46520-3_3'
apa: 'Brázdil, T., Kučera, A., & Novotný, P. (2016). Optimizing the expected
mean payoff in Energy Markov Decision Processes (Vol. 9938, pp. 32–49). Presented
at the ATVA: Automated Technology for Verification and Analysis, Chiba, Japan:
Springer. https://doi.org/10.1007/978-3-319-46520-3_3'
chicago: Brázdil, Tomáš, Antonín Kučera, and Petr Novotný. “Optimizing the Expected
Mean Payoff in Energy Markov Decision Processes,” 9938:32–49. Springer, 2016.
https://doi.org/10.1007/978-3-319-46520-3_3.
ieee: 'T. Brázdil, A. Kučera, and P. Novotný, “Optimizing the expected mean payoff
in Energy Markov Decision Processes,” presented at the ATVA: Automated Technology
for Verification and Analysis, Chiba, Japan, 2016, vol. 9938, pp. 32–49.'
ista: 'Brázdil T, Kučera A, Novotný P. 2016. Optimizing the expected mean payoff
in Energy Markov Decision Processes. ATVA: Automated Technology for Verification
and Analysis, LNCS, vol. 9938, 32–49.'
mla: Brázdil, Tomáš, et al. Optimizing the Expected Mean Payoff in Energy Markov
Decision Processes. Vol. 9938, Springer, 2016, pp. 32–49, doi:10.1007/978-3-319-46520-3_3.
short: T. Brázdil, A. Kučera, P. Novotný, in:, Springer, 2016, pp. 32–49.
conference:
end_date: 2016-10-20
location: Chiba, Japan
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2016-10-17
date_created: 2018-12-11T11:51:23Z
date_published: 2016-09-22T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '22'
department:
- _id: KrCh
doi: 10.1007/978-3-319-46520-3_3
ec_funded: 1
intvolume: ' 9938'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1607.00678
month: '09'
oa: 1
oa_version: Preprint
page: 32 - 49
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5943'
quality_controlled: '1'
scopus_import: 1
status: public
title: Optimizing the expected mean payoff in Energy Markov Decision Processes
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9938
year: '2016'
...
---
_id: '1327'
abstract:
- lang: eng
text: 'We consider partially observable Markov decision processes (POMDPs) with
a set of target states and positive integer costs associated with every transition.
The traditional optimization objective (stochastic shortest path) asks to minimize
the expected total cost until the target set is reached. We extend the traditional
framework of POMDPs to model energy consumption, which represents a hard constraint.
The energy levels may increase and decrease with transitions, and the hard constraint
requires that the energy level must remain positive in all steps till the target
is reached. First, we present a novel algorithm for solving POMDPs with energy
levels, developing on existing POMDP solvers and using RTDP as its main method.
Our second contribution is related to policy representation. For larger POMDP
instances the policies computed by existing solvers are too large to be understandable.
We present an automated procedure based on machine learning techniques that automatically
extracts important decisions of the policy allowing us to compute succinct human
readable policies. Finally, we show experimentally that our algorithm performs
well and computes succinct policies on a number of POMDP instances from the literature
that were naturally enhanced with energy levels. '
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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Anchit
full_name: Gupta, Anchit
last_name: Gupta
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. Stochastic shortest
path with energy constraints in POMDPs. In: Proceedings of the 15th International
Conference on Autonomous Agents and Multiagent Systems. ACM; 2016:1465-1466.'
apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Gupta, A., & Novotný, P. (2016).
Stochastic shortest path with energy constraints in POMDPs. In Proceedings
of the 15th International Conference on Autonomous Agents and Multiagent Systems
(pp. 1465–1466). Singapore: ACM.'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Anchit Gupta, and
Petr Novotný. “Stochastic Shortest Path with Energy Constraints in POMDPs.” In
Proceedings of the 15th International Conference on Autonomous Agents and Multiagent
Systems, 1465–66. ACM, 2016.
ieee: T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, and P. Novotný, “Stochastic
shortest path with energy constraints in POMDPs,” in Proceedings of the 15th
International Conference on Autonomous Agents and Multiagent Systems, Singapore,
2016, pp. 1465–1466.
ista: 'Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. 2016. Stochastic
shortest path with energy constraints in POMDPs. Proceedings of the 15th International
Conference on Autonomous Agents and Multiagent Systems. AAMAS: Autonomous Agents
& Multiagent Systems, 1465–1466.'
mla: Brázdil, Tomáš, et al. “Stochastic Shortest Path with Energy Constraints in
POMDPs.” Proceedings of the 15th International Conference on Autonomous Agents
and Multiagent Systems, ACM, 2016, pp. 1465–66.
short: T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, P. Novotný, in:, Proceedings
of the 15th International Conference on Autonomous Agents and Multiagent Systems,
ACM, 2016, pp. 1465–1466.
conference:
end_date: 2016-05-13
location: Singapore
name: 'AAMAS: Autonomous Agents & Multiagent Systems'
start_date: 2016-05-09
date_created: 2018-12-11T11:51:23Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:49:54Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1602.07565
month: '01'
oa: 1
oa_version: Preprint
page: 1465 - 1466
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: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the 15th International Conference on Autonomous Agents
and Multiagent Systems
publication_status: published
publisher: ACM
publist_id: '5942'
quality_controlled: '1'
scopus_import: 1
status: public
title: Stochastic shortest path with energy constraints in POMDPs
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1660'
abstract:
- lang: eng
text: We study the pattern frequency vector for runs in probabilistic Vector Addition
Systems with States (pVASS). Intuitively, each configuration of a given pVASS
is assigned one of finitely many patterns, and every run can thus be seen as an
infinite sequence of these patterns. The pattern frequency vector assigns to each
run the limit of pattern frequencies computed for longer and longer prefixes of
the run. If the limit does not exist, then the vector is undefined. We show that
for one-counter pVASS, the pattern frequency vector is defined and takes one of
finitely many values for almost all runs. Further, these values and their associated
probabilities can be approximated up to an arbitrarily small relative error in
polynomial time. For stable two-counter pVASS, we show the same result, but we
do not provide any upper complexity bound. As a byproduct of our study, we discover
counterexamples falsifying some classical results about stochastic Petri nets
published in the 80s.
alternative_title:
- LICS
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Stefan
full_name: Kiefer, Stefan
last_name: Kiefer
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil T, Kiefer S, Kučera A, Novotný P. Long-run average behaviour of probabilistic
vector addition systems. In: IEEE; 2015:44-55. doi:10.1109/LICS.2015.15'
apa: 'Brázdil, T., Kiefer, S., Kučera, A., & Novotný, P. (2015). Long-run average
behaviour of probabilistic vector addition systems (pp. 44–55). Presented at the
LICS: Logic in Computer Science, Kyoto, Japan: IEEE. https://doi.org/10.1109/LICS.2015.15'
chicago: Brázdil, Tomáš, Stefan Kiefer, Antonín Kučera, and Petr Novotný. “Long-Run
Average Behaviour of Probabilistic Vector Addition Systems,” 44–55. IEEE, 2015.
https://doi.org/10.1109/LICS.2015.15.
ieee: 'T. Brázdil, S. Kiefer, A. Kučera, and P. Novotný, “Long-run average behaviour
of probabilistic vector addition systems,” presented at the LICS: Logic in Computer
Science, Kyoto, Japan, 2015, pp. 44–55.'
ista: 'Brázdil T, Kiefer S, Kučera A, Novotný P. 2015. Long-run average behaviour
of probabilistic vector addition systems. LICS: Logic in Computer Science, LICS,
, 44–55.'
mla: Brázdil, Tomáš, et al. Long-Run Average Behaviour of Probabilistic Vector
Addition Systems. IEEE, 2015, pp. 44–55, doi:10.1109/LICS.2015.15.
short: T. Brázdil, S. Kiefer, A. Kučera, P. Novotný, in:, IEEE, 2015, pp. 44–55.
conference:
end_date: 2015-07-10
location: Kyoto, Japan
name: 'LICS: Logic in Computer Science'
start_date: 2015-07-06
date_created: 2018-12-11T11:53:19Z
date_published: 2015-07-01T00:00:00Z
date_updated: 2021-01-12T06:52:20Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/LICS.2015.15
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1505.02655
month: '07'
oa: 1
oa_version: Preprint
page: 44 - 55
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: IEEE
publist_id: '5490'
quality_controlled: '1'
scopus_import: 1
status: public
title: Long-run average behaviour of probabilistic vector addition systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1667'
abstract:
- lang: eng
text: We consider parametric version of fixed-delay continuoustime Markov chains
(or equivalently deterministic and stochastic Petri nets, DSPN) where fixed-delay
transitions are specified by parameters, rather than concrete values. Our goal
is to synthesize values of these parameters that, for a given cost function, minimise
expected total cost incurred before reaching a given set of target states. We
show that under mild assumptions, optimal values of parameters can be effectively
approximated using translation to a Markov decision process (MDP) whose actions
correspond to discretized values of these parameters. To this end we identify
and overcome several interesting phenomena arising in systems with fixed delays.
acknowledgement: The research leading to these results has received funding from the
People Programme (Marie Curie Actions) of the European Union’s Seventh Framework
Programme (FP7/2007-2013) under REA grant agreement n∘ [291734]. This work is partly
supported by the German Research Council (DFG) as part of the Transregional Collaborative
Research Center AVACS (SFB/TR 14), by the EU 7th Framework Programme under grant
agreement no. 295261 (MEALS) and 318490 (SENSATION), by the Czech Science Foundation,
grant No. 15-17564S, and by the CAS/SAFEA International Partnership Program for
Creative Research Teams.
alternative_title:
- LNCS
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: L'Uboš
full_name: Korenčiak, L'Uboš
last_name: Korenčiak
- first_name: Jan
full_name: Krčál, Jan
last_name: Krčál
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Vojtěch
full_name: Řehák, Vojtěch
last_name: Řehák
citation:
ama: Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. Optimizing performance
of continuous-time stochastic systems using timeout synthesis. 2015;9259:141-159.
doi:10.1007/978-3-319-22264-6_10
apa: 'Brázdil, T., Korenčiak, L., Krčál, J., Novotný, P., & Řehák, V. (2015).
Optimizing performance of continuous-time stochastic systems using timeout synthesis.
Presented at the QEST: Quantitative Evaluation of Systems, Madrid, Spain: Springer.
https://doi.org/10.1007/978-3-319-22264-6_10'
chicago: Brázdil, Tomáš, L’Uboš Korenčiak, Jan Krčál, Petr Novotný, and Vojtěch
Řehák. “Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout
Synthesis.” Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-319-22264-6_10.
ieee: T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, and V. Řehák, “Optimizing
performance of continuous-time stochastic systems using timeout synthesis,” vol.
9259. Springer, pp. 141–159, 2015.
ista: Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. 2015. Optimizing performance
of continuous-time stochastic systems using timeout synthesis. 9259, 141–159.
mla: Brázdil, Tomáš, et al. Optimizing Performance of Continuous-Time Stochastic
Systems Using Timeout Synthesis. Vol. 9259, Springer, 2015, pp. 141–59, doi:10.1007/978-3-319-22264-6_10.
short: T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, V. Řehák, 9259 (2015) 141–159.
conference:
end_date: 2015-09-03
location: Madrid, Spain
name: 'QEST: Quantitative Evaluation of Systems'
start_date: 2015-09-01
date_created: 2018-12-11T11:53:22Z
date_published: 2015-08-22T00:00:00Z
date_updated: 2021-01-12T06:52:24Z
day: '22'
department:
- _id: KrCh
doi: 10.1007/978-3-319-22264-6_10
ec_funded: 1
intvolume: ' 9259'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1407.4777
month: '08'
oa: 1
oa_version: Preprint
page: 141 - 159
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5482'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Optimizing performance of continuous-time stochastic systems using timeout
synthesis
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9259
year: '2015'
...
---
_id: '3135'
abstract:
- lang: eng
text: 'We introduce consumption games, a model for discrete interactive system with
multiple resources that are consumed or reloaded independently. More precisely,
a consumption game is a finite-state graph where each transition is labeled by
a vector of resource updates, where every update is a non-positive number or ω.
The ω updates model the reloading of a given resource. Each vertex belongs either
to player □ or player ◇, where the aim of player □ is to play so that the resources
are never exhausted. We consider several natural algorithmic problems about consumption
games, and show that although these problems are computationally hard in general,
they are solvable in polynomial time for every fixed number of resource types
(i.e., the dimension of the update vectors) and bounded resource updates. '
acknowledgement: 'Tomas Brazdil, Antonin Kucera, and Petr Novotny are supported by
the Czech Science Foundation, grant No. P202/10/1469. Krishnendu Chatterjee is supported
by the FWF (Austrian Science Fund) NFN Grant No S11407-N23 (RiSE) and ERC Start
grant (279307: Graph Games).'
alternative_title:
- LNCS
author:
- first_name: Brázdil
full_name: Brázdil, Brázdil
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: Antonín
full_name: Kučera, Antonín
last_name: Kučera
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
citation:
ama: 'Brázdil B, Chatterjee K, Kučera A, Novotný P. Efficient controller synthesis
for consumption games with multiple resource types. In: Vol 7358. Springer; 2012:23-38.
doi:10.1007/978-3-642-31424-7_8'
apa: 'Brázdil, B., Chatterjee, K., Kučera, A., & Novotný, P. (2012). Efficient
controller synthesis for consumption games with multiple resource types (Vol.
7358, pp. 23–38). Presented at the CAV: Computer Aided Verification, Berkeley,
CA, USA: Springer. https://doi.org/10.1007/978-3-642-31424-7_8'
chicago: Brázdil, Brázdil, Krishnendu Chatterjee, Antonín Kučera, and Petr Novotný.
“Efficient Controller Synthesis for Consumption Games with Multiple Resource Types,”
7358:23–38. Springer, 2012. https://doi.org/10.1007/978-3-642-31424-7_8.
ieee: 'B. Brázdil, K. Chatterjee, A. Kučera, and P. Novotný, “Efficient controller
synthesis for consumption games with multiple resource types,” presented at the
CAV: Computer Aided Verification, Berkeley, CA, USA, 2012, vol. 7358, pp. 23–38.'
ista: 'Brázdil B, Chatterjee K, Kučera A, Novotný P. 2012. Efficient controller
synthesis for consumption games with multiple resource types. CAV: Computer Aided
Verification, LNCS, vol. 7358, 23–38.'
mla: Brázdil, Brázdil, et al. Efficient Controller Synthesis for Consumption
Games with Multiple Resource Types. Vol. 7358, Springer, 2012, pp. 23–38,
doi:10.1007/978-3-642-31424-7_8.
short: B. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, in:, Springer, 2012, pp.
23–38.
conference:
end_date: 2012-07-13
location: Berkeley, CA, USA
name: 'CAV: Computer Aided Verification'
start_date: 2012-07-07
date_created: 2018-12-11T12:01:35Z
date_published: 2012-07-01T00:00:00Z
date_updated: 2021-01-12T07:41:18Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-31424-7_8
ec_funded: 1
intvolume: ' 7358'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1202.0796
month: '07'
oa: 1
oa_version: Preprint
page: 23 - 38
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '3562'
quality_controlled: '1'
scopus_import: 1
status: public
title: Efficient controller synthesis for consumption games with multiple resource
types
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7358
year: '2012'
...