Publications

2022

  1. Badings, T., Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., & Topcu, U. (2022). Scenario-Based Verification of Uncertain Parametric MDPs. STTT. (to appear)
    DOI: 10.1007/s10009-022-00673-z arXiv: 2112.13020 supplemental material
  2. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., & Topcu, U. (2022). Convex Optimization for Parameter Synthesis in MDPs. IEEE Trans. Autom. Control. (to appear)
    DOI: 10.1109/TAC.2021.3133265 arXiv: 2107.00108 supplemental material
  3. Junges, S., & Rot, J. (2022). Learning Language Intersections. A Journey from Process Algebra via Timed Automata to Model Learning, LNCS 13560, pp. 371–381, Springer.
    DOI: 10.1007/978-3-031-15629-8_20 supplemental material
  4. Junges, S., & Spaan, M. T. J. (2022). Abstraction-Refinement for Hierarchical Probabilistic Models. CAV, LNCS 13371, pp. 102–123, Springer.
    DOI: 10.1007/978-3-031-13185-1_6 arXiv: 2206.02653 supplemental material
  5. Badings, T., Jansen, N., Junges, S., Stoelinga, M., & Volk, M. (2022). Sampling-Based Verification of CTMCs with Uncertain Rates. CAV, LNCS 13372, pp. 26–47, Springer.
    DOI: 10.1007/978-3-031-13188-2_2 arXiv: 2205.08300 supplemental material
  6. Kim, E., Shenoy, J., Junges, S., Fremont, D. J., Sangiovanni-Vincentelli, A. L., & Seshia, S. (2022). Querying Labelled Data with Scenario Programs for Sim-to-Real Validation. ICCPS, pp. 34–45.
    DOI: 10.1109/ICCPS54341.2022.00010 arXiv: 2112.00206
  7. Andriushchenko, R., Ceska, M., Junges, S., & Katoen, J.-P. (2022). Inductive Synthesis of Finite-State Controllers for POMDPs. UAI. (to appear)
    arXiv: 2203.10803
  8. Spel, J., Heck, L., Junges, S., Katoen, J.-P., & Moerman, J. (2022). Gradient-Descent for Randomized Controllers under Partial Observability. VMCAI, LNCS 13182, pp. 127–150.
    DOI: 10.1007/978-3-030-94583-1_7 arXiv: abs/2111.04407 supplemental material

2021

  1. Ceska, M., Hensel, C., Junges, S., & Katoen, J.-P. (2021). Counterexample-guided Inductive Synthesis for Probabilistic Systems. Formal Asp. Comput.
    DOI: 10.1007/s00165-021-00547-2
  2. Quatmann, T., Junges, S., & Katoen, J.-P. (2021). Markov Automata with Multiple Objectives. FMSD.
    DOI: 10.1007/s10703-021-00364-6 supplemental material
  3. Junges, S., Katoen, J.-P., Pérez, G. A., & Winkler, T. (2021). The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci., 119, pp. 183–210.
    DOI: 10.1016/j.jcss.2021.02.006 arXiv: 2009.13128
  4. Hensel, C., Junges, S., Katoen, J.-P., Quatmann, T., & Volk, M. (2021). The Probabilistic Model Checker Storm. STTT.
    DOI: 10.1007/s10009-021-00633-z arXiv: 2002.07080 supplemental material further information
  5. Winterer, L., Junges, S., Wimmer, R., Jansen, N., Topcu, U., Katoen, J.-P., & Becker, B. (2021). Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions. IEEE Trans. Autom. Control., 66(3), pp. 1040–1054.
    DOI: 10.1109/TAC.2020.2990140
  6. Cubuktepe, M., Jansen, N., Junges, S., Marandi, A., Suilen, M., & Topcu, U. (2021). Robust Finite-State Controllers for Uncertain POMDPs. AAAI.
  7. Andriushchenko, R., Ceska, M., Junges, S., Katoen, J.-P., & Stupinsky, S. (2021). PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. CAV, LNCS 12759, pp. 856–869, Springer.
    DOI: 10.1007/978-3-030-81685-8_40 supplemental material
  8. Holtzen, S., Junges, S., Vazquez-Chanlatte, M., Millstein, T., Sanjit A. Seshia, & Van den Broeck, G. (2021). Model Checking Finite-Horizon Markov Chains with Probabilistic Inference. CAV, LNCS 12760, pp. 577–601, Springer.
    DOI: 10.1007/978-3-030-81688-9_27 supplemental material
  9. Junges, S., Jansen, N., & Sanjit A. Seshia. (2021). Enforcing Almost-Sure Reachability in POMDPs. CAV, LNCS 12760, Springer.
    DOI: 10.1007/978-3-030-81688-9_28 arXiv: 2007.00085 supplemental material
  10. Junges, S., Torfah, H., & Sanjit A. Seshia. (2021). Runtime Monitors for Markov Decision Processes. CAV, LNCS 12760, Springer.
    DOI: 10.1007/978-3-030-81688-9_26 supplemental material
  11. Vazquez-Chanlatte, M., Junges, S., Fremont, D. J., & Seshia, S. (2021). Entropy-Guided Control Improvisation. RSS.
    DOI: 10.15607/RSS.2021.XVII.051 arXiv: 2103.05672
  12. Torfah, H., Junges, S., Fremont, D., & Sanjit A. Seshia. (2021). Formal Analysis of AI-Based Autonomy: From Modeling to Runtime Assurance. RV, LNCS 12974, pp. 311–330, Springer.
    DOI: 10.1007/978-3-030-88494-9_19
  13. Spel, J., Junges, S., & Katoen, J.-P. (2021). Finding Provably Optimal Markov Chains. TACAS, LNCS 12651, pp. 173–190, Springer.
    DOI: 10.1007/978-3-030-72016-2_10
  14. Andriushchenko, R., Ceska, M., Junges, S., & Katoen, J.-P. (2021). Inductive Synthesis for Probabilistic Programs Reaches New Horizons. TACAS, LNCS 12651, pp. 191–209, Springer.
    DOI: 10.1007/978-3-030-72016-2_11 supplemental material

