July 30, 2024
The paper “Markov Decision Processes with Sure Parity and Multiple Reachability Objectives” by Raphaël Berthon, Joost-Pieter Katoen and Tobias Winkler has been accepted for the 18th Int. Conference on Reachability Problems (RP 2024) in Vienna. The paper presents new algorithms and complexity bounfs to achieve one sure parity condition and several quantitative threshold objectives on Markov decision processes.
June 21, 2024
The paper entitled “A Spectrum of Approximate Probabilistic Bisimulations” by Timm Spork (TU Dresden), Christel Baier (TU Dresden), Joost-Pieter Katoen, Jakob Piribauer (TU Dresden) and Tim Quatmann has been accepted for the 35th Int. Conf. on Concurrency Theory (CONCUR) in Calgary, Canada. The paper compares several different (and some new) notions of approximate strong and weak approximate probabilistic bisimulation relations and relates them.
April 11, 2024
The paper entitled “Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains” by Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler has received the EAPLS (Eur. Association of Programming Languages) Best Paper Award@ETAPS 2024. The paper provides efficient and scalable algorithms to compute expected visiting times in Markov chains, and shows how this can be used to compute reachability probabilities, stationary distributions and conditional…
Read more about ETAPS Best Paper AwardMarch 21, 2024
Joost-Pieter Katoen has been elected as member of Leopoldina, the German Academy of Sciences. This academy was established in 1652 and is the oldest academy in the world. Katoen is the first computer scienttist from RWTH Aachen University in Leopoldina and the 15th RWTH member of Leopoldina ever. See also press announcements: https://www.rwth-aachen.de/cms/root/Die-RWTH/Aktuell/Pressemitteilungen/Maerz-2024/~bgppks/Joost-Pieter-Katoen-in-die-Leopoldina-au/lidx/1/ and…
Read more about LeopoldinaFebruary 24, 2024
The paper entitled “Exact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions” by Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase and Joost-Pieter Katoen has been accepted for the Conference Object-Oriented Programming, Systems, Languages, and Applications 2024 (OOPSLA). The paper presents a novel exact inference technique for discrete probabilistic programs with unbounded loops and conditioning. It uses probability generating functions to do…
Read more about Paper at OOPSLA 2024February 13, 2024
The paper “Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains” by Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler has been nominated for one of the ETAPS 2024 best paper awards. (For Tim, this is the second year in a row to be nominated for such an award.)
January 18, 2024
The ERC has granted the Proof-of-Concept proposal VERIPROB (A Deductive Verifier for Probabilistic Programs) by Joost-Pieter Katoen. The grant will enables the further development of Caesar, a verifier vor weakest precondition-reasoning on probabilistic programs.
December 22, 2023
The papers “Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains” by Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler and “Learning Explainable and Better Performing Representations of POMDP Strategies” by Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky and Stefanie Mohr have both been accepted at TACAS 2024 in Luxemburg. The first paper presents new and efficient algorithms for computing expected visited times in…
Read more about Two Papers at TACAS 2024December 10, 2023
The paper entitled “Natural Strategic Ability in Stochastic Multi-Agent Systems” by Raphael Berthon, Monyque Myttelmann, Antoniello Murano and Joost-Pieter Katoen has been accepted for the 38th AAAI Conference on Artificial Intelligence (AAAI 2024) in Vancouver, Canada. The paper present complexity result on the model checking of the probabilistic alternating temporal logics PATL and PATL∗ under natural strategies on probabilistic multi-agent systems.
November 16, 2023
Two papers were accepted at the Dafny 2024 workshop. The paper “Caesar: A Verifier for Probabilistic Programs” by Philipp Schröer, Kevin Batz, Benjamin Kaminski (Saarland University and UCL), Joost-Pieter Katoen and Christoph Matheja (TU Denmark) presents a quantitative program verification infrastructure for discrete probabilistic programs, building on our work published at OOPSLA 2023. The paper “Generation of Verified Assembly Code Using Dafny and Reinforcement Learning” by Christopher Brix…
Read more about Two Papers at Dafny 2024November 15, 2023
Tim Quatmann has been awarded a KI-Starter Grant for his project proposal “Verifying AI Systems under Partial Observability“. The KI-Starter Grant is an initiative of the State North-Rhine Westphalia to strengthen its position in AI and in particular stimulates young researchers in their academic career. Tim’s project focuses on the automated verification using model checking of partially observable probabilistic models. The aim is to obtain safer, more reliable, and trustworthy AI agents that…
Read more about Tim Quatmann wins a KI-Starter GrantNovember 7, 2023
The paper entitled “Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs” by Kevin Batz, Tom Biskup, Joost-Pieter Katoen, and Tobias Winkler has been accepted at the 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024). The paper shows how to use deductive verification to resolve pure nondeterminism in probabilistic programs such that the obtained determinized program satisfies a given quantitative specification.
November 7, 2023
The paper entitled “Model Checking Temporal Properties of Recursive Probabilistic Programs” by Tobias Winkler, Christina Gehnen and Joost-Pieter Katoen has been accepted for the special issues devoted to FoSSaCS 2022 in the journal Logical Methods in Computer Science. The paper shows that model checking a probabilistic pushdown automata against omega visibly push-down languages (e.g., expressed as CaReT formulas) is decidable. It also provides some complexity bounds on this problem.
November 6, 2023
Tom Biskup has received the Berthold Vöcking Master Award 2023 for his thesis “Invariant-based Strategy Synthesis for Nondeterministic Probabilistic Programs”. The thesis addresses the problem of making provably good decisions in face of stochastic uncertainty which is key in, e.g., complex planning tasks. Tom’s solution draws on well-known principles from deductive program verification such as loop invariants.
October 27, 2023
The paper “A Deductive Verification Infrastructure for Probabilistic Programs” by Philipp Schröer, Kevin Batz, Benjamin Kaminski, Joost-Pieter Katoen and Christoph Matheja received a distinguished artifact award at OOPSLA 2023. The artifact consists of the deductive verifier Caesar together with a couple of benchmark examples. Caesar has a website at www.caesarverifier.org where the tool can be downloaded and documentation is provided.