# Effectiveness for Input Output Conformance Simulation iocos

Carlos Gregorio-Rodríguez, Luis Llana, Rafael Martínez-Torres

► To cite this version:

Carlos Gregorio-Rodríguez, Luis Llana, Rafael Martínez-Torres. Effectiveness for Input Output Conformance Simulation iocos. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. pp.100-116, 10.1007/978-3-662-43613-4_7. hal-01398009

HAL Id: hal-01398009

https://inria.hal.science/hal-01398009

Submitted on 16 Nov 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Effectiveness for input output conformance simulation iocos\*

Carlos Gregorio-Rodríguez, Luis Llana, and Rafael Martínez-Torres

Departamento Sistemas Informáticos y Computación
Universidad Complutense de Madrid, Spain
cgr@sip.ucm.es, llana@ucm.es, rmartine@fdi.ucm.es

**Abstract.** In this paper we continue the study of the input-output conformance simulation (iocos). In particular, we focus on implementation aspects to show that iocos is indeed an interesting semantic relation for formal methods. We address two complementary issues: a) In the context of model based testing (MBT) we present an online, also called on-the-fly, testing algorithm that checks whether an implementation conforms a given specification. Online testing combines test generation and execution and avoids the generation of the complete test suite for the specification. We prove both soundness and completeness of the online algorithm with respect to the iocos relation. b) In the context of formal verification and model checking minimisation a key issue is to efficiently compute the considered semantic relations; we show how the coinductive flavour of our conformance relation iocos makes it appropriate to be cast into an instance of the Generalised Coarsest Partition Problem (GCPP) and thus it can be efficiently computed.

**Keywords:** Model Based Testing, Online Testing, Simulation Algorithm, Input Output Conformance Simulation, Model Checking Minimisation, Verification, Generalised Coarsest Partition Problem, Formal Methods.

## 1 Introduction

In a recent paper [12] we introduced the input-output conformance simulation relation (iocos) that refines the classic Tretman's ioco. The work by Tretmans [25] has settled a solid and widespread framework in the Model Based Testing (MBT) community: it offers both offline and online [9] testing algorithms; and there are several model-based test generation tools (e.g. [26,3]) that implement the ioco-testing theory.

From a theoretical point of view, some interesting particularities of the ioco-framework are: behaviours are modelled as labelled transition systems (LTS); quiescent states (see [24]) are considered; implementations should be input-enabled; and the ioco relation is a trace-based semantics, and thus a linear semantics [27].

<footnote>* Research partially supported by the Spanish MEC projects TIN2009-14312-C02-01 and TIN2012-36812-C02-01</footnote>
Our iocos approach shares LTS as models, quiescence, and much of the con-
formance philosophy, while considering a wider behaviour domain not imposing,
but allowing, implementations to be input enabled. The substantial difference is
that the conformance relation is an input-output simulation (iocos) —a branch-
ing semantics [27]— with greater discriminatory power than ioco (see Theo-
rem 1 below). In [12] we presented an offline algorithm that starting from a
formal model of the specification produced a test suite to be checked against the
possible implementations. We proved the resulting test suite to be sound and
exhaustive for the given specification with respect to iocos.

In this paper we present an alternative approach to offline testing that avoids
the generation of the whole test suite. When time or space requirements are con-
sidered, a more suitable testing approach is the so called online testing. Online
testing considers a concrete implementation to be checked against the specifica-
tion. It combines test generation from the specification model and test execution
against the implementation. In this approach only a single step of a test is gen-
erated from the model and executed in the implementation; the results of this
execution are taken into account to generate the next step in the test, that is
again checked against the implementation. In order to show the applicability of
our conformance relation, in this paper we define an online testing algorithm for
iocos that we prove to be sound and complete.

An essential point of our conformance relation is that it is simulation-based.
Simulation is an important notion pervading many fields in computer science
(model checking, concurrency theory, formal verification...). It is an active area
of research both theoretical (e.g. [2,8,17,10]) and practical (e.g. [5,22]). Regarding
practical implementation applications for iocos, it is particularly interesting its
use in model checking minimisation ([6,14]) as a technique to overcome the state
explosion problem.

The quest for efficient algorithms<fnref n="1" /> to compute this relation has been an area
of active research in the last years (e.g.[11,5,22]). In [22] you can find an excel-
lent review of the state of the art for simulation algorithms. One of the most
outstanding algorithms is the one presented in [11], and subsequently corrected
in [28]. It is one of the fastest algorithms and quasi-optimal in space. This al-
gorithm exploits the representation of the simulation problem as a Generalised
Coarsest Partition Problem (GCPP). We show in this paper how the confor-
mance relation iocos can be cast into an instance of the GCPP. Therefore it can
be efficiently computed using the algorithm in [28].

The paper is organised as follows: in Section 2 we present the essential no-
tation, definitions and results of the iocos-theory used in the rest of the paper.
In Section 3, definition and behaviour of our online testing algorithm are ex-
plained and we discuss other related online testing algorithms in the literature.
Section 4 is devoted to prove that iocos is indeed a relation that can be effi-

<footnote n="1">¹ As a general overview, we could say that while deciding trace inclusion on finite-state processes is PSPACE-hard [23], the simulation preorder is decidable in polynomial time. Actually, simulation preorder is the coarsest preorder included in trace inclusion with this property.</footnote>
ciently computed. We use the technique of system transformation to adequate
iocos to the problem definition in [11]. Then we prove that this transformation
holds all requirements to be computed as a GCPP. Finally in Section 5 we make
a summary and advance some future research lines. In order to meet the space
requirements, there is an appendix containing the more technical proofs of the
paper. This appendix will be available on-line in case of acceptance of the paper.

## 2 Preliminaries

This section presents the notation used in the paper and reviews the formal
framework of the iocos theory introduced in [12,16].

We consider two disjoint finite sets of actions: inputs $I$, initiated by the
environment and annotated with a question mark, $a?$, $b?$, $c? \in I$; and outputs $O$,
initiated by the system, and annotated with an exclamation mark, $o!$, $u!$, $t! \in O$.
In many cases we want to name actions in a general sense, inputs and outputs
indistinctly. We will consider the set $L = I \cup O$ and we will omit the exclamation
or question marks when naming generic actions, $x, y, z \in L$.

A state with no output actions cannot autonomously proceed, such a state
is called quiescent. Quiescence is an essential component of the ioco theory. For
the sake of simplicity and without lost of generality (see for instance [25,24]), we
directly introduce the event of quiescence as a special action denoted by $\delta! \in O$
into the definition of our models.

**Definition 1.** A labelled transition system with inputs and outputs is a 4-tuple $(S, I, O, \rightarrow)$ such that

- $S$ is a set of states or behaviours.

- $I$ and $O$ are disjoint sets of input and output actions respectively. Output action include the quiescence symbol $\delta! \in O$. We define $L = I \cup O$.

- $\rightarrow \subseteq S \times L \times S$. As usual we write $p \xrightarrow{x} q$ instead of $(p, x, q) \in \rightarrow$ and $p \xrightarrow{x} \rightarrow$, for $x \in L$, if there exists $q \in S$ such that $p \xrightarrow{x} q$. Analogously, we will write $p \xrightarrow{x} \leftarrow$, for $x \in L$, if there is no $q$ such that $p \xrightarrow{x} q$.

In order to allow only coherent quiescent systems the set of transitions $\rightarrow$
should also satisfy:

