Checking Finite State Machine Conformance when there are Distributed Observations

TL;DR

This paper investigates the conformance checking of distributed finite state machines, revealing undecidability issues and providing conditions for decidability, with implications for testing and development of distributed systems.

Contribution

It defines a language for multi-port FSMs to characterize conformance, proves undecidability of certain conformance problems, and analyzes complexity under bounded conditions.

Findings

${ ilde L}(M)$ can be uniquely defined but may not be regular.

Deciding $N ot rianglelefteq_s M$ is generally undecidable.

Deciding $N rianglelefteq_s^k M$ is polynomial-time with bounds, NP-hard otherwise.

Abstract

This paper concerns state-based systems that interact with their environment at physically distributed interfaces, called ports. When such a system is used a projection of the global trace, called a local trace, is observed at each port. This leads to the environment having reduced observational power: the set of local traces observed need not uniquely define the global trace that occurred. We consider the previously defined implementation relation $\sqsubseteq_s$ and start by investigating the problem of defining a language ${\mathcal {\tilde L}} (M)$ for a multi-port finite state machine (FSM) $M$ such that $N \sqsubseteq_s M$ if and only if every global trace of $N$ is in ${\mathcal {\tilde L}} (M)$. The motivation is that if we can produce such a language ${\mathcal {\tilde L}} (M)$ then this can potentially be used to inform development and testing. We show that ${\mathcal {\tilde L}} (M)$ can be uniquely defined but need not be regular. We then prove that it is generally undecidable whether $N \sqsubseteq_s M$, a consequence of this result being that it is undecidable whether there is a test case that is capable of distinguishing two states or two multi-port FSM in distributed testing. This result complements a previous result that it is undecidable whether there is a test case that is guaranteed to distinguish two states or multi-port FSMs. We also give some conditions under which $N \sqsubseteq_s M$ is decidable. We then consider the implementation relation $\sqsubseteq_s^k$ that only concerns input sequences of length $k$ or less. Naturally, given FSMs $N$ and $M$ it is decidable whether $N \sqsubseteq_s^k M$ since only a finite set of traces is relevant. We prove that if we place bounds on $k$ and the number of ports then we can decide $N \sqsubseteq_s^k M$ in polynomial time but otherwise this problem is NP-hard.