关于在Bach中引入受限列表的表现能力、正确性和效率问题
摘要：基于数据的协同语言在处理并发性方面提供了另一种方式，旨在通过异步地通过信息在共享空间上是否可用来同步进程，从而清晰地分离交互和计算。尽管这些语言拥有有趣的属性，但验证程序的正确性仍然具有挑战性。一些工作，例如Anemone，引入了一些功能，包括动画和模型检查临时逻辑公式，以更好地理解系统建模。然而，模型检查由于状态空间爆炸问题而提出了性能问题。在本文中，我们提出了一个保护列表构造作为解决这个问题的方法。我们证明了保护列表构造在增加性能的同时严格丰富了基于数据的协同语言的表达能力。此外，我们引入了一种细化的概念，以一种保持正确性的方式引入保护列表构造。
作者：Manel Barkallah (Nadi Research Institute Faculty of Computer Science University of Namur Namur, Belgium), Jean-Marie Jacquet (Nadi Research Institute Faculty of Computer Science University of Namur Namur, Belgium)
论文ID：2308.10655
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-08-22