- if $p \xrightarrow{\delta!} p'$ then $p = p'$. A quiescent transition is always reflexive.

- if $p \xrightarrow{o!} \leftarrow$ for any $o! \in O \setminus \{\delta!\}$, then $p \xrightarrow{\delta!} p'$. A state with no (regular) outputs is quiescent.

- if there is $o! \in O \setminus \{\delta!\}$ such that $p \xrightarrow{o!} \rightarrow$, then $p \xrightarrow{\delta!} \leftarrow$. A quiescent state
performs no other output action.

- A system is *input-enabled* if at any $s \in S$ for every $a? \in I$ we have $s \xrightarrow{a?} \rightarrow$. $\square$

We denote the set of labelled transition systems with inputs and outputs
just as LTS. In general we use $p, q, p', q'...$ for states or behaviours, but also
$i, i', s$ and $s'$ when we want to emphasise the concrete role of a behaviours as
implementation or specification. We consider implementations and specifications, or, more generally, behaviours under study, as states of the same LTS.

A trace is a finite sequence of symbols of L. We will normally use the symbol $\sigma$ to denote traces, that is, $\sigma \in L^*$. The empty trace is denoted by $\epsilon$ and we juxtapose, $\sigma_1\sigma_2$, to indicate concatenation of traces. The transition relation of labelled transition systems can naturally be extended using traces instead of single actions, $p \xrightarrow{\sigma} q$. Next we introduce some definitions and notation frequently used in the paper.

**Definition 2.** Let $(S, I, O, \rightarrow) \in LTS$, and $p \in S$, we define:

