论文标题
概率传感器中的过程对称性
Process Symmetry in Probabilistic Transducers
论文作者
论文摘要
模型检查是确定系统是否满足给定规范的过程。通常，当设置包含多个过程时，规格超过了与单个过程相对应的输入信号集和输出信号。然后，关于过程身份的许多属性是对称的。在这项工作中，我们考虑了确定给定系统是否对流程身份表现出对称性的问题。当系统对称时，这可以深入了解系统的行为，并允许设计人员仅使用代表性规范，而不是在所有可能的过程身份上迭代。 具体而言，我们考虑概率系统，并提出了几种对称性的变体。我们从精确的对称性开始，在给定排列$π$的情况下，在给定排列输入的情况下，系统保持了排列的输出的确切分布。我们开始研究对称性的近似版本，包括由小$ l_ \ infty $ norm引起的对称性，基于Parikh-Image的对称性的变体和定性对称性。对于每种类型的对称性，我们考虑确定给定系统是否表现出这种对称性的问题。
Model checking is the process of deciding whether a system satisfies a given specification. Often, when the setting comprises multiple processes, the specifications are over sets of input and output signals that correspond to individual processes. Then, many of the properties one wishes to specify are symmetric with respect to the processes identities. In this work, we consider the problem of deciding whether the given system exhibits symmetry with respect to the processes' identities. When the system is symmetric, this gives insight into the behaviour of the system, as well as allows the designer to use only representative specifications, instead of iterating over all possible process identities. Specifically, we consider probabilistic systems, and we propose several variants of symmetry. We start with precise symmetry, in which, given a permutation $π$, the system maintains the exact distribution of permuted outputs, given a permuted inputs. We proceed to study approximate versions of symmetry, including symmetry induced by small $L_\infty$ norm, variants of Parikh-image based symmetry, and qualitative symmetry. For each type of symmetry, we consider the problem of deciding whether a given system exhibits this type of symmetry.
