State Identification for Labeled Transition Systems with Inputs and Outputs

TL;DR

This paper introduces an algorithm for state identification in labeled transition systems with inputs and outputs, extending FSM testing theory to more complex systems and demonstrating high effectiveness in practical benchmarks.

Contribution

It generalizes the adaptive distinguishing sequence algorithm from FSMs to LTSs, enabling effective state identification in richer system models.

Findings

Algorithm distinguishes over 99% of incompatible state pairs in benchmarks.

The approach extends FSM testing techniques to LTSs, broadening applicability.

Experimental results show practical effectiveness despite theoretical limitations.

Abstract

For Finite State Machines (FSMs) a rich testing theory has been developed to discover aspects of their behavior and ensure their correct functioning. Although this theory is widely used, e.g., to check conformance of protocol implementations, its applicability is limited by restrictions of the FSM framework: the fact that inputs and outputs alternate in an FSM, and outputs are fully determined by the previous input and state. Labeled Transition Systems with inputs and outputs (LTSs), as studied in ioco testing theory, provide a richer framework for testing component oriented systems, but lack the algorithms for test generation from FSM theory. In this article, we propose an algorithm for the fundamental problem of state identification during testing of LTSs. Our algorithm is a direct generalization of the well-known algorithm for computing adaptive distinguishing sequences for FSMs proposed by Lee & Yannakakis. Our algorithm has to deal with so-called compatible states, states that cannot be distinguished in case of an adversarial system-under-test. Analogous to the result of Lee & Yannakakis, we prove that if an (adaptive) test exists that distinguishes all pairs of incompatible states of an LTS, our algorithm will find one. In practice, such adaptive tests typically do not exist. However, in experiments with an implementation of our algorithm on an industrial benchmark, we find that tests produced by our algorithm still distinguish more than 99% of the incompatible state pairs.

Figures

Tables

Table 1. Table 1: Computation statistics

Subalphabet	Number of states	Pairs of compatible states	Nodes in splitting graph	Depth distinguishing graph	Incompatible pairs not distinguished
InitIdleSleep	1616	16638 (0.64%)	1121	33	1145 (0.044%)
InitIdleStandbyRunning	2855	14171 (0.17%)	2082	33	2183 (0.027%)
InitIdleStandbySleep	3168	25974 (0.26%)	2226	33	3826 (0.038%)
InitIdleStandbyLowPower	2614	13834 (0.20%)	1809	33	2920 (0.043%)
InitError	2649	373427 (5.3%)	3097	35	17972 (0.27%)

Equations

$$digraph(A)$$

$$\text{in}(q)=\{a\in I\mid T(q,a)\downarrow \}$$

$$\text{out}(q)=\{x\in O\mid T(q,x)\downarrow \}$$

$$q\text{after}ϵ=\{q\}$$

