Gerco Van Heerdt
email: gerco.heerdt@ucl.ac.uk

Matteo Sammartino
email: matteo.sammartino@rhul.ac.uk

Alexandra Silva
email: alexandra.silva@ucl.ac.uk

Learning Automata with Side-Effects

Keywords: automata, learning, side-effects, monads, algebras

Automata learning has been successfully applied in the verification of hardware and software. The size of the automaton model learned is a bottleneck for scalability, and hence optimizations that enable learning of compact representations are important. This paper exploits monads, both as a mathematical structure and a programming construct, to design and prove correct a wide class of such optimizations. Monads enable the development of a new learning algorithm and correctness proofs, building upon a general framework for automata learning based on category theory. The new algorithm is parametric on a monad, which provides a rich algebraic structure to capture non-determinism and other side-effects. We show that this allows us to uniformly capture existing algorithms, develop new ones, and add optimizations.

Introduction

The increasing complexity of software and hardware systems calls for new scalable methods to design, verify, and continuously improve systems. Black-box inference methods aim at building models of running systems by observing their response to certain queries. This reverse engineering process is very amenable for automation and allows for fine-tuning the precision of the model depending on the properties of interest, which is important for scalability.

One of the most successful instances of black-box inference is automata learning, which has been used in various verification tasks, ranging from finding bugs in implementations of network protocols [START_REF] De | Protocol state fuzzing of TLS implementations[END_REF] to rejuvenating legacy software [START_REF] Schuts | Refactoring of legacy software using model learning and equivalence checking: an industrial experience report[END_REF]. Vaandrager [START_REF] Frits | Model learning[END_REF] has written a comprehensive overview of the widespread use of automata learning in verification.

A limitation in automata learning is that the models of real systems can become too large to be handled by tools. This demands compositional methods and techniques that enable compact representation of behaviors.

In this paper, we show how monads can be used to add optimizations to learning algorithms in order to obtain compact representations. We will use as playground for our approach the well known L algorithm [START_REF] Angluin | Learning regular sets from queries and counterexamples[END_REF], which learns a minimal deterministic finite automaton (DFA) accepting a regular language by interacting with a teacher, i.e., an oracle that can reply to specific queries about the target language. Monads allow us to take an abstract approach, in which category theory is used to devise an optimized learning algorithm and a generic correctness proof for a broad class of compact models.

The inspiration for this work is quite concrete: it is a well-known fact that non-deterministic finite automata (NFAs) can be much smaller than deterministic ones for a regular language. The subtle point is that given a regular language, there is a canonical deterministic automaton accepting it-the minimal one-but there might be many "minimal" non-deterministic automata accepting the same language. This raises a challenge for learning algorithms: which non-deterministic automaton should the algorithm learn? To overcome this, Bollig et al. [START_REF] Bollig | Angluin-style learning of NFA[END_REF] developed a version of Angluin's L algorithm, which they called NL , in which they use a particular class of NFAs, Residual Finite State Automata (RFSAs), which do admit minimal canonical representatives. Though NL indeed is a first step in incorporating a more compact representation of regular languages, there are several questions that remain to be addressed. We tackle them in this paper.

DFAs and NFAs are formally connected by the subset construction. Underpinning this construction is the rich algebraic structure of languages and of the state space of the DFA obtained by determinizing an NFA. The state space of a determinized DFA-consisting of subsets of the state space of the original NFA-has a join-semilattice structure. Moreover, this structure is preserved in language acceptance: if there are subsets U and V , then the language of U ∪ V is the union of the languages of the first two. Formally, the function that assigns to each state its language is a join-semilattice map, since languages themselves are just sets of words and have a lattice structure. And languages are even richer: they have the structure of complete atomic Boolean algebras. This leads to several questions: Can we exploit this structure and have even more compact representations? What if we slightly change the setting and look at weighted languages over a semiring, which have the structure of a semimodule (or vector space, if the semiring is a field)?

The latter question is strongly motivated by the widespread use of weighted languages and corresponding weighted finite automata (WFAs) in verification, from the formal verification of quantitative properties [START_REF] Chatterjee | Quantitative languages[END_REF][START_REF] Droste | Weighted automata and weighted logics[END_REF][START_REF] Kuperberg | Linear temporal logic for regular cost functions[END_REF], to probabilistic model-checking [START_REF] Baier | Model checking linear-time properties of probabilistic systems[END_REF], to the verification of on-line algorithms [START_REF] Aminof | Reasoning about online algorithms with weighted automata[END_REF].

Our key insight is that the algebraic structures mentioned above are in fact algebras for a monad T . In the case of join-semilattices this is the powerset monad, and in the case of vector spaces it is the free vector space monad. These monads can be used to define a notion of T -automaton, with states having the structure of an algebra for the monad T , which generalizes non-determinism as a side-effect. From T -automata we can derive a compact, equivalent version by taking as states a set of generators and transferring the algebraic structure of the original state space to the transition structure of the automaton.

This general perspective enables us to generalize L to a new algorithm L T , which learns compact automata featuring non-determinism and other side-effects captured by a monad. Moreover, L T incorporates further optimizations arising from the monadic representation, which lead to more scalable algorithms.

We start by giving an overview of our approach, which also states our main contributions in greater detail and ends with a road map of the rest of the paper.

Overview and Contributions

In this section, we explain the original L algorithm and discuss the challenges in adapting the algorithm to learn automata with side-effects, illustrating them through a concrete example-NFAs. We then highlight our main contributions.

L algorithm. This algorithm learns the minimal DFA accepting a language L ⊆ A * over a finite alphabet A. It assumes the existence of a minimally adequate teacher, which is an oracle that can answer two types of queries: 1. Membership queries: given a word w ∈ A * , does w belong to L? and 2. Equivalence queries: given a hypothesis DFA H, does H accept L? If not, the teacher returns a counterexample, i.e., a word incorrectly classified by H. The algorithm incrementally builds an observation table made of two parts: a top part, with rows ranging over a finite set S ⊆ A * ; and a bottom part, with rows ranging over S • A (• is pointwise concatenation). Columns range over a finite E ⊆ A * . For each u ∈ S ∪ S • A and v ∈ E, the corresponding cell in the table contains 1 if and only if uv ∈ L. Intuitively, each row u contains enough information to fully identify the Myhill-Nerode equivalence class of u with respect to an approximation of the target language-rows with the same content are considered members of the same equivalence class. Cells are filled in using membership queries.

As an example, and to set notation, consider the table below over A = {a, b}. It shows that L contains the word aa and does not contain the words ε (the empty word), a, b, ba, aaa, and baa. E ε a aa S ε 0 0 1

S • A a 0 1 0 b 0 0 0 row t : S → 2 E row t (u)(v) = 1 ⇐⇒ uv ∈ L row b : S → (2 E ) A row b (u)(a)(v) = 1 ⇐⇒ uav ∈ L
We use functions row t and row b to describe the top and bottom parts of the table, respectively. Notice that S and S • A may intersect. For conciseness, when tables are depicted, elements in the intersection are only shown in the top part.

A key idea of the algorithm is to construct a hypothesis DFA from the different rows in the table. The construction is the same as that of the minimal DFA from the Myhill-Nerode equivalence, and exploits the correspondence between table rows and Myhill-Nerode equivalence classes. The state space of the hypothesis DFA is given by the set H = {row t (s) | s ∈ S}. Note that there may be multiple rows with the same content, but they result in a single state, as they all belong to the same Myhill-Nerode equivalence class. The initial state is row t (ε), and we use the ε column to determine whether a state is accepting: row t (s) is accepting whenever row t (s)(ε) = 1. The transition function is defined as row t (s) a -→ row b (s)(a). (Notice that the continuation is drawn from the bottom part of the table). For the hypothesis automaton to be well-defined, ε must be in S and E, and the table must satisfy two properties:

-Closedness states that each transition actually leads to a state of the hypothesis. That is, the table is closed if for all t ∈ S and a ∈ A there is s ∈ S such that row t (s) = row b (t)(a). -Consistency states that there is no ambiguity in determining the transitions.

That is, the table is consistent if for all s 1 , s 2 ∈ S such that row t (s 1 ) = row t (s 2 ) we have row b (s 1 ) = row b (s 2 ).

The algorithm updates the sets S and E to satisfy these properties, constructs a hypothesis, submits it in an equivalence query, and, when given a counterexample, refines the hypothesis. This process continues until the hypothesis is correct. The algorithm is shown in Fig. 1.

Example Run. We now run the algorithm with the target language

L = {w ∈ {a} * | |w| = 1}. The minimal DFA accepting L is M = a a a (1)
Initially, S = E = {ε}. We build the observation table given in Fig. 2a. This table is not closed, because the row with label a, having 0 in the only column, does not appear in the top part of the table: the only row ε has 1. To fix this, we add the word a to the set S. Now the table (Fig. 2b) is closed and consistent, so we construct the hypothesis that is shown in Fig. 2c and pose an equivalence query. The teacher replies no and informs us that the word aaa should have been accepted. L handles a counterexample by adding all its prefixes to the set S. We only have to add aa and aaa in this case. The next table (Fig. 2d) is closed, but not consistent: the rows ε and aa both have value 1, but their extensions a and aaa differ. To fix this, we prepend the continuation a to the column ε on which they differ and add a • ε = a to E. This distinguishes row t (ε) from row t (aa), as seen in the next table in Fig. 2e. The table is now closed and consistent, and the new hypothesis automaton is precisely the correct one M.

ε ε 1 a 0 (a) ε ε 1 a 0 aa 1 (b) a a (c) ε ε 1 a 0 aa 1 aaa 1 aaaa 1 (d) ε a ε 1 0 a 0 1 aa 1 1 aaa 1 1 aaaa 1 1 (e)
As mentioned, the hypothesis construction approximates the theoretical construction of the minimal DFA, which is unique up to isomorphism. That is, for S = E = A * the relation that identifies words of S having the same value in row t is precisely the Myhill-Nerode's right congruence.

Learning non-deterministic automata. As is well known, NFAs can be smaller than the minimal DFA for a given language. For example, the language L above is accepted by the NFA

N = a a a (2)
which is smaller than the minimal DFA M. Though in this example, which we chose for simplicity, the state reduction is not massive, it is known that in general NFAs can be exponentially smaller than the minimal DFA [START_REF] Dexter | Automata and computability[END_REF]. This reduction of the state space is enabled by a side-effect-non-determinism, in this case.

Learning NFAs can lead to a substantial gain in space complexity, but it is challenging. The main difficulty is that NFAs do not have a canonical minimal representative: there may be several non-isomorphic state-minimal NFAs accepting the same language, which poses problems for the development of the learning algorithm. To overcome this, Bollig et al. [START_REF] Bollig | Angluin-style learning of NFA[END_REF] proposed to use a particular class of NFAs, namely RFSAs, which do admit minimal canonical representatives. However, their ad-hoc solution for NFAs does not extend to other automata, such as weighted or alternating. In this paper we present a solution that works for any side-effect, specified as a monad.

