Petr's photo

Petr Novotný

Assistant professor in computer science
I work as an assistant professor at the Faculty of Informatics, Masaryk University, Brno, Czech Republic. Previously, I was an ISTFellow postdoc at IST Austria, working in the group of Krishnendu Chatterjee. My chief research interests are analysis of probabilistic programs, application of formal methods in AI, and theoretical foundations of probabilistic verification.

I am looking for motivated student collaborators! Funded positions for undergraduates are available, with a possibility of long-term collaboration. The collaboration will be focused on probabilistic programs, their analysis, and the use of probabilistic programming in AI. Feel free to contact me for further info.
You can download my full academic CV here (version from November 2019).

What's new

January 2019 Our paper Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications was accepted at ICAPS'20!
November 2019 Our paper Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes was accepted at AAAI'20!
September 2019 Giving a talk at the University of Oxford.
July 2019 Giving a talk at ICALP'19.
June 2019 Our paper Deciding Fast Termination for Probabilistic VASS with Nondeterminism was accepted at ATVA'19!

Contact

Faculty of Informatics, Masaryk University
Botanická 68a
60200 Brno
Czech Republic

e-mail: petr.novotny {at} fi.muni.cz

Why Probability?

Computing systems are often pictured as an epitome of determinism, precisely following their pre-programmed instructions. This picture of computers is far from being complete, as many systems encompass an inherently probabilistic behaviour. This is already true for some classical application domains, such as security protocols. However, the proliferation of probabilistic systems in computing is nowadays driven mainly by the advances in the development of intelligent systems. These systems often operate with fuzzy inputs (e.g. a robot with imprecise sensors), act according to an imprecise model of their environment (e.g. a self-driving car interpreting the sensor data into positions of obstacles), and are themselves subject to randomly distributed errors.

Analysis of Probabilistic Programs

To ensure that inherently probabilistic systems, such as those appearing in AI domain, are safe to use, I develop formal methods that can automatically analyze code with probabilistic instructions and check whether the program behaves according to the designer's intentions. In my research, I focus on the development of new automated proof techniques for termination [POPL'18, POPL'16] and safety [POPL'17] properties of probabilistic programs.

Formal Methods for AI Planning

Apart from developing verification techniques for general probabilistic code, I also work on applying formal methods to concrete problems and algorithms in the domain of AI planning. I focus particularly on the problem of risk-averse planning, where the goal is to plan a sequence of actions for an autonomous agent so as to maximize the agent's expected utility and at the same time keep the risk of a catastrophic outcome below an acceptable level [AAAI'17, IJCAI'18]. I work also on planning algorithms for agents with limited energy resources [CAV'12, CAV'14, AAMAS'16].

Theoretical Foundations of Probabilistic Verification

The aforementioned techniques must rest on solid theoretical foundations. Hence, the third pillar of my work is theoretical research of problems related to complex probabilistic processes. In particular, I work on decidability and complexity issues in probabilistic vector addition systems with states (pVASS) [LICS'14, LICS'15]. The pVASS can be viewed as abstractions of probabilistic programs that capture the essential dynamics of program variables while abstracting away some complexities of the control-flow structure; many technqiues developed for analysis of pVASS can be leveraged for analysis of real-world programs.
See also my DBLP and Google Scholar profiles.

