Complete list of publications

Publications related to the ITI project:

• Journal papers


• T. Babiak, V. Rehak, and J. Strejcek. Almost linear Buchi automata. Mathematical Structures in Computer Science, 22(02):203-235, 2012. [PDF, (c) Cambridge University Press, Cambridge Journals Online] [DOI link] [BibTex]
  
  
• Conference and workshop papers:


• Christel Baier, Clemens Dubslaff, Lubos Korenciak, Antonin Kucera, and Vojtech Rehak. Mean-payoff optimization in continuous-time markov chains with parametric alarms. ACM Trans. Model. Comput. Simul., 29(4):28:1-28:26, December 2019. [PDF] [BibTex]
  
  
• D. Klaska, A. Kucera, T. Lamser, and V. Rehak. Automatic synthesis of efficient regular strategies in adversarial patrolling games. In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, Stockholm, Sweden, July 10-15, 2018, pages 659-666. International Foundation for Autonomous Agents and Multiagent Systems Richland, SC, USA / ACM, 2018. [PDF] [BibTex]
  
  
• T. Brazdil, A. Kucera, and V. Rehak. Solving patrolling problems in the internet environment. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 121-127. ijcai.org, 2018. [PDF] [BibTex]
  
  
• C. Baier, C. Dubslaff, L. Korenciak, A. Kucera, and V. Rehak. Synthesis of optimal resilient control strategies. In ATVA 2017: Automated Technology for Verification and Analysis, volume 10482 of Lecture Notes in Computer Science, pages 417-434, 2017. [PDF, LNCS] [BibTex]
  
  
• C. Baier, C. Dubslaff, L. Korenciak, A. Kucera, and V. Rehak. Mean-payoff optimization in continuous-time Markov chains with parametric alarms. In Quantitative Evaluation of Systems - 14th International Conference, QEST 2017, volume 10503 of Lecture Notes in Computer Science, pages 190-206. Springer-Verlag, 2017. [PDF, (c) Springer-Verlag, LNCS] [BibTex]
  
  
• L. Korenciak, V. Rehak, and A. Farmadin. Extension of PRISM by synthesis of optimal timeouts in fixed-delay CTMC. In Integrated Formal Methods - 12th International Conference, IFM 2016, volume 9681 of Lecture Notes in Computer Science, pages 130-138. Springer-Verlag, 2016. [PDF, (c) Springer-Verlag, LNCS] [BibTex]
  
  
• L. Korenciak, A. Kucera, and V. Rehak. Efficient timeout synthesis in fixed-delay CTMC using policy iteration. In 24th IEEE International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS 2016, pages 367-372. IEEE, 2016. [PDF, (c) IEEE] [BibTex]
  
  
• T. Brazdil, L. Korenciak, J. Krcal, P. Novotny, and V. Rehak. Optimizing performance of continuous-time stochastic systems using timeout synthesis. In Quantitative Evaluation of Systems, 12th International Conference, QEST 2015, volume 9259 of Lecture Notes in Computer Science, pages 141-159. Springer, 2015. [PDF, (c) Springer-Verlag, LNCS] [BibTex]
  
  
• M. Abaffy, T. Brazdil, V. Rehak, B. Bosansky, A. Kucera, and J. Krcal. Solving adversarial patrolling games with bounded error: (extended abstract). In International conference on Autonomous Agents and Multi-Agent Systems, AAMAS '14, pages 1617-1618. IFAAMAS/ACM, 2014. [BibTex]
  
  
• L. Korenciak, J. Krcal, and V. Rehak. Dealing with zero density using piecewise phase-type approximation. In Computer Performance Engineering - 11th European Workshop, EPEW 2014, volume 8721 of Lecture Notes in Computer Science, pages 119-134. Springer, 2014. [DOI link] [full version on arXiv] [BibTex]
  
  
• T. Brazdil, L. Korenciak, J. Krcal, J. Kretinsky, and V. Rehak. On time-average limits in deterministic and stochastic Petri nets. In ACM/SPEC International Conference on Performance Engineering, ICPE'13, pages 421-422. ACM, 2013. [DOI link] [BibTex]
  
  
• M. Chmelik and V. Rehak. Controllable-choice Message Sequence Graphs. In Proceedings of Mathematical and Engineering Methods in Computer Science, 8th Doctoral Workshop (MEMICS 2012), Revised Selected Papers, volume 7721 of Lecture Notes in Computer Science, pages 118-130 Springer-Verlag, 2013. [PDF, (c) Springer-Verlag, LNCS] [DOI link] [full version on arXiv] [BibTex]
  
  
• T. Brazdil, H. Hermanns, J. Krcal, J. Kretinsky, and V. Rehak. Verification of open interactive Markov chains. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), volume 18 of Leibniz International Proceedings in Informatics (LIPIcs), pages 474-485, Dagstuhl, Germany, 2012. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. [PDF] [DOI link] [full version] [BibTex]
  
  
• M. Bezdeka, O. Bouda, L. Korenciak, M. Madzin, and V. Rehak. Sequence Chart Studio. In Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12), pages 148-153. IEEE, 2012. [PDF Preprint] [DOI link] [BibTex]
  
  
• T. Babiak, M. Kretinsky, V. Rehak, and J. Strejcek. LTL to Buchi Automata Translation: Fast and More Deterministic. In Proceedings of 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), volume 7214 of Lecture Notes in Computer Science, pages 95-109. Springer-Verlag, 2012. [PDF Preprint, (c) Springer-Verlag, LNCS] [DOI link] [full version on arXiv] [BibTex]
  
  
• T. Brazdil, J. Krcal, J. Kretinsky, and V. Rehak. Fixed-delay Events in Generalized Semi-Markov Processes Revisited. In Proceedings of the 22nd international conference on Concurrency theory (CONCUR'11), volume 6901 of Lecture Notes in Computer Science, pages 140-155. Springer-Verlag, 2011. [PDF Preprint, (c) Springer-Verlag, LNCS] [DOI link] [full version on arXiv] [BibTex]
  
  
• T. Brazdil, J. Krcal, J. Kretinsky, A. Kucera, and V. Rehak. Measuring performance of continuous-time stochastic processes using timed automata. In Proceedings of 14th International Conference on Hybrid Systems: Computation and Control (HSCC'11), pages 33-42. ACM, 2011. [PDF Preprint] [DOI link] [full version on arXiv] [BibTex]
  
  
• V. Rehak, P. Slovak, J. Strejcek, and L. Helouet. Decidable Race Condition and Open Coregions in HMSC. In Postproceedings of Graph Transformation and Visual Modeling Techniques 2010 (GT-VMT 2010)., volume 29 of Electronic Communications of the EASST, 12 pages, 2010. [PDF Preprint] [PDF] [BibTex]
  
  
• T. Brazdil, J. Krcal, J. Kretinsky, A. Kucera, and V. Rehak. Stochastic Real-Time Games with Qualitative Timed Automata Objectives. In CONCUR 2010 - Concurrency Theory: 21st International Conference, volume 6269 of Lecture Notes in Computer Science, pages 207-221. Springer-Verlag, 2010. [PDF Preprint, (c) Springer-Verlag, LNCS] [DOI link] [full version] [BibTex]
  
  
• T. Babiak, V. Rehak, and J. Strejcek. Almost Linear Buchi Automata. In Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09). EPTCS 8, pages 16-25, 2009. [PDF Preprint] [DOI link] [BibTex]
  
  
• Technical reports and others:


• T. Brazdil, H. Hermanns, J. Krcal, J. Kretinsky, and V. Rehak. Verification of Open Interactive Markov Chains. Technical Report FIMU-RS-2012-04, 52pp, Faculty of Informatics, Masaryk University, 2012. [PDF] [BibTex]
  
  
• M. Chmelik and V. Rehak. Controllable-choice Message Sequence Graphs. CoRR, abs/1209.4499, 2012. [PDF] [arXiv:1209.4499] [BibTex]
  
  
• T. Babiak, M. Kretinsky, V. Rehak, and J. Strejcek. LTL to Buchi Automata Translation: Fast and More Deterministic. CoRR, abs/1201.0682, 2012. [PDF] [arXiv:1201.0682] [BibTex]
  
  
• T. Babiak, M. Kretinsky, V. Rehak, and J. Strejcek. A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness. CoRR, abs/1011.4214, 2010. [PDF] [arXiv:1011.4214v1] [BibTex]
  
  
• T. Brazdil, J. Krcal, J. Kretinsky, A. Kucera, and V. Rehak. Stochastic Real-Time Games with Qualitative Timed Automata Objectives. Technical Report FIMU-RS-2010-05, 39pp, Faculty of Informatics, Masaryk University, 2010. [PDF] [PostScript] [BibTex]
  
  
• V. Rehak, P. Slovak, J. Strejcek, and L. Helouet. Decidable Race Condition for HMSC. Technical Report FIMU-RS-2009-10, 30pp, Faculty of Informatics, Masaryk University, 2009. [PDF] [PostScript] [BibTex]
  
  
• J. Babica, V. Rehak, P. Slovak, P. Troubil, and M. Zavadil. Formalisms and Tools for Design and Specification of Network Protocols. Technical Report FIMU-RS-2007-02, 33pp, Faculty of Informatics, Masaryk University, 2007. [PDF] [PostScript] [BibTex]
  
  

Publications related to process rewrite systems (my PhD research):

• Journal papers


• M. Kretinsky, V. Rehak, and J. Strejcek. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. Electronic Notes in Theoretical Computer Science, 239:105-117, 2009. Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008). [PDF Preprint] [DOI link] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. Reachability is decidable for weakly extended process rewrite systems. Information and Computation, 207(6):671-680, 2009. [PDF Preprint] [DOI link] [BibTex]
  
  
• L. Bozzelli, M. Kretinsky, V. Rehak, and J. Strejcek. On Decidability of LTL Model Checking for Process Rewrite Systems. Acta Informatica, 46(1):1-28, 2009. [PDF Preprint] [DOI link] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. Petri nets are less expressive than state-extended PA. Theoretical Computer Science, 394(1-2):134-140, 2008. [PDF Preprint] [DOI link] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. Refining the Undecidability Border of Weak Bisimilarity. In Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05), volume 149 of Electronic Notes in Theoretical Computer Science, pages 17-36. Elsevier Science Publishers, 2006. [PDF Preprint] [DOI link] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. In Philippe Schnoebelen, editor, INFINITY'2003: 5th International Workshop on Verification of Infinite-State Systems, volume 98 of Electronic Notes in Theoretical Computer Science, pages 75-88. Elsevier Science Publishers, 2004. [DOI link] [BibTex]
  
  
• Conference and workshop papers:


• M. Kretinsky, V. Rehak, and J. Strejcek. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Preliminary Proceedings of the 9th International Workshop on Verification of Infinite-State Systems, INFINITY'2007, pages 1-11. Univerisity of Lisboa, 2007. [PDF] [PostScript] [BibTex]
  
  
• L. Bozzelli, M. Kretinsky, V. Rehak, and J. Strejcek. On Decidability of LTL Model Checking for Process Rewrite Systems. In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, volume 4337 of Lecture Notes in Computer Science, pages 248-259. Springer-Verlag, 2006. [PDF, (c) Springer-Verlag, LNCS] [DOI link] [BibTex]
  
  
• V. Rehak. Weakly Extended Process Rewrite Systems. In MOVEP'06: 7th school on MOdeling and VErifying parallel Processes, pages 360-364. Universite de Bordeaux, 2006. Student's paper. [PDF] [PostScript] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. Reachability of Hennessy-Milner Properties for Weakly Extended PRS. In R. Ramanujam and Sandeep Sen, editors, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, volume 3821 of Lecture Notes in Computer Science, pages 213-224. Springer-Verlag, 2005. [PDF, (c) Springer-Verlag, LNCS] [DOI link] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. Refining the Undecidability Border of Weak Bisimilarity. In Preliminary Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05), volume NS-05-4 of BRICS Notes Series, pages 3-14. Basic Research in Computer Science, Aarhus, Denmark, 2005. [PDF] [PostScript] [BibTex]
  
  
• V. Rehak. Reachability for Extended Process Rewrite Systems. In MOVEP'04: 6th school on MOdeling and VErifying parallel Processes, pages 77-82. Universite Libre de Bruxelles, 2004. Student's paper. [PDF] [PostScript] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. Extended Process Rewrite Systems: Expressiveness and Reachability. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory: 15th International Conference, volume 3170 of Lecture Notes in Computer Science, pages 355-370. Springer-Verlag, 2004. [PDF, (c) Springer-Verlag, LNCS] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. In Philippe Schnoebelen, editor, Preliminary Proceedings of the 5th International Workshop on Verification of Infinite-State Systems, INFINITY'2003, pages 73-85. Les Universites a Marseille, 2003. [PDF] [PostScript] [BibTex]
  
  
• Technical reports:


• L. Bozzelli, M. Kretinsky, V. Rehak, and J. Strejcek. On Decidability of LTL Model Checking for Process Rewrite Systems. Technical Report FIMU-RS-2006-05, 27pp, Faculty of Informatics, Masaryk University, 2006. Full version of FSTTCS 2006 paper. [PDF] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. Refining the Undecidability Border of Weak Bisimilarity. Technical Report FIMU-RS-2005-06, 22pp, Faculty of Informatics, Masaryk University, 2005. Full version of INFINITY 2005 paper. [PDF] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. On the Expressive Power of Extended Process Rewrite Systems. Technical Report RS-04-07, 12pp, Basic Research in Computer Science, Aarhus, Denmark, 2004. [PDF] [BibTex]
  
  
• M. Kretinsky, V. Rehak, and J. Strejcek. Process Rewrite Systems with Weak Finite-State Unit. Technical Report FIMU-RS-2003-05, 23pp, Faculty of Informatics, Masaryk University Brno, 2003. Full version of INFINITY 2003 paper. [PDF] [BibTex]
  
  
• Thesis:


• V. Rehak. On Extensions of Process Rewrite Systems. PhD thesis, Masaryk University, Brno, 2007. [PDF] [PostScript] [BibTex]
  
  
• V. Rehak. On Extensions of Process Rewrite Systems, PhD thesis proposal, Faculty of Informatics, Masaryk University, 2004. [PDF] [PostScript]
  
  