The crucial observation underlying our approach is that the language semantics of an NFA is defined in terms of its determinization, i.e., the DFA obtained by taking sets of states of the NFA as state space. In other words, this DFA is defined over an algebraic structure induced by the powerset, namely a (complete) join semilattice (JSL) whose join operation is set union. This automaton model does admit minimal representatives, which leads to the key idea for our algorithm: learning NFAs as automata over JSLs. In order to do so, we use an extended table where rows have a JSL structure, defined as follows. The join of two rows is given by an element-wise or, and the bottom element is the row containing only zeroes. More precisely, the new table consists of the two functions

row t : P(S) → 2 E row b : P(S) → (2 E ) A
given by row

t (U ) = {row t (s) | s ∈ U } and row b (U )(a) = {row b (s)(a) | s ∈ U }.
Formally, these functions are JSL homomorphisms, and they induce the following general definitions:

-The table is closed if for all U ⊆ S, a ∈ A there is U ⊆ S such that row t (U ) = row b (U )(a). -The table is consistent if for all U 1 , U 2 ⊆ S s.t. row t (U 1 ) = row t (U 2 ) we have row b (U 1 ) = row b (U 2 ).
We remark that our algorithm does not actually store the whole extended Optimizations. In this paper we also present two optimizations to our algorithm. For the first one, note that the state space of the hypothesis constructed by the algorithm can be very large since it encodes the entire algebraic structure. We show that we can extract a minimal set of generators from the table and compute a succinct hypothesis in the form of an automaton with side-effects, without any algebraic structure. For JSLs, this consists in only taking rows that are not the join of other rows, i.e., the join-irreducibles. By applying this optimization to this specific case, we essentially recover the learning algorithm of Bollig et al. [START_REF] Bollig | Angluin-style learning of NFA[END_REF].

The second optimization is a generalization of the optimized counterexample handling method of Rivest and Schapire [START_REF] Rivest | Inference of finite automata using homing sequences[END_REF], originally intended for L and DFAs. It consists in processing counterexamples by adding a single suffix of the counterexample to E, instead of adding all prefixes of the counterexample to S. This can avoid the algorithm posing a large number of membership queries. Example Revisited. We now run the new algorithm on the language L = {w ∈ {a} * | |w| = 1} considered earlier. Starting from S = E = {ε}, the observation table (Fig. 3a) is immediately closed and consistent. (It is closed because we have row t ({a}) = row t (∅).) This gives the JSL hypothesis shown in Fig. 3b, which leads to an NFA hypothesis having a single state that is initial, accepting, and has no transitions (Fig. 3c). The hypothesis is incorrect, and the teacher may supply us with counterexample aa. Adding prefixes a and aa to S leads to the table in Fig. 3d. The table is again closed, but not consistent:

ε ε 1 a 0 (a) a a (b) (c) ε ε 1 a 0 aa 1 aaa 1 (d) ε a ε 1 0 a 0 1 aa 1 1 aaa 1 1 (e)
row t ({a}) = row t (∅), but row b ({a})(a) = row t ({aa}) = row t (∅) = row b (∅)(a)
. Thus, we add a to E. The resulting table (Fig. 3e) is closed and consistent. We note that row aa is the union of other rows: row t ({aa}) = row t ({ε, a}) (i.e., it is not a join-irreducible), and therefore can be ignored when building the succinct hypothesis. This hypothesis has two states, ε and a, and indeed it is the correct one N.

Contributions and road map of the paper. After some preliminary notions in Section 3, we present the main contributions:

-In Section 4, we develop a general algorithm L T , which generalizes the NFA one presented in Section 2 to an arbitrary monad T capturing side-effects, and we provide a general correctness proof for our algorithm. -In Section 5, we describe the first optimization and prove its correctness.

-In Section 6 we describe the second optimization. We also show how it can be combined with the one of Section 5, and how it can lead to a further small optimization, where the consistency check on the table is dropped. -Finally, in Section 7 we show how L T can be applied to several automata models, highlighting further case-specific optimizations when available.

Preliminaries

In this section we define a notion of T -automaton, a generalization of nondeterministic finite automata parametric in a monad T . We assume familiarity with basic notions of category theory: functors (in the category Set of sets and functions) and natural transformations. Side-effects can be conveniently captured as a monad. A monad T = (T, η, µ) is a triple consisting of an endofunctor T on Set and two natural transformations: a unit η : Id ⇒ T and a multiplication µ : T 2 ⇒ T , which satisfy the compatibility laws µ

• η T = id T = µ • T η and µ • µ T = µ • T µ.
Example 1 (Monads). An example of a monad is the triple (P, {-}, ), where P denotes the powerset functor associating a collection of subsets to a set, {-} is the singleton operation, and is just union of sets. Another example is the triple (V (-), e, m), where V (X) is the free semimodule (over a semiring S) over X, namely {ϕ | ϕ : X → S having finite support}. The support of a function ϕ : X → S is the set of x ∈ X such that ϕ(x) = 0. Then e : X → V (X) is the characteristic function for each x ∈ X, and m :

V (V (X)) → V (X) is defined for ϕ ∈ V (V (X)) and x ∈ X as m(ϕ)(x) = ψ∈V (X) ϕ(ψ) × ψ(x).
Given a monad T , a T -algebra is a pair (X, h) consisting of a carrier set X and a function h :

T X → X such that h • µ X = h • T h and h • η X = id X . A T -homomorphism between two T -algebras (X, h) and (Y, k) is a function f : X → Y such that f • h = k • T f
. The abstract notion of T -algebra instantiates to expected notions, as illustrated in the following example.

Example 2 (Algebras for a monad). The P-algebras are the (complete) joinsemilattices, and their homomorphisms are join-preserving functions. If S is a field, V -algebras are vector spaces, and their homomorphisms are linear maps.

We will often refer to a T -algebra (X, h) as X if h is understood or if its specific definition is irrelevant. Given a set X, (T X, µ X ) is a T -algebra called the free T -algebra on X. One can build algebras pointwise for some operations. For instance, if Y is a set and (X, x) a T -algebra, then we have a T -algebra (X Y , f ), where f : T (X Y ) → X Y is given by f (W )(y) = (x • T (ev y ))(W ) and ev y : X Y → X by ev y (g) = g(y). If U and V are T -algebras and f : U → V is a T -algebra homomorphism, then the image img(f ) of f is a T -algebra, with the T -algebra structure inherited from V . The following proposition connects algebra homomorphisms from the free T -algebra on a set U to an algebra V with functions U → V . We will make use of this later in the section. Proposition 3. Given a set U and a T -algebra (V, v), there is a bijective correspondence between T -algebra homomorphisms T U → V and functions U → V : for a T -algebra homomorphism f :

T U → V , define f † = f • η : U → V ; for a function g : U → V , define g = v • T g : T U → V .
Then g is a T -algebra homomorphism called the free T -extension of g, and we have f † = f and g † = g.

We now have all the ingredients to define our notion of automaton with sideeffects and their language semantics. We fix a monad (T, η, µ) with T preserving finite sets, as well as a T -algebra O that models outputs of automata.

Definition 4 (T -automaton

). A T -automaton is a quadruple (Q, δ : Q → Q A , out : Q → O, init ∈ Q),
where Q is a T -algebra, the transition map δ and output map out are T -algebra homomorphisms, and init is the initial state.

Example 5. DFAs are Id-automata when O = 2 = {0, 1} is used to distinguish accepting from rejecting states. For the more general case of O being any set, DFAs generalize into Moore automata. Example 6. Recall that P-algebras are JSLs, and their homomorphisms are joinpreserving functions. In a P-automaton, Q is equipped with a join operation, and Q A is a join-semilattice with pointwise join: (f ∨ g)(a) = f (a) ∨ g(a) for a ∈ A. Since the automaton maps preserve joins, we have, in particular, δ(q 1 ∨ q 2 )(a) = δ(q 1 )(a) ∨ δ(q 2 )(a). One can represent an NFA over a set of states S as a Pautomaton by taking Q = (P(S), ) and O = 2, the Boolean join-semilattice with the or operation as its join. Let init ⊆ S be the set of initial states and out : P(Q) → 2 and δ : P(S) → P(S) A the respective extensions (Proposition 3) of the NFA's output and transition functions. The resulting P-automaton is precisely the determinized version of the NFA.

More generally, an automaton with side-effects given by a monad T always represents a T -automaton with a free state space. Proposition 7. A T -automaton of the form ((T X, µ X ), δ, out, init), for any set X, is completely defined by the set X with the element init ∈ T X and functions

δ † : X → (T X) A out † : X → O.
We call such a T -automaton a succinct automaton, which we sometimes identify with the representation (X, δ † , out † , init). These automata are closely related to the ones studied in [START_REF] Goncharov | Towards a coalgebraic chomsky hierarchy[END_REF].

A (generalized) language is a function L : A * → O. For every T -automaton we have an observability and a reachability map, telling respectively which state is reached by reading a given word and which language each state recognizes.

Definition 8 (Reachability/Observability Maps). The reachability map of a T -automaton A is a function r

A : A * → Q inductively defined as: r A (ε) = init and r A (ua) = δ(r A (u))(a). The observability map of A is a function o A : Q → O A * given by: o A (q)(ε) = out(q) and o A (q)(av) = o A (δ(q)(a))(v).
The language accepted by A is the map

L A = o A (init) = out A • r A : A * → O.
Example 9. For an NFA A represented as a P-automaton, as seen in Example 6, o A (q) is the language of q in the traditional sense. Note that q, in general, is a set of states: o A (q) takes the union of languages of singleton states. The set L A is the language accepted by the initial states, i.e., the language of the NFA. The reachability map r A (u) returns the set of states reached via all paths reading u.

Given a language L : A * → O, there exists a (unique) minimal T -automaton M L accepting L, which is minimal in the number of states. Its existence follows from general facts. See for example [START_REF] Gerco Van Heerdt | An abstract automata learning framework[END_REF]. In the following, we will also make use of the minimal Moore automaton accepting L. Although this always exists-by instantiating Definition 10 with T = Id-it need not be finite. The following property says that finiteness of Moore automata and of T -automata accepting the same language are related.

Proposition 11. The minimal Moore automaton accepting L is finite if and only if the minimal T -automaton accepting L is finite.

A General Algorithm

In this section we introduce our extension of L to learn automata with side-effects. The algorithm is parametric in the notion of side-effect, represented as the monad T , and is therefore called L T . We fix a language L : A * → O that is to be learned, and we assume that there is a finite T -automaton accepting L. This assumption generalizes the requirement of L that L is regular (i.e., accepted by a specific class of T -automata, see Example 5).

An observation table consists of a pair of functions

row t : S → O E row b : S → (O E ) A
given by row t (s)(e) = L(se) and row b (s)(a)(e) = L(sae), where S, E ⊆ A * are finite sets with ε ∈ S ∩ E. For O = 2, we recover exactly the L observation table . The key idea for L T is defining closedness and consistency over the free T -extensions of those functions.

Definition 12 (Closedness and Consistency). The table is closed if for all U ∈ T (S) and a ∈ A there exists a U ∈ T (S) such that row

t (U ) = row b (U )(a). The table is consistent if for all U 1 , U 2 ∈ T (S) such that row t (U 1 ) = row t (U 2 ) we have row b (U 1 ) = row b (U 2 ).
For closedness, we do not need to check all elements of T (S) × A against elements of T (S), but only those of S × A, thanks to the following result.