1. $p$ after $\sigma = \{p' | p' \in S, p \xrightarrow{\sigma} p'\}$, the set of states after the trace $\sigma$.

2. $\text{outs}(p) = \{o! | o! \in O, p \xrightarrow{o!} \}$, the outputs of a state $p$ (it may include $\delta!$).

3. $\text{ins}(p) = \{a? | a? \in I, p \xrightarrow{a?} \}$, the set of inputs of a state $p$. $\square$

A behaviour is deterministic when for any $x \in L$, if $p \xrightarrow{x} p_1$ and $p \xrightarrow{x} p_2$ then $p_1 = p_2$; or equivalently the set $p$ after $\sigma$ is always empty or a singleton. While some models prevent non determinism we assume and allow all kinds of non-deterministic behaviour both in specifications and implementations.

Next we recall the simulation-based formal definition of iocos.

**Definition 3.** Let $(S, I, O, \rightarrow) \in LTS$, we say that a relation $R \subseteq S \times S$ is a iocos-relation if and only if for any $(p, q) \in R$ the following conditions hold:

1. $\text{ins}(q) \subseteq \text{ins}(p)$

2. $\forall a? \in \text{ins}(q)$ if $p \xrightarrow{a?} p'$ then $\exists q' \in S$ such that $q \xrightarrow{a?} q' \wedge (p', q') \in R$.

3. $\forall o! \in \text{outs}(p)$ if $p \xrightarrow{o!} p'$ then $\exists q' \in S$ such that $q \xrightarrow{o!} q' \wedge (p', q') \in R$.

We define the *input-output conformance simulation (iocos)* as the union of all iocos-relations (the biggest iocos-relation). $\square$

Additional details on iocos rationale and examples appear in [12], where it is also proved that iocos is a strictly finer relation than ioco.

**Theorem 1.** [12] Let $(S, I, O, \rightarrow) \in LTS$; then iocos $\subseteq$ ioco. That is, for any $p, q \in S$, whenever we have $p$ iocos $q$ it is also true that $p$ ioco $q$. $\square$

# 3 An online testing algorithm for iocos

The main goal of this section is to prove iocos as a suitable conformance relation to be used in online testing. As usual, the online testing algorithm merges test generation and execution into a single interactive process. In order to understand the notation and some ideas and key concepts behind Algorithm 1, next we recall the iocos theory of testing: test definition and test execution.

**Definition 4.** A test is a syntactical term defined by the following BNF:

$$T = \mathbf{x} | \checkmark | T_1 \oplus T_2 | T_1 + T_2 | x; T \quad \text{where } x \in L$$

We denote the set of tests as $\mathcal{T}$. $\square$
As usual in MBT, the environments we want to model should be able to respond at any moment to any possible output of the implementation under test. That is, tests like `a?`; `$T_a$?` will not be accepted as valid tests, but should be completed into tests like `a?`; `$T_{a?} + \sum_{o! \in O} o!$`; `$T_{o!}$`. For the sake of simplicity we use $\sum_{i \in \{1, \dots, n\}} T_i$ as a shortcut for $T_1 + \dots + T_n$.

Particularly interesting is that we consider two kind of choices in the tests: the one corresponding to the `+` operator, with conjunctive semantics, and the `⊕` operator with a disjunctive meaning. To define how tests interacts with behaviours and what is the result of the execution of that experiment, we follow Abramsky's ideas in [1] and use a predicate to define the outcomes of the interaction between a test and the behaviour or implementation being tested.

**Definition 5.** Let $(S, I, O, \rightarrow) \in \mathit{LTS}$, $s \in S$, $a? \in I$, and $o! \in O$, we inductively define the predicate **pass** $\subseteq S \times \mathcal{T}$ as follows:

$$s \text{ pass } \mathcal{X} = \text{ false}$$

$$s \text{ pass } \checkmark = \text{ true}$$

$$s \text{ pass } o!; T_{o!} = \begin{cases} true & \text{if } o! \notin \text{ outs}(s) \\ \bigwedge \{s' \text{ pass } T_{o!} | s \xrightarrow{o!} s'\} & \text{otherwise} \end{cases}$$

$$s \text{ pass } a?; T_{a?} = \begin{cases} false & \text{if } a? \notin \text{ ins}(s) \\ \bigwedge \{s' \text{ pass } T_{a?} | s \xrightarrow{a?} s'\} & \text{otherwise} \end{cases}$$

$$s \text{ pass } T_1 + T_2 = s \text{ pass } T_1 \wedge s \text{ pass } T_2$$

$$s \text{ pass } T_1 \oplus T_2 = s \text{ pass } T_1 \vee s \text{ pass } T_2$$

□

For the sake of convenience the **pass** predicate is inductively defined over the whole set of tests, with a simpler structural formulation, while at the end we will only be interested in valid tests.

In [12] we defined an algorithm (Definition 6 below) that starting from a given specification *s* produced a test suite *T*(*s*) of valid tests that characterised the specification with respect to the *iocos* conformance relation as stated in Theorem 2 below.

**Definition 6.** Let $(S, I, O, \rightarrow) \in \mathit{LTS}$ and $p \in S$. We denote with $\mathcal{T}(p)$ the set of valid tests from *p* by applying a finite number of recursive applications of one of the following non-deterministic choices:

1. $T = \checkmark \in \mathcal{T}(p)$.

2. If $a? \in \text{ins}(p)$, then $T \in \mathcal{T}(p)$ where

$$T = a?; \bigoplus \{Tp_{a?} | p \xrightarrow{a?} p_{a?}\} + \sum_{o! \in \text{outs}(p)} o!; \bigoplus \{Tp_{o!} | p \xrightarrow{o!} p_{o!}\} + \sum_{\substack{o! \in O \\ o! \notin \text{outs}(p)}} o!; \mathcal{X}$$

3. If $\text{ins}(p) = \emptyset$ then $T \in \mathcal{T}(p)$ where

$$T = \sum_{o! \in \text{outs}(p)} o!; \bigoplus \{Tp_{o!} | p \xrightarrow{o!} p_{o!}\} + \sum_{\substack{o! \in O \\ o! \notin \text{outs}(p)}} o!; \mathcal{X}$$
In all cases the tests $T_p$ are chosen non-deterministically from the set $T(p)$,
$T_\delta(p) = \check{\text{✓}}$ if $p \xrightarrow{\delta!} \emptyset$, and $T_{\delta!}(p) = \mathbf{X}$ otherwise. $\square$

**Theorem 2.** [12](Completeness) Let $(S, I, O, \rightarrow) \in \mathit{LTS}$ and $p, q \in S$, $T \in \mathcal{T}(p) : q \mathit{pass} T$ iff $q \mathit{iocos} p$. $\square$

**Online Algorithm** Offline generation of test leads to a massive test suite.<fnref n="2" /> This is not surprising given that the test suite should be able to prove and disprove the conformance with any *possible* implementation. Online testing, on the contrary, considers a concrete implementation under test (IUT) and, therefore, the testing process can be guided by the mutual interaction.

The online testing algorithm for *iocos* is defined in Algorithm 1. This algorithm somehow merges the test generation and execution (Definition 5 and 6), and it considers only the necessary continuations by taking into account the current state of the specification and the last response from the implementation.

Algorithm 1 starts with a specification, an IUT, and a desired number of iterations (parameters *s*, *IUT* and *maxIter* in function *TE*). The testing process will continue until a **X** verdict is found, indicating IUT does not conform *s*, or until the number of iterations has been reached without a faulty behaviour found in IUT.

According to Definition 5 the testing process will yield a **X** verdict on these cases: a mandatory input is rejected by IUT or an unexpected output by IUT is registered by the tester. In Algorithm 1, the first situation is solved in the first conditional inside the first **case** statements in function $TE_{\text{REC}}$ (lines 16 and 17). Let us note that to check the enabled actions in IUT (line 16), is equivalent to check condition 1 in Definition 3 (*iocos*).

Otherwise, if the action that the test chooses to offer is actually enabled in the IUT, the stimulus is sent to the implementation (line 18) and then condition 2 in Definition 3 (*iocos*) should be tested: at least one of the descendant tests must be passed by the current state of the implementation, otherwise the final return statement outside the loop will propagate the **X** verdict. The *copy* clause (line 19)—theoretically essential, see [1,21]—is used to check every descendant test against the same state of the implementation. For software artifacts, and even embedded systems that can be easily replicated, this is indeed a feasible operation.

In a similar way, if we focus on output actions, conditional in lines 28 and 29 detects unexpected outputs from the implementation. Otherwise, if an output received from the IUT is acceptable, the algorithm has to proceed and check condition 3 in Definition 3 (*iocos*) as described previously.

Algorithm 1 is non-deterministic and the three cases in the **choice** statement (line 13) are arbitrarily chosen in every run of the function $TE_{\text{REC}}$. The *reset* case introduces the possibility of breadth exploration of the IUT, while the other two choices produce a (one step) deep exploration.

<footnote n="2">² Of course, there is a very interesting line of research in MBT that tries to reduce the size of the test suite while keeping a *good* coverage.</footnote>
<caption>**Algorithm 1 Online Testing Algorithm for iocos**</caption>

1: **function** TE(s, iut, maxIter)
2:     **continue** ← ✓
3:     **numIter** ← maxIter
4:     **while** numIter > 0 ∧ **continue** == ✓ **do**
5:         **continue**, numIter ← TE<sub>REC</sub>(s, iut, numIter)
6:         **if** **continue** == ✓ **then**
7:             **reset** iut
8:             **return** **continue**
9:     **function** TE<sub>REC</sub>(s, iut, numIter)
10:     **if** numIter == 0 **then**
11:         **return** ✓, numIter
12:     **else**
13:         **choice**
14:             **case** action **do**
15:                 **choice** a ∈ ins(s)
16:                 **if** a? is not enabled in iut **then**
17:                     **return** X, numIter
18:                 **send** a? to iut
19:             **iut0** ← copy(iut)
20:             **for** s' ∈ s after a? **do**
21:                 **iut** ← copy(iut0)
22:                 **continue**, numIter ← TE<sub>REC</sub>(s', iut, numIter - 1)
23:                 **if** **continue** == ✓ **then**
24:                     **return** ✓, numIter
25:             **return** X, numIter
26:             **case** wait **do**
27:                 **wait** o! from iut
28:                 **if** s after o! = Ø **then**
29:                     **return** X, T
30:                 **iut0** ← copy(iut)
31:             **for** s' ∈ s after o! **do**
32:                 **iut** ← copy(iut0)
33:                 **continue**, numIter ← TE<sub>REC</sub>(s', iut, numIter - 1)
34:                 **if** **continue** == ✓ **then**
35:                     **return** ✓, numIter
36:             **return** X, numIter
37:             **case** reset **do**
38:                 **return** ✓, maxIter
39:
There are in the literature of MBT two essential works we can relate Algorithm 1 with. In [9] de Vries and Tretmans presented an online algorithm for ioco that is non-deterministic and even termination is one of the non-deterministic choices. In [15] Larsen et al. describe an online algorithm for an ioco-based performance relation extended with real time and considering a concrete environment, namely rtioco<sub>e</sub>. Algorithm 1 is more similar in form to that on [15] and share with it the *reset* clause and the explicit use of the number of iterations. We do not consider explicit environments but the most general possible environment.<sup>3</sup> As in [9,15], quiescence detection can be implemented with a timeout.

In [29] you can find a practical online testing algorithm that is implemented
in the MBT tool developed at Microsoft Research called Spec Explorer. The
framework and the approach are somehow different: they use interface automaton
as the specification model and assume the implementation to be in the domain
of the specifications. In this work soundness and completeness are not even
mentioned.

**Soundness and Completeness** The rest of this section is devoted to prove that Algorithm 1 is indeed sound and complete.

In [9] correctness of the online algorithm for ioco is stated under fairness assumptions (*weather conditions* [19]) in the non-deterministic choices. In [15] online algorithm for rtioco<sub>e</sub> is proved to be sound and complete assuming the classic *test hypothesis*,<sup>4</sup>fairness in the randomisation of algorithm choices, and deterministic IUT.

In our model, we allow both implementations and specifications to behave
non-deterministically and, as usual, we assume fairness in the non-deterministic
choices and the *test hypothesis* ([9,15]). Test hypothesis assumes that any IUT
can be modelled in the domain of *LTS*.

**Theorem 3.** Let $(S, I, O, \rightarrow)$ be a LTS, let $i, s \in S$, and $n \in \mathbb{N}$. If the function call $\text{TE}(s, i, n)$ in Algorithm 1 returns a $\mathbf{x}$, then $i$ satisfies s.

*Proof.* The proof proceed by induction on the parameter *n* of TE(s, i, n), follow-
ing the ideas commented in the algorithm explanation. □

Asserting completeness implies that, for any faulty implementation of a given
specification s, the online testing process in Algorithm 1 should eventually yield
a x result, that is, the algorithm should drive the computation through a test
passed by the specification and failed by the implementation. Let us note that a
key point to prove the completeness is to assure that all states in the specification
and implementation should be inspected. This is where the fairness requirement
is needed: every infinitely often eligible action is eventually executed. To ensure
this possibility one of the choices of the algorithm is to reset the IUT and to

<footnote n="3">³ To introduce environments might lead to a reduction of the search-space because this additional knowledge can be used to further restrict the testing process.</footnote>

<footnote n="4">⁴ The behaviour of IUT can be described in the model domain. Only the existence is assumed, not a concrete and known instance.</footnote>
restart the algorithm (lines 37 and 38). Moreover, assuming the fairness hypothesis also implies that the number of times required to ensure that all states have been checked is not known a priori. So the number of iterations appearing in Proposition 1 and Theorem 1 cannot be determined at the beginning of the execution.

**Proposition 1.** Let $(S, I, O, \rightarrow)$ be a LTS, let $i, s \in S$, and let $T \in T(s)$ be a test such that $s$ pass $T$ and $i$ pass $T$. Then there exist $n, n' \in \mathbb{N}$ such that $\text{TE}_{\text{REC}}(s, i, n)$ returns $\mathbf{X}, n'$.

*Proof.* We make the proof by induction on the depth of $T$. The case base is when $T = \checkmark$ that is trivial since $i$ pass $T$. According to Definition 6, there are two cases. We are going to consider the test

$$T = a?; \bigoplus \{T_{s_{a?}} | s \xrightarrow{a?} s_{a?}\} + \sum_{o! \in \text{outs}(s)} o!; \bigoplus \{T_{s_{o!}} | s \xrightarrow{o!} s_{o!}\} + \sum_{\substack{o! \in O \\ o! \notin \text{outs}(s)}} o!; \mathbf{X}$$

The other case is simpler than this one. Since $i$ pass $T$, there are three possibilities to make the test fail:

1. $i$ pass $s$ $a$?; $\bigoplus \{T_{s_{a?}} | s \xrightarrow{a?} s_{a?}\}$. Since we are assuming the fairness hypothesis, by choosing an arbitrary high $n$ the choice in line 15 of the algorithm will eventually choose the action $a?$. If $a?$ is not enabled in $i$, then the algorithm returns $\mathbf{X}$ in line 17. Otherwise the algorithm sends $a?$ to the implementation. Again, by the fairness hypothesis the implementation, eventually will go to a state $i'$ such that $i'$ pass $\bigoplus \{T_{s_{a?}} | s \xrightarrow{a?} s_{a?}\}$. Let us name $n_{i'}$ the number of iterations needed to reach this state. On the other hand, since $s$ pass $T$, $s'$ pass $\bigoplus \{T_{s_{a?}} | s \xrightarrow{a?} s_{a?}\}$ for any $s' \in s$ after $a?$. So by induction hypothesis for any $s' \in s$ after $a?$ there exist $n_{s'} \in \mathbb{N}$ such that $\text{TE}_{\text{REC}}(s', i, n_{s'})$ returns $\mathbf{X}$. So by choosing $n_0 \ge n_{i'} + \sum_{s' \in s \text{ after } a?} n_{s'}$, there exists $n'$ such that the $\text{TE}_{\text{REC}}(s, i, n_0)$ returns $\mathbf{X}, n'$.

2. $i$ pass $s \sum_{o! \in \text{outs}(s)} o!$; $\bigoplus \{T_{s_{o!}} | s \xrightarrow{o!} s_{o!}\}$. In this case there is $o! \in \text{outs}(s)$ such that $i$ produces output $o!$ and goes to an state $i'$ such that $i$ pass $\bigoplus \{T_{s_{o!}} | s \xrightarrow{o!} s_{o!}\}$. By the fairness hypothesis the implementation will eventually produce that output and will go to state $i'$. Let us name $n_{i'}$ the number of iterations needed to reach this state. On the other hand, $s'$ pass $\bigoplus \{T_{s_{o!}} | s \xrightarrow{o!} s_{o!}\}$ for any $s' \in s$ after $o!$. So by induction hypothesis for any $s' \in s$ after $o!$ there exist $n_{s'} \in \mathbb{N}$ such that $\text{TE}_{\text{REC}}(s', i, n_{s'})$ returns $\mathbf{X}$. So by choosing $n_0 \ge n_{i'} + \sum_{s' \in s \text{ after } o!} n_{s'}$, there exists $n'$ such that the $\text{TE}_{\text{REC}}(s, i, n_0)$ returns $\mathbf{X}, n'$.

3. $i$ pass $s \sum_{\substack{o! \in O \\ o! \notin \text{outs}(s)}} o!$; $\mathbf{X}$. In this case there is $o! \in O$ such that $i$ produces output $o!$. By the fairness hypothesis the implementation will produce this output and the algorithm will return $\mathbf{X}$ in line 29. □

Since the main function of the algorithm just makes calls to the recursive algorithm as a corollary we get the following result:
**Theorem 4.** Let $(S, I, O, \rightarrow)$ be a LTS, let $i, s \in S$. If *iocos* s then there exist $n \in \mathbb{N}$ such that the function call TE(s, i, n) in Algorithm 1 returns $\mathbf{x}$. $\square$

# 4 iocos as a Generalised Coarsest Partition Problem

Milner in [18] introduced the preorder relation called simulation. Simulation equivalence strongly preserves ACTL\*, and also strongly preserves LTL and ACTL as sublogics of ACTL\* [6]. Both ACTL and LTL are widely used for model checking in practice.

Simulation is a close relative of the well known bisimulation equivalence [20]. Bisimulation equivalence can be fast computed by reducing it to the problem of determining the coarsest partition of a set stable with respect to a given relation [13]. An equivalent result for computing simulation as a generalised coarsest partition problem (GCPP) was given in [11] and corrected in [28]. This algorithm keeps a very good time complexity while its space complexity can be considered minimal.

Although iocos definition is simulation-like, it has particularities inherited from the classic requirements for the conformance relations when dealing with inputs and outputs, and even the use of input-output actions is not symmetric in the definition. Therefore, the applicability of simulation algorithms to compute iocosis not straightforward.

We will show in this section that fortunately we can compute iocos by using any algorithm that solves the GCPP. To achieve this goal, first we will show how to transform the LTS into graphs and partitions as defined in [11,28]. Then we will define the relation g-iocos (graph-iocos) in the transformed LTS that will be equivalent to iocos. Finally, we will formally prove that the transformed LTS holds the conditions of the GCPP.

## 4.1 Transforming an LTS into a graph

The GCPP in [11] is defined in terms of graphs. These graphs have no labels in the edges. The objective is to transform an LTS into a graph without actions and without losing information. The idea to achieve this is to *encode* the action associated to a transition into the states of the graph. So the states of the associated graph of an LTS will be pairs: the first component of the pair refers to a state of the LTS whereas the second component is the action needed to reach this state.

One of the details that we have to deal with to transform iocos into a simulation is that in Definition 3 (iocos) the implementation is allowed to introduce unspecified behaviour. We do not need to take into account those states reached by implementation when input actions are not present in the specification. To overcome this situation, in the transformed system, we need to represent these states by adding a sort of new *magic state*, that we denote by the symbol $*$. Such a state has the next property: every possible implementation will fulfil it. Moreover, in the transformation we will embed the transition action symbol into
the state itself. Exceptionally, and just for the sake of uniformity, a new action symbol (·) is used for states with no incoming transitions.

**Definition 7.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system. We define its transformed graph as $\mathbb{T}(\mathcal{L}) = (N, \Rightarrow)$ where $N = (S \cup \{*\}) \times (L \cup \{\cdot\})$ and $\Rightarrow$ is defined by the following rules.

$$ \frac{s \xrightarrow{y} s'}{(s, x) \Rightarrow (s', y)}, \quad \frac{s \xrightarrow{a?} (s, x) \Rightarrow (*, a?)}{(*, x) \Rightarrow (*, y)}, \quad \frac{s, s' \in S}{x, y \in L \cup \{\cdot\}, a? \in I} $$

The nodes of $N$ will be denoted by the letters $n, n_1, n_2$, etc. Since these nodes come from states of the original labelled transition system, we annotate the arcs of the graph with the action of the target node for readability reasons. In this way will write $n_1 \xrightarrow{x} n_2$ whenever $n_1 \Rightarrow n_2$ and there is $s_2 \in S$ such that $n_2 = (s_2, x)$.

Following the same rationale we adapt the definition of the function $\text{ins}$:
$\text{ins}(*, x) = \emptyset$ and $\text{ins}(s, x) = \text{ins}(s)$ if $s \in S$. $\square$

**Definition 8.** Let $(N, \Rightarrow)$ be the transformed graph of an $\mathcal{L} \in \text{LTS}$, a relation $R \subseteq N \times N$ is g-iocos simulation iff for any $n_1, n_2 \in N$, $(n_1, n_2) \in R$ the following conditions hold:

1. $n_1 = (s_1, x), n_2 = (s_2, y)$ and $x = y$.

2. $\text{ins}(n_2) \subseteq \text{ins}(n_1)$

3. for all $a \in L$, if $n_1 \stackrel{a}{\Rightarrow} n'_1$ then exists $n'_2$ such that $n_2 \stackrel{a}{\Rightarrow} n'_2$ and $n'_1 R n'_2$.

For $n_1, n_2 \in N$, we say that $n_1$ g-iocos $n_2$ if there exists a g-iocos simulation $R$ such that $(n_1, n_2) \in R$. $\square$

At a first glance, g-iocos is defined as a kind of ready simulation preorder [4]. Next, we show that computing g-iocos over graphs is equivalent to compute iocos on LTS. Proposition 2 describes how to transform a concrete iocos-simulation into a g-iocos-simulation, while Proposition 3 presents the reciprocal transformation. Finally, Theorem 5 is a corollary of the previous results showing iocos and g-iocos to be two different formulations for the same semantics in two different domains.

**Proposition 2.** Let $\mathcal{L} = (S, I, O, \rightarrow)$, let $\mathbb{T}(\mathcal{L}) = (N, \Rightarrow)$ be its transformed graph, let $R$ be iocos relation $R \subseteq S \times S$, and let $R' \subseteq N \times N$ defined as

$$ R' = \{((i, a), (s, a)|(i, s) \in R, \forall a \in L \cup \{\cdot\}) \cup \{(i, a)(*, a)| a \in L \cup \{\cdot\}, i \in S \cup \{*\}\} $$

Then $R'$ is a g-iocos simulation.

*Proof.* Let us take $(n_1, n_2) \in R'$ and check that $R'$ holds the statements of Definition 8.

$n_2 = (*, a)$. i.e., we are in the second subset of $R'$. Trivially we have $\text{ins}(n_1) \supseteq \emptyset = \text{ins}(n_2)$ (statement 2 of Definition 8). As $(*, x) \Rightarrow (*, y)$ for any $x, y \in L$ and $(n'_1, (*, a)) \in R'$ for any $n'_1$, then statement 3 of Definition 8 holds.
$n_1 = (*, a)$. As $R'$ is defined, $n_2 = (*, a)$, and it is solved as in the previous case. $n_1 \neq (*, a)$ and $n_2 \neq (*, a)$. Let us assume that $n_1 = (i, a)$ and $n_2 = (s, a)$. Since $R$ is an iocos simulation, we obtain $\text{ins}(n_1) = \text{ins}((i, a)) = \text{ins}(i) \supseteq \text{ins}(s) = \text{ins}((s, a)) = \text{ins}(n_2)$ (statement 2 of Definition 8).

Now let us take action $x \in L$ such that $n_1 \underset{x}{\Rightarrow} n'_1$. If $x \in O$ then we obtain that there exist $i'$ such that $i \xrightarrow{x} i'$ and $n'_1 = (i', x)$. Since $R$ is a iocos simulation, then there exists $s'$ such that $s \xrightarrow{a} s'$ and $(s, s') \in R$. Again, by the construction of the transitions $n_2 = (s, a) \stackrel{x}{\Rightarrow} (s', x) = n'_2$ and $(n'_1, n'_2) \in R'$ by definition of $R'$.

If $x \in I$ there are two possibilities: either $x \notin \text{ins}(i)$ or $x \in \text{ins}(i)$. In the first case we have $(i, a) \xrightarrow{x} (*, a) = n'_1$ by the way transitions are defined. Since $R$ is an iocos simulation $\text{ins}(s) \subseteq \text{ins}(i)$ and therefore $x \notin \text{ins}(s)$. Then $n_2 = (s, a) \stackrel{x}{\Rightarrow} (*, x) = n'_2$ and $(n'_1, n'_2) \in R'$. In the second case there exists $i'$ such that $i \xrightarrow{x} i'$. If $x \in \text{ins}(s)$, since $R$ is an iocos simulation there exists $s'$ such that $s \xrightarrow{x} s'$ and $(s, s') \in R$. By the construction of the transitions $n_2 = (s, a) \stackrel{x}{\Rightarrow} (s', x) = n'_2$ and $(n'_1, n'_2) \in R'$ by definition of $R'$. If $x \notin \text{ins}(s)$, then $(s, a) \xrightarrow{x} (*, x) = n'_2$. Then $(n'_1, n'_2) \in R'$ by definition of $R'$ □

**Proposition 3.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system, let $\mathbb{T}(\mathcal{L}) = (N, \Rightarrow)$ be its transformed graph, let $R' \subseteq N \times N$ be a g-iocos relation, and let $R \subseteq S \times S$ defined as $R = \{(i, s) | \exists a \in \bar{L} \cup \{\cdot\}. ((i, a), (s, a)) \in R' \wedge i, s \in S\}$. Then $R$ is a iocos simulation.

*Proof.* Let $(i, s) \in R$. By construction of $R$, there exists $a \in L$ and $n_1 = (i, a)$ and $n_2 = (s, a)$ such that $(n_1, n_2) \in R'$. Since $R'$ is a g-iocos simulation, we have $\text{ins}(i) = \text{ins}((i, a)) = \text{ins}(n_1) \supseteq \text{ins}(n_2) = \text{ins}((s, a)) = \text{ins}(s)$ according to the statement 1 of the definition of iocos. Now let us check the other two conditions:

- Let us consider $b? \in \text{ins}(s)$ such that $i \xrightarrow{b?} i'$, so $(i, a) \stackrel{b?}{\Rightarrow} (i', b?)$. Since $R'$ is a g-iocos simulation there exists $n'_2 = (s', b?)$ such that $n_2 \stackrel{b?}{\Rightarrow} n_2$. Since $b? \in \text{ins}(s)$, $s' \neq *,$ so $s' \in S$. Finally, by definition of, $R$ we obtain $(i', s') \in R$.

- The case when $o! \in \text{outs}(i)$ and $i \xrightarrow{o!} i'$ is similar to the previous one, but in this case $s' \neq *$ because $o! \notin I$. □

Finally, we obtain the theorem that relates iocos and g-iocos. This theorem is a corollary of the previous Proposition 2 and 3.

**Theorem 5.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system and $\mathbb{T}(\mathcal{L}) = (N, \Rightarrow)$ its transformed graph. Then, for any $s_1, s_2 \in S$, we have $(s_1, s_2) \in \text{iocos}$ if and only if $((s_1, x), (s_2, x)) \in \text{g-iocos} \ \forall x \in L$. □

## 4.2 g-iocos as a GCPP problem

To conclude this section we will show that g-iocos can be seen as an instance of the GCPP. In order to make the paper self-contained, we are going to reproduce in condensed form definitions from [11].
**Definition 9.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system and $T(\mathcal{L}) = (N, \Rightarrow)$ its transformed graph.

1. A partition pair is a tuple $\langle S, \preceq \rangle$ such that $S = \{\alpha, \beta, \dots\}$ is a partition of $N$ and $\preceq$ is a reflexive and acyclic relation on $S$.

2. Let $S$ be a partition and let $n \in N$, we write $[n]_S$ as the unique element of $S$ that contains $n$.

3. Let $\alpha, \beta \in S$, we write $\alpha \Rightarrow \exists \beta$ iff $\exists a \in \alpha$ such that $a \Rightarrow g$ for some $b \in \beta$. We write $\alpha \Rightarrow \forall \beta$ iff $\forall a \in \alpha$ we have $a \Rightarrow b$ for some $b \in \beta$.

4. We say that $\langle S, \preceq \rangle$ is stable with respect to $\Rightarrow$ iff

$$ \forall \alpha, \beta, \gamma \in S \quad \text{if} \quad (\alpha, \beta) \in \preceq \wedge \alpha \Rightarrow \exists \gamma \quad \text{then} \quad \exists \epsilon \in S : (\gamma, \epsilon) \in \preceq \wedge \beta \Rightarrow \forall \epsilon $$

5. Let $\langle S_1, \preceq_1 \rangle$ and $\langle S_2, \preceq_2 \rangle$ be partition pairs. We say that $\langle S_1, \preceq_1 \rangle$ is a refinement of $\langle S_2, \preceq_2 \rangle$, written $\langle S_1, \preceq_1 \rangle \sqsubseteq \langle S_2, \preceq_2 \rangle$, if $S_1$ is finer than $S_2$, i.e., $(\forall \alpha \in S_1 \exists \alpha' \in S_2 : \alpha \subseteq \alpha')$ and $\preceq_1 \subseteq \preceq_2$ ($S_1$) where $\preceq_2$ ($S_1$) is the induced relation on $S_1$ by $\preceq_2$: $(\alpha, \beta) \in \preceq_2$ ($S_1$) iff there exist $\alpha'$, $\beta' \in S_2$ such that $\alpha \subseteq \alpha'$, $\beta \subseteq \beta'$ and $(\alpha', \beta') \in \preceq_2$.

6. Let us consider a pair $\langle S, \preceq \rangle$, the Generalised Coarsest Partition Problem (GCPP) for $\langle S, \preceq \rangle$ consists in finding a partition pair $\langle S_0, \preceq_0 \rangle$ such that: a) $\langle S_0, \preceq_0 \rangle \sqsubseteq \langle S, \preceq \rangle$, b) $\langle S_0, \preceq_0 \rangle$ is stable respect to $\Rightarrow$, and c) $\langle S_0, \preceq_0 \rangle$ is maximal fitting a) and b). $\square$

Now we are ready to set up our key concepts in order to embed iocos com-
putation into GCPP problem via a g-iocos reduction.

**Definition 10.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system and $T(\mathcal{L}) = (N, \Rightarrow)$ its transformed graph. We write $\equiv_{\text{g-iocos}}$ for the kernel of g-iocos, that is $(a, b) \in \equiv_{\text{g-iocos}}$ iff $(a, b) \in \text{g-iocos}$ and $(b, a) \in \text{g-iocos}$.

Since $\equiv_{\text{g-iocos}}$ is an equivalence relation, it induces the partition $N / \equiv_{\text{g-iocos}}$. In this partition we can define $\preceq_{\text{g-iocos}}$ as the natural relation induced by $\text{g-iocos}$ in $N / \equiv_{\text{g-iocos}}$, namely, for $n_1, n_2 \in N$, $([n_1]_{\text{g-iocos}}, [n_2]_{\text{g-iocos}}) \in \preceq_{\text{g-iocos}}$ iff $(n_1, n_2) \in \text{g-iocos}$. $\square$

Let us note, that $\preceq_{\text{g-iocos}}$ is reflexive and acyclic in $N / \equiv_{\text{g-iocos}}$, so $\langle N / \equiv_{\text{g-iocos}}$, $\preceq_{\text{g-iocos}} \rangle$ is a partition pair. So, the rest of this section is devoted to prove that the partition $\langle N / \equiv_{\text{g-iocos}}$, $\preceq_{\text{g-iocos}} \rangle$ can be solved with any algorithm that solves the GCPP. In order to do it we need to define an initial partition pair $\langle \Omega, \preceq \rangle$ such that $\langle N / \equiv_{\text{g-iocos}}$, $\preceq_{\text{g-iocos}} \rangle \sqsubseteq \langle \Omega, \preceq \rangle$.

**Definition 11.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system and $T(\mathcal{L}) = (N, \Rightarrow)$ its transformed graph.

- We define the partition $\Omega = \{\alpha_1, \alpha_2, \dots, \alpha_n\} \subseteq \mathcal{P}(N)$ as follows: $(n_1, n_2) \in \alpha_i$ if and only if $n_1 = (s_1, x)$, $n_2 = (s_2, y)$, $\text{ins}(s_2) = \text{ins}(s_1)$ and $x = y$.

- We define the relation $\preceq \subseteq \Omega \times \Omega$ as $[n_1]_{\Omega} \preceq [n_2]_{\Omega}$ iff $n_1 = (s_1, x)$, $n_2 = (s_2, y)$, $\text{ins}(s_2) \subseteq \text{ins}(s_1)$ and $x = y$. $\square$
**Lemma 1.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system and its transformed graph $\mathbb{T}(\mathcal{L}) = (N, \Rightarrow)$. Then $\langle N/ \equiv_{\text{g-iocos}}, \preceq_{\text{g-iocos}} \rangle \subseteq \langle \Omega, \prec \rangle$.

*Proof.* This lemma is immediate because of the definition of g-iocos-simulation, kernel $\equiv_{\text{g-iocos}}$ and the induced partition pair $\langle N/ \equiv_{\text{g-iocos}}, \preceq_{\text{g-iocos}} \rangle$. $\square$

**Lemma 2.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system and its transformed graph, $\mathbb{T}(\mathcal{L}) = (N, \Rightarrow)$, then the partition pair $\langle N/ \equiv_{\text{g-iocos}}, \preceq_{\text{g-iocos}} \rangle$ is stable with respect to $\Rightarrow$.

*Proof.* Let us consider equivalence classes $[n_1]_{\text{g-iocos}}$, $[n_2]_{\text{g-iocos}}$, $\gamma \in N/ \equiv_{\text{g-iocos}}$ such that $([n_1]_{\text{g-iocos}}, [n_2]_{\text{g-iocos}}) \in \preceq_{\text{g-iocos}}$ and $[n_1]_{\text{g-iocos}} \Rightarrow \exists \gamma$. Then there exists $n'_1 \in \gamma$ and $x \in L$ such that $n_1 \xrightarrow{x} n'_1$. As $(n_1, n_2) \in \text{g-iocos}$ there exists $n'_2$ such that $n_2 \xrightarrow{x} n'_2$ and $([n'_1]_{\text{g-iocos}}, [n'_2]_{\text{g-iocos}}) \in \preceq_{\text{g-iocos}}$. Let us consider $n'_2$ a maximal element with respect to g-iocos, i.e, for any $n'_i$ such that $(n_1, n'_i) \in \text{g-iocos}$ we have $(n'_i, n'_2) \in \text{g-iocos}$.

Next we will prove that $[n_2] \Rightarrow_{\lor} [n'_2]$. Let us consider $n_3 \in [n_2]$. Since they belong to the same $\equiv_{\text{g-iocos}}$ class, the equivalence kernel makes true $(n_2, n_3) \in \text{g-iocos}$. Therefore there exists $n'_3$ such that $n_3 \xrightarrow{x} n'_3$ and $(n'_2, n'_3) \in \text{g-iocos}$. Again, $(n_3, n_2) \in \text{g-iocos}$, there exists $n''_2$ such that $n_2 \xrightarrow{x} n''_2$ and $(n'_3, n''_2) \in \text{g-iocos}$. Since g-iocos is transitive we obtain $(n'_2, n''_2) \in \text{g-iocos}$. Since $n'_2$ was a maximal element then $n'_2 = n''_2$ and then $n'_3 \in [n'_2]$. $\square$

We also need to show that $\langle N/ \equiv_{\text{g-iocos}}, \preceq_{\text{g-iocos}} \rangle$ is maximal with respect to the points a) and b) of the GCPP. In order to do it, first let us note that any partition pair $\langle S, \prec \rangle$ induces a natural relation in $N$ that we will denote by $\prec(N)$.

**Definition 12.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system and $\mathbb{T}(\mathcal{L}) = (N, \Rightarrow)$ its transformed graph, and let $\langle S, \prec \rangle$ be a partition pair. We define the relation $\prec(N) \subseteq N \times N$ as $(n_1, n_2) \in \prec(N)$ iff $([n_1]_S, [n_2]_S) \in \prec$.

Second, if $\langle S, \prec \rangle$ satisfies the points a) and b) of the GCPP for the partition pair $\langle \Omega, \prec \rangle$, then the following lemma states that $\prec(N)$ is a g-iocos-simulation.