$$q\text{after}\mu \sigma =\{\begin{array}{ll}T(q,\mu )\text{after}\sigma & \text{if }T(q,\mu )\downarrow \\ \varnothing & \text{otherwise}\end{array}$$

$$\text{enabled}(q,\sigma )=\{\begin{array}{ll}\varnothing & \text{if }q\text{after}\sigma =\varnothing \\ \{q\}& \text{otherwise}\end{array}$$

$$q\text{before}\sigma =\{q^{\prime }\in Q\mid q\in q^{\prime }\text{after}\sigma \}$$

$$A\text{after}\sigma =q_0\text{after}\sigma$$

$$\text{traces}(q)=\{\rho \in L^{\ast }\mid q\text{after}\rho \ne \varnothing \}$$

$$F$$

$$(G,\mu ,G^{\prime })\in T_{CCS}\wedge (G,\mu ,G^{\prime \prime })\in T_{CCS}$$

$$T(G,\mu )$$

$$\exists a\in \text{in}(q):T(q,a)\in P$$

$$\forall a\in \text{in}(q):T(q,a)\in P$$

$$\forall a\in \text{in}(q)\cap \text{in}(q^{\prime }):(T(q,a),T(q^{\prime },a))\in R\text{, and}$$

$$\exists x\in \text{out}(q)\cap \text{out}(q^{\prime }):(T(q,x),T(q^{\prime },x))\in R$$

$$T((q_1,q_2),\mu )$$

$$\forall a\in \text{in}(r)\cap \text{in}(r^{\prime }):(T(r,a),T(r^{\prime },a))\in P\text{, and}$$

$$\exists x\in \text{out}(r)\cap \text{out}(q^{\prime }):(T(r,x),T(r^{\prime },x))\in P$$

$$\forall x\in \text{out}(l):$$

$$\exists a\in \text{in}(l):LCA(Y,l\text{after}a)\ne \varnothing$$

$$\Pi (P,\mu ,v)$$

$$T_n$$

$$\forall q,q^{\prime }\in P:q/◊q^{\prime }$$

Full text

In this article, we propose an algorithm for the fundamental problem of state identification during testing of LTSs. Our algorithm is a direct generalization of the well-known algorithm for computing adaptive distinguishing sequences for FSMs proposed by Lee & Yannakakis. Our algorithm has to deal with so-called compatible states, states that cannot be distinguished in case of an adversarial system-under-test. Analogous to the result of Lee & Yannakakis, we prove that if an (adaptive) test exists that distinguishes all pairs of incompatible states of an LTS, our algorithm will find one. In practice, such adaptive tests typically do not exist. However, in experiments with an implementation of our algorithm on an industrial benchmark, we find that tests produced by our algorithm still distinguish more than 99% of the incompatible state pairs.

1 Introduction

Starting with Moore’s famous 1956 paper [16], a rich theory of testing finite-state machines (FSMs) has been developed to discover aspects of their behavior and ensure their correct functioning; see e.g. [12] for a survey. One of the classical testing problems is state identification: given some FSM, determine in which state it was initialized, by providing inputs and observing outputs.

Various forms of distinguishing sequences were proposed, ranging from sets of sequences to single sequences solving the problem. Moreover, when combined with state access sequences, so called $n$-complete test suites can be constructed [8]. The challenge in using $n$-complete test suites is to keep their size as small as possible. Using a single (adaptive) sequence for state identification [11], helps to reach this objective. If such a single sequence does not exist, then a distinguishing sequence distinguishing most states may be supplemented with some additional distinguishing sequences that distinguish the remaining states [15].

Although state identification algorithms for FSMs have been widely used, e.g., to check conformance of protocol implementations, their applicability is limited by the expressivity of the FSM framework. In FSMs, inputs and outputs strictly alternate, outputs are fully determined by the previous input and state, and inputs must be enabled in every state. Labeled Transition Systems with inputs and outputs (LTSs), as studied in ioco testing theory [24], provide a richer framework for testing component oriented systems: transitions are labeled by either an input or an output, allowing any combination of inputs and outputs, multiple outputs may be starting from the same state, allowing (observable) output nondeterminism, and states do not need to have transitions for all inputs, allowing partiality. However, LTSs lack the algorithms for test generation from FSM theory. Although progress has been made in defining and constructing $n$-complete test suites for LTSs [4], an algorithm to solve the state identification problem as in [11], and hence to provide slim $n$-complete test suites, is missing.

Therefore we generalize the construction algorithms for adaptive distinguishing sequences, as given in [11]. As in [4], we have to face the problem of compatible states [18, 20], which does not occur for FSMs. States are compatible when they cannot be distinguished in case of an adversarial system-under-test, e.g. when two states have a transition for the same output to the same state. As it is easy to construct LTSs with compatible states, we made sure our algorithms can deal with such LTSs: they accept LTSs with compatible states, but they ‘work around’ them, dealing with all incompatible states.

The outline of the paper is as follows. We first introduce graphs, LTSs, and some syntax for denoting trees. Then we elaborate on compatibility and the related concept of validity. Furthermore, we introduce test cases, and define when they distinguish states of an LTS. After that we define a data structure called splitting graph, present an algorithm that constructs a splitting graph for a given LTS, and another algorithm that extracts a test case from a splitting graph. We show that, unlike for FSMs, the splitting graph may have an exponential number of nodes. However, this is worst case behaviour, as our experiments on an industrial case study will show. Analogous to FSMs, it may not be possible to distinguish all states of an LTS with a single test case. Our experiments show that this is typically the case in practice, but nevertheless more than 99% of the incompatible state pairs are distinguished by the constructed test case. Following [11], we show that our algorithms constructs a test case distinguishing all incompatible state pairs, if it exists.

Related work

There are (at least) three ortogonal ways in which the classical FSM (or Mealy machine) model can be generalized.

A first generalization is to add nondeterminism. Whereas an FSM has exactly one outgoing transition for each state $q$ and input $i$, a nonderministic FSM allows for more than one transition. Alur, Courcoubetis & Yannakakis [1] propose an algorithm to generate adaptive distinguishing sequences for nondeterministic FSMs, using (overlapping) subsets of states, similar to our algorithm. However, their sequences only distinguish pairs of states, and are not designed to distinguish more states at the same time. In between FSMs and nondeterministic FSMs we find the observable FSMs, which have at most one outgoing transition for each state $q$, input $i$ and output $o$; one may use a determinization construction to convert any nondeterministic FSM into an observable one. The LTSs that we consider have observable nondeterminism.

A second generalization of FSMs is to relax the requirement that each input is enabled in each state. In a partial FSM, states do not necessarily have outgoing transitions for every state and every input. Petrenko & Yevtushenko [17] derive complete test suites for partial, observable FSMs, which is the closest to the automata model that we study in this paper. Their test generation is based on (adaptive) state counting [10], which is a trace search-based method which recognizes when states are distinguished, but does not provide a constructive way to build a test that distinguishes (many) states at once. Yannakakis & Lee [26] present a randomized algorithm which generates, with high probability, checking sequences, i.e., $n$-complete test suites consisting of a single sequence. This approach is also applicable to partial FSMs, as opposed to the adaptive distinguishing sequence construction algorithms of [11], which apply to plain FSMs.

A third generalization of FSMs is to relax the requirement that inputs and outputs alternate. In our LTS, inputs and outputs may occur in arbitrary order. Bensalem, Krichen & Tripakis [19] give an algorithm for extracting adaptive distinguishing sequences for all states of a given LTS, by translating back and forth between a corresponding Mealy machine. This translation is only possible, if all states of the LTS have at most one outgoing output transition. Van den Bos, Janssen & Moerman [4] do not need such a restriction. They propose an algorithm that generates an adaptive distinguishing sequence for all pairs of incompatible states. In this paper, we generalize the result of [4] to distinguish more states at the same time.

2 Preliminaries

We write $f:X\rightharpoonup Y$ to denote that $f$ is a partial function from $X$ to $Y$. We write $f(x)\downarrow$ to mean $\exists y:f(x)=y$, i.e., the result is defined, and $f(x)\uparrow$ if the result is undefined. We often identify a partial function $f$ with the set of pairs $\{(x,y)\in X\times Y\mid f(x)=y\}$.

If $\Sigma$ is a set of symbols then $\Sigma^{\ast}$ denotes the set of all finite words over $\Sigma$. The empty word is denoted by $\epsilon$, the word consisting of symbol $a\in\Sigma$ is denoted $a$, and concatenation of words is denoted by juxtaposition.

Throughout this article, we use standard notations and terminology related to finite directed graphs (digraphs) and finite directed acyclic graphs (DAGs), as for instance defined in [6, 2]. If $G=(V,E)$ is a digraph and $v\in V$, then we let $\mathit{Post}_{G}(v)$, or briefly $\mathit{Post}(v)$, denote the set of direct successors of $v$, that is, $\mathit{Post}(v)=\{w\in V\mid(v,w)\in E\}$. Similarly, $\mathit{Pre}_{G}(v)$, or briefly $\mathit{Pre}(v)$, denotes the set of direct predecessors of $v$, that is, $\mathit{Pre}(v)=\{w\in V\mid(w,v)\in E\}$. Vertex $v$ is called a root if $\mathit{Pre}(v)=\emptyset$, a leaf if $\mathit{Post}(v)=\emptyset$, and internal if $\mathit{Post}(v)\neq\emptyset$. We write $\textit{leaves}(G)=\{v\in V\mid\mathit{Post}(v)=\emptyset\}$, and $\textit{internal}(G)=V\setminus\textit{leaves}(G)$.

The automata considered this paper are deterministic, finite labeled transition systems with transitions that are labeled by inputs or outputs. Since a single state may have outgoing transitions labeled with different outputs, and since outputs are not controllable, the behavior of our automata is nondeterministic: in general, for a given sequence of inputs, the resulting sequence of outputs is not uniquely determined. Nevertheless, our automata are deterministic in the sense of classical automata theory: for any observed sequence of inputs and outputs the resulting state is uniquely determined. We say that our automata have observable nondeterminism.

Because the inputs and outputs will be fixed throughout this article, we fix $I$ and $O$ as nonempty, disjoint, finite sets of input and output labels, respectively, and write $L=I\cup O$. We will use $a,b$ to denote input labels, $x,y,z$ to denote output labels, and $\mu$ for labels that are either inputs or outputs.

Definition 1

An automaton (with inputs and outputs) is a triple $A=(Q,T,q_{0})$ with $Q$ a finite set of states, $T:Q\times L\rightharpoonup Q$ a transition function, and $q_{0}\in Q$ the initial state. We associate a digraph to $A$ as follows

[TABLE]

Concepts and notations for $\mathit{digraph}(A)$ extend to $A$. Thus we say, for instance, that automaton $A$ is acyclic when $\mathit{digraph}(A)$ is acyclic, and we write $\mathit{Post}(q)$ for the set of direct successors of a state $q$. For $A=(Q,T,q_{0})$ and $q\in Q$ we write $A/q$ for $(Q,T,q)$, that is, the automaton obtained from $A$ by replacing the initial state by $q$.

Figure 1 shows an example automaton. Below, we recall the definitions of some basic operations on (sets of) automata states. Operations $\mathit{in}$, $\mathit{out}$ and $\mathit{init}$ retrieve all the inputs, outputs, or labels enabled in a state, respectively. To every set of states $P$ and every sequence of labels $\sigma$ we can associate three sets of states: $P\text{ }\textit{after}\text{ }\sigma$, $P\text{ }\textit{before}\text{ }\sigma$, and $\textit{enabled}(P,\sigma)$. The set $P\text{ }\textit{after}\text{ }\sigma$ comprises all states that can be reached starting from a state of $P$ via a path with trace $\sigma$, whereas the set $P\text{ }\textit{before}\text{ }\sigma$ consists of all the states from where it is possible to reach a state in $P$ via a trace in $\sigma$, and $\textit{enabled}(P,\sigma)$ consists of all states in $P$ from where a path with trace $\sigma$ is possible. The traces operation provides the sequences of labels that can be observed from one or more of the states. We use a subscript if confusion may arise due to the use of several automata in the same context, e.g. $\textit{out}_{A}(q)$ denotes the enabled outputs of $q$ in automaton $A$.

Definition 2

Let $A=(Q,T,q_{0})$ be an automaton, $q\in Q$, $\mu\in L$ and $\sigma\in L^{*}$. Then we define:

[TABLE]

[TABLE]

Definitions are lifted to sets of states by pointwise extension. Thus, for $P\subseteq Q$, $\textit{in}(P)=\bigcup_{p\in P}\textit{in}(p)$, $P\text{ }\textit{after}\text{ }\sigma=\bigcup_{p\in P}p\text{ }\textit{after}\text{ }\sigma$, etc. We sometimes write the automaton, instead of the singleton set containing the initial state.

We find it convenient to use a fragment of Milner’s Calculus of Communicating Systems [14] as syntax for denoting acyclic automata. In particular, its recursive definition will allow us to incrementally construct test cases in Sections 5 and 6.

Definition 3

The set of expressions $E_{\mathit{CCS}}$ is defined by the BNF grammar

[TABLE]

The set $T_{\mathit{CCS}}\subseteq E_{\mathit{CCS}}\times L\times E_{\mathit{CCS}}$ is the smallest set of triples such that, for all $\mu\in L$ and $F,F^{\prime},G\in E_{\mathit{CCS}}$,

$(\mu.F,\mu,F)\in T_{\mathit{CCS}}$ 2. 2.

If $(F,\mu,G)\in T_{\mathit{CCS}}$ then $(F+F^{\prime},\mu,G)\in T_{\mathit{CCS}}$ 3. 3.

If $(F,\mu,G)\in T_{\mathit{CCS}}$ then $(F^{\prime}+F,\mu,G)\in T_{\mathit{CCS}}$

An expression $F\in E_{\mathit{CCS}}$ is deterministic iff, for all subexpressions $G$ of $F$,

[TABLE]

To each deterministic expression $F\in E_{\mathit{CCS}}$ we associate an automaton $A_{F}=(Q,T,F)$, where $Q$ is the set of subexpressions of $F$, and transition function $T$ is defined by

[TABLE]

Example 1

The CCS expression $a.(x.\mathbf{0}+y.\mathbf{0})$ has subexpressions $a.(x.\mathbf{0}+y.\mathbf{0})$, $x.\mathbf{0}+y.\mathbf{0}$, $x.\mathbf{0}$, $y.\mathbf{0}$, and $\mathbf{0}$. These are the states of its associated automaton. The automaton’s transition relation is: $\{(a.(x.\mathbf{0}+y.\mathbf{0}),a,x.\mathbf{0}+y.\mathbf{0}),(x.\mathbf{0}+y.\mathbf{0},x,\mathbf{0}),(x.\mathbf{0}+y.\mathbf{0},y,\mathbf{0})(x.\mathbf{0},x,\mathbf{0}),(y.\mathbf{0},y,\mathbf{0})\}$. Note that states $x.\mathbf{0}$ and $y.\mathbf{0}$ are not reachable from initial state $a.(x.\mathbf{0}+y.\mathbf{0})$.

Suspension automata are automata with the additional property that in each state at least one output label is enabled. We note that this requirement can be easily enforced by adding a self-loop for an additional output label, that denotes ‘no-output’ or quiescence [24], in each state that has no output transition. We note that our definition of suspension automata, which is taken from [4], is more general than the one from [24, 25], since we only require states to be non-blocking, while suspension automata from [24, 25] adhere to some additional properties associated to this special quiescence output.

Definition 4

Let $A=(Q,T,q_{0})$ be an automaton. We call a state $q\in Q$ blocking if $\textit{out}(q)=\emptyset$, and call $A$ non-blocking if none of its states is blocking. A non-blocking automaton is also called a suspension automaton.

We will use suspension automata as the specifications to derive test cases from. Figure 1 shows a suspension automaton. Plain automata are sometimes used as an intermediate structure to do computations, and test cases will be acyclic automata adhering to some additional properties.

3 Validity and Compatibility

In this section, we recall the definitions of the related notions of validity and compatibility [4]. We first give an efficient algorithm for computing valid states. After that, we show how the relation between validity and compatibility can be used to efficiently compute all pairs of compatible states occurring in a suspension automaton. We will need this last relation when constructing test cases to distinguish incompatible states.

3.1 Validity

We consider the following 2-player concurrent game, which is a minor variant of reachability games studied e.g., in [13, 5]. Two players, the tester and the System Under Test (SUT), play on a state space consisting of an automaton $A=(Q,T,q_{0})$. At any point during the game there is a current state, which is $q_{0}$ initially. To advance the game, both the tester and the SUT choose an action from the current state $q$:

• •

The tester chooses either an input from $\textit{in}(q)$, or the special action $\theta\not\in L$. By choosing $\theta$, the tester indicates that she performs no input and allows the SUT to execute any output he wishes.

• •

The SUT chooses an output from $\textit{out}(q)$, or $\theta$ if no output is possible.

The game moves to a next state according to the following rule (this is the input-eager assumption from [5]): If the tester chooses an enabled input $a$ this will be executed, i.e., the current state changes to $T(q,a)$; if the SUT chooses an enabled output $x$ this will only be executed when the tester has chosen $\theta$, in this case the current state changes to $T(q,x)$; when both players choose $\theta$, the game terminates. The tester wins the game if she reaches a blocking state, and the SUT wins if he has a strategy that ensures that the tester will never win. A (memoryless) strategy for the tester is a function ${\mathit{m}ove}:Q\rightarrow I\cup\{\theta\}$. We say a strategy is winning if the tester will always win the game (within a finite number of moves) when selecting actions according to this strategy, no matter which actions the SUT takes. Following Beneš et al [3] and Van den Bos et al [4], we call states for which the tester has a winning strategy invalid, and the remaining states in $Q$ valid. The sets of valid and invalid states are characterized by the following lemma (cf Proposition 2.18 of [13]):

Lemma 1

Let $A=(Q,T,q_{0})$ be an automaton.

The set of invalid states of $A$ is the smallest set $P\subseteq Q$ such that $q\in P$ if

[TABLE] 2. 2.

The set of valid states of $A$ is the largest set $P\subseteq Q$ such that $q\in P$ implies

[TABLE]

Based on Lemma 1(1), Algorithm 1 computes the set of invalid states of an automaton $A$ and, for each invalid state $q$, the first move $\mathit{move}(q)$ of a winning strategy for the tester, as well as the maximum number $\mathit{level}(q)$ of moves required to win the game.

Algorithm 1 is a minor variation of the classical algorithm for computing attractor sets and traps in 2-player concurrent games [13] and the procedure described by Beneš et al [3], which takes as input an automaton, of which each state $q$ has $\textit{in}(q)=L_{I}$, and prunes away invalid states. Key invariants of the while-loop of lines 13-33 are that states in $W\cup P$ are invalid, and for $q\in Q\setminus(P\cup W)$, $\mathit{count}(q)$ gives the number of output transitions to states in $Q\setminus P$.

Let $n$ be the number of states in $Q$, and $m$ the number of transitions in $T$. We assume, for convenience, that $m\geq n$. If we use an adjacency-list representation of $A$ and represent the set of incoming transitions using a linked list, then the time complexity of the initialization part (lines 2-11) is $\mathcal{O}(m)$. The while-loop (lines 13-33) visits each transition of $A$ at most twice (in lines 15 and 26) and performs a constant amount of work. Thus the time complexity of the while loop is $\mathcal{O}(m)$. This means that the time complexity of Algorithm 1 is also $\mathcal{O}(m)$.

The next lemma states some basic properties of the $\mathit{level}$ function that records the maximum number of moves required to win.

Lemma 2

Let $A=(Q,T,q_{0})$ be an automaton and $P\subseteq Q$ the set of invalid states of $A$. Let $\mathit{move}$ and $\mathit{level}$ be as computed by Algorithm 1. Then, for all $q\in P$ and $a\in I$,

$\mathit{level}(q)=0~{}\Leftrightarrow~{}q$* is blocking,* 2. 2.

$\mathit{level}(q)>0\wedge\mathit{move}(q)=a~{}\Rightarrow~{}T(q,a)\in P\wedge\mathit{level}(T(q,a))<\mathit{level}(q)$, 3. 3.

$\mathit{level}(q)>0\wedge\mathit{move}(q)=\theta~{}\Rightarrow~{}\forall x\in\textit{out}(q):\mathit{level}(T(q,x))<\mathit{level}(q)$.

3.2 Compatibility

Two states of a suspension automaton are compatible [18, 20] if a tester may not be able to distinguish them in the presence of an adversarial SUT. For example, if the tester wants to determine whether the SUT behaves according to state 2 or 3 of the suspension automaton of Figure 1, taking output transition $x$ will result in reaching state 4, from both states, but after reaching state 4, it cannot be determined, from which of the two states the $x$ transition was taken. Hence, states 2 and 3 are compatible.

Definition 5

Let $(Q,T,q_{0})$ be a suspension automaton. A relation $R\subseteq Q\times Q$ is a compatibility relation if for all $(q,q^{\prime})\in R$ we have

[TABLE]

Two states $q,q^{\prime}\in Q$ are compatible, denoted $q\mathrel{\Diamond}q^{\prime}$, if there exists a compatibility relation $R$ relating $q$ and $q^{\prime}$. Otherwise, the states are incompatible, denoted by $q\not\mathrel{\Diamond}q^{\prime}$. For $P\subseteq Q$ a set of states, we write $\Diamond(P)$ to denote that all states in $P$ are pairwise compatible, i.e., $\forall q,q^{\prime}\in P:q\mathrel{\Diamond}q^{\prime}$.

We note that the compatibility relation is symmetric and reflexive, but not transitive. For an elaborate discussion of compatibility, we refer the reader to [4]. The notions of compatibility and validity can be related using the following synchronous composition operator:

Definition 6

Let $A_{1}=(Q_{1},T_{1},q^{1}_{0})$ and $A_{2}=(Q_{2},T_{2},q^{2}_{0})$ be automata. The synchronous composition of $A_{1}$ and $A_{2}$, notation $A_{1}\|A_{2}$, is the automaton $A=(Q_{1}\times Q_{2},T,(q^{1}_{0},q^{2}_{0}))$, where transition function $T$ is given by:

[TABLE]

The next lemma asserts that states $q$ and $q^{\prime}$ are compatible precisely when the pair $(q,q^{\prime})$ is a valid state of $S$ composed with itself.111This is a variation of Lemma 22 from [4], which is stated for a slightly different composition operator that involves demonic completions. Adding demonic completions is useful in the setting of [4], but not needed for our purposes.

Lemma 3

Let $S=(Q,T,q_{0})$ be a suspension automaton with $q,q^{\prime}\in Q$. Then $q\mathrel{\Diamond}q^{\prime}$ if and only if $(q,q^{\prime})$ is a valid state of $S\|S$.

Proof

($\Leftarrow$) Suppose that $(q,q^{\prime})$ is a valid state of $S\|S$. Then, by Lemma 1(1), $(q,q^{\prime})$ is contained in the largest subset $P$ of the states of $S\|S$ that satisfies the conditions of Lemma 1(2). Using Definition 6, we infer that, for all $(r,r^{\prime})\in P$:

[TABLE]

But this means that $P$ is a compatibility relation, and therefore $q\mathrel{\Diamond}q^{\prime}$.

($\Rightarrow$) Suppose that $q\mathrel{\Diamond}q^{\prime}$. Then, by Definition 5, there exists a compatibility relation $R$ relating $q$ and $q^{\prime}$. Since $R\subseteq Q\times Q$, $R$ is a subset of the set of states of $S\|S$. By combining Definitions 5 and 6, we infer that $R$ is the set $P$ from Lemma 1(2). This implies that $(q,q^{\prime})$ is a valid state of $S\|S$. ∎

Example 2

Figure 2 shows the synchronization of the suspension automaton of Figure 1. It has 6 valid states, and in particular it shows that $2\mathrel{\Diamond}3$.

Lemma 3 suggests an efficient algorithm for computing compatibility of states. Suppose $S$ is a suspension automaton with $n$ states and $m$ transitions, with $m\geq n$. Then we may compute composition $S\|S$ in time $\mathcal{O}(m(n+\log m))$. The idea is that we first sort the list of transitions on the value of their action label, which takes $\mathcal{O}(m\log m)$ time. Next we check for each transition $t=(q,\mu,q^{\prime})$ what are the possible transitions that may synchronize with $t$. Since $t$ may only synchronize with $\mu$-transitions, and since there are at most $n$ $\mu$-transitions (as $S$ is deterministic), we may compute the list of transitions of the composition in $\mathcal{O}(mn)$ time. Thus, the overall time complexity of computing $S\|S$ is $\mathcal{O}(m(n+\log m))$. The composition $S\|S$ has $n^{2}$ states and $\mathcal{O}(mn)$ transitions. Next we use Algorithm 1 to compute the set of invalid states of $S\|S$, which requires $\mathcal{O}(mn)$ time. Two states $q$ and $q^{\prime}$ of $S$ are compatible iff $(q,q^{\prime})$ is not in this set. Altogether, we need $\mathcal{O}(m(n+\log m))$ time to compute the compatible state pairs.

4 Test Cases

In this section, we introduce a simple notion of test cases. The goal of these test cases is state identification, i.e., to explore whether a state of the SUT, that is reached after some initial interactions, has the same traces as the state where it should be according to a given suspension automaton. Our test cases are adaptive in the sense that inputs that are sent to the SUT may depend on previous outputs generated by the SUT. They are similar to the adaptive distinguishing sequences of Lee & Yannakakis [11], except that inputs and outputs do not necessarily alternate, and the graph structure is a DAG rather than a tree.

Definition 7

A test case is an acyclic automaton $A=(Q,T,q_{0})$ such that each state $q\in Q$ enables either a single input action, or zero or more output actions. We refer to states that enable a single input as input states, and states that enable at least one output as output states. Thus each state from a test case is either an input state, an output state, or a leaf.

To each test case $A$ we associate a set of observations: maximal traces that we may observe during a run of $A$.

Definition 8

For each test case $A$, $\textit{Obs}(A)$ is the set of traces that reach a leaf of $A$: $\textit{Obs}(A)=\{\sigma\in\textit{traces}(A)\mid A\text{ }\textit{after}\text{ }\sigma\subseteq\textit{leaves}(A)\}$.

Given a suspension automaton $S$, we only want to consider test cases $A$ that are consistent with $S$ in the sense that each input that is provided by $A$ is also specified by $S$, and conversely each output that is allowed by $S$ also occurs in $A$.

Definition 9

Let $A=(Q,T,q_{0})$ be a test case and $S=(Q^{\prime},T^{\prime},q^{\prime}_{0})$ a suspension automaton. We say that $A$ is a test case for $S$ if, for each state $(q,q^{\prime})$ of $A\|S$ reachable from the initial state $(q_{0},q^{\prime}_{0})$:

• •

if $q$ is an input state then $\textit{in}(q)\subseteq\textit{in}(q^{\prime})$,

• •

if $q$ is an output state then $\textit{out}(q^{\prime})\subseteq\textit{out}(q)$.

We say $A$ is a test case for state $q^{\prime}\in Q^{\prime}$ if $A$ is a test case for $S/q^{\prime}$. Furthermore, $A$ is a test case for a set of states $P\subseteq Q^{\prime}$ if $A$ is a test case for all $q^{\prime}\in P$.

Lemma 4

Suppose $A=(Q,T,q_{0})$ is a test case for a set $P$ of states of suspension automaton $S$. Suppose that $T(q_{0},\mu)=q_{1}$, for some label $\mu$ and state $q_{1}$. Then $A/q_{1}$ is a test case for $P\text{ }\textit{after}\text{ }\mu$.

If $A$ is a test case for a suspension automaton $S$ then the composition $A\|S$ is also a test case. We can view $A\|S$ as the subautomaton of $A$ in which all outputs that are not enabled in $S$ have been pruned away. A test case distinguishes two states, if the states enable different observable traces of the test case.

Lemma 5

If $A$ is a test case for a suspension automaton $S$, then the composition $A\|S$ is also a test case for $S$, satisfying $\textit{Obs}(A\|S)\subseteq\textit{Obs}(A)$.

Definition 10

Let $A$ be a test case for states $q$ and $q^{\prime}$ of suspension automaton $S$. Then $A$ distinguishes $q$ and $q^{\prime}$ if $\textit{Obs}(A\|(S/q))\cap\textit{Obs}(A\|(S/q^{\prime}))=\emptyset$.

Example 3

The associated automaton of the CCS expression $a.(x.\mathbf{0}+y.\mathbf{0})$ (see Example 1) is a test case for states 1 and 2 of the suspension automaton from Figure 1. Its observable traces are $\{ax,ay\}$, and it distinguishes states 1 and 2.

Lemma 6

Let $S=(Q,T,q_{0})$ be a suspension automaton with $q,q^{\prime}\in Q$. Then $q\not\mathrel{\Diamond}q^{\prime}$ iff there exists a test case that distinguishes $q$ and $q^{\prime}$.

Proof

By Lemma 3, $q\not\mathrel{\Diamond}q^{\prime}$ iff the pair $(q,q^{\prime})$ is an invalid state of $S\|S$. By definition, this means that in the game for $S\|S$ the tester has a winning strategy $\mathit{move}$. This strategy can be effectively computed by Algorithm 1. Using strategy $\mathit{move}$, we compute a test case $A$ as follows:

• •

The set of states consists of the set $P$ of invalid states of $S\|S$, extended with a single leaf state $l$.

• •

The initial state is $(q,q^{\prime})$.

• •

The transition relation of $A$ is obtained by (a) restricting the transition relation of $S\|S$ to $P$, (b) removing all input transitions, except the outgoing transitions with label $\mathit{move}(r,r^{\prime})$ from states with $\mathit{move}(r,r^{\prime})\in I$, (c) adding an output transition $((r,r^{\prime}),x,l)$ for each $(r,r^{\prime})\in P$ and $x\in O$ such that $\mathit{move}(r,r^{\prime})=\theta$ and $(r,r^{\prime})$ does not have an outgoing $x$-transition.

It is routine to check that $A$ is a test case for states $q$ and $q^{\prime}$ of $S$. We claim that $A$ distinguishes $q$ and $q^{\prime}$, that is, $\textit{Obs}(A\|S/q)\cap\textit{Obs}(A\|S/q^{\prime})=\emptyset$. Because suppose $\sigma\in\textit{Obs}(A\|S/q)$. Then $\sigma$ corresponds to a run from initial state $(q,q^{\prime})$ of $A$ to leaf node $l$. By construction of $A$, $\sigma$ must be of the form $\rho x$, where $\rho$ corresponds to a run in $A$ from $(q,q^{\prime})$ to some state $(r,r^{\prime})$ and $x\in\textit{out}(r)\setminus\textit{out}(r^{\prime})$. This means that $A\|S/q^{\prime}$ has a run with actions $\rho$ from initial state $((q,q^{\prime}),q^{\prime})$ to state $((r,r^{\prime}),r^{\prime})$. However, since $x\not\in\textit{out}(r^{\prime})$, $\sigma\not\in\textit{Obs}(A\|S/q^{\prime})$. By a symmetric argument, we may conclude that $\sigma\in\textit{Obs}(A\|S/q^{\prime})$ implies $\sigma\not\in\textit{Obs}(A\|S/q)$. Thus $\textit{Obs}(A\|S/q)\cap\textit{Obs}(A\|S/q^{\prime})=\emptyset$, as required. ∎

The following definition generalizes the notion of adaptive distinguishing sequence for FSM’s [9, 11] to the setting of suspension automata.

Definition 11

Let $S=(Q,T,q_{0})$ be a suspension automaton, $P\subseteq Q$, and $A$ a test case for $P$. We say that $A$ is an adaptive distinguishing graph for $P$ if, for all $q,q^{\prime}\in P$ with $q\not\mathrel{\Diamond}q^{\prime}$, $A$ distinguishes $q$ and $q^{\prime}$. Test case $A$ is an adaptive distinguishing graph for $S$ if it is an adaptive distinguishing graph for the set $Q$ of states of $S$.

Just like there are FSMs without an adaptive distinguishing sequence, there are suspension automata for which no adaptive distinguishing graph exists. This is the case for the suspension automaton from Figure 3. We cannot construct an adaptive distinguishing graph by choosing the root node to be an output state, since states 1 and 3 cannot be distinguished, as they both go to state 2 with their single output transition $y$. The root also cannot be an input state for either of all inputs $a$ or $b$. After $a$, states 1 and 2 both reach state 1, and after $b$, states 2 and 3 both reach state 3.

In the remainder of this paper, we present algorithms for constructing an adaptive distinguishing graph for $S$ from a suspension automaton $S$, if it exists.

5 Splitting Graphs

In this section, we present the concept of a splitting graph, as well as an algorithm for constructing such a graph. Our algorithm generalizes the algorithm of Lee & Yannakakis [11] for computing a splitting tree for an FSM. In the next section, we will construct an adaptive distinguishing graph by extracting its parts from the splitting graph. An adaptive distinguishing graph that distinguishes all incompatible state pairs, is only guaranteed to be found, if some additional requirements on the splitting graph construction are satisfied. We will delay the discussion of adaptive distinguishing graphs to the next section, and focus on splitting graphs first.

We will first give the definition of a splitting graph, and the outer loop of our algorithm for constructing it. Then we define when a leaf node of a splitting graph is splittable (i.e., when child nodes can be added), and show that a splittable leaf exists whenever some leaf contains incompatible states. After that, we explain how to construct the child nodes for splittable leaves.

5.1 Splitting Graph Definition

A splitting graph for suspension automaton $S=(Q,T,q_{0})$ is a directed graph in which the vertices are subsets of states of $S$; there is a single root $Q$ , and an internal node is the union of its children. We require that, for each edge $(v,c)$ of the splitting graph, $c$ is a proper subset of $v$; this implies that a splitting graph is a DAG. We associate a test case $W(v)$ to each internal node $v$ and require a tight link between the observations of $W(v)$ and the children of $v$: each observation $\sigma$ has one child $c$ that contains all states enabling $\sigma$. As we have $|c|<|v|$, this means that, after following any trace $\sigma$ from test case $W(v)$, the states $v\setminus c$ have been distinguished from states from the states $c$.

Definition 12

A splitting graph for suspension automaton $S=(Q,T,q_{0})$ is a triple $Y=(V,E,W)$ with

• •

$Q\in V\subseteq\mathcal{P}(Q)\setminus\emptyset$

• •

$E\subseteq V\times V$ such that

$Q$ is the only root of $Y$, 2. 2.

$(v,w)\in E\implies v\supset w$, and 3. 3.

$v\in\textit{internal}(Y)\implies v=\bigcup\mathit{Post}(v)$.

• •

$W:\textit{internal}(Y)\rightarrow E_{\mathit{CCS}}$ is a witness function such that, for all internal vertices $v$, $A_{W(v)}$ is a test case such that:

$\forall\sigma\in\textit{Obs}(A_{W(v)}),\exists c\in\mathit{Post}(v):\textit{enabled}(c,\sigma)=\textit{enabled}(v,\sigma)$.

Splitting graph $Y$ is complete if, for each leaf $l$, the states contained in $l$ are pairwise compatible, i.e., $\Diamond(l)$.

Algorithm 2 shows the main loop for constructing a splitting graph for a given suspension automaton. The idea is to start with the trivial splitting graph with just a single node, and then repeatedly split leaf nodes, i.e., add child nodes, until all leaves only contain pairwise compatible states. This means that incompatible states are in different leaves when the algorithm terminates. Since nodes in a splitting graph are finite sets of states, and children are strict subsets of their parents, Algorithm 2 terminates after a finite number of refinements. With $\bot$, we denote the empty function.

5.2 Splitting Conditions

Before we elaborate on the algorithm for the method splitnode, we first explore what conditions should hold for a leaf $l$ to be splittable. The formal definition of these conditions is given below in Definition 14.

If we are lucky we can find, for each output $x\in\textit{out}(l)$, a state $q\in l$ that does not enable $x$. In this case, observing an output allows us to distinguish at least one state from some other states. Otherwise, we may check whether, for certain enabled inputs, or all outputs, the states of $l$ have a transition to the states of an internal node, i.e., a node that has already been split, because $l$ then may be split as well when these labels occur. In particular, the states of $l$ can be split for some label $\mu$ if the reached node is a least common ancestor of $l\text{ }\textit{after}\text{ }\mu$. An internal node $v$ is least common ancestor for a set of states $P$ if it contains $P$ but none of its children does.

Definition 13

Let $Y$ be a splitting graph for suspension automaton $S$ and let $P$ be a set of states of $S$. An internal node $v$ of $Y$ is a least common ancestor of $P$ if $P\subseteq v$ and, for all $c\in\mathit{Post}(v)$, $P\not\subseteq c$. We write $LCA(Y,P)$ for the set of least common ancestors of $P$ contained in $Y$.

Note that we can compute the set of least common ancestors for any set $P$ in a time that is linear in the size of the splitting graph.

Definition 14

Let $Y$ be a splitting graph for suspension automaton $S$.

A leaf $l$ of $Y$ is splittable on output if

[TABLE] 2. 2.

A leaf $l$ of $Y$ is splittable on input if

[TABLE]

A leaf $l$ of $Y$ is splittable if it is splittable on output or splittable on input.

Lemma 7

Each incomplete splitting graph has a splittable leaf.

Proof

Let $Y$ be an incomplete splitting graph for suspension automaton $S=(Q,T,q_{0})$. Since $Y$ is incomplete, there is at least one leaf that contains a pair of incompatible states. By Lemma 3, we have that for all states $q,q^{\prime}$ of $S$, $q\not\mathrel{\Diamond}q^{\prime}$ iff $(q,q^{\prime})$ is an invalid state of $S\|S$. Using Algorithm 1, we may therefore compute the pairs of incompatible states of $S$ and functions $\mathit{move}$ and $\mathit{level}$ on these pairs. Let $l$ be the leaf node that contains a pair of incompatible states $q,q^{\prime}$ for which the value $\mathit{level}(q,q^{\prime})$ is minimal. We claim that $l$ is a splittable leaf of $Y$. There are three cases:

Suppose $\mathit{level}(q,q^{\prime})=0$. Then, by Lemma 2(1), $(q,q^{\prime})$ is a blocking state of $S\|S$. This implies that $\textit{out}(q)\cap\textit{out}(q^{\prime})=\emptyset$. But this means that, for each output action $x$, either $x\not\in\textit{out}(q)$ or $x\not\in\textit{out}(q^{\prime})$. Therefore, $l$ can be split on output. 2. 2.

Suppose $\mathit{level}(q,q^{\prime})>0$ and $\mathit{move}(q,q^{\prime})=a\in I$. Then, by Lemma 3 and Lemma 2(2), both $q$ and $q^{\prime}$ enable input $a$ and, writing $r=T(q,a)$ and $r^{\prime}=T(q^{\prime},a)$, we have $r\not\mathrel{\Diamond}r^{\prime}$, $\{r,r^{\prime}\}\subseteq l\text{ }\textit{after}\text{ }a$, and $\mathit{level}(r,r^{\prime}))<\mathit{level}(q,q^{\prime})$. Since none of the leaves contains a pair of incompatible states with a $\mathit{level}$ value smaller than $(q,q^{\prime})$, we know that $Y$ does not have a leaf node that contains both $r$ and $r^{\prime}$. But this implies that $LCA(Y,l\text{ }\textit{after}\text{ }a)\neq\emptyset$, and so $l$ can be split on input. 3. 3.

Suppose $\mathit{level}(q,q^{\prime})>0$ and $\mathit{move}(q,q^{\prime})=\theta$. Let $x\in\textit{out}(l)$. If there exists an $s\in l$ such that $x\not\in\textit{out}(s)$ then we may split on output. Otherwise, both $q$ and $q^{\prime}$ enable output $x$. Write $r=T(q,x)$ and $r^{\prime}=T(q^{\prime},x)$. Then $\{r,r^{\prime}\}\subseteq l\text{ }\textit{after}\text{ }x$ and $r\not\mathrel{\Diamond}r^{\prime}$. By Lemma 3 and Lemma 2(2), $\mathit{level}(r,r^{\prime})<\mathit{level}(q,q^{\prime})$. Since none of the leaves contains a pair of incompatible states with a $\mathit{level}$ value smaller than $(q,q^{\prime})$, we know that $Y$ does not have a leaf node containing both $r$ and $r^{\prime}$. But this implies that $LCA(Y,l\text{ }\textit{after}\text{ }x)\neq\emptyset$, so $l$ can be split on output. ∎

5.3 Splitting Graph Construction

Based on the condition of Definition 14 that holds, we assign children to splittable leaf nodes, and update the witness function. This is worked out in the method splitnode of Algorithm 3. The algorithm may choose nondeterministically between a split on output or a split on input, if both are possible. Such a choice is denoted with the syntax for guarded commands [7], i.e., as the guards on lines 5 and 16, and their respective statements on lines 6-15, and 17-20.

If a leaf $l$ is split on output, then children are added for each output $x\in\textit{out}(l)$. If $\textit{enabled}(l,x)\neq l$, then we add $\textit{enabled}(l,x)$ as a child, as those are the only states from which $x$ can be observed. We also add (i.e., by using +) the term $x.\mathbf{0}$ to the witness of $l$, as observing $x$ distinguishes states in $\textit{enabled}(l,x)$ from states in $l\setminus\textit{enabled}(l,x)$.

If $\textit{enabled}(l,x)=l$, observing $x$ will not distinguish any states. We then use that there is a $v\in LCA(Y,l\text{ }\textit{after}\text{ }x)$, which means that some states of $l\text{ }\textit{after}\text{ }x$ are distinguished by the witness $W(v)$. Hence, by taking output $x$, followed by $W(v)$, some states of $l$ are distinguished. Therefore, we add $x.W(v)$ to the witness of $l$, and split $l$ in the same way $v$ was split, i.e., if $d\subseteq l$ are all the states with $d\text{ }\textit{after}\text{ }x\subseteq c$ for some child $c\in\mathit{Post}(v)$, then $d$ is a child of $l$. We call such a split an induced split.

For splitting on some input $a$, we also use an induced split to obtain the children for $l$. Since there exists some $v\in LCA(Y,l\text{ }\textit{after}\text{ }a)$, at least two states of $l$ may be distinguished by the witness constructed for $v$, after taking input $a$. To each element of the induced split, we add all the states not enabling $a$. If we would not do this, Algorithm 3 may assign the empty set as children to a splittable leaf, such that it remains a leaf. As a consequence, Lemma 8 and also Corollary 1 then do not hold. This will be illustrated by Example 5. Corollary 1 shows termination of our splitting graph construction algorithm. It follows from the consecutive application of Lemma 8.

Definition 15

Let $Y$ be a splitting graph for suspension automaton $S$. Let $v$ be an internal node of $Y$, $P$ a set of states of $S$, and $\mu\in L$, such that $P\text{ }\textit{after}\text{ }\mu\subseteq v$. Then the induced split of $P$ with $\mu$ to $v$ is:

[TABLE]

Example 4

We compute the splitting graph of the suspension automaton from Figure 1, using Algorithm 2, and show the result in Figure 4(left).

For the root node $\{1,2,3,4\}$, we observe that state 4 does not enable $x$, while states 2 and 3 do not enable $y$. Hence, the root is split on output, gets children $\{1,2,3\}$ and $\{1,4\}$, and witness $x.\mathbf{0}+y.\mathbf{0}$.

Node $\{1,2,3\}$ can be split on input $a$, as states 1 and 2 enable $a$, and since the root node is an LCA of $\{1,2,3\}\text{ }\textit{after}\text{ }a$: from $T(1,a)=3$ and $T(2,a)=4$, we obtain that the root node is an LCA, since $\{3,4\}\subseteq\{1,2,3,4\}$, but $\{3,4\}\not\subseteq\{1,2,3\}$, and $\{3,4\}\not\subseteq\{1,4\}$. The induced split is $\{\{1\},\{2\}\}$. We then need to add state 3 to both sets, because state 3 does not enable $a$, so node {1,2,3} gets children {1,3} and {2,3}. Prepending $a$ to the witness of the root node gives us witness $a.(x.\mathbf{0}+y.\mathbf{0})$ for $\{1,2,3\}$.

Node $\{1,4\}$ can be split on output. As state 4 does not enable $x$, we only need to find an LCA for $\{1,4\}\text{ }\textit{after}\text{ }y=\{1,2\}$, which is the previously split node $\{1,2,3\}$. For $x$ we have witness $x.\mathbf{0}$, and for $y$ we use the witness of $\{1,2,3\}$, so the witness for {1,4} is $x.\mathbf{0}+y.a.(x.\mathbf{0}+y.\mathbf{0})$.

Next, node {1,3} can be split on output using {1,4} as LCA for $x$. Node {2,3} does not need to be split, as we have $2\mathrel{\Diamond}3$. All other leaves are singletons, so we have obtained a complete splitting graph.

Example 5

Figure 5 shows that using only the induced split as children, for splitting a leaf on input, results in an incomplete splitting graph. The construction of the splitting graph goes as follows. The root node {1,2,3,4,5} can be split on output, as each state only enables one of the three outputs $x$, $y$, and $z$: we obtain children {{1,2,7},{8},{3,4,5,6}}. Leaf {1,2,7} can be split on output, as $\{1,2,7\}\text{ }\textit{after}\text{ }x=\{1,2,8\}$ shows that we can use the root node as LCA. Leaf {3,4,5,6} cannot be split on output as $\{3,4,5,6\}\text{ }\textit{after}\text{ }z=\{3,4,5,6\}$, so there exists no LCA for $\{3,4,5,6\}\text{ }\textit{after}\text{ }z$. It can be split on input $a$: $\{3,4,5,6\}\text{ }\textit{after}\text{ }a=\{7,8\}$, so we can use the root node as LCA. Then $\Pi(\{3,4,5,6\},a,\{1,2,3,4,5\})=\{\{5\},\{6\}\}$, so these are added as children. It remains to split {1,2}, as they are incompatible: a test case with observations $\{azzax,azzay\}$ distinguishes 1 and 2. Leaf {1,2} cannot be split on input, as $\{1,2\}\text{ }\textit{after}\text{ }x=\{1,2\}$, so no LCA exists. For input $a$ we find that $\{1,2\}\text{ }\textit{after}\text{ }a$ = {3,4}, and {3,4,5,6} is an LCA. However, $\Pi(\{1,2\},a,\{3,4,5,6\})=\emptyset$, as both 3 and 4 are not contained in any child of {3,4,5,6}. Hence, we obtain $\mathit{Post}(\{1,2\})=\emptyset$, which means by definition that {1,2} is a leaf. Algorithm 2 will keep trying to split {1,2} indefinitely, and will hence not terminate.

Lemma 8

Algorithm 3 returns a splitting graph $Y^{\prime}$ for $S$, when given some splitting graph $Y$, such that one leaf $l$ of $Y$, has become an internal node in $Y^{\prime}$.

Proof

The input of Algorithm 3 is a splitting graph $Y$ for $S$. All the algorithm does is to take a single leaf node $l$, add children $C$ to it, and extend the evaluation function $W$ for some witness $A$ to $l$. This means that it in order to prove that Algorithm 3 returns a splitting graph, it suffices to show that (a) for all $d\in C$, $\emptyset\subset d\subset l$, (b) $l=\bigcup C$, (c) $A$ is a test case, and (d) $\forall\sigma\in\textit{Obs}(A),\exists c\in C:\textit{enabled}(c,\sigma)=\textit{enabled}(l,\sigma)$, and (e) $C\neq\emptyset$.

To prove (a) we inspect the three places in the algorithm where a new element $d$ was added to the set $C$ of children of $l$: line 8, line 12 and line 18:

• •

Line 8: In this case $x\in\textit{out}(l)$ and there exists a $q\in l$ such that output $x$ is not enabled from state $q$. This implies $\emptyset\subset d=\textit{enabled}(l,x)\subset l$, as required.

• •

Line 12: In this case, let $d\in\Pi(l,x,v)$ for some $v\in LCA(Y,l\text{ }\textit{after}\text{ }x)$. By definition of $\Pi$, $\emptyset\subset d$ and there is a $c\in\mathit{Post}_{Y}(v)$ such that $d=(c\text{ }\textit{before}\text{ }x)\cap l$. Note that this implies $d\subseteq l$. By definition of LCA, there exists a $q\in l\text{ }\textit{after}\text{ }x$ with $q\not\in c$. Because $q\in l\text{ }\textit{after}\text{ }x$, there exists a state $r\in l$ such that $T(r,x)=q$. Since $q\not\in c$, we know that $r\not\in c\text{ }\textit{before}\text{ }x$. Hence $\emptyset\subset d\subset l$, as required.

• •

Line 18: In this case, $d=e\cup(l\setminus\textit{enabled}(l,a))$, where $e\in\Pi(l,a,v)$ and $v\in LCA(Y,l\text{ }\textit{after}\text{ }a)$. By definition of $\Pi$, $\emptyset\neq e$ and there is a $c\in\mathit{Post}_{Y}(v)$ such that $e=(c\text{ }\textit{before}\text{ }a)\cap l$. This implies $\emptyset\subset d\subseteq l$. By definition of LCA, there exist $q\in l\text{ }\textit{after}\text{ }a$ such that $q\not\in c$. Because $q\in l\text{ }\textit{after}\text{ }a$, there exists a state $r\in l$ such that $T(r,a)=q$. Since $q\not\in c$, we know that $r\not\in c\text{ }\textit{before}\text{ }a$. This means $r\not\in e$ and thus $r\not\in d$. Hence $\emptyset\subset d\subset l$, as required.

For proving (b), it remains to show that $l\subseteq\bigcup C$. Choose $q\in l$. We consider two cases:

• •

A split on output was performed (line 5-15). Since $S$ is a suspension automaton, there is at least one output $x$ that is enabled in $q$. If there is another state in $l$ that does not enable $x$ then $\textit{enabled}(l,x)$ is added to $C$ and thus $q\in\bigcup C$, as required. Otherwise, sets $(c\text{ }\textit{before}\text{ }x)\cap l$ are added to $C$, for $c\in\mathit{Post}_{Y}(v)$ and some $v\in LCA(Y,l\text{ }\textit{after}\text{ }x)$. Let $r=T(q,x)$. Since $l\text{ }\textit{after}\text{ }x\subset v$ and $v=\bigcup\mathit{Post}_{Y}(v)$, there is some $c\in\mathit{Post}_{Y}(v)$ with $r\in c$. This implies $q\in(c\text{ }\textit{before}\text{ }x)\cap l$ and therefore $q\in\bigcup C$, as required.

• •

A split on input was performed (lines 16-20). In this case, the sets $e\cup(l\setminus\textit{enabled}(l,a))$ are added to $C$, for $e\in\Pi(l,a,v)$, some input $a$ and $v\in LCA(Y,l\text{ }\textit{after}\text{ }a)$. If state $q$ does not enable input $a$ then state $q$ is in each set that is added to $C$, and thus $q\in\bigcup C$, as required. Now suppose $q$ enables input $a$. Let $r=T(q,a)$. Then $r\in l\text{ }\textit{after}\text{ }a$ and thus $r\in v$. Since $v=\bigcup\mathit{Post}_{Y}(v)$, there is some $c\in\mathit{Post}_{Y}(v)$ with $r\in c$. Therefore, $q\in c\text{ }\textit{before}\text{ }x)\cap l\in\Pi(l,a,v)$, and therefore $q\in\bigcup C$, as required.

