Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Extended Abstract (adapted from the introduction of [14])

This invited talk presents the work conducted on the problems that arise when dealing with weighted automata containing \(\varepsilon \)-transitions: how to define the behaviour of such automata in which the presence of \(\varepsilon \)-circuits results in infinite summations, and second how to eliminate the \(\varepsilon \)-transitions in an automaton whose behaviour has been recognised to be well-defined. The origin of this work is the implementation, in the Awali platform [19], of an \(\varepsilon \)-transition removal algorithm for automata with weight in \(\mathbb {Q}\) or \(\mathbb {R}\), a case that had never been treated before in the rich literature on the subject of \(\varepsilon \)-transition removal algorithms (cf.  [16] for a survey). The results of this work have been published in [14].

The equivalence between non-deterministic finite automata (NFA) and non-deterministic finite automata with \(\varepsilon \)-transitions (\(\varepsilon \)-NFA) is a basic result in the theory of finite automata (e.g. in [10]). Besides the proof that \(\varepsilon \)-transitions do not increase the power of the computation model, this equivalence allows simple constructions; hence the interest in the construction of NFA from \(\varepsilon \)-NFA which amounts to the computation of the transitive closure of the graph of \(\varepsilon \)-transitions, more or less intertwined with the construction of the NFA itself.

Automata with weights taken in semirings have been considered since the beginning of the 60’s and the recent investigations on quantitative evaluation of systems make them of current interest. Removal of \(\varepsilon \)-transitions is of equal importance for weighted automata as for Boolean ones, but even the definition of the behaviour of a weighted automaton with \(\varepsilon \)-transitions is not so obvious: if the graph of \(\varepsilon \)-transitions contains a circuit, then the sum of the weights along the paths following this circuit may well be not defined, as for instance in the automaton \(\mathcal {Q}_{1}\) of Fig. 1(a). For that reason, some of the most mathematically oriented works on automata, such as [1] or [12], have ruled out the possibility of having circuits of \(\varepsilon \)-transitions in automata, either explicitly with the hypothesis of cycle-free automata, or implicitly by considering the discrete topology on the weight semiring. As a result, the automaton \(\mathcal {Q}_{2}\) of Fig. 1(b) is also considered as an illegitimate object. Yet, the natural topology on \(\mathbb {Q}\) or \(\mathbb {R}\) should allow to consider that such weighted automata with circuits of \(\varepsilon \)-transitions may be valid.

Fig. 1.
figure 1

A non-valid automaton \(\mathcal {Q}_{1}\), and \(\mathcal {Q}_{2}\) that should be considered valid

Full size image

The definition of the behaviour of weighted automata with \(\varepsilon \)-transitions requires a theoretical framework in which it is possible to define infinite sums, at least some particular ones. It appears indeed that these infinite sums are created by the paths along a circuit (as in the loops in Fig. 1) and may be expressed by the star operator.

A first approach to solving the issue of infinite sums, which we call the axiomatic approach, is the setting of a framework in which the star operator is always defined — making the previous evaluation always possible — and satisfies a number of axioms that guarantee the behaviour be well-defined and the evaluation correct. This yields on one hand the notions of complete, and continuous, semirings (cf. [2, 4, 7, 11]), and on the other the notion of Conway and partial Conway semirings (cf. [2, 3, 9]). The weighted automata we want to deal with, such as probabilistic or distance automata, are natural computational models, while their weight semirings (e.g. \(\mathbb {Q}\), \(\mathbb {R}\) or \(\mathbb {Z}\mathsf {min}\)) are neither complete nor continuous nor partial Conway semirings. In order to address these cases, we have made the choice in our previous work ([17, 18]) of a topological approach to infinite sums and to the notion of summability of infinite families.

A natural definition for a valid automaton is then that the family of all computations be summable, that is, that for every word w the family of weights of paths with label w be summable. One may be more cautious, and require that for every pair of states the family of weights of paths between these states and with label w be summable. This definition, taken in [17, 18], yields a consistent theory; it however conceals the weakness of not being effective as it says nothing on how one can compute or decide that an infinite family is summable. As noted above, the evaluation of infinite sums is made through the star operator, which implies block summations. And then, computations are likely to meet two pitfalls, different, and almost opposite:

  1. 1.

    A subfamily of a summable family is not necessarily summable, and an evaluation may fail on what is considered as a ‘valid’ automaton. Such a situation occurs with the automaton \(\mathcal {T}_{2}\) of Fig. 2(a) whose weights are in \(\mathbb {N}_{\infty }\), the semiring  equipped with the discrete topology, where an infinite sum is defined if, and only if, almost all terms are 0, or at least one term is . The sum of the weights of paths in this automaton is therefore defined, but the evaluation of this sum through the star operator may require to compute the star of 1 which is not defined.

  2. 2.

    On the other side, it is well-known that block summations may give values to non summable families. Automaton \(\mathcal {Q}_{3}\) of Fig. 2(b) yields an example of such a phenomenon. Weights of \(\mathcal {Q}_{3}\) are in \(\mathbb {Q}\) where, for every x in \(]-1;1[\), the star of x is defined and is equal to \((1-x)^{-1}\). The usual formula for the evaluation of the computations labelled by \(\varepsilon \) gives but a direct computation on the transition matrix M yields which shows that computations grouped by length are not summable.