**Lemma 3.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system and $\mathbb{T}(\mathcal{L}) = (N, \Rightarrow)$ its transformed graph, and let $\langle S, \prec \rangle$ be a refinement of $\langle \Omega, \prec \rangle$ such that is stable with respect to $\Rightarrow$. Then $\prec(N)$ is a g-iocos-simulation.

*Proof.* Let us consider $(n_1, n_2) \in N(\prec)$. Since $\langle S, \prec \rangle$ is a refinement of $\langle \Omega, \prec \rangle$, we obtain $([n_1]_{\Omega}, [n_2]_{\Omega}) \in \prec$. Then $n_1$ has the form $(s_1, x)$, and $n_2$ has the form $(s_2, y)$ with $x = y$ and $\text{ins}(n_2) \subseteq \text{ins}(n_1)$, hence fulfilling 1 of Definition 8.

Now let us consider $x \in L$ and $n'_1 \in N$ such that $n_1 \xrightarrow{x} n'_1$. By rewriting all those elements at coarse level in $S$ we obtain $([n_1]_S, [n_2]_S) \in \prec$ and $[n_1]_S \Rightarrow \exists [n'_1]_S$. Since $\langle S, \prec \rangle$ is stable there exists $\delta \in S$ such that $[n_2]_S \Rightarrow_{\lor} \delta$ and $([n'_1]_S, \delta) \in \prec$. At discrete level that means there exists $n'_2 \in \delta$ such that $n_2 \Rightarrow n'_2$. Since $\langle S, \prec \rangle$ is a refinement of $\langle \Omega, \prec \rangle$, we obtain $([n'_1]_{\Omega}, [n'_2]_{\Omega}) \in \prec$. Since $n_1 \xrightarrow{x} n'_1$, then $n'_1$ has the form $(s'_1, x)$ (see transformation rules in Definition 7). By the definition of $\Omega$ (Definition 11), then $n'_2$ has also the form $(s'_2, x)$. Therefore $n_2 \xrightarrow{x} n'_2$.
☐

Now Since g-iocos is the maximal g-iocos-simulation, we obtain that $\preceq (N) \subseteq g-iocos$. From this fact is easy to prove the following lemma.

**Lemma 4.** Let $G = (N, \Rightarrow)$ be the transformed graph of an LTS and let $\langle S, \preceq \rangle$ be a partition pair such that $\preceq (N)$ is a g-iocos-simulation. Then $\langle S, \preceq \rangle \sqsubseteq \langle N_{\equiv_{g-iocos}}, \preceq_{g-iocos} \rangle$.

*Proof.* First let us consider $\alpha \in S$ and $a, b \in \alpha$. Since $\preceq$ is reflexive we obtain $(\alpha, \alpha) \in \preceq$ and therefore $(a, b) \in \preceq (N)$ and $(b, a) \in \preceq (N)$. Now considering that $\preceq (N) \subseteq g-iocos$ we obtain $(a, b) \in \equiv_{g-iocos}$. Therefore all elements of $\alpha$ are in the same equivalence class in $N/ \equiv_{g-iocos}$, so $S$ is a refinement of $N/ \equiv_{g-iocos}$. Now let us consider $\alpha, \beta \in \preceq$, let us consider $a, b \in N$ such that $[a]_S = \alpha$ and $[b]_S = \beta$. Since $\preceq (N) \subseteq g-iocos$, we obtain $(a, b) \in g-iocos$ and $([a]_{g-iocos}, [b]_{g-iocos}) \in \preceq_{g-iocos}$. Since $[a]_S \subseteq [a]_{g-iocos}$ and $[b]_S \subseteq [b]_{g-iocos}$, we obtain $([a]_S, [b]_S) \in \preceq_{g-iocos} (S)$. ☐

☐

Finally, we obtain the main theorem of this section.

**Theorem 6.** Let $\mathcal{L} = (S, I, O, \rightarrow)$ be a labelled transition system and $T(\mathcal{L}) = (N, \Rightarrow)$ its transformed graph, then $\langle N_{\equiv_{g-iocos}}, \preceq_{g-iocos} \rangle$ is the solution of the GCPP for the partition pair $\langle \Omega, \preceq \rangle$.

*Proof.* The points a) and b) of the GCPP follows from Lemmas 1, and 2. The maximality follows from Lemmas 3 and 4. ☐

☐

# 5 Conclusions and Future Work

In this paper we have defined an online algorithm that allows to check if a certain implementation *iocos*-conforms a given specification by interacting with it and without computing any a priori set of tests. Under fairly standard hypothesis —even weaker than in other models— we prove the algorithm to be sound and complete.

We plan to introduce test selection criteria and coverage in the *iocos*-theory. This technique is mainly used in offline testing but we think that implementations of the online algorithm we have presented can also benefit from them to further restrict the search tree.

Since *iocos* is a branching semantics, it is essential in the online algorithm to make use of the *copy* clause (see for instance [1] for a more elaborated discussion). While this copy capability will exclude some systems to being tested with *iocos* —essentially unique systems that cannot be replicated— for a vast number of applications, for instance to check software products, it could definitely be a feasible operation. The implementation of our online algorithm is currently under development using cluster computing techniques.

In this paper we have also proved that the conformance relation *iocos*, in spite of its particularities and asymmetry with input and output actions, can
be solved with the GCPP. Actually, we are adapting the mCRL2 toolset [7],
that implements one of the best solution to the GCPP [28], to compute iocos
and the minimised LTS for a give specification. This technique, frequently used
in model checking, allows to reduce the size of the models and therefore the
state explosion in any further testing process. Moreover, we plan to investigate
the logic preservation properties of iocos that would allow to perform model
checking of the intended model specifications and integrate MBT and model
checking in the same theory.

