23 Publications

Mark all

[23]
2018 | Conference Paper | IST-REx-ID: 297 | OA
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.
View | Files available | DOI
 
[22]
2017 | Journal Article | IST-REx-ID: 466 | OA
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.
View | Files available | DOI
 
[21]
2017 | Journal Article | IST-REx-ID: 471 | OA
Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic (TOCL). 18(2), 12.
View | Files available | DOI | Download Submitted Version (ext.)
 
[20]
2017 | Conference Paper | IST-REx-ID: 645 | OA
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.
View | DOI | Download Submitted Version (ext.)
 
[19]
2017 | Journal Article | IST-REx-ID: 1407 | OA
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.
View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[18]
2016 | Conference Paper | IST-REx-ID: 1093 | OA
Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.
View | Files available | DOI
 
[17]
2016 | Conference Paper | IST-REx-ID: 1234 | OA
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.
View | Files available | DOI | Download Preprint (ext.)
 
[16]
2015 | Conference Paper | IST-REx-ID: 1689 | OA
Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 259–268.
View | Files available | DOI | Download Preprint (ext.)
 
[15]
2015 | Journal Article | IST-REx-ID: 1846 | OA
Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.
View | Files available | DOI
 
[14]
2015 | Conference Paper | IST-REx-ID: 1882 | OA
Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for quantitative specifications. FACS: Formal Aspects of Component Software, LNCS, vol. 8997, 306–324.
View | DOI | Download Preprint (ext.)
 
[13]
2015 | Technical Report | IST-REx-ID: 5429 | OA
Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 41p.
View | Files available | DOI
 
[12]
2015 | Technical Report | IST-REx-ID: 5435 | OA
Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 51p.
View | Files available | DOI
 
[11]
2015 | Conference Paper | IST-REx-ID: 1499 | OA
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.
View | Files available | DOI
 
[10]
2015 | Conference Paper | IST-REx-ID: 1502 | OA
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.
View | Files available | DOI
 
[9]
2015 | Conference Paper | IST-REx-ID: 1594
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.
View | DOI
 
[8]
2015 | Conference Paper | IST-REx-ID: 1601 | OA
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.
View | Files available | DOI
 
[7]
2015 | Conference Paper | IST-REx-ID: 1603 | OA
Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.
View | Files available | DOI | Download Preprint (ext.)
 
[6]
2015 | Conference Paper | IST-REx-ID: 1657
Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256.
View | Files available | DOI
 
[5]
2014 | Conference Paper | IST-REx-ID: 2026
Komárková Z, Kretinsky J. 2014. Rabinizer 3: Safraless translation of ltl to small deterministic automata. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 235–241.
View | DOI
 
[4]
2014 | Conference Paper | IST-REx-ID: 2027 | OA
Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Parker D, Ujma M. 2014. Verification of markov decision processes using learning algorithms. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ALENEX: Algorithm Engineering and Experiments, LNCS, vol. 8837, 98–114.
View | DOI | Download Submitted Version (ext.)
 
[3]
2014 | Conference Paper | IST-REx-ID: 2053 | OA
Hermanns H, Krčál J, Kretinsky J. 2014. Probabilistic bisimulation: Naturally on distributions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 249–265.
View | DOI | Download Submitted Version (ext.)
 
[2]
2014 | Conference Paper | IST-REx-ID: 2190 | OA
Esparza J, Kretinsky J. 2014. From LTL to deterministic automata: A safraless compositional approach. CAV: Computer Aided Verification, LNCS, vol. 8559, 192–208.
View | DOI | Download Submitted Version (ext.)
 
[1]
2013 | Conference Paper | IST-REx-ID: 2446 | OA
Chatterjee K, Gaiser A, Kretinsky J. 2013. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 8044, 559–575.
View | DOI | Download Preprint (ext.) | arXiv
 

Search

Filter Publications

23 Publications

Mark all

[23]
2018 | Conference Paper | IST-REx-ID: 297 | OA
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.
View | Files available | DOI
 
[22]
2017 | Journal Article | IST-REx-ID: 466 | OA
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.
View | Files available | DOI
 
[21]
2017 | Journal Article | IST-REx-ID: 471 | OA
Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic (TOCL). 18(2), 12.
View | Files available | DOI | Download Submitted Version (ext.)
 
[20]
2017 | Conference Paper | IST-REx-ID: 645 | OA
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.
View | DOI | Download Submitted Version (ext.)
 
[19]
2017 | Journal Article | IST-REx-ID: 1407 | OA
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.
View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[18]
2016 | Conference Paper | IST-REx-ID: 1093 | OA
Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.
View | Files available | DOI
 
[17]
2016 | Conference Paper | IST-REx-ID: 1234 | OA
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.
View | Files available | DOI | Download Preprint (ext.)
 
[16]
2015 | Conference Paper | IST-REx-ID: 1689 | OA
Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 259–268.
View | Files available | DOI | Download Preprint (ext.)
 
[15]
2015 | Journal Article | IST-REx-ID: 1846 | OA
Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.
View | Files available | DOI
 
[14]
2015 | Conference Paper | IST-REx-ID: 1882 | OA
Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for quantitative specifications. FACS: Formal Aspects of Component Software, LNCS, vol. 8997, 306–324.
View | DOI | Download Preprint (ext.)
 
[13]
2015 | Technical Report | IST-REx-ID: 5429 | OA
Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 41p.
View | Files available | DOI
 
[12]
2015 | Technical Report | IST-REx-ID: 5435 | OA
Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 51p.
View | Files available | DOI
 
[11]
2015 | Conference Paper | IST-REx-ID: 1499 | OA
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.
View | Files available | DOI
 
[10]
2015 | Conference Paper | IST-REx-ID: 1502 | OA
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.
View | Files available | DOI
 
[9]
2015 | Conference Paper | IST-REx-ID: 1594
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.
View | DOI
 
[8]
2015 | Conference Paper | IST-REx-ID: 1601 | OA
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.
View | Files available | DOI
 
[7]
2015 | Conference Paper | IST-REx-ID: 1603 | OA
Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.
View | Files available | DOI | Download Preprint (ext.)
 
[6]
2015 | Conference Paper | IST-REx-ID: 1657
Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256.
View | Files available | DOI
 
[5]
2014 | Conference Paper | IST-REx-ID: 2026
Komárková Z, Kretinsky J. 2014. Rabinizer 3: Safraless translation of ltl to small deterministic automata. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 235–241.
View | DOI
 
[4]
2014 | Conference Paper | IST-REx-ID: 2027 | OA
Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Parker D, Ujma M. 2014. Verification of markov decision processes using learning algorithms. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ALENEX: Algorithm Engineering and Experiments, LNCS, vol. 8837, 98–114.
View | DOI | Download Submitted Version (ext.)
 
[3]
2014 | Conference Paper | IST-REx-ID: 2053 | OA
Hermanns H, Krčál J, Kretinsky J. 2014. Probabilistic bisimulation: Naturally on distributions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 249–265.
View | DOI | Download Submitted Version (ext.)
 
[2]
2014 | Conference Paper | IST-REx-ID: 2190 | OA
Esparza J, Kretinsky J. 2014. From LTL to deterministic automata: A safraless compositional approach. CAV: Computer Aided Verification, LNCS, vol. 8559, 192–208.
View | DOI | Download Submitted Version (ext.)
 
[1]
2013 | Conference Paper | IST-REx-ID: 2446 | OA
Chatterjee K, Gaiser A, Kretinsky J. 2013. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 8044, 559–575.
View | DOI | Download Preprint (ext.) | arXiv
 

Search

Filter Publications