I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
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.
Info
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.
Info
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.
Info
Jan Kretinsky and Salomon Sickert. On refinements of Boolean and parametric modal transition systems. In Liu et al., pages 213–230.
Info
Jan Kretinsky and Salomon Sickert. On refinements of Boolean and parametric modal transition systems. Technical Report abs/1304.5278, arXiv.org, 2013.
Info
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.
Info
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.
Info
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.
Info
Holger Hermanns, Jan Krcal, and Jan Kretinsky. Compositional verification and optimization of interactive Markov chains. In D'Argenio and Melgratti, pages 364–379.
Info
Holger Hermanns, Jan Krcal, and Jan Kretinsky. Compositional verification and optimization of interactive Markov chains. Technical Report abs/1305.7332, arXiv.org, 2013.
Info
Jan Kretinsky and Salomon Sickert. MoTraS: A tool for modal transition systems and their extensions. In Hung and Ogawa, pages 487–491.
Info
Jan Kretinsky and Ruslan Ledesma-Garza. Rabinizer 2: Small deterministic automata for LTLGU. In Hung and Ogawa, pages 446–450.
Info

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.
Info
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.
Info
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. In Madhusudan and Seshia, pages 7–22.
Info
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. Technical Report abs/1106.1424, arXiv.org, 2012.
Info
Nikola Benes and Jan Kretinsky. Modal process rewrite systems. In Roychoudhury and D'Souza, pages 120–135.
Info
Nikola Benes and Jan Kretinsky. Modal process rewrite systems. Technical report FIMU-RS-2012-02, Faculty of Informatics, Masaryk University, Brno, 2012.
Info
Andreas Gaiser, Jan Kretinsky, and Javier Esparza. Rabinizer: Small deterministic automata for LTL(F, G). In Chakraborty and Mukund, pages 72–76.
Info
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.
Info
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.
Info
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.
Info

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.
Info
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.
Info
Jan Kretinsky. Probabilistic timed systems with non-determinism. PhD Thesis proposal, Masaryk University, Brno, Dept. of Computer Science, 2011.
Info
Tomas Brazdil, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Fixed-delay events in generalized semi-markov processes revisited. In CONCUR, pages 140–155, 2011.
Info
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.
Info
Nikola Benes, Ivana Cerna, and Jan Kretinsky. Modal transition systems: Composition and LTL model checking. In Bultan and Hsiung, pages 228–242.
Info
Nikola Benes, Jan Kretinsky, Kim G. Larsen, Mikael H. Moller, and Jiri Srba. Parametric modal transition systems. In Bultan and Hsiung, pages 275–289.
Info
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.
Info

2010

Jan Kretinsky. Modal transition systems. Master's thesis, Masaryk University, Brno, Dept. of Mathematics, 2010.
Info
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.
Info
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.
Info
Nikola Benes and Jan Kretinsky. Process algebra for modal transition systemses. In MEMICS, pages 9–18, 2010.
Info
Nikola Benes and Jan Kretinsky. Process algebra for modal transition systemses. Technical report FIMU-RS-2010-11, Faculty of Informatics, Masaryk University, Brno, 2010.
Info
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.
Info

2009

Jan Kretinsky. Fundamental properties of probabilistic branching-time logics. Master's thesis, Masaryk University, Brno, Dept. of Computer Science, 2009.
Info
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.
Info
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.
Info
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, and Jiri Srba. On determinism in modal transition systems. Theor. Comput. Sci., 410(41):4026–4043, 2009.
Info
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.
Info
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.
Info

2008

Tomas Brazdil, Vojtech Forejt, Jan Kretinsky, and Antonin Kucera. The satisfiability problem for probabilistic CTL. In LICS, pages 391–402, 2008.
Info
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.
Info