Lemma 13. If for all s ∈ S and a ∈ A there is U ∈ T (S) such that row t (U ) = row b (s)(a), then the table is closed. Example 14. For NFAs represented as P-automata, the properties are as presented in Section 2. Recall that for T = P and O = 2, the Boolean join-semilattice, row t and row b describe a table where rows are labeled by subsets of S. Then we have, for instance, row t ({s 1 , s 2 })(e) = row t (s 1 )(e) ∨ row t (s 2 )(e), i.e., row t ({s 1 , s 2 })(e) = 1 if and only if L(s 1 e) = 1 or L(s 2 e) = 1. Closedness amounts to check whether each row in the bottom part of the table is the join of a set of rows in the top part. Consistency amounts to check whether, for all sets of rows U 1 , U 2 ⊆ S in the top part of the table whose joins are equal, the joins of rows U 1 • {a} and U 2 • {a} in the bottom part are also equal, for all a ∈ A. If closedness and consistency hold, we can define a hypothesis T -automaton H, with state space H = img(row t ), init = row t (ε), and output and transitions

out : H → O out(row t (U )) = row t (U )(ε) δ : H → H A δ(row t (U )) = row b (U ).
The correctness of this definition follows from the abstract treatment of [START_REF] Gerco Van Heerdt | CALF: categorical automata learning framework[END_REF], instantiated to the category of T -algebras and their homomorphisms.

We can now give algorithm L T . Similarly to the example in Section 2, we only have to adjust lines 5 and 8 in Fig. 1. The resulting algorithm is shown in Fig. 4.

Correctness.

Correctness for L T amounts to proving that, for any target language L, the algorithm terminates returning the minimal T -automaton M L accepting L. As in the original L algorithm, we only need to prove that the algorithm terminates, that is, that only finitely many hypotheses are produced. Correctness follows from termination, since line 13 causes the algorithm to terminate only if the hypothesis automaton coincides with M L .

In order to show termination, we argue that the state space H of the hypothesis increases while the algorithm loops, and that H cannot be larger than M , the state space of M L . In fact, when a closedness defect is resolved (line 6), a row that was not previously found in the image of row t : T (S) → O E is added, so the set H grows larger. When a consistency defect is resolved (line 9), two previously equal rows become distinguished, which also increases the size of H.

As for counterexamples, adding their prefixes to S (line 11) creates a consistency defect, which will be fixed during the next iteration, causing H to increase. This is due to the following result, which says that the counterexample z has a prefix that violates consistency. Note that the hypothesis H in the statement below is the hypothesis obtained before adding the prefixes of z to S. Proposition 15. If z ∈ A * is such that L H (z) = L(z) and prefixes(z) ⊆ S, then there are a prefix ua of z, with u ∈ A * and a ∈ A, and U ∈ T (S) such that row t (u) = row t (U ) and row b (u)(a) = row b (U )(a). Now, note that by increasing S or E, the hypothesis state space H never decreases in size. Moreover, for S = A * and E = A * , row t = t L . Therefore, since H and M are defined as the images of row t and t L , respectively, the size of H is bounded by that of M . Since H increases while the algorithm loops, the algorithm must terminate and is thus correct.

Note that the learning algorithm of Bollig et al. does not terminate using this counterexample processing method [START_REF] Bollig | Angluin-style learning of nfa[END_REF]Appendix F]. This is due to their notion of consistency being weaker than ours: we have shown that progress is guaranteed because a consistency defect, in our sense, is created using this method.

Query complexity. The complexity of automata learning algorithms is usually measured in terms of the number of both membership and equivalence queries asked, as it is common to assume that computations within the algorithm are insignificant compared to evaluating the system under analysis in applications. The cost of answering queries themselves is not considered, as it depends on the implementation of the teacher, which the algorithm abstracts from.

The table is a T -algebra homomorphism, so membership queries for rows labeled in S are enough to determine all other rows. We measure the query complexities in terms of the number of states n of the minimal Moore automaton, the number of states t of the minimal T -automaton, the size k of the alphabet, and the length m of the longest counterexample. Note that t cannot be smaller than n, but it can be much bigger. For example, when T = P, t may be in O(2 n ). 3The maximum number of closedness defects fixed by the algorithm is n, as a closedness defect for the setting with algebraic structure is also a closedness defect for the setting without that structure. The maximum number of consistency defects fixed by the algorithm is t, as fixing a consistency defect distinguishes two rows that were previously identified. Since counterexamples lead to consistency defects, this also means that the algorithm will not pose more than t equivalence queries. A word is added to S when fixing a closedness defect, and O(m) words are added to S when processing a counterexample. The number of rows that we need to fill using queries is therefore in O(tmk). The number of columns added to the table is given by the number of times a consistency defect is fixed and thus in O(t). Altogether, the number of membership queries is in O(t 2 mk).

Succinct Hypotheses

We now describe the first of two optimizations, which is enabled by the use of monads. Our algorithm produces hypotheses that can be quite large, as their state space is the image of row t , which has the whole set T (S) as its domain. For instance, when T = P, T (S) is exponentially larger than S. We show how we can compute succinct hypotheses, whose state space is given by a subset of S. We start by defining sets of generators for the table. Definition 16. A set S ⊆ S is a set of generators for the table whenever for all s ∈ S there is U ∈ T (S ) such that row t (s) = row t (U ). 4Intuitively, U is the decomposition of s into a "combination" of generators. When T = P, S generates the table whenever each row can be obtained as the join of a set of rows labeled by S . Explicitly: for all s ∈ S there is {s 1 , . . . , s n } ⊆ S such that row t (s) = row t ({s 1 , . . . ,

s n }) = row t (s 1 ) ∨ • • • ∨ row t (s n ).
Recall that H, with state space H, is the hypothesis automaton for the table. The existence of generators S allows us to compute a T -automaton with state space T (S ) equivalent to H. We call this the succinct hypothesis, although T (S ) may be larger than H. Proposition 7 tells us that the succinct hypothesis can be represented as an automaton with side-effects in T that has S as its state space. This results in a lower space complexity when storing the hypothesis.

We now show how the succinct hypothesis is computed. Observe that, if generators S exist, row t factors through the restriction of itself to T (S ). Denote this latter function row t . Since we have T (S ) ⊆ T (S), the image of row t coincides with img(row t ) = H, and therefore the surjection restricting row t to its image has the form e : T (S ) → H. Any right inverse i : H → T (S ) of the function e (that is, e • i = id H , but whereas e is a T -algebra homomorphism, i need not be one) yields a succinct hypothesis as follows.

Definition 17 (Succinct Hypothesis). The succinct hypothesis is the Tautomaton S = (T (S ), δ, out, init) given by init = i(row t (ε)) and

out † : S → O out † (s) = row t (s)(ε) δ † : S → T (S ) A δ † (s)(a) = i(row b (s)(a)).
This definition is inspired by that of a scoop, due to Arbib and Manes [START_REF] Arbib | Fuzzy machines in a category[END_REF].

Proposition 18. Any succinct hypothesis of H accepts the language of H.

We now give a simple procedure to compute a minimal set of generators, that is, a set S such that no proper subset is a set of generators. This generalizes a procedure defined by Angluin et al. [START_REF] Angluin | Learning regular languages via alternating automata[END_REF] for non-deterministic, universal, and alternating automata.

Proposition 19. The following algorithm returns a minimal set of generators for the table:

S ← S while there are s ∈ S and U ∈ T (S \ {s}) s.t. row t (U ) = row t (s) S ← S \ {s} return S To determine whether U as in the above algorithm exists, one can always naively enumerate all possibilities, using that T preserves finite sets. This is what we call the basic algorithm. For specific algebraic structures, one may find more efficient methods, as we show in the following example.

Example 20. Consider the powerset monad T = P. We now exemplify two ways of computing succinct hypotheses, which are inspired by canonical RFSAs [START_REF] Denis | Residual finite state automata[END_REF]. The basic idea is to start from a deterministic automaton and to remove states that are equivalent to a set of other states. The algorithm given in Proposition 19 computes a minimal S that only contains labels of rows that are not the join of other rows. (In case two rows are equal, only one of their labels is kept.) In other words, as mentioned in Section 2, S contains labels of join-irreducible rows. To concretize the algorithm efficiently, we use a method introduced by Bollig et al. [START_REF] Bollig | Angluin-style learning of NFA[END_REF], which essentially exploits the natural order on the JSL of table rows. In contrast to the basic exponential algorithm, this results in a polynomial one. 5Bollig et al. determine whether a row is a join of other rows by comparing the row just to the join of rows below it. Like them, we make use of this also to compute right inverses of e, for which we will formalize the order.

The function e : P(S ) → H tells us which sets of rows are equivalent to a single state in H. We show two right inverses H → P(S ) for it. The first one,

i 1 (h) = {s ∈ S | row t (s) ≤ h},
stems from the construction of the canonical RFSA of a language [START_REF] Denis | Residual finite state automata[END_REF]. Here we use the order a ≤ b ⇐⇒ a ∨ b = b induced by the JSL structure. The resulting construction of a succinct hypothesis was first used by Bollig et al. [11]. This succinct hypothesis has a "maximal" transition function, meaning that no more transitions can be added without changing the language of the automaton.

The second inverse is

i 2 (h) = {s ∈ S | row t (s) ≤ h and for all s ∈ S s.t. row t (s) ≤ row t (s ) ≤ h we have row t (s) = row t (s )},
resulting in a more economical transition function, where some redundancies are removed. This corresponds to the simplified canonical RFSA [START_REF] Denis | Residual finite state automata[END_REF].

Example 21. Consider T = P, and recall the table in Fig. 3e. When S = S, the right inverse given by i 1 yields the succinct hypothesis shown below.

a a a a a a a Note that i 1 (row t (aa)) = {ε, a, aa}. Taking i 2 instead, the succinct hypothesis is just the DFA (1) because i 2 (row t (aa)) = {aa}. Rather than constructing a succinct hypothesis directly, our algorithm first reduces the set S . In this case, we have row t (aa) = row t ({ε, a}), so we remove aa from S . Now i 1 and i 2 coincide and produce the NFA [START_REF] Angluin | Learning regular sets from queries and counterexamples[END_REF]. Minimizing the set S in this setting essentially comes down to determining what Bollig et al. [START_REF] Bollig | Angluin-style learning of NFA[END_REF] call the prime rows of the table.

Remark 22. The algorithm in Proposition 19 implicitly assumes an order in which elements of S are checked. Although the algorithm is correct for any such order, different orders may give results that differ in size.

Optimized Counterexample Handling

The second optimization we give generalizes the counterexample processing method due to Rivest and Schapire [START_REF] Rivest | Inference of finite automata using homing sequences[END_REF], which improves the worst case complexity of the number of membership queries needed in L . Maler and Pnueli [START_REF] Maler | On the learnability of infinitary regular sets[END_REF] proposed to add all suffixes of the counterexample to the set E instead of adding all prefixes to the set S. This eliminates the need for consistency checks in the deterministic setting. The method by Rivest and Schapire finds a single suffix of the counterexample and adds it to E. This suffix is chosen in such a way that it either distinguishes two existing rows or creates a closedness defect, both of which imply that the hypothesis automaton will grow.

