doc. RNDr. Vojtěch Řehák, Ph.D.


office: C436
Botanická 554/68a
602 00 Brno

Show on the map

phone: +420 549 49 4687
e‑mail:
CV

Curriculum vitae

Person Identification
  • Vojtěch Řehák, 1. 4. 1979, married
Workplace
  • April 2005 - now: Faculty of Informatics, Masaryk University
Employment Position
  • associate professor
Education and Academic Qualifications
  • 2019: doc. in Computer Science, FI MU Brno, "Stochastic Real-Time Systems: Parameter Synthesis and Games"
  • 2007: Ph.D. in Computer Science, FI MU Brno, "On Extensions of Process Rewrite Systems"
  • 2002: MSc (Mgr.) in Computer Science (5 Year Master Degree Programme), FI MU Brno, "Randomized Symbolic Model Checking"
  • 1997: high school diploma, mathematics class of Gym. tř. Kpt. Jaroše
Pedagogical Activities
  • 1999 - 2006 a 2009 - now: seminars on topics related to formal languages and automata theory
  • 2007 - 2011: leader of a seminar group of PV177 Laboratory of Advanced Network Technologies
  • 2010 - now: teaching DTEDI Thesis proposal, organization of DSOKL Měkké dovednosti
  • 2011 - now: two lectures of PA160 Net-Centric Computing II
  • 2013 - now: lectures and seminars of IV111 Probability in Computer Science
  • 2014 - now: koordination of seminar groups of IB002 Algorithms and data structures I
  • 2014 - now: leader of a seminar group of IV125 Formela lab seminar
  • 2016 - now: leader of a seminar group of IA169 System Verification and Assurance
Scientific and Research Activities
  • model checking, formal verification, automata and formal languages, models of infinite-state processes
  • network protocol description, message sequence charts, realizability, race conditions, formal verification
  • stochastic systems, generalized semi-Markov processes, parameter synthesis
  • patrolling games
Academical Stays
  • October - November 2006: Institute of Formal Methods in Computer Science, Universität Stuttgart, Germany
  • November 2003 - February 2004: Marie Curie Fellowship - Basic Research in Computer Science, Aarhus University
University Activities
Appreciation of Science Community
  • Dean's award for distinquished PhD thesis
