PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs

Lecture notes in computer science, pp. 856–869

Abstract

Abstract This paper presents PAYNT, a tool to automatically synthesise probabilistic programs. PAYNT enables the synthesis of finite-state probabilistic programs from a program sketch representing a finite family of program candidates. A tight interaction between inductive oracle-guided methods with state-of-the-art probabilistic model checking is at the heart of PAYNT. These oracle-guided methods effectively reason about all possible candidates and synthesise programs that meet a given specification formulated as a conjunction of temporal logic constraints and possibly including an optimising objective. We demonstrate the performance and usefulness of PAYNT using several case studies from different application domains; e.g., we find the optimal randomized protocol for network stabilisation among 3M potential programs within minutes, whereas alternative approaches would need days to do so.

Authors 5

1. Roman Andriushchenko

   Brno University of Technology

   Affiliation as printed

   Brno University of Technology, Brno, Czech Republic

2. Milan Češka corresponding

   Brno University of Technology

   Affiliation as printed

   Brno University of Technology, Brno, Czech Republic

3. Sebastian Junges

   University of California, Berkeley

   Affiliation as printed

   University of California, Berkeley, USA

4. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

5. Šimon Stupinský

   Brno University of Technology

   Affiliation as printed

   Brno University of Technology, Brno, Czech Republic