We’re excited to announce that Michele Chiari and Francesco Pontiggia have won the Best Student Paper Award for their paper Decentralized Planning Using Probabilistic Hyperproperties at the conference on Autonomous Agents and Multiagent Systems (AAMAS) 2025 in Detroit at the end of May. The paper was written together with Filip Macák, Roman Andriushchenko, and Milan Češka, and introduces a novel framework for multi-agent planning under uncertainty. By leveraging probabilistic hyperproperties and model-checking techniques, the authors propose a more flexible and expressive method for decentralized decision-making — with important implications for the future of Artificial Intelligence (AI) and robotics.

The paper is part of the broader research carried out within the VASSAL Project (Verification and Analysis for Safety and Security of Applications in Life)—a collaboration among several institutions, including TU Wien, Brno University of Technology, CEA, Penn State University, and Honeywell. Given the increasing reliance on software in critical areas such as medical systems and autonomous vehicles, ensuring its reliability, security, and resilience is essential. VASSAL addressess current challenges in software verification and safety, focusing on advancing automated verification and analysis tools.

Congratulations on this outstanding achievement!

About Michele Chiari and Francesco Pontiggia

Michele Chiari

Michele Chiari is a Marie Skłodowska-Curie Postdoctoral Fellow at TU Wien, within the TrustCPS group led by Prof. Ezio Bartocci. His research focuses on formal methods for software verification, and he currently works on the verification of probabilistic programs. He received his Ph.D. and M.Sc. from Politecnico di Milano (Italy) where he worked on developing temporal logics based on context-free languages, and on their model checking. He also worked in the field of approximate computing on the development of an LLVM-based tool that automatically transforms floating-point computations to less precise, but faster representations.

Francesco Pontiggia

Francesco Pontiggia is a Ph.D. student in the TrustCPS Research Group at TU Wien, under the supervision of Prof. Ezio Bartocci, Dr. Michele Chiari and Prof. Laura Kovács. He is also part of the LogiCS@TUWien Doctoral College. He is interested in verification and synthesis problems for probabilistic programs and systems. In particular, his Ph.D. project is about probabilistic model checking for recursive probabilistic programs, and for so called probabilistic hyperproperties. He obtained his B.Sc. and M.Sc. in Computer Science and Engineering from Politecnico di Milano (Italy), with a Master thesis on a model checking tool for recursive programs.

Abstract

Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes (MDPs) and reachability or expected reward specifications. In this paper, we propose a different approach: we use an MDP describing how a single agent operates in an environment and probabilistic hyperproperties to capture desired temporal objectives for a set of decentralized agents operating in the environment. We extend existing approaches for model checking probabilistic hyperproperties to handle temporal formulae relating paths of different agents, thus requiring the self-composition between multiple MDPs. Using several case studies, we demonstrate that our approach provides a flexible and expressive framework to broaden the specification capabilities with respect to existing planning techniques. Additionally, we establish a close connection between a subclass of probabilistic hyperproperties and planning for a particular type of Dec-MDPs, for both of which we show undecidability. This lays the ground for the use of existing decentralized planning tools in the field of probabilistic hyperproperty verification.

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.