{'fraction_non_alphanumeric': 0.04906364453044019, 'fraction_numerical': 0.008465206274618203, 'mean_word_length': 3.809405117979395, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 14, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Ioco Theory for Probabilistic Automata

Model-based testing (MBT) is a well-known technology, which allows for automatic test case generation, execution and evaluation. To test non-functional properties, a number of test MBT frameworks have been developed to test systems with real-time, continuous behaviour, symbolic data and quantitative system aspects. Notably, a lot of these frameworks are based on Tretmans' classical input/output conformance (ioco) framework. However, a model-based test theory handling probabilistic behaviour does not exist yet. Probability plays a role in many different systems: unreliable communication channels, randomized algorithms and communication protocols, service level agreements pinning down up-time percentages, etc. Therefore, a probabilistic test theory is of great practical importance. We present the ingredients for a probabilistic variant of ioco and define the {\pi}oco relation, show that it conservatively extends ioco and define the concepts of test case, execution and evaluation.


Introduction
Model-based testing (MBT) is a way to test systems more effectively and more efficiently. By generating, executing and evaluating test cases automatically from a formal requirements model, more tests can be executed at a lower cost. A number of MBT tools have been developed, such as the Axini test manager, JTorx [1], STG [5], TorXakis [18], Uppaal-Tron [10,16], etc.
A wide variety of model-based test theories exist: the seminal theory of Input/Output conformance [25,27] is able to test functional properties, and has established itself as the robust core with a wide number of extensions. The correct functioning of today's complex cyberphysical systems, depends not only on functional behaviour, but largely on non-functional, quantitative system aspects, such as realtime and performance. MBT frameworks have been developed to support these aspects: To test timing requirements, such as deadlines, a number of timed ioco-variants have been developed, such as [2,10,15]. Symbolic data can be handled by the frameworks in [8,14]; resources by [3], and hybrid aspects in [19]. This paper introduces pioco, a conservative extension of ioco that is able to handle discrete probabilities. Starting point is a requirements model as a probabilistic quiescent transition system (pQTS), an input/output transition system, with two additional features: (1) Quiescence, which models the absence of outputs explicitly via a distinct δ label: quiescence is an important notion in ioco, because a systemunder-test (SUT) may fail a certain test case given an output is required, but the SUT does not provide one. (2) Discrete probabilistic choice. We work in the input-generative / output-reactive model [9], which extend Segala's classical probabilistic automaton model [20]: upon receiving an input, a pQTS chooses probabilistically, which target state to move to. For outputs, a pQTS chooses probabilistically both which action to take, and which state to move to, see Figure 1 for an example.
An important contribution of our paper is the notion of test case execution and evaluation. In particular, we show how the use of statistical hypothesis testing can be exploited to determine the verdict of a test execution: if we execute a test case sufficiently many times and the observed trace frequencies do not 2 Probabilistic quiescent transition systems 2.1 Basic definitions Definition 1. (Probability Distribution) A discrete probability distribution over a set X is a function µ : X −→ [0, 1] such that ∑ x∈X µ (x) = 1. The set of all distributions over X is denoted as Distr (X). The probability distribution that assigns 1 to a certain element x ∈ X is called the Dirac distribution over x and is denoted Dirac (x).

Probabilistic quiescent transition systems
As stated, we consider probabilistic transitions that are input reactive and output generative [9]: upon receiving an input, the system decides probabilistically which next state to move to. However, the system cannot decide probabilistically which inputs to accept. For outputs, in contrast, a system may make a probabilistic choice over various output actions. This means that each transition in a pQTS either involves a single input action, and a probabilistic choice over the target states; or it makes a probabilistic choice over several output actions, together with their target states. We refer to Figure 1 for an example. Moreover, we model quiescence explicitly via a δ -label. Quiescence means absence of outputs and is essential for testing: if the SUT does not provide any outputs, a test must determine whether or not this behaviour is correct. In the non-probabilistic case, this can be done either via the suspension automaton construction [26], or via QTSs [23]. The SA construction involves determinization. However, this is an ill-defined term for probabilistic systems. Therefore, we use the quiescent-labelling approach and demand to make quiescence explicit.
Finally, we assume that our pQTSs are finite and don't contain internal steps (i.e., τ-transitions).
• s 0 ∈ S the initial state, • L I and L δ O disjoint sets of input and output actions, with at least δ ∈ L δ O . We write L := L I ∪ L δ O for the set of all labels and let We write s µ,a → s if (s, µ) ∈ ∆ and µ (a, s ) > 0; and s → a if there are µ ∈ Distr (L × S) and s ∈ S such that s µ,a → s . If it is not clear from the context about which system we are talking, we will write s µ,a → A s , (s, µ) A and s → A a to clarify ambiguities. Lastly we say that A is input enabled if for all s ∈ S we have s → a? for every a ∈ L I .

Paths and traces
We define the usual language-theoretic concepts for pQTSs. where s i ∈ S, a i ∈ L for i = 1, 2, . . . and µ ∈ Distr (L, S), such that each finite path ends in a state and s i µ i ,a i → s i+1 for each nonfinal i. We use the notation first (π) := s 1 to denote the first state of a path, as well as last (π) := s n for a finite path ending in s n , and last (π) = ∞ for infinite paths. The set of all finite paths of a pQTS A is denoted by Path * (A ) and the set of all infinite paths by Path (A ) respectively.
• We write reach A (S , σ ) for the set of reachable states of a subset S ⊆ S via σ , i.e. reach A (S , σ ) = s ∈ S | ∃s ∈ S : s σ ⇒ s .
• We write after A (s) for the set of actions, enabled from state s, i.e. after A (s) = {a ∈ L | s → a}.
We lift this definition to traces by defining after A (s) .
• We write out A (σ ) = after A (σ ) ∩ L δ O to denote the set of all output actions as well as quiescence after trace σ .
In order for a pQTS to be meaningful, [23] postulated four well-formedness rules about quiescence, stating for instance that quiescence should not be succeeded by an output action. Since our current treatment does not rely on well-formedness, we omit these rules here. Moreover, our definition of a test case is a pQTS that does not adhere to the well-formedness criteria.

Trace distributions
Very much like the visible behaviour of a labelled transition system is given by its traces, the visible behaviour of a pQTS is given by its trace distributions: each trace distribution is a probability space that assigns a probability to (sets of) traces [20]. Just as a trace in an LTS is obtained by first selecting a path in the LTS and by then removing all states and internal actions, we do the same in the probabilistic case: we first resolve all the nondeterministic choices in the pQTS via an adversary, and by then removing all states -recall that our pQTSs do not contain internal actions. The resolution of the nondeterminism via an adversary leads to a purely probabilistic structure where we can assign a probability to each finite path, by multiplying the probabilities along that path. The mathematics to handle infinite paths is more complex, but completely standard [6]: in non-trivial situations, the probability assigned to an individual trace is 0 (cf., the probability to always roll a 6 with a dice is 0). Hence, we consider the probability assigned to sets of traces (e.g., the probability that a 6 turns up in the first 100 dice rolls). A classical result in measure theory shows that it is impossible to assign a probability to all sets of traces. Therefore, we collect those sets that can be assigned a probability in a so-called σ -field F .
Adversaries. Following the standard theory for probabilistic automata [21], we define the behavior of a pQTS via adversaries (a.k.a. policies or schedulers). These resolve the nondeterministic choices in pQTSs: in each state of the pQTSs, the adversary chooses which transition to take. Adversaries can be (1) history-dependent, i.e. the choice which transition to take can depend on the full history; (2) randomized, i.e. the adversary may make a random choice over all outgoing transitions; and (3) partial, i.e., at any point in time, a scheduler may decide, with some probability, to terminate the execution.
Thus, given any finite history leading to a current state, an adversary returns a discrete probability distribution over the set of available next transitions (distributions to be precise). In order to model termination, we define schedulers which continue the transitions of pQTSs with a halting extension.
We say that an adversary halts after k ∈ N steps, if it halts for every path π with |π| ≥ k. We denote all such adversaries by Adv The probability space assigned to an adversary. Intuitively an adversary tosses a coin at every step of the computation, thus resulting in a purely probabilistic (as opposed to nondeterministic) computation tree.
Loosely speaking, we follow a finite path in the transition system and multiply every scheduled probability along the way, resolving every nondeterminism according to the adversary E to get the ultimate path probability. The path probability function enables us to define a probability space associated with an adversary, thus giving every path in a pQTS A an exact probability.
Definition 7. (Adversary Probability Space) Let E be an adversary of A . The unique probability space associated to E is the probability space (Ω E , F E , P E ) given by. 1.
3. P E is the unique probability measure on F E s. t. P E (C π ) = Q E (π), for all π ∈ Path * (A ).
The set of all adversaries is denoted by adv (A ) with adv (A , k) being the set of adversaries halting after k ∈ N respectively.
Trace distributions. As we mentioned, a trace distribution is obtained from (the probability space assigned to) an adversary by removing all states. This means that the probability assigned to a set of traces X is defined as the probability of all paths whose trace is an element of X.
As an abbreviation, we will write P H (β ) := P H C β for β ∈ L * A Like before, we denote the set of trace distributions based on adversaries of A by trd (A ) and trd (A , k) if it is based on an adversary halting after k ∈ N steps respectively. Lastly we write where the embedding means that for every trace distribution H of A there is a trace distribution H of B such that for all traces σ of A , we have P H (σ ) = P H (σ ).
The fact that (Ω E , F E , P E ), (Ω H , F H , P H ) really define probability spaces, follows from standard measure theory arguments (see [6]).
We can see that this system has both probabilistic and nondeterministic choices. Observe that it has indeed only input reactive and output generative transitions as mentioned in the beginning of 2.2.
We will now consider an adversary E for A . The only nondeterministic choice we have in this system, is located at state s 0 , where we can either apply a? to enter the left branch, a? to enter the right branch, or do nothing (corresponding to µ 0 1 , µ 0 2 and µ 0 3 respectively). Therefore consider the adversary E (s 0 ) (µ 0 1 ) = 1 2 and E (s 0 ) (µ 0 2 ) = 1 2 and E (π) (µ) = Dirac for every other distribution µ after a path π (i.e. those are taken with probability 1).

The pioco relation
The classical input-output conformance relation ioco states that an implementation A i conforms to a specification A s if A i never provides any unspecified output. In particular this refers to the observation of quiescence, when other output was expected.
To generalize ioco to pQTSs, we introduce two auxiliary concepts. For a natural number k, the prefix relation H k H states that trace distribution H assigns exactly the same probabilities as H to traces of length k and halts afterwards. The output continuation of a trace distribution H prolongs the traces of H with output actions. More precisely, output continuation of H wrt length k contains all trace distributions that (1) coincide with H for traces upto length k and (2) the k + 1st action is an output label (incl δ ); i.e. traces of length k + 1 that end on an input action are assigned probability 0. Recall that P H (σ ) abbreviates P H (C σ ).  We are now able to define the core idea of pioco. Intuitively an implementation should conform to a specification, if the probability of every trace in A i specified in A s , can be matched in the specification. Just as in ioco, we will neglect underspecified traces continued with input actions (i.e., everything is allowed to happen after that). However, if there is unspecified output in the implementation, there is at least one adversary that schedules positive probability to this continuation, which consequently cannot be matched of output-continuations in the specification. Definition 12. Let A i and A s be two pQTS. Furthermore let A i be input enabled, then we say A i pioco A s if and only if Example 13. Consider the two systems of A and B shown in Figure 2 and assume that p ∈ [0, 1]. It is true that A pioco B, because we can always choose an adversary E of B, which imitates the probabilistic behaviour of B, i.e. choose E(ε)(µ) = ν such that ν (a!,t 1 ) = p and ν (b!,t 2 ) = 1 − p.
However, the opposite does not hold. For example assume p = 1 2 , then the trace distribution H assigning P H (a!) = 1 is in outcont (H, B, 1) but not in outcont (H, A , 1) and hence B pioco A .

Properties of the p-ioco relation
As stated before, the relation pioco conservatively extends the ioco relation, i.e. both relations coincide for non-probabilistic QTSs. Moreover, we show that several other characteristic properties of ioco carry over to pioco as well. Below, a QTS is a pQTS where every occurring distribution is the Dirac distribution.
Theorem 14. Let A i and A s be two QTS and let A i be input enabled, then Intuitively it makes sense that the implementation is input enabled, since it should accept every input at any time. The following two results justify, that we assume the specification to be not input enabled, since otherwise pioco would coincide with trace distribution inclusion. Equivalently it is known that ioco coincides with trace inclusion, if we assume both the implementation and the specification were input enabled. Thus, as stated before, we can see that pioco extends ioco.

Theorem 16. Let A i and A s be two input enabled pQTS, then
Next, we show that, under some input-enabledness restrictions, the pioco relation is transitive. Again, note that this is also true for ioco for non-probabilistic systems.
Theorem 17. (Transitivity of pioco) Let A , B and C be pQTS, such that A and B are input enabled, then 4 Testing for pQTS 4

.1 Test cases for pQTSs.
We will consider tests as sets of traces based on an action signature L I , L δ O , which will describe possible behaviour of the tester. This means that at each state in a test case, the tester either provides stimuli or waits for a response of the system. Additionally to output conformance testing like in [24], we introduce probabilities into our testing transition system. Thus we can represent each test case as a pQTS, albeit with a mirrored action signature (L O , L I ∪ {δ }). This is necessary for the parallel composition of the test pQTS and the SUT.
Since we consider tests to be pQTS, we also use all the terminology introduced earlier on. Additionally we require tests to not contain loops (or infinite paths respectively).   For a given specification pQTS A s = S, s 0 , L I , L δ O , ∆ , we say that a test t is a test for A s , if it is based on the same action signature L I , L δ O . Similar to before, we denote all tests for A s by T (A s ) and all test suites by T S (A s ) respectively.
Note that we mirrored the action signature for tests, as can be seen in Figure 3a and Figure 3b respectively. That is, because we require tests and implementations to shake hands on shared actions. A special role is dedicated to quiescence in the context of parallel composition, since the composed system is considered quiescent if and only if the two systems are quiescent.
We will proceed to define parallel composition. Formally this means that output actions of one component are allowed to be present as input actions of the other component. These will be synchronized upon. However, keeping in mind the mirrored action signature of tests, we wish to avoid possibly unwanted synchronization, which is why we introduce system compatibility.
Before we parallel compose a test case with a system, we obviously need to define which outcome of a test case is considered correct, and which is not (i.e., when it fails).

Definition 21. (Test case annotation) For a given test t a test annotation is a function
a : ctraces (t) −→ {pass, fail} .
A pairt = (t, a) consisting of a test and a test annotation is called an annotated test. The set of all sucht is defined asT = (t i , a i ) i∈I for some index set I is called annotated Test Suite. If t is a test case for a specification A s we define the pioco test annotation a pioco A s ,t : pass otherwise.

Test execution.
By taking the intersection of all complete traces within a test and all traces of an implementation, we will define the set of all traces that will be executed by an annotated test case. Example 23. Consider the specification of a shuffle music player and a derived test for it given in Figure  3. Assuming we are to test whether or not the following two implementations conform to the specification with respect to pioco: Here p 1 , . . . , p N ∈ [0, 1] such that ∑ N i=1 p i = 1. Now when we compose A i 1 with t in Figure3b, we can clearly see that every complete trace of the parallel system is annotated with fail, as it would also have been the case for classical ioco theory. However, if we now also consider A i 2 and compose it with the same test t, every trace of the composed system would be given a pass label if we restricted ourselves to the annotation function and the output verdict. Note how every trace shuffle?·Song_i! is given probability p i for i = 1, . . . , N. The only restriction we assumed valid for p 1 , . . . , p N is that they sum up to 1 so a correct distribution for A i 2 would be p 1 = N−1 N and p 2 = . . . = p N = 1 N 2 . This, however, should intuitively not be given the verdict pass, since it differs from the uniform distribution given in the specification A s .

Test evaluation
In order to give a verdict of whether or not the implementation passed the test (suite), we need to extend the test evaluation process of classical ioco testing with a statistical component. Thus the idea of evaluating probabilistic systems becomes two folded. On the one hand, we want that no unexpected output (or unexpected quiescence) ever occurs during the execution. On the other hand, we want the observed frequencies of the SUT to conform in some way to the probabilities described in the specification. Thus the SUT will pass the test suite only if it passes both criteria. We will do this by augmenting classical ioco theory with zero hypothesis testing, which will be discussed in the following.
To conduct an experiment, we need to define a length k ∈ N and a width m ∈ N first. This refers to how long the traces we want to record should be and how many times we reset the machine. This will give us traces σ 1 , . . . , σ m ∈ L k , which we call a sample. Additionally, we assume that the implementation is governed by an underlying trace distribution H in every run, thus running the machine m times, gives us a sequence of possibly m different trace distributions H = H 1 , . . . , H m . So in every run the implementation makes two choices: 1) It chooses the trace distribution H and 2) H chooses a trace σ to execute. Consequently that means that once a trace distribution H i is chosen, it is solely responsible for the trace σ i . Thus for i = j the choice of σ i is independent from the choice of σ j .
Our statistical analysis is build upon the frequencies of traces occurring in a sample O. Thus the frequency function will be defined as Note that although every run is governed by possibly different trace distributions, we can still derive useful information from the frequency function. For fixed k, m ∈ N and H, the sample O can be treated as a Bernoulli experiment of length m, where success occurs in position i = 1, . . . m, if σ = σ i . The success probability is then given by P H i (σ ). So for given H, the expected value for σ is given by . Note that this expected value E H is the expected distribution over L k if we assume it is based on the m trace distributions H.
In order to apply zero hypothesis testing and compare an observed distribution with E H , we will use the notion of metric spaces. This will enable us to measure deviation of two distributions. We will use the metric space L k , dist , where dist is the euclidean distance of two distributions defined as Now that we have a measure of deviation, we can say that a sample O is accepted if freq (O) lies in some distance r of the expected value E H , or equivalently if freq (O) is contained in the closed ball B r E H = ν ∈ Distr L k | dist ν, E H ≤ r . Then the set freq −1 B r E H summarizes all samples that deviate at most r from the expected value. An inherent problem of hypothesis testing are the type 1 and type 2 errors, i.e. the probability of falsely accepting the hypothesis or falsely rejecting it. This problem is established in our framework by the choice of a level of significance α ∈ [0, 1] and connected with it, the choice of radius r for the ball mentioned above. So for a given level of significance α the following choice of the radius will in some sense minimize the probability of false acceptance of an erroneous sample and of false rejection of a valid sample (i.e., at most α).
Thus assuming we have m different underlying trace distributions, we can determine when an observed sample seems reasonable and is declared valid. Unifying over all sets of such H, we will define the total set of acceptable outcomes, called Observations.
Definition 24. The acceptable outcomes of H with significance level α ∈ [0, 1] are given by the set of samples of length k ∈ N and width m ∈ N, defined as The set of observations of A with significance level α ∈ [0, 1] is given by Obs H, α .
Example 25. Assume that the wanted level of significance is given by α = 0.05 and consider the probabilistic automaton in Figure 4 representing the toss of a fair coin. Furthermore assume that we are given two samples of depth k = 2 and width m = 100.
To sample this case, assume E is the adversary that assigns probability equal to 1 to the unique outgoing transition (if there is one) and probability 1 to halting, in case there is no outgoing transition. We take H = trd (E) and can see, that then µ H (a?b!) = µ H (a?c!) = 1 2 and µ H (σ ) = 0 for all other sequences σ . We define H 100 = (H 1 , . . . , H 100 ), where H 1 = . . . = H 100 = H. As we can see, we have E H 100 = µ H . Since µ H only assigns positive probability to a?b! and a?c!, we get P H 100 (B r (µ H )) = O| 1 2 − r ≤ freq (O) (a?b!) ≤ 1 2 + r . One can show that the smallest ball, where this probability is greater or equal than 0.95 is given by the ball of radiusr = 1 10 . Thus a sample O 1 , which consists of 42 times a?b! and 58 times a?c! is an observation, and a sample O 2 , which consists of 38 times a?b! and 62 times a?c! is not.
Thus we can finally define a verdict function, that assigns pass when a test case never finds erroneous behaviour (i.e. wrong output or wrong probabilistic behaviour).
(Verdict function) For any given A i , we assign the verdict We extend V α t to a function V α T : pQT S → {pass, fail}, which assigns verdicts to a pQTS based on a given annotated test suite by V α T (A i ) = pass if for allt ∈T and V α T (A i ) = fail otherwise.

