Publications

2024

  1. Sebastian Junges et al., “Parameter synthesis for Markov models: covering the parameter space,” Formal Methods Syst. Des., no. 1, 2024.
  2. Maris Galesloot, Thiago D. Simao, Sebastian Junges, and Nils Jansen, “Factored Online Planning in Many-Agent POMDPs,” in AAAI, 2024.
    DOI: https://doi.org/10.1609/aaai.v38i16.29689 arXiv: 2312.11434 supplemental material
  3. Roman Andriushchenko, Milan Češka, Sebastian Junges, and Filip Macak, “Policies Grow on Trees: Model Checking Families of MDPs,” in ATVA, 2024. (to appear)
  4. Kazuki Watanabe, Marck van der Vegt, Sebastian Junges, and Ichiro Hasuo, “Compositional Value Iteration with Pareto Caching,” in CAV, 2024. (to appear)
    supplemental material
  5. Marnix Suilen, Marck van der Vegt, and Sebastian Junges, “A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs,” in CONCUR, 2024. (to appear)
  6. Loes Kruger, Sebastian Junges, and Jurriaan Rot, “State Matching and Multiple References in Adaptive Active Automata Learning,” in FM, 2024. (to appear)
  7. Eline Bovy, Marnix Suilen, Sebastian Junges, and Nils Jansen, “Imprecise Probabilities Meet Partial Observability: Game Semantics for Robust POMDPs,” in IJCAI, 2024. (to appear)
  8. Wietze Koops, Sebastian Junges, and Nils Jansen, “Approximate Dec-POMDP Solving Using Multi-Agent A*,” in IJCAI, 2024. (to appear)
  9. Loes Kruger, Sebastian Junges, and Jurriaan Rot, “Small Test Suites for Active Automata Learning,” in TACAS, 2024.
    DOI: 10.1007/978-3-031-57249-4_6 arXiv: 2401.12703 supplemental material
  10. Thom S. Badings, Matthias Volk, Sebastian Junges, Mariëlle Stoelinga, and Nils Jansen, “CTMCs with Imprecisely Timed Observations,” in TACAS, 2024.
    DOI: 10.1007/978-3-031-57249-4_13 arXiv: 2401.06574 supplemental material
  11. Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot, and Sebastian Junges, “Pareto Curves for Compositionally Model Checking String Diagrams of MDPs,” in TACAS, 2024.
    DOI: 10.1007/978-3-031-57249-4_14 arXiv: 2401.08377 supplemental material

2023

  1. Steven Carr, Nils Jansen, Sebastian Junges, and Ufuk Topcu, “Safe Reinforcement Learning via Shielding for POMDPs,” in AAAI, 2023.
    DOI: 10.1609/AAAI.V37I12.26723 arXiv: 2204.00755 supplemental material
  2. Thom Badings, Sebastian Junges, Ahmadreza Marandi, Ufuk Topcu, and Nils Jansen, “Efficient Sensitivity Analysis for Parametric Robust Markov Chains,” in CAV, 2023.
    DOI: 10.1007/978-3-031-37709-9_4 arXiv: 2305.01473 supplemental material
  3. Roman Andriushchenko, Alexander Bork, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, and Filip Macak, “Search and Explore: Symbiotic Policy Synthesis in POMDPs,” in CAV, 2023.
    DOI: 10.1007/978-3-031-37709-9_6 arXiv: 2305.1414 supplemental material
  4. Wietze Koops, Sebastian Junges, Nils Jansen, and Thiago Simao, “Recursive Small-Step Multi-Agent A* for Dec-POMDPs,” in IJCAI, 2023.
    DOI: 10.24963/IJCAI.2023/600 supplemental material
  5. Arnd Hartmanns, Sebastian Junges, Tim Quatmann, and Maximilian Weininger, “A Practitioner’s Guide to MDP Model Checking Algorithms,” in TACAS, 2023.
    DOI: 10.1007/978-3-031-30823-9_24 arXiv: 2301.10197 supplemental material
  6. Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja, “Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants,” in TACAS, 2023.
    DOI: 10.1007/978-3-031-30820-8_25 supplemental material repo
  7. Marck van der Vegt, Nils Jansen, and Sebastian Junges, “Robust Almost-Sure Reachability in Multi-Environment MDPs,” in TACAS, 2023.
    DOI: 10.1007/978-3-031-30823-9_26

