Complete list of publications
 Journal papers

T. Babiak, V. Rehak, and J. Strejcek.
Almost linear Buchi automata.
Mathematical Structures in Computer Science, 22(02):203235, 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.
Meanpayoff optimization in continuoustime markov chains with
parametric alarms.
ACM Trans. Model. Comput. Simul., 29(4):28:128: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 1015, 2018,
pages 659666. 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 TwentySeventh International Joint Conference on
Artificial Intelligence, IJCAI 2018, July 1319, 2018, Stockholm,
Sweden, pages 121127. 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 417434,
2017.
[PDF,
LNCS]
[BibTex]

C. Baier, C. Dubslaff, L. Korenciak, A. Kucera, and V. Rehak.
Meanpayoff optimization in continuoustime Markov chains with
parametric alarms.
In Quantitative Evaluation of Systems  14th International Conference,
QEST 2017, volume 10503 of Lecture Notes in Computer Science,
pages 190206. SpringerVerlag, 2017.
[PDF,
(c) SpringerVerlag,
LNCS]
[BibTex]

L. Korenciak, V. Rehak, and A. Farmadin.
Extension of PRISM by synthesis of optimal timeouts in fixeddelay
CTMC.
In Integrated Formal Methods  12th International Conference, IFM
2016, volume 9681 of Lecture Notes in Computer Science, pages
130138. SpringerVerlag, 2016.
[PDF,
(c) SpringerVerlag,
LNCS]
[BibTex]

L. Korenciak, A. Kucera, and V. Rehak.
Efficient timeout synthesis in fixeddelay CTMC using policy
iteration.
In 24th IEEE International Symposium on Modeling, Analysis and Simulation
of Computer and Telecommunication Systems, MASCOTS 2016, pages
367372. IEEE, 2016.
[PDF,
(c) IEEE]
[BibTex]