For proving (c) we again consider the two cases of splitting on output or input:

• •

If a split on output was performed, then root of $A$ is an output state, as each observation has an output prefix: on line 9 or 13 either $x.\mathbf{0}$ or $x.W(v)$ for some $v\in LCA(Y,l\text{ }\textit{after}\text{ }x)$ are added to $A$. Since $\mathbf{0}$ is a test case, and $A_{W(v)}$ is a test case since $v$ is an internal node of $Y$, $A$ is also a test case.

• •

If a split on input was performed, then the root of $A$ is an input state, as it enables a single input according to line 20: $A=A_{a.W(v)}$ for some $v\in LCA(Y,l\text{ }\textit{after}\text{ }x)$. As $A_{W(v)}$ is a test case since $v$ is an internal node of $Y$, $A$ is also a test case.

For proving (d), we inspect the three places in the algorithm where children were added to $C$, and where witness observations were added to $A$. We will show that for each added observation $\sigma$, a child $d$ constructed at the same place can be used to prove $\textit{enabled}(d,\sigma)=\textit{enabled}(l,\sigma)$.

• •

On lines 8 and 9, a child $d=\textit{enabled}(l,x)$ was added to $C$, and observation $x$ was added to $A$. Hence, for $x\in\textit{Obs}(A)$ we have child $d$ with $\textit{enabled}(d,x)=\textit{enabled}(l,x)$.