Fig. 2.
figure 2

The two pitfalls of the \(\varepsilon \)-removal computations

Full size image

We therefore take a stronger definition of validity: we will say that a weighted automaton is valid if the sum of weighted labels of every rational set of paths is well-defined. This definition has several outcomes. It insures first that in any kind of semirings, any (reasonable) \(\varepsilon \)-removal algorithm will succeed on every valid weighted automaton and turn it into an equivalent proper automaton. Second, this definition is not as restrictive as it may appear. It rules out tricky examples in awkward semirings (such as \(\mathbb {N}_{\infty }\)) but coincides with the former definition in all cases of usual semirings. It encompasses the cases treated with the axiomatic approach where indeed the decision of validity is trivial. Finally, this definition provides a framework in which the closure algorithm yields a decision procedure for the validity of automata in the cases we wanted to treat. All in all, this definition of validity is more complex than the other ones but fulfills our goals without narrowing its domain of application.

A byproduct of this definition of validity is the stability and consistency with natural transformations of automata: a subautomaton of a valid automaton is valid and so is a covering (kind of unfolding) of a valid automaton. The validity of automata is also consistent with that of rational expressions, provided the transformation of the latter into the former does not artificially introduce \(\varepsilon \)-transitions. This last condition brings to light a weakness of Thompson’s construction compared to the other classical ones.

After the definition of validity, the next step is the computation of the behaviour of an automaton, which amounts to describing algorithms for \(\varepsilon \)-transition removal. It begins with the study of the relationships between the validity of an automaton and the starability of its transition matrix. In the axiomatic approach, the behaviour of an automaton is defined by the star of the transition matrix and the problem is to set up conditions that guarantee its starability. The topological approach goes in the opposite direction and an automaton which is not valid may well have a starable transition matrix. It is proved that under the condition that an automaton is valid, its transition matrix is starable and the classical formulas can be applied to compute the star. This leads to a first family of algorithms that have been abundantly described in the literature ([13, 15, 16]).

Another family of algorithms, hardly less classical, is based on the iteration of elementary operations of suppression of \(\varepsilon \)-transitions. The correctness comes from the correctness of each elementary operation, but the termination of the algorithm has to be carefully checked.

The final task is to address the problem of deciding the validity of an automaton. The success of an algorithm on a given automaton is not a sufficient condition for the automaton be valid. There is no general and uniform answer to the problem and that the existence, and the details, of a solution will depend on the properties of the weight semiring. It is for instance classical that the only valid automata with weights in \(\mathbb {N}\) or \(\mathbb {Z}\) are those with no circuits of \(\varepsilon \)-transitions, a decidable property. The opposite case, that is, the one in which every automaton is valid, and which meets the class of rationally additive semirings of [8], is also characterised.

The cases in-between, that is, semirings such that some, but not all, automata with circuits of \(\varepsilon \)-transitions are valid, is a new area of reasearch. In this work, it is established that the validity of \(\mathbb {K}\)-automata is decidable — decided by the success of the algorithm quoted above — when \(\mathbb {K}\) is a topological (partially) ordered positive semiring (TOPS) with the property that the domain of the star operator is downward closed. This class of semirings contains for instance \(\mathbb {Q}_+\), \(\mathbb {R}_+\), \(\mathbb {Z}\mathsf {min}\) (and all the tropical semirings). Moreover, in starable TOPS — such as for instance the semiring \({{\mathrm {Rat}\,A^{*}}}\) of rational languages over \(A^{*}\) — every weighted automaton is valid and this class contains the continuous semirings (cf. [5]).

With a last step, the decidability problem for \(\mathbb {Q}\)- or \(\mathbb {R}\)-automata is reduced to the one for automata with weights in TOPS by considering the absolute value of such automata. The initial goal of solving the problem of \(\varepsilon \)-transition removal algorithm for \(\mathbb {Q}\)- or \(\mathbb {R}\)-automata is then reached: we have both the theoretical justification and the algorithm that allows to transform the automaton \(\mathcal {Q}_{4}\) of Fig. 3(a) into the automaton \(\mathcal {Q}_{5}\) of Fig. 3(b).

Fig. 3.
figure 3

A transformation which needs theoretical foundation

Full size image

As a last remark, it can be mentioned that, for sake of simplicity, the only automata considered in this work are the weighted automata over free monoids, but the same definitions, constructions and results hold for automata over graded monoids (that is, monoids with a length), and thus in particular for transducers.

This work fills the effectivity gap that was left open by our definition of valid automata in [17, 18]. In general, the success of any \(\varepsilon \)-removal algorithm may never insure the validity of an automaton. In order to reach a decidability procedure, we have been led to a strong definition of validity, which implies stability under automata transformations that are paths preserving. The algorithms described in this work are implemented in Awali [19].