2022

  1. Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk, “The Probabilistic Model Checker Storm,” STTT, 2022.
    DOI: 10.1007/s10009-021-00633-z arXiv: 2002.07080 supplemental material further information
  2. Thom Badings, Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu, “Scenario-Based Verification of Uncertain Parametric MDPs,” STTT, 2022.
    DOI: 10.1007/s10009-022-00673-z arXiv: 2112.13020 supplemental material
  3. Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu, “Convex Optimization for Parameter Synthesis in MDPs,” IEEE Trans. Autom. Control., 2022.
    DOI: 10.1109/TAC.2021.3133265 arXiv: 2107.00108 supplemental material
  4. Sebastian Junges and Jurriaan Rot, “Learning Language Intersections,” in A Journey from Process Algebra via Timed Automata to Model Learning, 2022.
    DOI: 10.1007/978-3-031-15629-8_20 supplemental material repo
  5. Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen, “Parameter Synthesis in Markov Models: A Gentle Survey,” in Principles of Systems Design, 2022.
    DOI: 10.1007/978-3-031-22337-2_20 arXiv: https://doi.org/10.48550/arXiv.2207.06801
  6. Hazem Torfah, Carol Xie, Sebastian Junges, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia, “Learning Monitorable Operational Design Domains for Assured Autonomy,” in ATVA, 2022.
    DOI: 10.1007/978-3-031-19992-9_1
  7. Sebastian Junges and Matthijs T. J. Spaan, “Abstraction-Refinement for Hierarchical Probabilistic Models,” in CAV, 2022.
    DOI: 10.1007/978-3-031-13185-1_6 arXiv: 2206.02653 supplemental material repo
  8. Thom Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga, and Matthias Volk, “Sampling-Based Verification of CTMCs with Uncertain Rates,” in CAV, 2022.
    DOI: 10.1007/978-3-031-13188-2_2 arXiv: 2205.08300 supplemental material repo
  9. Edward Kim, Jay Shenoy, Sebastian Junges, Daniel J. Fremont, Alberto L. Sangiovanni-Vincentelli, and Sanjit Seshia, “Querying Labelled Data with Scenario Programs for Sim-to-Real Validation,” in ICCPS, 2022.
    DOI: 10.1109/ICCPS54341.2022.00010 arXiv: 2112.00206
  10. Dennis Gross, Nils Jansen, Sebastian Junges, and Guillermo A. Pérez, “COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking,” in SETTA, 2022.
    DOI: 10.1007/978-3-031-21213-0_3 arXiv: 2209.07133 supplemental material
  11. Roman Andriushchenko, Milan Češka, Sebastian Junges, and Joost-Pieter Katoen, “Inductive Synthesis of Finite-State Controllers for POMDPs,” in UAI, 2022.
    URL: https://proceedings.mlr.press/v180/andriushchenko22a.html arXiv: 2203.10803 supplemental material repo
  12. Jip Spel, Linus Heck, Sebastian Junges, Joost-Pieter Katoen, and Joshua Moerman, “Gradient-Descent for Randomized Controllers under Partial Observability,” in VMCAI, 2022.
    DOI: 10.1007/978-3-030-94583-1_7 arXiv: abs/2111.04407 supplemental material

