I have a new webpage.

I am associate professor with the Department of Software Science (SWS) at Radboud University Nijmegen in the Netherlands. I'm a member of the ELLIS society.

My group conducts broad foundational and application-driven research in artificial intelligence (AI). We take a broad stance on AI that brings together the areas of machine learning and formal methods, in particular formal verification. We tackle problems that are inspired by autonomous systems, industrial projects, and in particular planning problems in robotics. We use methods that span deep machine learning (ML) techniques using recurrent or graph neural networks or problems captured by partially observable Markov decision processes (POMDPs) in a data-driven context. The following goals are central to our efforts:

  • Increase the dependability of AI in safety-critical environments.
  • Render AI models robust against uncertain knowledge about the environment they operate in.
  • Enhance the capabilities of verification to handle real-world problems using learning techniques.
    •

In particular, we are interested in various aspects of Dependability and Safety in Artificial Intelligence, Intelligent Decision-making under Uncertainty and Safe Reinforcement Learning. A key aspect of our research is a thorough understanding of the (epistemic or aleatoric) uncertainty that may occur when AI systems operate in the real world.

Concrete Topics (also) include the following. Happy to talk, if you are interested!

  • Learning and synthesis for partially observable probabilistic systems, like POMDPs
  • Neural network robustness
  • Semantics and verification of probabilistic programs
  • Approximate hard- and software-systems
Please feel free to contact me at any time via email: n.jansen 'at' science.ru 'dot' nl. For further contact options, see here.

News

November 9, 2022Our paper Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions has been accepted for the Journal of Artificial Intelligence Research (JAIR). The publication will be part of a JAIR special issue dedicated to award winning AI papers and is a thorough extension of the distinguished AAAI paper. Congrats Thom!
September 17, 2022Our paper Robust Anytime Learning of Markov Decision Processes has been accepted at NeurIPS 2022. The work is a collaboration with David Parker from the University of Oxford. Congratulations, Marnix and Thiago!
September 13, 2022Our paper COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking has been accepted for publication at SETTA 2022. Congratulations, Dennis!
June 10, 2022The Lorentz center workshop Rigorous Automated Planning was a great success. We had guests from all over the world with expertise in AI, Planning, Robotics, and Formal Methods, and we identified a large number of challenges and synergies for bringing these areas closer together. I co-organized this event together with Jana Tumova, Alessandro Abate, Matthijs Spaan, and Ufuk Topcu.
May 15, 2022Our paper Sampling-Based Verification of CTMCs with Uncertain Rates has been accepted CAV 2022. The paper is the first to provide a method for statistically correct verification of continuous-time Markov chains with unknown transition rates. Congratulations Thom!
May 11, 2022Our paper Scenario-Based Verification of Uncertain Parametric MDPs has been accepted in the International Journal on Software Tools for Technology Transfer (STTT, special issue devoted to TACAS 2020). The paper uses the sampling-based scenario approach to obtain high-confidence guarantees for uncertain MDPs. Congratulations Thom!
Feb 25, 2022We received the great news that our paper Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise has won a distinguished paper award at AAAI 2022. The conference received 9251 submissions, of which 1349 were accepted for publication in the first place. Special congratulations to my PhD student Thom Badings!
Feb 10, 2022The aforementioned paper Grouping of Maintenance Actions with Deep Reinforcement Learning and Graph Convolutional Networks has won the best student paper award at ICAART 2022. Congratulations for this great success, David!
Dec 7, 2021Our paper Grouping of Maintenance Actions with Deep Reinforcement Learning and Graph Convolutional Networks, with our Master student David Kerkkamp as first author, has been accepted for ICAART 2022. The paper is based on David's Master thesis at Rolsch Assetmanagement within the PrimaVera project, and investigates the utility of graph neural networks in a setting that concerns predictive maintenance of sewer pipe networks. Congrats David and Zaharah!
Dec 1, 2021Our paper Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise has been accepted for AAAI 2022. Congrats Thom!
Nov 19, 2021Our paper Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes got published at the Journal of Artificial Intelligence Research (JAIR). The work subsumes and extends previous papers on combining the training of recurrent neural networks as policy representation for POMDPs with the rigor of formal verification. Congrats Steve!
Nov 8, 2021Our paper Convex Optimization for Parameter Synthesis in MDPs has been accepted for publication in IEEE Transactions on Automatic Control. The paper subsumes and extends a successful line of work that employs convex optimization techniques for the efficient parameter synthesis in Markov decision processes.
Sep 15, 2021The paper Formalizing and guaranteeing human-robot interaction has been published at Communications of the ACM. This paper provides an overview to challenges in Human-Robot-Interaction regarding trust and safety, and how formal methods can help. This collaborative paper is a result of the very fruitful Dagstuhl Meeting Verification and Synthesis of Human-Robot Interaction
July 15, 2021Our paper Damage detection using in-domain and cross-domain transfer learning has been accepted for publication at the journal Neural Computing and Applications. Congrats Zaharah!
June 09, 2021Our paper Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes has been accepted for publication at the Journal of Artificial Intelligence Research (JAIR). Congrats Steve!
May 11, 2021Our paper Safe Policies for Factored Partially Observable Stochastic Games has been accepted for publication at RSS 2021. Congrats Steve!
Apr 18, 2021Our paper Enforcing Almost-Sure Reachability in POMDPs has been accepted for publication at CAV 2021.
Mar 25, 2021Our paper Deep reinforcement learning for rehabilitation planning of water pipes network has been accepted for at Adaptive and Learning Agents (ALA) 2021, co-located with AAMAS.
Feb 22, 2021Our paper Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids has been accepted for publication at NFM 2021. Congrats Thom and Marnix!
Feb 19, 2021I just received the happy news that I got early tenure.
Feb 2, 2021The press widely covers our work on AI uncertainty, see for example CACM, Innovation Origins, Computable, Bits & Chips, Engineers Forum, and Executive-People.
Jan 25, 2021Radboud University published a press release about our work on uncertainty in AI, and in particular our AAAI and IJCAI papers on uncertain POMDPs. Check it out here.
Jan 24, 2021Our paper Adaptive Shielding under Uncertainty has been accepted for publication at ACC 2021.
Dec 17, 2020Our paper AlwaysSafe: Reinforcement Learning without Safety Constraint Violations during Training has been accepted for publication at AAMAS 2021.
Older news hidden.

