有限词上偏域加权规范的终止式反应系统综合

本文研究从定量规范综合终止式反应系统的问题。此类系统被建模为有限 transducer，其执行表示为 $(I\times O)^*$ 中的有限词，其中 $I,O$ 分别为有限的输入与输出符号集合。加权规范 $S$ 为 $(I\times O)^*$ 中的词赋予有理数值（或 $-\infty$），我们考虑三种综合目标：阈值目标，要求系统执行高于给定阈值；最优值与近似目标，要求系统通过提供相对于 $S$ 分别产生最优值与 $\varepsilon$-最优值的输出符号来尽可能好地执行。我们针对由配备求和、折扣求和与平均度量的确定性加权自动机给出的、有限词上偏域的这三种目标与加权规范，建立了一套可判定性结果图景。所得目标一般并非正则的，我们发展了无限博弈框架以解决相应的综合问题，即（加权）关键前缀博弈这一类。