2020

  1. Baier, C., Hensel, C., Hutschenreiter, L., Junges, S., Katoen, J.-P., & Klein, J. (2020). Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. Inf. Comput., 272, pp. 104504.
  2. Hartmanns, A., Junges, S., Katoen, J.-P., & Quatmann, T. (2020). Multi-cost Bounded Tradeoff Analysis in MDP. J. Autom. Reason., 64(7), pp. 1483–1522.
    DOI: 10.1007/s10817-020-09574-9 supplemental material
  3. Bork, A., Junges, S., Katoen, J.-P., & Quatmann, T. (2020). Verification of Indefinite-Horizon POMDPs. ATVA, LNCS 12302, pp. 288–304, Springer.
    DOI: 10.1007/978-3-030-59152-6_16 arXiv: 2007.00102 supplemental material
  4. Batz, K., Junges, S., Kaminski, B. L., Katoen, J.-P., Matheja, C., & Schröer, P. (2020). PrIC3: Property Directed Reachability for MDPs. CAV, LNCS 12225, pp. 512–538, Springer.
  5. Jansen, N., Könighofer, B., Junges, S., Serban, A., & Bloem, R. (2020). Safe Reinforcement Learning Using Probabilistic Shields. CONCUR, LIPIcs 171, pp. 3:1–3:16, Schloss Dagstuhl - LZI.
  6. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., & Topcu, U. (2020). Scenario-Based Verification of Uncertain MDPs. TACAS, LNCS 12078, pp. 287–305, Springer.

2019

  1. Ghadhab, M., Junges, S., Katoen, J.-P., Kuntz, M., & Volk, M. (2019). Safety analysis for vehicle guidance systems with dynamic fault trees. Rel. Eng. and Sys. Safety, 186, pp. 37–50.
  2. Spel, J., Junges, S., & Katoen, J.-P. (2019). Are Parametric Markov Chains Monotonic? ATVA, LNCS 11781, pp. 479–496, Springer.
    supplemental material
  3. Winkler, T., Junges, S., Pérez, G. A., & Katoen, J.-P. (2019). On the Complexity of Reachability in Parametric Markov Decision Processes. CONCUR, LIPIcs 140, pp. 14:1–14:17, Schloss Dagstuhl - LZI.
  4. Ceska, M., Hensel, C., Junges, S., & Katoen, J.-P. (2019). Counterexample-Driven Synthesis for Probabilistic Program Sketches. FM, LNCS 11800, pp. 101–120, Springer.
  5. Ceska, M., Jansen, N., Junges, S., & Katoen, J.-P. (2019). Shepherding Hordes of Markov Chains. TACAS, LNCS 11428, pp. 172–190, Springer.
  6. Ceska, M., Dehnert, C., Jansen, N., Junges, S., & Katoen, J.-P. (2019). Model Repair Revamped - - On the Automated Synthesis of Markov Chains -. From Reactive Systems to Cyber-Physical Systems, LNCS 11500, pp. 107–125, Springer.

