论 Bach 中守卫列表的引入：表达性、正确性与效率问题
编程语言
2023-08-22 v1
摘要
并发理论已受到相当关注，但大多限于 CCS、CSP 和 ACP 等同步进程代数范畴。作为处理并发的另一种方式，基于数据的协调语言旨在通过共享空间上信息的可用或不可用异步地同步进程，从而在交互与计算间提供清晰分离。尽管这些语言具备有趣性质，验证程序正确性仍具挑战性。部分工作（如 Anemone）引入了包括动画与时态逻辑公式模型检查在内的设施，以更好地理解系统建模。然而，模型检查因状态空间爆炸问题而存在已知性能缺陷。本文提出一种守卫列表构造作为解决该问题的方案。我们确立守卫列表构造在严格丰富基于数据的协调语言表达性的同时提升了性能。此外，我们引入一种精化概念，以保持正确性的方式引入守卫列表构造。
引用
@article{arxiv.2308.10655,
title = {On the Introduction of Guarded Lists in Bach: Expressiveness, Correctness, and Efficiency Issues},
author = {Manel Barkallah and Jean-Marie Jacquet},
journal= {arXiv preprint arXiv:2308.10655},
year = {2023}
}
备注
In Proceedings ICE 2023, arXiv:2308.08920