Detail publikačního výsledku

PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs

ANDRIUSHCHENKO, R.; ČEŠKA, M.; STUPINSKÝ, Š.; JUNGES, S.; KATOEN, J.

Originální název

PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs

Anglický název

PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

Probabilistic programs,
Inductive Synthesis,
Counterexamples,
Probabilistic Model Checking

Klíčová slova v angličtině

Probabilistic programs,
Inductive Synthesis,
Counterexamples,
Probabilistic Model Checking

Autoři

ANDRIUSHCHENKO, R.; ČEŠKA, M.; STUPINSKÝ, Š.; JUNGES, S.; KATOEN, J.

Rok RIV

2022

Vydáno

19.07.2021

Nakladatel

Springer Verlag

Místo

Cham

ISBN

978-3-030-81684-1

Kniha

International Conference on Computer Aided Verification (CAV)

Edice

Lecture Notes in Computer Science

Svazek

12759

Strany od

856

Strany do

869

Strany počet

14

BibTex

@inproceedings{BUT172523,
  author="ANDRIUSHCHENKO, R. and ČEŠKA, M. and STUPINSKÝ, Š. and JUNGES, S. and KATOEN, J.",
  title="PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs",
  booktitle="International Conference on Computer Aided Verification (CAV)",
  year="2021",
  series="Lecture Notes in Computer Science",
  volume="12759",
  pages="856--869",
  publisher="Springer Verlag",
  address="Cham",
  doi="10.1007/978-3-030-81685-8\{_}40",
  isbn="978-3-030-81684-1"
}