Publications

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

Published or accepted for publication:

Marnix Suilen, Thiago D. Simão, David Parker, Nils Jansen. Robust Anytime Learning of Markov Decision Processes. In NeurIPS, 2022.
Dennis Gross, Nils Jansen, Sebastian Junges, Guillermo Perez. COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking. In SETTA, 2022.
Thom S. Badings, Nils Jansen, Sebastian Junges, Mariëlle Stoelinga, Matthias Volk. Sampling-Based Verification of CTMCs with Uncertain Rates. In CAV, 2022.
Thom S. Badings, Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Scenario-Based Verification of Uncertain Parametric MDPs. In STTT, 2022.
Thom S. Badings, Alessandro Abate, Nils Jansen, David Parker, Hasan A. Poonawala, Marielle Stoelinga. Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise. In AAAI 2022.
David Kerkkamp, Zaharah A. Bukhsh, Yingqian Zhang and Nils Jansen. Grouping of Maintenance Actions with Deep Reinforcement Learning and Graph Convolutional Networks. In ICAART 2022.
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Convex Optimization for Parameter Synthesis in MDPs. In Transactions on Automatic Control 2021.
Zaharah Allah Bukhsh, Nils Jansen, Aaqib Saeed. In-domain and Cross-domain Transferability for Damage Detection in Structural Health Monitoring. Neural Computing and Applications, 2021, to appear
Steven Carr, Nils Jansen, Suda Bharadwaj, Matthijs Spaan, Ufuk Topcu. Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes. In Journal of Artificial Intelligence Research (JAIR) , 2021, to appear.
Steven Carr, Nils Jansen, Suda Bharadwaj, Matthijs Spaan, Ufuk Topcu. Safe Policies for Factored Partially Observable Stochastic Games. In RSS 2021, to appear.
Sebastian Junges, Nils Jansen, Sanjit A. Seshia. Enforcing Almost-Sure Reachability in POMDPs. In CAV 2021, to appear.
Zaharah A. Bukhsh, Nils Jansen and Hajo Molegraaf. Deep reinforcement learning for rehabilitation planning of water pipes network. In Adaptive and Learning Agents 2021, co-located with AAMAS.
Thom S. Badings, Arnd Hartmanns, Nils Jansen and Marnix Suilen. Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids. In NFM 2021, to appear.
Stefan Pranger, Bettina Koenighofer, Martin Tappler, Martin Deixelberger, Nils Jansen, Roderick Bloem. Adaptive Shielding under Uncertainty. In ACC 2021, to appear.
Thiago D. Simão, Matthijs T. J. Spaan, Nils Jansen. AlwaysSafe: Reinforcement Learning without Safety Constraint Violations during Training. In AAMAS 2021, to appear.
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen, Ufuk Topcu. Robust Finite-State Controllers for Uncertain POMDPs. In AAAI 2021, to appear.
Hadas Kress-Gazit, Kerstin Eder, Guy Hoffman, Henny Admoni, Brenna Argall, Rüdiger Ehlers, Christoffer Heckman, Nils Jansen, Ross Knepper, Jan Kretínský, Shelly Levy-Tzedek, Jamy Li, Todd Murphey, Laurel D. Riek, Dorsa Sadigh. Formalizing and Guaranteeing* Human-Robot Interaction. In Communications of the ACM, 2020, to appear.
Mohamadreza Ahmadi, Nils Jansen, Bo Wu, Ufuk Topcu. Control Theory Meets POMDPs: A Hybrid Systems Approach. In Transactions on Automatic Control, 2020, to appear.
pdf Murat Cubuktepe, Nils Jansen, Mohammed Alshiekh, Ufuk Topcu. Synthesis of Provably Correct Autonomy Protocols for Shared Control. In Transactions on Automatic Control, 2020, to appear.
pdf Nils Jansen, Sebastian Junges, Bettina Koenighofer, Alex Serban, Roderick Bloem. Safe Reinforcement Learning using Probabilistic Shields. In CONCUR, pages 3:1--3:16, 2020.
Bettina Koenighofer, Florian Lorber, Nils Jansen, Roderick Bloem Roderick Bloem. Shield Synthesis for Reinforcement Learning. In ISoLA, pages 290--306, 2020.
pdf Dennis Gross, Nils Jansen, Guillermo Perez and Stephan Raaijmakers. Robustness Verification for Classifier Ensembles. In ATVA, pages 271-287, 2020.
pdf Marnix Suilen, Nils Jansen, Murat Cubuktepe, Ufuk Topcu. Robust Policy Synthesis for Uncertain POMDPs via Convex Optimization. In IJCAI, pages 4113-4120, 2020.
pdf Steven Carr, Nils Jansen, Ufuk Topcu. Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints. In IJCAI, pages 4121-4127, 2020.
pdf Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker. Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions. In Transactions on Automatic Control, 2020, to appear.
pdf Leonore Winterer, Ralf Wimmer, Nils Jansen, Bernd Becker. Strengthening Deterministic Policies for POMDPs. In NFM, pages 115-132 2020.
Dung Phan, Radu Grosu, Nils Jansen, Nicola Paoletti, Scott Smolka, Scott Stoller. Neural Simplex Architecture. In NFM, pages 97-114, 2020.
pdfMurat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu . Scenario-Based Verification of Uncertain MDPs. In TACAS, pages 287-305, 2020.
pdf Steven Carr, Nils Jansen, Ralf Wimmer, Alexandru C. Serban, Bernd Becker, Ufuk Topcu. Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks. In IJCAI 2019, pages 5532-5539.
Milan Ceska, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Model Repair Revamped - On the Automated Synthesis of Markov Chains. In From Reactive Systems to Cyber-Physical Systems, 2019.
pdf Nils Jansen, Laura Humphrey, Jana Tumova, Ufuk Topcu. Structured Synthesis for Probabilistic Systems. In NFM, pages 237-254, 2019.
pdf Milan Ceska, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Shepherding Hordes of Markov Chains. In TACAS, pages 172-190, 2019.
Mohamadreza Ahmadi, Murat Cubuktepe, Nils Jansen, Ufuk Topcu. Verification of Uncertain POMDPs Using Barrier Certificates. In 56th Annual Allerton Conference on Communication, Control, and Computing, pages 115-122, 2018.
pdf Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Synthesis in pMDPs: A Tale of 1001 Parameters. In ATVA, pages 160--176, 2018.
pdf> Sebastian Junges, Nils Jansen, Ruohan Zhang, Joost-Pieter Katoen, Ufuk Topcu, Mary Hayhoe. Model Checking For Safe Navigation Among Humans. In QEST, pages 207--222, 2018.
pdf Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-state Controllers of POMDPs via Parameter Synthesis. In Conference on Uncertainty in Artificial Intelligence (UAI), pages 519-529, 2018.
pdf Steven Carr, Nils Jansen, Ralf Wimmer, Jie Fu, Ufuk Topcu. Human-in-the-Loop Synthesis of Partially Observable Markov Decision Processes. In the American Control Conference, pages 762--769, 2018.
pdf Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver. Conditioning in Probabilistic Programming. In ACM Transactions on Programming Languages and Systems (TOPLAS) 40(1), 4:1-4:50, 2018.
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 IEEE Conference on Decision and Control (CDC), pages 2201-2208, 2017.
pdf Nils Jansen, Murat Cubuktepe, Ufuk Topcu. Synthesis of Shared Control Protocols with Provable Safety and Performance Guarantees. In 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 DeLFI, volume 169 of LNI, pages 239–251. Gesellschaft fu ̈r Informatik, 2010.

