|
|
 |
|
 |
|
Publications by Jan Kretinsky
|
|
 |
|
 |
2013 | |
Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-time stochastic games with time-bounded reachability. Inf. Comput., 224:46–70, 2013. |
|
|
Krishnendu Chatterjee, Andreas Gaiser, and Jan Kretinsky. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In Sharygina and Veith, pages 559–575. |
|
|
Krishnendu Chatterjee, Andreas Gaiser, and Jan Kretinsky. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. Technical Report abs/1304.5281, arXiv.org, 2013. |
|
|
Jan Kretinsky and Salomon Sickert. On refinements of Boolean and parametric modal transition systems. In Liu et al., pages 213–230. |
|
|
Jan Kretinsky and Salomon Sickert. On refinements of Boolean and parametric modal transition systems. Technical Report abs/1304.5278, arXiv.org, 2013. |
|
|
Tomas Brazdil, Lubos Korenciak, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. On time-average limits in deterministic and stochastic Petri nets. In Seelam et al., pages 421–422. |
|
|
Nikola Benes, Benoit Delahaye, Uli Fahrenberg, Jan Kretinsky, and Axel Legay. Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory. In D'Argenio and Melgratti, pages 76–90. |
|
|
Nikola Benes, Benoit Delahaye, Uli Fahrenberg, Jan Kretinsky, and Axel Legay. Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory. Technical Report abs/1306.0741, arXiv.org, 2013. |
|
|
Holger Hermanns, Jan Krcal, and Jan Kretinsky. Compositional verification and optimization of interactive Markov chains. In D'Argenio and Melgratti, pages 364–379. |
|
|
Holger Hermanns, Jan Krcal, and Jan Kretinsky. Compositional verification and optimization of interactive Markov chains. Technical Report abs/1305.7332, arXiv.org, 2013. |
|
|
Jan Kretinsky and Salomon Sickert. MoTraS: A tool for modal transition systems and their extensions. In Hung and Ogawa, pages 487–491. |
|
Jan Kretinsky and Ruslan Ledesma-Garza. Rabinizer 2: Small deterministic automata for LTL GU. In Hung and Ogawa, pages 446–450. |
|
2012 | |
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, Mikael H. Moller, and Jiri Srba. Dual-priced modal transition systems with time durations. In Bjørner and Voronkov, pages 122–137. |
|
|
Nikola Benes, Jan Kretinsky, Kim G. Larsen, Mikael H. Moller, and Jiri Srba. Dual-priced modal transition systems with time durations. Technical report FIMU-RS-2012-01, Faculty of Informatics, Masaryk University, Brno, 2012. |
|
|
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. In Madhusudan and Seshia, pages 7–22. |
|
|
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. Technical Report abs/1106.1424, arXiv.org, 2012. |
|
|
Nikola Benes and Jan Kretinsky. Modal process rewrite systems. In Roychoudhury and D'Souza, pages 120–135. |
|
|
Nikola Benes and Jan Kretinsky. Modal process rewrite systems. Technical report FIMU-RS-2012-02, Faculty of Informatics, Masaryk University, Brno, 2012. |
|
|
Andreas Gaiser, Jan Kretinsky, and Javier Esparza. Rabinizer: Small deterministic automata for LTL(F, G). In Chakraborty and Mukund, pages 72–76. |
|
|
Nikola Benes, Jan Kretinsky, Kim G. Larsen, and Jiri Srba. Exptime-completeness of thorough refinement on modal transition systems. Inf. Comput., 218:54–68, 2012. |
|
|
Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Verification of open interactive markov chains. In D'Souza et al., pages 474–485. |
|
|
Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Verification of open interactive markov chains. Technical report FIMU-RS-2012-04, Faculty of Informatics, Masaryk University, Brno, 2012. |
|
2011 | |
Tomas Brazdil, Jan Krcal, Jan Kretinsky, Antonin Kucera, and Vojtech Rehak. Measuring performance of continuous-time stochastic processes using timed automata. In Caccamo et al., pages 33–42. |
|
|
Tomas Brazdil, Jan Krcal, Jan Kretinsky, Antonin Kucera, and Vojtech Rehak. Measuring performance of continuous-time stochastic processes using timed automata. Technical Report abs/1101.4204, arXiv.org, 2011. |
|
|
Jan Kretinsky. Probabilistic timed systems with non-determinism. PhD Thesis proposal, Masaryk University, Brno, Dept. of Computer Science, 2011. |
|
|
Tomas Brazdil, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Fixed-delay events in generalized semi-markov processes revisited. In CONCUR, pages 140–155, 2011. |
|
|
Tomas Brazdil, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Fixed-delay events in generalized semi-markov processes revisited. Technical Report abs/1106.1424, arXiv.org, 2011. |
|
|
Nikola Benes, Ivana Cerna, and Jan Kretinsky. Modal transition systems: Composition and LTL model checking. In Bultan and Hsiung, pages 228–242. |
|
|
Nikola Benes, Jan Kretinsky, Kim G. Larsen, Mikael H. Moller, and Jiri Srba. Parametric modal transition systems. In Bultan and Hsiung, pages 275–289. |
|
|
Nikola Benes, Jan Kretinsky, Kim G. Larsen, Mikael H. Moller, and Jiri Srba. Parametric modal transition systems. Technical report FIMU-RS-2011-03, Faculty of Informatics, Masaryk University, Brno, 2011. |
|
2010 | |
Jan Kretinsky. Modal transition systems. Master's thesis, Masaryk University, Brno, Dept. of Mathematics, 2010. |
|
|
Tomas Brazdil, Jan Krcal, Jan Kretinsky, Antonin Kucera, and Vojtech Rehak. Stochastic real-time games with qualitative timed automata objectives. In CONCUR, pages 207–221, 2010. |
|
|
Tomas Brazdil, Jan Krcal, Jan Kretinsky, Antonin Kucera, and Vojtech Rehak. Stochastic real-time games with qualitative timed automata objectives. Technical report FIMU-RS-2010-05, Faculty of Informatics, Masaryk University, Brno, 2010. |
|
|
Nikola Benes and Jan Kretinsky. Process algebra for modal transition systemses. In MEMICS, pages 9–18, 2010. |
|
|
Nikola Benes and Jan Kretinsky. Process algebra for modal transition systemses. Technical report FIMU-RS-2010-11, Faculty of Informatics, Masaryk University, Brno, 2010. |
|
|
Nikola Benes, Ivana Cerna, and Jan Kretinsky. Disjunctive modal transition systems and generalized LTL model checking. Technical report FIMU-RS-2010-12, Faculty of Informatics, Masaryk University, Brno, 2010. |
|
2009 | |
Jan Kretinsky. Fundamental properties of probabilistic branching-time logics. Master's thesis, Masaryk University, Brno, Dept. of Computer Science, 2009. |
|
|
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, and Jiri Srba. Checking thorough refinement on modal transition systems is exptime-complete. In ICTAC, pages 112–126, 2009. |
|
|
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, and Jiri Srba. Checking thorough refinement on modal transition systems is exptime-complete. Technical report FIMU-RS-2009-03, Faculty of Informatics, Masaryk University, Brno, 2009. |
|
|
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, and Jiri Srba. On determinism in modal transition systems. Theor. Comput. Sci., 410(41):4026–4043, 2009. |
|
|
Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-time stochastic games with time-bounded reachability. In FSTTCS, pages 61–72, 2009. |
|
|
Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-time stochastic games with time-bounded reachability. Technical report FIMU-RS-2009-09, Faculty of Informatics, Masaryk University, Brno, 2009. |
|
2008 | |
Tomas Brazdil, Vojtech Forejt, Jan Kretinsky, and Antonin Kucera. The satisfiability problem for probabilistic CTL. In LICS, pages 391–402, 2008. |
|
|
Tomas Brazdil, Vojtech Forejt, Jan Kretinsky, and Antonin Kucera. The satisfiability problem for probabilistic CTL. Technical report FIMU-RS-2008-03, Faculty of Informatics, Masaryk University, Brno, 2008. |
|
|
|
Contact