Finally, once the ground model has proved to be useful, we plan to improve
the expressiveness introducing a syntax language and integrating internal τ ac-
tions.

References

1. Samson Abramsky. Observational equivalence as a testing equivalence. *Theoretical Computer Science*, 53(3):225–241, 1987.

2. Luca Aceto, David de Frutos Escrig, Carlos Gregorio-Rodríguez, and Anna Ingolfsdottir. Axiomatizing weak simulation semantics over BCCSP. *Theoretical Computer Science*, To appear, 2013. Available online since 26 March 2013.

3. Axel Belinfante. Jtorx: A tool for on-line model-driven test derivation and execution. In Javier Esparza and Rupak Majumdar, editors, *TACAS*, volume 6015 of *LNCS*, pages 266–270. Springer, 2010.

4. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. *Journal of the ACM*, 42(1):232–268, 1995.

5. Peter E. Bulychev, Thomas Chatain, Alexandre David, and Kim Guldstrand Larsen. Efficient on-the-fly algorithm for checking alternating timed simulation. In Joël Ouaknine and Frits W. Vaandrager, editors, *FORMATS*, volume 5813 of LNCS, pages 73–87. Springer, 2009.

6. Doron Bustan and Orna Grumberg. Simulation-based minimization. *ACM Trans. Comput. Logic*, 4(2):181–206, April 2003.

