On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (INFINITY, 2003)

Extended Process Rewrite Systems: Expressiveness and Reachability. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (CONCUR, 2004)

Reachability of Hennessy-Milner Properties for Weakly Extended PRS. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (FSTTCS, 2005)

Refining the Undecidability Border of Weak Bisimilarity. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (INFINITY, 2005)

Verifying VHDL Designs with Multiple Clocks in SMV. - Ales Smrcka; Vojtech Rehák; Tomás Vojnar; David Safránek; Petr Matousek; Z. Rehák (FMICS/PDMC, 2006)

Petri nets are less expressive than state-extended PA. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (Theor. Comput. Sci., 2008)

On decidability of LTL model checking for process rewrite systems. - Laura Bozzelli; Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (Acta Informatica, 2009)

Almost Linear Büchi Automata - Tomás Babiak; Vojtech Rehák; Jan Strejcek (EXPRESS, 2009)

On Decidability of LTL+Past Model Checking for Process Rewrite Systems. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (INFINITY, 2009)

Reachability is decidable for weakly extended process rewrite systems. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (Inf. Comput., 2009)

Stochastic Real-Time Games with Qualitative Timed Automata Objectives. - Tomás Brázdil; Jan Krcál; Jan Kretínský; Antonín Kucera 001; Vojtech Rehák (CONCUR, 2010)

A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness - Tomás Babiak; Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (CoRR, 2010)

Decidable Race Condition and Open Coregions in HMSC. - Vojtech Rehák; Petr Slovák; Jan Strejcek; Loïc Hélouët (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010)

Fixed-Delay Events in Generalized Semi-Markov Processes Revisited. - Tomás Brázdil; Jan Krcál; Jan Kretínský; Vojtech Rehák (CONCUR, 2011)

Measuring performance of continuous-time stochastic processes using timed automata. - Tomás Brázdil; Jan Krcál; Jan Kretínský; Antonín Kucera 001; Vojtech Rehák (HSCC, 2011)

Sequence Chart Studio. - Martin Bezdeka; Ondrej Bouda; Lubos Korenciak; Matú Madzin; Vojtech Rehák (ACSD, 2012)

Verification of Open Interactive Markov Chains. - Tomás Brázdil; Holger Hermanns; Jan Krcál; Jan Kretínský; Vojtech Rehák (FSTTCS, 2012)

Controllable-Choice Message Sequence Graphs. - Martin Chmelik; Vojtech Rehák (MEMICS, 2012)

LTL to Büchi Automata Translation: Fast and More Deterministic. - Tomás Babiak; Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (TACAS, 2012)

On time-average limits in deterministic and stochastic petri nets. - Tomás Brázdil; Lubos Korenciak; Jan Krcál; Jan Kretínský; Vojtech Rehák (ICPE, 2013)

Solving adversarial patrolling games with bounded error: (extended abstract). - Michal Abaffy; Tomás Brázdil; Vojtech Rehák; Branislav Bosanský; Antonín Kucera 001; Jan Krcál (AAMAS, 2014)

Dealing with Zero Density Using Piecewise Phase-Type Approximation. - Lubos Korenciak; Jan Krcál; Vojtech Rehák (EPEW, 2014)

Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis. - Tomás Brázdil; Lubos Korenciak; Jan Krcál; Petr Novotný 001; Vojtech Rehák (QEST, 2015)

Strategy Synthesis in Adversarial Patrolling Games. - Tomás Brázdil; Petr Hlinený; Antonín Kucera 001; Vojtech Rehák; Matús Abaffy (CoRR, 2015)

Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC. - Lubos Korenciak; Vojtech Rehák; Adrian Farmadin (IFM, 2016)

Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration. - Lubos Korenciak; Antonín Kucera 001; Vojtech Rehák (MASCOTS, 2016)

Synthesis of Optimal Resilient Control Strategies. - Christel Baier; Clemens Dubslaff; Lubos Korenciak; Antonín Kucera 001; Vojtech Rehák (ATVA, 2017)

Synthesis of Optimal Resilient Control Strategies. - Christel Baier; Clemens Dubslaff; Lubos Korenciak; Vojtech Rehák (CoRR, 2017)

Automatic Synthesis of Efficient Regular Strategies in Adversarial Patrolling Games. - David Klaska; Antonín Kucera 001; Tomás Lamser; Vojtech Rehák (AAMAS, 2018)

Solving Patrolling Problems in the Internet Environment. - Tomás Brázdil; Antonín Kucera 001; Vojtech Rehák (IJCAI, 2018)

Synthesizing Efficient Solutions for Patrolling Problems in the Internet Environment. - Tomás Brázdil; Antonín Kucera 001; Vojtech Rehák (CoRR, 2018)

PROLEMus: A Proactive Learning-Based MAC Protocol Against PUEA and SSDF Attacks in Energy Constrained Cognitive Radio Networks. - Milan Patnaik; V. Kamakoti 001; Vashek Matyas; Vojtech Rehák (IEEE Trans. Cogn. Commun. Netw., 2019)

Mean-payoff Optimization in Continuous-time Markov Chains with Parametric Alarms. - Christel Baier; Clemens Dubslaff; Lubos Korenciak; Antonín Kucera 001; Vojtech Rehák (ACM Trans. Model. Comput. Simul., 2019)

Adversarial Patrolling with Drones. - David Klaska; Antonín Kucera 001; Vojtech Rehák (AAMAS, 2020)

Regstar: efficient strategy synthesis for adversarial patrolling games. - David Klaska; Antonín Kucera 001; Vít Musil; Vojtech Rehák (UAI, 2021)

Minimizing Expected Intrusion Detection Time in Adversarial Patrolling. - David Klaska; Antonín Kucera 001; Vít Musil; Vojtech Rehák (AAMAS, 2022)

General Optimization Framework for Recurrent Reachability Objectives. - David Klaska; Antonín Kucera 001; Vít Musil; Vojtech Rehák (IJCAI, 2022)

On-the-fly adaptation of patrolling strategies in changing environments. - Tomás Brázdil; David Klaska; Antonín Kucera 001; Vít Musil; Petr Novotný 001; Vojtech Rehák (UAI, 2022)

Synthesizing Resilient Strategies for Infinite-Horizon Objectives in Multi-Agent Systems. - David Klaska; Antonín Kucera 001; Martin Kurecka; Vít Musil; Petr Novotný 001; Vojtech Rehák (IJCAI, 2023)

Mean Payoff Optimization for Systems of Periodic Service and Maintenance. - David Klaska; Antonín Kucera 001; Vít Musil; Vojtech Rehák (IJCAI, 2023)

Optimizing Local Satisfaction of Long-Run Average Objectives in Markov Decision Processes. - David Klaska; Antonín Kucera 001; Vojtech Kur; Vít Musil; Vojtech Rehák (AAAI, 2024)

Multiple Mean-Payoff Optimization Under Local Stability Constraints. - David Klaska; Antonín Kucera 001; Vojtech Kur; Vít Musil; Vojtech Rehák (AAAI, 2025)

Who Let the Guards Out: Visual Support for Patrolling Games. - Matej Lang; Adam J. Stepánek; Róbert Zvara; Vojtech Rehák; Barbora Kozlíková (IEEE Trans. Vis. Comput. Graph., 2025)

Memory Assignment for Finite-Memory Strategies in Adversarial Patrolling Games. - Vojtech Kur; Vít Musil; Vojtech Rehák (CoRR, 2025)