June 15, 2020
The paper entitled “Multi-Cost Bounded Trade-off Analysis in MDP” by Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen and Tim Quatmann has been accepted for the Journal of Automated Reasoning. The paper presents a memory-efficient algorithm for multi-objective model checking problems on Markov decision processes (MDPs) with multiple cost structures.
June 4, 2020
The paper entitled “Explaining Boolean-logic Driven Markov Processes using GSPNs” authored by Shahid Khan, Joost-Pieter Katoen and Marc Bouissou (EDF) has been accepted for the European Dependable Computing Conference (EDCC 2020). The paper presents a modular semantics of BDMPs using generalised stochastic Petri nets. Transition priorities are used to resolve possible non-deterministic error propagation.
June 2, 2020
We are looking for a talented student assistant to apply formal methods in the context of wireless networks. The job description can be found here.
May 19, 2020
We presented our results on benchmarking software model-checkers on automotive code at the virtual NFM2020 symposium. Check out the video at https://youtu.be/XLzIXVNCIuk?t=19941 !
May 13, 2020
We are happy to inform you that Joost-Pieter Katoen has been appointed Chair of the TACAS Steering Committee. TACAS is one of the flagship conferences on formal analysis techniques and tools for computer systems. He takes over this role from Bernhard Steffen (TU Dortmund) who has been SC chair since the foundation of TACAS in 1995.
May 4, 2020
The paper “Synthesizing and Optimizing FDIR Recovery Strategies From Fault Trees“ by Sascha Müller, Liana Mikaelyan, Andreas Gerndt (DLR German Aerospace Center, Braunschweig) and Thomas Noll has been accepted for publication by the Science of Computer Programming Journal. It investigates the synthesis of efficient recovery strategies for Failure Detection, Isolation and Recovery (FDIR) for space systems by means of dynamic fault trees and Markov automata.
May 2, 2020
The paper “A Compositional Semantics for Repairable BDMPs” by Shahid Khan, Joost-Pieter Katoen and Marc Bouissou (EDF) has been accepted for the 39th International Conference on Computer Safety, Reliability and Security. The paper describes a formal compositional semantics of Boolean-Driven Markov Processes and empirically validates the semantics using a discrete-event simulator for BDMPs.
April 24, 2020
The paper entitled “Various Ways to Quantify BDMPs” by Marc Bouissou, Joost-Pieter Katoen, Shahid Khan and Pavel Krcal has been accepted as invited contribution to the MARS2020 workshop. The paper compares various analysis techniques to determine the reliability of Boolean-Driven Markov Processes. It does so by analysing an emergency power supply of power plants.
April 17, 2020
The paper entitled “Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions” by Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, and Bernd Becker has been accepted for publication in IEEE Transactions on Automated Control (impact factor 5). The paper shows that by applying game-based abstraction to POMDP can significantly boost the optimal strategy synthesis in POMDPs.
April 15, 2020
We are looking for 1-2 student assistants who would be mainly working on the correction of exercise sheets for the course of Theoretical Foundations of the UML (FUML). Applicants of the job are expected with a background in theoretical computer science (mathematical logic, formal language, automata theory, computability & complexity, etc.). Drop us an email (Chen chenms@cs.rwth-aachen.de, Salmani salmani@cs.rwth-aachen.de) if you are interested.
April 13, 2020
The paper entitled “Approximating Values of Generalized-Reachability Stochastic Games” by Pranav Ashok, Krishnendu Chatterjee, Jan Kretinsky, Maximilian Weininger and Tobias Winkler has been accepted for presentation at LICS 2020. The main result of the paper is an algorithm to compute the Pareto curve for several objectives in two-player stochastic games.
April 6, 2020
The following three papers from the MOVES Group have been accepted for presentation at CAV 2020: “PrIC3: Property Directed Reachability for MDPs” by Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Philipp Schröer “Stochastic Games with Lexicographic Reachability-Safety Objectives” by Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger and Tobias Winkler, and “Unbounded-Time Safety Verification of Stochastic Differential Dynamics”…
Read more about Three Papers at CAV 2020March 9, 2020
The paper entitled “Generative Datalog with Continuous Distributions” by Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen and Peter Lindner has been accepted for presentation at PODS 2020, the ACM Conference on Principles of Database Systems. The paper provides a semantics to the probabilistic programming (aka: querying) language Datalog with continuous distributions.
February 21, 2020
The paper “Benchmarking Software Model Checkers on Automotive Code” by Lukas Westhofen (OFFIS), Philipp Berger and Joost-Pieter Katoen has been accepted for presentation at the 12th NASA Formal Methods Symposium. The paper reports on applying 12 SVComp and one commercial software model checkers on two C programs from automotive. Bottom line: the tools from SVComp did poorly, a modified CBMC version with k-induction did reasonable and the commercial tool did the best.
February 20, 2020
We are pleased to announce that Tsinghua University Press is about to publish a Chinese translation of the book “Principles of Model Checking” by Christel Baier and Joost-Pieter Katoen (MIT Press, 2008).