23 Publications

Mark all

[23]
2018 | Conference Paper | IST-REx-ID: 297 | OA
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.
View | Files available | DOI
 
[22]
2017 | Journal Article | IST-REx-ID: 466 | OA
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 of Computational Logic, 2017.
View | Files available | DOI
 
[21]
2017 | Journal Article | IST-REx-ID: 471 | OA
P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” ACM Transactions on Computational Logic (TOCL), vol. 18, no. 2. ACM, 2017.
View | Files available | DOI | Download Submitted Version (ext.)
 
[20]
2017 | Conference Paper | IST-REx-ID: 645 | OA
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.
View | DOI | Download Submitted Version (ext.)
 
[19]
2017 | Journal Article | IST-REx-ID: 1407 | OA
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.
View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[18]
2016 | Conference Paper | IST-REx-ID: 1093 | OA
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.
View | Files available | DOI
 
[17]
2016 | Conference Paper | IST-REx-ID: 1234 | OA
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.
View | Files available | DOI | Download Preprint (ext.)
 
[16]
2015 | Conference Paper | IST-REx-ID: 1689 | OA
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,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015, pp. 259–268.
View | Files available | DOI | Download Preprint (ext.)
 
[15]
2015 | Journal Article | IST-REx-ID: 1846 | OA
N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement checking on parametric modal transition systems,” Acta Informatica, vol. 52, no. 2–3. Springer, pp. 269–297, 2015.
View | Files available | DOI
 
[14]
2015 | Conference Paper | IST-REx-ID: 1882 | OA
U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality for quantitative specifications,” presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.
View | DOI | Download Preprint (ext.)
 
[13]
2015 | Technical Report | IST-REx-ID: 5429 | OA
K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria, 2015.
View | Files available | DOI
 
[12]
2015 | Technical Report | IST-REx-ID: 5435 | OA
K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria, 2015.
View | Files available | DOI
 
[11]
2015 | Conference Paper | IST-REx-ID: 1499 | OA
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.
View | Files available | DOI
 
[10]
2015 | Conference Paper | IST-REx-ID: 1502 | OA
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.
View | Files available | DOI
 
[9]
2015 | Conference Paper | IST-REx-ID: 1594
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.
View | DOI
 
[8]
2015 | Conference Paper | IST-REx-ID: 1601 | OA
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.
View | Files available | DOI
 
[7]
2015 | Conference Paper | IST-REx-ID: 1603 | OA
T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.
View | Files available | DOI | Download Preprint (ext.)
 
[6]
2015 | Conference Paper | IST-REx-ID: 1657
K. Chatterjee, Z. Komárková, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes.” IEEE, pp. 244–256, 2015.
View | Files available | DOI
 
[5]
2014 | Conference Paper | IST-REx-ID: 2026
Z. Komárková and J. Kretinsky, “Rabinizer 3: Safraless translation of ltl to small deterministic automata,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 235–241.
View | DOI
 
[4]
2014 | Conference Paper | IST-REx-ID: 2027 | OA
T. Brázdil et al., “Verification of markov decision processes using learning algorithms,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 98–114.
View | DOI | Download Submitted Version (ext.)
 
[3]
2014 | Conference Paper | IST-REx-ID: 2053 | OA
H. Hermanns, J. Krčál, and J. Kretinsky, “Probabilistic bisimulation: Naturally on distributions,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy, 2014, vol. 8704, pp. 249–265.
View | DOI | Download Submitted Version (ext.)
 
[2]
2014 | Conference Paper | IST-REx-ID: 2190 | OA
J. Esparza and J. Kretinsky, “From LTL to deterministic automata: A safraless compositional approach,” presented at the CAV: Computer Aided Verification, 2014, vol. 8559, pp. 192–208.
View | DOI | Download Submitted Version (ext.)
 
[1]
2013 | Conference Paper | IST-REx-ID: 2446 | OA
K. Chatterjee, A. Gaiser, and J. Kretinsky, “Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis,” vol. 8044. Springer, pp. 559–575, 2013.
View | DOI | Download Preprint (ext.) | arXiv
 

Search

Filter Publications