2018

  1. Volk, M., Junges, S., & Katoen, J.-P. (2018). Fast Dynamic Fault Tree Analysis by Model Checking Techniques. IEEE Trans. Industrial Informatics, 14(1), pp. 370–379.
  2. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., & Topcu, U. (2018). Synthesis in pMDPs: A Tale of 1001 Parameters. ATVA, LNCS 11138, pp. 160–176, Springer.
  3. Junges, S., Katoen, J.-P., Stoelinga, M., & Volk, M. (2018). One Net Fits All - A Unifying Semantics of Dynamic Fault Trees Using GSPNs. Petri Nets, LNCS 10877, pp. 272–293, Springer.
  4. Junges, S., Jansen, N., Katoen, J.-P., Topcu, U., Zhang, R., & Hayhoe, M. M. (2018). Model Checking for Safe Navigation Among Humans. QEST, LNCS 11024, pp. 207–222, Springer.
  5. Hartmanns, A., Junges, S., Katoen, J.-P., & Quatmann, T. (2018). Multi-cost Bounded Reachability in MDP. TACAS, LNCS 10806, pp. 320–339, Springer.
  6. Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winterer, L., Katoen, J.-P., & Becker, B. (2018). Finite-State Controllers of POMDPs using Parameter Synthesis. UAI, pp. 519–529, AUAI Press.

2017

  1. Junges, S., Guck, D., Katoen, J.-P., Rensink, A., & Stoelinga, M. (2017). Fault trees on a diet: automated reduction by graph rewriting. Formal Asp. Comput., 29(4), pp. 651–703.
  2. Dehnert, C., Junges, S., Katoen, J.-P., & Volk, M. (2017). A storm is Coming: A Modern Probabilistic Model Checker. CAV, LNCS 10427, Springer.
  3. Quatmann, T., Junges, S., & Katoen, J.-P. (2017). Markov Automata with Multiple Objectives. CAV, LNCS 10426, Springer.
  4. Winterer, L., Junges, S., Wimmer, R., Jansen, N., Topcu, U., Katoen, J.-P., & Becker, B. (2017). Motion planning under partial observability using game-based abstraction. CDC, pp. 2201–2208, IEEE.
  5. Ghadhab, M., Junges, S., Katoen, J.-P., Kuntz, M., & Volk, M. (2017). Model-Based Safety Analysis for Vehicle Guidance Systems. SAFECOMP, LNCS 10488, pp. 3–19, Springer.
  6. Budde, C. E., Dehnert, C., Hahn, E. M., Hartmanns, A., Junges, S., & Turrini, A. (2017). JANI: Quantitative Model and Tool Interaction. TACAS, LNCS 10206, pp. 151–168.
  7. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., Papusha, I., Poonawala, H. A., & Topcu, U. (2017). Sequential Convex Programming for the Efficient Verification of Parametric MDPs. TACAS, LNCS 10206, pp. 133–150, Springer.

2016

  1. Quatmann, T., Dehnert, C., Jansen, N., Junges, S., & Katoen, J.-P. (2016). Parameter Synthesis for Markov Models: Faster Than Ever. ATVA, LNCS 9938, pp. 50–67, Springer.
  2. Junges, S., Guck, D., Katoen, J.-P., & Stoelinga, M. (2016). Uncovering Dynamic Fault Trees. DSN, pp. 299–310, IEEE CS.
  3. Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Katoen, J.-P., Ábrahám, E., & Bruintjes, H. (2016). Parameter Synthesis for Probabilistic Systems. MBMV, pp. 72–74, Albert-Ludwigs-Universität Freiburg.
  4. Volk, M., Junges, S., & Katoen, J.-P. (2016). Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates. SAFECOMP, LNCS 9922, pp. 253–265, Springer.
  5. Dombrowski, C., Junges, S., Katoen, J.-P., & Gross, J. (2016). Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks. SRDS, pp. 307–316, IEEE CS.
  6. Junges, S., Jansen, N., Dehnert, C., Topcu, U., & Katoen, J.-P. (2016). Safety-Constrained Reinforcement Learning for MDPs. TACAS, LNCS 9636, pp. 130–146, Springer.
  7. Junges, S., Jansen, N., Katoen, J.-P., & Topcu, U. (2016). Probabilistic Verification for Cognitive Models. FS-16, AAAI Press.

2015

  1. Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., & Ábrahám, E. (2015). PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. CAV, LNCS 9206, pp. 214–231, Springer.
  2. Corzilius, F., Kremer, G., Junges, S., Schupp, S., & Ábrahám, E. (2015). SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. SAT, LNCS 9340, pp. 360–368, Springer.
  3. Junges, S., Guck, D., Katoen, J.-P., Rensink, A., & Stoelinga, M. (2015). Fault Trees on a Diet - - Automated Reduction by Graph Rewriting -. SETTA, LNCS 9409, pp. 3–18, Springer.

2014

  1. Bohlender, D., Bruintjes, H., Junges, S., Katelaan, J., Nguyen, V. Y., & Noll, T. (2014). A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models. ISoLA, LNCS 8803, pp. 177–192, Springer.

2013

  1. Junges, S., Loup, U., Corzilius, F., & Ábrahám, E. (2013). On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers. CAI, LNCS 8080, pp. 186–198, Springer.

2012

  1. Corzilius, F., Loup, U., Junges, S., & Ábrahám, E. (2012). SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox - (Tool Presentation). SAT, LNCS 7317, pp. 442–448, Springer.