Almagor, Shaull ;
Kupferman, Orna
HighQuality Synthesis Against Stochastic Environments
Abstract
In the classical synthesis problem, we are given a linear temporal logic (LTL) formula psi over sets of input and output signals, and we synthesize a transducer that realizes psi: with every sequence of input signals, the transducer associates a sequence of output signals so that the generated computation satisfies psi. One weakness of automated synthesis in practice is that it pays no attention to the quality of the synthesized system. Indeed, the classical setting is Boolean: a computation satisfies a specification or does not satisfy it. Accordingly, while the synthesized system is correct, there is no guarantee about its quality. In recent years, researchers have considered extensions of the classical Boolean setting to a quantitative one. The logic FLTL is a multivalued logic that augments LTL with quality operators. The satisfaction value of an FLTL formula is a real value in [0,1], where the higher the value is, the higher is the quality in which the computation satisfies the specification.
Decision problems for LTL become search or optimization problems for FLTL. In particular, in the synthesis problem, the goal is to generate a transducer that satisfies the specification in the highest possible quality. Previous work considered the worstcase setting, where the goal is to maximize the quality of the computation with the minimal quality. We introduce and solve the stochastic setting, where the goal is to generate a transducer that maximizes the expected quality of a computation, subject to a given distribution of the input signals. Thus, rather than being hostile, the environment is assumed to be probabilistic, which corresponds to many realistic settings. We show that the problem is 2EXPTIMEcomplete, like classical LTL synthesis. The complexity stays 2EXPTIME also in two extensions we consider: one that maximizes the expected quality while guaranteeing that the minimal quality is, with probability 1, above a given threshold, and one that allows assumptions on the environment.
BibTeX  Entry
@InProceedings{almagor_et_al:LIPIcs:2016:6568,
author = {Shaull Almagor and Orna Kupferman},
title = {{HighQuality Synthesis Against Stochastic Environments}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {28:128:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770224},
ISSN = {18688969},
year = {2016},
volume = {62},
editor = {JeanMarc Talbot and Laurent Regnier},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6568},
URN = {urn:nbn:de:0030drops65688},
doi = {10.4230/LIPIcs.CSL.2016.28},
annote = {Keywords: Stochastic and Quantitative Synthesis, Markov Decision Process}
}
2016
Keywords: 

Stochastic and Quantitative Synthesis, Markov Decision Process 
Seminar: 

25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Issue date: 

2016 
Date of publication: 

2016 