具有因果记忆的分布式系统综合中的全局获胜条件(完整版)
计算机科学中的逻辑
2021-10-19 v2
摘要
在分布式系统的综合中,我们通过从形式规范自动推导正确实现来自动化分布式程序与硬件的开发。对于同步分布式系统,综合问题已知是不可判定的。对于异步系统,可判定与不可判定综合问题之间的边界是一个长期开放问题。我们在 Petri 博弈的设定中研究该问题,Petri 博弈是一种为异步进程配备因果记忆的分布式系统框架。Petri 博弈将 Petri 网扩展为系统库所与环境库所的区分。分布式系统的组件是博弈的参与者,表示为在每个同步期间交换信息的令牌。该模型先前的可判定性结果仅限于局部获胜条件,即仅涉及单个组件的条件。在本文中,我们考虑全局获胜条件,例如互斥,即涉及所有组件状态的条件。我们给出全局获胜条件的可判定与不可判定结果。首先,对于以坏标记给出的获胜条件,我们证明在具有有界数量系统参与者和一名环境参与者的 Petri 博弈中,是否存在系统参与者的获胜策略是可判定的。其次,对于同时涉及好标记与坏标记的获胜条件,我们证明在至少具有两名系统参与者和一名环境参与者的 Petri 博弈中,是否存在系统参与者的获胜策略是不可判定的。因此,我们的结果表明,一方面,确实可以在分布式系统综合中使用像互斥这样的全局安全性规范。但另一方面,添加全局活性规范会导致对几乎所有 Petri 博弈而言不可判定的综合问题。
引用
@article{arxiv.2107.09280,
title = {Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory (Full Version)},
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-Rüdiger Olderog},
journal= {arXiv preprint arXiv:2107.09280},
year = {2021}
}