(If your not a computer scientist and you are puzzled by the dominance of my conference publications over journal ones, this thread and memo summarize the historical context behind the publishing culture in CS. While I am not a strong defender of this culture, I find some of its elements, such as the fast feedback to one's results, very appealing.)

    Peer-Reviewed Conference Papers

  1. Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.
    K. Chatterjee, M. Chmelík, D. Karkhanis, P. Novotný and A. Royer
    ICAPS 2020 (to appear).
  2. Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes.
    T. Brázdil, K. Chatterjee, P. Novotný, J. Vahala.
    AAAI 2020 (to appear). [tech. report]
  3. Bidding Games on Markov Decision Processes.
    G. Avni, T. A. Henzinger, R. Ibsen-Jensen, P. Novotný.
    RP 2019. [paper]
  4. Deciding Fast Termination for Probabilistic VASS with Nondeterminism.
    T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan.
    ATVA 2019. [paper, tech. report]
  5. On the Complexity of Value Iteration.
    N. Balaji, S. Kiefer, P. Novotný, G.A. Pérez, and M. Shirmohammadi.
    ICALP 2019. [paper, tech. report]
  6. Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-sum Objectives.
    K. Chatterjee, A. Elgyütt, P. Novotný, and O. Rouillé.
    IJCAI-ECAI 2018. [paper, tech. report]
  7. Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS.
    T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, and F. Zuleger.
    LICS 2018. [paper, tech. report]
  8. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs.
    S. Agrawal, K. Chatterjee, and P. Novotný.
    POPL 2018. [paper, tech. report]
  9. Optimizing Expectation with Guarantees in POMDPs.
    K. Chatterjee, P. Novotný, G. A. Pérez, J.-F. Raskin, and Đ. Žikelić.
    AAAI 2017 [paper, tech. report]
  10. Stochastic Invariants for Probabilistic Termination.
    K. Chatterjee, P. Novotný, and Đ. Žikelić.
    POPL 2017. [paper, tech. report]
  11. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.
    K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad.
    POPL 2016. [paper, tech. report]
  12. Stochastic Shortest Path with Energy Constraints in POMDPs: (Extended Abstract).
    T. Brázdil, K. Chatterjee, M. Chmelík, A. Gupta, and P. Novotný.
    AAMAS 2016. [paper, tech. report]
  13. Optimizing the Expected Mean Payoff in Energy Markov Decision Processes.
    T. Brázdil, A. Kučera, and P. Novotný.
    ATVA 2016. [paper, tech. report]
  14. Stability in Graphs and Games.
    T. Brázdil, V. Forejt, A. Kučera, and P. Novotný.
    CONCUR 2016. [paper, tech. report]
  15. Long-Run Average Behaviour of Probabilistic Vector Addition Systems.
    T. Brázdil, S. Kiefer, A. Kučera, and P. Novotný.
    LICS 2015. [paper, tech. report]
  16. Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis.
    T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, and V. Řehák.
    QEST 2015. [paper, tech. report]
  17. Minimizing Running Costs in Consumption Systems.
    T. Brázdil, D. Klaška, A. Kučera, and P. Novotný.
    CAV 2014. [paper, tech. report]
  18. Zero-Reachability in Probabilistic Multi-Counter Automata.
    T. Brázdil, S. Kiefer, A. Kučera, P. Novotný, and J.-P. Katoen.
    CSL-LICS 2014. [paper, tech. report]
  19. Solvency Markov Decision Processes with Interest.
    T. Brázdil, T. Chen, V. Forejt, P. Novotný, and A. Simaitis.
    FSTTCS 2013. [paper, tech. report]
  20. Determinacy in Stochastic Games with Unbounded Payoff Functions.
    T. Brázdil, A. Kučera, and P. Novotný.
    MEMICS 2012. [paper, tech. report] Best paper award
  21. Efficient Controller Synthesis for Consumption Games with Multiple Resource Types.
    T. Brázdil, K. Chatterjee, A. Kučera, and P. Novotný.
    CAV 2012. [paper, tech. report]
  22. Minimizing Expected Termination Time in One-Counter Markov Decision Processes.
    T. Brázdil, A. Kučera, P. Novotný, and D. Wojtczak.
    ICALP 2012. [paper, tech. report]

    23. Peer-Reviewed Journals

  23. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.
    K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad.
    ACM TOPLAS, 2018.

    24. Technical Reports

  24. Efficient Algorithms for Checking Fast Termination in VASS.
    T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, and D. Velan.
    [tech. report]

Autumn 2019

Office hours: Monday 10:00-11:30, C412 (during the term)
Note: On November 4 and 11, the office hours will be extraordinarily held on Monday, 13:00-14:30 (in C412).

Courses: Tutorials:

Spring 2019

Courses: Tutorials:

Autumn 2018

Courses: Tutorials:

Research Engagement for Bachelor's and Master' Students

I am looking for motivated student collaborators! Would you like to dig deeper into some of the modern topics in computer science? Do you enjoy learning new things? Would you like to try to contribute to the body of scientific knowledge? If yes, then read on!

My research focuses on verification and analysis of systems that exhibit probabilistic behaviour. Such systems prominently appear particularly in the field of artificial intelligence (AI), but also in other domains, such as privacy & security, operations research, and bio-informatics.

There is a wide range of student research opportunities within this field ranging from implementation work to proving theorems. No previous research experience is necessary: diligence and a willingness to learn new things are crucial.

There are several ways of joining my research. First, you can have a look at the Bachelor's and Master's thesis topics below. Those that are directly related to some of my ongoing research projects are marked by an asterisk (*); although also the unmarked topics could potentially evolve into research projects. Second, if you do not find exactly the topic that would suit you or you would like to explore further possibilities, just get in touch with me and we can discuss suitable topics.

Last but not least, funding is available for long-term collaborators on my research project "Verification and Analysis of Probabilistic Programs." In addition, depending on the precise topic there is a possibility of short-term research visits at select institutions.


Bachelor's and Master's Thesis Projects

A list of thesis topics that I currently offer can be found below or in the university information system. Most of the topics allow for scaling to both Bachelor's and Master's levels. The thesis language is negotiable (Czech, Slovak, English).

The list is not meant to be exhaustive — I am open to discussing other project ideas related to these topics or to my general research interests.

If you are interested in doing a thesis under my supervision, let me know; I'll be happy to answer your questions and clarify the details.

Links to particular topics: