Guessing winning policies in LTL synthesis by semantic learning
J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414.
LibreCat: https://research-explorer.ista.ac.at/record/14259
DOI: 10.1007/978-3-031-37706-8_20

Stopping criteria for value iteration on stochastic games with quantitative objectives
J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2023.
LibreCat: https://research-explorer.ista.ac.at/record/13967
DOI: 10.1109/LICS56636.2023.10175771
WoS: 001036707700042
arXiv: 2304.09930

Index appearance record with preorders
J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618.
LibreCat: https://research-explorer.ista.ac.at/record/10602
DOI: 10.1007/s00236-021-00412-y
WoS: 000735765500001

Anytime guarantees for reachability in uncountable Markov decision processes
K. Grover, J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 33rd International Conference on Concurrency Theory , Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
LibreCat: https://research-explorer.ista.ac.at/record/12775
DOI: 10.4230/LIPIcs.CONCUR.2022.11
arXiv: 2008.04824

Strategy representation by decision trees in reactive synthesis
T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp. 385–407.
LibreCat: https://research-explorer.ista.ac.at/record/297
DOI: 10.1007/978-3-319-89960-2_21
WoS: 000546326300021

Faster statistical model checking for unbounded temporal properties
P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic (TOCL) 18 (2017).
LibreCat: https://research-explorer.ista.ac.at/record/471
DOI: 10.1145/3060139

Unifying two views on multiple mean-payoff objectives in Markov decision processes
K. Chatterjee, Z. Ketínská, J. Kretinsky, Logical Methods in Computer Science 13 (2017).
LibreCat: https://research-explorer.ista.ac.at/record/466
DOI: 10.23638/LMCS-13(2:15)2017

Value iteration for long run average reward in markov decision processes
P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R. Majumdar, V. Kundak (Eds.), Springer, 2017, pp. 201–221.
LibreCat: https://research-explorer.ista.ac.at/record/645
DOI: 10.1007/978-3-319-63387-9_10

Index appearance record for transforming Rabin automata into parity automata
J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460.
LibreCat: https://research-explorer.ista.ac.at/record/13160
DOI: 10.1007/978-3-662-54577-5_26
arXiv: 1701.05738

Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
M. Svoreová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cbrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.
LibreCat: https://research-explorer.ista.ac.at/record/1407
DOI: 10.1016/j.nahs.2016.04.006
WoS: 000390637000014
arXiv: 1410.5387

Linear distances between Markov chains
P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
LibreCat: https://research-explorer.ista.ac.at/record/1093
DOI: 10.4230/LIPIcs.CONCUR.2016.20

Faster statistical model checking for unbounded temporal properties
P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp. 112–129.
LibreCat: https://research-explorer.ista.ac.at/record/1234
DOI: 10.1007/978-3-662-49674-9_7

Polynomial time decidability of weighted synchronization under partial observability
J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–154.
LibreCat: https://research-explorer.ista.ac.at/record/1499
DOI: 10.4230/LIPIcs.CONCUR.2015.142

Controller synthesis for MDPs and frequency LTL\'47U
V. Forejt, J. Krdál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.
LibreCat: https://research-explorer.ista.ac.at/record/1594
DOI: 10.1007/978-3-662-48899-7_12

The Hanoi omega-automata format
T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller, D. Parker, J. Strejdek, in:, Springer, 2015, pp. 479–486.
LibreCat: https://research-explorer.ista.ac.at/record/1601
DOI: 10.1007/978-3-319-21690-4_31

Refinement checking on parametric modal transition systems
N. Benes, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297.
LibreCat: https://research-explorer.ista.ac.at/record/1846
DOI: 10.1007/s00236-015-0215-4

Compositionality for quantitative specifications
U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015, pp. 306–324.
LibreCat: https://research-explorer.ista.ac.at/record/1882
DOI: 10.1007/978-3-319-15317-9_19

Unifying two views on multiple mean-payoff objectives in Markov decision processes
K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.
LibreCat: https://research-explorer.ista.ac.at/record/1657
DOI: 10.1109/LICS.2015.32

Unifying two views on multiple mean-payoff objectives in Markov decision processes
K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015.
LibreCat: https://research-explorer.ista.ac.at/record/5429
DOI: 10.15479/AT:IST-2015-318-v1-1

Unifying two views on multiple mean-payoff objectives in Markov decision processes
K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015.
LibreCat: https://research-explorer.ista.ac.at/record/5435
DOI: 10.15479/AT:IST-2015-318-v2-1