• •

On lines 12 and 13, children $d\in\Pi(l,x,v)$ are added to $C$, and observations $x\sigma$ are added to $A$ for all $\sigma\in\textit{Obs}(A_{W(v)})$, using some $v\in LCA(Y,l\text{ }\textit{after}\text{ }x)$. Since $v$ is an internal node of $Y$, there is a $c\in\mathit{Post}(v)$ such that $\textit{enabled}(c,\sigma)=\textit{enabled}(v,\sigma)$. If $c\text{ }\textit{before}\text{ }x\cap l=\emptyset$, then it holds that $(l\text{ }\textit{after}\text{ }x)\cap c=\emptyset$, so from $l\text{ }\textit{after}\text{ }x\subseteq v$ (by $v\in LCA(Y,l\text{ }\textit{after}\text{ }x$) it then follows that $\textit{enabled}(l\text{ }\textit{after}\text{ }x,\sigma)=\textit{enabled}(l,x\sigma)=\emptyset$. Hence any $d\in\Pi(l.x.v)$ can be used to show $\textit{enabled}(d,x\sigma)=\textit{enabled}(l,x\sigma)$ as $d\subseteq l$. Else, there is some $d\in\Pi(l,x,v)$ with $d=(c\text{ }\textit{before}\text{ }x)\cap l$. Let $e=c\setminus(d\text{ }\textit{after}\text{ }x)$, and observe that $e\cap(l\text{ }\textit{after}\text{ }x)=\emptyset$. From $\textit{enabled}(c,\sigma)=\textit{enabled}(v,\sigma)$ and $l\text{ }\textit{after}\text{ }x\subseteq v$ it then follows that $\textit{enabled}((d\text{ }\textit{after}\text{ }x)\cup e,\sigma)=\textit{enabled}((l\text{ }\textit{after}\text{ }x)\cup(v\setminus(l\text{ }\textit{after}\text{ }x)),\sigma)$, so $\textit{enabled}(d\text{ }\textit{after}\text{ }x,\sigma)=\textit{enabled}(l\text{ }\textit{after}\text{ }x,\sigma)$. It follows that $\textit{enabled}(d,x\sigma)=\textit{enabled}(l,x\sigma)$.

• •

On lines 19 and 20 children $d\cup(l\setminus\textit{enabled}(l,a))$ for all $d\in\Pi(l,a,v)$ are assigned to $C$, and observations $a\sigma$ are added to $A$ for all $\sigma\in\textit{Obs}(A_{W(v)})$, using some $v\in LCA(Y,l\text{ }\textit{after}\text{ }a)$. Again, since $v$ is an internal node of $Y$, there is a $c\in\mathit{Post}(v)$ such that $\textit{enabled}(c,\sigma)=\textit{enabled}(v,\sigma)$. If $l\text{ }\textit{after}\text{ }a\cap c=\emptyset$, then it follows, with similar arguments as for lines 12 and 13, that $\textit{enabled}(l\text{ }\textit{after}\text{ }a,\sigma)=\textit{enabled}(l,a\sigma)=\emptyset$. Since $\textit{enabled}(l\setminus\textit{enabled}(l,a),a)=\emptyset$, and hence also $\textit{enabled}(l\setminus\textit{enabled}(l,a),a\sigma)=\emptyset$, we can use any child $e$ from line 12 to show $\textit{enabled}(e,a\sigma)=\textit{enabled}(l,a\sigma)$. Else, there is some $d\in\Pi(l,a,v)$ with $d=(c\text{ }\textit{before}\text{ }a)\cap l$. With the same reasoning as for lines 12 and 13, we obtain $\textit{enabled}(d,a\sigma)=\textit{enabled}(l,a\sigma)$. By again using that $\textit{enabled}(l\setminus\textit{enabled}(l,a),a\sigma)=\emptyset$, we obtain $\textit{enabled}(d\cup(l\setminus\textit{enabled}(l,a)),a\sigma)=\textit{enabled}(l,a\sigma)$.

For proving (e) we consider the two cases of splitting on output or input:

• •

Suppose an output split is performed. The body of the for-loop on lines 7-14 is then executed at least once, since the algorithm only accepts suspension automata, so each state is non-blocking, and consequently $|\textit{out}(l)|\geq 1$. Hence, suppose that the for-loop is executed for some $x\in\textit{out}(l)$. To prove that $C\neq\emptyset$, we now need to show that $\{\textit{enabled}(l,x)\}\neq\emptyset$ (line 8), and that $\Pi(l,x,v)\neq\emptyset$ (line 12), using some $v\in LCA(Y,l\text{ }\textit{after}\text{ }x$ (line 11).

For line 8, we use from (a) that $\emptyset\subset\textit{enabled}(l,x)$, so $\{\textit{enabled}(l,x)\}\neq\emptyset$.

For line 12, we need to prove that there exists a $c\in\mathit{Post}(v)$ such that $(c\text{ }\textit{before}\text{ }x)\cap l\neq\emptyset$. Because there is some $v\in LCA(Y,l\text{ }\textit{after}\text{ }x)$, we have $l\text{ }\textit{after}\text{ }x\subseteq v$. Since $x\in\textit{out}(l)$, there is a $q\in l\text{ }\textit{after}\text{ }x$, so $\emptyset\subset q\text{ }\textit{before}\text{ }x\subseteq l$. Because $v=\bigcup\mathit{Post}(v)$, there is a $c\in\mathit{Post}(v)$ with $q\in c$. Hence, $q\text{ }\textit{before}\text{ }x\subseteq c\text{ }\textit{before}\text{ }x$. It then follows that $(c\text{ }\textit{before}\text{ }x)\cap l\neq\emptyset$.

• •

Suppose an input split is performed for some input $a$. We then have a $c\in\mathit{Post}(v)$ with $(c\text{ }\textit{before}\text{ }a)\cap l\neq\emptyset$, for the same reasons as given for line 12. Consequently, $\Pi(l,a,v)\neq\emptyset$. Adding the (possibly empty) set $l\setminus\textit{enabled}(l,a)$ to each element of $\Pi(l,a,v)$ results in a non-empty set $C$. ∎

Corollary 1

Algorithm 2 returns a complete splitting graph for $S$.

The algorithm of [11] constructs a splitting tree in polynomial time, because leaves of a node form a partition of that node. Our splitting graphs do not have this property. Clearly, a splitting graph for a suspension automaton with $n$ states cannot have more than $2^{n}$ nodes, as the set of nodes is a subset of $\mathcal{P}(Q)\setminus\emptyset$ by Definition 12. For $n\in\mathbb{N}$ with $n\geq 3$, consider suspension automaton $S_{n}=(\{1,\dots,n\},T_{n},1)$, where $T_{n}$ consists of the following output transitions:

[TABLE]

Figure 6 depicts suspension automata $S_{n}$ for $n=3,4,5$. We can prove Lemma 9 by showing that $S_{n}$ has a splitting graph with $2^{n-1}$ nodes.

Lemma 9

Let $S$ be a suspension automaton with $n$ states. Then a splitting graph returned by Algorithm 2 has $\mathcal{O}(2^{n})$ nodes. This bound is tight.

Proof

We already showed that a splitting graph has at most an exponential number of states. We will now prove that Algorithm 2 returns a splitting graph with exactly $2^{n-1}$ nodes for suspension automaton $S_{n}$ with $n\geq 3$:

We first note that different states are pairwise incompatible, since we can easily construct a test case identifying any of the states: observing output $n$, after having observed $i$ (other) outputs, means that the test case was executed from state $n-i$. Consequently, if a node of the split graph contains more than 1 state, it has children.

The root node is split on output, so it has children for all size $n-2$ subsets of $\{1,\ldots,n-1\}$, and it has child $\{n\}$. We now show that the split graph has nodes for all non-empty subsets of $\{1,\ldots,n-1\}$, except trivial subset $\{1,\ldots,n-1\}$.

Suppose we have a non-trivial subset $s$ of $\{1,\ldots,n-1\}$ with at least two elements. For all $x\in s$ state $x$ does not enable output $x$, but all other states of $s$ do, so we obtain child $s\setminus\{x\}$ by a split on output $x$. By repeatedly removing a single element by splitting on that element, we can show that the split graph contains a node for any nonempty, non-trivial subset of $\{1,\ldots,n-1\}$. There are $2^{n-1}-2$ nonempty, non-trivial subsets of $\{1,\ldots,n-1\}$. In addition, the split graph also has nodes $\{1,\ldots,n\}$ and $\{n\}$. Hence, in total the splitting graph has $2^{n-1}$ nodes. ∎

6 Extracting Test Cases from a Splitting Graph

Algorithm 4 retrieves CCS terms, of which the associated automata are test cases that distinguish states. The algorithm “concatenates” several CCS terms while keeping track of the current set of states. Each CCS term ensures that one state is distinguished from the rest because it lacks some output. We compute the current states for the leaves of the CCS term, and attach another CCS term to this leaf, if the current set of states consists of some incompatible pair of states. Hence in total, the automaton of the resulting CCS term distinguishes multiple pairs of states.

Example 6

We construct the adaptive distinguishing graph for the suspension automaton from Figure 1, using the splitting graph from Figure 4, which also shows the result of this example. Algorithm 4 starts with $P=\{1,2,3,4\}$ and $F=\mathbf{0}$. Hence, we search for a least common ancestor for $Q$. This will be the root node of the splitting graph, with witness $x.\mathbf{0}+y.\mathbf{0}$.

The function is then called with $F=x.\mathbf{0}+y.\mathbf{0}$, and will result in two recursive calls of the function on line 13 for $P=\{1,2,3,4\}$ and $F=x.\mathbf{0}$, and $P=\{1,2,3,4\}$ and $F=y.\mathbf{0}$ respectively. In the first case, the condition of line 10 holds, and we the function is called for $P=\{1,2,3,4\}\text{ }\textit{after}\text{ }x=\{1,4\}$ and $F=\mathbf{0}$, which means that lines 8-9 are executed next, using the only LCA for {1,4}, namely {1,4}.

The algorithm will then do some more recursive calls, checking whether the witness of {1,4} must be extended further to distinguish more states. This will not be the case, because only singleton sets are reached at the leaves of the witness, and $\mathrel{\Diamond}\{q\}$ holds for any state $q$, since $\mathrel{\Diamond}$ is reflexive. Hence, we need to prepend $x$ to the witness of {1,4} to obtain the left term of the + operator of the resulting CCS term of the algorithm: $x.(x.\mathbf{0}+y.a.(x.\mathbf{0}+y.\mathbf{0}))$.

As $P=\{1,2,3,4\}\text{ }\textit{after}\text{ }y=\{1,2\}$, its LCA {1,2,3} will be used to complete the construction of the right term of the + operator of the result.

The associated automaton of the resulting CCS term is an adaptive distinguishing graph for the suspension automaton, as it distinguishes all incompatible state pairs.

Lemma 10

Algorithm 4 terminates and outputs a CCS term $F$ that denotes a test case satisfying, for each $\sigma\in\textit{Obs}(A_{F})$, $\Diamond(Q\text{ }\textit{after}\text{ }\sigma)$.

Proof

Let $S=(Q,T,q_{0})$ be the suspension automaton, and $Y$ the splitting graph for $S$, that we provide to Algorithm 4. We note that all computations are atomic, or reducing the size of the CCS expression before making a recursive call, except line 8. However, LCAs can be computed straightforwardly: start at the root, if it is not an LCA, continue with the children containing the set of states the LCA is computed for, and repeat. This procedure always succeeds in finign an LCA, due to the following argument. Any set of states, with at least two incompatible states, has a least common ancestor in the splitting graph, as the leaves of $Y$ are sets of mutually compatible states, its root node contains all the states from $S$, and all the states of a non-leaf are contained in at least one of its children, by Definition 12.

By construction, Algorithm 4 follows the labels of each $\sigma\in\textit{Obs}(A_{W(v)})$ for nodes $v$ obtained on line 8. By the property from Definition 12 that $\textit{enabled}(c,\sigma)=\textit{enabled}(v,\sigma)$, and $c\subset v$, we see that $|P|>|P\text{ }\textit{after}\text{ }\sigma|$, so after visiting line 8 at most $|Q|-1$ times, set $P$ will only contain mutually compatible states. ∎

Algorithm 4 does not always construct an adaptive distinguishing graph for all incompatible state pairs. To ensure this, it must be able to select an “injective” splitting node as LCA on line 8. This will guarantee that a transition never maps two incompatible states to two compatible states (which cannot be distinguished any more), or that an input is used that is not enabled in some states.

Definition 16

Let $S=(Q,T,q_{0})$ be a suspension automaton, $P\subseteq Q$ a set of states, and $\mu\in L$ a label. Then $\mu$ is injective for $P$ if

[TABLE]

Analogous to the result of [11], Theorem 6.1 asserts that if an adaptive distinguishing graph exists our algorithms will find it, provided there are no compatible states. This last assumption is motivated in Example 7. We first need to establish the following lemma.

Lemma 11

Let $S$ be a suspension automaton such that all pairs of distinct states are incompatible. Suppose $A=(Q,T,q_{0})$ is an adaptive distinguishing graph for a set $P$ of states of $S$. Suppose that $T(q_{0},\mu)=q_{1}$, for some label $\mu$ and state $q_{1}$. Then $\mu$ is injective for $P$ and $A/q_{1}$ is an adaptive distinguishing graph for $P\text{ }\textit{after}\text{ }\mu$.

Theorem 6.1

Let $S$ be a suspension automaton such that all pairs of distinct states are incompatible. Then $S$ has an adaptive distinguishing graph if and only if, during construction of a splitting graph $Y$ for $S$, Algorithm 3 can and does only perform injective splits, that is, whenever Algorithm 3 splits a leaf $l$ on output, then $x$ is injective for $l$, for all $x\in\textit{out}(l)$, and whenever it splits a leaf $l$ on input $a$, then $a$ is injective for $l$. Moreover, in this case Algorithm 4 constructs an adaptive distinguishing graph for $S$, when $Y$ is given as input.

Proof

Let $S=(Q,T,q_{0})$.

($\impliedby$) Suppose splitting graph $Y=(V,E,W)$ for $S$ has been constructed using injective splits only. Then, for each internal node $v$ of $Y$, $A_{W(v)}$ is a test case for $v$: inputs performed by the test case $A_{W(v)}$ will be enabled in all the corresponding states of $S$. This means that also the CCS term $F$ computed from $Y$ by Algorithm 4 will correspond to a test case for the set $Q$ of states of $S$. Since all the splits in $Y$ are injective, we have that for any pair $q,q^{\prime}$ of incompatible states of $S$, and for any observation $\sigma$ of $A_{F}$ that is enabled in both $q$ and $q^{\prime}$, the unique state in $q\text{ }\textit{after}\text{ }\sigma$ is incompatible with the unique state in $q^{\prime}\text{ }\textit{after}\text{ }\sigma$. But since, by construction, $Q\text{ }\textit{after}\text{ }\sigma$ only contains mutually compatible states, for each observation $\sigma$ of $A_{F}$, we conclude that $A_{F}$ distinguishes $q$ and $q^{\prime}$. Therefore, $A_{F}$ is an adapaptive distinguishing graph for $S$.

($\implies$) Suppose $A=(Q^{\prime},T^{\prime},q^{\prime}_{0})$ is an adaptive distinguishing graph for $S$.

Let $Y$ be an incomplete splitting graph. We show that $Y$ has a leaf for which an injective split exists.

Assume w.l.o.g. that $A$ is a tree (any DAG can be unfolded into a tree). We associate to each node $r$ of $A$ a height, which is the length of the maximal path from $r$ to a leaf. Also, we associate to each node of $r$ a set of states from $S$ called the current set: the current set of $q^{\prime}_{0}$ is $Q$, and if the current set of state $r$ is $P$ and $T^{\prime}(r,\mu)=r^{\prime}$ then the current set of $r^{\prime}$ is $r\text{ }\textit{after}\text{ }\mu$. Lemma 11 implies that if the current set of $r$ equals $P$, $A/r$ is an adaptive distinguishing graph for $P$.

Now, amongst the leaves of $Y$ that contains a maximal number of states, choose a leaf $l$ that is contained in the current set $P$ of a node $r$ of $A$ with minimal height. We consider two cases:

• •

$r$ is an input state of $A$. Then $r$ enables a single input action $a$. Let $T^{\prime}(r,a)=r^{\prime}$. Then the current set of $r^{\prime}$ is $P\text{ }\textit{after}\text{ }a$ and the height of $r^{\prime}$ is less than the height of $r$. By Lemma 11, $a$ is injective for $P$. By definition of injectivity, $a$ is also injective for subset $l$ of $P$. Since all pairs of distinct states of $S$ are incompatible, the number of states in $l\text{ }\textit{after}\text{ }a$ equals the number of elements of $l$. Moreover, since $l\text{ }\textit{after}\text{ }a$ is contained in $P\text{ }\textit{after}\text{ }a$, and amongst the leaves of $Y$ that contains a maximal number of states $l$ is contained in the current set of a node with minimal height, $l\text{ }\textit{after}\text{ }a$ is not contained in any leaf of $Y$. Thus leaf $l$ is splittable on input $a$, and this split is injective.

• •

$r$ is an output state of $A$. Suppose $x\in\textit{out}(l)$. Then either there is a $q\in l$ such that $x\not\in\textit{out}(q)$, or the number of states in $l\text{ }\textit{after}\text{ }x$ equals the number of elements of $l$ and $l\text{ }\textit{after}\text{ }x$ is not contained in any leaf of $Y$. This means that $l$ is splittable on output, with a split that is injective for each output $x$. ∎

Example 7

Without the assumption that there are no compatible state pairs, Theorem 6.1 does not hold. The suspension automaton $S$ of Figure 7 has an adaptive distinguishing graph, but our algorithm does not find it. Note that states $2$ and $3$ are compatible, and also states $6$ and $7$ are compatible. An adaptive distinguishing graph for $S$ is denoted by CCS term $x.a.b.(z.\mathbf{0}+t.\mathbf{0})+y.a.b.(z.\mathbf{0}+t.\mathbf{0})+z.\mathbf{0}+t.\mathbf{0}$. When we construct a splitting graph for $S$, the set of all states $\{1,2,3,4,5,6,7,8\}$ will be split on output, resulting in children $\{1\}$, $\{2,3,4\}$, $\{5\}$ and $\{6,7,8\}$. Now a split of $\{2,3,4\}$ on input $b$ is not injective and a split on input $a$ is not possible since the set of LCAs is empty. Similarly, there is no injective split of $\{6,7,8\}$.

7 Experimental Results on a Case Study

In [22], an FSM model, with over 10.000 states, was learned of an industrial piece of software, called the Engine Status Manager (ESM). During the learning process, testing against the ESM posed a significant challenge: it turned out to be extremely difficult to find counterexamples for hypothesis models. Initially, existing conformance testing algorithms were used to find counterexamples for hypothesis models (random walk, W-method, Wp-method, etc), but for larger hypothesis models these methods were unsuccessful. However, adaptive distinguishing sequences as in [11], augmented with additional pairwise distinguishing sequences for states not distinguished by the adaptive sequence, were able to find the required counterexamples. Therefore, the ESM models are good candidates to show the strength of the adaptive distinguishing graphs of this paper too.

Of course, applying our adaptive distinguishing graphs directly on the Mealy machine models, would not show our capability to handle the more expressive suspension automata. We therefore transformed the FSM models in such a way that they exhibit output nondeterminism. We first split all Mealy $i/o$ transitions in two consecutive transitions $i$ and $o$, and added a self-loop output transition ‘quiescence’ (denoting absense of response) to all states only having input transitions, to make it non-blocking. To ensure determinism, information about data parameters from the ESM was added to the labels of the Mealy machine in [22]. For our experiments, we removed this information again, resulting in suspension automata with states with multiple outgoing output transitions.

For performance reasons, we reduced the Mealy machine model with a subalphabet, before applying the transformation steps described above, i.e., we removed all $i/o$ transitions with $i$ not in the subalphabet. We obtained these subalphabets from [21], which contains a figure displaying interesting subalphabets based on domain knowledge. Table 1 shows that the resulting suspension automata still have a significant size.

We applied the algorithms of this paper to obtain a splitting graph and an adaptive distinguishing graph. The splitting graph was constructed as in Algorithm 3, so without requiring injectivity of the used labels. However, in the construction of the adaptive distinguishing graph (Algorithm 4) we chose on line 8 an LCA which was injective for the most pairs of states.

Table 1 shows that there are many pairs of incompatible states to distinguish. However, the number of nodes of the splitting graph are in the order of magnitude of the number of states of the suspension automaton, and the longest observable trace (i.e., the depth) of the adaptive distinguishing graphs is not long at all. Moreover, over 99% of the pairs of incompatible states are distinguished by the adaptive distinguishing graph. This indicates that the adaptive distinguishing graphs, although constructed from a non-injective splitting graph, can be very effective in testing.

To further explore the structure of the adaptive distinguishing graph, we computed the size of each leaf: the number of automaton states, that enable the observable trace to that leaf. We note that this includes states compatible to some of the automaton states. Additionally, states may enable multiple observable traces, and hence a single state may increase the size of several leaves. Figure 8 shows the results: the x-axis displays all leaf sizes, and a column of some subalphabet shows the number of leaves of this size (y-axis). We see that the majority of leaves are of small size, while leaves of larger size occur less. We see that subalphabet InitError has the most large leaves, which could explain the adaptive distinguishing graph’s relatively large number of pairs of incompatible states not distinguished.

8 Conclusions and Future Work

We studied the state identification problem for suspension automata, generalizing results from [11]. We presented algorithms to construct test cases that distinguish all incompatible state pairs, if possible, or many, if not. Experiments suggest that this approach is quite effective.

We see several directions for future research. First, though we did apply our algorithms to instances of an industrial benchmark, we would like to apply it to different case studies as well, to further explore the applicability of our approach. We note however that there are not that many (large) LTS benchmarks available.

An open problem is to give a bound on the depth of the distinguishing graph that our algorithms constructs. For FSMs, a quadratic bound is known [11], with examples to show it is tight [23, 11]. These examples extend to our setting, as we generalize from the FSM setting, but the proof for the quadratic bound on adaptive distinguishing sequences from [11] does not.

If our algorithm returns an adaptive distinguishing graph that does not distinguish all incompatible state pairs, the question remains how to efficiently distinguish these remaining states. Graphs distinguishing pairs of states can be obtained directly from our splitting graph, or by computing them as in [4], but distinguishing all remaining pairs results in a large overhead compared to the small size of the distinguishing graph we obtained in our experiments. On the one hand, we can optimize the obtained distinguishing graph by improving the splitting graph’s quality by applying heuristics that optimize the choice of labels for splitting leaves. On the other hand, we can use causes for states not being distinguished to construct a distinguishing graph that distinguishes all or at least many of the not distinguished states.

Though our distinguishing graphs significantly improve the size of an $n$-complete test suite, the problem to compute good access sequences for such a test suite requires further research as well [4]. Due to the output nondeterminism of suspension automata, we need an input-fairness assumption, to ensure that all outputs enabled from a state may eventually be observed. However, for access sequences we rather have a more adaptive strategy, in the spirit of [5], that reacts on the outputs as produced by the tested system rightaway. Adaptively choosing access sequences means that for reaching the same state, different access sequences may be used. However, the proof of $n$-completeness of a test suite depends on using one unique access sequence for accessing the same state. It remains an open problem whether using different access sequences breaks $n$-completeness or not.