Selected Talks

For some of the talks the slides are available. For the others, please contact me.

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.

Current Team

PhD

Postdoc

Former Members

Master

Bachelor

Teaching

Lectures

Bachelor / Master Thesis

I offer several thesis projects for topics concerning verification and machine learning, parameter synthesis, uncertain probabilistic systems, and probabilistic programming. Some topics are listed on the institute webpage, for a full overview just contact me.

Finished Projects:

  • Applying Machine Learning to create Control Software for a Model Factory (Reinier Josse, with ICT Group)
  • Routing Algorithms for Autonomous Agricultural Vehicles (Laura Philipse, with PHACT Innovation Experts)
  • Learning State Representations for Formal Verification using Atari 2600 Games (David Kerkkamp)
  • Connecting Mixed-Integer Linear Programming and Finite-memory POMDP Strategies (Tom Smitjes)
  • Creating a Formal Model of the Game 2048 (Johan Sijtsma)
  • Human-in-the-loop Strategy Synthesis: PAC-MAN verified (Manuela Bergau)
  • A Comparison of Model Checking Tools for Synchronisation Problems (Sjoerd Hemels)
  • Solving reachability properties for uncertain MDPs by robust geometric programming (Marnix Suilen)
  • On-the-fly model checking for probabilistic programs
  • Counterexamples for expected rewards on discrete-time Markov chains
  • Verification and synthesis for parametric Markov chains
  • Minimal critical subsystems for probabilistic models with nondeterminism
  • Compositional counterexamples for MDPs
  • Verification and synthesis for parametric Markov chains
  • Hierarchical counterexamples for DTMCs—case studies
  • Minimal critical subsystems for PCTL properties of Markov models