The main idea is finding the distinguishing suffix via the hypothesis automaton H. Given u ∈ A * , let q u be the state in H reached by reading u, i.e., q u = r H (u). For each q ∈ H, we pick any U q ∈ T (S) that yields q according to the table, i.e., such that row t (U q ) = q. Then for a counterexample z we have that the residual language w.r.t. U qz does not "agree" with the residual language w.r.t. z.

The above intuition can be formalized as follows. Let R : A * → O A * be given by R(u) = t L (U qu ) for all u ∈ A * , the residual language computation. We have the following technical lemma, saying that a counterexample z distinguishes the residual languages t L (z) and R(z).

Lemma 23. If z ∈ A * is such that L H (z) = L(z), then t L (z)(ε) = R(z)(ε).
We assume that U qε = η(ε). For a counterexample z, we then have

R(ε)(z) = t L (ε)(z) = R(z)(ε).
While reading z, the hypothesis automaton passes a sequence of states q u0 , q u1 ,q u2 ,. . . ,q un , where u 0 = , u n = z, and u i+1 = u i a for some a ∈ A is a prefix of z. If z were correctly classified by H, all residuals R(u i ) would classify the remaining suffix v of z, i.e., such that z = u i v, in the same way. However, the previous lemma tells us that, for a counterexample z, this is not case, meaning that for some suffix v we have R(ua)(v) = R(u)(av). In short, this inequality is discovered along a transition in the path to z.

Corollary 24. If z ∈ A * is such that L H (z) = L(z), then there are u, v ∈ A * and a ∈ A such that uav = z and R(ua)(v) = R(u)(av).
To find such a decomposition efficiently, Rivest and Schapire use a binary search algorithm. We conclude with the following result that turns the above property into the elimination of a closedness witness. That is, given a counterexample z and the resulting decomposition uav from the above corollary, we show that, while currently row t (U qua ) = row b (U qu )(a), after adding v to E we have row t (U qua )(v) = row b (U qu )(a)(v). (To see that the latter follows from the proposition below, note that for all U ∈ T (S) and e ∈ E, row t (U )(e) = t L (U )(e) and for each a ∈ A, row b (U )(a )(e) = t L (U )(a e).) The inequality means that either we have a closedness defect, or there still exists some U ∈ T (S) such that row t (U ) = row b (U qu )(a). In this case, the rows row t (U ) and row t (U qua ) have become distinguished by adding v, which means that the size of H has increased. A closedness defect also increases the size of H, so in any case we make progress.

Proposition 25. If z ∈ A * is such that L H (z) = L(z), then there are u, v ∈ A * and a ∈ A such that row t (U qua ) = row b (U qu )(a) and t L (U qua )(v) = t L (U qu )(av).
We now show how to combine this optimized counterexample processing method with the succinct hypothesis optimization from Section 5. Recall that the succinct hypothesis S is based on a right inverse i : H → T (S ) of e : T (S ) → H. Choosing such an i is equivalent to choosing U q for each q ∈ H. We then redefine R using the reachability map of the succinct hypothesis. Specifically,

R(u) = t L (r S (u)) for all u ∈ A * .
Unfortunately, there is one complication. We assumed earlier that U qε = η(ε), or more specifically R(ε)(z) = L(z). This now may be impossible because we do not even necessarily have ε ∈ S . We show next that if this equality does not hold, then there are two rows that we can distinguish by adding z to E. Thus, after testing whether R(ε)(z) = L(z), we either add z to E (if the test fails) or proceed with the original method.

Proposition 26. If z ∈ A * is such that R(ε)(z) = L(z), then row t (init S ) = row t (ε) and t L (init S )(z) = t L (ε)(z).
To see that the original method still works, we prove the analogue of Proposition 25 for the new definition of R.

Proposition 27. If z ∈ A * is such that L S (z) = L(z) and R(ε)(z) = L(z), then there are u, v ∈ A * and a ∈ A such that row t (r † S (ua)) = row b (r † S (u))(a) and t L (r † S (ua))(v) = t L (r † S (u))(av). Example 28.
Recall the succinct hypothesis S from Fig. 3c for the table in Fig. 2a. Note that S = S cannot be further reduced. The hypothesis is based on the right inverse i : H → P(S) of e : P(S) → H given by i(row t (ε)) = {ε} and i(row t (∅)) = ∅. This is the only possible right inverse because e is bijective. For the prefixes of the counterexample aa we have r S (ε) = {ε} and r S (a) = r S (aa) = ∅. Note that t L ({ε})(aa) = 1 while t L (∅)(a) = t L (∅)(ε) = 0. Thus, R(ε)(aa) = R(a)(a). Adding a to E would indeed create a closedness defect.

Query complexity. Again, we measure the membership and equivalence query complexities in terms of the number of states n of the minimal Moore automaton, the number of states t of the minimal T -automaton, the size k of the alphabet, and the length m of the longest counterexample.

A counterexample now gives an additional column instead of a set of rows, and we have seen that this leads to either a closedness defect or to two rows being distinguished. Thus, the number of equivalence queries is still at most t, and the number of columns is still in O(t). However, the number of rows that we need to fill using membership queries is now in O(nk). This means that a total of O(tnk) membership queries is needed to fill the table.

Apart from filling the table, we also need queries to analyze counterexamples. The binary search algorithm mentioned after Corollary 24 requires for each counterexample O(log m) computations of R(x)(y) for varying words x and y. Let r be the maximum number of queries required for a single such computation. Note that for u, v ∈ A * , and letting α : T O → O be the algebra structure on O,

we have R(u)(v) = α(T (ev v • t L )(U qu )) for the original definition of R and R(u)(v) = α(T (ev v • t L )(r † S (u)))
in the succinct hypothesis case. Since the restricted map Dropping Consistency. We described the counterexample processing method based around Proposition 25 in terms of the succinct hypothesis S rather than the actual hypothesis H by showing that R can be defined using S. Since the definition of the succinct hypothesis does not rely on the property of consistency to be well-defined, this means we could drop the consistency check from the algorithm altogether. We can still measure progress in terms of the size of the set H, but it will not be the state space of an actual hypothesis during intermediate stages. This observation also explains why Bollig et al. [START_REF] Bollig | Angluin-style learning of NFA[END_REF] are able to use a weaker notion of consistency in their algorithm. Interestingly, they exploit the canonicity of their choice of succinct hypotheses to arrive at a polynomial membership query complexity that does not involve the factor t.

T (ev v • t L ) : T S → T O is completely determined by ev v • t L : S → O,

Examples

In this section we list several examples that can be seen as T -automata and hence learned via an instance of L T . We remark that, since our algorithm operates on finite structures (recall that T preserves finite sets), for each automaton type one can obtain a basic, correct-by-construction instance of L T for free, by plugging the concrete definition of the monad into the abstract algorithm. However, we note that this is not how L T is intended to be used in a real-world context; it should be seen as an abstract specification of the operations each concrete implementation needs to perform, or, in other words, as a template for real implementations.

For each instance below, we discuss whether certain operations admit a more efficient implementation than the basic one, based on the specific algebraic structure induced by the monad. Due to our general treatment, the optimizations of Sections 5 and 6 apply to all of these instances.

Non-deterministic automata. As discussed before, non-deterministic automata are P-automata with a free state space, provided that O = 2 is equipped with the "or" operation as its P-algebra structure. We also mentioned that, as Bollig et al. [START_REF] Bollig | Angluin-style learning of NFA[END_REF] showed, there is a polynomial time algorithm to check whether a given row is the join of other rows. This gives an efficient method for handling closedness straight away. Moreover, as shown in Example 20, it allows for an efficient construction of the succinct hypothesis. Unfortunately, checking for consistency defects seems to require a number of computations exponential in the number of rows. However, as explained at the end of Section 6, we can in fact drop consistency altogether.

Universal automata. Just like non-deterministic automata, universal automata can be seen as P-automata with a free state space. The difference is that the P-algebra structure on O = 2 is dual: it is given by the "and" rather than the "or" operation. Universal automata accept a word when all paths reading that word are accepting. One can dualize the optimized specific algorithms for the case of non-deterministic automata. This is precisely what Angluin et al. [START_REF] Angluin | Learning regular languages via alternating automata[END_REF] have done.

Partial automata. Consider the maybe monad Maybe(X) = 1 + X, with natural transformations having components η X : X → 1 + X and µ X : 1 + 1 + X → 1 + X defined in the standard way. Partial automata with states X can be represented as Maybe-automata with state space Maybe(X) = 1 + X, where there is an additional sink state, and output algebra O = Maybe(1) = 1 + 1. Here the left value is for rejecting states, including the sink one. The transition map δ : 1 + X → (1 + X) A represents an undefined transition as one going to the sink state. The algorithm L Maybe is mostly like L , except that implicitly the table has an additional row with zeroes in every column. Since the monad only adds a single element to each set, there is no need to optimize the basic algorithm for this specific case.

Weighted automata. Recall from Section 3 the free semimodule monad V , sending a set X to the free semimodule over a finite semiring S. Weighted automata over a set of states X can be represented as V -automata whose state space is the semimodule V (X), the output function out : V (X) → S assigns a weight to each state, and the transition map δ : V (X) → V (X) A sends each state and each input symbol to a linear combination of states. The obvious semimodule structure on S extends to a pointwise structure on the potential rows of the table. The basic algorithm loops over all linear combinations of rows to check closedness and over all pairs of combinations of rows to check consistency, making them extremely expensive operations. If S is a field, a row can be decomposed into a linear combination of other rows in polynomial time using standard techniques from linear algebra. As a result, there are efficient procedures for checking closedness and constructing succinct hypotheses. It was shown by Van Heerdt et al. [START_REF] Gerco Van Heerdt | CALF: categorical automata learning framework[END_REF] that consistency in this setting is equivalent to closedness of the transpose of the table. This trick is due to Bergadano and Varricchio [START_REF] Bergadano | Learning behaviors of automata from multiplicity and equivalence queries[END_REF], who first studied learning of weighted automata.

Alternating automata. We use the characterization of alternating automata due to Bertrand and Rot [START_REF] Bertrand | Coalgebraic determinization of alternating automata[END_REF]. Recall that, given a partially ordered set (P, ≤), an upset is a subset U of P such that, if x ∈ U and x ≤ y, then y ∈ U . Given Q ⊆ P , we write ↑Q for the upward closure of Q, that is the smallest upset of P containing Q. We consider the monad A that maps a set X to the set of all upsets of P(X). Its unit is given by η X (x) =↑{{x}} and its multiplication by

µ X (U ) = {V ⊆ X | ∃ W ∈U ∀ Y ∈W ∃ Z∈Y Z ⊆ V }.
Algebras for the monad A are completely distributive lattices [START_REF] Markowsky | Free completely distributive lattices[END_REF]. The sets of sets in A(X) can be seen as DNF formulae over elements of X, where the outer powerset is disjunctive and the inner one is conjunctive. Accordingly, we define an algebra structure β : A(2) → 2 on the output set 2 by letting β(U ) = 1 if {1} ∈ U , 0 otherwise. Alternating automata with states X can be represented as A-automata with state space A(X), output map out : A(X) → 2, and transition map δ : A(X) → A(X) A , sending each state to a DNF formula over X. The only difference with the usual definition of alternating automata is that A(X) is not the full set PP(X), which is not a monad [START_REF] Klin | Iterated covariant powerset is not a monad[END_REF]. However, for each formula in PP(X) there is an equivalent one in A(X).

