License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2020.46
URN: urn:nbn:de:0030-drops-132874
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13287/
Filiot, Emmanuel ;
Löding, Christof ;
Winter, Sarah
Synthesis from Weighted Specifications with Partial Domains over Finite Words
Abstract
In this paper, we investigate the synthesis problem of terminating reactive systems from quantitative specifications. Such systems are modeled as finite transducers whose executions are represented as finite words in (I × O)^*, where I, O are finite sets of input and output symbols, respectively. A weighted specification S assigns a rational value (or -∞) to words in (I × O)^*, and we consider three kinds of objectives for synthesis, namely threshold objectives where the system’s executions are required to be above some given threshold, best-value and approximate objectives where the system is required to perform as best as it can by providing output symbols that yield the best value and ε-best value respectively w.r.t. S. We establish a landscape of decidability results for these three objectives and weighted specifications with partial domain over finite words given by deterministic weighted automata equipped with sum, discounted-sum and average measures. The resulting objectives are not regular in general and we develop an infinite game framework to solve the corresponding synthesis problems, namely the class of (weighted) critical prefix games.
BibTeX - Entry
@InProceedings{filiot_et_al:LIPIcs:2020:13287,
author = {Emmanuel Filiot and Christof L{\"o}ding and Sarah Winter},
title = {{Synthesis from Weighted Specifications with Partial Domains over Finite Words}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {46:1--46:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Nitin Saxena and Sunil Simon},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/13287},
URN = {urn:nbn:de:0030-drops-132874},
doi = {10.4230/LIPIcs.FSTTCS.2020.46},
annote = {Keywords: synthesis, weighted games, weighted automata on finite words}
}
|
Keywords: |
|
synthesis, weighted games, weighted automata on finite words |
|
Collection: |
|
40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020) |
|
Issue Date: |
|
2020 |
|
Date of publication: |
|
04.12.2020 |
