Nils Jansen

PhD thesis on probabilistic counterexamples

The PhD thesis of Nils Jansen titled “Counterexamples in Probabilistic Verification” has recently been published online at the library webpage and can also be found here. The thesis covers multiple approaches and new concepts to the generation and representation of counterexamples for refuted properties on probabilistic systems. All results have been published at several conference proceedings […]

Paper accepted at CAV 2015

Our paper “PROPhESY: A PRObabilistic ParamEter SYnthesis Tool” by  Christian Dehnert, Sebastian Junges, Nils Jansen,  Florian Corzilius, Matthias Volk, Harold Bruintjes,  Joost-Pieter Katoen, and Erika Ábrahám was accepted for publication at the 27th International Conference on Computer Aided Verification (CAV) 2015. The paper presents the tool PROPhESY, which is dedicated to model checking and parameter synthesis for parametric discrete-time Markov […]

Paper accepted at FM 2015

The paper “Counterexamples for Expected Rewards” by Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker was accepted for publication at the 20th International Symposium on Formal Methods (FM) 2015. The paper presents the first approaches on counterexamples for discrete-time Markov chains and expected reward properties. Methods are proposed to extract a minimal subsystem which already […]

Paper accepted at NFM 2015

Our paper “A Greedy Approach for the Efficient Repair of Stochastic Models” by Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, and Joost-Pieter Katoen was accepted at NFM 2015. The paper addresses the problem of model repair for parametric discrete-time Markov chains which consists of changing a model with minimal costs such that a desired property is satisfied. We present a […]

Paper accepted for LMCS

Our paper “High-level Counterexamples for Probabilistic Automata” by Ralf Wimmer, Nils Jansen, Erika Ábrahám and Joost-Pieter Katoen was accepted for publication in the journal Logical Methods in Computer Science (LMCS). In this paper we investigate the computation of several variations of (minimal) counterexamples that are represented in PRISM’s high-level language which defines a subclass of probabilistic programs. These NP-hard problems are solved […]

Paper accepted at ATVA'14

Our paper “Fast Debugging of PRISM Models” by Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám and Joost-Pieter Katoen was accepted at ATVA 2014. The paper presents a new way to compute critical parts of a PRISM program by utilizing a MAX-SAT solver. This is the first approach rendering the computation of these sort of […]

Paper accepted in Theoretical Computer Science

The paper “Minimal Counterexamples for Linear-Time Probabilistic Verification” by Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen and Bernd Becker was accepted for publication in the journal Theoretical Computer Science. The paper thoroughly examines the possibilities for computing so-called minimal critical subsystems for Markov decision processes by means of mixed integer linear programming.

Survey paper probabilistic counterexamples

A survey paper concerning the generation of counterexamples for probabilistic systems was published by Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen and Ralf Wimmer within the scope of the PhD school SFM in Bertinoro, Italy. This paper gives a nice introduction to the foundations and the state-of-the-art of this topic, explaining all methods […]

Paper accepted at QEST 2014

The paper “Accelerating Parametric Probabilistic Verification” by Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen and Bernd Becker was accepted at QEST 2014 in Florence. The paper considers a new approach on Model Checking parametric discrete-time Markov chains based on eliminating the strongly connected components of the system graph. Together with […]