7. Sjoerd Cranen, JanFriso Groote, JeroenJ.A. Keiren, FrankP.M. Stappers, ErikP. Vink, Wieger Wesselink, and TimA.C. Willemse. An overview of the mcr12 toolset and its recent advances. In Nir Piterman and ScottA. Smolka, editors, *Tools and Algorithms for the Construction and Analysis of Systems*, volume 7795 of LNCS, pages 199–213. Springer Berlin Heidelberg, 2013.

8. David de Frutos-Escrig, Carlos Gregorio-Rodríguez, Miguel Palomino, and David Romero-Hernández. Unifying the linear time-branching time spectrum of process semantics. *Logical Methods in Computer Science*, 9(2:11):1–74, 2013.

9. René G. de Vries and Jan Tretmans. On-the-fly conformance testing using spin. *STTT*, 2(4):382–393, 2000.

10. Ignacio Fábregas, David de Frutos-Escrig, and Miguel Palomino. Logics for contravariant simulations. In John Hatcliff and Elena Zucca, editors, *FMOODS/FORTE*, volume 6117 of LNCS, pages 224–231. Springer, 2010.

11. Raffaella Gentilini, Carla Piazza, and Alberto Policriti. From bisimulation to sim-
ulation: Coarsest partition problems. *J. Autom. Reasoning*, 31(1):73–103, 2003.