Conclusion and Future Work
We introduced the core of a probabilistic test theory by extending classical ioco theory. We defined the conformance relation pioco for probabilistic quiescent transition systems, and proved several characteristic properties. In particular, we showed that pioco is a conservative extension of ioco. Second, we have provided definitions of a test case, test execution and test evaluation. Here, test execution is crucial, since it needs to assess whether the observed behaviour respects the probabilities in the specification pQTS. Following [4], we have used statistical hypothesis testing here. Being a first step, there is ample future work to be carried out. First, it is important to establish the correctness of the testing framework, by showing the soundness and completeness. Second, we would like to implement our framework in the MBT testing framework JTorX, and test realistic applications. Also, we would like to extend our theory to handle τ-transitions. Finally, we think that tests themselves should be probabilistic, in particular since many MBT tools in practice do already choose their next action probabilistically.
By assumption we know that H ∈ trd (A s , m + 1). In particular that means there must be at least one adversary E ∈ adv (A s , m + 1) such that trd (E) = H. However, for this adversary, we know that H * m trd (E) and for all σ ∈ L m L I we have P trd(E) (σ ) = 0 and by trace distribution inclusion trd (E) = H. Thus H ∈ outcont (H * , A s , m) and therefore A i pioco A s .
Proof of Theorem 16. " =⇒ " Let A i pioco A s , fix m ∈ N and take a trace distribution H * ∈ trd (A i , m). To show that H * ∈ trd (A s , m), we prove that every prefix of H * is in trd (A s , m), i.e. if H k H * for some k ∈ N, then H ∈ trd (A s ). The proof is by induction up to m ∈ N over the prefix trace distribution length, denoted by k.
Obviously H ∈ trd (A i , 0) yields both H 0 H * and H ∈ trd (A s ). Now assume, we know that H k H * for some k < m and H ∈ trd (A s ). Furthermore let H ∈ trd (A i , k + 1), such that H k+1 H * . If we can show that H ∈ trd (A s , k + 1), we are done.
With H ∈ trd (A s , k), we take H ∈ outcont (H , A i , k) such that all traces of length k + 1 ending in an output action have the same probability, i.e. for all σ ∈ L k L δ O , we have P H (σ ) = P H (σ ). By assumption A i pioco A s and thus H ∈ outcont (H , A s , k) ⊆ trd (A s ).
Let E ∈ adv (A s , k + 1) the corresponding adversary such that trd (E) = H . By construction, we have P trd(E) (σ a!) = P H (σ a!) and P trd(E) (σ b?) = 0 in general = P H (σ b?) for all σ ∈ L k . We create yet another adversary, denoted by E ∈ adv (A s , k + 1) such that for all σ ∈ L k and a! ∈ L δ O , we have P trd(E) (σ ) = P trd(E ) (σ ) and P trd(E) (σ a!) = P trd(E ) (σ a!). Taking the sum over all probabilities of those traces yields The aim is now to set the behaviour of E such that σ ∈ L k L I has P H (σ ) = P trd(E ) (σ ). We prove that this can indeed be done independently from σ . The input enabledness gives that for all σ b? ∈ traces (A i ), we also have σ b? ∈ traces (A s ). Assume P H (σ ) = p and thus However, since trd (E) k H , we also have P trd(E) (σ ) = p.
The last detail not yet specified about E is the behaviour of paths of length k + 1 ending in an input transition. We demonstrate the choice of E for pα 1 ! = P trd(E ) (σ b 1 ?), and denote the associated paths {π 1 , . . . , π n } = trace −1 (σ ). Furthermore π i := π i µb 1 ?s i j for some s i j ∈ S, j = 1, . . . , l, which are reachable after π i and distributions containing b?. Thus we want We can do the same for all α i for i = 1, . . . , ω. Note that the choice of the adversary does not depend on the chosen trace σ but solely on the presupposed behaviour of H . Thus we have found E ∈ adv (A s , k + 1) such that trd (E ) = H . Hence H ∈ trd (A s , k + 1), which ends the induction. Since this is possible for every m ∈ N, we get A i ⊆ pioco A s , ending the proof.
" ⇐= " See Lemma 15 for the proof. In particular we do not even require input enabledness for A s in this case.
Proof of Theorem 17. Let A pioco B and B pioco C and A and B be input enabled. By Theorem 16 we know, that A TD B. So let k ∈ N and H * ∈ trd (A , k). Consequently also H * ∈ trd (B, k) and thus the following embedding holds outcont (A , H * , k) ⊆ outcont (B, H * , k) ⊆ outcont (C , H * , k) , and thus A pioco C .