Abstract
In Boolean synthesis, we are given an LTL specification, and the goal is to construct a transducer that realizes it against an adversarial environment.
Often, a specification contains both Boolean requirements that should be satisfied against an adversarial environment, and multivalued components that refer to the quality of the satisfaction and whose expected cost we would like to minimize with respect to a probabilistic environment.
In this work we study, for the first time, meanpayoff games in which the system aims at minimizing the expected cost against a probabilistic environment, while surely satisfying an omegaregular condition against an adversarial environment.
We consider the case the omegaregular condition is given as a parity objective or by an LTL formula.
We show that in general, optimal strategies need not exist, and moreover, the limit value cannot be approximated by finitememory strategies.
We thus focus on computing the limitvalue, and give tight complexity bounds for synthesizing epsilonoptimal strategies for both finitememory and infinitememory strategies.
We show that our game naturally arises in various contexts of synthesis with Boolean and multivalued objectives. Beyond direct applications, in synthesis with costs and rewards to certain behaviors, it allows us to compute the minimal sensing cost of omegaregular specifications  a measure of quality in which we look for a transducer that minimizes the expected number of signals that are read from the input.
BibTeX  Entry
@InProceedings{almagor_et_al:LIPIcs:2016:6168,
author = {Shaull Almagor and Orna Kupferman and Yaron Velner},
title = {{Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {9:19:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770170},
ISSN = {18688969},
year = {2016},
volume = {59},
editor = {Jos{\'e}e Desharnais and Radha Jagadeesan},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6168},
URN = {urn:nbn:de:0030drops61689},
doi = {10.4230/LIPIcs.CONCUR.2016.9},
annote = {Keywords: Stochastic and Quantitative Synthesis, Mean Payoff Games, Sensing.}
}
Keywords: 

Stochastic and Quantitative Synthesis, Mean Payoff Games, Sensing. 
Collection: 

27th International Conference on Concurrency Theory (CONCUR 2016) 
Issue Date: 

2016 
Date of publication: 

24.08.2016 