12. Carlos Gregorio-Rodríguez, Luis Llana, and Rafael Martínez-Torres. Input-output conformance simulation (iocos) for model based testing. In Dirk Beyer and Michele Boreale, editors, *FMOODS/FORTE*, volume 7892 of LNCS, pages 114–129. Springer, 2013.
13. Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. *Information and Computation*, 86(1):43-68, 1990.

14. Joost-Pieter Katoen, Tim Kemna, Ivan Zapreev, and David N. Jansen. Bisimulation minimisation mostly speeds up probabilistic model checking. In Orna Grumberg and Michael Huth, editors, *Tools and Algorithms for the Construction and Analysis of Systems*, volume 4424 of *Lecture Notes in Computer Science*, pages 87–101. Springer Berlin Heidelberg, 2007.

15. Kim Guldstrand Larsen, Marius Mikucionis, and Brian Nielsen. Online testing of real-time systems using UPPAAL. In J. Grabowski and B. Nielsen, editors, *FATES*, volume 3395 of LNCS, pages 79–94. Springer, 2004.

16. Luis Llana and Rafael Martínez-Torres. Ioco as a simulation. In *3rd Workshop on Formal Methods in the Development of Software, WS-FMDS 2013*, volume to appear of LNCS, 2013.

17. Gerald Lüttgen and Walter Vogler. Ready simulation for concurrency: It's logical! *Information and Computation*, 208(7):845-867, 2010.

18. Robin Milner. An algebraic definition of simulation between programs. In *Proceedings 2nd Joint Conference on Artificial Intelligence*, pages 481-489. BCS, 1971. Report No. CS-205, Computer Science Department, Stanford University.

19. Robin Milner. *A Calculus of Communicating Systems*. LNCS 92. Springer, 1980.

20. Robin Milner. *Communication and Concurrency*. Prentice Hall, 1989.

21. Pablo Rabanal, Ismael Rodríguez, and Fernando Rubio. Testing restorable systems: formal definition and heuristic solution based on river formation dynamics. *Formal Aspects of Computing*, 25(5):743-768, 2013.

22. Francesco Ranzato. A more efficient simulation algorithm on kripke structures. In Krishnendu Chatterjee and Jiri Sgall, editors, *MFCS*, volume 8087 of LNCS, pages 753-764. Springer, 2013.

23. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong, editors, *STOC*, pages 1-9. ACM, 1973.

24. Gerjan Stokkink, Mark Timmer, and Mariëlle Stoelinga. Talking quiescence: a rigorous theory that supports parallel composition, action hiding and determinisation. In Alexander K. Petrenko and Holger Schlingloff, editors, *MBT*, volume 80 of EPTCS, pages 73-87, 2012.

25. Jan Tretmans. Model based testing with labelled transition systems. In R. M. Hilerons, J. P. Bowen, and M. Harman, editors, *Formal Methods and Testing*, volume 4949 of Lecture Notes in Computer Science, pages 1-38. Springer, 2008.

26. Jan Tretmans and Ed Brinksma. Torx: Automated model-based testing. In A. Hartman and K. Dussa-Ziegler, editors, *First European Conference on Model-Driven Software Engineering*, pages 31-43, December 2003.

27. Rob J. van Glabbeek. *Handbook of Process Algebra*, chapter The Linear Time – Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes, pages 3–99. Elsevier, 2001.

28. Rob J. van Glabbeek and Bas Ploeger. Correcting a space-efficient simulation algorithm. In Aarti Gupta and Sharad Malik, editors, *CAV*, volume 5123 of LNCS, pages 517–529. Springer, 2008.

29. Margus Veanes, Colin Campbell, Wolfram Schulte, and Nikolai Tillmann. Online testing with model programs. In Michel Wermelinger and Harald Gall, editors, *ESEC/SIGSOFT FSE*, pages 273–282. ACM, 2005.