静默一致性及其变体的可判定性与复杂性

静默一致性是并发对象的一种正确性概念，它赋予对象在静默状态（即对象的操作均未被执行的状态）下的行为以意义。实现对象的正确性是根据相应的抽象规范来定义的。这引发了两个重要的验证问题：成员性（检查实现的一个行为是否被规范允许）与正确性（检查实现的所有行为是否都被规范允许）。在本文中，我们证明静默一致性的成员性问题是NP-complete的，而正确性问题是可判定的，但为coNP-hard且属于EXPSPACE。对这两个问题，我们考虑了静默一致性的受限版本，即假设两个静默点之间的事件数量存在上限。此处，我们证明成员性问题属于PTIME，而正确性属于PSPACE。静默一致性不保证顺序一致性，即它允许在映射到抽象规范时，同一进程的操作调用被重排序。因此，我们还考虑了静默顺序一致性，它通过附加的顺序一致性条件加强了静默一致性。我们证明无限制的成员性和正确性版本分别为NP-complete和不可判定。当对两个静默点之间的事件数加以限制时，成员性属于PTIME，而正确性属于PSPACE。最后，我们考虑了一种静默顺序一致性版本，它对实现的每次运行中的进程数量设定上限，并证明带有此限制的静默顺序一致性的成员性问题属于PTIME。