Paper Accepted at CDC 2017

The paper entitled “Motion Planning under Partial Observability using Game-Based Abstraction” by Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, and Bernd Becker has been accepted for publication at CDC 2017 in Melbourne, Australia. The paper applies model-checking to synthesise motion plans for robots under partial observability, and makes this feasible by […]

Probabilistic Model Checker Storm: First Release

We launch the new probabilistic model checker Storm. It features the analysis of discrete- and continuous-time variants of both Markov chains and MDPs. It supports the Prism and JANI modeling languages, probabilistic programs, dynamic fault trees and generalized stochastic Petri nets. It has a modular set-up in which solvers and symbolic engines can easily be […]

Paper accepted at SRDS

The paper “Model-Checking Assisted Protocol Design for Ultra-Reliable Low-Latency Wireless Networks” by Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen and James Gross has been accepted at SRDS 2016 in Budapest, Hungary. It presents the modelling and verification of EchoRing, a protocol for the MAC-layer tailored towards ultra-reliable wireless communication. The verification process uncovered some inconsistencies in the protocol, and […]

Two papers accepted at ATVA

Two new papers have been accepted at ATVA 2016 in Chiba, Japan. The paper “Bounded Model Checking for Probabilistic Program” by Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Lukas Westhofen describes an automated on-the-fly verification approach for probabilistic programs. It incorporates key features such as conditioning and parametric probabilities. Experiments show the feasibility […]

Paper accepted at SETTA 2015

The paper “Fault trees on a Diet” by Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink and Mariëlle Stoelinga has been accepted at SETTA’15.  The paper presents a novel, fully automated reduction technique for Dynamic Fault Trees (DFTs). The key idea is to interpret DFTs as directed graphs and exploit graph rewriting to simplify them.