只等待非阻塞广播协议的安全性验证
Safety Verification of Wait-Only Non-Blocking Broadcast Protocols
AI总结：
该研究探讨了只等待非阻塞广播协议的安全性验证，证明了在特定条件下，状态和配置覆盖性问题的复杂性分别降低为P完全和PSPACE完全。
摘要：
广播协议是设计用于由进程网络执行的程序。每个进程运行相同的协议，它们之间的通信以同步的两种方式发生：广播，其中某个进程向所有其他进程发送消息，以及会面，其中某个进程向最多一个其他进程发送消息。在两种情况下，通信都是非阻塞的，这意味着即使没有进程能够接收消息，消息也会被发送。我们考虑两个覆盖性问题：状态覆盖性问题询问是否存在一个进程数量使得能够达到协议的给定状态，而配置覆盖性问题询问是否存在一个进程数量使得能够覆盖给定的配置。这两个问题已知是可判定的且Ackermann难。我们显示当协议是只等待（即没有进程状态既能发送又能接收消息）时，这些问题分别变为P完全和PSPACE完全。
英文摘要：
Broadcast protocols are programs designed to be executed by networks of processes. Each process runs the same protocol, and communication between them occurs in synchronously in two ways: broadcast, where one process sends a message to all others, and rendez-vous, where one process sends a message to at most one other process. In both cases, communication is non-blocking, meaning the message is sent even if no process is able to receive it. We consider two coverability problems: the state coverability problem asks whether there exists a number of processes that allows reaching a given state of the protocol, and the configuration coverability problem asks whether there exists a number of processes that allows covering a given configuration. These two problems are known to be decidable and Ackermann-hard. We show that when the protocol is Wait-Only (i.e., it has no state from which a process can both send and receive messages), these problems become P-complete and PSPACE-complete, respectively.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
