Publication Details

PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs

ANDRIUSHCHENKO Roman, ČEŠKA Milan, JUNGES Sebastian, KATOEN Joost-Pieter and STUPINSKÝ Šimon. PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. In: International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 12759. Cham: Springer Verlag, 2021, pp. 856-869. ISBN 978-3-030-81684-1.
Czech title
PAYNT: Nástroj pro induktivní syntézu pravděpodobnostních programů.
Type
conference paper
Language
english
Authors
Andriushchenko Roman, Ing. (DITS FIT BUT)
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT)
Junges Sebastian (RWTH Aachen University)
Katoen Joost-Pieter (RWTH)
Stupinský Šimon, Ing. ()
Keywords

Probabilistic programs,
Inductive Synthesis,
Counterexamples,
Probabilistic Model Checking

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.

Published
2021
Pages
856-869
Proceedings
International Conference on Computer Aided Verification (CAV)
Series
Lecture Notes in Computer Science
Volume
12759
Conference
33th International Conference on Computer Aided Verification, Las Vegas, US
ISBN
978-3-030-81684-1
Publisher
Springer Verlag
Place
Cham, DE
DOI
10.1007/978-3-030-81685-8_40
UT WoS
000698732400040
EID Scopus
2-s2.0-85113446002
BibTeX 
@INPROCEEDINGS{FITPUB12533,
   author = "Roman Andriushchenko and Milan \v{C}e\v{s}ka and Sebastian Junges and Joost-Pieter Katoen and \v{S}imon Stupinsk\'{y}",
   title = "PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs",
   pages = "856--869",
   booktitle = "International Conference on Computer Aided Verification (CAV)",
   series = "Lecture Notes in Computer Science",
   volume = 12759,
   year = 2021,
   location = "Cham, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-030-81684-1",
   doi = "10.1007/978-3-030-81685-8\_40",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12533"
}
Back to top