Professional Activities

Funded Projects

Program Committee Member and Boards

PhD Committee Member

Grant Reviewing

Event Organization / Chair

External Reviewer (incomplete list)

    ACC, ACM Transactions on Modeling and Computer Simulation, ATVA, CAV, CDC, CONCUR, FACS, FM, FMOODS–FORTE, FORMATS, FOSSACS, FSEN, FSTTCS, FTSCS, HSCC, IFM, IJCAI, Petri Nets, QEST, SIMULTECH, Journal of Automated Reasoning, Journal of Systems and Software, International Journal of Robotics Research, TACAS, TASE, Theoretical Computer Science, IEEE Transactions of Reliability, IEEE Transactions on Automatic Control, and VMCAI

My PhD thesis concerns the automatic generation of counterexamples for probabilistic systems. A counterexample for discrete-time Markov Chains (DTMCs) is classically defined as a (finite) set of paths. In this work, this set of paths is represented symbolically as a critical part of the original system, a so-called critical subsystem. This notion is extended to Markov decision processes (MDPs) and probabilistic automata (PAs). The results are introduced in four parts:

  • A model checking algorithm for DTMCs based on a decomposition of the system's graph in strongly connected components (SCCs). This approach is extended to parametric discrete-time Markov Chains.
  • The generation of counterexamples for DTMCs and reachability properties based on graph algorithms. A hierarchical abstraction scheme to compute abstract counterexamples is presented, followed by a general framework for both explicitly represented systems and symbolically represented systems using binary decision diagrams (BDDs).
  • The computation of minimal critical subsystems using SAT modulo theories (SMT) solving and mixed integer linear programming (MILP). This is investigated for reachability properties and omega-regular properties on DTMCs, MDPs, and PAs.
  • A new concept of high-level counterexamples for PAs. Markov models can be specified by means of a probabilistic programming language. An approach for computing critical parts of such a symbolic description of a system is presented, yielding human-readable counterexamples.
A thorough evaluation on common benchmarks is given comparing all methods and also competing with available implementations of other approaches.