2021

  1. Milan Češka, Christian Hensel, Sebastian Junges, and Joost-Pieter Katoen, “Counterexample-guided Inductive Synthesis for Probabilistic Systems,” Formal Asp. Comput., 2021.
    DOI: 10.1007/s00165-021-00547-2 repo
  2. Tim Quatmann, Sebastian Junges, and Joost-Pieter Katoen, “Markov Automata with Multiple Objectives,” FMSD, 2021.
    DOI: 10.1007/s10703-021-00364-6 supplemental material
  3. Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, and Tobias Winkler, “The complexity of reachability in parametric Markov decision processes,” J. Comput. Syst. Sci., 2021.
    DOI: 10.1016/j.jcss.2021.02.006 arXiv: 2009.13128
  4. Leonore Winterer et al., “Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions,” IEEE Trans. Autom. Control., no. 3, 2021.
    DOI: 10.1109/TAC.2020.2990140
  5. Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen, and Ufuk Topcu, “Robust Finite-State Controllers for Uncertain POMDPs,” in AAAI, 2021.
    DOI: https://doi.org/10.1609/aaai.v35i13.17401
  6. Roman Andriushchenko, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, and Simon Stupinsky, “PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs,” in CAV, 2021.
    DOI: 10.1007/978-3-030-81685-8_40 supplemental material repo
  7. Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd Millstein, Sanjit A. Seshia, and Guy Van den Broeck, “Model Checking Finite-Horizon Markov Chains with Probabilistic Inference,” in CAV, 2021.
    DOI: 10.1007/978-3-030-81688-9_27 supplemental material repo
  8. Sebastian Junges, Nils Jansen, and Sanjit A. Seshia, “Enforcing Almost-Sure Reachability in POMDPs,” in CAV, 2021.
    DOI: 10.1007/978-3-030-81688-9_28 arXiv: 2007.00085 supplemental material
  9. Sebastian Junges, Hazem Torfah, and Sanjit A. Seshia, “Runtime Monitors for Markov Decision Processes,” in CAV, 2021.
    DOI: 10.1007/978-3-030-81688-9_26 supplemental material repo
  10. Marcell Vazquez-Chanlatte, Sebastian Junges, Daniel J. Fremont, and Sanjit Seshia, “Entropy-Guided Control Improvisation,” in RSS, 2021.
    DOI: 10.15607/RSS.2021.XVII.051 arXiv: 2103.05672 repo
  11. Hazem Torfah, Sebastian Junges, Daniel Fremont, and Sanjit A. Seshia, “Formal Analysis of AI-Based Autonomy: From Modeling to Runtime Assurance,” in RV, 2021.
    DOI: 10.1007/978-3-030-88494-9_19
  12. Jip Spel, Sebastian Junges, and Joost-Pieter Katoen, “Finding Provably Optimal Markov Chains,” in TACAS, 2021.
    DOI: 10.1007/978-3-030-72016-2_10
  13. Roman Andriushchenko, Milan Češka, Sebastian Junges, and Joost-Pieter Katoen, “Inductive Synthesis for Probabilistic Programs Reaches New Horizons,” in TACAS, 2021.
    DOI: 10.1007/978-3-030-72016-2_11 supplemental material

2020

  1. Sebastian Junges, “Parameter synthesis in Markov models,” PhD thesis, RWTH Aachen University, Germany, 2020.
  2. Christel Baier, Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, and Joachim Klein, “Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination,” Inf. Comput., 2020.
  3. Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann, “Multi-cost Bounded Tradeoff Analysis in MDP,” J. Autom. Reason., no. 7, 2020.
    DOI: 10.1007/s10817-020-09574-9 supplemental material
  4. Alexander Bork, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann, “Verification of Indefinite-Horizon POMDPs,” in ATVA, 2020.
    DOI: 10.1007/978-3-030-59152-6_16 arXiv: 2007.00102 supplemental material
  5. Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer, “PrIC3: Property Directed Reachability for MDPs,” in CAV, 2020.
    DOI: 10.1007/978-3-030-53291-8_27 repo
  6. Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, and Roderick Bloem, “Safe Reinforcement Learning Using Probabilistic Shields,” in CONCUR, 2020.
  7. Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu, “Scenario-Based Verification of Uncertain MDPs,” in TACAS, 2020.
    DOI: doi.org/10.1007/978-3-030-45190-5_16

2019

  1. Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, and Matthias Volk, “Safety analysis for vehicle guidance systems with dynamic fault trees,” Rel. Eng. and Sys. Safety, 2019.
    DOI: 10.1016/j.ress.2019.02.005 arXiv: 1903.05361 further information
  2. Jip Spel, Sebastian Junges, and Joost-Pieter Katoen, “Are Parametric Markov Chains Monotonic?,” in ATVA, 2019.
    DOI: 10.1007/978-3-030-31784-3_28 supplemental material
  3. Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, and Joost-Pieter Katoen, “On the Complexity of Reachability in Parametric Markov Decision Processes,” in CONCUR, 2019.
    DOI: 10.4230/LIPIcs.CONCUR.2019.14
  4. Milan Češka, Christian Hensel, Sebastian Junges, and Joost-Pieter Katoen, “Counterexample-Driven Synthesis for Probabilistic Program Sketches,” in FM, 2019.
    DOI: 10.1007/978-3-030-30942-8_8 repo
  5. Milan Češka, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen, “Shepherding Hordes of Markov Chains,” in TACAS, 2019.
    DOI: 10.1007/978-3-030-17465-1_10 repo
  6. Milan Češka, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen, “Model Repair Revamped - - On the Automated Synthesis of Markov Chains -,” in From Reactive Systems to Cyber-Physical Systems, 2019.
    repo

