Publications of Nils Jansen

2019
Milan Ceska, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Shepherding Hordes of Markov Chains. Proc. of TACAS, Volume of LNCS, , 2019.
2018
DOIMurat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Synthesis in pMDPs: A Tale of 1001 Parameters. Proc. of ATVA, Volume 11138 of LNCS, pages 160-176, Springer, 2018.
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, Mary Hayhoe. Model Checking For Safe Navigation Among Humans. Proc. of QEST, Volume of LNCS, , 2018.
LinkSebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs via Parameter Synthesis. Proc. of UAI, AUAI, 2018.
DOIFederico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver. Conditioning in Probabilistic Programming. ACM Transactions on Programming Languages and Systems (TOPLAS) 40(1), pages 4:1-4:50, 2018.
2017
DOIDownloadLinkLeonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker. Motion Planning under Partial Observability using Game-Based Abstraction. IEEE 56th Annual Conference on Decision and Control (CDC), pages 2201-2208, IEEE, 2017.
DOILinkMurat 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. Proc. of TACAS, Volume 10206 of LNCS, pages 133-150, Springer, 2017.
DOIRadu Calinescu, Marco Autili, Javier Ciamara, Antinisca Di Marco, Simos Gerasimou, Paola Inverardi, Alexander Perucci, Nils Jansen, Joost-Pieter Katoen, Marta Kwiatkowska, Ole J. Mengshoel, Romina Spalazzese, Massimo Tivoli. Synthesis and Verification of Self-aware Computing Systems. In , Self-Aware Computing Systems, pages 337-373, 2017.
2016
DOIDownloadLinkNils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen. Bounded Model Checking for Probabilistic Programs. Proc. of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, Springer, 2016.
DOITim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever. Proc. of ATVA, Volume 9938 of LNCS, pages 50–67, Springer, 2016.
LinkSebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu. Probabilistic Verification for Cognitive Models. Proc. of Cross-Disciplinary Challenges for Autonomous Systems (CDCAS), Volume of AAAI Technical Reports, AAAI Press, 2016.
DOISebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs. Proc. of TACAS, Volume 9636 of LNCS, pages 130-146, Springer, 2016.
Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo. On the Semantic Intricacies of Conditioning. Collected Abstracts of the 1st Workshop on Probabilistic Programming Semantics (PPS 2016), 2016.
DOIChristian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Joost-Pieter Katoen, Erika Abraham, Harold Bruintjes. Parameter Synthesis for Probabilistic Systems. Proc. of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'16), pages 72-74, Albert-Ludwigs-Universität Freiburg, 2016.
DOIFrancesco Leofante, Simone Vuotto, Erika Abraham, Armando Tacchella, Nils Jansen. Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, Part I, Volume 9952 of LNCS, pages 496-514, Springer International Publishing, 2016.
2015
DownloadLinkNils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Probabilistic Programs - A Natural Model for Approximate Computations. Workshop on Approximate Computing (AC15), 2015.
DOIJoost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Federico Olmedo. Understanding Probabilistic Programs. 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.
DOIDownloadLinkChristian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, Erika Abraham. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. Proc. of the 27th Int. Conf. on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, pages 214–231, Springer, 2015.
DOIDownloadLinkTim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards. Proc. of the 20th Int. Symp. on Formal Methods (FM'15), Volume 9109 of LNCS, pages 435–452, Springer, 2015.
DOILinkLinkShashank Pathak, Erika Abraham, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen. A Greedy Approach for the Efficient Repair of Stochastic Models. Proc. of the 7th NASA Formal Methods Symp. (NFM'15), Volume 9058 of LNCS, pages 295–309, Springer, 2015.
DOIDownloadLinkRalf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen. High-level Counterexamples for Probabilistic Automata. Logical Methods in Computer Science (LMCS) 11(1:15), pages 1–23, 2015.
DownloadLinkNils Jansen. Counterexamples in Probabilistic Verification. Phd Thesis at RWTH Aachen University, 2015.
DOIDownloadLinkNils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo, Friedrich Gretz, Annabelle McIver. Conditioning in Probabilistic Programming. Proc. of the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS 2015), ENTCS 319, pages 199-216, 2015.
2014
DownloadLinkErika Abraham, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer. Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey. Proc. of the 14th Int. School on Formal Methods for the Design of Computer, Communication and Software Systems: Executable Software Models (SFM-14:ESM), Volume 8483 of LNCS, pages 65–121, Springer, 2014.
DOIDownloadLinkNils Jansen, Ralf Wimmer, Erika Abraham, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster. Symbolic Counterexample Generation for Large Discrete-Time Markov Chains. Science of Computer Programming 91 (Part A), pages 90–114, 2014.
DOIDownloadLinkNils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification. 11th Int. Conf. on Quantitative Evaluation of Systems (QEST'14), Volume 8657 of LNCS, pages 404–420, Springer, 2014.
DOIRalf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Minimal Counterexamples for Linear-Time Probabilistic Verification. Theoretical Computer Science 549, pages 61–100, 2014.
DownloadLinkChristian Dehnert, Nils Jansen, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen. Fast Debugging of PRISM Models. Int. Symp. on Automated Technology for Verification and Analysis (ATVA'14), Volume 8837 of LNCS, pages 146–162, Springer, 2014.
2013
DownloadLinkNils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification. Technical report at Cornell University number arXiv:1312.3979, 2013.
DOIDownloadLinkRalf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata. Proc. of the 10th Int. Conf. on Quantitative Evaluation of Systems (QEST'13), Volume 8054 of LNCS, pages 39–54, Springer-Verlag, 2013.
DOIDownloadLinkDaniel Neider, Nils Jansen. Regular Model Checking Using Solver Technologies and Automata Learning. 5th NASA Formal Methods Symposium (NFM'13), Volume 7871 of LNCS, pages 16–31, Springer Berlin Heidelberg, 2013.
DownloadLinkRalf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata. Technical report at Cornell University number arXiv:1305.5055, 2013.
2012
DOIDownloadLinkNils Jansen, Erika Abraham, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. The COMICS Tool - Computing Minimal Counterexamples for DTMCs. Proc. of the 10th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'12), Volume 7561 of LNCS, pages 349–353, Springer Berlin Heidelberg, 2012.
DOIDownloadLinkNils Jansen, Erika Abraham, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker. Symbolic Counterexample Generation for Discrete-time Markov Chains. 9th Int. Symp. on Formal Aspects of Component Software (FACS'12), Volume 7684 of LNCS, pages 134–151, Springer Berlin Heidelberg, 2012.
DownloadLinkRalf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes. Technical report at Reports of SFB/TR 14 AVACS number 88, 2012.
DownloadLinkNils Jansen, Erika Abraham, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. The COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains. Technical report at Cornell University number arXiv:1206.0603v1, 2012.
DOIDownloadLinkRalf Wimmer, Nils Jansen, Erika Abraham, Bernd Becker, Joost-Pieter Katoen. Minimal Critical Subsystems for Discrete-Time Markov Models. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), Volume 7214 of LNCS, pages 299–314, Springer Berlin Heidelberg, 2012.
DownloadLinkRalf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties. Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'12), pages 169–180, Verlag Dr. Kovac, 2012.
2011
DOIDownloadLinkErika Abraham, Nadine Bergner, Philipp Brauner, Florian Corzilius, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Johanna Nellen, Ulrik Schroeder. On Collaboratively Conveying Computer Science to Pupils. Proc. of the 11th Koli Calling Int. Conf. on Computing Education Research (KOLI'11), pages 132–137, ACM, 2011.
DOIDownloadLinkNils Jansen, Erika Abraham, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. Hierarchical Counterexamples for Discrete-Time Markov Chains. 9th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'11), Volume 6996 of LNCS, pages 443–452, Springer Berlin Heidelberg, 2011.
DOIDownloadLinkBettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham. Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking. Formal Techniques for Distributed Systems (FMOODS/FORTE'11), Volume 6722 of LNCS, pages 75–89, Springer Berlin Heidelberg, 2011.
DownloadLinkNils Jansen, Erika Abraham, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. Hierarchical Counterexamples for Discrete-Time Markov Chains. Technical report at RWTH Aachen University number AIB-2011-11, 2011.
DownloadLinkBettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham. SMT-based Counterexample Generation for Markov Chains. Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'11), pages 19–28, OFFIS-Institut für Informatik, 2011.
DownloadLinkBettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham. SMT-based Counterexample Generation for Discrete-Time Markov Chains. Workshop on Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems (ROCKS'11), , 2011.
2010
DOIDownloadLinkErika Abraham, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. DTMC Model Checking by SCC Reduction. 7th Int. Conf. on Quantitative Evaluation of Systems (QEST'10), pages 37–46, IEEE, 2010.
DownloadLinkErika Abraham, Philipp Brauner, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Ulrik Schroeder. Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik. Interaktive Kulturen - Die 8. E-Learning Fachtagung Informatik (DeLFI'10), Volume 169 of LNI, pages 239–251, Gesellschaft für Informatik, 2010.