I am an assistant professor at the Department of Software Science (SWS) at the Radboud University Nijmegen in the Netherlands. Before this, I worked as a PostDoc and Research Associate at UT Austin with Dr. Ufuk Topcu and at RWTH Aachen University with Prof. Dr. Ir. Joost-Pieter Katoen. I did my PhD with Prof. Dr. Erika Ábrahám in the Theory of Hybrid Systems Group, also at RWTH Aachen University. My research interests are roughly to be classified in the verification and synthesis for cyber-physical systems. This includes:

  • Verification and (parameter) synthesis of probabilistic systems
  • Semantics and Verification of probabilistic programs
  • Interdisciplinary work on formal methods, machine learning, and robotics
During my PhD I worked on the generation of counterexamples for probabilistic systems and their application, symbolic techniques, and the utilization of solving techniques like SAT, SMT or linear programming.

Please feel free to contact me at any time via email: n.jansen 'at' science.ru 'dot' nl

News

Jul 12, 2017The paper "Motion Planning under Partial Observability using Game-Based Abstraction" has been accepted for publication at the Conference on Decision and Control (CDC) 2017 in Seattle, USA.
The paper proposes a new game-based abstraction scheme for motion planning scenarios that are modelled as partially observable Markov decision processes. Experiments comparing with state of the art tools such as PRISM show a significant improvement in verification times.
June 1, 2017I'm very happy to start my new position as an assistant professor in the Netherlands within the Department of Software Science (SWS) at the Radboud University Nijmegen.
Jan 26, 2017I'm organizing a workshop on Formal Approaches to Explainable VERification (FEVER 2017) together with Benoît Delahaye, Scott A. Smolka, and Ufuk Topcu. The workshop is co-located with CAV 2017 and will take place in Heidelberg, Germany, on July 23.
Jan 25, 2017Together with Joost-Pieter Katoen, I participated in writing a chapter for the book Self-aware Computing Systems about the application of parametric systems in the synthesis and verification for such systems. The book chapter is now available online.
Jan 21, 2017The paper "Synthesis of Shared Control Protocols with Provable Safety and Performance Guarantees" has been accepted for publication at the American Control Conference (ACC) 2017 in Seattle, USA.
The paper is the first to formalize synthesis of shared control protocols in robotics applications with correctness guarantees for temporal logic specifications. Experiments in a simulation environment show both the feasibility and the applicability of our approaches.
Dec 22, 2016The paper "Sequential Convex Programming for the Efficient Verification of Parametric MDPs" has been accepted for publication at TACAS 2017 in Uppsala, Sweden.
The paper presents convex optimization approaches for the synthesis of parametric Markov decision processes. At the heart of this approach are geometric programs, which can be solved in polynomial time. Applications to state-of-the art parameter synthesis and model repair are discussed. Benchmarks show the superiority to direct approaches using SMT solving.
Oct 20, 2016 For my PhD thesis "Counterexamples in Probabilistic Verification" I was awarded the Borchers Badge of RWTH Aachen University in Germany.
June 18, 2016Two of my papers have been accepted at ATVA 2016 in Chiba, Japan.
The paper "Bounded Model Checking for Probabilistic Programs" 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 and scalability on a wide range of benchmarks.
The paper "Parameter Synthesis for Markov Models: Faster Than Ever" presents a parameter space partitioning algorithm for parametric DTMCs, via a reduction to MDPs. The beauty of the approach is that it naturally extends to parametric MDPs, which can be solved via stochastic games. The new algorithm is experimentally shown to be orders of magnitude faster than existing approaches.
June 13, 2016 The paper "Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots" has been accepted for publication at ISoLA 2016 in Corfu, Greece.
The paper addresses the challenging standing-up task for robots. The approach of a scripted stand-up strategy is improved by applying both static and runtime methods by integrating reinforcement learning, static analysis and runtime monitoring techniques.

Publications