Publications related to practical verification (the Liberouter project):

• Conference and workshop papers


• D. Antos and V. Rehak. Routing, L2 Addressing, and Packet Filtering in a Hardware Engine. In Proceedings of the 2nd Doctoral Wokrshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), pages 1-8. Brno University of Technology, 2006. [BibTex]
  
  
• P. Hlavka, V. Rehak, A. Smrcka, P. Simecek, D. Safranek, and T. Vojnar. Formal Verification of the CRC Algorithm Properties. In Proceedings of the 2nd Doctoral Wokrshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), pages 55-62. Brno University of Technology, 2006. [BibTex]
  
  
• A. Smrcka, V. Rehak, T. Vojnar, D. Safranek, P. Matousek, and Z. Rehak. 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, volume 4346 of Lecture Notes in Computer Science, pages 148-164. Springer-Verlag, 2007. [PDF, PostScript, (c) Springer-Verlag, LNCS] [DOI link] [BibTex]
  
  
• D. Antos and V. Rehak. Routing and Level 2 Addressing in a Hardware Accelerator for Network Applications. In ICT 2006, 13th International Conference on Telecommunications, pages 1-4. Universidade da Madeira, 2006. [PDF] [BibTex]
  
  
• D. Antos, V. Rehak, and P. Holub. Packet Filtering for FPGA-Based Routing Accelerator. In CESNET Conference 2006, pages 161-173. CESNET, 2006. [PDF] [BibTex]
  
  
• T. Kratochvila, V. Rehak, and D. Safranek. Formal Verification of a FIFO Component in Design of Network Monitoring Hardware. In CESNET Conference 2006, pages 151-160. CESNET, 2006. [PDF] [BibTex]
  
  
• D. Antos, V. Rehak, and J. Korenek. Hardware Router's Lookup Machine and its Formal Verification. In 3rd International Conference on Networking ICN'2004 Conference Proceedings, pages 1002-1007. University of Haute Alsace, Colmar, France, 2004. [PDF] [PostScript] [BibTex]
  
  
• D. Antos, J. Korenek, and V. Rehak. Vyhledavani v IPv6 smerovaci implementovanem v hradlovem poli (Lookups in IPv6 router implemented in an FPGA. In EurOpen, Sbornik prispevku XXIII. konference. (Proceedings of the 23rd conference), pages 91-102, 2003. (In Czech). [BibTex]
  
  
• Technical reports:


• P. Hlavka, T. Kratochvila, V. Rehak, D. Safranek, P. Simecek, and T. Vojnar. CRC64 Algorithm Analysis and Verification. Technical Report 27, 7pp, CESNET, December 2005. [PDF] [PostScript] [BibTex]
  
  
• J. Holecek, T. Kratochvila, V. Rehak, D. Safranek, and P. Simecek. Verification Process of Hardware Design in Liberouter Project. Technical Report 05, 7pp, CESNET, November 2004. [PDF] [PostScript] [BibTex]
  
  
• J. Holecek, T. Kratochvila, V. Rehak, D. Safranek, and P. Simecek. How to Formalize FPGA Hardware Design. Technical Report 04, 11pp, CESNET, October 2004. [PDF] [PostScript] [BibTex]
  
  
• J. Holecek, T. Kratochvila, V. Rehak, D. Safranek, and P. Simecek. Verification Results in Liberouter Project. Technical Report 03, 32pp, CESNET, September 2004. [PDF] [PostScript] [BibTex]
  
  
• T. Kratochvi la, V. Rehak, and P. Simecek. Verification of COMBO6 VHDL Design. Technical Report 17, 17pp, CESNET, November 2003. [PDF] [PostScript] [BibTex]
  
  
• D. Antos, J. Korenek, K. Minarikova, and V. Rehak. Packet Header Matching in Combo6 IPv6 Router. Technical Report 01, 15pp, CESNET, January 2003. [PDF] [PostScript] [BibTex]
  
  
• J. Barnat, T. Brazdil, P. Krcal, V. Rehak, and D. Safranek. Model Checking in IPv6 Hardware Router Design. Technical Report 07, 8pp, CESNET, July 2002. [PDF] [PostScript] [BibTex]
  
  

Publications related to symbolic model checking (my Master thesis):

• Vojtech Rehak. $\xor$-OBDD in Symbolic Model Checking. In M. Bielikova, editor, Proceedings of SOFSEM'02 Student Research Forum, pages 41-46, 2002. [PDF] [PostScript] [BibTex]
  
  
• V. Rehak. Randomized Symbolic Model Checking. Master's thesis, Masaryk University Brno, 2002. [PDF] [PostScript] [BibTex]