---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
PlanS_conform: '1'
_id: '21413'
abstract:
- lang: eng
text: "We present a general framework for applying learning algorithms and heuristical
guidance to the verification of Markov decision processes (MDPs).\r\nThe primary
goal of our techniques is to improve performance by avoiding an exhaustive exploration
of the state space, instead focussing on particularly relevant areas of the system,
guided by heuristics. Our work builds on the previous results of Br{á}zdil et
al., significantly extending it as well as refining several details and fixing
errors.\r\nThe presented framework focuses on probabilistic reachability, which
is a core problem in verification, and is instantiated in two distinct scenarios.\r\nThe
first assumes that full knowledge of the MDP is available, in particular precise
transition probabilities. It performs a heuristic-driven partial exploration of
the model, yielding precise lower and upper bounds on the required probability.
The second tackles the case where we may only sample the MDP without knowing the
exact transition dynamics. Here, we obtain probabilistic guarantees, again in
terms of both the lower and upper bounds, which provides efficient stopping criteria
for the approximation. In particular, the latter is an extension of statistical
model-checking (SMC) for unbounded properties in MDPs. In contrast to other related
approaches, we do not restrict our attention to time-bounded (finite-horizon)
or discounted properties, nor assume any particular structural properties of the
MDP."
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under grant agreement AdG-267989 (QUAREM)*, AdG-246967 (VERIWARE)*, StG-279307
(Graph Games)*\r\n, CoG-863818 (ForM-SMArt), and AdG-834115 (FUN2MODEL), by the
EU FP7 project HIERATIC*, by the German Research Foundation (DFG) project 427755713
(GOPro), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE)* , S11407-N23
(RiSE)*\r\n, and P23499-N23* , by the Czech Science Foundation grant No P202/12/P612*
and GA23-06963S, by the MUNI Award in Science and Humanities (MUNI/I/1757/2021)
of the Grant\r\nAgency of Masaryk University, by EPSRC project EP/K038575/1*, and
by the Microsoft faculty fellows award*. A preliminary version of this article appeared
at ATVA 2014 [33]. The * indicates funding that supported that version."
article_number: '10'
article_processing_charge: Yes
article_type: original
arxiv: 1
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: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Marta
full_name: Kwiatkowska, Marta
last_name: Kwiatkowska
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: David
full_name: Parker, David
last_name: Parker
- first_name: Mateusz
full_name: Ujma, Mateusz
last_name: Ujma
citation:
ama: Brázdil T, Chatterjee K, Chmelik M, et al. Learning algorithms for verification
of Markov decision processes. TheoretiCS. 2025;4. doi:10.46298/theoretics.25.10
apa: Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska,
M., … Ujma, M. (2025). Learning algorithms for verification of Markov decision
processes. TheoretiCS. TheoretiCS Foundation. https://doi.org/10.46298/theoretics.25.10
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt,
Jan Kretinsky, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, and Mateusz
Ujma. “Learning Algorithms for Verification of Markov Decision Processes.” TheoretiCS.
TheoretiCS Foundation, 2025. https://doi.org/10.46298/theoretics.25.10.
ieee: T. Brázdil et al., “Learning algorithms for verification of Markov
decision processes,” TheoretiCS, vol. 4. TheoretiCS Foundation, 2025.
ista: Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M,
Meggendorfer T, Parker D, Ujma M. 2025. Learning algorithms for verification of
Markov decision processes. TheoretiCS. 4, 10.
mla: Brázdil, Tomáš, et al. “Learning Algorithms for Verification of Markov Decision
Processes.” TheoretiCS, vol. 4, 10, TheoretiCS Foundation, 2025, doi:10.46298/theoretics.25.10.
short: T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska,
T. Meggendorfer, D. Parker, M. Ujma, TheoretiCS 4 (2025).
date_created: 2026-03-08T23:01:46Z
date_published: 2025-04-01T00:00:00Z
date_updated: 2026-03-09T11:43:38Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.46298/theoretics.25.10
ec_funded: 1
external_id:
arxiv:
- '2403.09184'
file:
- access_level: open_access
checksum: 2ccf563ae577ee08d82baf752292ca7b
content_type: application/pdf
creator: dernst
date_created: 2026-03-09T11:39:59Z
date_updated: 2026-03-09T11:39:59Z
file_id: '21417'
file_name: 2026_TheoretiCS_Brazdil.pdf
file_size: 861607
relation: main_file
success: 1
file_date_updated: 2026-03-09T11:39:59Z
has_accepted_license: '1'
intvolume: ' 4'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
project:
- _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: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-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
publication: TheoretiCS
publication_identifier:
eissn:
- 2751-4838
publication_status: published
publisher: TheoretiCS Foundation
quality_controlled: '1'
scopus_import: '1'
status: public
title: Learning algorithms for verification of 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19375'
abstract:
- lang: eng
text: "Despite the advances in probabilistic model checking, the scalability of
the verification methods remains limited. In particular, the state space often
becomes extremely large when instantiating parameterized Markov decision processes
(MDPs) even with moderate values. Synthesizing policies for such huge MDPs is
beyond the reach of available tools. We propose a learning-based approach to obtain
a reasonable policy for such huge MDPs.\r\n\r\nThe idea is to generalize optimal
policies obtained by model-checking small instances to larger ones using decision-tree
learning. Consequently, our method bypasses the need for explicit state-space
exploration of large models, providing a practical solution to the state-space
explosion problem. We demonstrate the efficacy of our approach by performing extensive
experimentation on the relevant models from the quantitative verification benchmark
set. The experimental results indicate that our policies perform well, even when
the size of the model is orders of magnitude beyond the reach of state-of-the-art
analysis tools."
acknowledgement: This research was funded in part by the DFG project 427755713 GOPro,
the DFG GRK 2428 (ConVeY), the MUNI Award in Science and Humanities (MUNI/I/1757/2021)
of the Grant Agency of Masaryk University, and the EU under MSCA grant agreement
101034413 (IST-BRIDGE).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Muqsit
full_name: Azeem, Muqsit
last_name: Azeem
- first_name: Debraj
full_name: Chakraborty, Debraj
last_name: Chakraborty
- first_name: Sudeep
full_name: Kanav, Sudeep
last_name: Kanav
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Mohammadsadegh
full_name: Mohagheghi, Mohammadsadegh
last_name: Mohagheghi
- first_name: Stefanie
full_name: Mohr, Stefanie
last_name: Mohr
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
citation:
ama: 'Azeem M, Chakraborty D, Kanav S, et al. 1–2–3–Go! Policy synthesis for parameterized
Markov decision processes via decision-tree learning and generalization. In: 26th
International Conference on Verification, Model Checking, and Abstract Interpretation.
Vol 15530. Springer Nature; 2025:97-120. doi:10.1007/978-3-031-82703-7_5'
apa: 'Azeem, M., Chakraborty, D., Kanav, S., Kretinsky, J., Mohagheghi, M., Mohr,
S., & Weininger, M. (2025). 1–2–3–Go! Policy synthesis for parameterized Markov
decision processes via decision-tree learning and generalization. In 26th International
Conference on Verification, Model Checking, and Abstract Interpretation (Vol.
15530, pp. 97–120). Denver, CO, United States: Springer Nature. https://doi.org/10.1007/978-3-031-82703-7_5'
chicago: Azeem, Muqsit, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh
Mohagheghi, Stefanie Mohr, and Maximilian Weininger. “1–2–3–Go! Policy Synthesis
for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.”
In 26th International Conference on Verification, Model Checking, and Abstract
Interpretation, 15530:97–120. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-82703-7_5.
ieee: M. Azeem et al., “1–2–3–Go! Policy synthesis for parameterized Markov
decision processes via decision-tree learning and generalization,” in 26th
International Conference on Verification, Model Checking, and Abstract Interpretation,
Denver, CO, United States, 2025, vol. 15530, pp. 97–120.
ista: 'Azeem M, Chakraborty D, Kanav S, Kretinsky J, Mohagheghi M, Mohr S, Weininger
M. 2025. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes
via decision-tree learning and generalization. 26th International Conference on
Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification,
Model Checking, and Abstract Interpretation, LNCS, vol. 15530, 97–120.'
mla: Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov
Decision Processes via Decision-Tree Learning and Generalization.” 26th International
Conference on Verification, Model Checking, and Abstract Interpretation, vol.
15530, Springer Nature, 2025, pp. 97–120, doi:10.1007/978-3-031-82703-7_5.
short: M. Azeem, D. Chakraborty, S. Kanav, J. Kretinsky, M. Mohagheghi, S. Mohr,
M. Weininger, in:, 26th International Conference on Verification, Model Checking,
and Abstract Interpretation, Springer Nature, 2025, pp. 97–120.
conference:
end_date: 2025-01-21
location: Denver, CO, United States
name: 'VMCAI: Verification, Model Checking, and Abstract Interpretation'
start_date: 2025-01-20
date_created: 2025-03-09T23:01:29Z
date_published: 2025-01-23T00:00:00Z
date_updated: 2025-09-30T10:46:54Z
day: '23'
department:
- _id: KrCh
doi: 10.1007/978-3-031-82703-7_5
ec_funded: 1
external_id:
arxiv:
- '2410.18293'
isi:
- '001446577100005'
intvolume: ' 15530'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2410.18293
month: '01'
oa: 1
oa_version: Preprint
page: 97-120
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 26th International Conference on Verification, Model Checking, and Abstract
Interpretation
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031827020'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree
learning and generalization
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15530
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20688'
abstract:
- lang: eng
text: 'We consider two-player zero-sum concurrent stochastic games (CSGs) played
on graphs with reachability and safety objectives. These include degenerate classes
such as Markov decision processes or turn-based stochastic games, which can be
solved by linear or quadratic programming; however, in practice, value iteration
(VI) outperforms the other approaches and is the most implemented method. Similarly,
for CSGs, this practical performance makes VI an attractive alternative to the
standard theoretical solution via the existential theory of reals.VI starts with
an under-approximation of the sought values for each state and iteratively updates
them, traditionally terminating once two consecutive approximations are ϵ-close.
However, this stopping criterion lacks guarantees on the precision of the approximation,
which is the goal of this work. We provide bounded (a.k.a. interval) VI for CSGs:
it complements standard VI with a converging sequence of over-approximations and
terminates once the over- and under-approximations are ϵ-close.'
acknowledgement: This research was funded in part by the German Research Foundation
(DFG) project 427755713 GOPro, the MUNI Award in Science and Humanities (MUNI/I/1757/2021)
of the Grant Agency of Masaryk University, the European Union’s Horizon 2020 research
and innovation programme under the Marie Sklodowska-Curie grant agreement No 101034413,
and the ERC Starting Grant DEUCE (101077178).
article_processing_charge: No
arxiv: 1
author:
- first_name: Marta
full_name: Grobelna, Marta
last_name: Grobelna
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
orcid: 0000-0002-0163-2152
citation:
ama: 'Grobelna M, Kretinsky J, Weininger M. Stopping criteria for value iteration
on concurrent stochastic reachability and safety games. In: 2025 40th Annual
ACM/IEEE Symposium on Logic in Computer Science. IEEE; 2025:568-580. doi:10.1109/lics65433.2025.00049'
apa: 'Grobelna, M., Kretinsky, J., & Weininger, M. (2025). Stopping criteria
for value iteration on concurrent stochastic reachability and safety games. In
2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 568–580).
Singapore, Singapore: IEEE. https://doi.org/10.1109/lics65433.2025.00049'
chicago: Grobelna, Marta, Jan Kretinsky, and Maximilian Weininger. “Stopping Criteria
for Value Iteration on Concurrent Stochastic Reachability and Safety Games.” In
2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science, 568–80.
IEEE, 2025. https://doi.org/10.1109/lics65433.2025.00049.
ieee: M. Grobelna, J. Kretinsky, and M. Weininger, “Stopping criteria for value
iteration on concurrent stochastic reachability and safety games,” in 2025
40th Annual ACM/IEEE Symposium on Logic in Computer Science, Singapore, Singapore,
2025, pp. 568–580.
ista: 'Grobelna M, Kretinsky J, Weininger M. 2025. Stopping criteria for value iteration
on concurrent stochastic reachability and safety games. 2025 40th Annual ACM/IEEE
Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 568–580.'
mla: Grobelna, Marta, et al. “Stopping Criteria for Value Iteration on Concurrent
Stochastic Reachability and Safety Games.” 2025 40th Annual ACM/IEEE Symposium
on Logic in Computer Science, IEEE, 2025, pp. 568–80, doi:10.1109/lics65433.2025.00049.
short: M. Grobelna, J. Kretinsky, M. Weininger, in:, 2025 40th Annual ACM/IEEE Symposium
on Logic in Computer Science, IEEE, 2025, pp. 568–580.
conference:
end_date: 2025-06-26
location: Singapore, Singapore
name: 'LICS: Logic in Computer Science'
start_date: 2025-06-23
corr_author: '1'
date_created: 2025-11-24T14:23:49Z
date_published: 2025-10-09T00:00:00Z
date_updated: 2025-11-26T07:34:19Z
day: '09'
department:
- _id: KrCh
doi: 10.1109/lics65433.2025.00049
ec_funded: 1
external_id:
arxiv:
- '2505.21087'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2505.21087
month: '10'
oa: 1
oa_version: Preprint
page: 568-580
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science
publication_identifier:
eisbn:
- '9798331579005'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Stopping criteria for value iteration on concurrent stochastic reachability
and safety games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '18600'
abstract:
- lang: eng
text: 'The analysis of formal models that include quantitative aspects such as timing
or probabilistic choices is performed by quantitative verification tools. Broad
and mature tool support is available for computing basic properties such as expected
rewards on basic models such as Markov chains. Previous editions of QComp, the
comparison of tools for the analysis of quantitative formal models, focused on
this setting. Many application scenarios, however, require more advanced property
types such as LTL and parameter synthesis queries as well as advanced models like
stochastic games and partially observable MDPs. For these, tool support is in
its infancy today. This paper presents the outcomes of QComp 2023: a survey of
the state of the art in quantitative verification tool support for advanced property
types and models. With tools ranging from first research prototypes to well-supported
integrations into established toolsets, this report highlights today’s active
areas and tomorrow’s challenges in tool-focused research for quantitative verification.'
acknowledgement: The authors are ordered alphabetically. This work was supported by
DFG RTG 2236/2 (UnRAVeL) and DFG project TRR 248 (CPEC, ID 389792660), by the EU
under MSCA grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199
(ProSVED), by ERC Starting Grant 101077178 (DEUCE), ERC Consolidator Grant 864075
(CAESAR), and ERC Advanced Grant 834115 (FUN2MODEL), by GAČR grant GA23-06963S (VESCAA),
by National Science Foundation grant 1856733, by NextGenerationEU project D53D23008400006
(SMARTITUDE), and by NWO VENI grant 639.021.754.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Roman
full_name: Andriushchenko, Roman
last_name: Andriushchenko
- first_name: Alexander
full_name: Bork, Alexander
last_name: Bork
- first_name: Carlos E.
full_name: Budde, Carlos E.
last_name: Budde
- first_name: Milan
full_name: Češka, Milan
last_name: Češka
- first_name: Kush
full_name: Grover, Kush
last_name: Grover
- first_name: Ernst Moritz
full_name: Hahn, Ernst Moritz
last_name: Hahn
- first_name: Arnd
full_name: Hartmanns, Arnd
last_name: Hartmanns
- first_name: Bryant
full_name: Israelsen, Bryant
last_name: Israelsen
- first_name: Nils
full_name: Jansen, Nils
last_name: Jansen
- first_name: Joshua
full_name: Jeppson, Joshua
last_name: Jeppson
- first_name: Sebastian
full_name: Junges, Sebastian
last_name: Junges
- first_name: Maximilian A.
full_name: Köhl, Maximilian A.
last_name: Köhl
- first_name: Bettina
full_name: Könighofer, Bettina
last_name: Könighofer
- 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: David
full_name: Parker, David
last_name: Parker
- first_name: Stefan
full_name: Pranger, Stefan
last_name: Pranger
- first_name: Tim
full_name: Quatmann, Tim
last_name: Quatmann
- first_name: Enno
full_name: Ruijters, Enno
last_name: Ruijters
- first_name: Landon
full_name: Taylor, Landon
last_name: Taylor
- first_name: Matthias
full_name: Volk, Matthias
last_name: Volk
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
- first_name: Zhen
full_name: Zhang, Zhen
last_name: Zhang
citation:
ama: 'Andriushchenko R, Bork A, Budde CE, et al. Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report. In: TOOLympics Challenge 2023.
Vol 14550. Springer Nature; 2024:90-146. doi:10.1007/978-3-031-67695-6_4'
apa: 'Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E.
M., … Zhang, Z. (2024). Tools at the Frontiers of Quantitative Verification: QComp
2023 Competition Report. In TOOLympics Challenge 2023 (Vol. 14550, pp.
90–146). Springer Nature. https://doi.org/10.1007/978-3-031-67695-6_4'
chicago: 'Andriushchenko, Roman, Alexander Bork, Carlos E. Budde, Milan Češka, Kush
Grover, Ernst Moritz Hahn, Arnd Hartmanns, et al. “Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report.” In TOOLympics Challenge 2023,
14550:90–146. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-67695-6_4.'
ieee: 'R. Andriushchenko et al., “Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report,” in TOOLympics Challenge 2023,
2024, vol. 14550, pp. 90–146.'
ista: 'Andriushchenko R, Bork A, Budde CE, Češka M, Grover K, Hahn EM, Hartmanns
A, Israelsen B, Jansen N, Jeppson J, Junges S, Köhl MA, Könighofer B, Kretinsky
J, Meggendorfer T, Parker D, Pranger S, Quatmann T, Ruijters E, Taylor L, Volk
M, Weininger M, Zhang Z. 2024. Tools at the Frontiers of Quantitative Verification:
QComp 2023 Competition Report. TOOLympics Challenge 2023. , LNCS, vol. 14550,
90–146.'
mla: 'Andriushchenko, Roman, et al. “Tools at the Frontiers of Quantitative Verification:
QComp 2023 Competition Report.” TOOLympics Challenge 2023, vol. 14550,
Springer Nature, 2024, pp. 90–146, doi:10.1007/978-3-031-67695-6_4.'
short: R. Andriushchenko, A. Bork, C.E. Budde, M. Češka, K. Grover, E.M. Hahn, A.
Hartmanns, B. Israelsen, N. Jansen, J. Jeppson, S. Junges, M.A. Köhl, B. Könighofer,
J. Kretinsky, T. Meggendorfer, D. Parker, S. Pranger, T. Quatmann, E. Ruijters,
L. Taylor, M. Volk, M. Weininger, Z. Zhang, in:, TOOLympics Challenge 2023, Springer
Nature, 2024, pp. 90–146.
date_created: 2024-12-01T23:01:53Z
date_published: 2024-11-01T00:00:00Z
date_updated: 2025-09-08T14:45:11Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-031-67695-6_4
external_id:
arxiv:
- '2405.13583'
isi:
- '001434957500004'
intvolume: ' 14550'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.2405.13583'
month: '11'
oa: 1
oa_version: Preprint
page: 90-146
publication: TOOLympics Challenge 2023
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031676949'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition
Report'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14550
year: '2024'
...
---
_id: '14259'
abstract:
- lang: eng
text: "We provide a learning-based technique for guessing a winning strategy in
a parity game originating from an LTL synthesis problem. A cheaply obtained guess
can be useful in several applications. Not only can the guessed strategy be applied
as best-effort in cases where the game’s huge size prohibits rigorous approaches,
but it can also increase the scalability of rigorous LTL synthesis in several
ways. Firstly, checking whether a guessed strategy is winning is easier than constructing
one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy
iteration faster than constructing one from scratch. Thirdly, the guess can be
used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn
contrast to previous works, we (i) reflect the highly structured logical information
in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata
translations, and (ii) learn to reflect it properly by learning from previously
solved games, bringing the solving process closer to human-like reasoning."
acknowledgement: This research was funded in part by the German Research Foundation
(DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
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: Maximilian
full_name: Prokop, Maximilian
last_name: Prokop
- first_name: Sabine
full_name: Rieder, Sabine
last_name: Rieder
citation:
ama: 'Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies
in LTL synthesis by semantic learning. In: 35th International Conference on
Computer Aided Verification. Vol 13964. Springer Nature; 2023:390-414. doi:10.1007/978-3-031-37706-8_20'
apa: 'Kretinsky, J., Meggendorfer, T., Prokop, M., & Rieder, S. (2023). Guessing
winning policies in LTL synthesis by semantic learning. In 35th International
Conference on Computer Aided Verification (Vol. 13964, pp. 390–414). Paris,
France: Springer Nature. https://doi.org/10.1007/978-3-031-37706-8_20'
chicago: Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder.
“Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In 35th
International Conference on Computer Aided Verification, 13964:390–414. Springer
Nature, 2023. https://doi.org/10.1007/978-3-031-37706-8_20.
ieee: J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning
policies in LTL synthesis by semantic learning,” in 35th International Conference
on Computer Aided Verification, Paris, France, 2023, vol. 13964, pp. 390–414.
ista: 'Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies
in LTL synthesis by semantic learning. 35th International Conference on Computer
Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414.'
mla: Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic
Learning.” 35th International Conference on Computer Aided Verification,
vol. 13964, Springer Nature, 2023, pp. 390–414, doi:10.1007/978-3-031-37706-8_20.
short: J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International
Conference on Computer Aided Verification, Springer Nature, 2023, pp. 390–414.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
das_tickbox: '1'
date_created: 2023-09-03T22:01:16Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2026-07-07T13:39:23Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37706-8_20
external_id:
isi:
- '001310786500020'
file:
- access_level: open_access
checksum: ed66278b61bb869e1baba3d9b9081271
content_type: application/pdf
creator: dernst
date_created: 2023-09-06T08:25:50Z
date_updated: 2023-09-06T08:25:50Z
file_id: '14276'
file_name: 2023_LNCS_CAV_Kretinsky.pdf
file_size: 428354
relation: main_file
success: 1
file_date_updated: 2023-09-06T08:25:50Z
has_accepted_license: '1'
intvolume: ' 13964'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 390-414
publication: 35th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031377051'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Guessing winning policies in LTL synthesis by semantic learning
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: 13964
year: '2023'
...
---
_id: '13967'
abstract:
- lang: eng
text: 'A classic solution technique for Markov decision processes (MDP) and stochastic
games (SG) is value iteration (VI). Due to its good practical performance, this
approximative approach is typically preferred over exact techniques, even though
no practical bounds on the imprecision of the result could be given until recently.
As a consequence, even the most used model checkers could return arbitrarily wrong
results. Over the past decade, different works derived stopping criteria, indicating
when the precision reaches the desired level, for various settings, in particular
MDP with reachability, total reward, and mean payoff, and SG with reachability.In
this paper, we provide the first stopping criteria for VI on SG with total reward
and mean payoff, yielding the first anytime algorithms in these settings. To this
end, we provide the solution in two flavours: First through a reduction to the
MDP case and second directly on SG. The former is simpler and automatically utilizes
any advances on MDP. The latter allows for more local computations, heading towards
better practical efficiency.Our solution unifies the previously mentioned approaches
for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific
subroutines as well as identify objective-independent concepts. These structural
concepts, while surprisingly simple, form the very essence of the unified solution.'
acknowledgement: This research was funded in part by DFG projects 383882557 “SUV”
and 427755713 “GOPro”.
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: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
orcid: 0000-0002-0163-2152
citation:
ama: 'Kretinsky J, Meggendorfer T, Weininger M. Stopping criteria for value iteration
on stochastic games with quantitative objectives. In: 38th Annual ACM/IEEE
Symposium on Logic in Computer Science. Vol 2023. IEEE; 2023. doi:10.1109/LICS56636.2023.10175771'
apa: 'Kretinsky, J., Meggendorfer, T., & Weininger, M. (2023). Stopping criteria
for value iteration on stochastic games with quantitative objectives. In 38th
Annual ACM/IEEE Symposium on Logic in Computer Science (Vol. 2023). Boston,
MA, United States: IEEE. https://doi.org/10.1109/LICS56636.2023.10175771'
chicago: Kretinsky, Jan, Tobias Meggendorfer, and Maximilian Weininger. “Stopping
Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.”
In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Vol. 2023.
IEEE, 2023. https://doi.org/10.1109/LICS56636.2023.10175771.
ieee: J. Kretinsky, T. Meggendorfer, and M. Weininger, “Stopping criteria for value
iteration on stochastic games with quantitative objectives,” in 38th Annual
ACM/IEEE Symposium on Logic in Computer Science, Boston, MA, United States,
2023, vol. 2023.
ista: 'Kretinsky J, Meggendorfer T, Weininger M. 2023. Stopping criteria for value
iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE
Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2023.'
mla: Kretinsky, Jan, et al. “Stopping Criteria for Value Iteration on Stochastic
Games with Quantitative Objectives.” 38th Annual ACM/IEEE Symposium on Logic
in Computer Science, vol. 2023, IEEE, 2023, doi:10.1109/LICS56636.2023.10175771.
short: J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium
on Logic in Computer Science, IEEE, 2023.
conference:
end_date: 2023-06-29
location: Boston, MA, United States
name: 'LICS: Logic in Computer Science'
start_date: 2023-06-26
corr_author: '1'
date_created: 2023-08-06T22:01:10Z
date_published: 2023-07-01T00:00:00Z
date_updated: 2026-08-12T06:39:58Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/LICS56636.2023.10175771
external_id:
arxiv:
- '2304.09930'
isi:
- '001036707700042'
intvolume: ' 2023'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2304.09930
month: '07'
oa: 1
oa_version: Preprint
publication: 38th Annual ACM/IEEE Symposium on Logic in Computer Science
publication_identifier:
isbn:
- '9798350335873'
issn:
- 1043-6871
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Stopping criteria for value iteration on stochastic games with quantitative
objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2023
year: '2023'
...
---
_id: '10602'
abstract:
- lang: eng
text: Transforming ω-automata into parity automata is traditionally done using appearance
records. We present an efficient variant of this idea, tailored to Rabin automata,
and several optimizations applicable to all appearance records. We compare the
methods experimentally and show that our method produces significantly smaller
automata than previous approaches.
acknowledgement: This work is partially funded by the German Research Foundation (DFG)
projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification
(No. 383882557), and the Alexander von Humboldt Foundation with funds from the German
Federal Ministry of Education and Research. It is an extended version of [21], including
all proofs together with further explanations and examples. Moreover, we provide
a new, more efficient construction based on (total) preorders, unifying previous
optimizations. Experiments are performed with a new, performant implementation,
comparing our approach to the current state of the art.
article_processing_charge: Yes (via OA deal)
article_type: original
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
with preorders. Acta Informatica. 2022;59:585-618. doi:10.1007/s00236-021-00412-y
apa: Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2022).
Index appearance record with preorders. Acta Informatica. Springer Nature.
https://doi.org/10.1007/s00236-021-00412-y
chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
“Index Appearance Record with Preorders.” Acta Informatica. Springer Nature,
2022. https://doi.org/10.1007/s00236-021-00412-y.
ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
record with preorders,” Acta Informatica, vol. 59. Springer Nature, pp.
585–618, 2022.
ista: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance
record with preorders. Acta Informatica. 59, 585–618.
mla: Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” Acta Informatica,
vol. 59, Springer Nature, 2022, pp. 585–618, doi:10.1007/s00236-021-00412-y.
short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica
59 (2022) 585–618.
corr_author: '1'
date_created: 2022-01-06T12:37:27Z
date_published: 2022-10-01T00:00:00Z
date_updated: 2025-04-15T06:53:08Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s00236-021-00412-y
external_id:
isi:
- '000735765500001'
file:
- access_level: open_access
checksum: bf1c195b6aaf59e8530cf9e3a9d731f7
content_type: application/pdf
creator: cchlebak
date_created: 2022-01-07T07:50:31Z
date_updated: 2022-01-07T07:50:31Z
file_id: '10603'
file_name: 2021_ActaInfor_Křetínský.pdf
file_size: 1066082
relation: main_file
success: 1
file_date_updated: 2022-01-07T07:50:31Z
has_accepted_license: '1'
intvolume: ' 59'
isi: 1
keyword:
- computer networks and communications
- information systems
- software
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 585-618
project:
- _id: B67AFEDC-15C9-11EA-A837-991A96BB2854
name: IST Austria Open Access Fund
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Index appearance record with preorders
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 59
year: '2022'
...
---
_id: '12775'
abstract:
- lang: eng
text: "We consider the problem of approximating the reachability probabilities in
Markov decision processes (MDP) with uncountable (continuous) state and action
spaces. While there are algorithms that, for special classes of such MDP, provide
a sequence of approximations converging to the true value in the limit, our aim
is to obtain an algorithm with guarantees on the precision of the approximation.\r\nAs
this problem is undecidable in general, assumptions on the MDP are necessary.
Our main contribution is to identify sufficient assumptions that are as weak as
possible, thus approaching the \"boundary\" of which systems can be correctly
and reliably analyzed. To this end, we also argue why each of our assumptions
is necessary for algorithms based on processing finitely many observations.\r\nWe
present two solution variants. The first one provides converging lower bounds
under weaker assumptions than typical ones from previous works concerned with
guarantees. The second one then utilizes stronger assumptions to additionally
provide converging upper bounds. Altogether, we obtain an anytime algorithm, i.e.
yielding a sequence of approximants with known and iteratively improving precision,
converging to the true value in the limit. Besides, due to the generality of our
assumptions, our algorithms are very general templates, readily allowing for various
heuristics from literature in contrast to, e.g., a specific discretization algorithm.
Our theoretical contribution thus paves the way for future practical improvements
without sacrificing correctness guarantees."
acknowledgement: "Kush Grover: The author has been supported by the DFG research training
group GRK\r\n2428 ConVeY.\r\nMaximilian Weininger: The author has been partially
supported by DFG projects 383882557\r\nStatistical Unbounded Verification (SUV)
and 427755713 Group-By Objectives in Probabilistic\r\nVerification (GOPro)"
alternative_title:
- LIPIcs
article_number: '11'
article_processing_charge: No
arxiv: 1
author:
- first_name: Kush
full_name: Grover, Kush
last_name: Grover
- 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: Maimilian
full_name: Weininger, Maimilian
last_name: Weininger
citation:
ama: 'Grover K, Kretinsky J, Meggendorfer T, Weininger M. Anytime guarantees for
reachability in uncountable Markov decision processes. In: 33rd International
Conference on Concurrency Theory. Vol 243. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2022. doi:10.4230/LIPIcs.CONCUR.2022.11'
apa: 'Grover, K., Kretinsky, J., Meggendorfer, T., & Weininger, M. (2022). Anytime
guarantees for reachability in uncountable Markov decision processes. In 33rd
International Conference on Concurrency Theory (Vol. 243). Warsaw, Poland:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2022.11'
chicago: Grover, Kush, Jan Kretinsky, Tobias Meggendorfer, and Maimilian Weininger.
“Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.”
In 33rd International Conference on Concurrency Theory, Vol. 243. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.CONCUR.2022.11.
ieee: K. Grover, J. Kretinsky, T. Meggendorfer, and M. Weininger, “Anytime guarantees
for reachability in uncountable Markov decision processes,” in 33rd International
Conference on Concurrency Theory, Warsaw, Poland, 2022, vol. 243.
ista: 'Grover K, Kretinsky J, Meggendorfer T, Weininger M. 2022. Anytime guarantees
for reachability in uncountable Markov decision processes. 33rd International
Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs,
vol. 243, 11.'
mla: Grover, Kush, et al. “Anytime Guarantees for Reachability in Uncountable Markov
Decision Processes.” 33rd International Conference on Concurrency Theory,
vol. 243, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:10.4230/LIPIcs.CONCUR.2022.11.
short: K. Grover, J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 33rd International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2022.
conference:
end_date: 2022-09-16
location: Warsaw, Poland
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2022-09-13
corr_author: '1'
das_tickbox: '1'
date_created: 2023-03-28T08:09:32Z
date_published: 2022-09-15T00:00:00Z
date_updated: 2026-07-07T13:37:58Z
day: '15'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2022.11
external_id:
arxiv:
- '2008.04824'
file:
- access_level: open_access
checksum: e282e43d3ae0ba6e067b72f4583e13c0
content_type: application/pdf
creator: dernst
date_created: 2023-09-26T10:43:15Z
date_updated: 2023-09-26T10:43:15Z
file_id: '14372'
file_name: 2022_LIPIcS_Grover.pdf
file_size: 960036
relation: main_file
success: 1
file_date_updated: 2023-09-26T10:43:15Z
has_accepted_license: '1'
intvolume: ' 243'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
publication: 33rd International Conference on Concurrency Theory
publication_identifier:
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Anytime guarantees for reachability in uncountable 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: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 243
year: '2022'
...
---
_id: '297'
abstract:
- lang: eng
text: Graph games played by two players over finite-state graphs are central in
many problems in computer science. In particular, graph games with ω -regular
winning conditions, specified as parity objectives, which can express properties
such as safety, liveness, fairness, are the basic framework for verification and
synthesis of reactive systems. The decisions for a player at various states of
the graph game are represented as strategies. While the algorithmic problem for
solving graph games with parity objectives has been widely studied, the most prominent
data-structure for strategy representation in graph games has been binary decision
diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain
the inherent flavor of the decisions of strategies, and are notoriously hard to
minimize to obtain succinct representation. In this work we propose decision trees
for strategy representation in graph games. Decision trees retain the flavor of
decisions of strategies and allow entropy-based minimization to obtain succinct
trees. However, decision trees work in settings (e.g., probabilistic models) where
errors are allowed, and overfitting of data is typically avoided. In contrast,
for strategies in graph games no error is allowed, and the decision tree must
represent the entire strategy. We develop new techniques to extend decision trees
to overcome the above obstacles, while retaining the entropy-based techniques
to obtain succinct trees. We have implemented our techniques to extend the existing
decision tree solvers. We present experimental results for problems in reactive
synthesis to show that decision trees provide a much more efficient data-structure
for strategy representation as compared to BDDs.
alternative_title:
- LNCS
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: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Viktor
full_name: Toman, Viktor
id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
last_name: Toman
orcid: 0000-0001-9036-063X
citation:
ama: 'Brázdil T, Chatterjee K, Kretinsky J, Toman V. Strategy representation by
decision trees in reactive synthesis. In: Vol 10805. Springer; 2018:385-407. doi:10.1007/978-3-319-89960-2_21'
apa: 'Brázdil, T., Chatterjee, K., Kretinsky, J., & Toman, V. (2018). Strategy
representation by decision trees in reactive synthesis (Vol. 10805, pp. 385–407).
Presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis
of Systems, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89960-2_21'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Jan Kretinsky, and Viktor Toman.
“Strategy Representation by Decision Trees in Reactive Synthesis,” 10805:385–407.
Springer, 2018. https://doi.org/10.1007/978-3-319-89960-2_21.
ieee: 'T. Brázdil, K. Chatterjee, J. Kretinsky, and V. Toman, “Strategy representation
by decision trees in reactive synthesis,” presented at the TACAS 2018: Tools and
Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece,
2018, vol. 10805, pp. 385–407.'
ista: 'Brázdil T, Chatterjee K, Kretinsky J, Toman V. 2018. Strategy representation
by decision trees in reactive synthesis. TACAS 2018: Tools and Algorithms for
the Construction and Analysis of Systems, LNCS, vol. 10805, 385–407.'
mla: Brázdil, Tomáš, et al. Strategy Representation by Decision Trees in Reactive
Synthesis. Vol. 10805, Springer, 2018, pp. 385–407, doi:10.1007/978-3-319-89960-2_21.
short: T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp.
385–407.
conference:
end_date: 2018-04-20
location: Thessaloniki, Greece
name: 'TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2018-04-14
date_created: 2018-12-11T11:45:41Z
date_published: 2018-04-12T00:00:00Z
date_updated: 2025-03-31T16:01:11Z
day: '12'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-89960-2_21
ec_funded: 1
external_id:
isi:
- '000546326300021'
file:
- access_level: open_access
checksum: b13874ffb114932ad9cc2586b7469db4
content_type: application/pdf
creator: dernst
date_created: 2018-12-17T16:29:08Z
date_updated: 2020-07-14T12:45:57Z
file_id: '5723'
file_name: 2018_LNCS_Brazdil.pdf
file_size: 1829940
relation: main_file
file_date_updated: 2020-07-14T12:45:57Z
has_accepted_license: '1'
intvolume: ' 10805'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 385 - 407
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'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication_status: published
publisher: Springer
publist_id: '7584'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Strategy representation by decision trees in reactive synthesis
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10805
year: '2018'
...
---
_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
corr_author: '1'
date_created: 2023-06-21T13:21:14Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2025-09-18T10:42:48Z
day: '31'
department:
- _id: KrCh
doi: 10.1007/978-3-662-54577-5_26
external_id:
arxiv:
- '1701.05738'
isi:
- '000440734900026'
intvolume: ' 10205'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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: 2025-06-11T06:33:00Z
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: '471'
abstract:
- lang: eng
text: 'We present a new algorithm for the statistical model checking of Markov chains
with respect to unbounded temporal properties, including full linear temporal
logic. The main idea is that we monitor each simulation run on the fly, in order
to detect quickly if a bottom strongly connected component is entered with high
probability, in which case the simulation run can be terminated early. As a result,
our simulation runs are often much shorter than required by termination bounds
that are computed a priori for a desired level of confidence on a large state
space. In comparison to previous algorithms for statistical model checking our
method is not only faster in many cases but also requires less information about
the system, namely, only the minimum transition probability that occurs in the
Markov chain. In addition, our method can be generalised to unbounded quantitative
properties such as mean-payoff bounds. '
article_number: '12'
article_processing_charge: No
arxiv: 1
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. Faster statistical model checking
for unbounded temporal properties. ACM Transactions on Computational Logic.
2017;18(2). doi:10.1145/3060139
apa: Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2017). Faster
statistical model checking for unbounded temporal properties. ACM Transactions
on Computational Logic. ACM. https://doi.org/10.1145/3060139
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Faster Statistical Model Checking for Unbounded Temporal Properties.” ACM
Transactions on Computational Logic. ACM, 2017. https://doi.org/10.1145/3060139.
ieee: P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
model checking for unbounded temporal properties,” ACM Transactions on Computational
Logic, vol. 18, no. 2. ACM, 2017.
ista: Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model
checking for unbounded temporal properties. ACM Transactions on Computational
Logic. 18(2), 12.
mla: Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal
Properties.” ACM Transactions on Computational Logic, vol. 18, no. 2, 12,
ACM, 2017, doi:10.1145/3060139.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational
Logic 18 (2017).
corr_author: '1'
date_created: 2018-12-11T11:46:39Z
date_published: 2017-05-01T00:00:00Z
date_updated: 2025-09-22T09:21:16Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3060139
ec_funded: 1
external_id:
arxiv:
- '1504.05739'
isi:
- '000405208400005'
intvolume: ' 18'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.05739
month: '05'
oa: 1
oa_version: Submitted Version
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: ACM Transactions on Computational Logic
publication_identifier:
issn:
- 1529-3785
publication_status: published
publisher: ACM
publist_id: '7349'
quality_controlled: '1'
related_material:
record:
- id: '1234'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Faster statistical model checking for unbounded temporal properties
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 18
year: '2017'
...
---
_id: '645'
abstract:
- lang: eng
text: Markov decision processes (MDPs) are standard models for probabilistic systems
with non-deterministic behaviours. Long-run average rewards provide a mathematically
elegant formalism for expressing long term performance. Value iteration (VI) is
one of the simplest and most efficient algorithmic approaches to MDPs with other
properties, such as reachability objectives. Unfortunately, a naive extension
of VI does not work for MDPs with long-run average rewards, as there is no known
stopping criterion. In this work our contributions are threefold. (1) We refute
a conjecture related to stopping criteria for MDPs with long-run average rewards.
(2) We present two practical algorithms for MDPs with long-run average rewards
based on VI. First, we show that a combination of applying VI locally for each
maximal end-component (MEC) and VI for reachability objectives can provide approximation
guarantees. Second, extending the above approach with a simulation-guided on-demand
variant of VI, we present an anytime algorithm that is able to deal with very
large models. (3) Finally, we present experimental results showing that our methods
significantly outperform the standard approaches on several benchmarks.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Pranav
full_name: Ashok, Pranav
last_name: Ashok
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: 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
last_name: Meggendorfer
citation:
ama: 'Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. Value iteration
for long run average reward in markov decision processes. In: Majumdar R, Kunčak
V, eds. Vol 10426. Springer; 2017:201-221. doi:10.1007/978-3-319-63387-9_10'
apa: 'Ashok, P., Chatterjee, K., Daca, P., Kretinsky, J., & Meggendorfer, T.
(2017). Value iteration for long run average reward in markov decision processes.
In R. Majumdar & V. Kunčak (Eds.) (Vol. 10426, pp. 201–221). Presented at
the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63387-9_10'
chicago: Ashok, Pranav, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretinsky, and
Tobias Meggendorfer. “Value Iteration for Long Run Average Reward in Markov Decision
Processes.” edited by Rupak Majumdar and Viktor Kunčak, 10426:201–21. Springer,
2017. https://doi.org/10.1007/978-3-319-63387-9_10.
ieee: 'P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, and T. Meggendorfer, “Value
iteration for long run average reward in markov decision processes,” presented
at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426,
pp. 201–221.'
ista: 'Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. 2017. Value iteration
for long run average reward in markov decision processes. CAV: Computer Aided
Verification, LNCS, vol. 10426, 201–221.'
mla: Ashok, Pranav, et al. Value Iteration for Long Run Average Reward in Markov
Decision Processes. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426,
Springer, 2017, pp. 201–21, doi:10.1007/978-3-319-63387-9_10.
short: P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R.
Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.
conference:
end_date: 2017-07-28
location: Heidelberg, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2017-07-24
date_created: 2018-12-11T11:47:41Z
date_published: 2017-07-13T00:00:00Z
date_updated: 2025-09-11T07:18:04Z
day: '13'
department:
- _id: KrCh
doi: 10.1007/978-3-319-63387-9_10
ec_funded: 1
editor:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Viktor
full_name: Kunčak, Viktor
last_name: Kunčak
external_id:
arxiv:
- '1705.02326'
isi:
- '000432196400010'
intvolume: ' 10426'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1705.02326
month: '07'
oa: 1
oa_version: Submitted Version
page: 201 - 221
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided 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_identifier:
isbn:
- 978-331963386-2
publication_status: published
publisher: Springer
publist_id: '7135'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Value iteration for long run average reward in markov decision processes
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 10426
year: '2017'
...
---
_id: '466'
abstract:
- lang: eng
text: 'We consider Markov decision processes (MDPs) with multiple limit-average
(or mean-payoff) objectives. There exist two different views: (i) the expectation
semantics, where the goal is to optimize the expected mean-payoff objective, and
(ii) the satisfaction semantics, where the goal is to maximize the probability
of runs such that the mean-payoff value stays above a given vector. We consider
optimization with respect to both objectives at once, thus unifying the existing
semantics. Precisely, the goal is to optimize the expectation while ensuring the
satisfaction constraint. Our problem captures the notion of optimization with
respect to strategies that are risk-averse (i.e., ensure certain probabilistic
guarantee). Our main results are as follows: First, we present algorithms for
the decision problems which are always polynomial in the size of the MDP. We also
show that an approximation of the Pareto-curve can be computed in time polynomial
in the size of the MDP, and the approximation factor, but exponential in the number
of dimensions. Second, we present a complete characterization of the strategy
complexity (in terms of memory bounds and randomization) required to solve our
problem. '
article_number: '15'
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: Zuzana
full_name: Křetínská, Zuzana
last_name: Křetínská
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff
objectives in Markov decision processes. Logical Methods in Computer Science.
2017;13(2). doi:10.23638/LMCS-13(2:15)2017
apa: Chatterjee, K., Křetínská, Z., & Kretinsky, J. (2017). Unifying two views
on multiple mean-payoff objectives in Markov decision processes. Logical Methods
in Computer Science. International Federation for Computational Logic. https://doi.org/10.23638/LMCS-13(2:15)2017
chicago: Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical
Methods in Computer Science. International Federation for Computational Logic,
2017. https://doi.org/10.23638/LMCS-13(2:15)2017.
ieee: K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple
mean-payoff objectives in Markov decision processes,” Logical Methods in Computer
Science, vol. 13, no. 2. International Federation for Computational Logic,
2017.
ista: Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple
mean-payoff objectives in Markov decision processes. Logical Methods in Computer
Science. 13(2), 15.
mla: Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes.” Logical Methods in Computer Science,
vol. 13, no. 2, 15, International Federation for Computational Logic, 2017, doi:10.23638/LMCS-13(2:15)2017.
short: K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science
13 (2017).
corr_author: '1'
das_tickbox: '1'
date_created: 2018-12-11T11:46:38Z
date_published: 2017-07-03T00:00:00Z
date_updated: 2026-07-06T13:26:27Z
day: '03'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.23638/LMCS-13(2:15)2017
ec_funded: 1
external_id:
isi:
- '000419160800002'
file:
- access_level: open_access
checksum: bfa405385ec6229ad5ead89ab5751639
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:32Z
date_updated: 2020-07-14T12:46:33Z
file_id: '5354'
file_name: IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf
file_size: 511832
relation: main_file
file_date_updated: 2020-07-14T12:46:33Z
has_accepted_license: '1'
intvolume: ' 13'
isi: 1
issue: '2'
language:
- iso: eng
month: '07'
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
- _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: 2590DB08-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '701309'
name: Atomic Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes
publication: Logical Methods in Computer Science
publication_identifier:
issn:
- 1860-5974
publication_status: published
publisher: International Federation for Computational Logic
publist_id: '7355'
pubrep_id: '957'
quality_controlled: '1'
related_material:
record:
- id: '5429'
relation: earlier_version
status: public
- id: '5435'
relation: earlier_version
status: public
- id: '1657'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Unifying two views on multiple mean-payoff objectives in Markov decision processes
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2017'
...
---
_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: 2026-04-15T10:02:12Z
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: Formal methods for the design and analysis of complex systems
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: '1234'
abstract:
- lang: eng
text: We present a new algorithm for the statistical model checking of Markov chains
with respect to unbounded temporal properties, including full linear temporal
logic. The main idea is that we monitor each simulation run on the fly, in order
to detect quickly if a bottom strongly connected component is entered with high
probability, in which case the simulation run can be terminated early. As a result,
our simulation runs are often much shorter than required by termination bounds
that are computed a priori for a desired level of confidence on a large state
space. In comparison to previous algorithms for statistical model checking our
method is not only faster in many cases but also requires less information about
the system, namely, only the minimum transition probability that occurs in the
Markov chain. In addition, our method can be generalised to unbounded quantitative
properties such as mean-payoff bounds.
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under\r\ngrant agreement 267989 (QUAREM), the Austrian Science Fund
\ (FWF) under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award),
the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh
Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility
Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation
under grant agreement P202/12/G061."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
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. Faster statistical model checking
for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:10.1007/978-3-662-49674-9_7'
apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Faster
statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129).
Presented at the TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, Eindhoven, The Netherlands: Springer. https://doi.org/10.1007/978-3-662-49674-9_7'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29.
Springer, 2016. https://doi.org/10.1007/978-3-662-49674-9_7.
ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
model checking for unbounded temporal properties,” presented at the TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands,
2016, vol. 9636, pp. 112–129.'
ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model
checking for unbounded temporal properties. TACAS: Tools and Algorithms for the
Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.'
mla: Daca, Przemyslaw, et al. Faster Statistical Model Checking for Unbounded
Temporal Properties. Vol. 9636, Springer, 2016, pp. 112–29, doi:10.1007/978-3-662-49674-9_7.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp.
112–129.
conference:
end_date: 2016-04-08
location: Eindhoven, The Netherlands
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2016-04-02
date_created: 2018-12-11T11:50:51Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1007/978-3-662-49674-9_7
ec_funded: 1
external_id:
arxiv:
- '1504.05739'
isi:
- '000406428000007'
intvolume: ' 9636'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.05739
month: '01'
oa: 1
oa_version: Preprint
page: 112 - 129
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: Formal methods for the design and analysis of complex systems
- _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: '6099'
quality_controlled: '1'
related_material:
record:
- id: '471'
relation: later_version
status: public
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Faster statistical model checking for unbounded temporal properties
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9636
year: '2016'
...
---
_id: '1499'
abstract:
- lang: eng
text: "We consider weighted automata with both positive and negative integer weights
on edges and\r\nstudy the problem of synchronization using adaptive strategies
that may only observe whether\r\nthe current weight-level is negative or nonnegative.
We show that the synchronization problem is decidable in polynomial time for deterministic
weighted automata."
acknowledgement: "The research leading to these results has received funding from
the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement
601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center
IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM),
the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein
Award), the Czech Science Foundation under grant agreement P202/12/G061, and People
Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme
(FP7/2007-2013) REA Grant No 291734."
alternative_title:
- LIPIcs
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Kim
full_name: Larsen, Kim
last_name: Larsen
- first_name: Simon
full_name: Laursen, Simon
last_name: Laursen
- first_name: Jiří
full_name: Srba, Jiří
last_name: Srba
citation:
ama: 'Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of
weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2015:142-154. doi:10.4230/LIPIcs.CONCUR.2015.142'
apa: 'Kretinsky, J., Larsen, K., Laursen, S., & Srba, J. (2015). Polynomial
time decidability of weighted synchronization under partial observability (Vol.
42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142'
chicago: Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time
Decidability of Weighted Synchronization under Partial Observability,” 42:142–54.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142.
ieee: 'J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability
of weighted synchronization under partial observability,” presented at the CONCUR:
Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.'
ista: 'Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability
of weighted synchronization under partial observability. CONCUR: Concurrency Theory,
LIPIcs, vol. 42, 142–154.'
mla: Kretinsky, Jan, et al. Polynomial Time Decidability of Weighted Synchronization
under Partial Observability. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2015, pp. 142–54, doi:10.4230/LIPIcs.CONCUR.2015.142.
short: J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2015, pp. 142–154.
conference:
end_date: 2015-09-04
location: Madrid, Spain
name: 'CONCUR: Concurrency Theory'
start_date: 2015-09-01
date_created: 2018-12-11T11:52:22Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2025-04-15T06:26:02Z
day: '01'
ddc:
- '000'
- '003'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2015.142
ec_funded: 1
file:
- access_level: open_access
checksum: 49eb5021caafaabe5356c65b9c5f8c9c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:12Z
date_updated: 2020-07-14T12:44:58Z
file_id: '4672'
file_name: IST-2016-498-v1+1_32.pdf
file_size: 623563
relation: main_file
file_date_updated: 2020-07-14T12:44:58Z
has_accepted_license: '1'
intvolume: ' 42'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 142 - 154
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5680'
pubrep_id: '498'
quality_controlled: '1'
scopus_import: 1
status: public
title: Polynomial time decidability of weighted synchronization under partial observability
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 42
year: '2015'
...
---
_id: '1502'
abstract:
- lang: eng
text: We extend the theory of input-output conformance with operators for merge
and quotient. The former is useful when testing against multiple requirements
or views. The latter can be used to generate tests for patches of an already tested
system. Both operators can combine systems with different action alphabets, which
is usually the case when constructing complex systems and specifications from
parts, for instance different views as well as newly defined functionality of
a~previous version of the system.
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 (Wittgestein Award), by People Programme
(Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013)
under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373
(nSafeCer). Jan Křetínský has been partially supported by the Czech Science Foundation,
grant No. P202/12/G061. Nikola Beneš has been supported by the\r\nMEYS project
No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for
Scientific Excellence."
alternative_title:
- 'Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based
Software Engineering '
article_processing_charge: No
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- 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: Dejan
full_name: Nickovic, Dejan
last_name: Nickovic
citation:
ama: 'Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition
operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:10.1145/2737166.2737175'
apa: 'Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., & Nickovic, D. (2015).
Complete composition operators for IOCO-testing theory (pp. 101–110). Presented
at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM.
https://doi.org/10.1145/2737166.2737175'
chicago: Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and
Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10.
ACM, 2015. https://doi.org/10.1145/2737166.2737175.
ieee: 'N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete
composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based
Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.'
ista: 'Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition
operators for IOCO-testing theory. CBSE: Component-Based Software Engineering
, Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based
Software Engineering , , 101–110.'
mla: Beneš, Nikola, et al. Complete Composition Operators for IOCO-Testing Theory.
ACM, 2015, pp. 101–10, doi:10.1145/2737166.2737175.
short: N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015,
pp. 101–110.
conference:
end_date: 2015-05-08
location: Montreal, QC, Canada
name: 'CBSE: Component-Based Software Engineering '
start_date: 2015-05-04
date_created: 2018-12-11T11:52:24Z
date_published: 2015-05-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2737166.2737175
ec_funded: 1
external_id:
isi:
- '000380554800013'
file:
- access_level: open_access
checksum: c6ce681035c163a158751f240cb7d389
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:46Z
date_updated: 2020-07-14T12:44:59Z
file_id: '5303'
file_name: IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf
file_size: 467561
relation: main_file
file_date_updated: 2020-07-14T12:44:59Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
page: 101 - 110
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: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_identifier:
isbn:
- 978-1-4503-3471-6
publication_status: published
publisher: ACM
publist_id: '5676'
pubrep_id: '625'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Complete composition operators for IOCO-testing theory
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2015'
...
---
_id: '1594'
abstract:
- lang: eng
text: Quantitative extensions of temporal logics have recently attracted significant
attention. In this work, we study frequency LTL (fLTL), an extension of LTL which
allows to speak about frequencies of events along an execution. Such an extension
is particularly useful for probabilistic systems that often cannot fulfil strict
qualitative guarantees on the behaviour. It has been recently shown that controller
synthesis for Markov decision processes and fLTL is decidable when all the bounds
on frequencies are 1. As a step towards a complete quantitative solution, we show
that the problem is decidable for the fragment fLTL\GU, where U does not occur
in the scope of G (but still F can). Our solution is based on a novel translation
of such quantitative formulae into equivalent deterministic automata.
acknowledgement: "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 Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework
Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the
CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative
Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie
Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013)
REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE),
and by the ERC Start Grant (279307: Graph Games).\r\n"
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Jan
full_name: Krčál, Jan
last_name: Krčál
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: 'Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency
LTL\GU. In: Vol 9450. Springer; 2015:162-177. doi:10.1007/978-3-662-48899-7_12'
apa: 'Forejt, V., Krčál, J., & Kretinsky, J. (2015). Controller synthesis for
MDPs and frequency LTL\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic
for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer.
https://doi.org/10.1007/978-3-662-48899-7_12'
chicago: Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for
MDPs and Frequency LTL\GU,” 9450:162–77. Springer, 2015. https://doi.org/10.1007/978-3-662-48899-7_12.
ieee: 'V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and
frequency LTL\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence,
and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.'
ista: 'Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency
LTL\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS,
vol. 9450, 162–177.'
mla: Forejt, Vojtěch, et al. Controller Synthesis for MDPs and Frequency LTL\GU.
Vol. 9450, Springer, 2015, pp. 162–77, doi:10.1007/978-3-662-48899-7_12.
short: V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.
conference:
end_date: 2015-11-28
location: Suva, Fiji
name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
start_date: 2015-11-24
date_created: 2018-12-11T11:52:55Z
date_published: 2015-11-22T00:00:00Z
date_updated: 2025-09-23T08:21:59Z
day: '22'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-662-48899-7_12
ec_funded: 1
external_id:
isi:
- '000375574900012'
intvolume: ' 9450'
isi: 1
language:
- iso: eng
month: '11'
oa_version: None
page: 162 - 177
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _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: Springer
publist_id: '5577'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Controller synthesis for MDPs and frequency LTL\GU
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9450
year: '2015'
...
---
_id: '1601'
abstract:
- lang: eng
text: We propose a flexible exchange format for ω-automata, as typically used in
formal verification, and implement support for it in a range of established tools.
Our aim is to simplify the interaction of tools, helping the research community
to build upon other people’s work. A key feature of the format is the use of very
generic acceptance conditions, specified by Boolean combinations of acceptance
primitives, rather than being limited to common cases such as Büchi, Streett,
or Rabin. Such flexibility in the choice of acceptance conditions can be exploited
in applications, for example in probabilistic model checking, and furthermore
encourages the development of acceptance-agnostic tools for automata manipulations.
The format allows acceptance conditions that are either state-based or transition-based,
and also supports alternating automata.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Tomáš
full_name: Babiak, Tomáš
last_name: Babiak
- first_name: František
full_name: Blahoudek, František
last_name: Blahoudek
- first_name: Alexandre
full_name: Duret Lutz, Alexandre
last_name: Duret Lutz
- first_name: Joachim
full_name: Klein, Joachim
last_name: Klein
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Daniel
full_name: Mueller, Daniel
last_name: Mueller
- first_name: David
full_name: Parker, David
last_name: Parker
- first_name: Jan
full_name: Strejček, Jan
last_name: Strejček
citation:
ama: 'Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format.
In: Vol 9206. Springer; 2015:479-486. doi:10.1007/978-3-319-21690-4_31'
apa: 'Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller,
D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486).
Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States:
Springer. https://doi.org/10.1007/978-3-319-21690-4_31'
chicago: Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein,
Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata
Format,” 9206:479–86. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_31.
ieee: 'T. Babiak et al., “The Hanoi omega-automata format,” presented at
the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015,
vol. 9206, pp. 479–486.'
ista: 'Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker
D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification,
LNCS, vol. 9206, 479–486.'
mla: Babiak, Tomáš, et al. The Hanoi Omega-Automata Format. Vol. 9206, Springer,
2015, pp. 479–86, doi:10.1007/978-3-319-21690-4_31.
short: T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller,
D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486.
conference:
end_date: 2015-07-24
location: San Francisco, CA, United States
name: 'CAV: Computer Aided Verification'
start_date: 2015-07-18
date_created: 2018-12-11T11:52:57Z
date_published: 2015-07-16T00:00:00Z
date_updated: 2025-09-23T13:50:55Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-319-21690-4_31
ec_funded: 1
external_id:
isi:
- '000364182900031'
file:
- access_level: open_access
checksum: 5885236fa88a439baba9ac6f3e801e93
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:38:12Z
date_updated: 2020-07-14T12:45:04Z
file_id: '7850'
file_name: 2015_CAV_Babiak.pdf
file_size: 1651779
relation: main_file
file_date_updated: 2020-07-14T12:45:04Z
has_accepted_license: '1'
intvolume: ' 9206'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 479 - 486
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _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: '5566'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The Hanoi omega-automata format
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9206
year: '2015'
...