Weighted automata is a basic tool for specification in quantitative verification, which allows to express quantitative features of analysed systems such as resource consumption. Quantitative specification can be assisted by automata learning as there are classic results on Angluin-style learning of weighted automata. The existing work assumes perfect information about the values returned by the target weighted automaton. In assisted synthesis of a quantitative specification, knowledge of the exact values is a strong assumption and may be infeasible. In our work, we address this issue by introducing a new framework of partially-observable deterministic weighted automata, in which weighted automata return intervals containing the computed values of words instead of the exact values. We study the basic properties of this framework with the particular focus on the challenges of
翻译:摘要:加权自动机是定量验证中用于规范描述的基本工具,能够表达分析系统(如资源消耗)的定量特征。借助自动机学习(例如基于Angluin风格的加权自动机学习经典成果)可辅助定量规范的构建。现有工作假定目标加权自动机返回值具有完美信息。在定量规范的辅助综合中,精确数值的认知是一种强假设,可能难以实现。本研究通过引入部分可观测确定性加权自动机新框架解决该问题,其中加权自动机返回包含词语计算值的区间而非精确值。我们重点研究该框架的基本性质,特别关注其面临的挑战。