Sebastian Junges

Sebastian Junges

Computer Scientist developing trustworthy algorithms to evaluate system dependability.

Syntax-Guided Synthesis in Probabilistic Programs

As a variant to the parameter synthesis, we consider probabilistic programs with holes, where the right expression for the holes have to be synthesised. A technical difference to parameter synthesis is that we consider finite sets of programs with often different control flow diagrams.

Algorithms

We developed algorithms based on counterexample-guided inductive synthesis [1], [2] and abstraction-refinement [3], see also [4] for a high-level overview. Both approaches can be efficiently combined using a method described in [5].

Application to POMDP controller synthesis

The synthesis algorithms are applicable to controller synthesis in POMDPs [6], [7].

Tool support

The algorithms above have all been implemented in PAYNT [8].

References

  1. 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
  2. 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
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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