Das Kapitel beginnt mit der Einführung des Konzepts der Konformitätsprüfung für deterministische Automaten und betont die Bedeutung von Äquivalenzabfragen im Automatenlernen. Er diskutiert die Grenzen erschöpfender Tests in Black-Box-Umgebungen und führt das Konzept vollständiger Testsuiten ein, die unter bestimmten Annahmen Äquivalenz garantieren. Die W-Methode, eine klassische Konstruktion für m-komplette Testsuiten, wird detailliert untersucht und ihre Erweiterungen und Verbesserungen hervorgehoben. Der Text wechselt dann zu einer kategorischen Perspektive und verallgemeinert die W-Methode auf Automaten in monoiden geschlossenen Kategorien. Diese Einstellung ermöglicht eine bequeme Definition von Erreichbarkeit und Sprachäquivalenz, die ein breites Spektrum von Automatentypen abdeckt. Der Hauptbeitrag des Kapitels ist die Definition und der Nachweis der (m) -Vollständigkeit von Testsuiten auf dieser allgemeinen Ebene, die in bekannte und neuartige Automatenklassen eingegliedert werden. Das Kapitel bietet auch einen detaillierten Vergleich mit verwandten Arbeiten und skizziert potenzielle Wege für zukünftige Forschung, was es zu einer umfassenden Ressource für fortgeschrittene Studien im Bereich Konformitätsprüfung und Automatentheorie macht.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Conformance testing of automata is about checking the equivalence of a known specification and a black-box implementation. An important notion in conformance testing is that of a complete test suite, which guarantees that if an implementation satisfying certain conditions passes all tests, then it is equivalent to the specification.
We introduce a framework for proving completeness of test suites at the general level of automata in monoidal closed categories. Moreover, we provide a generalization of a classical conformance testing technique, the W-method. We demonstrate the applicability of our results by recovering the W-method for deterministic finite automata, Moore machines, and Mealy machines, and by deriving new instances of complete test suites for weighted automata and deterministic nominal automata.
Hinweise
This research is supported by the NWO grant No. VI.Vidi.223.096.
1 Introduction
In conformance testing of deterministic automata, the problem is to check the equivalence of a known specification and a black-box implementation [15]. This form of testing is widely used, for instance, in practical implementations of automata learning, where one aims to infer an automaton model by systematically interacting with a black-box system [27, 28, 50]. In particular, conformance testing is a standard technique to evaluate whether a learned model is correct. In Angluin’s [4] minimally adequate teacher (MAT) framework for active automata learning, this is referred to as an equivalence query — which, when the system under learning really is a black-box, can only be implemented through testing.
In a black-box setting, testing can never be exhaustive [42]: for any (finite) collection of tests, we can construct a faulty implementation that passes all the tests. However, under certain assumptions on the implementation, it is possible to construct test suites which guarantee equivalence. These test suites are called complete. In particular, an m-complete test suite is complete with respect to all implementations with at most m states. The W-method [19, 52] is a classical construction of an m-complete test suite, which has been extended and improved in numerous ways (see [21, 35, 40] for an overview). State-of-the-art libraries for automata learning [29, 43] implement various (randomised) versions of these test suites to evaluate the equivalence query.
Anzeige
Active automata learning has been extended from deterministic finite automata [4] to a wide range of system types, such as Mealy machines [39], non-deterministic automata [12], register automata [1, 13, 18], nominal automata [41], weighted automata [8, 10, 25], automata over infinite words [5, 38], and probabilistic models [48]. Moreover, automata learning algorithms have been generalized to the abstract level of category theory [9, 20, 26, 49]. However, most variants of complete test suites are only developed for Mealy machines and DFAs. While the abstract frameworks for automata learning rely on equivalence queries, a general theory of evaluating these in practice through conformance testing is missing. Developing such a theory is relevant, as evaluating the equivalence query is often the bottleneck in automata learning [7].
In this paper, we study conformance testing at the generality of machines in a category, more specifically in monoidal closed categories. This setting goes back to classical work by Arbib and Manes [6], Goguen [24], and Adámek and Trnková [3]. This setting allows us to conveniently define reachability and language equivalence, by viewing automata both as algebras and as coalgebras.
Our main contribution is to define the W-method and to provide a framework for proving (m)-completeness of test suites at the general level of automata in monoidal closed categories. To this end, we generalize part of the bisimulation-based proof presented in [34] for Mealy machines, which ultimately goes back to [19, 52]. In particular, our main result allows us to prove completeness under the assumption that the we can reach all states in the implementation, a property guaranteed by the W-method in concrete cases. We instantiate our approach to recover known complete test suites for deterministic finite automata, Mealy machines, and Moore machines. We go on to instantiate it to weighted automata [22] and deterministic nominal automata [11], providing, to the best of our knowledge, the first account of complete test suites for these systems.
Related work. Our approach is inspired by the categorical automata learning framework of Urbat and Schröder [49], which similarly relies on the possibility of viewing automata as both algebras and coalgebras in the more general setting of adjoint automata. We address conformance testing instead of automata learning.
Anzeige
There is extensive literature on advanced complete test suites for concrete models, in particular for DFAs and Mealy machines (but also for e.g. NFAs [44] and other conformance relations such as ioco [14]). In this paper, we focus on the W-method, which conceptually underlies many of these techniques, as a first step towards a categorical theory of conformance testing.
In [31], a coalgebraic conformance testing theory is developed for Mealy machines with monadic effects. The focus in op. cit. is on modelling test purposes and execution at that level, but not on m-completeness.
Outline. In Section 2, we provide background on conformance testing and an overview of our approach. Then, in Section 3, we set the scene for the generalized test suite construction by recalling automata in monoidal closed categories and related concepts such as words and languages. We introduce our framework for proving completeness of test suites in Section 4. In Section 5, we use our results to obtain complete test suites for all the abovementioned classes of automata. Finally, Section 6 summarizes our results and discusses further work.
We assume familiarity with basic category theory [37]. Some notions we rely on are recalled in appendix [33]. Most proofs are also deferred to the appendix.
Notation. We write gf or \(g \circ f\) for the composition of morphisms g and f. We denote the product of X and Y by \(X \times Y\). For \(f :Z \rightarrow X\) and \(g :Z \rightarrow Y\), we let \(\langle f, g \rangle :Z \rightarrow X \times Y\) denote the tupling of f and g. The coproduct of X and Y is written as \(X + Y\). For \(f :X \rightarrow Z\) and \(g :Y \rightarrow Z\), we denote by \({[}f, g{]} :X + Y \rightarrow Z\) the cotupling of f and g. The coproduct of a family of objects \((X_i)_{i \in I}\) is written as \(\sum _{i \in I}{X_i}\). For a family of morphisms \(f_i :X_i \rightarrow Y\) indexed by \(i \in I\), we write \([f_i]_{i \in I} :\sum _{i \in I}{X_i} \rightarrow Y\) for the cotupling of the family. Furthermore, we write \(\kappa _{i} :X_i \rightarrow \sum _{i \in I}{X_i}\) for the coproduct injections.
2 Overview
In this section, we review some background on conformance testing and the W-method in particular, and we explain our approach to generalizing the test suite construction and the proof of its completeness.
Complete Test Suites. Let us introduce some terminology for conformance testing in the case of deterministic finite automata. For this section, we fix a set \(\varSigma \) of input symbols. A deterministic finite automaton (DFA) [46] is a tuple \((Q, q_0, \delta , F)\), where Q is a finite set of states, \(q_0 \in Q\) is an initial state, \(\delta :Q \times \varSigma \rightarrow Q\) is a transition function, and \(F \subseteq Q\) is a set of final states. The size of a DFA \(\mathcal {A} = (Q, q_0, \delta , F)\) is \(|\mathcal {A}| = |Q|\). The transition function \(\delta \) of \(\mathcal {A}\) extends to words over \(\varSigma \) as a function \(\delta ^* :Q \times \varSigma ^{*}\rightarrow Q\) as usual. We write \(q \in \mathcal {A}\) to mean \(q \in Q\).
Definition 2.1
Let \(\mathcal {A} = (Q, q_0, \delta , F)\) and \(\mathcal {B} = (Q', q_0', \delta ', F')\) be two DFAs.
(i)
The accepted language of \(q \in Q\) is \(L_{\mathcal {A}}(q) = \left\{ w \in \varSigma ^{*}\ |\ \delta ^*(q, w) \in F \right\} \). The accepted language of \(\mathcal {A}\) is \(L_{\mathcal {A}} = L_{\mathcal {A}}(q_{0}]\).
(ii)
Given a set \(L \subseteq \varSigma ^{*}\) of words, we say that two states \(p \in Q\) and \(q \in Q'\) are L-equivalent, denoted by \(p \sim {_{L}\,\,} q\), if \(L_{\mathcal {A}}(p) \cap L = L_{\mathcal {B}}(q) \cap L\). In the case \(L = \varSigma ^{*}\), we say that p and q are equivalent, denoted by \(p \sim {{q}}\). We write \(\mathcal {A} \sim _{L} \mathcal {B}\) for \(q_0 \sim {_{L}\,\,} q_0'\). We say that \(\mathcal {A}\) and \(\mathcal {B}\) are equivalent, denoted by \(\mathcal {A} \sim \mathcal {B}\), if \(q_0 \sim {{q_0'}}\).
(iii)
We say that \(\mathcal {A}\) is minimal if for all \(p, q \in Q\), \(p \sim {{q}}\) implies \(p = q\).
We now define the vocabulary for conformance testing. A test suite is a finite set \(T \subseteq \varSigma ^{*}\) of words. In the following, we use the symbol \(\mathcal {\mathcal {S}}\) for the specification and the symbol \(\mathcal {\mathcal {M}}\) for the implementation. We say that \(\mathcal {\mathcal {S}}\) and \(\mathcal {\mathcal {M}}\)agree on a test suite T if \(\mathcal {\mathcal {S}} \sim _{T} \mathcal {\mathcal {M}}\).
Since for any test suite, there exists a faulty implementation that agrees on all the tests, we need to restrict the space of possible faulty implementations to achieve completeness. This motivates the definition of a fault domain.
Definition 2.2
(i)
A fault domain is a collection of DFAs.
(ii)
Let \(\mathcal {\mathcal {S}}\) be an automaton. A test suite \(T \subseteq \varSigma ^{*}\) is complete for \(\mathcal {\mathcal {S}}\) with respect to a fault domain \(\mathcal {U}\) if for all DFAs \(\mathcal {\mathcal {M}} \in \mathcal {U}\), \(\mathcal {\mathcal {S}} \sim _{T} \mathcal {\mathcal {M}}\) implies \(\mathcal {\mathcal {S}} \sim \mathcal {\mathcal {M}}\).
Intuitively, a test suite is complete if it contains a failing test case for every inequivalent DFA in the given fault domain.
A fault domain that has often been considered in the literature [19, 21, 40, 52] is the collection \(\mathcal {U}_{m}\) of all DFAs that have at most m states, for some \(m \in \mathbb {N}\). Test suites that are complete with respect to this fault domain are called m-complete.
The W-method. The method of Vasilevskii and Chow, termed the W-method, constructs a test suite based on the specification using sets of words with special properties, called a state cover and a characterization set. A state cover P is a set of words containing sequences with which we can cover the whole state space, and a characterization set contains words that distinguish inequivalent states.
Definition 2.3
(i)
A state cover for a DFA \(\mathcal {\mathcal {S}} = (Q, q_0, \delta , F)\) is a finite set \(P \subseteq \varSigma ^{*}\) of words that contains the empty word and contains, for each state \(q \in Q\), an access sequence for q, i.e., a word \(w \in \varSigma ^{*}\) such that \(\delta ^*(q_0, w) = q\).
(ii)
A characterization set for a DFA \(\mathcal {\mathcal {S}}\) is a finite set \(W \subseteq \varSigma ^{*}\) of words such that \(\varepsilon \in W\) and for all states \(p, q \in \mathcal {\mathcal {S}}\), \(p \sim {_{W}\,\,} q\) implies \(p \sim {{q}}\).
Intuitively, a characterization set contains a so-called distinguishing sequence for any pair of inequivalent states p and q, i.e. a word \(w \in \varSigma ^{*}\) such that \(w \in L_{\mathcal {\mathcal {S}}}{(p)}\) and \(w \notin L_{\mathcal {\mathcal {S}}}{(q)}\) or vice-versa. Note that, by definition, such a distinguishing sequence always exists for inequivalent states.
We are now in the position to define the W-method. In the following definition, the symbol \(\cdot \) denotes concatenation of languages.
Definition 2.4
Let \(\mathcal {\mathcal {S}}\) be a DFA. Let P be a state cover for \(\mathcal {\mathcal {S}}\), let W be a characterization set for \(\mathcal {\mathcal {S}}\), and let k be a natural number. Then the W test suite of order k associated to P and W is defined as \(T^{k}_{P,W} = P \cdot \varSigma ^{\le k+1} \cdot W\).
The state cover P makes sure that we reach all states in the specification. The role of the infixes \(\varSigma ^{\le k+1}\) is to reach states in the implementation. Finally, the characterization set W is used to distinguish the states reached in the specification and the implementation after reading a word from \(P \cdot \varSigma ^{\le k+1}\).
It is a classical result [19, 52] that the W-method of order k is \(n + k\)-complete, where n is the number of states of the specification. This can be proven in two steps; this proof strategy is also used in [40] and [34]. The first step is to construct a state cover for the implementation from a state cover of the specification.
Lemma 2.5
Let \(\mathcal {\mathcal {S}}\) be a DFA with \(n = |\mathcal {\mathcal {S}}|\), and let \(\mathcal {\mathcal {M}} \in \mathcal {U}_{n + k}\) for some \(k \in \mathbb {N}\). Suppose that \(P \subseteq \varSigma ^{*}\) is a state cover for \(\mathcal {\mathcal {S}}\) and \(W \subseteq \varSigma ^{*}\) is a characterization set for \(\mathcal {\mathcal {S}}\). Suppose furthermore that \(\mathcal {\mathcal {S}}\) is minimal and \(\mathcal {\mathcal {S}} \sim _{P \cdot W} \mathcal {\mathcal {M}}\). Then \(P \cdot \varSigma ^{\le k}\) is a state cover for \(\mathcal {\mathcal {M}}\).
Second, we prove equivalence of two DFAs using a state cover for the implementation and the assumption that the two machines agree on suitable tests.
Lemma 2.6
Let \(\mathcal {\mathcal {S}}\) and \(\mathcal {\mathcal {M}}\) be two DFAs, and suppose \(C \subseteq \varSigma ^{*}\) is a state cover for \(\mathcal {\mathcal {M}}\) and \(W \subseteq \varSigma ^{*}\) is a characterization set for \(\mathcal {\mathcal {S}}\). Assume that \(\mathcal {\mathcal {S}}\) is minimal, and let \(T = C \cdot \varSigma ^{\le 1} \cdot W\). Then \(\mathcal {\mathcal {S}} \sim _{T} \mathcal {\mathcal {M}}\) implies \(\mathcal {\mathcal {S}} \sim \mathcal {\mathcal {M}}\).
For a proof of the above two lemmas in the case of Mealy machines, we refer the reader to [34]. In both lemmas, we assumed minimality of the specification: this is fine, as we can apply any minimization algorithm to a potential non-minimal specification. Furthermore, the hypotheses produced in active learning algorithms are generally minimal.
Altogether, we obtain \(n+k\)-completeness of the W-method.
Corollary 2.7
Let \(\mathcal {\mathcal {S}}\) be a minimal DFA with \(n = |\mathcal {\mathcal {S}}|\). Then for all state covers \(P \subseteq \varSigma ^{*}\) for \(\mathcal {\mathcal {S}}\), for all characterization sets \(W \subseteq \varSigma ^{*}\) for \(\mathcal {\mathcal {S}}\), and for all \(k \in \mathbb {N}\), the test suite \(T^{k}_{P,W}\) is \(n+k\)-complete for \(\mathcal {\mathcal {S}}\).
Proof
Let \(\mathcal {\mathcal {M}} \in \mathcal {U}_{n+k}\), and suppose \(\mathcal {\mathcal {S}} \sim _{T^{k}_{P,W}} \mathcal {\mathcal {M}}\). Since \(P \cdot W \subseteq T^{k}_{P,W}\), we also have \(\mathcal {\mathcal {S}} \sim _{P \cdot W} \mathcal {\mathcal {M}}\). Hence, by Lemma 2.5, \(P \cdot \varSigma ^{\le k}\) is a state cover for \(\mathcal {\mathcal {M}}\). Then, since \(T^{k}_{P,W} = (P \cdot \varSigma ^{\le k}) \cdot \varSigma ^{\le 1} \cdot W\), \(\mathcal {\mathcal {S}} \sim \mathcal {\mathcal {M}}\) follows by Lemma 2.6. \(\square \)
Fig. 1.
A DFA \(\mathcal {\mathcal {S}}\) for a coffee machine
Let us illustrate the W-method on a toy example. (This example is based on a Mealy machine in [34].) Suppose we have a coffee machine that can dispense coffee or espresso. Coffee costs 1 coin and espresso costs 2 coins. Suppose that the machine breaks whenever we try to order something without enough money, or when we insert more than 2 coins. Then the DFA \(\mathcal {\mathcal {S}}\) over the alphabet \(\varSigma = \{c, e, 1\}\) depicted in Figure 1 accepts precisely those interaction sequences that do not break the coffee machine.
By taking the shortest access sequences for all the states, we see that a state cover for \(\mathcal {\mathcal {S}}\) is given by \(P = \{\varepsilon , c, 1, 11\}\). The input sequence c distinguishes \(q_0\) and \(q_1\), as well as \(q_2\) and \(q_3\), and the input sequence 1 distinguishes \(q_0\) and \(q_2\), as well as \(q_1\) and \(q_2\), \(q_0\) and \(q_3\), and \(q_1\) and \(q_3\). Hence, a characterization set for this DFA is \(W = \{\varepsilon , c, 1\}\). Thus, setting \(k = 0\), the W-method gives the test suite \(T^{0}_{P,W} = P \cdot \varSigma {\le 1} \cdot W\).
By Corollary 2.7, \(T^{0}_{P,W}\) is 4-complete for \(\mathcal {\mathcal {S}}\). For instance, consider the implementation \(\mathcal {\mathcal {M}}_1\) that is the same as \(\mathcal {\mathcal {S}}\) except that the c-transition of \(q_2\) goes to \(q_2\). Then the test case 11c1 (and only this) detects this fault. Similarly, the faulty implementation \(\mathcal {\mathcal {M}}_2\) that is the same as \(\mathcal {\mathcal {S}}\) except that the e-transition of \(q_2\) goes to \(q_1\) is rejected by the test case 11ec (and only this).
Generalizing the W-method. We wish to generalize the W-method to a categorical setting. The first hurdle towards achieving this goal is giving definitions of a state cover and of a characterization set. This is challenging because the nature of the two sets is fundamentally different: the state cover concerns reachability of states, whereas the characterization set is about equivalence of states. These two notions are dual to each other [6]: the former is described using free algebras, while the latter by cofree algebras.
We observe that the setting of automata in monoidal closed categories (called machines by Goguen [24] and sequential\(\varSigma \)-automata by Adámek and Trnková [3] in the Cartesian monoidal case) provides an adequate framework for our goals. This setting defines an abstract notion of automaton which can be viewed both as an algebra and as a coalgebra for suitable endofunctors, giving a straightforward way to define reachability and equivalence of states. It covers many kinds of automata, including DFAs, Moore machines, Mealy machines, linear weighted automata, and deterministic nominal automata.
This setting is particularly nice since it allows us to work with concrete descriptions of the initial algebra and of the final coalgebra for the functors describing the algebraic and coalgebraic presentations of automata, respectively. Additionally, these descriptions are direct generalizations of the corresponding and well-known [30, 47] concepts in the case of DFAs: the initial algebra arises as the object of words, and the final coalgebra as the object of languages. Crucially, this provides a link between these two objects, making it more or less straightforward to define generalizations of a state cover and of a characterization set.
In this categorical setting, we provide a generalization of Lemma 2.6. We do not generalize Lemma 2.5, as it relies on notions of size that are better handled on a case-by-case basis. As applications, we will be able to derive complete test suites for all the abovementioned classes of of automata.
3 Words, Languages, and Automata
In this section, we define the ingredients necessary to carry out our generalized test suite construction. In particular, we define words, languages, and automata in monoidal closed categories, and operations on these objects. We recall that words form an initial algebra [24] and that languages form a final coalgebra [49] of certain endofunctors. We show how to give definitions in such a way that the resulting algebraic and coalgebraic language semantics for automata coincide.
For the remainder of this paper, we fix a monoidal closed category \(\mathcal {C}\) with tensor product \(- \otimes -\), tensor unit \(I\), associator \(\alpha \), left unitor \(\lambda * \), and right unitor \(\varrho \). The internal hom of \(\mathcal {C}\) is denoted by \([-, -]\). We denote by \(\tau _{X}({-})\) the natural bijection
arising from the adjunction \(- \otimes X \dashv [{X},{-}]\). We denote the counit of same adjunction by \(\varepsilon _{X,Y} :[{X},{Y}] \otimes X \rightarrow Y\). Furthermore, we fix two objects \(\varSigma , O\in \mathcal {C}\). We think of \(\varSigma \) as the alphabet object and of \(O\) as the output object. The alphabet object generalizes the set of input symbols for DFAs. In the case of DFAs, the output of a state is simply a Boolean value stating whether the state is accepting or not. The output object generalizes this concept, so that the output of a state can be an arbitrary value. We assume that \(\mathcal {C}\) has binary products and countable coproducts. Finally, we assume that for any \(X \in \mathcal {C}\), the functor \(X \otimes -\) preserves countable coproducts. This assumption is satisfied, for instance, if the functor \(X \otimes -\) also has a right adjoint, as is the case in any braided monoidal closed category.
We note that, intuitively, the internal hom \([-, -]\) internalizes the homsets of the category \(\mathcal {C}\) as objects of \(\mathcal {C}\), in the sense that for any pair of objects X and Y, there is a natural bijection \(\mathcal {C}({X},{Y}) \cong \mathcal {C}({I},{[{X},{Y}]})\).
3.1 Words
We begin by defining words and operations on words.
Definition 3.1
(i)
For an object \(X \in \mathcal {C}\), define its n-fold tensor product by recursion on n: \(X^0 = I\) and \(X^{n+1} = X^n \otimes X\).
(ii)
For a natural number \(k \in \mathbb {N}\), let \(X^{\le k} = \sum _{n \le k}{X^n}\).
(iii)
Finally, let \(X^* = \sum _{n \in N}{X^n}\), and define \(j_{k} :X^{\le k} \rightarrow X^*\) as \([\kappa _{n}]_{n \le k}\).
We think of \(\varSigma ^{*}\) as the object of words over \(\varSigma \).
At this point, we note that both functors \(- \otimes X\) and \(X \otimes -\) preserve countable coproducts (the former by having a right adjoint \([X, -]\), and the latter by assumption). In particular, for any object X, we have isomorphisms
Combining these yields the isomorphism
We define two operations on words, cons and snoc. Intuitively, cons prepends a letter to the beginning of a word, and \(\text {snoc}\) appends a letter to the end.
Definition 3.2
(i)
We define a family of morphisms \(\text {cons}_n :\varSigma \otimes \sigma ^{n} \rightarrow \varSigma ^{n+1}\) by recursion on n: \([0] = \lambda ^{-1}_\varSigma \circ \varrho {\varSigma }\) and \(\text {cons}_{n+1} = (\text {cons}_{n} \otimes 1_{\varSigma }) \circ {\alpha _{\varSigma , \varSigma ^{n}, \varSigma }^{-1}}\).
(ii)
Let \(\text {cons} :\varSigma \otimes \varSigma ^{*} \rightarrow \varSigma ^{*}\) be defined as the composite
(iii)
The map \(\text {snoc}:\varSigma ^{*} \otimes \varSigma \rightarrow \varSigma ^{*}\) is defined as the composition of the isomorphism
and \([\kappa _{n+1}]_{n \in \mathbb {N}} :\sum _{n \in \mathbb {N}}{\varSigma ^{n+1}} \rightarrow \varSigma ^{*}\).
We can also define concatenation of words.
Definition 3.3
(i)
We define a family of maps \(\mu _{m,n} :\varSigma ^{m} \otimes \varSigma ^{n} \rightarrow \varSigma ^{m+n}\) by recursion on n: \(\mu _{m,0} = \varrho _{\varSigma }{m}\) and \(\mu _{m,n+1} = ( \mu _{m,n} \otimes 1_{\varSigma }) \circ {\alpha _{\varSigma ^{m}, \varSigma ^{n}, \varSigma }^{-1}}\).
(ii)
We define the map \(\mu :\varSigma ^{*} \otimes \varSigma ^{*} \rightarrow \varSigma ^{*}\) as the composite
In the next section, we will use the following concatenation operation on morphisms into \(\varSigma ^{*}\), which generalizes concatenation of languages.
Definition 3.4
Let \(a :X \rightarrow \varSigma ^{*}\), \(b :Y \rightarrow \varSigma ^{*}\) be two morphisms. The concatenation of a and b, denoted by \(a \cdot b\), is defined as the composite
By convention, \(\cdot \) associates to the left.
We can characterize \(\varSigma ^{*}\) as the initial algebra of a certain endofunctor on \(\mathcal {C}\). From now on, we fix the functor \(F:\mathcal {C} \rightarrow \mathcal {C}\) given on objects by \(FX = I+ X \otimes \varSigma \).
Proposition 3.5
Let \(\alpha = {[}\kappa _{0}, \text {snoc}{]} :I+ \varSigma ^{*} \otimes \varSigma \rightarrow \varSigma ^{*}\). Then the algebra \((\varSigma ^{*}, \alpha )\) is an initial \(F\)-algebra.
For an \(F\)-algebra \((A, \alpha _{A})\), we denote the unique \(F\)-algebra homomorphism from \((\varSigma ^{*}, \alpha )\) to \((A, \alpha _{A})\) by \(r_{\alpha _{A}} :\varSigma ^{*}\rightarrow A\).
3.2 Languages
We now turn to languages. In the set-theoretical case, languages can be defined as functions \(\varSigma ^{*}\rightarrow 2\). Replacing the output set \(2\) by an arbitrary object yields the following definition.
Definition 3.6
A language is a morphism \(\varSigma ^{*}\rightarrow O\).
Internalizing the above notion, we may think of \([\varSigma ^{*}, O]\) as the object of languages.
We define two operations on languages. The first one computes the output for the empty word. The second one corresponds to the derivative of languages [16].
Definition 3.7
(i)
Define the morphism \(\textrm{ev}_0:[\varSigma ^{*}, O]\rightarrow O\) as the composite \(\textrm{ev}_0= \varepsilon _{\varSigma ^{*},O} \circ (1_{[\varSigma ^{*}, O]} \otimes \kappa _{0}) \circ {\varrho ^{-1}_{[\varSigma ^{*}, O]}}\).
(ii)
Define the morphism \(d:[\varSigma ^{*}, O]\rightarrow [\varSigma , [\varSigma ^{*}, O]]\) as \(\tau _{\varSigma }({\tau _{\varSigma ^{*}}{(d')}})\), where \(d'\) is the composite \(d' = \varepsilon _{\varSigma ^{*},O} \circ (1_{[\varSigma ^{*}, O]} \otimes \text {cons}) \circ \alpha _{[\varSigma ^{*}, O], \varSigma , \varSigma ^{*}}^{-1}\).
We can characterize \([\varSigma ^{*}, O]\) as the final coalgebra for a certain endofunctor. From now on, we fix the functor \(G:\mathcal {C} \rightarrow \mathcal {C}\) given on objects by \(GX = O\times [\varSigma , X]\).
Proposition 3.8
Let \(\gamma = \langle \textrm{ev}_0, d \rangle :[\varSigma ^{*}, O]\rightarrow O\times [\varSigma , [\varSigma ^{*}, O]]\). Then the coalgebra \(([\varSigma ^{*}, O], \gamma )\) is a final \(G\)-coalgebra.
For a \(G\)-coalgebra \((C, \gamma _{C})\), we denote the unique \(G\)-coalgebra homomorphism from \((C, \gamma _{C})\) to \(([\varSigma ^{*}, O], \gamma )\) by \(l_{\gamma _{C}} :C \rightarrow [\varSigma ^{*}, O]\).
3.3 Automata
We conclude this section with a discussion of automata in monoidal closed categories. These are very similar to classical DFAs. The difference is that we replace Cartesian product with tensor product, and we generalize the initial state to an initial state morphism and the set of final states to an output morphism.
Definition 3.9
An automaton over \(\varSigma \) in \(\mathcal {C}\) is a tuple \((Q, i_{Q}, \delta _{Q}, f_{Q})\), where \(Q \in \mathcal {C}\) and \(i_{Q} :I\rightarrow Q\), \(\delta _{Q} :Q \otimes \varSigma \rightarrow Q\), \(f_{Q} :Q \rightarrow O\) are morphisms in \(\mathcal {C}\).
We think of Q as an object of states, of \(i_{Q}\) as selecting an initial state, of \(\delta _{Q}\) as a transition morphism, and of \(f_{Q}\) as an output morphism.
We can view any automaton \(\mathcal {A} = (Q, i_{Q}, \delta _{Q}, f_{Q})\) as an \(F\)-algebra \((Q, {[}i_{Q}, \delta _{Q}{]})\) equipped with an output morphism \(f_{Q}\). Hence, by the initiality of \((\varSigma ^{*}, \alpha )\), we get the unique \(F\)-algebra homomorphism \(r_{{[}i_{Q}, \delta _{Q}{]}} :\varSigma ^{*}\rightarrow Q\). We denote this morphism by \(r_{\mathcal {A}}\). Intuitively, the morphism \(r_{\mathcal {A}}\) maps a word w to the state of \(\mathcal {A}\) reached from the initial state upon reading the input w.
Definition 3.10
(i)
Given an automaton \(\mathcal {A} = (Q, i_{Q}, \delta _{Q}, f_{Q})\), the recognized language of \(\mathcal {A}\) is defined as
.
(ii)
We say that two automata \(\mathcal {A}\) and \(\mathcal {B}\) are equivalent, denoted by \(\mathcal {A} \sim \mathcal {B}\), if they recognize the same language, i.e. \(L_\mathcal {A} = L_\mathcal {B}\).
The recognized language of an automaton generalizes the usual concept of accepted language of DFAs: the language assigns to a given word the output of the state reached from the initial state upon reading that word.
We can also view any automaton \(\mathcal {A} = (Q, i_{Q}, \delta _{Q}, f_{Q})\) as a \(G\)-coalgebra \((Q, \langle f_{Q}, \tau _{\varSigma }{(\delta _{Q})} \rangle )\) equipped with an initial state \(i_{Q}\). By the finality of \(([\varSigma ^{*}, O], \gamma )\), we get the unique \(G\)-coalgebra homomorphism \(l_{\langle f_{Q}, \tau _{\varSigma }{(\delta _{Q})} \rangle } :Q \rightarrow [\varSigma ^{*}, O]\). We denote this morphism by \(l_{\mathcal {A}}\). Intuitively, the morphism \(l_{\mathcal {A}}\) maps a state of \(\mathcal {A}\) to the language accepted from that state.
Note that the definition of recognized language relies on the initial algebra morphism \(r_{\mathcal {A}}\). Alternatively, it can be defined coalgebraically as the morphism
The following proposition asserts that these two presentations are equivalent.
Proposition 3.11
The bijection \(\mathcal {C}({\varSigma ^{*}},{O}) \cong \mathcal {C}({I},{{\varSigma ^{*}},{O}})\) sends \(L_\mathcal {A}\) to \(L_\mathcal {A}'\).
Note that, by definition, a DFA \(\mathcal {A}\) is minimal if and only if the function \(q \mapsto L_{\mathcal {A}}{(q)}\) is injective. As a direct generalization, we define an automaton \(\mathcal {A}\) to be minimal if \(l_{\mathcal {A}}\) is a monomorphism. (Goguen [24] calls such an automaton reduced, while Arbib and Manes [6] call such an automaton observable.)
4 Test Suites and the Generalized W-method
We now generalize the test suite construction to our categorical setting. We continue to use the symbol \(\mathcal {\mathcal {S}}\) for the specification and \(\mathcal {\mathcal {M}}\) for the implementation.
Since in the case of DFAs, test suites, state covers, and characterization sets are sets of words, it would make sense to define the generalizations of these as subobjects of \(\varSigma ^{*}\). However, it turns out that the theory becomes simpler if we consider arbitrary morphisms instead of monos. In particular, this allows us to bypass the need for factorization systems (cf. Remark 4.14).
We define a test suite to be a morphism \(t :T \rightarrow \varSigma ^{*}\). We say that two automata \(\mathcal {\mathcal {S}}\) and \(\mathcal {\mathcal {M}}\)agree ont, denoted by \(\mathcal {\mathcal {S}} \sim _{t} \mathcal {\mathcal {M}}\), if \(L_\mathcal {\mathcal {S}} \circ t = L_\mathcal {\mathcal {M}} \circ t\). Note that we removed the condition of finiteness from our generalized test suite definition. Similarly, we will drop the assumption of finiteness in the definitions of the generalizations of state cover and characterization set. We choose to do this in order to make the theory simpler. In practice, all these components will still be finitary in some sense: for instance, a finite-dimensional vector space or an orbit-finite nominal set.
Definition 4.1
(i)
A fault domain is a collection of automata (in \(\mathcal {C}\)).
(ii)
A test suite \(t :T \rightarrow \varSigma ^{*}\) is complete for an automaton \(\mathcal {\mathcal {S}}\) with respect to a fault domain \(\mathcal {U}\) if for all automata \(\mathcal {\mathcal {M}} \in \mathcal {U}\), \(\mathcal {\mathcal {S}} \sim _{t} \mathcal {\mathcal {M}}\) implies \(\mathcal {\mathcal {S}} \sim \mathcal {\mathcal {M}}\).
We now define the generalization of state covers. Before we do so, we introduce an auxiliary notion.
Definition 4.2
We say that a morphism \(a :A \rightarrow \varSigma ^{*}\)contains the empty word if the morphism \(\kappa _{0} :I\rightarrow \varSigma ^{*}\) factors through a, i.e. there exists a morphism \(i_A :I\rightarrow A\) such that \(\kappa _{0} = a i_A\).
Definition 4.3
Let \(\mathcal {\mathcal {S}} = (\mathcal {S}, i_{\mathcal {S}}, \delta _{\mathcal {S}}, f_{\mathcal {S}})\) be an automaton. A state cover for \(\mathcal {\mathcal {S}}\) is a morphism \(p :P \rightarrow \varSigma ^{*}\) containing the empty word such that the composite
is a split epi.
Intuitively, a state cover for \(\mathcal {\mathcal {S}}\) is a collection of words such that we can effectively assign an access sequence to each state in \(\mathcal {\mathcal {S}}\).
Unfortunately, being a state cover is a relatively strong condition which cannot be satisfied in some of our examples of interest, such as ordered automata (cf. Remark 4.5). It turns out that in order to prove the generalization of Lemma 2.6, a weaker albeit more complicated condition suffices.
Definition 4.4
Let \(\mathcal {\mathcal {S}} = (\mathcal {S}, i_{\mathcal {S}}, \delta _{\mathcal {S}}, f_{\mathcal {S}})\) be an automaton. A weak state cover for \(\mathcal {\mathcal {S}}\) is a morphism \(p :P \rightarrow \varSigma ^{*}\) containing the empty word together with a map \(\delta _P :P \otimes \varSigma \rightarrow P\) such that the following diagram commutes.
Intuitively, a weak state cover assigns to each word w in P and symbol a in \(\varSigma \) a word \(v = \delta _P(w, a)\) in P such that we reach the same state upon reading wa and v. Thus, it provides a transition structure on a restricted collection of words \(p :P \rightarrow \varSigma ^{*}\) that follows the transitions of the automaton \(\mathcal {\mathcal {S}}\).
Remark 4.5
For motivation of why we need the weaker definition of state covers, consider the example of ordered automata [32]. These are automata in the category \(\textbf{Pos}\) of posets and monotone maps equipped with the Cartesian monoidal structure. In this example, we choose the alphabet \(\varSigma \) to be a discrete finite poset. Hence, the object of words \(\varSigma ^{*}\) is also a discrete poset. This implies that, apart from degenerate cases, a state cover \(p :P \rightarrow \varSigma ^{*}\) cannot exist. For, suppose we have an ordered automaton \(\mathcal {\mathcal {S}}\) with state space S and a morphism \(p :P \rightarrow \varSigma ^{*}\). For p to be a state cover, we need to find a right inverse \(s :S \rightarrow P\) of \(r_{\mathcal {\mathcal {S}}} \circ p\). Such a morphism must map related elements of S to related elements of P. But if two elements of P are related, then they are necessarily sent by p to the same word due to the discrete order on \(\varSigma ^{*}\). Hence, the composite \(r_{\mathcal {\mathcal {S}}} \circ p \circ s\) sends every connected subset of S (viewed as an undirected graph) to the same state. Thus, s is a right inverse only if each connected component of S has size 1, i.e. if S is a discrete poset.
Proposition 4.6
Let \(\mathcal {\mathcal {S}}\) be an automaton. Then every state cover for \(\mathcal {\mathcal {S}}\) is a weak state cover for \(\mathcal {\mathcal {S}}\).
Proof
Let \(p :P \rightarrow \varSigma ^{*}\) be a state cover for \(\mathcal {\mathcal {S}} = (\mathcal {S}, i_{\mathcal {S}}, \delta _{\mathcal {S}}, f_{\mathcal {S}})\). Then p contains the empty word. Since \(r_{\mathcal {\mathcal {S}}} \circ p\) is a split epi, it has a right inverse \(s :\mathcal {S}\rightarrow P\). Defining \(\delta _P\) as \(s \circ r_{\mathcal {S}} \circ \text {snoc}\circ (p \otimes 1_{\varSigma })\) makes the required diagram commute. \(\square \)
Characterization sets are generalized as follows.
Definition 4.7
Let \(\mathcal {\mathcal {S}} = (\mathcal {S}, i_{\mathcal {S}}, \delta _{\mathcal {S}}, f_{\mathcal {S}})\) be an automaton. A characterization morphism for \(\mathcal {\mathcal {S}}\) is a morphism \(w :W \rightarrow \varSigma ^{*}\) containing the empty word such that for all \(f, g :X \rightarrow \mathcal {S}\), if \([w, 1_{O}] \circ l_{\mathcal {\mathcal {S}}} \circ f = [w, 1_{O}] \circ l_{\mathcal {\mathcal {S}}} \circ g :X \rightarrow [W, O]\), then \(l_{\mathcal {\mathcal {S}}} \circ f = l_{\mathcal {\mathcal {S}}} \circ g :X \rightarrow [\varSigma ^{*}, O]\).
Remark 4.8
For motivation of the definition of characterization morphisms, note that, given an automaton \(\mathcal {\mathcal {S}} = (S, i_{\mathcal {S}}, \delta _{\mathcal {S}}, f_{\mathcal {S}})\), the categorical counterpart of the relation \( \sim { }\) for \(\mathcal {\mathcal {S}}\) from Section 2 is the kernel pair \((e_1, e_2)\) of \(l_{\mathcal {\mathcal {S}}} :S \rightarrow [\varSigma ^{*}, O]\), and that the counterpart of the relation \( \sim {_{W}\,\,} \) for a morphism \(w :W \rightarrow \varSigma ^{*}\) is the kernel pair \((e_1^w, e_2^w)\) of \([w, 1_{O}] \circ l_{\mathcal {\mathcal {S}}} :S \rightarrow [W, O]\). Thus, the condition \(p \sim {_{W}\,\,} q \implies p \sim {{q}}\) can be expressed by saying that \(\langle e_1^w, e_2^w \rangle \) factors through \(\langle e_1, e_2 \rangle \). This is equivalent to the definition given above.
We now state our main theorem, which is a generalization of Lemma 2.6.
Theorem 4.9
Let \(\mathcal {\mathcal {S}}\) and \(\mathcal {\mathcal {M}}\) be two automata. Suppose \((c, \delta _C)\) is a weak state cover for \(\mathcal {\mathcal {M}}\) and w is a characterization morphism for \(\mathcal {\mathcal {S}}\). Assume that \(\mathcal {\mathcal {S}}\) is minimal and let \(t = c \cdot j_{1} \cdot w\). Then \(\mathcal {\mathcal {S}} \sim _{t} \mathcal {\mathcal {M}}\) implies \(\mathcal {\mathcal {S}} \sim \mathcal {\mathcal {M}}\).
To state completeness of the generalized test suite, we introduce an abstract fault domain, which is in a sense the most general fault domain with respect to which the test suite is complete.
Definition 4.10
For a morphism \(c :C \rightarrow \varSigma ^{*}\), define the fault domain \(\mathcal {U}_{c}\) as
$$\begin{aligned} \mathcal {U}_{c} = \left\{ \mathcal {\mathcal {M}}\ |\ \exists \delta _C.\ (c, \delta _C) \text { is a weak state cover for}\, \mathcal {\mathcal {M}} \right\} . \end{aligned}$$
Corollary 4.11
Let \(\mathcal {\mathcal {S}}\) be a minimal automaton. Then for all \(c :C \rightarrow \varSigma ^{*}\) and for all characterization morphisms \(w :W \rightarrow \varSigma ^{*}\) for \(\mathcal {\mathcal {S}}\), the test suite \(t = c \cdot j_{1} \cdot w\) is complete for \(\mathcal {\mathcal {S}}\) with respect to \(\mathcal {U}_{c}\).
Proof
Let \(\mathcal {\mathcal {M}} \in \mathcal {U}_{c}\), and assume \(\mathcal {\mathcal {S}} \sim _{t} \mathcal {\mathcal {M}}\). Then there exists a \(\delta _C\) such that \((c, \delta _C)\) is a weak state cover for \(\mathcal {\mathcal {M}}\). Thus, \(\mathcal {\mathcal {S}} \sim \mathcal {\mathcal {M}}\) follows by Theorem 4.9. \(\square \)
We now turn to the generalized W-method.
Definition 4.12
Let \(p :P \rightarrow \varSigma ^{*}\) and \(w :W \rightarrow \varSigma ^{*}\) be two morphisms, and let \(k \in \mathbb {N}\). Then the W test suite of order k associated to p and w is defined as the morphism \(t^{k}_{p, w} = p \cdot j_{k+1} \cdot w\).
We state completeness of the generalized W-method with respect to a fault domain which is a special case of the one given in Definition 4.10, namely, \(\mathcal {U}^{k}_{p} = \mathcal {U}_{p \cdot j_{k}}\). Completeness with respect to this fault domain in the case of Mealy machines has already been considered by Maarse [36]. The related notion of k-A-completeness for Mealy machines has been introduced by Vaandrager, Fiterǎu-Broştean, and Melse [51].
Corollary 4.13
Let \(\mathcal {\mathcal {S}}\) be a minimal automaton. Then for all \(p :P \rightarrow \varSigma ^{*}\), for all characterization morphisms \(w :W \rightarrow \varSigma ^{*}\) for \(\mathcal {\mathcal {S}}\), and for all \(k \in \mathbb {N}\), the test suite \(t^{k}_{p, w}\) is complete for \(\mathcal {\mathcal {S}}\) with respect to \(\mathcal {U}^{k}_{p}\).
Remark 4.14
In order to simplify the theory, we have opted for defining test suites (as well as state covers and characterization morphisms) as arbitrary morphisms instead of subobjects. However, we note that our theory would also work out if we defined test suites to be \(\mathcal {M}\)-morphisms for some factorization system \((\mathcal {E}, \mathcal {M})\) such that all morphisms in \(\mathcal {E}\) are epimorphisms. To obtain the adjusted test suite, we simply need to take the \((\mathcal {E}, \mathcal {M})\)-factorization of the original test suite. Whether we restrict test suites to \(\mathcal {M}\)-morphisms or not does not influence the completeness of test suites due to the following proposition.
Proposition 4.15
Let \((\mathcal {E}, \mathcal {M})\) be a factorization system on \(\mathcal {C}\) such that all morphisms in \(\mathcal {E}\) are epimorphisms. Let \(t :T \rightarrow \varSigma ^{*}\) be a test suite and let
be its \((\mathcal {E}, \mathcal {M})\)-factorization. Then for all automata \(\mathcal {\mathcal {S}}\) and \(\mathcal {\mathcal {M}}\), \(\mathcal {\mathcal {S}} \sim _{t} \mathcal {\mathcal {M}}\) if and only if \(\mathcal {\mathcal {S}} \sim _{t'} \mathcal {\mathcal {M}}\).
Proof
Follows immediately from the definition of \(\mathcal {\mathcal {S}} \sim _{t} \mathcal {\mathcal {M}}\) and the fact that \(e \in \mathcal {E}\) is an epimorphism. \(\square \)
Corollary 4.16
Let t and \(t'\) be defined as in the previous proposition. Then for all automata \(\mathcal {\mathcal {S}}\) and for all fault domains \(\mathcal {U}\), t is complete for \(\mathcal {\mathcal {S}}\) with respect to \(\mathcal {U}\) if and only if \(t'\) is complete for \(\mathcal {\mathcal {S}}\) with respect to \(\mathcal {U}\).
In view of Corollary 4.16, we may replace the original test suite t with the factorized test suite \(t'\) when dealing with completeness. We will use this fact when considering instances of the general framework in the next section.
5 Applications
In this section, we use our general framework to derive complete test suites for various kinds of automata, including weighted automata and deterministic nominal automata. Details for the examples can be found in appendix [33].
5.1 DFAs, Moore Machines, and Mealy Machines
DFAs are covered by our framework: the categorical definitions of Section 3 and Section 4 specialize to the familiar ones in Section 2 if we take as \(\mathcal {C}\) the category \(\textbf{Set}\) of sets and functions with the cartesian product as monoidal structure and if we set \(O= 2\). A difference is that, as mentioned in Section 4, the specialized notions of test suite, state cover, and characterization morphism are functions into \(\varSigma ^{*}\) rather than mere subsets. We recover the original definitions by taking the images of the functions (cf. Remark 4.14). We also recover the W-method and Lemma 2.6.
Moore machines are essentially the same as DFAs, except that the set of final states \(F \subseteq Q\) is generalized to an output function \(f :Q \rightarrow O\) for some output set \(O\). In the abstract framework, this amounts to changing the output object from \(2\) to \(O\). Also in this case, we recover the W-method and an analogue of Lemma 2.6. As an example, take the Moore machine \(\mathcal {\mathcal {S}}\) with states and transitions identical to those of the DFA in Figure 1, and with the output function \(f :Q \rightarrow \mathbb {N}\cup \{-1\}\) that assigns to each state the amount of coins stored in the coffee machine in that state: \(f(q_0) = 0\), \(f(q_1) = 1\), \(f(q_2) = 2\), and \(f(q_3) = -1\), where \(-1\) is used as a value indicating an error. Then \(P = \{\varepsilon , c, 1, 11\}\) is still a state cover for \(\mathcal {\mathcal {S}}\), \(W = \{\varepsilon , c, 1\}\) is still a characterization set for \(\mathcal {\mathcal {S}}\), and the test suite \(T^{0}_{P,W}\) is still 4-complete for \(\mathcal {\mathcal {S}}\). A difference in this example is that the input sequence 1 also distinguishes \(q_0\) and \(q_1\). Hence, we could also use the alternative and smaller characterization set \(W' = \{\varepsilon , 1\}\). This results in the smaller 4-complete test suite \(T^{0}_{P,W'} = P \cdot \varSigma ^{\le 1} \cdot W'\).
Mealy machines are similar to Moore machines, but they assign an output to each transition instead of each state. Formally, this amounts to replacing the output morphism \(f :Q \rightarrow O\) by \(\lambda :Q \times \varSigma \rightarrow O\). Mealy machines are covered by our framework by considering the category \(\textbf{Set}\) of sets and functions with the cartesian monoidal structure and by taking the output object to be the set \(O^{\varSigma }\). In particular, we recover [34, Lemma 3.8].
We mention a subtle difference between our presentation of the W-method and the usual one found in the literature. Traditionally, the output function of a Mealy machine is extended to words as a function \(\lambda ^* :Q \times \varSigma ^{*}\rightarrow O^*\) that records all the outputs encountered during a run of the machine. In contrast, the function \(L_\mathcal {A} :\varSigma ^{*}\rightarrow O^{\varSigma }\) for a Mealy machine \(\mathcal {A}\) maps a word w and an input symbol a to the output of the last transition during the run of the input word wa. Hence, the assumption \(\mathcal {\mathcal {S}} \sim _{T} \mathcal {\mathcal {M}}\) only guarantees that the last transitions of \(\mathcal {\mathcal {S}}\) and \(\mathcal {\mathcal {M}}\) match on input words from T. We can recover the stronger guarantee that \(\lambda ^*(q_0, w) = \lambda ^*(q_0', w)\) for all \(w \in T\) by making sure that the test suite is prefix-closed (i.e. any prefix of any word in T is also in T).
5.2 Weighted Automata
Weighted automata [22] are generalizations of DFAs where a weight is assigned to each transition, expressing e.g. the cost or reliability of its execution. In this subsection, we fix a field \(\mathbb {K}\) and a finite set \(\varSigma \) of input symbols.
Definition 5.1
A weighted automaton (WA) is a tuple \((Q, s_0, \delta , f)\), where Q is a finite set of states, \(s_0 :Q \rightarrow \mathbb {K}\) is an input weight function, \(\delta :Q \times \varSigma \times Q \rightarrow \mathbb {K}\) is a transition weight function, and \(f :Q \rightarrow \mathbb {K}\) is an output weight function.
The transition function \(\delta \) of a WA \((Q, s_0, \delta , f)\) can be conveniently represented as a \(\varSigma \)-indexed family of \(\mathbb {K}\)-valued matrices \(M^{\delta }_{a} \in \mathbb {K}^{Q \times Q}\ (a \in \varSigma )\) defined as \(M^{\delta }_{a}(p, q) = \delta (q, a, p)\). Note that the column index specifies the source state and the row index the target state. Similarly, the input and output weight functions \(s_0\) and f can be thought of as \(\mathbb {K}\)-valued column vectors of cardinality Q.
WAs are covered by our framework: letting \(\varSigma '\) be the free vector space over \(\varSigma \), WAs correspond to automata over \(\varSigma '\) in the category \(\textbf{Vect}_{\mathbb {K}}\) of vector spaces over \(\mathbb {K}\) and linear maps equipped with the tensor product of vector spaces as monoidal structure, taking the output object \(O= \mathbb {K}\). The corresponding automaton in \(\textbf{Vect}_{\mathbb {K}}\) has state space \(\mathbb {K}^{Q}\). The correspondence is spelled out in appendix [33]. In the remainder of the section, we identify WAs and automata in \(\textbf{Vect}_{\mathbb {K}}\) via this correspondence.
We recall that WAs recognize weighted languages, i.e. functions \(\varSigma ^{*}\rightarrow \mathbb {K}\). For a WA \(\mathcal {A} = (Q, s_0, \delta , f)\) and a word \(w \in \varSigma ^{*}\), define the matrix \(M^{\delta }_{w}\) by recursion on w: \(M^{\delta }_{\varepsilon } = I\) (where \(I\) denotes the unit matrix) and \(M^{\delta }_{wa} = M^{\delta }_{a} M^{\delta }_{w}\). The recognized language\(L_\mathcal {A}(s)\) of an input weight vector \(s \in \mathbb {K}^{Q}\) is then defined as \(L_\mathcal {A}(s)(w) = f^t M^{\delta }_{w} s\), where \(f^t\) denotes the transpose of f. The recognized language of \(\mathcal {A}\) is \(L_\mathcal {A} = L_\mathcal {A}(s_0)\). We note furthermore that the function \(s \mapsto L_\mathcal {A}(s)\) is a linear map \(\mathbb {K}^{Q} \rightarrow \mathbb {K}^{\varSigma ^{*}}\), which follows directly from the definition of \(L_\mathcal {A}(s)\).
Fig. 2.
A WA \(\mathcal {\mathcal {S}}\) for computing the decimal value of a binary number
As an example, consider the WA \(\mathcal {\mathcal {S}}\) over the alphabet \(\{a,b\}\) and field \(\mathbb {R}\) depicted in Figure 2. (This example is taken from [22].) The input, output, and transition weights not shown are equal to 0. This automaton recognizes the weighted language \(L :\varSigma ^{*}\rightarrow \mathbb {R}\) that maps a word w to the decimal value of w if understood as a binary number with a standing for the digit 0 and b for the digit 1.
Let us instantiate the abstract framework to the case of WAs. We start by noting that if the vector spaces V and W have generating sets B and C, respectively, then \(V \otimes W\) is generated by \(\left\{ a \otimes b\ |\ a \in A, b \in B \right\} \cong B \times C\). Furthermore, if \(V_i\) is a vector space with generating set \(B_i\) for all \(i \in I\), then the direct sum \(\bigoplus _{i \in I}{V_i}\) is generated by \(\bigcup _{i \in I}{\left\{ \kappa _{i}(b)\ |\ b \in B_i \right\} } \cong \coprod _{i \in I}{B_i}\) (where \(\coprod \) denotes the disjoint union of sets). Hence, the vector space \((\varSigma ')^n\) (where \(\varSigma '\) is the free vector space over \(\varSigma \)) is generated by the set \(\varSigma {n}\), \((\varSigma ')^{\le k}\) by \(\varSigma ^{\le k}\), and \((\varSigma ')^*\) by \(\varSigma ^{*}\). Furthermore, the map \(j_{k} :(\varSigma ')^{\le k} \rightarrow (\varSigma ')^*\) is the inclusion of the subspace \((\varSigma ')^{\le k}\). Since a linear map \((\varSigma ')^* \rightarrow \mathbb {K}\) is completely determined by its values on the basis vectors, the categorical notion of language is in bijective correspondence with weighted languages. The following proposition states how various notions from Section 3 specialize to the case of WAs.
Proposition 5.2
Let \(\mathcal {A} = (Q, s_0, \delta , f)\) be a WA.
(i)
The morphism \(\mu :(\varSigma ')^* \otimes (\varSigma ')^* \rightarrow (\varSigma ')^*\) corresponds to the bilinear map \((\varSigma ')^* \times (\varSigma ')^* \rightarrow (\varSigma ')^*\) defined on basis elements by \((u, v) \mapsto u v\).
(ii)
The morphism \(r_{\mathcal {A}} :(\varSigma ')^* \rightarrow \mathbb {K}^{Q}\) is the linear extension of the map \(\varSigma ^{*}\rightarrow \mathbb {K}^{Q}\) sending w to \(M^{\delta }_{w} s_0\).
(iii)
The recognized language of \(\mathcal {A}\) in the categorical sense is the linear extension of the recognized language of \(\mathcal {A}\).
(iv)
The morphism \(l_{\mathcal {A}} :\mathbb {K}^{Q} \rightarrow \textbf{Vect}_{\mathbb {K}}({(\varSigma ')^*},{\mathbb {K}})\) sends an input weight vector \(s \in \mathbb {K}^{Q}\) to the linear extension of the weighted language \(L_\mathcal {A}(s)\).
(v)
The automaton \(\mathcal {A}\) is minimal iff for all \(s \in \mathbb {K}^{Q}\), \(L_\mathcal {A}(s) = 0\) implies \(s = 0\).
We now turn to the discussion of test suites. For the remainder of this section, we fix a specification WA \(\mathcal {\mathcal {S}} = (Q, s_0, \delta , f)\). Test suites, state covers, and characterization morphisms specialize to linear maps with codomain \((\varSigma ')^*\). We focus on the case where these morphisms are actually subspace inclusions. Hence, we say that a subspace is a test suite, and we may refer to a certain subspace as a state cover or as a characterization space, the meaning being that the corresponding subspace inclusion is a state cover or a characterization morphism. We concentrate on those subspaces that are generated by subsets of \(\varSigma ^{*}\).
Proposition 5.3
Let \(\mathcal {\mathcal {M}}\) be a WA, let \(T \subseteq \varSigma ^{*}\), and let \(t :\text {span}{(T)} \rightarrow (\varSigma ')^*\) be the subspace inclusion. Then \(\mathcal {\mathcal {S}} \sim _{t} \mathcal {\mathcal {M}}\) if and only if \(L_\mathcal {\mathcal {S}}|_T = L_\mathcal {\mathcal {M}}|_T\).
Thus, we obtain a notion of completeness of test suites for WAs: a test suite \(T \subseteq \varSigma ^{*}\) is complete for \(\mathcal {\mathcal {S}}\) with respect to a fault domain \(\mathcal {U}\) if and only if \(L_\mathcal {\mathcal {S}}|_T = L_\mathcal {\mathcal {M}}|_T\) implies \(L_\mathcal {\mathcal {S}} = L_\mathcal {\mathcal {M}}\) for all \(\mathcal {\mathcal {M}} \in \mathcal {U}\). This notion is completely analogous to that for DFAs.
The following proposition characterizes the key components of the generalized W-method in the case of WAs in terms of subsets of \(\varSigma ^{*}\).
Proposition 5.4
(i)
Let \(P \subseteq \varSigma ^{*}\). Then \(\text {span}{(P)}\) is a state cover for \(\mathcal {\mathcal {S}}\) if and only if \(\varepsilon \in P\) and \(\mathbb {K}^{Q}\) is generated by \(\left\{ M^{\delta }_{w} s_0\ |\ w \in P \right\} \).
(ii)
Let \(W \subseteq \varSigma ^{*}\). Then \(\text {span}{(W)}\) is a characterization space for \(\mathcal {\mathcal {S}}\) if and only if \(\varepsilon \in W\) and for all \(s \in \mathbb {K}^{Q}\), \(L_\mathcal {\mathcal {S}}(s)|_W = 0\) implies \(L_\mathcal {\mathcal {S}}(s) = 0\).
Motivated by the previous proposition, if \(P \subseteq \varSigma ^{*}\) is such that \(\text {span}{(P)}\) is a state cover for \(\mathcal {\mathcal {S}}\), then we also call P itself a state cover. Similarly, if \(\text {span}{(W)}\) is a characterization space, we call W a characterization set. Notice the similarity of the characterizations with the corresponding definitions in Section 2 for DFAs.
We are now ready to derive a specialized W-method for WAs. It turns out that, under the identification of subspaces of \((\varSigma ')^*\) and subsets of \(\varSigma ^{*}\), it coincides with the classical W-method (Definition 2.4). Furthermore, it is characterized as the image of the generalized W test suite from Definition 4.12.
Lemma 5.5
Let \(P, W \subseteq \varSigma ^{*}\), let \(k \in \mathbb {N}\), and let \(p :\text {span}{(P)} \rightarrow (\varSigma ')^*\) and \(w :\text {span}{(W)} \rightarrow (\varSigma ')^*\) denote the inclusions. Then \(\text {span}{(T^{k}_{P,W})} = \text {im}{t^{k}_{p, w}}\).
To state completeness of the specialized W-method, we define an appropriate fault domain, which is a restriction of the fault domain \(\mathcal {U}^{k}_{p}\).
Definition 5.6
For a set \(P \subseteq \varSigma ^{*}\) and natural number k, define
$$\begin{aligned} \mathcal {U}^{k}_{P} = \left\{ \mathcal {\mathcal {M}}\ |\ P \cdot \varSigma ^{\le k} \text { is a state cover for }\,\mathcal {\mathcal {M}} \right\} . \end{aligned}$$
The following theorem asserts completeness of the W-method for WAs.
Theorem 5.7
Suppose \(\mathcal {\mathcal {S}}\) is minimal. Then for all \(P \subseteq \varSigma ^{*}\), for all characterization sets \(W \subseteq \varSigma ^{*}\) for \(\mathcal {\mathcal {S}}\), and for all \(k \in \mathbb {N}\), the test suite \(T^{k}_{P,W}\) (Definition 2.4) is complete for \(\mathcal {\mathcal {S}}\) with respect to \(\mathcal {U}^{k}_{P}\).
Continuing our previous example, we derive a complete test suite for the WA \(\mathcal {\mathcal {S}}\) of Figure 2. We have \(M^{\delta }_{\varepsilon } s_0 = M^{\delta }_{\varepsilon } q_0 = q_0\) and \(M^{\delta }_{b} s_0 - M^{\delta }_{\varepsilon } s_0 = M^{\delta }_{b} q_0 - M^{\delta }_{\varepsilon } q_0 = (q_0 + q_1) - q_0 = q_1\). Since \(\{ q_0, q_1 \}\) is a basis for \(\mathbb {K}^{Q}\), by Proposition 5.4 (i), \(P = \{\varepsilon , b\}\) is a state cover for \(\mathcal {\mathcal {S}}\).
Next, we show that \(W = \{\varepsilon , b\}\) is a characterization set for \(\mathcal {\mathcal {S}}\). For this, we recall that \(L_\mathcal {\mathcal {S}}(q_0) = L_\mathcal {\mathcal {S}}\) maps a word w to the decimal value of w understood as a binary number with a standing for 0 and b for 1. Furthermore, \(L_\mathcal {\mathcal {S}}(q_1)\) maps a word w to \(2^{|w|}\). Thus, if \(s = k_0q_0 + k_1q_1\) such that \(L_\mathcal {\mathcal {S}}(s)|_W = 0\), then \(L_\mathcal {\mathcal {S}}(s)(\varepsilon ) = k_0 L_\mathcal {\mathcal {S}}(q_0)(\varepsilon ) + k_1 L_\mathcal {\mathcal {S}}(q_1)(\varepsilon ) = k_1 = 0\). Moreover, we have \(L_\mathcal {\mathcal {S}}(s)(b) = k_0 L_\mathcal {\mathcal {S}}(q_0)(b) + k_1 L_\mathcal {\mathcal {S}}(q_1)(b) = k_0 + 2k_1 = k_0 = 0\). Thus, \(L_\mathcal {\mathcal {S}}(s)|_W = 0\) implies \(s = 0\). Hence, by Proposition 5.4 (ii), \(W = \{ \varepsilon , b \}\) is a characterization set for \(\mathcal {\mathcal {S}}\).
By Theorem 5.7, we conclude that \(T^{1}_{P,W} = P \cdot \varSigma ^{\le 2} \cdot W\) is a complete test suite for \(\mathcal {\mathcal {S}}\) with respect to \(\mathcal {U}^{1}_{P}\). See appendix [33] for an example of how a possible faulty implementation is rejected.
5.3 Nominal Automata
Nominal automata [11] are a model of computation over potentially infinite alphabets. They are based on the notion of nominal sets, which are essentially sets with certain symmetries. The idea is that we demand that the transition function of a nominal automaton respect the symmetries of the state space, so that we can represent it via finite manners.
In this subsection, we fix a countable set \(\mathbb {A}\) of atoms. We denote by \(\text {Perm}{(\mathbb {A})}\) the group of finite permutations over \(\mathbb {A}\) (i.e. bijections \(\pi :\mathbb {A}\rightarrow \mathbb {A}\) such that \(\pi (a) = a\) for all but finitely many \(a \in \mathbb {A}\)). For a \(\text {Perm}{(\mathbb {A})}\)-set X, we denote the action of \(\pi \) on an element \(x \in X\) by \(\pi \cdot x\). We recall that an equivariant function\(f :X \rightarrow Y\) between \(\text {Perm}{(\mathbb {A})}\)-sets satisfies \(f(\pi \cdot x) = \pi \cdot f(x)\), an equivariant subset\(A \subseteq X\) is such that \(x \in A \implies \pi \cdot x \in A\), and an equivariant element\(a \in X\) is such that \(\{a\}\) is an equivariant subset. For background on nominal sets in general, we refer to [45]. Finally, we fix an orbit-finite nominal set \(\varSigma \) acting as the alphabet.
Definition 5.8
A deterministic nominal automaton (or DNA for short) is a tuple \((Q, q_0, \delta , F)\), where Q is an orbit-finite nominal set of states, \(q_0 \in Q\) is an equivariant initial state, \(\delta :Q \times \varSigma \rightarrow Q\) is an equivariant transition map, and \(F \subseteq Q\) is an equivariant subset of final states.
For DNA \(\mathcal {A} = (Q, q_0, \delta , F)\), we write \(q \in \mathcal {A}\) for \(q \in Q\).
DNAs are covered by our framework, since they correspond precisely to automata over \(\varSigma \) in the category \(\textbf{Nom}\) of nominal sets and equivariant maps with the cartesian product as monoidal structure, taking the output object \(O= 2\), the discrete nominal set with 2 elements. To see this, note that, given a nominal set Q, an equivariant element \(q_0 \in Q\) corresponds to an equivariant map \(1 \rightarrow Q\) (where 1 is the discrete nominal set with 1 element), and that an equivariant subset \(F \subseteq Q\) corresponds to an equivariant map \(Q \rightarrow 2\). We identify DNAs with automata in \(\textbf{Nom}\) via this correspondence.
DNAs recognize nominal languages: these are equivariant subsets of \(\varSigma ^{*}\), the nominal set of words over \(\varSigma \) with the pointwise group action. The transition map \(\delta \) of a nominal automaton \(\mathcal {A} = (Q, q_0, \delta , F)\) can be extended to an equivariant map \(\delta ^* :Q \times \varSigma ^{*}\rightarrow Q\) just as in the case of DFAs. The accepted language\(L_{\mathcal {A}}{(q)}\) of a state \(q \in Q\) is also defined analogously to DFAs as the set \(L_{\mathcal {A}}{(q)} = \left\{ w \in \varSigma ^{*}\ |\ \delta ^*(q, w) \in F \right\} \), and the accepted language \(L_{\mathcal {A}}\) of \(\mathcal {A}\) is \(L_{\mathcal {A}}{(q_{0})}\).
Fig. 3.
An example DNA \(\mathcal {\mathcal {S}}\) accepting the language \(L = \left\{ aa\ |\ a \in \mathbb {A} \right\} \)
As an example, consider the DNA \(\mathcal {\mathcal {S}}\) over the alphabet \(\mathbb {A}\) of atoms (regarded as a nominal set with group action \(\pi \cdot a = \pi (a)\)) depicted in Figure 3. (This example is taken from [40].) The automaton has state space \(Q = \{q_0,q_2,q_3\} \cup \left\{ q_{1,a}\ |\ a \in \mathbb {A} \right\} \); the infinite amount of states \(\left\{ q_{1,a}\ |\ a \in \mathbb {A} \right\} \) is depicted with one symbolic state \(q_{1,a}\). The transitions
and
are to be understood as one transition for each \(a \in \mathbb {A}\). Furthermore, transitions of the form
for \(A \subseteq \mathbb {A}\) stand for a number of transitions, one for each \(a \in A\). The automaton \(\mathcal {\mathcal {S}}\) accepts the nominal language \(L = \left\{ aa\ |\ a \in \mathbb {A} \right\} \).
We now instantiate the abstract framework to DNAs. We first note that the categorical construction of the nominal set \(\varSigma ^{*}\) coincides with the description given above. Thus, languages \(\varSigma ^{*}\rightarrow 2\) in the categorical sense correspond precisely to nominal languages. Furthermore, the map \(j_{k} :\varSigma ^{\le k} \rightarrow \varSigma ^{*}\) is simply the inclusion of a subset. The map \(\mu :\varSigma ^{*}\times \varSigma ^{*}\rightarrow \varSigma ^{*}\) is given by concatenation of words. For any DNA \(\mathcal {A}\), the morphism \(r_{\mathcal {A}}\) maps a word \(w \in \varSigma ^{*}\) to \(\delta ^*(q_0, w)\). Thus, the categorical notion of recognized language corresponds to the accepted language of \(\mathcal {A}\) as defined above. Moreover, the morphism \(l_{\mathcal {A}}\) maps a state \(q \in \mathcal {A}\) to \(L_{\mathcal {A}}{(q)}\). Finally, an automaton \(\mathcal {A}\) is minimal (in the categorical sense) if for all \(p, q \in \mathcal {A}\), \(L_{\mathcal {A}}{(p)} = L_{\mathcal {A}}{(q)}\) implies \(p = q\).
For the remainder of this section, we fix a specification DNA \(\mathcal {\mathcal {S}} = (Q, q_0, \delta , F)\). Similarly to the case of WAs, we focus on the case where test suites, state covers, and characterization morphisms are actually subset inclusions. A subset inclusion is equivariant if and only if the subset is equivariant. Thus, we say that an equivariant subset of \(\varSigma ^{*}\)is a test suite, state cover, or characterization set. If \(T \subseteq \varSigma ^{*}\) is a test suite, and \(t :T \rightarrow \varSigma ^{*}\) is the corresponding inclusion, then \(\mathcal {\mathcal {S}} \sim _{t} \mathcal {\mathcal {M}}\) if and only if \(L_{\mathcal {\mathcal {S}}} \cap T = L_{\mathcal {\mathcal {M}}} \cap T\) for any DNA \(\mathcal {\mathcal {M}}\). Hence, the notion of completeness of test suites for DNAs coincides with that for DFAs. A set \(W \subseteq \varSigma ^{*}\) is a characterization set for \(\mathcal {\mathcal {S}}\) if and only if \(\varepsilon \in W\) and for all \(p, q \in Q\), \(L_{\mathcal {\mathcal {S}}}{(p)} \cap W = L_{\mathcal {\mathcal {S}}}{(q)} \cap W\) implies \(L_{\mathcal {\mathcal {S}}}{(p)} = L_{\mathcal {\mathcal {S}}}{(q)}\). Thus, characterization sets are exactly the same as for DFAs.
The specialized W-method for DNAs coincides with the W-method for DFAs. Furthermore, just as for WAs, it is characterized as the image of the generalized W test suite. Namely, if \(P, W \subseteq \varSigma ^{*}\), \(p :P \rightarrow \varSigma ^{*}\) and \(w :W \rightarrow \varSigma ^{*}\) are the subset inclusions, and \(k \in \mathbb {N}\), then \(T^{k}_{P,W} = \text {im}{t^{k}_{p, w}}\).
The following theorem asserts the completeness of the W-method for DNAs, and it is an immediate consequence of Corollary 4.13 and 4.16.
Theorem 5.9
Suppose \(\mathcal {\mathcal {S}}\) is minimal. Then for all \(P \subseteq \varSigma ^{*}\), for all characterization sets \(W \subseteq \varSigma ^{*}\) for \(\mathcal {\mathcal {S}}\), and for all \(k \in \mathbb {N}\), the test suite \(T^{k}_{P,W}\) is complete for \(\mathcal {\mathcal {S}}\) with respect to \(\mathcal {U}^{k}_{p}\) (where \(p :P \rightarrow \varSigma ^{*}\) is the inclusion).
Continuing the previous example, we derive a complete test suite for the DNA \(\mathcal {\mathcal {S}}\). We first show that \(P = \{\varepsilon \} \cup \left\{ a\ |\ a \in \mathbb {A} \right\} \cup \left\{ aa\ |\ a \in \mathbb {A} \right\} \cup \left\{ aab\ |\ a, b \in \mathbb {A} \right\} \) is a weak state cover for \(\mathcal {\mathcal {S}}\). Define the map \(\delta _P :P \times \varSigma \rightarrow P\) as
It can be checked that \(\delta _P\) is equivariant. Furthermore, we have \(\delta ^*(q_0, \delta _P(w, c)) = \delta ^*(q_0, wc)\), as can readily be verified.
Next, we note that \(W = \{\varepsilon \} \cup \left\{ a\ |\ a \in \mathbb {A} \right\} \cup \left\{ aa\ |\ a \in \mathbb {A} \right\} \) is a characterization set for \(\mathcal {\mathcal {S}}\). Hence, we obtain the complete test suite \(T^{0}_{P,W} = P \cdot \mathbb {A}^{\le 1} \cdot W\). We remark that \(T^{0}_{P,W}\) is an infinite but orbit-finite subset of \(\varSigma ^{*}\).
6 Conclusion and Future Work
We introduced a general framework for studying the W-method and proving completeness of test suites, at the categorical level of automata in monoidal closed categories. Besides recovering basic instances such as DFAs, Mealy machines, and Moore machines, our framework instantiates to complete test suites for the new cases of weighted automata and deterministic nominal automata.
There are several open questions and avenues for future work. We have focused on the classical W-method, but it would be useful to also cover refinements thereof such as Wp [23], where distinguishing sequences depend on the state reached, or Hybrid ADS [40]. The latter requires an understanding of adaptive distinguishing sequences at an abstract level, which is of interest on its own. A further direction is to include in our framework a notion of finiteness of test suites using, e.g., finitely presentable objects [2]. Moreover, a key aspect of the W-method is that the size of the state cover and characterization set are polynomial in the size of the specification, and it would be useful to capture this at a more general level.
A possible direction for future work is to move from weighted automata over a field to weighted automata over a semiring, and complement for instance the learning algorithms for weighted automata over the integers proposed in [17, 25]. Instantiating to the Boolean semiring could then connect to more concrete work on complete test suites for non-deterministic automata [44].
Our results assume a state cover and a characterization set as input. We have not touched upon the topic on how to acquire these sets from the specification. It would be of practical relevance to develop algorithms for computing state covers and characterization sets for weighted automata and for deterministic nominal automata.
Disclosure of Interests
The authors have no competing interests to declare that are relevant to the content of this article.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
arising from the adjunction \(- \otimes X \dashv [{X},{-}]\). We denote the counit of same adjunction by \(\varepsilon _{X,Y} :[{X},{Y}] \otimes X \rightarrow Y\). Furthermore, we fix two objects \(\varSigma , O\in \mathcal {C}\). We think of \(\varSigma \) as the alphabet object and of \(O\) as the output object. The alphabet object generalizes the set of input symbols for DFAs. In the case of DFAs, the output of a state is simply a Boolean value stating whether the state is accepting or not. The output object generalizes this concept, so that the output of a state can be an arbitrary value. We assume that \(\mathcal {C}\) has binary products and countable coproducts. Finally, we assume that for any \(X \in \mathcal {C}\), the functor \(X \otimes -\) preserves countable coproducts. This assumption is satisfied, for instance, if the functor \(X \otimes -\) also has a right adjoint, as is the case in any braided monoidal closed category.
and \([\kappa _{n+1}]_{n \in \mathbb {N}} :\sum _{n \in \mathbb {N}}{\varSigma ^{n+1}} \rightarrow \varSigma ^{*}\).
.
is a split epi.
be its \((\mathcal {E}, \mathcal {M})\)-factorization. Then for all automata \(\mathcal {\mathcal {S}}\) and \(\mathcal {\mathcal {M}}\), \(\mathcal {\mathcal {S}} \sim _{t} \mathcal {\mathcal {M}}\) if and only if \(\mathcal {\mathcal {S}} \sim _{t'} \mathcal {\mathcal {M}}\).
and
are to be understood as one transition for each \(a \in \mathbb {A}\). Furthermore, transitions of the form
for \(A \subseteq \mathbb {A}\) stand for a number of transitions, one for each \(a \in A\). The automaton \(\mathcal {\mathcal {S}}\) accepts the nominal language \(L = \left\{ aa\ |\ a \in \mathbb {A} \right\} \).
