Petr's photo

Petr Novotný

Associate professor of computer science
I work as an associate 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 systems, application of formal methods in AI (particularly in decision making under uncertainty), and theoretical foundations of probabilistic verification.

You can download my full academic CV here (version from May 2021).

Ph.D. Students

I have the privilege to collaborate with the following bright students:

What's new

February 2023 Our paper On Lexicographic Proof Rules for Probabilistic Termination was accepted in Formal Aspects of Computing.
December 2022 In the PC of CONCUR'23.
November 2022 Our paper Shielding in Resource-Constrained Goal POMDPs was accepted at AAAI'23.
September 2022 Our paper Efficient Strategy Synthesis for MDPs with Resource Constraints was accepted in IEEE Transactions on Automatic Control.
August 2022 In the PC of AAAI 2023
July 2022 Our paper On-the-fly Adaptation of Patrolling Strategies in Changing Environments was accepted at UAI'22.
August 2021 In the PC of AAMAS 2022
July 2021 We have two papers accepted at Formal Methods 2021: The paper On Lexicographic Proof Rules for Probabilistic Termination studies new martingale-based proof rules for almost-sure termination of probabilistic programs (you can view the full version here). The paper Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption is an extended tool paper describing the FiMDP tool for strategy synthesis in Markov decision processes with resource constraints and omega-regular objectives. The tool is accessible on github and you are invited to play around with it!

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, and are themselves subject to randomly distributed errors.

Analysis of Probabilistic Programs

To ensure that probabilistic systems are safe to use, I develop formal methods that automatically analyze probabilistic code and check whether the program behaves according to the designer's intentions. Recently, I have focused on the development of new automated proof techniques for termination [POPL'16, POPL'18, FM'21] and safety [POPL'17] properties of probabilistic programs.

Formal Methods for AI Planning and Decision Making under Uncertainty

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 synthesise a policy (a blueprint for interacting with the environment) for an autonomous agent so as to maximize the agent's expected utility, while keeping the risk of undesirable outcomes below an acceptable level [AAAI'17, IJCAI'18, AAAI'20]. I also work on planning algorithms for agents with limited energy resources [CAV'12, CAV'14, AAMAS'16, CAV'20, AAAI'23.].

Theoretical Foundations of Probabilistic Verification

The aforementioned techniques must rest on solid theoretical foundations. Hence, the third pillar of my work is theoretical research related to complex probabilistic processes. For instance, I work on decidability and complexity issues in probabilistic vector addition systems with states (pVASS) [LICS'14, LICS'15, ATVA'19 ]. 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. I also contributed to determining the exact complexity of computing optimal strategies in finite-horizon Markov decision processes [ICALP'19 ] resolving an open question dating back to 1980's (see here and here).
See my DBLP and Google Scholar profiles. ArXiv preprints are accessible via DBLP links. If you cannot access some of the publications, email me and I will be happy to provide a preprint.

(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.)

Autumn 2022

Courses: Tutorials:

Spring 2022

Courses: Tutorials:

Autumn 2021

Courses: Tutorials:

Spring 2021

Courses:

Autumn 2021

Courses: Tutorials:

Research Engagement for Bachelor's and Master' Students

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 range of student research opportunities within this field ranging from implementation work to proving theorems. Previous research experience is not 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 in the Information system of MU. 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.