An adaptation of L for alternating automata was introduced by Angluin et al. [START_REF] Angluin | Learning regular languages via alternating automata[END_REF] and further investigated by Berndt et al. [START_REF] Berndt | Learning residual alternating automata[END_REF]. The former found that given a row r ∈ 2 E and a set of rows X ⊆ 2 E , r is equal to a DNF combination of rows from X (where logical operators are applied component-wise) if and only if it is equal to the combination defined by Y = {{x ∈ X | x(e) = 1} | e ∈ E ∧ r(e) = 1}. We can reuse this idea to efficiently find closedness defects and to construct the hypothesis. Even though the monad A formally requires the use of DNF formulae representing upsets, in the actual implementation we can use smaller formulae, e.g., Y above instead of its upward closure. In fact, it is easy to check that DNF combinations of rows are invariant under upward closure. Similar as before, we do not know of an efficient way to ensure consistency, but we could drop it.

Writer automata. The examples considered so far involve existing classes of automata. To further demonstrate the generality of our approach, we introduce a new (as far as we know) type of automaton, which we call writer automaton.

The writer monad Writer(X) = M × X for a finite monoid M has a unit η X : X → M × X given by adding the unit e of the monoid, η X (x) = (e, x), and a multiplication µ X : M × M × X → M × X given by performing the monoid multiplication, µ X (m 1 , m 2 , x) = (m 1 m 2 , x). In Haskell, the writer monad is used for such tasks as collecting successive log messages, where the monoid is given by the set of sets or lists of possible messages and the multiplication adds a message.

The algebras for this monad are sets Q equipped with an M-action. One may take the output object to be the set M with the monoid multiplication as its action. Writer-automata with a free state space can be represented as deterministic automata that have an element of M associated with each transition. The semantics is as expected: M-elements multiply along paths and finally multiply with the output of the last state to produce the actual output.

The basic learning algorithm has polynomial time complexity. To determine whether a given row is a combination of rows in the table, i.e., whether it is given by a monoid value applied to one of the rows in the table, one simply tries all of these values. This allows us to check for closedness, to minimize the generators, and to construct the succinct hypothesis, in polynominal time. Consistency involves comparing all ways of applying monoid values to rows and, for each comparison, at most |A| further comparisons between one-letter extensions. The total number of comparisons is clearly polynomial in |M|, |S|, and |A|.

Conclusion

We have presented L T , a general adaptation of L that uses monads to learn an automaton with algebraic structure, as well as a method for finding a succinct equivalent based on its generators. Furthermore, we adapted the optimized counterexample handling method of Rivest and Schapire [START_REF] Rivest | Inference of finite automata using homing sequences[END_REF] to this setting and discussed instantiations to non-deterministic, universal, partial, weighted, alternating, and writer automata.

Related Work. This paper builds on and extends the theoretical toolkit of Van Heerdt et al. [START_REF] Gerco Van Heerdt | CALF: categorical automata learning framework[END_REF][START_REF] Gerco Van Heerdt | An abstract automata learning framework[END_REF], who are developing a categorical automata learning framework (CALF) in which learning algorithms can be understood and developed in a structured way.

An adaptation of L that produces NFAs was first developed by Bollig et al. [START_REF] Bollig | Angluin-style learning of NFA[END_REF]. Their algorithm learns a special subclass of NFAs consisting of RFSAs, which were introduced by Denis et al. [START_REF] Denis | Residual finite state automata[END_REF]. Angluin et al. [START_REF] Angluin | Learning regular languages via alternating automata[END_REF] unified algorithms for NFAs, universal automata, and alternating automata, the latter of which was further improved by Berndt et al. [START_REF] Berndt | Learning residual alternating automata[END_REF]. We are able to provide a more general framework, which encompasses and goes beyond those classes of automata. Moreover, we study optimized counterexample handling, which [START_REF] Angluin | Learning regular languages via alternating automata[END_REF][START_REF] Bollig | Angluin-style learning of NFA[END_REF][START_REF] Berndt | Learning residual alternating automata[END_REF] do not consider.

The algorithm for weighted automata over an arbitrary field was studied in a category theoretical context by Jacobs and Silva [START_REF] Jacobs | Automata learning: A categorical perspective[END_REF] and elaborated on by Van Heerdt et al. [START_REF] Gerco Van Heerdt | CALF: categorical automata learning framework[END_REF]. The algorithm itself was introduced by Bergadano and Varricchio [START_REF] Bergadano | Learning behaviors of automata from multiplicity and equivalence queries[END_REF]. The theory of succinct automata used for our hypotheses is based on the work of Arbib and Manes [START_REF] Arbib | Fuzzy machines in a category[END_REF], revamped to more recent category theory. Future Work. Whereas our general algorithm effortlessly instantiates to monads that preserve finite sets, a major challenge lies in investigating monads that do not enjoy this property. The algorithm for weighted automata generalizes to an infinite field [START_REF] Bergadano | Learning behaviors of automata from multiplicity and equivalence queries[END_REF][START_REF] Jacobs | Automata learning: A categorical perspective[END_REF][START_REF] Gerco Van Heerdt | CALF: categorical automata learning framework[END_REF] and even a principal ideal domain [START_REF] Gerco Van Heerdt | Learning weighted automata over principal ideal domains[END_REF]. However, for an infinite semiring in general we cannot guarantee termination, which is because a finitely generated semimodule may have an infinite chain of strict submodules [START_REF] Gerco Van Heerdt | Learning weighted automata over principal ideal domains[END_REF]. Intuitively, this means that while fixing closedness defects increases the size of the hypothesis state space semimodule, an infinite number of steps may be needed to resolve all closedness defects. In future work we would like to characterize more precisely for which semirings we can learn, and ideally formulate this characterization on the monad level.

As a result of the correspondence between learning and conformance testing [START_REF] Berg | On the correspondence between conformance testing and regular inference[END_REF][START_REF] Gerco Van Heerdt | CALF: categorical automata learning framework[END_REF], it should be possible to include in our framework the W-method [START_REF] Tsun | Testing software design modeled by finite-state machines[END_REF], which is often used in case studies deploying L (e.g. [START_REF] Chalupar | Automated reverse engineering using Lego R[END_REF][START_REF] De | Protocol state fuzzing of TLS implementations[END_REF]). We defer a thorough investigation of conformance testing to future work.

Fig. 1 :

 1 Fig. 1: L algorithm.

Fig. 2 :

 2 Fig. 2: Example run of L on L = {w ∈ {a} * | |w| = 1}.

Fig. 3 :

 3 Fig. 3: Example run of the L adaptation for NFAs on L = {w ∈ {a} * | |w| = 1}.

Definition 10 (

 10 Minimal T -Automaton for L). Let t L : A * → O A * be the function giving the residual languages of L, namely t L (u) = λv.L(uv). The minimal T -automaton M L accepting L has state space M = img(t L ), initial state init = t L (ε), and T -algebra homomorphisms out : M → O and δ : M → M A given by out(t L (U )) = L(U ) and δ(t L (U ))(a)(v) = t L (U )(av).

Fig. 4 :

 4 Fig. 4: Adaptation of L for T -automata.

  r is at most |S|, which is bounded by n in this optimized algorithm. For some examples (see for instance the writer automata in Section 7), we even have r = 1. The overall membership query complexity is O(tnk + tr log m).

Take the language {a p }, for some p ∈ N and a singleton alphabet {a}. Its residual languages are ∅ and {a i } for all 0 ≤ i ≤ p, thus the minimal DFA accepting the language has p + 2 states. However, the residual languages w.r.t. sets of words are all the subsets of {ε, a, aa, . . . , a p }-hence, the minimal T -automaton has 2 p+1 states.

Here and hereafter we assume that T (S ) ⊆ T (S), and more generally that T preserves inclusion maps. To eliminate this assumption, one could take the inclusion map f : S → S and write row t (T (f )(U )) instead of row t (U ).

When we refer to computational complexities, as opposed to query complexities, they are in terms of the sizes of S, E, and A.

This work was partially supported by the ERC Starting Grant ProFoundNet (grant code 679127), a Leverhulme Prize (PLP-2016-129), and the EPSRC Standard Grant CLeVer (EP/S028641/1).


Abdul-Hamid Soubra

Borut Macuh

SEISMIC ACTIVE AND PASSIVE EARTH PRESSURES ON RIGID RETAINING STRUCTURES BY A KINEMATICAL APPROACH

The seismic active and passive earth pressure problems are investigated by means of the kinematical method of the limit analysis theory. Two rotational kinematically admissible failure mechanisms Ml and M2 are proposed. Quasi-static representation of earthquake effects using the seismic coefficient concept is adopted. The solutions obtained are rigorous upper-bound ones in the framework of the limit analysis theory. The numerical results of the seismic active and passive earth pressure coefficients are presented and compared with other authors' results. These results improve the best available upper-bound solutions given by Chen and Liu (1990) in the active case and Soubra (2000) in the passive case. The best upper-bound solutions as given by the different upper-bound approaches are presented for practical use in geotechnical engineering.

INTRODUCTION

The well-known Mononobe-Okabe analysis of seismic lateral earth pressures (see [START_REF] Mononobe | On determination of earth pressure during earthquakes[END_REF][START_REF] Mononobe | On determination of earth pressure during earthquakes[END_REF][START_REF] Okabe | General theory on earth pressure and seismic stability of retaining walls and dams[END_REF]) is a direct modification of the Coulomb wedge method where the earthquake effects are replaced by a quasi-static inertia force whose magnitude is computed on the basis of the seismic coefficient concept. As in the Coulomb analysis, the failure surface is assumed planar in the Mononobe-Okabe method, regardless of the fact that the most critical sliding surface may be curved. Similar to Coulomb' s, the Mononobe-Okabe analysis may underestimate the active earth pressure and overestimate the passive earth pressure. In this paper, the seismic active and passive earth pressure problems are investigated by the upper-bound method of limit analysis using rotational log-spiral failure mechanisms. problems using kinematically admissible velocity fields. It should be noted here, that the upper-bound theorem gives an unsafe estimate of the active and passive failure load.

THEORETICAL ANALYSIS OF THE SEISMIC ACTIVE AND PASSIVE EARTH PRESSURE PROBLEMS

An earthquake has two possible effects on a soil-wall system. One is to increase the driving forces. The other is to decrease the shearing resistance of the soil. The assumptions made in the analysis can be summarized as follows:

THE UPPER-BOUND THEOREM OF LIMIT ANALYSIS The upper-bound theorem which assumes a perfectly plastic soil model with an associated flow rule, states that the rate of energy dissipation in any kinematically admissible velocity field can be equated to the rate of work done by the external forces, and so enables a strict upper-bound on the true limit load to be deduced (see [START_REF] Drucker | Extended limit design theorems for continuous media[END_REF], Chen 1975and SalenGon 1990). A kinematically admissible velocity field is one, which satisfies compatibility, the flow rule and the velocity boundary conditions. l Only the decrease (respectively increase) of the passive (respectively active) pressures due to the increase in driving forces is investigated under seismic loading conditions. The shear strength of the soil is assumed unaffected as the result of the seismic loading. l A constant seismic coefficient is assumed for the entire soil mass involved. Only the horizontal seismic coefficient K, is considered, the vertical seismic coefficient being often disregarded.

l An adhesive force P,, is assumed to act at the soil-structure interface. The intensity of this force is cd.tg&gqi.

Failure mechanisms

In this paper, the upper-bound theorem of limit analysis is applied to the seismic active and passive earth pressure Two rotational log-spiral failure mechanisms are considered in the present analysis. One for the active state Ml (cf. Thus, the surface BC is a surface of velocity discontinuity.

These failure mechanisms can be specified completely by two variables O,, and 8,.

As shown in Fig. 1, the external forces contributing to the total rate of external work consist of the weight of the soil mass in motion W, the active or passive earth force (P,,, or p,,J, the adhesive force P,, (P,,=c~f~fgs/tg~), the surcharge q,L acting on the ground surface and the different inertia forces. These inertia forces concern the soil mass and the surcharge loading. Since no general plastic deformation of the soil is permitted to occur, the energy is dissipated solely at the velocity discontinuity surface BC between the material at rest and the material in motion. The rate of energy dissipation per unit length along this velocity discontinuity can be expressed as [cf. Chen (197.5)] ~=cVcos@

(1) where V is the velocity which makes an angle 4 with the velocity discontinuity.

NUMERICAL RESULTS

The most critical earth pressure coefficients can be obtained by numerical maximization (respectively minimization) of the active (respectively passive) coefficients with regard to the parameters $ and 8,. The optimization procedure can be performed using the optimization tool available in most Paper No. 7.10 spreadsheet software packages. In this paper, one uses the Solver optimization tool of M icrosof? Excel. Two computer programs have been developed using Visual Basic ' VBA' to define the active and passive earth pressure coefficients as function of the two angular parameters $ and 0, defined in Fig. 1. In the following sections, the active and passive earth pressure coefficients obtained from the present analysis are presented and compared to those given by other authors.

Comparison of Results with Existing Solutions

In order to confirm the validity of the present upper-bound solution, the seismic active and passive earth pressure coefficients are calculated and compared with solutions given by other authors. Chang and Chen (1982) [cf. Chen and Liu 19901 considered a log-sandwich failure mechanism and gave rigorous upperbound solutions of the K,,e and Kay E coefficients. On the other hand, [START_REF] Soubra | Static and seismic passive earth pressure coefficients on rigid retaining structures[END_REF] has recently considered a translational multi-block failure mechanism for the study of the seismic passive earth pressure problem. His mechanism improves significantly the available upper-bound solutions given by [START_REF] Chen | Limit analy sis in soil mechanics[END_REF]. The comparisons between the present upper-bound solutions and the best available upper-bound solutions are presented in Figs. 2 and For the active case, the results given by the present approach are better than those presented by [START_REF] Chen | Limit analy sis in soil mechanics[END_REF], the improvement equals 11.5% for P/$=1/2 when are @=45" , &,b=l, &' +O and K,=O.3. For the passive case, the present upper-bound solutions are better than those of [START_REF] Soubra | Static and seismic passive earth pressure coefficients on rigid retaining structures[END_REF] for p>f5" , the improvement attains 20.1% for j?@=I when 4=45" , &$=I, ti$=O and K,=O.3. Therefore, the present failure mechanisms give interesting solutions of the seismic active and passive earth pressure coefficients. 1 and2.

It can be observed that for p/$=0, the passive earth pressure coefficients K,,e and K,,y, (respectively Ku% and KqE) decrease (respectively increase) with the KH increase. For the passive case, the decrease is more significant for looser soils with lower @ values than for denser soils with higher @ values. For example, for &@=I and ;r/~=~/+O, the reduction of the K,,$ coefficient is -25 -15 -5 5 15 25 35 45 equal to 10% for $=#_5" and attains 32% for P (" ) $=20" when KH increases from 0 to 0.3. From Table 1, one can see that for some configurations (see [START_REF] Soubra | Static and seismic passive earth pressure coefficients on rigid retaining structures[END_REF] for #=4.5" , &#=I, A.+=0 and K" =O.3

for instance @=40" , 6/@=2/3, /3/$=1/3, A/+0), the passive earth pressure coefficient Kpy, increases with the KH increase. This seems to be surprising. However, this result is logical for the present failure mechanism since in this case, the center of the log-spiral lies below the line of action of the surcharge inertia force (see Fig. 4) and thus, this force has the favorable effect of increasing the passive earth force. Finally, it should be mentioned that the seismic acceleration generated by earthquakes not only imposes extra loading to a soil mass but also shift the sliding surface to less favorable positions.

Paper Since there is no unique mechanism giving the best upperbound solutions, one presents in Tables 3 and4 the optimal upper-bound solutions. Table 3 gives the lowest upper-bound solutions given by both [START_REF] Soubra | Static and seismic passive earth pressure coefficients on rigid retaining structures[END_REF] and the present failure mechanism in the passive case and Table 4 gives the greatest solutions between the present upper-bounds and the solutions by [START_REF] Chen | Limit analy sis in soil mechanics[END_REF] in the active case. These tables give the best upper-bound solutions available in the literature and can be used by practicing geotechnical engineers.

CONCLUSIONS

Two rotational kinematically admissible failure mechanisms have been considered for the calculation of the seismic active and passive earth pressures using the upper-bound method of the limit analysis theory. The solutions presented are rigorous upper-bound ones in the framework of the limit analysis theory. The numerical results obtained lead to the following conclusions: For the passive case, the present rotational failure mechanism gives better upper-bound solutions of the K,,$ coefficient than the multi-block mechanism, the improvement attains 20. I % for @=45" , s&l, p@ =J, U$=O and KH=0.3. For the active case, the present results are also better than the ones given by Chen and Liu (1990), the improvement equals 11.5% for p@=1/2 when $=45" , &@=I, U@=O and KH=0.3. Finally, extensive numerical results of the best seismic active and passive earth pressure coefficients as given by the different upper-bound approaches are presented for practical use in geotechnical engineering.

  Fig. la) and the other for the passive state M2 (cf. Fig. lb).

Fig. 1 .

 1 Fig. 1. Log-spiral failure mechanisms (a) M l for active; and (6) M 2 for passive earth pressure analy ses

  By equating the total rate of external work to the total rate of internal energy dissipation, one can see that the work equation of the rotational log-spiral mechanism is identical to the moment equilibrium equation around the center of the logspiral. It should be emphasized that the moment equilibrium equation of the soil mass in motion can be written around the center of the log-spiral slip surface without specifying the normal stress distribution along the slip surface since the logspiral function has a particular property, that the resultant of the forces (0.dl) and (tan@a&) passes through the pole of the spiral. Hence, the seismic active and passive forces can be expressed respectively as follows PUE = K" , ,,d + Kp& where f&, K,,e, L,E, &,E, KucE and KpcE are the seismic earth pressure coefficients. The coefficients K, KY and Kc represent respectively the effect of soil weight, surcharge loading and cohesion and the subscripts a and p represent the active and passive cases respectively.

  Fig. 2. Comparison of present Ku* coefficient with that of Chen and Liu (1990) for +459&@ =l, k/$1=0 and KH=0.3

  ) the passive (respectively active) earth pressures. It is to be mentioned that the zyxwvutsrqponmlkjihg K,,cE and KurE $, K,,4E, KdsE and Ku+ are affected by earthquake, extensive numerical results based on the present failure mechanisms are presented in Tables

Fig. 3 .

 3 Fig. 3. Comparison of zyxwvutsrqponmlkjihgfedcbaZYXWVUTSRQPONMLKJIHGFEDCBA present K,,% coefficient with rhat of

Fig

  Fig. 4. Critical slip surfaces for 1$=40" , 6/1$=2/S, /Ih$=l/3, W I++and KH=O, 0.15, 0.3 (Passive Case)

Fig. 6 .

 6 Fig. 6. Critical slip suqaces for 1$=20' , &# ~=l, /3/qkU$=O and KH=O, 0.2 (Active Case)

Table 1 .

 1 Seismic passive earth pressure coefficients K,,e and K,,+ (l/@-d)

	#I" )

Table 2 .

 2 Seismic active earth pressure coefficients zyxwvutsrqponmlkjihgfedcbaZYXWVUTSRQPONMLKJIHGFEDCBA Ku

	K ud

* and KqE (J../q?=O)

Table 3 .

 3 Lowest upper-bound solutions for seismic passive earth pressure coefficients

zyxwvutsrqponmlkjihgfedcbaZYXWVUTSRQPO K,,$ and K,+ (p/$=~# =O)

					9(" )
	t?@ KH	20	25	30	35	40
	0	0	2.04	2.46	3.00	3.69	4.60
		0.15	1 .a0	2.21	2.73	3.39	4.27
		0.3	1.48	1.91	2.42	3.06	3.91
	l/3	0	2.39	3.07	4.03	5.44	7.62
		0.15	2.08	2.72	3.62	4.96	7.04
		0.3	1.64	2.28	3.13	4.39	6.33
	213	0	2.75	3.79	5.34	7.95	12.60
		0.15	2.37	3.32	4.79	7.25	11.68
		0.3	1.83	2.74	4.10	6.35	10.44

Table 4 .

 4 Greatest upper-bound solutions for seismic active earth pressure coefficients KU

* (k' qk0)

						K 4
	p/4	S/4	KH	20	25	30	35	40	REFERENCES
	0	0	0	0.49	0.41	0.33	0.27	0.22
			0.15	0.62	0.52	0.43	0.36	0.30
			0.3	0.83	0.66	0.57	0.48	0.40
		213	0	0.44	0.36	0.30	0.25	0.20
			0.15	0.58	0.48	0.4 1	0.34	0.28
			0.3	0.85	0.68	0.57	0.49	0.42
	l/3	0	0	0.54	0.45	0.37	0.31	0.25
			0.15	0.72	0.60	0.5 1	0.42	0.35
			0.3	1.21	0.97	0.75	0.61	0.51
		213	0	0.49	0.41	0.34	0.28	0.23
			0.15	0.70	0.59	0.49	0.42	0.35
			0.3	1.25	1.01	0.81	0.67	0.56

ACKNOWLEDGEMENT

The Ministry of Foreign Affairs in France and the Ministry of Science and Technology in Republic of Slovenia are gratefully acknowledged for their financial support.


Bjoern Gerold

Spiros Kotopoulis

Sandy Cochran

Michiel Postema

Paul Prentice

Hybrid laser-ultrasound cavitation for cloud evolution studies

We report on the development of an instrument for hybrid 'sonoptic' cavitation studies. A focused ultrasound transducer is housed in a custom-built chamber, which permits optical access to the focal volume, without perturbing the propagating acoustic waves. This configuration allows pulsed-laser irradiation of the liquid at the focus, and simultaneous high-speed observation of cavitation activity in this region. In this paper we provide a brief description of the apparatus and present preliminary data on the distinct cavitation regimes we have observed; specifically, laser-induced cavitation in an established field, and a new phenomenon that we refer to as laser-nucleated acoustic cavitation. The former involves a laser-pulse of energy above the threshold value for optical breakdown for the medium, in a pre-established ultrasound field. Here, a cavity rapidly expands to a maximum diameter of a few 100 µms, from the plasma generated on absorption of the optical energy, and collapses to form debris that is subsequently driven by the ultrasound radiation. By contrast, laser-nucleated acoustic cavitation is initiated by a pulse of energy below the breakdown threshold, in a pre-established field. For this regime, either form of radiation does not result in cavitation activity without the Gerold et al. -Hybrid laser-ultrasound cavitation for cloud evolution studies 52 other. In combination, the role of the laser-pulse is to initiate activity which is dominated by the ultrasound exposure from the outset. Crucially, the spatial and temporal precision afforded to the occurrence of cavitation by laser-nucleation, allows us to consolidate our assertion of acoustic cavitation. With observations at unprecedented resolutions, we compare the size of constituent cavities within a single acoustical cycle to theoretical predictions, based on the frequency of the ultrasound driving the activity.

It is expected that such observations will contribute to a greater understanding of cavitation in focused ultrasound, including for potential future therapeutic applications.

Introduction

Acoustic cavitation

Acoustic cavitation refers specifically to the formation and subsequent activity of bubbles, or cavities in the pressure fluctuations of an acoustic field, to distinguish from its mechanical or hydro-dynamical counterparts. The phenomenon is a common occurrence in the application of high intensity focused ultrasound (HIFU) fields to the ablation of diseased tissue, known as focused ultrasound surgery (FUS). In this emerging technique, ultrasound is focused transcutaneously to the site of pathology, thus alleviating the need for conventional surgical intervention, and associated risk of infection and extended patient recovery times. In current clinical procedure, the heating is achieved via viscous absorption of the mechanical energy [START_REF] Ter Haar | Ultrasound focal beam surgery[END_REF], which is most intense at the focus, where the pressure amplitudes are the largest within the field. Heating also occurs in surrounding healthy tissue, such as in the near-field, but at levels that are not harmful, provided the exposure is not prolonged.

Acoustic cavitation occurs in FUS when the rarefactional tension imposed on the tissue during a negative pressure phase, is sufficient to form microscopic cavities, which fill with gas and vapour extracted from the host tissue. The occurrence of the phenomenon depends on a complex mix of the physical properties of the tissue, and the ultrasonic exposure parameters [START_REF] Ter Haar | Ultrasound focal beam surgery[END_REF]. Continued HIFU excitation acts to further drive the bubble dynamics with a wide range of subsequent physical activity possible, including net growth through rectified diffusion, repulsion due to radiation forces, cloud formation via bubble-bubble interactions (fragmentation and coalescence), and free-radical production or sonochemistry (to mention but a few). It is generally recognized that cavitation in FUS has significant potential to mediate enhanced therapy, such as rapid tissue heating by 'trapping' of the acoustic energy at the focus, or promoting drug delivery via tissue extravasation and microstreaming/pumping [START_REF] Coussios | Role of acoustic cavitation in the delivery and monitoring of cancer treatment by high-intensity focused ultrasound[END_REF]. Translation of the phenomenon into medical practice is hampered, in part, by a fundamental lack of understanding of the rapid development of cavitation under HIFU exposure, and parallel development of acoustical detection techniques for monitoring and control purposes. Nonetheless, a growing body of literature demonstrates both active and passive methods of acoustical cavitation detection, and correlation to cavitation related bio-effects in tissue [START_REF] M C Glaughlin | A study of bubble activity generated in ex-vivo tissue by high intensity focused ultrasound[END_REF], and tissue-mimicking materials [START_REF] Holt | Measurements of bubble-enhanced heating from focused MHzfrequency ultrasound in a tissue-mimicking material[END_REF]. The deficit in understanding cavitation evolution, particularly over the first few hundred acoustic cycles, stem from several inherent difficulties in studying the phenomenon in vitro, including: [START_REF] Ter Haar | Ultrasound focal beam surgery[END_REF] uncertainty in predicting the exact location within the field, and moment, of cavitation inception, (2) ultra-fast dynamics, driven at the MHz frequencies typical for FUS applications, and (3) cavities in MHz fields tend to be of the order of a few microns. This may be theoretically inferred with the 'rule-of-thumb' simplified Minnaert's equation [5], for bubble radius, R f resonant to a central ultrasound frequency, f c , given by;

R f f c ≈ 3 ms -1
It may be appreciated that direct observational verification of bubble size is challenging for these reasons. Several studies have attempted to observe and characterize cloud evolution in HIFU fields with high-speed cameras, for example [START_REF] Chen | High-speed observation of cavitation bubble cloud structures in the focal region of a 1.2 MHz high-intensity focused ultrasound transducer[END_REF]. The best high-speed photography devices available are certainly capable of framing at the Nyquist sampling rate for MHz ultrasound, necessary to fully resolve dynamics. Microscopy objective lenses are also well capable of resolving objects on the micron scale. The researchers were, however, forced to image at spatial and temporal resolutions far below those necessary to make any meaningful observations of cavitation clouds, simply to guarantee the imaging of something! As such, they were restricted to presenting images of 'established' clouds on the millimetre scale, at 10 kHz sampling rates, with little impact on the understanding of the dynamical evolution.

Other researchers have resorted to less direct means for studying cavity sizes in acoustic fields. One such technique relies on sonoluminescence observations in pulsed ultrasound of varying inter-burst durations [START_REF] Lee | Determination of the size distribution of sonoluminescence bubbles in a pulsed acoustic field[END_REF][START_REF] Brotchie | Effect of power and frequency on bubble-size distributions in acoustic cavitation[END_REF], assuming quiescent bubbles dissolve over a period determined by the initial size. Brotchie et al [START_REF] Brotchie | Effect of power and frequency on bubble-size distributions in acoustic cavitation[END_REF] developed the technique to report that resonant bubble radii in a 1056 kHz field increase with acoustic power, up to some threshold intensity, at which stage R f stabilizes at ~5 µm.

Another approach, based on a similar principle, employed active pulse-receive acoustic detection of bubbles, nucleated via HIFU induced destruction of ultrasound contrast agents (UCAs) [START_REF] Chen | The disappearance of ultrasound contrast microbubbles: observation of bubble dissolution and cavitation nucleation[END_REF]. The authors used acoustic scattering to measure resonant dissolution times for 'freed bubbles' in a 1.1 MHz field -at pressure amplitudes similar to those of the present work -by comparing scattering patterns to models adjusted to account for the diffusivities of UCA core gases. Although they had to assume multiple size distributions to fit the data, features from the scattering amplitudes corresponded to R f 's ≈ 0.45, 1.2 and 1.56 µm.

Laser-induced cavitation

In contrast to its acoustic counterpart LIC is a very well characterized and understood phenomenon [START_REF] Fujimoto | Time-resolved studies of Nd:YAG laser-induced breakdown[END_REF], with interest driven largely by ophthalmology applications. This owes to the reliability and reproducibility of employing laser-pulses to generate a cavity at a location, pre-defined by the focal point of a lens, used to concentrate the optical energy into the host medium. LIC studies have contributed greatly to the understanding of especially single cavity activity, such as jet-formation in the presence of a boundary, and its dependence on the cavity-boundary distance [START_REF] Brujan | Dynamics of laser-induced cavitation bubbles near an elastic boundary[END_REF]. Although the laser-medium interaction (and to an extent the resulting cavity, such as the degree of asymmetry that evolves) depends somewhat on parameters such as the pulse duration [START_REF] Vogel | Shock wave emission and cavitation bubble formation by picoseconds and nanosecond optical breakdown in water[END_REF], it is well known that the process is plasma-mediated. Absorption of the optical energy at the focus causes localized weak breakdown to form a plasma, which rapidly expands to form a 'hot' cavity of vapour and gas. The requirement for plasma formation imposes an energy threshold on the pulse, below which breakdown does not occur, and a cavity does not form. These factors also translate to a typical lower bound for the maximum diameter LIC bubbles can have, following the initial inflation stage -generally a few 100 µm, with millimetre-sized bubbles being commonly investigated.

In this paper we describe a sonoptic chamber for hybrid laser-acoustic cavitation studies. We use a propagating HIFU field, and introduce cavitation activity by optically focusing a nanosecond laser-pulse into the US focal volume. We have found that reducing the pulse energy to below the breakdown threshold for the system, allows cavitation nucleation, without the characteristically large (relative to R f determined by the field frequency f c ) bubble formation associated with conventional LIC.

Methodology

The hybrid laser-ultrasound experimental platform has been described in detail elsewhere [START_REF] Gerold | Laser-nucleated acoustic cavitation in focused ultrasound[END_REF], but a short overview is given here for background. The key feature is the sonoptic chamber that accommodates a HIFU field, the focal region of which can be irradiated with a laser-pulse and observed through a microscope objective lens. We employ a 3 nanosecond frequency-doubled neodymium-doped yttrium aluminium garnet (Nd:YAG) laser-pulse for cavitation induction and nucleation. The pulse is steered into the back aperture of a long working distance objective lens (Mitutoyo 50× 0.42 NA MPlan NIR ∞-corrected), from a dichroic mirror reflective to the laser wavelength, 532 nm. The sonoptic chamber is custom-built to 'fit' the HIFU field of a 1.47 MHz focused-bowl transducer, such that the field propagates unhindered by reflection or scattering -other than from cavitation intentionally introduced to the focal region. In this way unwanted interference effects are avoided, and the focused ultrasound may be expected to propagate as it would in an idealised FUS procedure. Fig. 1 (a) depicts the dual focus (optic and ultrasonic) region of the apparatus, schematically. The central glass box is the 'confocal chamber' and contains the liquid which hosts the cavitation activity reported below. The objective lens configuration of fig. 1 (a) is that used for the observations reported, whereby ones lens focuses the laser and a second orthogonally orientated lens (Mitutoyo 5× 0.14 NA MPlan APO ∞corrected) is used for imaging purposes. This configuration decouples the laser axis from the imaging and allows the laser spot to be translated independently (as distinct from imaging through the focusing lens as described previously [START_REF] Gerold | Laser-nucleated acoustic cavitation in focused ultrasound[END_REF]). Fig. 1 (b) and(c) depicts the US focus within the confocal chamber, where cavitation is instigated. The transducer is driven by a sinusoid signal from a function generator (Tektronix) passed through an RF power amplifier (Electronics and Innovation) and impedance matching network. Alignment of the ultrasonic and laser foci is critical to reproducibility, and is achieved through Schlieren imaging to visualise the ultrasound focus, and translation of the chamber to coincide to the laser spot, inset Fig. 1 (a), [START_REF] Palanchon | Optical observations of acoustical radiation force effects on individual air bubbles[END_REF]. Two high-speed cameras were used for the collection of the data presented below, courtesy of the EPSRC instrument loan pool, the Shimadzu HPV-1 and Cordin 550-62. The former is capable of 100 frames at up to 1 Mfps, the latter 62 frames at up to 4 Mfps. The Cordin is a compressed gas-driven rotating drum device, with a formidable reputation. The sensitive optics of the cameras are protected from scattered laser radiation with a green optical filter.

Quoted laser-pulse energies are measured at the back aperture of the objective lens with a power meter (ThorLabs), and HIFU peak negative pressure (PNP) amplitudes with a fibre-optic hydrophone (Precision Acoustics). Spatial scales for the high-speed images presented were determined by imaging flow cytometry beads of diameters 10 and 50 µm, in situ. For an experiment, the laser is switched to single pulse mode and triggered from the high-speed camera, with an appropriate delay for the Q-switch. The HIFU field is pre-established (turned on) 5-10 seconds before the laser-pulse is generated, and high-speed photography initiated. All the results presented below use degassed (to < 4 mgL -1 of dissolved oxygen) tap water as the host medium. The optical breakdown threshold for the system, defined as the pulse energy below which no LIC was observed, was determined to be 1.10 ± 0.02 mJ, where the error is attributed to instrumental fluctuations in the pulse energies generated, according to the user manual, and consistent with our own power meter measurements.

Results and Discussion

Fig. 2 (a)-(d) represents the various forms of laser-acoustic cavitation that may be studied with the experimental architecture described. Sequence 2 (a) is representative of conventional LIC, as described in the introductory section above. A 1.20 ± 0.02 mJ pulse is focused into the water, of sufficient energy to cause optical breakdown and plasma formation. A spherical cavity of gas and vapour subsequently expands over ~40 µs to a maximum radius, R max ≈300 µm. The inertia of the liquid acts to collapse the cavity over the next ~40 µs, which then oscillates through a series of rebounds, with a period of ~20 µs.

The cavitation debris in the aftermath of the primary LIC is subject to two further stimulations, at ~110 and ~190 µs. It is well known that plasma formation through the absorption of a laser pulse generates a spherically radiating acoustic transient, as does the collapse of an LIC [START_REF] Fujimoto | Time-resolved studies of Nd:YAG laser-induced breakdown[END_REF][START_REF] Vogel | Shock wave emission and cavitation bubble formation by picoseconds and nanosecond optical breakdown in water[END_REF]. As the absorption occurs at ~0 µs and the collapse at ~80 µs, this would imply a propagation time ≈110 µs, for the each of the transients to return to the site of cavitation. Taking the speed of sound in water as 1500 ms -1 , this translates to a total propagation distance of ≈ 16 cm. We thereby infer that the transients are reflected, and effectively re-focused, from the spherically curved transducer (of geometric focus 80 mm, see above), as opposed to the walls of the confocal chamber.

Sequence 2 (b) is a recording of the cavitation activity that resulted from a 1.20 ± 0.02 mJ laser-pulse focused into the HIFU field with measured PNP = 1.3 ± 0.15 MPa The early stages of the dynamics are clearly dominated by LIC, with rapid bubble expansion to an R max ≈ 300 µm, i.e. comparable to that of 2 (a); LIC without ultrasound radiation. The collapse time is also seemingly unaffected by the ultrasound. The only notable differences are the larger volume of cavitation debris and a slight upwards translation (~50 µm at 190 µs, indicated by a line drawn across the images in question, fig. 2) in the centroid of the cloud, in the case of ultrasound radiation being present. We attribute these effects to bubble fragmentation events under the added acoustic energy available to the system, and the action of the primary radiation force [5,[START_REF] Palanchon | Optical observations of acoustical radiation force effects on individual air bubbles[END_REF] (buoyancy is negligible over these timescales, and in any case would act equally in both scenarios).

Sequence 2 (c) captures the cavitation activity resulting from a laser-pulse of 0.95 ± 0.02 mJ incident to the same location as in 2 (b), and in an equivalent field. Such a low energy laser-pulse does not produce any cavitation activity, without the pre-established US field. More than fifty tests were undertaken to confirm this. This sequence is representative of the minimal amount of cavitation activity we observed, which consists of a single small nucleus of <10 µm (arrowed black throughout sequence), which proceeds to translate upwards. We term this activity laser-nucleated acoustic cavitation (LNAC), to distinguish it from LIC in an established US field, 2 (b).

Note that the translation speed is approximately constant throughout the sequence and commences from the moment of nucleation. This is in contrast to the LIC in the preestablished field, the centroid of which does not notably translate for the first ~100 µs. However, the translations speed of the debris cloud of 2 (b) and the LNAC of 2 (c) are comparable, as one would expect in an ultrasound field of equivalent intensity. Fig. 2 (d) depicts LNAC, again with a laser pulse energy of 0.95 ± 0.02 mJ, incident to the focal volume of a much higher intensity field, of PNP = 4.1 ± 0.5 MPa. As for sequence 2 (c), absorption results in a small cavity nucleus that rapidly develops into a cloud of interacting cavities, which translate as a single entity away from the HIFU source. Although the drag may be expected to be greater for this cloud, than for the cavitation of 2 (c), the translation speed is much higher due to the dependence of the radiation force on the square of the pressure amplitude [5,15].

force on the square of the pressure amplitude [5,15]. To consolidate our assertion that fig. 2 (c andd) is cavitation that is acoustic in nature, we now consider the size of the component structures within the cloud. In fig. 2 the imaging rate is less than the HIFU frequency, which is adequate to image cloud morphology evolution and translation, but insufficient to resolve component cavity dynamics. The relatively long exposure times used to capture these images result in 'objects' becoming smeared over a region of pixels, as they oscillate under the influence of the incident US. As such, the best we can expect to infer is an upper bound on the maximum diameter during the oscillation. Moreover, this assumes no translation, coalescence, non-symmetrical dynamics etc., which is evidently not the case, and could lead to erroneous measurements.

Fig. 3 (a-f) are close-ups of six consecutive frames extracted from a sequence recorded at 3.05 Mfps, at an 'advanced' stage of LNAC cloud evolution, some 15.8 µs following laser-pulse absorption and initial recorded cavitation activity. This sampling rate satisfies the Nyquist criterion for the 1.47 MHz HIFU frequency used, and as such allows quasi-resolved observation within a single acoustical cycle. Each frame represents an integration of the cavity dynamic over an exposure time significantly less than the inter-frame time of 0.33 µs, compared to the duration of a negative or positive phase of the ultrasound, which at half the period ≈ 0.34 µs. The HIFU driving this cavitation was of PNP = 2.20 ± 0.26 MPa. This 'mini-sequence' records the cloud through just more than 2 cycles of US propagation. Intuitively, 3 (a)-(c) was recorded during a negative-positive-negative cycle, with (d)-(f) capturing an expansion phase during a negative-positive transition. Fig. 3 (b andd) in particular, allow us to put an upper limit on the minimum radius, R min , of some of the cavities within the cloud, of the order of a few µms. We estimate that equivalent features in the negative pressure phases of the incident US have R max 's in the range of ~10 µms. This would put many of the observable cavities at around the resonant size for the frequency used, in accordance with published literature. We also note that although the apparent translation under the action of the primary radiation force is much reduced from that observed in fig. 2 (d) -due to both reduced US intensity and increased frame rate for sequence acquisition -this might still result in a slight overestimate to the feature dimensions.

Conclusions

In conclusion, we present preliminary observations on a new technique that allows what appears to be predominantly acoustic cavitation to be nucleated, or seeded, by a nanosecond laser-pulse in an acoustic field. Crucially, the dominance of a large laser-induced bubble is avoided by reducing the pulse energy. The key advantage is the spatial and temporal precision the technique affords, which allows the incorporation of ultra-high speed micro-photography, at the resolutions required to observe cloud formation and evolution.

Figure 1 .

 1 Figure 1 . Sche matic r epre sentatio n o f the son optic ch ambe r, ho using the u ltrasou nd focal volu me, an d the op ti ca l focu s of a lase r pu lse p assed th rou gh a l ong working di sta nce microscop e ob jective le ns. In set is a schli eren imag e of the fo cal vol ume (l ighter blu e) u se d to al ign th e op ti ca l focus (g ree n spo t) . S imula te d, an d to -scale re prese ntation of the ( a) tran sve rse, and (b) axial fo cu s of th e HIFU fie ld, w ithin the con fo cal re gio n of the so nop ti c chamb er, wh ich has dimen sions: 20x20 x1 4mm. Hig her pe ak pressur es a re ind icated red , with amb ient atmosph eric pr essure r epre sented a s d eep er b lue. It can be see n that the chamb er ho using d oes no t inte rfe re with the pr opa gating p ressur e fie ld.

Figure 2 -

 2 Figure 2 -Selected individual frames extracted from high speed sequences recorded with the Shimadzu HPV-1 camera operating at 0.5 Mfps (x10 6 frames per second), depicting the various regimes of laser-ultrasound cavitation that may be studied with the apparatus: (a) Laser-induced cavitation (LIC) formed with a laser pulse of above the breakdown threshold, (b) LIC in a low intensity ultrasound field. The line across the 190 µ s images serves to indicate the upwards translation of the debris cloud in the presence of ultrasound. (c) Laser nucleated acoustic cavitation (LNAC) with a laser-pulse below the breakdown threshold, in a low intensity, pre-established ultrasound field, and (d) LNAC in a high intensity, pre-established field. Each frame is 1.2 mm in width.

Figure 3 .

 3 Figure 3. Con se cu ti ve frames extracted fr om an u ltra hi gh-spee d seq uen ce of a LNA C clo ud in the e arly stage s o f d ev el opmen t in a n in te rmedi ate inte nsity fie ld. This sequ ence wa s r ecord ed at 3.05 Mfps, with ti mi ngs of e ach image a cq uisitio n a s in dicated . (a ) A clo ud of e xpan ded cavities (a lte rna ti ve ly, of high ' vo id fr action' , de fin ed as th e ratio of gas pha se vol ume to liq uid ph ase vo lume) ind icates a ra refaction al ne gative pre ssur e a mplitud e p hase of the pro pag ating ul tra soun d in th e lo ca le o f the cloud . (b) A t ~0.33 µs later th e clo ud a ppe ars to be compose d of compr esse d ca vi ti es (o r is of a lower void fraction ) ther eby in dicating a postive pre ssur e compr essi ona l ph ase of the ul tr asoun d is acting a t the time o f ima ge acq uisition . Note, an fc of 1.47 MHz u se d for th is work e qua te s to a pre ssu re p hase o sci llatio n pe riod of ! 0.7µ s. (c) -(f) Con tin ued cycling un der the pro pag ating HIFU pre ssu re fl uctu ation s. Ima ge acqui stio n wa s thro ugh the 5 x o bjective le ns i n th e ortho gon al config uratio n.

Acknowledgements

The research leading to these results has received funding from the European Community's Seventh Framework Programme (FP7/2007-2013) under grant agreement n° 230674 (Nanoporation project).

Paul Prentice acknowledges the Norwegian Research Council for Yggdrasil mobility award no. 210949/F11. We are particularly grateful to Mr Adrain Walker of the EPSRC instrument loan pool, for continued access to various high-speed imaging devices.