编排综合中的研究挑战
摘要：契约自动机允许在服务合同的行为方面进行正式定义，其中一些服务提供和请求是可选的，而另一些是必需的。如果所有服务请求都与相应的提供相匹配，则合同的组合被认为是一致的。每当合同的组合不一致时，可以使用编排合成算法进行细化以达成一致。该算法是监督控制理论中使用的合成算法的变体，其基于可选变迁是可控的这一事实，而必要变迁最多是半可控的，并且并非总是可控的。实际上，得到的编排使尽可能保持一致的行为。在本文中，我们讨论了契约自动机的编排合成算法的最新发展。特别是，我们提出了半可控性的细化概念，并通过示例将其与原始概念进行比较。然后，我们讨论了编排合成算法的当前限制，并确定了一些研究挑战以及研究路线图。
作者：Davide Basile (Formal Methods and Tools lab, ISTI-CNR, Pisa, Italy), Maurice H. ter Beek (Formal Methods and Tools lab, ISTI-CNR, Pisa, Italy)
论文ID：2308.10651
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-08-24