2018

  1. Matthias Volk, Sebastian Junges, and Joost-Pieter Katoen, “Fast Dynamic Fault Tree Analysis by Model Checking Techniques,” IEEE Trans. Industrial Informatics, no. 1, 2018.
  2. Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu, “Synthesis in pMDPs: A Tale of 1001 Parameters,” in ATVA, 2018.
  3. Sebastian Junges, Joost-Pieter Katoen, Mariëlle Stoelinga, and Matthias Volk, “One Net Fits All - A Unifying Semantics of Dynamic Fault Trees Using GSPNs,” in Petri Nets, 2018.
  4. Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, and Mary M. Hayhoe, “Model Checking for Safe Navigation Among Humans,” in QEST, 2018.
  5. Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann, “Multi-cost Bounded Reachability in MDP,” in TACAS, 2018.
  6. Sebastian Junges et al., “Finite-State Controllers of POMDPs using Parameter Synthesis,” in UAI, 2018.
    URL: http://auai.org/uai2018/proceedings/papers/195.pdf

2017

  1. Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, and Mariëlle Stoelinga, “Fault trees on a diet: automated reduction by graph rewriting,” Formal Asp. Comput., no. 4, 2017.
  2. Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk, “A storm is Coming: A Modern Probabilistic Model Checker,” in CAV, 2017.
    DOI: 10.1007/978-3-319-63390-9_31
  3. Tim Quatmann, Sebastian Junges, and Joost-Pieter Katoen, “Markov Automata with Multiple Objectives,” in CAV, 2017.
    DOI: 10.1007/978-3-319-63387-9_7 arXiv: 1704.06648
  4. Leonore Winterer et al., “Motion planning under partial observability using game-based abstraction,” in CDC, 2017.
  5. Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, and Matthias Volk, “Model-Based Safety Analysis for Vehicle Guidance Systems,” in SAFECOMP, 2017.
  6. Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini, “JANI: Quantitative Model and Tool Interaction,” in TACAS, 2017.
  7. Murat Cubuktepe et al., “Sequential Convex Programming for the Efficient Verification of Parametric MDPs,” in TACAS, 2017.

2016

  1. Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen, “Parameter Synthesis for Markov Models: Faster Than Ever,” in ATVA, 2016.
  2. Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, and Mariëlle Stoelinga, “Uncovering Dynamic Fault Trees,” in DSN, 2016.
  3. Christian Dehnert et al., “Parameter Synthesis for Probabilistic Systems,” in MBMV, 2016.
  4. Matthias Volk, Sebastian Junges, and Joost-Pieter Katoen, “Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates,” in SAFECOMP, 2016.
  5. Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, and James Gross, “Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks,” in SRDS, 2016.
  6. Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, and Joost-Pieter Katoen, “Safety-Constrained Reinforcement Learning for MDPs,” in TACAS, 2016.
  7. Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, and Ufuk Topcu, “Probabilistic Verification for Cognitive Models,” 2016, no. FS-16.

2015

  1. Christian Dehnert et al., “PROPhESY: A PRObabilistic ParamEter SYnthesis Tool,” in CAV, 2015.
  2. Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, and Erika Ábrahám, “SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving,” in SAT, 2015.
  3. Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, and Mariëlle Stoelinga, “Fault Trees on a Diet - - Automated Reduction by Graph Rewriting -,” in SETTA, 2015.

2014

  1. Dimitri Bohlender, Harold Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, and Thomas Noll, “A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models,” in ISoLA, 2014.

2013

  1. Sebastian Junges, Ulrich Loup, Florian Corzilius, and Erika Ábrahám, “On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers,” in CAI, 2013.

2012

  1. Florian Corzilius, Ulrich Loup, Sebastian Junges, and Erika Ábrahám, “SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox - (Tool Presentation),” in SAT, 2012.