My journal and conference publications are listed below. See also my Google Scholar profile or my DBLP entry.

Currently under submission:

pdf Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu. Probabilistic Model Checking for Complex Cognitive Tasks – A case study in human-robot interaction
Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver. Conditioning in Probabilistic Programming

Published or accepted for publication:

pdf Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker. Motion Planning under Partial Observability using Game-Based Abstraction. In Proc. of IEEE Conference on Decision and Control (CDC), 2017, to appear.
pdf Nils Jansen, Murat Cubuktepe, Ufuk Topcu. Synthesis of Shared Control Protocols with Provable Safety and Performance Guarantees. In Proc. of the American Control Conference, IEEE, pages 1866--1873, 2017.
pdf Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, Ufuk Topcu. Sequential Convex Programming for the Efficient Verification of Parametric MDPs. In Proc. of TACAS, volume 10206 of LNCS, pages 133--150, 2017.
Radu Calinescu, Marco Autili, Javier Cámara, Antinisca Di Marco, Simos Gerasimou, Paola Inverardi, Alexander Perucci, Nils Jansen, Joost-Pieter Katoen, Marta Kwiatkowska, Ole J Mengshoel, Romina Spalazzese, and Massimo Tivoli. Synthesis and Verification of Self-aware Computing Systems. In Self-Aware Computing Systems, 2017.
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu. Probabilistic Verification for Cognitive Models. In Proc. of CDCAS. AAAI Technical Reports FS-16. AAAI Press, 2016.
pdf Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Lukas Westhofen. Bounded model checking for probabilistic programs. In Proc. of ATVA, volume 9638 of LNCS, pages 68--85. Springer, 2016.
pdf Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. Parameter synthesis for Markov models: Faster than ever. In Proc. of ATVA, volume 9938 of LNCS, pages 50-67. Springer, 2016.
pdf Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, and Joost-Pieter Katoen. Safety-constrained reinforcement learning for MDPs. In Proc. of TACAS, volume 9636 of LNCS, pages 130–146. Springer, 2016
pdf Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Joost-Pieter Katoen, Erika Ábrahám, and Harold Bruintjes. Parameter synthesis for probabilistic systems. In MBMV, pages 72–74. Albert-Ludwigs-Universität Freiburg, 2016.
pdf Ralf Wimmer, Nils Jansen, Erika Ábrahám, and Joost-Pieter Katoen. High-level counterexamples for probabilistic automata. Logical Methods in Computer Science, 11(1:15), 2015.
pdf Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker. Counterexamples for expected rewards. In Proc. of FM, volume 9109 of LNCS, pages 435–452. Springer, 2015.
pdf Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, and Joost-Pieter Katoen. A greedy approach for the efficient repair of stochastic models. In Proc. of NFM, volume 9058 of LNCS, pages 295–309. Springer, 2015.
pdf Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, and Federico Olmedo. Understanding probabilistic programs. In Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, volume 9360 of LNCS, pages 15–32. Springer, 2015.
pdf Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo, Friedrich Gretz, and Annabelle McIver. Conditioning in probabilistic programming. Electr. Notes Theor. Comput. Sci., 319:199–216, 2015.
pdf Nils Jansen. A greedy approach for the efficient repair of stochastic models. In Frontiers of Formal Methods, volume AIB-2011-11. RWTH Aachen University, 2015.
pdf Nils Jansen. Counterexamples in Probabilistic Verification. Dissertation, RWTH Aachen University, 2015.
pdf Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, and Erika Ábrahám. Prophesy: A probabilistic parameter synthesis tool. In Proc. of CAV, volume 9206, pages 214–231, 2015.
pdf Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker. Minimal counterexamples for linear-time probabilistic verification. Theoretical Computer Science, 549:61– 100, 2014.
pdf Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, and Johann Schuster. Symbolic counterexample generation for large discrete-time Markov chains. Science of Computer Programming, 91(A):90–114, 2014.
pdf Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker. Accelerating parametric probabilistic verification. In Proc. of QEST, volume 8657 of LNCS, pages 404–420. Springer, 2014.
pdf Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, and Joost-Pieter Katoen. Fast debugging of PRISM models. In Proc. of ATVA, volume 8837 of LNCS, pages 146–162. Springer, 2014.
pdf Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, and Ralf Wimmer. Counterexample generation for discrete-time Markov models: An introductory survey. In Proc. of SFM, volume 8483 of LNCS, pages 65–121. Springer, 2014.
pdf Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, and Ralf Wimmer. Counterexample generation for discrete-time Markov models: An introductory survey. In Proc. of SFM, volume 8483 of LNCS, pages 65–121. Springer, 2014.
pdf Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker. High-level counterexamples for probabilistic automata. In Proc. of QEST, volume 8054 of LNCS, pages 18–33. Springer, 2013.
pdf Daniel Neider and Nils Jansen. Regular model checking using solver technologies and automata learning. In Proc. of NFM, volume 7871 of LNCS, pages 16–31. Springer, 2013.
pdf Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker. Minimal critical subsystems for discrete-time Markov models. In Proc. of TACAS, volume 7214 of LNCS, pages 299–314. Springer, 2012.
pdf Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker. Minimal critical subsystems as counterexamples for ω-regular DTMC properties. In Proc. of MBMV, pages 169–180. Verlag Dr. Kovac, 2012.
pdf Nils Jansen, Erika Ábrahám, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, and Bernd Becker. Symbolic counterexample generation for discrete-time Markov chains. In Proc. of FACS, volume 7684 of LNCS, pages 134–151. Springer, 2012.
pdf Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, and Bernd Becker. The COMICS tool – Computing minimal counterexamples for DTMCs. In Proc. of ATVA, volume 7561 of LNCS, pages 349–353. Springer, 2012.
pdf Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, and Bernd Becker. Hierarchical counterexamples for discrete-time Markov chains. In Proc. of ATVA, volume 6996 of LNCS, pages 443–452. Springer, 2011.
pdf Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, and Erika Ábrahám. SMT-based counterexample generation for Markov chains. In Proc. of MBMV, pages 19–28. Offis Oldenburg, 2011.
pdf Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, and Erika Ábrahám. Counterexample generation for Markov chains using SMT-based bounded model checking. In Proc. of FMOODS/FORTE, volume 6722 of LNCS, pages 75–89. Springer, 2011.
pdf Erika Ábrahám, Nadine Bergner, Philipp Brauner, Florian Corzilius, Nils Jansen, Thiemo Leon- hardt, Ulrich Loup, Johanna Nellen, and Ulrik Schroeder. On collaboratively conveying computer science to pupils. In Proc. of KOLI, pages 132–137. ACM, 2011.
pdf Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, and Bernd Becker. DTMC model checking by SCC reduction. In Proc. of QEST, pages 37–46. IEEE Computer Society, 2010.
pdf Erika Ábrahám, Philipp Brauner, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, and Ulrik Schroeder. Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik. In Proc. of DeLFI, volume 169 of LNI, pages 239–251. Gesellschaft fu ̈r Informatik, 2010.

Tools

PROPhESY

At CAV 2015, we published PROPhESY, the state-of-the-art tool for parameter synthesis for probabilistic systems. We recently extended PROPhESY by a new approach called parameter-lifting, which is described here. This largely improves the scalability of parameter synthesis for parametric DTMCs and enables a sound approach for parametric MDPs. Visit the webpage of the tool, containing a downloadable version, documentation, a video tutorial, and case studies here.

COMICS

During my PhD, I was the main developer of the COMICS tool which computes small critical subsystems as counterexamples for discrete-time Markov chains. The last version is available here and the tool is described here. Note that this tool is not maintained anymore. In case you are interested in counterexamples for probabilistic systems, please feel free to contact me.