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 both undergraduates and Ph.D. candidates are available. 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 August 2018).

What's new

February 2018 On the PC of HIGHLIGHTS'19.
December 2018 My research on analysis of probabilistic received funding from the Czech Science Foundation! From January 2019, I will act as the principal investigator for the grant project "Verification and Analysis of Probabilistic Programs."
September 2018 Giving an invited talk on Risk-Aware Planning in Partially Observable Markov Decision Processes at the GAMENET conference (a meeting of the COST Action European Network for Game Theory) in Krakow.
July 2018 Check out our new complexity results on finite-horizon MDPs, a collaboration with N. Balaji, S. Kiefer, G.A. Pérez, and M. Shirmohammadi. Feedback is welcome.
July 2018 Presenting at IJCAI'18. Check out the paper here.

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.

    Conference Papers

  1. Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-sum Objectives.
    K. Chatterjee, A. Elgyütt, P. Novotný, and O. Rouillé.
    IJCAI-ECAI 2018. [tech. report]
  2. Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS.
    T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, F. Zuleger.
    LICS 2018. [tech. report]
  3. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs.
    S. Agrawal, K. Chatterjee, and P. Novotný.
    POPL 2018. [paper, tech. report]
  4. Optimizing Expectation with Guarantees in POMDPs.
    K. Chatterjee, P. Novotný, G. A. Pérez, J.-F. Raskin, and Đ. Žikelić.
    AAAI 2017 [paper, tech. report]
  5. Stochastic Invariants for Probabilistic Termination.
    K. Chatterjee, P. Novotný, and Đ. Žikelić.
    POPL 2017. [paper, tech. report]
  6. 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]
  7. 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]
  8. Optimizing the Expected Mean Payoff in Energy Markov Decision Processes.
    T. Brázdil, A. Kučera, and P. Novotný.
    ATVA 2016. [paper, tech. report]
  9. Stability in Graphs and Games.
    T. Brázdil, V. Forejt, A. Kučera, and P. Novotný.
    CONCUR 2016. [paper, tech. report]
  10. 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]
  11. 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]
  12. Minimizing Running Costs in Consumption Systems.
    T. Brázdil, D. Klaška, A. Kučera, and P. Novotný.
    CAV 2014. [paper, tech. report]
  13. 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]
  14. Solvency Markov Decision Processes with Interest.
    T. Brázdil, T. Chen, V. Forejt, P. Novotný, and A. Simaitis.
    FSTTCS 2013. [paper, tech. report]
  15. 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
  16. 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]
  17. 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]

    18. Technical Reports

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

Spring 2019

Office hours: Monday 15:30-17:00, C412 (during the term)

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 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 (*). 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 participants 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 internships at select institutions (IST Austria, UT Austin,...).


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:

Ph.D. Position in Verification and Analysis of Probabilistic Programs

I offer a funded Ph.D. candidate position in the area of probabilistic program analysis. The aim of the project is to develop new techniques for verification of probabilistic programs, with a particular focus on verification of systems in the domain of artificial intelligence. The project offers opportunities for both foundational theoretical work as well as implementation of prototype tools.

A successful applicant will receive, apart from the standard Ph.D. stipend at FI MU, a significant supplemental funding in the form of a part-time job contract. The funding also covers all tuition fees.

The official call is posted on the faculty website, with an application deadline of May 15, 2019 (follow this link for an electronic application form). Prospective candidates are strongly encouraged to get in touch with me beforehand (see my contact details), enclosing their CV and a statement of motivation.

You can also find out why it is a good idea to study in Brno. :)