分布式观测下的有限状态机一致性检查

本文关注在物理分布式接口（称为端口）处与环境交互的基于状态的系统。当使用此类系统时，在每个端口观测到全局迹的投影，称为局部迹。这导致环境的观测能力降低：观测到的局部迹集不必唯一地定义发生的全局迹。我们考虑先前定义的实现关系$\sqsubseteq_s$，首先研究为多端口有限状态机（FSM）$M$定义语言${\mathcal {\tilde L}} (M)$的问题，使得$N \sqsubseteq_s M$当且仅当$N$的每个全局迹都在${\mathcal {\tilde L}} (M)$中。动机是，如果我们能生成这样的语言${\mathcal {\tilde L}} (M)$，那么它可能用于指导开发和测试。我们证明${\mathcal {\tilde L}} (M)$可以唯一地定义，但不必是正则的。然后我们证明$N \sqsubseteq_s M$通常是不可判定的，这一结果的一个推论是，在分布式测试中是否存在能够区分两个状态或两个多端口FSM的测试用例是不可判定的。该结果补充了先前关于是否存在保证区分两个状态或多端口FSM的测试用例是不可判定的结果。我们还给出了$N \sqsubseteq_s M$可判定的一些条件。然后我们考虑仅涉及长度不超过$k$的输入序列的实现关系$\sqsubseteq_s^k$。自然地，给定FSM $N$和$M$，$N \sqsubseteq_s^k M$是可判定的，因为只涉及有限迹集。我们证明，如果对$k$和端口数施加界限，则可以在多项式时间内判定$N \sqsubseteq_s^k M$，否则该问题是NP难的。