23 Publications

Mark all

[23]
2018 | Conference Paper | IST-REx-ID: 297 | OA
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.
View | Files available | DOI
 
[22]
2017 | Journal Article | IST-REx-ID: 466 | OA
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 of Computational Logic, 2017.
View | Files available | DOI
 
[21]
2017 | Journal Article | IST-REx-ID: 471 | OA
P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” ACM Transactions on Computational Logic (TOCL), vol. 18, no. 2. ACM, 2017.
View | Files available | DOI | Download Submitted Version (ext.)
 
[20]
2017 | Conference Paper | IST-REx-ID: 645 | OA
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.
View | DOI | Download Submitted Version (ext.)
 
[19]
2017 | Journal Article | IST-REx-ID: 1407 | OA
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.
View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[18]
2016 | Conference Paper | IST-REx-ID: 1093 | OA
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.
View | Files available | DOI
 
[17]
2016 | Conference Paper | IST-REx-ID: 1234 | OA
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.
View | Files available | DOI | Download Preprint (ext.)
 
[16]
2015 | Conference Paper | IST-REx-ID: 1689 | OA
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,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015, pp. 259–268.
View | Files available | DOI | Download Preprint (ext.)
 
[15]
2015 | Journal Article | IST-REx-ID: 1846 | OA
N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement checking on parametric modal transition systems,” Acta Informatica, vol. 52, no. 2–3. Springer, pp. 269–297, 2015.
View | Files available | DOI
 
[14]
2015 | Conference Paper | IST-REx-ID: 1882 | OA
U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality for quantitative specifications,” presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.
View | DOI | Download Preprint (ext.)
 
[13]
2015 | Technical Report | IST-REx-ID: 5429 | OA
K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria, 2015.
View | Files available | DOI
 
[12]
2015 | Technical Report | IST-REx-ID: 5435 | OA
K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria, 2015.
View | Files available | DOI
 
[11]
2015 | Conference Paper | IST-REx-ID: 1499 | OA
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.
View | Files available | DOI
 
[10]
2015 | Conference Paper | IST-REx-ID: 1502 | OA
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.
View | Files available | DOI
 
[9]
2015 | Conference Paper | IST-REx-ID: 1594
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.
View | DOI
 
[8]
2015 | Conference Paper | IST-REx-ID: 1601 | OA
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.
View | Files available | DOI
 
[7]
2015 | Conference Paper | IST-REx-ID: 1603 | OA
T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.
View | Files available | DOI | Download Preprint (ext.)
 
[6]
2015 | Conference Paper | IST-REx-ID: 1657
K. Chatterjee, Z. Komárková, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes.” IEEE, pp. 244–256, 2015.
View | Files available | DOI
 
[5]
2014 | Conference Paper | IST-REx-ID: 2026
Z. Komárková and J. Kretinsky, “Rabinizer 3: Safraless translation of ltl to small deterministic automata,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 235–241.
View | DOI
 
[4]
2014 | Conference Paper | IST-REx-ID: 2027 | OA
T. Brázdil et al., “Verification of markov decision processes using learning algorithms,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 98–114.
View | DOI | Download Submitted Version (ext.)
 
[3]
2014 | Conference Paper | IST-REx-ID: 2053 | OA
H. Hermanns, J. Krčál, and J. Kretinsky, “Probabilistic bisimulation: Naturally on distributions,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy, 2014, vol. 8704, pp. 249–265.
View | DOI | Download Submitted Version (ext.)
 
[2]
2014 | Conference Paper | IST-REx-ID: 2190 | OA
J. Esparza and J. Kretinsky, “From LTL to deterministic automata: A safraless compositional approach,” presented at the CAV: Computer Aided Verification, 2014, vol. 8559, pp. 192–208.
View | DOI | Download Submitted Version (ext.)
 
[1]
2013 | Conference Paper | IST-REx-ID: 2446 | OA
K. Chatterjee, A. Gaiser, and J. Kretinsky, “Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis,” vol. 8044. Springer, pp. 559–575, 2013.
View | DOI | Download Preprint (ext.) | arXiv
 

Search

Filter Publications