Synthesis from Weighted Specifications with Partial Domains over Finite Words
Synthesis from Weighted Specifications with Partial Domains over Finite Words
复制标题
DOI：
10.4230/lipics.fsttcs.2020.46
复制
发表时间：
2021-03
期刊：
影响因子：
--
通讯作者：
E. Filiot;Christof Löding;Sarah Winter
中科院分区：
文献类型：
--
作者：
E. Filiot;Christof Löding;Sarah Winter
本文从定量规范出发，研究了终止反应系统的综合问题。这样的系统被建模为有限换能器，其执行被表示为(Σi×Σo)中的有限字，其中Σi，Σo分别是输入和输出符号的有限集合。加权规范S给(−∞i×Σo)中的词赋予一个有理值(或Σ)，我们考虑了三种综合目标，即要求系统执行超过某个给定阈值的阈值目标、要求系统通过提供分别产生最佳值和ε最佳值的输出符号来尽可能地执行的阈值目标、最优值和近似目标。我们建立了这三个目标的可判断性结果的图景，并用配备和、折扣和和平均度量的确定性加权自动机给出了有限字上具有部分论域的加权规格说明。由此产生的目标一般不是正则的，我们开发了一个无限对策框架来解决相应的综合问题，即(加权的)临界前缀对策类。2012年ACM学科分类计算→逻辑与验证理论；计算理论→传感器；计算理论→定量自动机
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. 2012 ACM Subject Classification Theory of computation → Logic and verification; Theory of computation → Transducers; Theory of computation → Quantitative automata