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 […]

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 […]

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 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 […]

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.