paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Multiparty testing preorders

多方测试预序
LMCS vol.Volume 19, Issue 12023匹配度 1/10 · 该论文属于纯并发理论与形式语义中的测试预序研究,未涉及LLM/智能体、静态分析、浮点程序分析或贝叶斯程序分析,与用户研究画像的核心方向几乎无交集。引用 3 inbox
Rocco de Nicola, Hernán Melgratti
crossref: 2026-09-10

AI 速览

一句话:提出无协调与个人主义两种多方测试预序,刻画其相对经典 must 测试预序的粗细关系及装饰迹表征。

在面向服务计算中,经典 must 测试方法已被用于分析客户端与服务器(或更一般地,两个对等方)之间契约的合规性。然而多方场景中,伙伴通常不具备完全协调能力,因此需要更宽松的合规概念。本文通过限制潜在观察者集合,提出两种新的测试预序:无协调预序只允许并行观察者使用给定服务的不同接口部分且彼此不能通信;个人主义预序则让并行观察者将所有不在目标接口中的动作视为静默。作者证明无协调预序比经典 must 测试预序更粗,且比个人主义预序更细;并为两者给出装饰迹刻画:无协调预序由 must-set 与 Mazurkiewicz 迹定义,个人主义预序由仅含指定可见动作的过滤迹类与 must-set 描述。

问题
经典 must 测试预序用于双方合规性分析,但多方场景中伙伴缺乏完全协调,现有概念过严,需要更宽松的合规判定。
方法
通过限制潜在观察者集合定义无协调与个人主义两种测试预序,并给出基于 must-set、Mazurkiewicz 迹和过滤迹的语义刻画。
评估
以理论证明评估:无协调预序粗于经典 must 测试预序、细于个人主义预序,且两种预序均获得装饰迹表征。
原文摘要(Abstract)

Variants of the must testing approach have been successfully applied in service oriented computing for analysing the compliance between (contracts exposed by) clients and servers or, more generally, between two peers. It has however been argued that multiparty scenarios call for more permissive notions of compliance because partners usually do not have full coordination capabilities. We propose two new testing preorders, which are obtained by restricting the set of potential observers. For the first preorder, called uncoordinated, we allow only sets of parallel observers that use different parts of the interface of a given service and have no possibility of intercommunication. For the second preorder, that we call individualistic, we instead rely on parallel observers that perceive as silent all the actions that are not in the interface of interest. We have that the uncoordinated preorder is coarser than the classical must testing preorder and finer than the individualistic one. We also provide a characterisation in terms of decorated traces for both preorders: the uncoordinated preorder is defined in terms of must-sets and Mazurkiewicz traces while the individualistic one is described in terms of classes of filtered traces that only contain designated visible actions and must-sets.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2249,
  title = {Multiparty testing preorders},
  author = {Rocco de Nicola and Hernán Melgratti},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 19, Issue 1},
  year = {2023},
  doi = {10.46298/lmcs-19(1:1)2023}
}