Selected Publications
  • KLAŠKA, David, Antonín KUČERA, Tomáš LAMSER a Vojtěch ŘEHÁK. Automatic Synthesis of Efficient Regular Strategies in Adversarial Patrolling Games. In Proceedings of the 2018 International Conference on Autonomous Agents & Multiagent Systems. Richland, SC: International Foundation for Autonomous Agents and Multiagent Systems, 2018. s. 659-666, 8 s. ISBN 978-1-5108-6808-3. doi:10.5555/3237383.3237481. URL info
  • BRÁZDIL, Tomáš, Antonín KUČERA a Vojtěch ŘEHÁK. Solving Patrolling Problems in the Internet Environment. In Jerome Lang. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden. Neuveden: International Joint Conferences on Artificial Intelligence, 2018. s. 121-127, 7 s. ISBN 978-0-9992411-2-7. doi:10.24963/ijcai.2018/17. IJCAI.org info
  • BAIER, Christel, Clemens DUBSLAFF, Ľuboš KORENČIAK, Antonín KUČERA a Vojtěch ŘEHÁK. Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms. In Nathalie Bertrand, Luca Bortolussi. Quantitative Evaluation of Systems. Cham: Springer, 2017. s. 190-206, 17 s. ISBN 978-3-319-66334-0. doi:10.1007/978-3-319-66335-7_12. info
  • BAIER, Christel, Clemens DUBSLAFF, Ľuboš KORENČIAK, Antonín KUČERA a Vojtěch ŘEHÁK. Synthesis of Optimal Resilient Control Strategies. In Deepak D'Souza, K. Narayan Kumar. Automated Technology for Verification and Analysis. Cham: Springer International Publishing, 2017. s. 417-434, 18 s. ISBN 978-3-319-68166-5. doi:10.1007/978-3-319-68167-2_27. info
  • KORENČIAK, Ľuboš, Antonín KUČERA a Vojtěch ŘEHÁK. Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration. In 2016 IEEE 24th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. London: IEEE Computer Society, 2016. s. 367-372, 6 s. ISBN 978-1-5090-3431-4. doi:10.1109/MASCOTS.2016.34. URL info
  • BRÁZDIL, Tomáš, Ľuboš KORENČIAK, Jan KRČÁL, Petr NOVOTNÝ a Vojtěch ŘEHÁK. Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis. In Javier Campos, Boudewijn R. Haverkort. Quantitative Evaluation of Systems. BERLIN: SPRINGER-VERLAG BERLIN, 2015. s. 141-159, 19 s. ISBN 978-3-319-22263-9. doi:10.1007/978-3-319-22264-6_10. info
  • BABIAK, Tomáš, Jan STREJČEK a Vojtěch ŘEHÁK. Almost linear Büchi automata. Mathematical Structures in Computer Science, Cambridge: Cambridge University Press, 2012, roč. 22, č. 2, s. 203-235. ISSN 0960-1295. doi:10.1017/S0960129511000399. URL info
  • BABIAK, Tomáš, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. LTL to Büchi Automata Translation: Fast and More Deterministic. In Cormac Flanagan, Barbara König. TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2012. s. 95-109, 15 s. ISBN 978-3-642-28755-8. doi:10.1007/978-3-642-28756-5_8. URL info
  • BRÁZDIL, Tomáš, Holger HERMANNS, Jan KRČÁL, Jan KŘETÍNSKÝ a Vojtěch ŘEHÁK. Verification of Open Interactive Markov Chains. In Deepak D'Souza and Telikepalli Kavitha and Jaikumar Radhakrishnan. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2012. s. 474-485, 12 s. ISBN 978-3-939897-47-7. doi:10.4230/LIPIcs.FSTTCS.2012.474. URL info
  • BRÁZDIL, Tomáš, Jan KRČÁL, Jan KŘETÍNSKÝ a Vojtěch ŘEHÁK. Fixed-delay Events in Generalized Semi-Markov Processes Revisited. In CONCUR 2011 - Concurrency Theory: 22nd International Conference. Berlin Heidelberg New York: Springer, 2011. s. 140-155, 16 s. ISBN 978-3-642-23216-9. info
  • ŘEHÁK, Vojtěch, Petr SLOVÁK, Jan STREJČEK a Loïc HÉLOUËT. Decidable Race Condition and Open Coregions in HMSC. In Jochen Küster, Emilio Tuosto. Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010). Paphos, Kypr: ECEASST, 2010. 12 s. ISSN 1863-2122. URL info
  • BRÁZDIL, Tomáš, Jan KRČÁL, Jan KŘETÍNSKÝ, Antonín KUČERA a Vojtěch ŘEHÁK. Stochastic Real-Time Games with Qualitative Timed Automata Objectives. In CONCUR 2010 - Concurrency Theory. Berlin Heidelberg New York: Springer, 2010. s. 207-221, 15 s. ISBN 978-3-642-15374-7. doi:10.1007/978-3-642-15375-4_15. info
  • BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Process Rewrite Systems. Acta informatica, Berlin: Springer-Verlag, 2009, roč. 46, č. 1, s. 1-28. ISSN 0001-5903. URL info
  • KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008). 2009. vyd. Amsterdam, The Netherlands: Elsevier Science Publishers, 2009. s. 105-117, 13 s. ISSN 1571-0661. URL info
  • KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Petri Nets Are Less Expressive Than State-Extended PA. Theoretical Computer Science, Amsterdam, North Holland: Elsevier Science Publishers, 2008, roč. 394, 1-2, s. 134-140. ISSN 0304-3975. info
  • SMRČKA, Aleš, Vojtěch ŘEHÁK, Tomáš VOJNAR, David ŠAFRÁNEK, Petr MATOUŠEK a Zdeněk ŘEHÁK. Verifying VHDL Designs with Multiple Clocks in SMV. In Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006. Bonn: Springer-Verlag, 2007. s. 148-164, 16 s. ISBN 978-3-540-70951-0. info
  • KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Proc. of 9th Internat. Workshop on Verification of Infinite-State Systems. 2007. info
  • KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Refining Undecidability Border of Weak Bisimilarity. In Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05). 2006. vyd. Amsterdam, The Netherlands: Elsevier Science, 2006. s. 17-36, 20 s. ISSN 1571-0661. URL info
  • ANTOŠ, David a Vojtěch ŘEHÁK. Routing and Level 2 Addressing in a Hardware Accelerator for Network Applications. In ICT 2006, 13th International Conference on Telecommunications. Funchal, Madeira: University of Aveiro, Portugal, 2006. s. 1-4, 4 s. ISBN 972-98368-4-1. info
  • BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Process Rewrite Systems. In FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings. Berlin: Springer-Verlag, 2006. s. 248-259, 12 s. ISBN 978-3-540-49994-7. info
  • KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Reachability of Hennessy - Milner properties for weakly extended PRS. In FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference. Berlin, Heidelberg: Springer-Verlag, 2005. s. 213-224, 12 s. ISBN 3-540-30495-9. info
  • ANTOŠ, David, Vojtěch ŘEHÁK a Jan KOŘENEK. Hardware Router's Lookup Machine and its Formal Verification. In ICN'2004 Conference Proceedings. Gosier, Guadeloupe, French Caribbean: University of Haute Alsace, Colmar, France, 2004. s. 1002-1007, 6 s. ISBN 0-86341-325-0. URL info
  • KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Extended Process Rewrite Systems: Expressiveness and Reachability. In CONCUR 2004 - Concurrency Theory. LNCS 3170. Berlin, Heidelberg, New York: Springer, 2004. s. 355-370, 16 s. ISBN 3-540-22940-X. info
  • KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. In INFINITY'2003: 5th International Workshop on Verification of Infinite-State Systems. 2004. vyd. Amsterdam, The Netherlands: Elsevier Science, 2004. s. 75-88, 14 s. ISSN 1571-0661. URL info
  • ŘEHÁK, Vojtěch. Randomized symbolic model checking. Brno, 2002. iii, 38 s. info

2019/07/04