The paper entitled “SAFEST: the static and dynamic fault tree analysis tool” by Matthias Volk (Twente), Muzammil Ibne Irshad (DGB), Joost-Pieter Katoen, Falak Sher (DGB), Marielle Stoelinga (Twente) and Ahmad Zafar (DGB) has been accepted for presentation at the European Conference On Safety And Reliability (ESREL) 2023 in Southampton, UK. The paper presents a powerful […]

The paper entitled “Search and Explore: Symbiotic Policy Synthesis in POMDPs” by Roman Andriushchenko (Brno University of Technology), Alexander Bork, Milan Ceska (Brno), Sebastian Junges (Radboud University, Netherlands), Joost-Pieter Katoen and Filip Macak (Brno) has been accepted for presentation at the 33th Conference on Computer-Aided Verification in Paris. The paper presents a symbiotic anytime algorithm that tightly integrates a belief-based […]

The paper entitled “Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks” by Bahare Salmani and Joost-Pieter Katoen has been accepted for presentation at IJCAI 2023 (the 32nd Int. Joint Conf. on Artificial Intelligence) in Macao. Out of 4566 full-paper submissions, about 15% has been accepted. The paper gives an algorithm for estimating the […]

The paper entitled “On Certificates, Expected Runtimes, and Termination in ProbabilisticPushdown Automata” by Tobias Winkler and Joost-Pieter Katoen has been accepted for presentation at the IEEE/ACM Annual Symposium on Logic on Computer Science 2023 to be held in Boston. The paper studies certification of numerical characteristics of probabilistic pushdown systems, that is, how one can […]

The paper entitled “A Compositional Semantics of Boolean-logic Driven Markov Processes” by Shahid Khan, Joost-Pieter Katoen andMarc Bouissou (EDF) has been accepted as regular paper for IEEE Transactions on Dependable and Secure Computing. This paper provides a compositional and operational semantics (using Markov automata) of BDMPs, a prominent dynamic extension of static fault trees to […]

The proceedings of the 25th Symposium on Formal Methods (FM 2023), edited by Marsha Chechik (Toronto), Joost-Pieter Katoen and Martin Leucker (Lübeck), and published as LNCS volume 14000, are available from March 2 and accessible under: https://link.springer.com/book/10.1007/978-3-031-27481-7.

The project proposal “Probabilistic Model Checking under Partial Observability with Multiple Objectives” (POMPOM) has been granted for funding by the German Research Council. The project aims to develop new model-checking algorithms for combinations of qualitative, stochastic and total expected reward objectives for partially observable Markov decision processes (and games). The funding is for two years […]

The paper entitled “Stochastic Games with Lexicographic Objectives” by Krishnendu Chatterjee (IST Austria), Joost-Pieter Katoen, Stephanie Moor (TU Munich), Maximilian Weininger (Tu Munich), and Tobias Winkler has been accepted for publication in Formal Methods in System Design. This paper presents a detailed study of stochastic turn-based games (SG) with lexicographic objectives. The paper is an […]

Three papers of the MOVES group have been accepted for TACAS 2023! “A Practitioner’s Guide to MDP Model Checking Algorithms” by Arnd Hartmanns, Sebastian Junges, Tim Quatmann and Maximilian Weininger presents an empirical evaluation of various algorithms (different forms of value iteration, policy iteration and direct algorithms) to compute reachability probabilities in Markov decision processes. […]

The paper entitled “A Calculus for Amortized Expected Runtimes” by Kevin Batz, Benjamin Kaminski (Saarland/UCL), Joost-Pieter Katoen, Christoph Matheja (DTU Lyngby) and Lena Verscht has been accepted for presentation at the 50th ACM Symposium on Principles of Programming Languages (POPL). The paper presents a weakest precondition-style calculus to determine the amortized expected run-time of randomized […]