T. Brazdil, L. Korenciak, J. Krcal, P. Novotny, and V. Rehak.
Optimizing performance of continuoustime stochastic systems using
timeout synthesis.
In Quantitative Evaluation of Systems, 12th International Conference,
QEST 2015, volume 9259 of Lecture Notes in Computer Science,
pages 141159. Springer, 2015.
[PDF,
(c) SpringerVerlag,
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
MultiAgent Systems, AAMAS '14, pages
16171618. IFAAMAS/ACM, 2014.
[BibTex]

L. Korenciak, J. Krcal, and V. Rehak.
Dealing with zero density using piecewise phasetype approximation.
In Computer Performance Engineering  11th European Workshop, EPEW 2014, volume 8721 of Lecture Notes in Computer Science, pages 119134. Springer, 2014.
[DOI link]
[full version on arXiv]
[BibTex]

T. Brazdil, L. Korenciak, J. Krcal, J. Kretinsky, and V. Rehak.
On timeaverage limits in deterministic and stochastic Petri nets.
In ACM/SPEC International Conference
on Performance Engineering, ICPE'13, pages 421422. ACM, 2013.
[DOI link]
[BibTex]

M. Chmelik and V. Rehak.
Controllablechoice 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 118130
SpringerVerlag, 2013.
[PDF,
(c) SpringerVerlag,
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
474485, Dagstuhl, Germany, 2012. Schloss DagstuhlLeibnizZentrum 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 148153. 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 95109. SpringerVerlag,
2012.
[PDF Preprint,
(c) SpringerVerlag,
LNCS]
[DOI link]
[full version on arXiv]
[BibTex]

T. Brazdil, J. Krcal, J. Kretinsky, and V. Rehak.
Fixeddelay Events in Generalized SemiMarkov Processes
Revisited.
In Proceedings of the 22nd international conference on Concurrency theory
(CONCUR'11), volume 6901 of Lecture Notes in Computer Science,
pages 140155. SpringerVerlag, 2011.
[PDF Preprint,
(c) SpringerVerlag,
LNCS]
[DOI link]
[full version on arXiv]
[BibTex]

T. Brazdil, J. Krcal, J. Kretinsky, A. Kucera, and V. Rehak.
Measuring performance of continuoustime stochastic processes using
timed automata.
In Proceedings of 14th International Conference on Hybrid Systems:
Computation and Control (HSCC'11), pages 3342. 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 (GTVMT 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 RealTime Games with Qualitative Timed Automata
Objectives.
In CONCUR 2010  Concurrency Theory: 21st International Conference,
volume 6269 of Lecture Notes in Computer Science, pages 207221.
SpringerVerlag, 2010.
[PDF Preprint,
(c) SpringerVerlag,
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 1625, 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 FIMURS201204, 52pp, Faculty of Informatics, Masaryk
University, 2012.
[PDF]
[BibTex]

M. Chmelik and V. Rehak.
Controllablechoice 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 RealTime Games with Qualitative Timed Automata
Objectives.
Technical Report FIMURS201005, 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 FIMURS200910, 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 FIMURS200702, 33pp, Faculty of Informatics, Masaryk
University, 2007.
[PDF]
[PostScript]
[BibTex]
 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:105117, 2009.
Joint Proceedings of the 8th, 9th, and 10th International Workshops on
Verification of InfiniteState 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):671680, 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):128, 2009.
[PDF Preprint]
[DOI link]
[BibTex]

M. Kretinsky, V. Rehak, and J. Strejcek.
Petri nets are less expressive than stateextended PA.
Theoretical Computer Science, 394(12):134140, 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
InfiniteState Systems (INFINITY'05), volume 149 of Electronic Notes
in Theoretical Computer Science, pages 1736. 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
FiniteState Unit.
In Philippe Schnoebelen, editor, INFINITY'2003: 5th International Workshop
on Verification of InfiniteState Systems, volume 98 of
Electronic Notes in Theoretical Computer Science, pages 7588.
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 InfiniteState Systems, INFINITY'2007, pages 111.
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 248259. SpringerVerlag, 2006.
[PDF, (c) SpringerVerlag,
LNCS]
[DOI link]
[BibTex]

V. Rehak.
Weakly Extended Process Rewrite Systems.
In MOVEP'06: 7th school on MOdeling and VErifying parallel Processes,
pages 360364. Universite de Bordeaux, 2006.
Student's paper.
[PDF]
[PostScript]
[BibTex]

M. Kretinsky, V. Rehak, and J. Strejcek.
Reachability of HennessyMilner 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 213224. SpringerVerlag,
2005.
[PDF, (c) SpringerVerlag, 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 InfiniteState Systems (INFINITY'05), volume NS054 of
BRICS Notes Series, pages 314. 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 7782. 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 355370. SpringerVerlag, 2004.
[PDF, (c) SpringerVerlag, LNCS]
[BibTex]

M. Kretinsky, V. Rehak, and J. Strejcek.
On Extensions of Process Rewrite Systems: Rewrite Systems with Weak
FiniteState Unit.
In Philippe Schnoebelen, editor, Preliminary Proceedings of the 5th
International Workshop on Verification of InfiniteState Systems,
INFINITY'2003, pages 7385. 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 FIMURS200605, 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 FIMURS200506, 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 RS0407, 12pp, Basic Research in Computer Science, Aarhus,
Denmark, 2004.
[PDF]
[BibTex]

M. Kretinsky, V. Rehak, and J. Strejcek.
Process Rewrite Systems with Weak FiniteState Unit.
Technical Report FIMURS200305, 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]
 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 18. 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 5562. 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 148164. SpringerVerlag, 2007.
[PDF,
PostScript,
(c) SpringerVerlag,
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 14. Universidade da Madeira, 2006.
[PDF]
[BibTex]

D. Antos, V. Rehak, and P. Holub.
Packet Filtering for FPGABased Routing Accelerator.
In CESNET Conference 2006, pages 161173. 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 151160. 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 10021007. 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 91102, 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]

Vojtech Rehak.
$\xor$OBDD in Symbolic Model Checking.
In M. Bielikova, editor, Proceedings of SOFSEM'02 Student Research
Forum, pages 4146, 2002.
[PDF]
[PostScript]
[BibTex]

V. Rehak.
Randomized Symbolic Model Checking.
Master's thesis, Masaryk University Brno, 2002.
[PDF]
[PostScript]
[BibTex]